Parser.Dep: make --dep full output relative paths

Add Filepath.make_relative_to_cwd to convert absolute paths to
paths relative to the current working directory. Use it in
print_full's norm_path so that .depend files contain portable
relative paths instead of machine-specific absolute paths.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: Lef Ioannidis

src/basic/FStarC.Filepath.fsti

@@ -35,3 +35,6 @@ val canonicalize : string -> string
 
 (* Like canonicalize, but always returns an absolute path. *)
 val normalize_file_path: string -> ML string
+
+(* Make a path relative to the current working directory. *)
+val make_relative_to_cwd: string -> ML string

src/ml/FStarC_Filepath.ml

@@ -63,3 +63,20 @@ let file_exists = Sys.file_exists
 (* Sys.is_directory raises Sys_error if the path does not exist *)
 let is_directory f = Sys.file_exists f && Sys.is_directory f
 
+let make_relative_to_cwd (path:string) : string =
+  if not (is_path_absolute path) then path
+  else
+    let path = normalize_file_path path in
+    let cwd  = normalize_file_path (Sys.getcwd ()) in
+    let split s = List.filter (fun x -> x <> "") (BatString.nsplit s ~by:"/") in
+    let path_parts = split path in
+    let cwd_parts  = split cwd  in
+    let rec skip_common pp cp =
+      match pp, cp with
+      | ph :: pt, ch :: ct when ph = ch -> skip_common pt ct
+      | _ -> (pp, cp)
+    in
+    let (remaining_path, remaining_cwd) = skip_common path_parts cwd_parts in
+    let ups = List.map (fun _ -> "..") remaining_cwd in
+    String.concat "/" (ups @ remaining_path)
+

src/parser/FStarC.Parser.Dep.fst

@@ -2067,7 +2067,10 @@ let print_full (outc : out_channel) (deps:deps) : ML unit =
     in
     let sb = FStarC.StringBuffer.create 10000 in
     let pr str = ignore <| FStarC.StringBuffer.add str sb in
-    let norm_path s = replace_chars (replace_chars s '\\' "/") ' ' "\\ " in
+    let norm_path s =
+      let s = Filepath.make_relative_to_cwd s in
+      replace_chars (replace_chars s '\\' "/") ' ' "\\ "
+    in
     let print_entry (target : string) (all_deps : list string) : ML unit =
         (* Print a target with dependencies. *)
         pr target; pr ":";