Allow recording partial hints, make --record_hints settable

src/basic/FStarC.Options.fst

@@ -1745,6 +1745,7 @@ let settable = function
     | "quake"
     | "query_cache"
     | "query_stats"
+    | "record_hints"
     | "record_options"
     | "retry"
     | "reuse_hint_for"

src/basic/FStarC.String.fsti

@@ -25,6 +25,8 @@ val make:    int -> char -> string
 val split:   chars: list char -> s: string -> Tot (list string)
 val strcat:  string -> string -> Tot string
 val concat:  separator: string -> strings: list string -> Tot string
+
+(* Negative if s1<s2, zero if equal, positive if s1>s2 *)
 val compare: s1: string -> s2: string -> Tot int
 val strlen:  string -> Tot nat
 val length:  string -> Tot nat

src/fstar/FStarC.Interactive.Ide.fst

@@ -1259,10 +1259,9 @@ let interactive_mode' init_st =
   write_hello ();
 
   let exit_code =
-    if FStarC.Options.record_hints() || FStarC.Options.use_hints() then
-      FStarC.SMTEncoding.Solver.with_hints_db (List.hd (Options.file_list ())) (fun () -> go init_st)
-    else
-      go init_st in
+    let fn = List.hd (Options.file_list ()) in
+    SMTEncoding.Solver.with_hints_db fn (fun () -> go init_st)
+  in
   exit exit_code
 
 let interactive_mode (filename:string): unit =

src/fstar/FStarC.Interactive.Legacy.fst

@@ -15,7 +15,7 @@
 *)
 
 module FStarC.Interactive.Legacy
-open FStarC
+
 open FStarC
 open FStarC.Effect
 open FStarC.List
@@ -572,9 +572,5 @@ let interactive_mode (filename:string): unit =
         env
   in
 
-  if FStarC.Options.record_hints() //and if we're recording or using hints
-  || FStarC.Options.use_hints()
-  then FStarC.SMTEncoding.Solver.with_hints_db
-            (List.hd (Options.file_list ()))
-            (fun () -> go (1, 0) filename stack None env ts)
-  else go (1, 0) filename stack None env ts
+  let fn = List.hd (Options.file_list ()) in
+  SMTEncoding.Solver.with_hints_db fn (fun () -> go (1, 0) filename stack None env ts)

src/fstar/FStarC.Universal.fst

@@ -444,11 +444,7 @@ let tc_one_file
           extracted_defs,
           env
       in
-      if (Options.should_verify (string_of_lid fmod.name) //if we're verifying this module
-            && (FStarC.Options.record_hints() //and if we're recording or using hints
-                || FStarC.Options.use_hints()))
-      then SMT.with_hints_db (Pars.find_file fn) check_mod
-      else check_mod () //don't add a hints file for modules that are not actually verified
+      SMT.with_hints_db (Pars.find_file fn) check_mod
   in
   if not (Options.cache_off()) then
       let r = Ch.load_module_from_cache (tcenv_of_uenv env) fn in

src/ml/FStarC_Hints.ml

@@ -111,6 +111,7 @@ let read_hints (filename: string) : hints_read_result =
            raise Exit
     )
   with
+   | Yojson.Json_error _
    | Exit ->
       MalformedJson
    | Sys_error _ ->

src/smtencoding/FStarC.SMTEncoding.Solver.fst

@@ -59,16 +59,27 @@ type z3_replay_result = either (option UC.unsat_core), error_labels
 let z3_result_as_replay_result = function
     | Inl l -> Inl l
     | Inr (r, _) -> Inr r
-let recorded_hints : ref (option hints) = BU.mk_ref None
+
+// Hints are stored in this reference as we progress through the file,
+// and written out by calling finalize_hints_db below.
+let src_filename : ref string = BU.mk_ref ""
+let recorded_hints : ref hints = BU.mk_ref []
 let replaying_hints: ref (option hints) = BU.mk_ref None
+let refreshing_hints : ref bool = BU.mk_ref false
 
 (****************************************************************************)
 (* Hint databases (public)                                                  *)
 (****************************************************************************)
 let use_hints () = Options.use_hints ()
-let initialize_hints_db src_filename format_filename : unit =
-    if Options.record_hints() then recorded_hints := Some [];
-    let norm_src_filename = BU.normalize_file_path src_filename in
+
+(* fresh: true iff we are recording hints for the whole file, and hence should
+not merge hints with old ones. *)
+let initialize_hints_db filename (refresh:bool) : unit =
+    recorded_hints := [];
+    refreshing_hints := refresh;
+
+    let norm_src_filename = BU.normalize_file_path filename in
+    src_filename := norm_src_filename;
     (*
      * Read the hints file into replaying_hints
      * But it will only be used when use_hints is on
@@ -104,27 +115,77 @@ let initialize_hints_db src_filename format_filename : unit =
             ()
     end
 
-let finalize_hints_db src_filename :unit =
-    begin if Options.record_hints () then
-          let hints = Option.get !recorded_hints in
-          let hints_db = {
-                module_digest = BU.digest_of_file src_filename;
-                hints = hints
-              }  in
-          let norm_src_filename = BU.normalize_file_path src_filename in
-          let val_filename = Options.hint_file_for_src norm_src_filename in
-          write_hints val_filename hints_db
-    end;
-    recorded_hints := None;
-    replaying_hints := None
+let rec merge_hints (prev next : hints) : hints =
+  match prev, next with
+  (* Can Nones really happen? *)
+  | None :: prev, next -> merge_hints prev next
+  | prev, None :: next -> merge_hints prev next
+  | Some p :: prev,  Some n :: next ->
+    (* Take the lesser one, or prefer n if they are for the same query. *)
+    if String.compare p.hint_name n.hint_name < 0 || (p.hint_name = n.hint_name && p.hint_index < n.hint_index) then
+      Some p :: merge_hints prev (Some n :: next)
+    else if p.hint_name = n.hint_name && p.hint_index = n.hint_index then
+      Some n :: merge_hints prev next
+    else
+      Some n :: merge_hints (Some p :: prev) next
+  | [], next -> next
+  | prev, [] -> prev
+
+let merge_hints_db (prev next : hints_db) : hints_db =
+  {
+    module_digest = next.module_digest;
+    hints = merge_hints prev.hints next.hints;
+  }
+
+(* This is called after we check every single top-level in the interactive mode, so
+we can record hints before "finishing" a module (which is never triggered in
+interactive mode, currently). *)
+let flush_hints () : unit =
+  let hints = !recorded_hints in
+  let src_filename = !src_filename in
+  (* If empty, don't do anything. *)
+  if Cons? hints then begin
+    let hints_db = {
+      module_digest = BU.digest_of_file src_filename;
+      hints = hints;
+    } in
+    let val_filename = Options.hint_file_for_src src_filename in
+    let hints_db =
+      (* If it's a full --record_hints run, overwrite file. Otherwise merge with
+      old hints. *)
+      if !refreshing_hints
+      then hints_db
+      else
+        match read_hints val_filename with
+        | HintsOK prev_hints -> merge_hints_db prev_hints hints_db
+        | _ -> hints_db
+    in
+    write_hints val_filename hints_db
+  end;
+  recorded_hints := [];
+  replaying_hints := None
+
+let finalize_hints_db () : unit =
+  flush_hints ()
 
 let with_hints_db fname f =
-    initialize_hints_db fname false;
+  (* Forbid reentrant calls, which would trash the state. This
+  happens (benignly) in the IDE, since the top-level invocation of the
+  interactive mode is wrapped by this function, and that driver will
+  call the typechecker to check dependencies of the current file, which
+  are also wrapped (even if lax). This will do the right thing of only
+  handling the outer invocation. *)
+  if !src_filename <> "" then
+    f ()
+  else begin
+    (* If --record_hints is set at this time, and this is not an interactive, we're fully refreshing. *)
+    initialize_hints_db fname (Options.record_hints () && not (Options.interactive ()));
     let result = f () in
     // for the moment, there should be no need to trap exceptions to finalize the hints db
     // no cleanup needs to occur if an error occurs.
-    finalize_hints_db fname;
+    finalize_hints_db ();
     result
+  end
 
 (***********************************************************************************)
 (* Invoking the SMT solver and extracting an error report from the model, if any   *)
@@ -612,9 +673,8 @@ let query_info settings z3result =
 
 //caller must ensure that the recorded_hints is already initiailized
 let store_hint hint =
-  match !recorded_hints with
-  | Some l -> recorded_hints := Some (l@[Some hint])
-  | _ -> assert false; ()
+  let l = !recorded_hints in
+  recorded_hints := l@[Some hint]
 
 let record_hint settings z3result =
     if not (Options.record_hints()) then () else
@@ -1208,7 +1268,7 @@ type solver_cfg = {
   valid_intro      : bool;
   valid_elim       : bool;
   z3version        : string;
-  context_pruning  : bool
+  context_pruning  : bool;
 }
 
 let _last_cfg : ref (option solver_cfg) = BU.mk_ref None

src/smtencoding/FStarC.SMTEncoding.Solver.fsti

@@ -18,5 +18,7 @@ module FStarC.SMTEncoding.Solver
 open FStarC.Effect
 
 val with_hints_db : string -> (unit -> 'a) -> 'a
+val flush_hints () : unit
+
 val dummy: FStarC.TypeChecker.Env.solver_t
 val solver: FStarC.TypeChecker.Env.solver_t

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -1083,6 +1083,11 @@ let tc_decls env ses =
       (Some (Ident.string_of_lid (Env.current_module env)))      
       "FStarC.TypeChecker.Tc.encode_sig";
 
+
+    (* Potentially write hints to disk after every query, when on interactive mode. *)
+    if Options.interactive () then
+      SMTEncoding.Solver.flush_hints ();
+
     (List.rev_append ses' ses, env), ses_elaborated
     end
   in

ulib/FStar.String.fsti

@@ -75,7 +75,8 @@ val split:   list char -> string -> Tot (list string)
 /// `concat s l` concatentates the strings in `l` delimited by `s`
 val concat:  string -> list string -> Tot string
 
-/// `compare s0 s1`: lexicographic ordering on strings
+/// `compare s0 s1`: lexicographic ordering on strings.
+/// Negative if s1<s2, zero if equal, positive if s1>s2
 val compare: string -> string -> Tot int
 
 /// `lowercase`: transform each character to its lowercase variant