Merge pull request #3428 from mtzguido/range

ulib: FStar.Range: allow inspecting the unsealed __range
FStarLang · Sep 1, 2024 · 5db2e80 · 5db2e80
2 parents a920424 + 6f4160a
commit 5db2e80
Show file tree

Hide file tree

Showing 17 changed files with 1,750 additions and 250 deletions.
diff --git a/ocaml/fstar-lib/FStar_Range.ml b/ocaml/fstar-lib/FStar_Range.ml
@@ -5,4 +5,11 @@ let mk_range f a b c d = FStar_Compiler_Range_Type.mk_range f {line=a;col=b} {li
 let range_0 : range = let z = Prims.parse_int "0" in mk_range "dummy" z z z z
 let join_range r1 r2 = FStar_Compiler_Range_Ops.union_ranges r1 r2
 
+let explode (r:__range) =
+  (r.use_range.file_name,
+   r.use_range.start_pos.line,
+   r.use_range.start_pos.col,
+   r.use_range.end_pos.line,
+   r.use_range.end_pos.col)
+
 type ('Ar,'Amsg,'Ab) labeled = 'Ab
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml