From 7dde78d3bf90bb94b61f3d1818df36fb753a2136 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 15 Aug 2024 17:55:37 -0700 Subject: [PATCH 1/3] Syntax: showable for modul, and use it --- src/fstar/FStar.Universal.fst | 4 +++- src/syntax/FStar.Syntax.Print.fst | 1 + src/syntax/FStar.Syntax.Print.fsti | 2 +- src/tosyntax/FStar.ToSyntax.ToSyntax.fst | 2 +- src/typechecker/FStar.TypeChecker.Tc.fst | 6 +++--- 5 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/fstar/FStar.Universal.fst b/src/fstar/FStar.Universal.fst index 3e2e0e9ccb6..474b6f19b05 100644 --- a/src/fstar/FStar.Universal.fst +++ b/src/fstar/FStar.Universal.fst @@ -34,6 +34,8 @@ open FStar.Syntax.DsEnv open FStar.TypeChecker open FStar.CheckedFiles +open FStar.Class.Show + (* Module abbreviations for the universal type-checker *) module DsEnv = FStar.Syntax.DsEnv module TcEnv = FStar.TypeChecker.Env @@ -476,7 +478,7 @@ let tc_one_file let tcmod = tc_result.checked_module in let smt_decls = tc_result.smt_decls in if Options.dump_module (string_of_lid tcmod.name) - then BU.print1 "Module after type checking:\n%s\n" (FStar.Syntax.Print.modul_to_string tcmod); + then BU.print1 "Module after type checking:\n%s\n" (show tcmod); let extend_tcenv tcmod tcenv = if not (Options.lax()) then FStar.SMTEncoding.Z3.refresh(); diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst index 56e0fbbd58b..ec8a12c29e0 100644 --- a/src/syntax/FStar.Syntax.Print.fst +++ b/src/syntax/FStar.Syntax.Print.fst @@ -1014,6 +1014,7 @@ instance showable_qualifier = { show = qual_to_string; } instance showable_pat = { show = pat_to_string; } instance showable_const = { show = const_to_string; } instance showable_letbinding = { show = lb_to_string; } +instance showable_modul = { show = modul_to_string; } instance pretty_term = { pp = term_to_doc; } instance pretty_univ = { pp = univ_to_doc; } diff --git a/src/syntax/FStar.Syntax.Print.fsti b/src/syntax/FStar.Syntax.Print.fsti index 40cdc3bd8d7..8b2a9a93dd7 100644 --- a/src/syntax/FStar.Syntax.Print.fsti +++ b/src/syntax/FStar.Syntax.Print.fsti @@ -42,7 +42,6 @@ val tag_of_term : term -> string val lbname_to_string : lbname -> string val pat_to_string : pat -> string val branch_to_string : Syntax.branch -> string -val modul_to_string : modul -> string val univ_names_to_string : univ_names -> string val univ_to_string : universe -> string val univs_to_string : universes -> string @@ -107,6 +106,7 @@ instance val showable_qualifier : showable qualifier instance val showable_pat : showable pat instance val showable_const : showable sconst instance val showable_letbinding : showable letbinding +instance val showable_modul : showable modul instance val pretty_term : pretty term instance val pretty_univ : pretty universe diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index 74875b91424..bff0f80b95d 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -4341,7 +4341,7 @@ let desugar_modul env (m:AST.modul) : env_t & Syntax.modul = let env, modul, pop_when_done = desugar_modul_common None env m in let env, modul = Env.finish_module_or_interface env modul in if Options.dump_module (string_of_lid modul.name) - then BU.print1 "Module after desugaring:\n%s\n" (Print.modul_to_string modul); + then BU.print1 "Module after desugaring:\n%s\n" (show modul); (if pop_when_done then export_interface modul.name env else env), modul ) diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst index 16f07b4e8da..a9795a54dfe 100644 --- a/src/typechecker/FStar.TypeChecker.Tc.fst +++ b/src/typechecker/FStar.TypeChecker.Tc.fst @@ -1217,7 +1217,7 @@ let check_module env0 m b = if Debug.any() then BU.print2 "Checking %s: %s\n" (if m.is_interface then "i'face" else "module") (Print.lid_to_string m.name); if Options.dump_module (string_of_lid m.name) - then BU.print1 "Module before type checking:\n%s\n" (Print.modul_to_string m); + then BU.print1 "Module before type checking:\n%s\n" (show m); let env = {env0 with admit = not (Options.should_verify (string_of_lid m.name))} in let m, env = tc_modul env m b in @@ -1226,7 +1226,7 @@ let check_module env0 m b = (* Debug information for level Normalize : normalizes all toplevel declarations an dump the current module *) if Options.dump_module (string_of_lid m.name) - then BU.print1 "Module after type checking:\n%s\n" (Print.modul_to_string m); + then BU.print1 "Module after type checking:\n%s\n" (show m); if Options.dump_module (string_of_lid m.name) && !dbg_Normalize then begin let normalize_toplevel_lets = fun se -> match se.sigel with @@ -1240,7 +1240,7 @@ let check_module env0 m b = | _ -> se in let normalized_module = { m with declarations = List.map normalize_toplevel_lets m.declarations } in - BU.print1 "%s\n" (Print.modul_to_string normalized_module) + BU.print1 "%s\n" (show normalized_module) end; m, env From 5f5426b94913dc6b2121f826c3fdb8dafbe62951 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 15 Aug 2024 15:47:38 -0700 Subject: [PATCH 2/3] Introduce --read_checked_file option --- src/basic/FStar.Options.fst | 8 ++++++++ src/basic/FStar.Options.fsti | 1 + src/fstar/FStar.CheckedFiles.fst | 30 ++++++++++++++++++++---------- src/fstar/FStar.CheckedFiles.fsti | 8 ++++++++ src/fstar/FStar.Main.fst | 16 ++++++++++++++++ 5 files changed, 53 insertions(+), 10 deletions(-) diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst index 8cff3ca64de..e64f00ff126 100644 --- a/src/basic/FStar.Options.fst +++ b/src/basic/FStar.Options.fst @@ -238,6 +238,7 @@ let defaults = ("quake_keep" , Bool false); ("query_cache" , Bool false); ("query_stats" , Bool false); + ("read_checked_file" , Unset); ("record_hints" , Bool false); ("record_options" , Bool false); ("report_assumes" , Unset); @@ -425,6 +426,7 @@ let get_quake_hi () = lookup_opt "quake_hi" let get_quake_keep () = lookup_opt "quake_keep" as_bool let get_query_cache () = lookup_opt "query_cache" as_bool let get_query_stats () = lookup_opt "query_stats" as_bool +let get_read_checked_file () = lookup_opt "read_checked_file" (as_option as_string) let get_record_hints () = lookup_opt "record_hints" as_bool let get_record_options () = lookup_opt "record_options" as_bool let get_retry () = lookup_opt "retry" as_bool @@ -1152,6 +1154,11 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d Const (Bool true), text "Print SMT query statistics"); + ( noshort, + "read_checked_file", + PathStr "path", + text "Read a checked file and dump it to standard output."); + ( noshort, "record_hints", Const (Bool true), @@ -1937,6 +1944,7 @@ let quake_hi () = get_quake_hi () let quake_keep () = get_quake_keep () let query_cache () = get_query_cache () let query_stats () = get_query_stats () +let read_checked_file () = get_read_checked_file () let record_hints () = get_record_hints () let record_options () = get_record_options () let retry () = get_retry () diff --git a/src/basic/FStar.Options.fsti b/src/basic/FStar.Options.fsti index 5b26448be34..8bf0ecd3859 100644 --- a/src/basic/FStar.Options.fsti +++ b/src/basic/FStar.Options.fsti @@ -185,6 +185,7 @@ val quake_hi : unit -> int val quake_keep : unit -> bool val query_cache : unit -> bool val query_stats : unit -> bool +val read_checked_file : unit -> option string val record_hints : unit -> bool val record_options : unit -> bool val retry : unit -> bool diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst index eafddb1998a..1de82818f65 100644 --- a/src/fstar/FStar.CheckedFiles.fst +++ b/src/fstar/FStar.CheckedFiles.fst @@ -233,28 +233,38 @@ let load_checked_file (fn:string) (checked_fn:string) :cache_t = end else add_and_return (Unknown, Inr x.parsing_data) +let load_tc_result (checked_fn:string) : option (list (string & string) & tc_result) = + let entry : option (checked_file_entry_stage1 & checked_file_entry_stage2) = + BU.load_2values_from_file checked_fn + in + match entry with + | Some ((_,s2)) -> Some (s2.deps_dig, s2.tc_res) + | _ -> None + (* * Second step for loading checked files, validates the tc data * Either the reason why tc_result is invalid * or tc_result *) -let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:string) - :either string tc_result = +let load_checked_file_with_tc_result + (deps:Dep.deps) + (fn:string) + (checked_fn:string) + : either string tc_result += if !dbg then BU.print1 "Trying to load checked file with tc result %s\n" checked_fn; - let load_tc_result (fn:string) :list (string & string) & tc_result = - let entry :option (checked_file_entry_stage1 & checked_file_entry_stage2) = BU.load_2values_from_file checked_fn in - match entry with - | Some ((_,s2)) -> s2.deps_dig, s2.tc_res - | _ -> - failwith "Impossible! if first phase of loading was unknown, it should have succeeded" + let load_tc_result' (fn:string) :list (string & string) & tc_result = + match load_tc_result fn with + | Some x -> x + | None -> failwith "Impossible! if first phase of loading was unknown, it should have succeeded" in let elt = load_checked_file fn checked_fn in //first step, in case some client calls it directly match elt with | Invalid msg, _ -> Inl msg - | Valid _, _ -> checked_fn |> load_tc_result |> snd |> Inr + | Valid _, _ -> checked_fn |> load_tc_result' |> snd |> Inr | Unknown, parsing_data -> match hash_dependences deps fn with | Inl msg -> @@ -262,7 +272,7 @@ let load_checked_file_with_tc_result (deps:Dep.deps) (fn:string) (checked_fn:str BU.smap_add mcache checked_fn elt; Inl msg | Inr deps_dig' -> - let deps_dig, tc_result = checked_fn |> load_tc_result in + let deps_dig, tc_result = checked_fn |> load_tc_result' in if deps_dig = deps_dig' then begin //mark the tc data of the file as valid diff --git a/src/fstar/FStar.CheckedFiles.fsti b/src/fstar/FStar.CheckedFiles.fsti index 9cadce26d91..cecd4fa3344 100644 --- a/src/fstar/FStar.CheckedFiles.fsti +++ b/src/fstar/FStar.CheckedFiles.fsti @@ -41,6 +41,14 @@ type tc_result = { extraction_time:int } +val load_tc_result (checked_fn:string) : option (list (string & string) & tc_result) + +val load_checked_file_with_tc_result + (deps:Dep.deps) + (fn:string) + (checked_fn:string) + : either string tc_result + (* * Read parsing data from the checked file * This function is passed as a callback to Parser.Dep diff --git a/src/fstar/FStar.Main.fst b/src/fstar/FStar.Main.fst index e68caef5f79..a761cec2218 100644 --- a/src/fstar/FStar.Main.fst +++ b/src/fstar/FStar.Main.fst @@ -23,6 +23,8 @@ open FStar.CheckedFiles open FStar.Universal open FStar.Compiler +open FStar.Class.Show + module E = FStar.Errors module UF = FStar.Syntax.Unionfind module RE = FStar.Reflection.V2.Embeddings @@ -160,6 +162,20 @@ let go _ = else failwith "You seem to be using the F#-generated version ofthe compiler ; \o reindenting is not known to work yet with this version" + (* --read_checked: read and print a checked file *) + else if Some? (Options.read_checked_file ()) then + let path = Some?.v <| Options.read_checked_file () in + let env = Universal.init_env Parser.Dep.empty_deps in + let res = FStar.CheckedFiles.load_tc_result path in + match res with + | None -> + let open FStar.Pprint in + Errors.raise_err_doc (Errors.Fatal_ModuleOrFileNotFound, [ + Errors.Msg.text "Could not read checked file:" ^/^ doc_of_string path + ]) + + | Some (_, tcr) -> + print1 "%s\n" (show tcr.checked_module) (* --lsp *) else if Options.lsp_server () then FStar.Interactive.Lsp.start_server () From 0dadae5c72ca5373c04577960d6f4c6b88852260 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 15 Aug 2024 17:59:58 -0700 Subject: [PATCH 3/3] snap --- .../fstar-lib/generated/FStar_CheckedFiles.ml | 26 +- ocaml/fstar-lib/generated/FStar_Main.ml | 151 +++-- ocaml/fstar-lib/generated/FStar_Options.ml | 564 +++++++++--------- .../fstar-lib/generated/FStar_Syntax_Print.ml | 2 + .../generated/FStar_ToSyntax_ToSyntax.ml | 3 +- .../generated/FStar_TypeChecker_Tc.ml | 9 +- ocaml/fstar-lib/generated/FStar_Universal.ml | 4 +- 7 files changed, 417 insertions(+), 342 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index 6bde5c00c93..5f4604aadb8 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -275,6 +275,17 @@ let (load_checked_file : Prims.string -> Prims.string -> cache_t) = else add_and_return (Unknown, (FStar_Pervasives.Inr (x.parsing_data))))))) +let (load_tc_result : + Prims.string -> + ((Prims.string * Prims.string) Prims.list * tc_result) + FStar_Pervasives_Native.option) + = + fun checked_fn -> + let entry = FStar_Compiler_Util.load_2values_from_file checked_fn in + match entry with + | FStar_Pervasives_Native.Some (uu___, s2) -> + FStar_Pervasives_Native.Some ((s2.deps_dig), (s2.tc_res)) + | uu___ -> FStar_Pervasives_Native.None let (load_checked_file_with_tc_result : FStar_Parser_Dep.deps -> Prims.string -> @@ -289,12 +300,11 @@ let (load_checked_file_with_tc_result : FStar_Compiler_Util.print1 "Trying to load checked file with tc result %s\n" checked_fn else ()); - (let load_tc_result fn1 = - let entry = FStar_Compiler_Util.load_2values_from_file checked_fn in - match entry with - | FStar_Pervasives_Native.Some (uu___1, s2) -> - ((s2.deps_dig), (s2.tc_res)) - | uu___1 -> + (let load_tc_result' fn1 = + let uu___1 = load_tc_result fn1 in + match uu___1 with + | FStar_Pervasives_Native.Some x -> x + | FStar_Pervasives_Native.None -> FStar_Compiler_Effect.failwith "Impossible! if first phase of loading was unknown, it should have succeeded" in let elt = load_checked_file fn checked_fn in @@ -302,7 +312,7 @@ let (load_checked_file_with_tc_result : | (Invalid msg, uu___1) -> FStar_Pervasives.Inl msg | (Valid uu___1, uu___2) -> let uu___3 = - let uu___4 = load_tc_result checked_fn in + let uu___4 = load_tc_result' checked_fn in FStar_Pervasives_Native.snd uu___4 in FStar_Pervasives.Inr uu___3 | (Unknown, parsing_data) -> @@ -313,7 +323,7 @@ let (load_checked_file_with_tc_result : (FStar_Compiler_Util.smap_add mcache checked_fn elt1; FStar_Pervasives.Inl msg) | FStar_Pervasives.Inr deps_dig' -> - let uu___2 = load_tc_result checked_fn in + let uu___2 = load_tc_result' checked_fn in (match uu___2 with | (deps_dig, tc_result1) -> if deps_dig = deps_dig' diff --git a/ocaml/fstar-lib/generated/FStar_Main.ml b/ocaml/fstar-lib/generated/FStar_Main.ml index 6038d71d86e..5ffe51baadb 100644 --- a/ocaml/fstar-lib/generated/FStar_Main.ml +++ b/ocaml/fstar-lib/generated/FStar_Main.ml @@ -184,68 +184,103 @@ let go : 'uuuuu . 'uuuuu -> unit = FStar_Compiler_Effect.failwith "You seem to be using the F#-generated version ofthe compiler ; \\o\n reindenting is not known to work yet with this version") else - (let uu___9 = FStar_Options.lsp_server () in + (let uu___9 = + let uu___10 = FStar_Options.read_checked_file () in + FStar_Pervasives_Native.uu___is_Some uu___10 in if uu___9 - then FStar_Interactive_Lsp.start_server () + then + let path = + let uu___10 = FStar_Options.read_checked_file () in + FStar_Pervasives_Native.__proj__Some__item__v + uu___10 in + let env = + FStar_Universal.init_env FStar_Parser_Dep.empty_deps in + let res1 = FStar_CheckedFiles.load_tc_result path in + match res1 with + | FStar_Pervasives_Native.None -> + let uu___10 = + let uu___11 = + let uu___12 = + let uu___13 = + FStar_Errors_Msg.text + "Could not read checked file:" in + let uu___14 = + FStar_Pprint.doc_of_string path in + FStar_Pprint.op_Hat_Slash_Hat uu___13 + uu___14 in + [uu___12] in + (FStar_Errors_Codes.Fatal_ModuleOrFileNotFound, + uu___11) in + FStar_Errors.raise_err_doc uu___10 + | FStar_Pervasives_Native.Some (uu___10, tcr) -> + let uu___11 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_modul + tcr.FStar_CheckedFiles.checked_module in + FStar_Compiler_Util.print1 "%s\n" uu___11 else - (let uu___11 = FStar_Options.interactive () in + (let uu___11 = FStar_Options.lsp_server () in if uu___11 - then - (FStar_Syntax_Unionfind.set_rw (); - (match filenames with - | [] -> - (FStar_Errors.log_issue - FStar_Compiler_Range_Type.dummyRange - (FStar_Errors_Codes.Error_MissingFileName, - "--ide: Name of current file missing in command line invocation\n"); - FStar_Compiler_Effect.exit Prims.int_one) - | uu___13::uu___14::uu___15 -> - (FStar_Errors.log_issue - FStar_Compiler_Range_Type.dummyRange - (FStar_Errors_Codes.Error_TooManyFiles, - "--ide: Too many files in command line invocation\n"); - FStar_Compiler_Effect.exit Prims.int_one) - | filename::[] -> - let uu___13 = - FStar_Options.legacy_interactive () in - if uu___13 - then - FStar_Interactive_Legacy.interactive_mode - filename - else - FStar_Interactive_Ide.interactive_mode - filename)) + then FStar_Interactive_Lsp.start_server () else - if - (FStar_Compiler_List.length filenames) >= - Prims.int_one - then - (let uu___13 = - FStar_Dependencies.find_deps_if_needed - filenames - FStar_CheckedFiles.load_parsing_data_from_cache in - match uu___13 with - | (filenames1, dep_graph) -> - let uu___14 = - FStar_Universal.batch_mode_tc filenames1 - dep_graph in - (match uu___14 with - | (tcrs, env, cleanup1) -> - ((let uu___16 = cleanup1 env in ()); - (let module_names = - FStar_Compiler_List.map - (fun tcr -> - FStar_Universal.module_or_interface_name - tcr.FStar_CheckedFiles.checked_module) - tcrs in - report_errors module_names; - finished_message module_names - Prims.int_zero)))) - else - FStar_Errors.raise_error - (FStar_Errors_Codes.Error_MissingFileName, - "No file provided") - FStar_Compiler_Range_Type.dummyRange)))))) + (let uu___13 = FStar_Options.interactive () in + if uu___13 + then + (FStar_Syntax_Unionfind.set_rw (); + (match filenames with + | [] -> + (FStar_Errors.log_issue + FStar_Compiler_Range_Type.dummyRange + (FStar_Errors_Codes.Error_MissingFileName, + "--ide: Name of current file missing in command line invocation\n"); + FStar_Compiler_Effect.exit Prims.int_one) + | uu___15::uu___16::uu___17 -> + (FStar_Errors.log_issue + FStar_Compiler_Range_Type.dummyRange + (FStar_Errors_Codes.Error_TooManyFiles, + "--ide: Too many files in command line invocation\n"); + FStar_Compiler_Effect.exit Prims.int_one) + | filename::[] -> + let uu___15 = + FStar_Options.legacy_interactive () in + if uu___15 + then + FStar_Interactive_Legacy.interactive_mode + filename + else + FStar_Interactive_Ide.interactive_mode + filename)) + else + if + (FStar_Compiler_List.length filenames) >= + Prims.int_one + then + (let uu___15 = + FStar_Dependencies.find_deps_if_needed + filenames + FStar_CheckedFiles.load_parsing_data_from_cache in + match uu___15 with + | (filenames1, dep_graph) -> + let uu___16 = + FStar_Universal.batch_mode_tc + filenames1 dep_graph in + (match uu___16 with + | (tcrs, env, cleanup1) -> + ((let uu___18 = cleanup1 env in ()); + (let module_names = + FStar_Compiler_List.map + (fun tcr -> + FStar_Universal.module_or_interface_name + tcr.FStar_CheckedFiles.checked_module) + tcrs in + report_errors module_names; + finished_message module_names + Prims.int_zero)))) + else + FStar_Errors.raise_error + (FStar_Errors_Codes.Error_MissingFileName, + "No file provided") + FStar_Compiler_Range_Type.dummyRange))))))) let (lazy_chooser : FStar_Syntax_Syntax.lazy_kind -> FStar_Syntax_Syntax.lazyinfo -> diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml index 67054f6cd25..faa13e22599 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -359,6 +359,7 @@ let (defaults : (Prims.string * option_val) Prims.list) = ("quake_keep", (Bool false)); ("query_cache", (Bool false)); ("query_stats", (Bool false)); + ("read_checked_file", Unset); ("record_hints", (Bool false)); ("record_options", (Bool false)); ("report_assumes", Unset); @@ -620,6 +621,9 @@ let (get_query_cache : unit -> Prims.bool) = fun uu___ -> lookup_opt "query_cache" as_bool let (get_query_stats : unit -> Prims.bool) = fun uu___ -> lookup_opt "query_stats" as_bool +let (get_read_checked_file : + unit -> Prims.string FStar_Pervasives_Native.option) = + fun uu___ -> lookup_opt "read_checked_file" (as_option as_string) let (get_record_hints : unit -> Prims.bool) = fun uu___ -> lookup_opt "record_hints" as_bool let (get_record_options : unit -> Prims.bool) = @@ -1011,7 +1015,7 @@ let (interp_quake_arg : Prims.string -> (Prims.int * Prims.int * Prims.bool)) let uu___ = ios f1 in let uu___1 = ios f2 in (uu___, uu___1, true) else FStar_Compiler_Effect.failwith "unexpected value for --quake" | uu___ -> FStar_Compiler_Effect.failwith "unexpected value for --quake" -let (uu___452 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) +let (uu___453 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) = let cb = FStar_Compiler_Util.mk_ref FStar_Pervasives_Native.None in let set1 f = @@ -1023,11 +1027,11 @@ let (uu___452 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) | FStar_Pervasives_Native.Some f -> f msg in (set1, call) let (set_option_warning_callback_aux : (Prims.string -> unit) -> unit) = - match uu___452 with + match uu___453 with | (set_option_warning_callback_aux1, option_warning_callback) -> set_option_warning_callback_aux1 let (option_warning_callback : Prims.string -> unit) = - match uu___452 with + match uu___453 with | (set_option_warning_callback_aux1, option_warning_callback1) -> option_warning_callback1 let (set_option_warning_callback : (Prims.string -> unit) -> unit) = @@ -2246,12 +2250,11 @@ let rec (specs_with_types : let uu___155 = text - "Record a database of hints for efficient proof replay" in + "Read a checked file and dump it to standard output." in (FStar_Getopt.noshort, - "record_hints", - (Const - (Bool - true)), + "read_checked_file", + (PathStr + "path"), uu___155) in let uu___155 = @@ -2260,9 +2263,9 @@ let rec (specs_with_types : let uu___157 = text - "Record the state of options used to check each sigelt, useful for the `check_with` attribute and metaprogramming. Note that this implies a performance hit and increases the size of checked files." in + "Record a database of hints for efficient proof replay" in (FStar_Getopt.noshort, - "record_options", + "record_hints", (Const (Bool true)), @@ -2274,14 +2277,28 @@ let rec (specs_with_types : let uu___159 = text + "Record the state of options used to check each sigelt, useful for the `check_with` attribute and metaprogramming. Note that this implies a performance hit and increases the size of checked files." in + (FStar_Getopt.noshort, + "record_options", + (Const + (Bool + true)), + uu___159) in + let uu___159 + = + let uu___160 + = + let uu___161 + = + text "Retry each SMT query N times and succeed on the first try. Using --retry disables --quake." in (FStar_Getopt.noshort, "retry", (PostProcessed ((fun - uu___160 + uu___162 -> - match uu___160 + match uu___162 with | Int i -> @@ -2302,18 +2319,18 @@ let rec (specs_with_types : true); Bool true) | - uu___161 + uu___163 -> FStar_Compiler_Effect.failwith "impos"), (IntStr "positive integer"))), - uu___159) in - let uu___159 + uu___161) in + let uu___161 = - let uu___160 + let uu___162 = - let uu___161 + let uu___163 = text "Optimistically, attempt using the recorded hint for toplevel_name (a top-level name in the current module) when trying to verify some other term 'g'" in @@ -2321,12 +2338,12 @@ let rec (specs_with_types : "reuse_hint_for", (SimpleStr "toplevel_name"), - uu___161) in - let uu___161 + uu___163) in + let uu___163 = - let uu___162 + let uu___164 = - let uu___163 + let uu___165 = text "Report every use of an escape hatch, include assume, admit, etc." in @@ -2335,12 +2352,12 @@ let rec (specs_with_types : (EnumStr ["warn"; "error"]), - uu___163) in - let uu___163 + uu___165) in + let uu___165 = - let uu___164 + let uu___166 = - let uu___165 + let uu___167 = text "Disable all non-critical output" in @@ -2349,12 +2366,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___165) in - let uu___165 + uu___167) in + let uu___167 = - let uu___166 + let uu___168 = - let uu___167 + let uu___169 = text "Path to the Z3 SMT solver (we could eventually support other solvers)" in @@ -2362,211 +2379,197 @@ let rec (specs_with_types : "smt", (PathStr "path"), - uu___167) in - let uu___167 + uu___169) in + let uu___169 = - let uu___168 + let uu___170 = - let uu___169 + let uu___171 = text "Toggle a peephole optimization that eliminates redundant uses of boxing/unboxing in the SMT encoding (default 'false')" in (FStar_Getopt.noshort, "smtencoding.elim_box", BoolStr, - uu___169) in - let uu___169 - = - let uu___170 - = + uu___171) in let uu___171 = let uu___172 = - text - "Control the representation of non-linear arithmetic functions in the SMT encoding:" in let uu___173 = let uu___174 = + text + "Control the representation of non-linear arithmetic functions in the SMT encoding:" in let uu___175 = let uu___176 = - text - "if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'" in let uu___177 = let uu___178 = text - "if 'native' use '*, div, mod'" in + "if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'" in let uu___179 = let uu___180 = text + "if 'native' use '*, div, mod'" in + let uu___181 + = + let uu___182 + = + text "if 'wrapped' use '_mul, _div, _mod : Int*Int -> Int'" in - [uu___180] in + [uu___182] in + uu___180 + :: + uu___181 in uu___178 :: uu___179 in - uu___176 - :: - uu___177 in FStar_Errors_Msg.bulleted - uu___175 in - let uu___175 + uu___177 in + let uu___177 = text "(default 'boxwrap')" in FStar_Pprint.op_Hat_Hat + uu___176 + uu___177 in + FStar_Pprint.op_Hat_Hat uu___174 uu___175 in - FStar_Pprint.op_Hat_Hat - uu___172 - uu___173 in (FStar_Getopt.noshort, "smtencoding.nl_arith_repr", (EnumStr ["native"; "wrapped"; "boxwrap"]), - uu___171) in - let uu___171 - = - let uu___172 - = + uu___173) in let uu___173 = let uu___174 = - text - "Toggle the representation of linear arithmetic functions in the SMT encoding:" in let uu___175 = let uu___176 = + text + "Toggle the representation of linear arithmetic functions in the SMT encoding:" in let uu___177 = let uu___178 = - text - "if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'" in let uu___179 = let uu___180 = text + "if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'" in + let uu___181 + = + let uu___182 + = + text "if 'native', use '+, -, -'" in - [uu___180] in - uu___178 + [uu___182] in + uu___180 :: - uu___179 in + uu___181 in FStar_Errors_Msg.bulleted - uu___177 in - let uu___177 + uu___179 in + let uu___179 = text "(default 'boxwrap')" in FStar_Pprint.op_Hat_Hat + uu___178 + uu___179 in + FStar_Pprint.op_Hat_Hat uu___176 uu___177 in - FStar_Pprint.op_Hat_Hat - uu___174 - uu___175 in (FStar_Getopt.noshort, "smtencoding.l_arith_repr", (EnumStr ["native"; "boxwrap"]), - uu___173) in - let uu___173 + uu___175) in + let uu___175 = - let uu___174 + let uu___176 = - let uu___175 + let uu___177 = text "Include an axiom in the SMT encoding to introduce proof-irrelevance from a constructive proof" in (FStar_Getopt.noshort, "smtencoding.valid_intro", BoolStr, - uu___175) in - let uu___175 + uu___177) in + let uu___177 = - let uu___176 + let uu___178 = - let uu___177 + let uu___179 = text "Include an axiom in the SMT encoding to eliminate proof-irrelevance into the existence of a proof witness" in (FStar_Getopt.noshort, "smtencoding.valid_elim", BoolStr, - uu___177) in - let uu___177 - = - let uu___178 - = + uu___179) in let uu___179 = let uu___180 = - text - "Split SMT verification conditions into several separate queries, one per goal. Helps with localizing errors." in let uu___181 = let uu___182 = + text + "Split SMT verification conditions into several separate queries, one per goal. Helps with localizing errors." in let uu___183 = - text - "Use 'no' to disable (this may reduce the quality of error messages)." in let uu___184 = let uu___185 = text - "Use 'on_failure' to split queries and retry when discharging fails (the default)" in + "Use 'no' to disable (this may reduce the quality of error messages)." in let uu___186 = let uu___187 = text + "Use 'on_failure' to split queries and retry when discharging fails (the default)" in + let uu___188 + = + let uu___189 + = + text "Use 'yes' to always split." in - [uu___187] in + [uu___189] in + uu___187 + :: + uu___188 in uu___185 :: uu___186 in - uu___183 - :: - uu___184 in FStar_Errors_Msg.bulleted - uu___182 in + uu___184 in FStar_Pprint.op_Hat_Hat - uu___180 - uu___181 in + uu___182 + uu___183 in (FStar_Getopt.noshort, "split_queries", (EnumStr ["no"; "on_failure"; "always"]), - uu___179) in - let uu___179 - = - let uu___180 - = - let uu___181 - = - text - "Do not use the lexical scope of tactics to improve binder names" in - (FStar_Getopt.noshort, - "tactic_raw_binders", - (Const - (Bool - true)), uu___181) in let uu___181 = @@ -2575,9 +2578,9 @@ let rec (specs_with_types : let uu___183 = text - "Do not recover from metaprogramming errors, and abort if one occurs" in + "Do not use the lexical scope of tactics to improve binder names" in (FStar_Getopt.noshort, - "tactics_failhard", + "tactic_raw_binders", (Const (Bool true)), @@ -2589,9 +2592,9 @@ let rec (specs_with_types : let uu___185 = text - "Print some rough information on tactics, such as the time they take to run" in + "Do not recover from metaprogramming errors, and abort if one occurs" in (FStar_Getopt.noshort, - "tactics_info", + "tactics_failhard", (Const (Bool true)), @@ -2603,9 +2606,9 @@ let rec (specs_with_types : let uu___187 = text - "Print a depth-indexed trace of tactic execution (Warning: very verbose)" in + "Print some rough information on tactics, such as the time they take to run" in (FStar_Getopt.noshort, - "tactic_trace", + "tactics_info", (Const (Bool true)), @@ -2617,11 +2620,12 @@ let rec (specs_with_types : let uu___189 = text - "Trace tactics up to a certain binding depth" in + "Print a depth-indexed trace of tactic execution (Warning: very verbose)" in (FStar_Getopt.noshort, - "tactic_trace_d", - (IntStr - "positive_integer"), + "tactic_trace", + (Const + (Bool + true)), uu___189) in let uu___189 = @@ -2630,12 +2634,11 @@ let rec (specs_with_types : let uu___191 = text - "Use NBE to evaluate metaprograms (experimental)" in + "Trace tactics up to a certain binding depth" in (FStar_Getopt.noshort, - "__tactics_nbe", - (Const - (Bool - true)), + "tactic_trace_d", + (IntStr + "positive_integer"), uu___191) in let uu___191 = @@ -2644,10 +2647,12 @@ let rec (specs_with_types : let uu___193 = text - "Attempt to normalize definitions marked as tcnorm (default 'true')" in + "Use NBE to evaluate metaprograms (experimental)" in (FStar_Getopt.noshort, - "tcnorm", - BoolStr, + "__tactics_nbe", + (Const + (Bool + true)), uu___193) in let uu___193 = @@ -2656,12 +2661,10 @@ let rec (specs_with_types : let uu___195 = text - "Print the time it takes to verify each top-level definition. This is just an alias for an invocation of the profiler, so it may not work well if combined with --profile. In particular, it implies --profile_group_by_decl." in + "Attempt to normalize definitions marked as tcnorm (default 'true')" in (FStar_Getopt.noshort, - "timing", - (Const - (Bool - true)), + "tcnorm", + BoolStr, uu___195) in let uu___195 = @@ -2670,9 +2673,9 @@ let rec (specs_with_types : let uu___197 = text - "Attach stack traces on errors" in + "Print the time it takes to verify each top-level definition. This is just an alias for an invocation of the profiler, so it may not work well if combined with --profile. In particular, it implies --profile_group_by_decl." in (FStar_Getopt.noshort, - "trace_error", + "timing", (Const (Bool true)), @@ -2684,9 +2687,9 @@ let rec (specs_with_types : let uu___199 = text - "Emit output formatted for debugging" in + "Attach stack traces on errors" in (FStar_Getopt.noshort, - "ugly", + "trace_error", (Const (Bool true)), @@ -2698,9 +2701,9 @@ let rec (specs_with_types : let uu___201 = text - "Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)" in + "Emit output formatted for debugging" in (FStar_Getopt.noshort, - "unthrottle_inductives", + "ugly", (Const (Bool true)), @@ -2712,9 +2715,9 @@ let rec (specs_with_types : let uu___203 = text - "Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects." in + "Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)" in (FStar_Getopt.noshort, - "unsafe_tactic_exec", + "unthrottle_inductives", (Const (Bool true)), @@ -2726,9 +2729,9 @@ let rec (specs_with_types : let uu___205 = text - "Use equality constraints when comparing higher-order types (Temporary)" in + "Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects." in (FStar_Getopt.noshort, - "use_eq_at_higher_order", + "unsafe_tactic_exec", (Const (Bool true)), @@ -2740,9 +2743,9 @@ let rec (specs_with_types : let uu___207 = text - "Use a previously recorded hints database for proof replay" in + "Use equality constraints when comparing higher-order types (Temporary)" in (FStar_Getopt.noshort, - "use_hints", + "use_eq_at_higher_order", (Const (Bool true)), @@ -2754,9 +2757,9 @@ let rec (specs_with_types : let uu___209 = text - "Admit queries if their hash matches the hash recorded in the hints database" in + "Use a previously recorded hints database for proof replay" in (FStar_Getopt.noshort, - "use_hint_hashes", + "use_hints", (Const (Bool true)), @@ -2768,11 +2771,12 @@ let rec (specs_with_types : let uu___211 = text - "Use compiled tactics from path" in + "Admit queries if their hash matches the hash recorded in the hints database" in (FStar_Getopt.noshort, - "use_native_tactics", - (PathStr - "path"), + "use_hint_hashes", + (Const + (Bool + true)), uu___211) in let uu___211 = @@ -2781,12 +2785,11 @@ let rec (specs_with_types : let uu___213 = text - "Do not run plugins natively and interpret them as usual instead" in + "Use compiled tactics from path" in (FStar_Getopt.noshort, - "no_plugins", - (Const - (Bool - true)), + "use_native_tactics", + (PathStr + "path"), uu___213) in let uu___213 = @@ -2795,9 +2798,9 @@ let rec (specs_with_types : let uu___215 = text - "Do not run the tactic engine before discharging a VC" in + "Do not run plugins natively and interpret them as usual instead" in (FStar_Getopt.noshort, - "no_tactics", + "no_plugins", (Const (Bool true)), @@ -2809,18 +2812,32 @@ let rec (specs_with_types : let uu___217 = text + "Do not run the tactic engine before discharging a VC" in + (FStar_Getopt.noshort, + "no_tactics", + (Const + (Bool + true)), + uu___217) in + let uu___217 + = + let uu___218 + = + let uu___219 + = + text "Prunes the context to include only the facts from the given namespace or fact id. Facts can be include or excluded using the [+|-] qualifier. For example --using_facts_from '* -FStar.Reflection +FStar.Compiler.List -FStar.Compiler.List.Tot' will remove all facts from FStar.Compiler.List.Tot.*, retain all remaining facts from FStar.Compiler.List.*, remove all facts from FStar.Reflection.*, and retain all the rest. Note, the '+' is optional: --using_facts_from 'FStar.Compiler.List' is equivalent to --using_facts_from '+FStar.Compiler.List'. Multiple uses of this option accumulate, e.g., --using_facts_from A --using_facts_from B is interpreted as --using_facts_from A^B." in (FStar_Getopt.noshort, "using_facts_from", (ReverseAccumulated (SimpleStr "One or more space-separated occurrences of '[+|-]( * | namespace | fact id)'")), - uu___217) in - let uu___217 + uu___219) in + let uu___219 = - let uu___218 + let uu___220 = - let uu___219 + let uu___221 = text "This does nothing and will be removed" in @@ -2829,12 +2846,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___219) in - let uu___219 + uu___221) in + let uu___221 = - let uu___220 + let uu___222 = - let uu___221 + let uu___223 = text "Display version number" in @@ -2842,7 +2859,7 @@ let rec (specs_with_types : "version", (WithSideEffect ((fun - uu___222 + uu___224 -> display_version (); @@ -2851,12 +2868,12 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___221) in - let uu___221 + uu___223) in + let uu___223 = - let uu___222 + let uu___224 = - let uu___223 + let uu___225 = text "Warn when (a -> b) is desugared to (a -> Tot b)" in @@ -2865,12 +2882,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___223) in - let uu___223 + uu___225) in + let uu___225 = - let uu___224 + let uu___226 = - let uu___225 + let uu___227 = text "Z3 command line options" in @@ -2879,12 +2896,12 @@ let rec (specs_with_types : (ReverseAccumulated (SimpleStr "option")), - uu___225) in - let uu___225 + uu___227) in + let uu___227 = - let uu___226 + let uu___228 = - let uu___227 + let uu___229 = text "Z3 options in smt2 format" in @@ -2893,12 +2910,12 @@ let rec (specs_with_types : (ReverseAccumulated (SimpleStr "option")), - uu___227) in - let uu___227 + uu___229) in + let uu___229 = - let uu___228 + let uu___230 = - let uu___229 + let uu___231 = text "Restart Z3 after each query; useful for ensuring proof robustness" in @@ -2907,12 +2924,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___229) in - let uu___229 + uu___231) in + let uu___231 = - let uu___230 + let uu___232 = - let uu___231 + let uu___233 = text "Set the Z3 per-query resource limit (default 5 units, taking roughtly 5s)" in @@ -2920,12 +2937,12 @@ let rec (specs_with_types : "z3rlimit", (IntStr "positive_integer"), - uu___231) in - let uu___231 + uu___233) in + let uu___233 = - let uu___232 + let uu___234 = - let uu___233 + let uu___235 = text "Set the Z3 per-query resource limit multiplier. This is useful when, say, regenerating hints and you want to be more lax. (default 1)" in @@ -2933,12 +2950,12 @@ let rec (specs_with_types : "z3rlimit_factor", (IntStr "positive_integer"), - uu___233) in - let uu___233 + uu___235) in + let uu___235 = - let uu___234 + let uu___236 = - let uu___235 + let uu___237 = text "Set the Z3 random seed (default 0)" in @@ -2946,12 +2963,12 @@ let rec (specs_with_types : "z3seed", (IntStr "positive_integer"), - uu___235) in - let uu___235 + uu___237) in + let uu___237 = - let uu___236 + let uu___238 = - let uu___237 + let uu___239 = text "Set the version of Z3 that is to be used. Default: 4.8.5" in @@ -2959,12 +2976,12 @@ let rec (specs_with_types : "z3version", (SimpleStr "version"), - uu___237) in - let uu___237 + uu___239) in + let uu___239 = - let uu___238 + let uu___240 = - let uu___239 + let uu___241 = text "Don't check positivity of inductive types" in @@ -2972,7 +2989,7 @@ let rec (specs_with_types : "__no_positivity", (WithSideEffect ((fun - uu___240 + uu___242 -> if warn_unsafe @@ -2983,75 +3000,63 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___239) in - let uu___239 - = - let uu___240 - = + uu___241) in let uu___241 = let uu___242 = - text - "The [-warn_error] option follows the OCaml syntax, namely:" in let uu___243 = let uu___244 = + text + "The [-warn_error] option follows the OCaml syntax, namely:" in let uu___245 = - text - "[r] is a range of warnings (either a number [n], or a range [n..n])" in let uu___246 = let uu___247 = text - "[-r] silences range [r]" in + "[r] is a range of warnings (either a number [n], or a range [n..n])" in let uu___248 = let uu___249 = text - "[+r] enables range [r] as warnings (NOTE: \"enabling\" an error will downgrade it to a warning)" in + "[-r] silences range [r]" in let uu___250 = let uu___251 = text + "[+r] enables range [r] as warnings (NOTE: \"enabling\" an error will downgrade it to a warning)" in + let uu___252 + = + let uu___253 + = + text "[@r] makes range [r] fatal." in - [uu___251] in + [uu___253] in + uu___251 + :: + uu___252 in uu___249 :: uu___250 in uu___247 :: uu___248 in - uu___245 - :: - uu___246 in FStar_Errors_Msg.bulleted - uu___244 in + uu___246 in FStar_Pprint.op_Hat_Hat - uu___242 - uu___243 in + uu___244 + uu___245 in (FStar_Getopt.noshort, "warn_error", (ReverseAccumulated (SimpleStr "")), - uu___241) in - let uu___241 - = - let uu___242 - = - let uu___243 - = - text - "Use normalization by evaluation as the default normalization strategy (default 'false')" in - (FStar_Getopt.noshort, - "use_nbe", - BoolStr, uu___243) in let uu___243 = @@ -3060,9 +3065,9 @@ let rec (specs_with_types : let uu___245 = text - "Use normalization by evaluation for normalizing terms before extraction (default 'false')" in + "Use normalization by evaluation as the default normalization strategy (default 'false')" in (FStar_Getopt.noshort, - "use_nbe_for_extraction", + "use_nbe", BoolStr, uu___245) in let uu___245 @@ -3072,9 +3077,9 @@ let rec (specs_with_types : let uu___247 = text - "Enforce trivial preconditions for unannotated effectful functions (default 'true')" in + "Use normalization by evaluation for normalizing terms before extraction (default 'false')" in (FStar_Getopt.noshort, - "trivial_pre_for_unannotated_effectful_fns", + "use_nbe_for_extraction", BoolStr, uu___247) in let uu___247 @@ -3084,12 +3089,24 @@ let rec (specs_with_types : let uu___249 = text + "Enforce trivial preconditions for unannotated effectful functions (default 'true')" in + (FStar_Getopt.noshort, + "trivial_pre_for_unannotated_effectful_fns", + BoolStr, + uu___249) in + let uu___249 + = + let uu___250 + = + let uu___251 + = + text "Debug messages for embeddings/unembeddings of natively compiled terms" in (FStar_Getopt.noshort, "__debug_embedding", (WithSideEffect ((fun - uu___250 + uu___252 -> FStar_Compiler_Effect.op_Colon_Equals debug_embedding @@ -3097,12 +3114,12 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___249) in - let uu___249 + uu___251) in + let uu___251 = - let uu___250 + let uu___252 = - let uu___251 + let uu___253 = text "Eagerly embed and unembed terms to primitive operations and plugins: not recommended except for benchmarking" in @@ -3110,7 +3127,7 @@ let rec (specs_with_types : "eager_embedding", (WithSideEffect ((fun - uu___252 + uu___254 -> FStar_Compiler_Effect.op_Colon_Equals eager_embedding @@ -3118,12 +3135,12 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___251) in - let uu___251 + uu___253) in + let uu___253 = - let uu___252 + let uu___254 = - let uu___253 + let uu___255 = text "Emit profiles grouped by declaration rather than by module" in @@ -3132,12 +3149,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___253) in - let uu___253 + uu___255) in + let uu___255 = - let uu___254 + let uu___256 = - let uu___255 + let uu___257 = text "Specific source locations in the compiler are instrumented with profiling counters. Pass `--profile_component FStar.TypeChecker` to enable all counters in the FStar.TypeChecker namespace. This option is a module or namespace selector, like many other options (e.g., `--extract`)" in @@ -3146,12 +3163,12 @@ let rec (specs_with_types : (Accumulated (SimpleStr "One or more space-separated occurrences of '[+|-]( * | namespace | module | identifier)'")), - uu___255) in - let uu___255 + uu___257) in + let uu___257 = - let uu___256 + let uu___258 = - let uu___257 + let uu___259 = text "Profiling can be enabled when the compiler is processing a given set of source modules. Pass `--profile FStar.Pervasives` to enable profiling when the compiler is processing any module in FStar.Pervasives. This option is a module or namespace selector, like many other options (e.g., `--extract`)" in @@ -3160,12 +3177,12 @@ let rec (specs_with_types : (Accumulated (SimpleStr "One or more space-separated occurrences of '[+|-]( * | namespace | module)'")), - uu___257) in - let uu___257 + uu___259) in + let uu___259 = - let uu___258 + let uu___260 = - let uu___259 + let uu___261 = text "Display this information" in @@ -3173,26 +3190,26 @@ let rec (specs_with_types : "help", (WithSideEffect ((fun - uu___260 + uu___262 -> ( - let uu___262 + let uu___264 = specs warn_unsafe in display_usage_aux - uu___262); + uu___264); FStar_Compiler_Effect.exit Prims.int_zero), (Const (Bool true)))), - uu___259) in - let uu___259 + uu___261) in + let uu___261 = - let uu___260 + let uu___262 = - let uu___261 + let uu___263 = text "List all debug keys and exit" in @@ -3200,7 +3217,7 @@ let rec (specs_with_types : "list_debug_keys", (WithSideEffect ((fun - uu___262 + uu___264 -> display_debug_keys (); @@ -3209,8 +3226,11 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___261) in - [uu___260] in + uu___263) in + [uu___262] in + uu___260 + :: + uu___261 in uu___258 :: uu___259 in @@ -3663,7 +3683,7 @@ let (settable_specs : (fun uu___ -> match uu___ with | ((uu___1, x, uu___2), uu___3) -> settable x) all_specs -let (uu___660 : +let (uu___661 : (((unit -> FStar_Getopt.parse_cmdline_res) -> unit) * (unit -> FStar_Getopt.parse_cmdline_res))) = @@ -3680,11 +3700,11 @@ let (uu___660 : (set1, call) let (set_error_flags_callback_aux : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = - match uu___660 with + match uu___661 with | (set_error_flags_callback_aux1, set_error_flags) -> set_error_flags_callback_aux1 let (set_error_flags : unit -> FStar_Getopt.parse_cmdline_res) = - match uu___660 with + match uu___661 with | (set_error_flags_callback_aux1, set_error_flags1) -> set_error_flags1 let (set_error_flags_callback : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = @@ -4185,6 +4205,8 @@ let (quake_hi : unit -> Prims.int) = fun uu___ -> get_quake_hi () let (quake_keep : unit -> Prims.bool) = fun uu___ -> get_quake_keep () let (query_cache : unit -> Prims.bool) = fun uu___ -> get_query_cache () let (query_stats : unit -> Prims.bool) = fun uu___ -> get_query_stats () +let (read_checked_file : unit -> Prims.string FStar_Pervasives_Native.option) + = fun uu___ -> get_read_checked_file () let (record_hints : unit -> Prims.bool) = fun uu___ -> get_record_hints () let (record_options : unit -> Prims.bool) = fun uu___ -> get_record_options () diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml index 1c969625188..02948141278 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml @@ -1996,6 +1996,8 @@ let (showable_const : FStar_Const.sconst FStar_Class_Show.showable) = let (showable_letbinding : FStar_Syntax_Syntax.letbinding FStar_Class_Show.showable) = { FStar_Class_Show.show = lb_to_string } +let (showable_modul : FStar_Syntax_Syntax.modul FStar_Class_Show.showable) = + { FStar_Class_Show.show = modul_to_string } let (pretty_term : FStar_Syntax_Syntax.term FStar_Class_PP.pretty) = { FStar_Class_PP.pp = term_to_doc } let (pretty_univ : FStar_Syntax_Syntax.universe FStar_Class_PP.pretty) = diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 6d70d7cca13..77e03c131fa 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -10386,7 +10386,8 @@ let (desugar_modul : if uu___5 then let uu___6 = - FStar_Syntax_Print.modul_to_string modul1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_modul modul1 in FStar_Compiler_Util.print1 "Module after desugaring:\n%s\n" uu___6 else ()); diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index 3f1cdcd3a68..45769f74760 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -5556,7 +5556,8 @@ let (check_module : FStar_Options.dump_module uu___3 in if uu___2 then - let uu___3 = FStar_Syntax_Print.modul_to_string m in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_modul m in FStar_Compiler_Util.print1 "Module before type checking:\n%s\n" uu___3 else ()); @@ -5783,7 +5784,8 @@ let (check_module : FStar_Options.dump_module uu___5 in if uu___4 then - let uu___5 = FStar_Syntax_Print.modul_to_string m1 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_modul m1 in FStar_Compiler_Util.print1 "Module after type checking:\n%s\n" uu___5 else ()); @@ -5874,7 +5876,8 @@ let (check_module : (m1.FStar_Syntax_Syntax.is_interface) } in let uu___6 = - FStar_Syntax_Print.modul_to_string normalized_module in + FStar_Class_Show.show FStar_Syntax_Print.showable_modul + normalized_module in FStar_Compiler_Util.print1 "%s\n" uu___6 else ()); (m1, env2))) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Universal.ml b/ocaml/fstar-lib/generated/FStar_Universal.ml index a748af0c9e6..5e48acab0f9 100644 --- a/ocaml/fstar-lib/generated/FStar_Universal.ml +++ b/ocaml/fstar-lib/generated/FStar_Universal.ml @@ -1277,7 +1277,9 @@ let (tc_one_file : FStar_Options.dump_module uu___4 in if uu___3 then - let uu___4 = FStar_Syntax_Print.modul_to_string tcmod in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_modul tcmod in FStar_Compiler_Util.print1 "Module after type checking:\n%s\n" uu___4 else ());