Merge pull request #2884 from FStarLang/guido_range

Unifying the range type into FStar.Range
FStarLang · Apr 21, 2023 · 20039e9 · 20039e9
2 parents d36f875 + b419530
commit 20039e9
Show file tree

Hide file tree

Showing 67 changed files with 6,271 additions and 5,923 deletions.
diff --git a/doc/book/code/Vec.ml b/doc/book/code/Vec.ml
@@ -176,9 +176,9 @@ let (implies_intro :
   =
   fun uu___ ->
     FStar_Tactics_Effect.tac_bind
-      (Prims.mk_range "Vec.fst" (Prims.of_int (160)) (Prims.of_int (2))
+      (FStar_Range.mk_range "Vec.fst" (Prims.of_int (160)) (Prims.of_int (2))
          (Prims.of_int (160)) (Prims.of_int (14)))
-      (Prims.mk_range "Vec.fst" (Prims.of_int (161)) (Prims.of_int (2))
+      (FStar_Range.mk_range "Vec.fst" (Prims.of_int (161)) (Prims.of_int (2))
          (Prims.of_int (161)) (Prims.of_int (9)))
       (Obj.magic
          (FStar_Tactics_Derived.apply

diff --git a/ocaml/fstar-lib/FStar_Range.ml b/ocaml/fstar-lib/FStar_Range.ml
@@ -1,2 +1,7 @@
-type range = FStar_Compiler_Range.range
-let prims_to_fstar_range = FStar_Compiler_Range.prims_to_fstar_range
+type __range = FStar_Compiler_Range.range
+type range = __range
+
+let mk_range f a b c d = FStar_Compiler_Range.mk_range f {line=a;col=b} {line=c;col=d}
+let range_0 : range = let z = Prims.parse_int "0" in mk_range "<dummy>" z z z z
+
+type ('Ar,'Amsg,'Ab) labeled = 'Ab
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Util.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Propositions.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Propositions.ml
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_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_Arith.ml b/ocaml/fstar-lib/generated/FStar_Reflection_Arith.ml