Some library reorg

src/parser/FStarC.Parser.Const.fst

@@ -573,7 +573,7 @@ let fext_on_dom_g_lid = fext_lid "on_dom_g"
 
 let sealed_lid      = p2l ["FStar"; "Sealed"; "sealed"]
 let seal_lid        = p2l ["FStar"; "Sealed"; "seal"]
-let unseal_lid      = p2l ["FStar"; "Tactics"; "Unseal"; "unseal"] (* In a separate module due to the mention of TAC *)
+let unseal_lid      = p2l ["FStar"; "Stubs"; "Tactics"; "Unseal"; "unseal"] (* In a separate module due to the mention of TAC *)
 let map_seal_lid    = p2l ["FStar"; "Sealed"; "map_seal"]
 let bind_seal_lid   = p2l ["FStar"; "Sealed"; "bind_seal"]
 let tref_lid        = p2l ["FStar"; "Stubs"; "Tactics"; "Types"; "tref"]

tests/Makefile

@@ -20,6 +20,7 @@ ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
 ALL_TEST_DIRS += simple_hello
+ALL_TEST_DIRS += dune_hello
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))

tests/dune_hello/.gitignore

@@ -0,0 +1,3 @@
+*.ml
+_build
+lib

tests/dune_hello/Hello.fst

@@ -0,0 +1,5 @@
+module Hello
+
+open FStar.IO
+
+let _ = print_string "Hi!\n"

tests/dune_hello/Makefile

@@ -0,0 +1,15 @@
+FSTAR_EXE ?= ../../bin/fstar.exe
+
+.PHONY: all
+all: run
+
+Hello.ml: Hello.fst
+	$(FSTAR_EXE) --codegen OCaml Hello.fst --extract Hello
+
+bin/hello.exe: Hello.ml
+	$(FSTAR_EXE) --ocamlenv dune build @install --profile=release
+	$(FSTAR_EXE) --ocamlenv dune install --prefix=.
+
+.PHONY: run
+run: bin/hello.exe
+	./bin/hello.exe | grep "Hi!"

tests/dune_hello/dune

@@ -0,0 +1,11 @@
+(executable
+ (name hello)
+ (public_name hello.exe)
+ (libraries fstar.lib)
+ (modes native)
+)
+(env
+  (_
+    (bin_annot false)
+    (flags (:standard -w -A)))
+)

tests/dune_hello/dune-project

@@ -0,0 +1,7 @@
+(lang dune 3.8)
+(name hello)
+
+(package
+  (name hello)
+  (synopsis "An example F* application")
+)

ulib/FStar.Tactics.Unseal.fsti → ulib/FStar.Stubs.Tactics.Unseal.fsti

@@ -16,7 +16,7 @@
 (**
 The [unseal] primitive to observe sealed values.
 *)
-module FStar.Tactics.Unseal
+module FStar.Stubs.Tactics.Unseal
 
 open FStar.Sealed
 open FStar.Tactics.Effect

ulib/FStar.Stubs.Tactics.V1.Builtins.fsti

@@ -26,8 +26,7 @@ open FStar.Stubs.Reflection.V1.Data
 open FStar.Reflection.Const
 open FStar.Tactics.Effect
 open FStar.Stubs.Tactics.Types
-
-include FStar.Tactics.Unseal
+include FStar.Stubs.Tactics.Unseal
 
 (** [top_env] returns the environment where the tactic started running.
  * This works even if no goals are present. *)

ulib/FStar.Stubs.Tactics.V2.Builtins.fsti

@@ -27,8 +27,7 @@ open FStar.Stubs.Reflection.V2.Builtins
 open FStar.Tactics.Effect
 open FStar.Tactics.Effect
 open FStar.Stubs.Tactics.Types
-
-include FStar.Tactics.Unseal
+include FStar.Stubs.Tactics.Unseal
 
 (** Resolve unification variable indirections at the top of the term. *)
 val compress : term -> Tac term

ulib/FStar.Tactics.CanonCommMonoidSimple.fst

@@ -22,7 +22,7 @@ open FStar.Tactics.V2.Bare
 open FStar.Classical
 open FStar.Tactics.CanonCommSwaps
 
-let term_eq = FStar.Tactics.V2.term_eq_old
+let term_eq = FStar.Stubs.Tactics.V2.Builtins.term_eq_old
 
 (* A simple expression canonizer for commutative monoids.
    For a canonizer with more features see FStar.Tactics.CanonCommMonoid.fst.

ulib/FStar.Tactics.Parametricity.fst

@@ -319,7 +319,7 @@ let param_inductive (se:sigelt) (fv0 fv1 : fv) : Tac decls =
     //Tactics.Util.iter (fun bv -> dump ("param bv = " ^ binder_to_string bv)) param_bs;
     let typ = mk_e_app (param' s typ) [replace_by s false orig; replace_by s true orig] in
     (* dump ("new typ = " ^ term_to_string typ); *)
-    let ctors = Tactics.V2.Bare.map (param_ctor nm s) ctors in
+    let ctors = Tactics.Util.map (param_ctor nm s) ctors in
     let se = Sg_Inductive {nm=inspect_fv fv1; univs; params=param_bs; typ; ctors} in
     (* dump ("param_ind : " ^ term_to_string (quote se)); *)
     [pack_sigelt se]