Merge pull request #3758 from mtzguido/range_basename

FStarC.Range: always use basenames
FStarLang · Feb 15, 2025 · d5e2783 · d5e2783
2 parents e67d0f9 + ccd171d
commit d5e2783
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 14 deletions.
diff --git a/src/basic/FStarC.Range.Ops.fst b/src/basic/FStarC.Range.Ops.fst
@@ -50,12 +50,10 @@ let rng_included r1 r2 =
 
 let string_of_pos pos =
     format2 "%s,%s" (string_of_int pos.line) (string_of_int pos.col)
-let file_of_range r       =
-    let f = r.def_range.file_name in
-    string_of_file_name f
-let set_file_of_range r (f:string) = {r with def_range = {r.def_range with file_name = f}}
+let file_of_range r = r.def_range.file_name
+let set_file_of_range r (f:string) = {r with def_range = {r.def_range with file_name = Filepath.basename f}}
 let string_of_rng r =
-    format3 "%s(%s-%s)" (string_of_file_name r.file_name) (string_of_pos r.start_pos) (string_of_pos r.end_pos)
+    format3 "%s(%s-%s)" r.file_name (string_of_pos r.start_pos) (string_of_pos r.end_pos)
 let string_of_def_range r = string_of_rng r.def_range
 let string_of_use_range r = string_of_rng r.use_range
 let string_of_range r     = string_of_def_range r
@@ -142,7 +140,11 @@ instance pretty_range = {
 (* See FStarC.Find.refind_file, this just applies it to both filename
 components. *)
 let refind_rng (r:rng) : rng =
-  { r with file_name = FStarC.Find.refind_file r.file_name }
+  { r with file_name =
+      if Options.Ext.enabled "fstar:no_absolute_paths"
+      then r.file_name (* already a basename *)
+      else FStarC.Find.refind_file r.file_name
+  }
 
 let refind_range (r:range) : range =
   { r with

diff --git a/src/basic/FStarC.Range.Type.fst b/src/basic/FStarC.Range.Type.fst
@@ -45,6 +45,8 @@ instance ord_pos : ord pos = {
 [@@ PpxDerivingYoJson; PpxDerivingShow ]
 type rng = {
   file_name:file_name;
+  (* ^ Note: this must be a basename, without any directory components. The
+  interface should protect this fact. *)
   start_pos:pos;
   end_pos:pos;
 }
@@ -85,19 +87,13 @@ let mk_pos l c = {
     col=max 0 c
 }
 let mk_rng file_name start_pos end_pos = {
-    file_name = file_name;
+    file_name = Filepath.basename file_name;
     start_pos = start_pos;
     end_pos   = end_pos
 }
 
 let mk_range f b e = let r = mk_rng f b e in range_of_rng r r
 
-let string_of_file_name f =
-  if Options.Ext.enabled "fstar:no_absolute_paths" then
-    Filepath.basename f
-  else
-    f
-
 open FStarC.Json
 let json_of_pos (r: pos): json
   = JsonAssoc [
@@ -106,7 +102,7 @@ let json_of_pos (r: pos): json
     ]
 let json_of_rng (r: rng): json
   = JsonAssoc [
-      "file_name", JsonStr (string_of_file_name r.file_name);
+      "file_name", JsonStr r.file_name;
       "start_pos", json_of_pos r.start_pos;
       "end_pos", json_of_pos r.end_pos;
     ]