Loading dependences on the fly

FStar.fst.config.json

@@ -1,7 +1,8 @@
 {
   "fstar_exe": "./out/bin/fstar.exe",
   "options": [
-    "--ext", "optimize_let_vc"
+    "--ext", "optimize_let_vc",
+    "--ext", "fly_deps"
   ],
   "include_dirs": [
   ]

examples/Cfg.fst.config.json

@@ -1,7 +1,8 @@
 {
   "fstar_exe": "../out/bin/fstar.exe",
   "options": [
-    "--ext", "optimize_let_vc"
+    "--ext", "optimize_let_vc",
+    "--ext", "fly_deps"
   ],
   "include_dirs": [
   ]

examples/dependencies/Makefile

@@ -21,7 +21,7 @@ ROOTS     = Test.fst
 
 FSTAR_FLAGS = $(OTHERFLAGS) --cmi --odir $(OUT_DIR) --cache_dir $(CACHE_DIR) \
   --cache_checked_modules --already_cached 'Prims FStar' \
-  --ext optimize_let_vc
+  --ext optimize_let_vc --ext fly_deps
 
 FSTAR = $(FSTAR_EXE) $(FSTAR_FLAGS)
 

examples/dsls/DSL.fst.config.json

@@ -1,7 +1,8 @@
 {
 	"fstar_exe": "fstar.exe",
 	"options": [
-		"--ext", "optimize_let_vc"
+		"--ext", "optimize_let_vc",
+		"--ext", "fly_deps"
 	],
 	"include_dirs": [
 		"bool_refinement",

examples/miniparse/MiniParse.fst.config.json

@@ -1,7 +1,8 @@
 {
   "fstar_exe": "fstar.exe",
   "options": [
-    "--ext", "optimize_let_vc"
+    "--ext", "optimize_let_vc",
+    "--ext", "fly_deps"
   ],
   "include_dirs": [
   ]

examples/native_tactics/Makefile

@@ -5,7 +5,7 @@
 # 'include test.mk'.
 
 FSTAR_HOME=../..
-OTHERFLAGS += --ext optimize_let_vc
+OTHERFLAGS += --ext optimize_let_vc --ext fly_deps
 FSTAR_EXE ?= $(FSTAR_HOME)/out/bin/fstar.exe
 FSTAR=$(FSTAR_EXE) $(OTHERFLAGS)
 

examples/old/tls-record-layer/Makefile

@@ -177,13 +177,13 @@ chacha-aead-test: chacha-aead-compile
 	./test_chacha_aead.exe
 
 bignum-ver:
-	$(FSTAR) --ext optimize_let_vc crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst --include crypto
-	$(FSTAR) --ext optimize_let_vc crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst --include crypto
-	$(FSTAR) --ext optimize_let_vc crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst --include crypto
-	$(FSTAR) --ext optimize_let_vc crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4.fst --include crypto
-	$(FSTAR) --ext optimize_let_vc crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst --include crypto
-	$(FSTAR) --ext optimize_let_vc crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
-	$(FSTAR) --ext optimize_let_vc --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part1.fst --include crypto
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part2.fst --include crypto
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part3.fst --include crypto
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part4.fst --include crypto
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part5.fst --include crypto
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps crypto/Crypto.Symmetric.Poly1305.Bignum.Lemmas.Part6.fst --include crypto
+	$(FSTAR) --ext optimize_let_vc --ext fly_deps --include crypto crypto/Crypto.Symmetric.Poly1305.Bignum.fst
 
 KRML_INCLUDES=$(addprefix -I ,spartan_aes crypto $(KRML_HOME)/krmllib $(KRML_HOME)/test)
 ifeq ($(OS),Windows_NT)

examples/old/tls-record-layer/crypto/Makefile

@@ -2,7 +2,7 @@ FSTAR_HOME=../../..
 
 FSTAR?=$(FSTAR_HOME)/bin/fstar.exe
 
-OPTIONS=--fstar_home $(FSTAR_HOME) --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20 --ext optimize_let_vc $(OTHERFLAGS)
+OPTIONS=--fstar_home $(FSTAR_HOME) --max_fuel 4 --initial_fuel 0 --max_ifuel 2 --initial_ifuel 0 --z3rlimit 20 --ext optimize_let_vc --ext fly_deps $(OTHERFLAGS)
 
 FSTAR_INCLUDE_PATHS=--include $(FSTAR_HOME)/ulib/hyperstack --include hacl
 

examples/sample_project/Makefile

@@ -14,7 +14,7 @@ TOP_LEVEL_FILE=ml/main.ml
 OUTPUT_DIRECTORY=_output
 
 ################################################################################
-FSTAR=fstar.exe --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --ext optimize_let_vc $(OTHERFLAGS)
+FSTAR=fstar.exe --cache_checked_modules --odir $(OUTPUT_DIRECTORY) --ext optimize_let_vc --ext fly_deps $(OTHERFLAGS)
 ML_FILES=$(addprefix $(OUTPUT_DIRECTORY)/,$(addsuffix .ml,$(subst .,_, $(subst .fst,,$(FSTAR_FILES)))))
 OCAML_EXE=$(PROGRAM).ocaml.exe
 KRML_EXE=$(PROGRAM).exe

mk/common.mk

@@ -9,6 +9,8 @@ else
 cygpath=$(abspath $(1))
 endif
 
+FSTAR_OPTIONS += --ext fly_deps
+FSTAR_ARGS += --ext fly_deps
 MAKEFLAGS += --no-builtin-rules
 Q?=@
 SIL?=--silent

src/FStarCompiler.fst.config.json

@@ -6,7 +6,8 @@
     "--lax",
     "--cache_dir", "../stage1/fstarc.checked",
     "--warn_error",
-    "-271-272-241-319-274"
+    "-271-272-241-319-274",
+    "--ext", "fly_deps"
   ],
   "include_dirs": [
     "."

src/basic/FStarC.Common.fst

@@ -26,18 +26,21 @@ module List = FStarC.List
 module BU = FStarC.Util
 module SB = FStarC.StringBuffer
 
-let snapshot (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b) = BU.atomically (fun () ->
+let snapshot msg (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b) = BU.atomically (fun () ->
   let len : int = List.length !stackref in
   let arg' = push arg in
+  if FStarC.Debug.any () then Format.print2 "(%s)snapshot %s\n" msg (string_of_int len);
   (len, arg'))
 
-let rollback (pop: unit -> 'a) (stackref: ref (list 'c)) (depth: option int) =
+let rollback msg (pop: unit -> 'a) (stackref: ref (list 'c)) (depth: option int) =
+  if FStarC.Debug.any () then Format.print2 "(%s)rollback %s ... " msg (match depth with None -> "None" | Some len ->string_of_int len);
   let rec aux n : 'a =
-    if n <= 0 then failwith "Too many pops"
+    if n <= 0 then failwith "(rollback) Too many pops"
     else if n = 1 then pop ()
     else (ignore (pop ()); aux (n - 1)) in
   let curdepth = List.length !stackref in
   let n = match depth with Some d -> curdepth - d | None -> 1 in
+  if FStarC.Debug.any () then Format.print1 " depth is %s\n "(string_of_int (List.length (!stackref)));
   BU.atomically (fun () -> aux n)
 
 // This function is separate to make it easier to put breakpoints on it

src/basic/FStarC.Common.fsti

@@ -19,9 +19,9 @@
 module FStarC.Common
 open FStarC.Effect
 
-val snapshot (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b)
+val snapshot (msg:string) (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b)
 
-val rollback (pop: unit -> 'a) (stackref: ref (list 'c)) (depth: option int) : 'a
+val rollback (msg:string) (pop: unit -> 'a) (stackref: ref (list 'c)) (depth: option int) : 'a
 
 val runtime_assert (b:bool) (msg:string) : unit
 

src/basic/FStarC.EditDist.fst

@@ -1,5 +1,5 @@
 module FStarC.EditDist
-
+open FStarC.Effect
 
 let edit_distance (s1 s2 : string) : int =
   let cache : IMap.t (IMap.t int) = IMap.create 10 in

src/basic/FStarC.Options.fst

@@ -171,8 +171,8 @@ let depth () =
   let lev::_ = !history in
   List.length lev
 
-let snapshot ()    = Common.snapshot push history ()
-let rollback depth = Common.rollback pop  history depth
+let snapshot ()    = Common.snapshot "Options" push history ()
+let rollback depth = Common.rollback "Options" pop  history depth
 
 let set_option k v =
   let map : optionstate = peek() in
@@ -229,7 +229,6 @@ let defaults = [
   ("ide"                                       , Bool false);
   ("ide_id_info_off"                           , Bool false);
   ("ifuel"                                     , Unset);
-  ("in"                                        , Bool false);
   ("include"                                   , List []);
   ("initial_fuel"                              , Int 2);
   ("initial_ifuel"                             , Int 1);
@@ -248,7 +247,6 @@ let defaults = [
   ("log_failing_queries"                       , Bool false);
   ("log_queries"                               , Bool false);
   ("log_types"                                 , Bool false);
-  ("lsp"                                       , Bool false);
   ("max_fuel"                                  , Int 8);
   ("max_ifuel"                                 , Int 2);
   ("message_format"                            , String "auto");
@@ -494,10 +492,8 @@ let get_hide_uvar_nums          ()      = lookup_opt "hide_uvar_nums"
 let get_hint_info               ()      = lookup_opt "hint_info"                as_bool
 let get_hint_dir                ()      = lookup_opt "hint_dir"                 (as_option as_string)
 let get_hint_file               ()      = lookup_opt "hint_file"                (as_option as_string)
-let get_in                      ()      = lookup_opt "in"                       as_bool
 let get_ide                     ()      = lookup_opt "ide"                      as_bool
 let get_ide_id_info_off         ()      = lookup_opt "ide_id_info_off"          as_bool
-let get_lsp                     ()      = lookup_opt "lsp"                      as_bool
 let get_print                   ()      = lookup_opt "print"                    as_bool
 let get_print_in_place          ()      = lookup_opt "print_in_place"           as_bool
 let get_initial_fuel            ()      = lookup_opt "initial_fuel"             as_int
@@ -1035,26 +1031,16 @@ let specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.docum
     Const (Bool true),
     text "Print information regarding hints (deprecated; use --query_stats instead)");
 
-  ( noshort,
-    "in",
-    Const (Bool true),
-    text "Legacy interactive mode; reads input from stdin");
-
   ( noshort,
     "ide",
     Const (Bool true),
-    text "JSON-based interactive mode for IDEs");
+    text "JSON-based interactive mode for IDEs (used by VSCode, emacs, neovim, etc.)");
 
   ( noshort,
     "ide_id_info_off",
     Const (Bool true),
     text "Disable identifier tables in IDE mode (temporary workaround useful in Steel)");
 
-  ( noshort,
-    "lsp",
-    Const (Bool true),
-    text "Language Server Protocol-based interactive mode for IDEs");
-
   ( noshort,
     "include",
     ReverseAccumulated (PathStr "dir"),
@@ -1955,6 +1941,12 @@ let restore_cmd_line_options should_clear =
     set_option' ("verify_module", List (List.map String old_verify_module));
     Success
 
+let with_restored_cmd_line_options (f:unit -> 'a) : 'a =
+  let snap = snapshot_all () in
+  let h = !history in
+  let _ = restore_cmd_line_options true in
+  finally (fun _ -> history := h; restore_all snap) f
+
 let module_name_of_file_name f =
     let f = Filepath.basename f in
     let f = String.substring f 0 (String.length f - String.length (Filepath.get_file_extension f) - 1) in
@@ -2084,7 +2076,7 @@ let dump_module                  s  = get_dump_module() |> List.existsb (module_
 let eager_subtyping              () = get_eager_subtyping()
 let error_contexts               () = get_error_contexts              ()
 let expose_interfaces            () = get_expose_interfaces          ()
-let interactive                  () = get_in () || get_ide () || get_lsp ()
+let interactive                  () = get_ide ()
 let message_format               () =
   match get_message_format () with
   | "auto" -> (
@@ -2138,8 +2130,6 @@ let lang_extensions              () = get_lang_extensions             ()
 let lax                          () = get_lax                         ()
 let load                         () = get_load                        ()
 let load_cmxs                    () = get_load_cmxs                   ()
-let legacy_interactive           () = get_in                          ()
-let lsp_server                   () = get_lsp                         ()
 let log_queries                  () = get_log_queries                 ()
 let log_failing_queries          () = get_log_failing_queries         ()
 let keep_query_captions          () =

src/basic/FStarC.Options.fsti

@@ -82,7 +82,7 @@ val defaults                    : list (string & option_val)
 val init                        : unit    -> unit  //sets the current options to their defaults
 val clear                       : unit    -> unit  //wipes the stack of options, and then inits
 val restore_cmd_line_options    : bool -> parse_cmdline_res //inits or clears (if the flag is set) the current options and then sets it to the cmd line
-
+val with_restored_cmd_line_options : (unit -> 'a) -> 'a
 (* Control the option stack *)
 (* Briefly, push/pop are used by the interactive mode and internal_*
  * by #push-options/#pop-options. Read the comment in the .fs for more
@@ -166,8 +166,6 @@ val lang_extensions             : unit    -> list string
 val lax                         : unit    -> bool
 val load                        : unit    -> list string
 val load_cmxs                   : unit    -> list string
-val legacy_interactive          : unit    -> bool
-val lsp_server                  : unit    -> bool
 val log_queries                 : unit    -> bool
 val log_failing_queries         : unit    -> bool
 val log_types                   : unit    -> bool

src/basic/FStarC.Range.Ops.fst

@@ -17,10 +17,9 @@
    Operations over the FStarC.Range.Type.range type.
 *)
 module FStarC.Range.Ops
-
-open FStarC
 friend FStarC.Range.Type
 
+open FStarC
 open FStarC.Json
 open FStarC.Effect 
 open FStarC.Class.Ord

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

@@ -46,6 +46,7 @@ module TcUtil = FStarC.TypeChecker.Util
 module EMB    = FStarC.Syntax.Embeddings
 module Cfg    = FStarC.TypeChecker.Cfg
 module PO     = FStarC.TypeChecker.Primops
+module Print  = FStarC.Syntax.Print
 
 let dbg_ExtractionReify = Debug.get_toggle "ExtractionReify"
 
@@ -1322,6 +1323,7 @@ let extract' (g:uenv) (m:modul) : uenv & option mlmodule =
 
 let extract (g:uenv) (m:modul) =
   ignore <| Options.restore_cmd_line_options true;
+  debug g (fun _ -> Format.print1 "Starting extraction, uenv=%s\n" (show g));
   let tgt = 
     match Options.codegen() with
     | None -> failwith "Impossible: We're in extract, codegen must be set!"

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

@@ -56,6 +56,13 @@ let plug () = Options.codegen () = Some Options.Plugin
            || Options.codegen () = Some Options.PluginNoLib
 let plug_no_lib () = Options.codegen () = Some Options.PluginNoLib
 
+instance showable_mlbinding : showable mlbinding = {
+  show = function 
+    | Bv (x, _) -> show x
+    | Fv (x, _) -> show x
+    | ErasedFv x -> Format.fmt1 "Erased %s" (show x)
+}
+
 (**** Type definitions *)
 
 (** A top-level F* type definition, i.e., a type abbreviation,
@@ -108,6 +115,23 @@ type uenv = {
   currentModule: mlpath // needed to properly translate the definitions in the current file
 }
 
+let with_restored_tc_scope 
+      (env:uenv)
+      (f:uenv -> 'a & uenv)
+: 'a & uenv
+= let (res, uenv'), tcenv' =
+    TypeChecker.Env.with_restored_scope
+      env.env_tcenv 
+      (fun tcenv ->
+        let uenv = {env with env_tcenv=tcenv} in
+        let res, uenv' = f uenv in
+        (res, uenv'), uenv'.env_tcenv)
+  in
+  res, {uenv' with env_tcenv=tcenv'}
+
+instance showable_uenv : showable uenv = {
+  show = fun e -> show e.env_bindings
+}
 (**** Getters and Setters *)
 
 let tcenv_of_uenv (u:uenv) : TypeChecker.Env.env = u.env_tcenv

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

@@ -16,6 +16,7 @@
 
 module FStarC.Extraction.ML.UEnv
 open FStarC
+open FStarC.Class.Show
 open FStarC.Effect
 open FStarC.Ident
 open FStarC.Extraction.ML.Syntax
@@ -50,6 +51,8 @@ type mlbinding =
   | Fv  of fv & exp_binding
   | ErasedFv of fv
 
+instance val showable_mlbinding : showable mlbinding
+
 (** Type abbreviations, aka definitions *)
 val tydef : Type0
 val tydef_fv : tydef -> fv
@@ -59,6 +62,8 @@ val tydef_def: tydef -> mltyscheme
 
 (** The main type of this module *)
 val uenv : Type0
+instance val showable_uenv: showable uenv
+val with_restored_tc_scope (env:uenv) (f:uenv -> 'a & uenv) : 'a & uenv
 val tcenv_of_uenv : u:uenv -> TypeChecker.Env.env
 val set_tcenv : u:uenv -> t:TypeChecker.Env.env -> uenv
 val current_module_of_uenv : u:uenv -> mlpath