Merge pull request #3976 from mtzguido/misc

Misc fixes

Author: mtzguido

Makefile

@@ -119,7 +119,6 @@ $(FSTAR1_BARE_EXE): .bare1.src.touch .src.ml.touch $(MAYBEFORCE)
 	  CACHE_DIR=stage1/plugins.checked/ \
 	  OUTPUT_DIR=stage1/plugins.ml/ \
 	  CODEGEN=PluginNoLib \
-	  OTHERFLAGS="--ext __guts $(OTHERFLAGS)" \
 	  TAG=plugins \
 	  TOUCH=$@ \
 	  $(MAKE) -f mk/plugins.mk ocaml
@@ -200,7 +199,6 @@ $(FSTAR2_BARE_EXE): .bare2.src.touch .src.ml.touch $(MAYBEFORCE)
 	  CACHE_DIR=stage2/plugins.checked/ \
 	  OUTPUT_DIR=stage2/plugins.ml/ \
 	  CODEGEN=PluginNoLib \
-	  OTHERFLAGS="--ext __guts $(OTHERFLAGS)" \
 	  TAG=plugins \
 	  TOUCH=$@ \
 	  $(MAKE) -f mk/plugins.mk ocaml
@@ -305,14 +303,14 @@ endif
 	touch $@
 
 .install-stage1.touch: export FSTAR_LINK_LIBDIRS=$(LINK_OK)
-.install-stage1.touch: .stage1.src.touch
+.install-stage1.touch: .stage1.src.touch $(MAYBEFORCE)
 	$(call bold_msg, "INSTALL", "STAGE 1")
 	$(MAKE) -C stage1 install PREFIX=$(CURDIR)/stage1/out
 	@# ^ pass PREFIX to make sure we don't get it from env
 	touch $@
 
 .install-stage2.touch: export FSTAR_LINK_LIBDIRS=$(LINK_OK)
-.install-stage2.touch: .stage2.src.touch
+.install-stage2.touch: .stage2.src.touch $(MAYBEFORCE)
 	$(call bold_msg, "INSTALL", "STAGE 2")
 	$(MAKE) -C stage2 install PREFIX=$(CURDIR)/stage2/out FSTAR_DUNE_RELEASE=1
 	@# ^ pass PREFIX to make sure we don't get it from env

src/data/FStarC.HashMap.fst

@@ -5,7 +5,6 @@ module FStarC.HashMap
 open FStarC
 open FStarC.Effect
 open FStarC.Class.Hashable
-module BU = FStarC.Util
 
 let hashmap (k v : Type) : Tot Type0 =
   PIMap.t (k & v)

src/extraction/FStarC.Extraction.ML.UEnv.fst

@@ -267,7 +267,7 @@ let no_fstar_stubs_ns (ns : list mlsymbol) : list mlsymbol =
   | "FStar"::"NormSteps"::rest when plug () ->
     "Fstarcompiler.FStarC"::"NormSteps"::rest
 
-  | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.enabled "__guts" -> "FStarC"::rest
+  | "FStar"::"Stubs"::rest when plug_no_lib () -> "FStarC"::rest
 
   (* These 3 modules are special, and are not in the guts. They live in src/ml/full and
   are visible at the ambient namespace when building the plugin lib. *)

src/fstar/FStarC.Hooks.fst

@@ -54,14 +54,13 @@ let lazy_chooser (k:Syntax.Syntax.lazy_kind) (i:Syntax.Syntax.lazyinfo) : Syntax
     | Syntax.Syntax.Lazy_embedding (_, t) -> Thunk.force t
     | Syntax.Syntax.Lazy_extension s      -> FStarC.Syntax.Util.exp_string (Format.fmt1 "((extension %s))" s)
 
-// This is called directly by the Javascript port (it doesn't call Main)
-let setup_hooks () =
-    Syntax.DsEnv.ugly_sigelt_to_string_hook := show;
-    Errors.set_parse_warn_error Parser.ParseIt.parse_warn_error;
-    Syntax.Syntax.lazy_chooser := Some lazy_chooser;
-    Syntax.Util.tts_f := Some show;
-    Syntax.Util.ttd_f := Some Class.PP.pp;
-    TypeChecker.Normalize.unembed_binder_knot := Some RE.e_binder;
-    iter Tactics.Interpreter.register_tactic_primitive_step Tactics.V1.Primops.ops;
-    iter Tactics.Interpreter.register_tactic_primitive_step Tactics.V2.Primops.ops;
-    ()
+let () =
+  Syntax.DsEnv.ugly_sigelt_to_string_hook := show;
+  Errors.set_parse_warn_error Parser.ParseIt.parse_warn_error;
+  Syntax.Syntax.lazy_chooser := Some lazy_chooser;
+  Syntax.Util.tts_f := Some show;
+  Syntax.Util.ttd_f := Some Class.PP.pp;
+  TypeChecker.Normalize.unembed_binder_knot := Some RE.e_binder;
+  iter Tactics.Interpreter.register_tactic_primitive_step Tactics.V1.Primops.ops;
+  iter Tactics.Interpreter.register_tactic_primitive_step Tactics.V2.Primops.ops;
+  ()

src/fstar/FStarC.Hooks.fsti

@@ -15,10 +15,7 @@
 *)
 module FStarC.Hooks
 
-open FStarC.Effect
-
-(* This function sets ties some know between modules in the compiler source tree,
-enabling more recursion and breaking some dependencies.
-
-This is called directly by the Javascript port (it doesn't call Main) and the ocaml tests. *)
-val setup_hooks () : unit
+(* This module sets ties some know between modules in the compiler source tree,
+enabling more recursion and breaking some dependencies. It does this via a
+top-level effect. You only need to import this module in order for this to
+happen. *)

src/fstar/FStarC.Main.fst

@@ -24,6 +24,8 @@ open FStarC.CheckedFiles
 open FStarC.Universal
 open FStarC.Util
 
+open FStarC.Hooks (* KEEP: we need this module for its top-level effect. *)
+
 open FStarC.Class.Show
 
 module E = FStarC.Errors
@@ -442,7 +444,6 @@ let handle_error e =
 
 let main () =
   try
-    Hooks.setup_hooks ();
     let _, time = Timing.record_ms go in
     if FStarC.Options.query_stats()
     then print2_error "TOTAL TIME %s ms: %s\n"

src/syntax/FStarC.Syntax.Syntax.fst

@@ -280,14 +280,6 @@ instance ord_ident : ord ident =
 instance ord_fv : ord lident =
   ord_instance_from_cmp (fun x y -> Order.order_from_int (order_fv x y))
 
-let syn p k f = f k p
-let mk_fvs () = mk_ref None
-let mk_uvs () = mk_ref None
-
-//let memo_no_uvs = mk_ref (Some no_uvs)
-//let memo_no_names = mk_ref (Some no_names)
-let list_of_freenames (fvs:freenames) = elems fvs
-
 (* Constructors for each term form; NO HASH CONSING; just makes all the auxiliary data at each node *)
 let mk (t:'a) r = {
     n=t;