From e543e657cc0df8c7361e6c5f71e8ae0e50b36f76 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 30 Jan 2025 14:12:12 -0800 Subject: [PATCH] Options.Ext: refactor, and allow turning off boolean extensions by setting to 0/off/false instead of just empty --- src/basic/FStarC.Options.Ext.fst | 13 +++++++++++-- src/basic/FStarC.Options.Ext.fsti | 5 +++++ src/basic/FStarC.Plugins.fst | 2 +- src/basic/FStarC.Range.Type.fst | 2 +- src/extraction/FStarC.Extraction.ML.UEnv.fst | 2 +- src/smtencoding/FStarC.SMTEncoding.Encode.fst | 10 +++++----- src/smtencoding/FStarC.SMTEncoding.Pruning.fst | 4 ++-- src/smtencoding/FStarC.SMTEncoding.Solver.fst | 4 ++-- src/smtencoding/FStarC.SMTEncoding.SolverState.fst | 8 ++++---- src/syntax/FStarC.Syntax.Resugar.fst | 2 +- src/tactics/FStarC.Tactics.CtrlRewrite.fst | 2 +- src/tactics/FStarC.Tactics.V2.Basic.fst | 4 ++++ src/tactics/FStarC.Tactics.V2.Basic.fsti | 1 + src/tactics/FStarC.Tactics.V2.Primops.fst | 1 + src/typechecker/FStarC.TypeChecker.Cfg.fst | 2 +- src/typechecker/FStarC.TypeChecker.Rel.fst | 4 ++-- ulib/FStar.Stubs.Tactics.V2.Builtins.fsti | 4 ++++ ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml | 1 + 18 files changed, 48 insertions(+), 23 deletions(-) diff --git a/src/basic/FStarC.Options.Ext.fst b/src/basic/FStarC.Options.Ext.fst index 4c8ddc59582..d9c64464567 100644 --- a/src/basic/FStarC.Options.Ext.fst +++ b/src/basic/FStarC.Options.Ext.fst @@ -23,7 +23,11 @@ module BU = FStarC.Util type ext_state = | E : map : BU.psmap string -> ext_state -let cur_state = BU.mk_ref (E (BU.psmap_empty ())) +(* If we ever want to set any defaults, this is the place to do it. *) +let init : ext_state = + E (BU.psmap_empty ()) + +let cur_state = BU.mk_ref init (* Set a key-value pair in the map *) let set (k:key) (v:value) : unit = @@ -38,6 +42,11 @@ let get (k:key) : value = in r +let enabled (k:key) : bool = + let v = get k in + let v = String.lowercase v in + v <> "" && not (v = "off" || v = "false" || v = "0") + (* Find a home *) let is_prefix (s1 s2 : string) : ML bool = let open FStarC.String in @@ -67,4 +76,4 @@ let restore (s:ext_state) : unit = () let reset () : unit = - cur_state := E (BU.psmap_empty ()) + cur_state := init diff --git a/src/basic/FStarC.Options.Ext.fsti b/src/basic/FStarC.Options.Ext.fsti index 26aa1ab012c..a0cbae57e1a 100644 --- a/src/basic/FStarC.Options.Ext.fsti +++ b/src/basic/FStarC.Options.Ext.fsti @@ -29,6 +29,11 @@ val set (k:key) (v:value) : unit (* Get the value from the map, or return "" if not there *) val get (k:key) : value +(* For boolean-like options, return true if enabled. We consider an +extension enabled when set to a non-empty string what is NOT "off", +"false", or "0" (and this comparison is case-insensitive). *) +val enabled (k:key) : bool + (* Get a list of all KV pairs that "begin" with k, considered as a namespace. *) val getns (ns:string) : list (key & value) diff --git a/src/basic/FStarC.Plugins.fst b/src/basic/FStarC.Plugins.fst index e5ebae7151b..d21c88f5bc8 100644 --- a/src/basic/FStarC.Plugins.fst +++ b/src/basic/FStarC.Plugins.fst @@ -126,7 +126,7 @@ let compile_modules dir ms = if it could find a plugin with the proper name. This will fail hard if loading the plugin fails. *) let autoload_plugin (ext:string) : bool = - if Options.Ext.get "noautoload" <> "" then false else ( + if Options.Ext.enabled "noautoload" then false else ( if Debug.any () then BU.print1 "Trying to find a plugin for extension %s\n" ext; match Find.find_file (ext ^ ".cmxs") with diff --git a/src/basic/FStarC.Range.Type.fst b/src/basic/FStarC.Range.Type.fst index 4b13ade7863..21883db463b 100644 --- a/src/basic/FStarC.Range.Type.fst +++ b/src/basic/FStarC.Range.Type.fst @@ -93,7 +93,7 @@ let mk_rng file_name start_pos end_pos = { let mk_range f b e = let r = mk_rng f b e in range_of_rng r r let string_of_file_name f = - if Options.Ext.get "fstar:no_absolute_paths" = "1" then + if Options.Ext.enabled "fstar:no_absolute_paths" then BU.basename f else if Options.ide () then try diff --git a/src/extraction/FStarC.Extraction.ML.UEnv.fst b/src/extraction/FStarC.Extraction.ML.UEnv.fst index 64e10d4ee89..44651801cc1 100644 --- a/src/extraction/FStarC.Extraction.ML.UEnv.fst +++ b/src/extraction/FStarC.Extraction.ML.UEnv.fst @@ -254,7 +254,7 @@ let is_fv_type g fv = let no_fstar_stubs_ns (ns : list mlsymbol) : list mlsymbol = match ns with - | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.get "__guts" <> "" -> "FStarC"::rest + | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.enabled "__guts" -> "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. *) diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index 6a414bc8185..d3df2f34161 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Encode.fst @@ -824,7 +824,7 @@ let encode_top_level_let : let app_is_prop = Term.mk_subtype_of_unit app in if should_encode_logical then ( - if is_sub_singleton && Options.Ext.get "retain_old_prop_typing" = "" + if is_sub_singleton && not (Options.Ext.enabled "retain_old_prop_typing") then ( Util.mkAssume(mkForall (S.range_of_lbname lbn) ([[app_is_prop]], vars, mkImp(mk_and_l binder_guards, mk_Valid <| app_is_prop)), @@ -1064,7 +1064,7 @@ let encode_sig_inductive (env:env_t) (se:sigelt) let is_l = mk_data_tester env l xx in let inversion_case, decls' = if injective_type_params - || Options.Ext.get "compat:injectivity" <> "" + || Options.Ext.enabled "compat:injectivity" then ( let _, data_t = Env.lookup_datacon env.tcenv l in let args, res = U.arrow_formals data_t in @@ -1183,7 +1183,7 @@ let encode_datacon (env:env_t) (se:sigelt) let s_fuel_tm = mkApp("SFuel", [fuel_tm]) in let vars, guards, env', binder_decls, names = encode_binders (Some fuel_tm) formals env in let injective_type_params = - injective_type_params || Options.Ext.get "compat:injectivity" <> "" + injective_type_params || Options.Ext.enabled "compat:injectivity" in let fields = names |> @@ -1345,11 +1345,11 @@ let encode_datacon (env:env_t) (se:sigelt) | Tm_fvar fv -> if BU.for_some (S.fv_eq_lid fv) mutuals then Some (bs, c) - else if Options.Ext.get "compat:2954" <> "" + else if Options.Ext.enabled "compat:2954" then (warn_compat(); Some (bs, c)) //compatibility mode else None | _ -> - if Options.Ext.get "compat:2954" <> "" + if Options.Ext.enabled "compat:2954" then (warn_compat(); Some (bs, c)) //compatibility mode else None ) diff --git a/src/smtencoding/FStarC.SMTEncoding.Pruning.fst b/src/smtencoding/FStarC.SMTEncoding.Pruning.fst index 48c87fc48bf..4451cdccf29 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Pruning.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Pruning.fst @@ -47,7 +47,7 @@ type pruning_state = { } let debug (f: unit -> unit) : unit = - if Options.Ext.get "debug_context_pruning" <> "" + if Options.Ext.enabled "debug_context_pruning" then f() let print_pruning_state (p:pruning_state) @@ -461,7 +461,7 @@ let prune (p:pruning_state) (roots:list decl) | Some a -> [a]) (reached_names@p.ambients) in - // if Options.Ext.get "debug_context_pruning" <> "" + // if Options.Ext.enabled "debug_context_pruning" // then ( // BU.print1 "Retained %s assumptions\n" (show (List.length reached_assumptions)) // ); diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst index c6cd200a8b0..3673d0892e7 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Solver.fst @@ -605,7 +605,7 @@ let query_info settings z3result = let msg = if used_hint settings then Pprint.doc_of_string "Hint-replay failed" :: msg else msg in FStarC.Errors.log_issue range FStarC.Errors.Warning_HitReplayFailed msg) end - else if Options.Ext.get "profile_context" <> "" + else if Options.Ext.enabled "profile_context" then match z3result.z3result_status with | UNSAT core -> process_unsat_core core | _ -> () @@ -1221,7 +1221,7 @@ let get_cfg env : solver_cfg = ; valid_intro = Options.smtencoding_valid_intro () ; valid_elim = Options.smtencoding_valid_elim () ; z3version = Options.z3_version () - ; context_pruning = Options.Ext.get "context_pruning" <> "" + ; context_pruning = Options.Ext.enabled "context_pruning" } let save_cfg env = diff --git a/src/smtencoding/FStarC.SMTEncoding.SolverState.fst b/src/smtencoding/FStarC.SMTEncoding.SolverState.fst index 31b38d51e10..eebd5dd11da 100644 --- a/src/smtencoding/FStarC.SMTEncoding.SolverState.fst +++ b/src/smtencoding/FStarC.SMTEncoding.SolverState.fst @@ -80,7 +80,7 @@ let solver_state_to_string (s:solver_state) = instance showable_solver_state : showable solver_state = { show = solver_state_to_string } let debug (msg:string) (s0 s1:solver_state) = - if Options.Ext.get "debug_solver_state" <> "" + if Options.Ext.enabled "debug_solver_state" then ( BU.print3 "Debug (%s):{\n\t before=%s\n\t after=%s\n}" msg (solver_state_to_string s0) @@ -317,7 +317,7 @@ let give_now (resetting:bool) (ds:list decl) (s:solver_state) let give_aux resetting (ds:list decl) (s:solver_state) : solver_state -= if Options.Ext.get "context_pruning" <> "" += if Options.Ext.enabled "context_pruning" then give_delay_assumptions resetting ds s else give_now resetting ds s @@ -460,7 +460,7 @@ let filter_with_unsat_core queryid (core:U.unsat_core) (s:solver_state) U.filter core all_decls let would_have_pruned (s:solver_state) = - if Options.Ext.get "context_pruning_sim" = "" + if not (Options.Ext.enabled "context_pruning_sim") then None else (*find the first level with pruning roots, and prune the context with respect to them *) @@ -479,7 +479,7 @@ let would_have_pruned (s:solver_state) = let flush (s:solver_state) : list decl & solver_state = let s = - if Options.Ext.get "context_pruning" <> "" + if Options.Ext.enabled "context_pruning" then ( (*find the first level with pruning roots, and prune the context with respect to them *) let rec aux levels = diff --git a/src/syntax/FStarC.Syntax.Resugar.fst b/src/syntax/FStarC.Syntax.Resugar.fst index de239bfc176..a97ec986883 100644 --- a/src/syntax/FStarC.Syntax.Resugar.fst +++ b/src/syntax/FStarC.Syntax.Resugar.fst @@ -530,7 +530,7 @@ let rec resugar_term' (env: DsEnv.env) (t : S.term) : A.term = mk (A.App (acc, aa, qq))) h else if not (Options.print_implicits ()) - && Options.Ext.get "show_hide_reveal" = "" + && not (Options.Ext.enabled "show_hide_reveal") && is_hide_or_reveal e && List.length args = 1 //args already filtered then ( diff --git a/src/tactics/FStarC.Tactics.CtrlRewrite.fst b/src/tactics/FStarC.Tactics.CtrlRewrite.fst index 2929f24f764..7b895b67215 100644 --- a/src/tactics/FStarC.Tactics.CtrlRewrite.fst +++ b/src/tactics/FStarC.Tactics.CtrlRewrite.fst @@ -109,7 +109,7 @@ let __do_rewrite (* unrefine typ as is done for the type arg of eq2 *) let typ = - if Options.Ext.get "__unrefine" <> "" then + if Options.Ext.enabled "__unrefine" then let typ_norm = N.unfold_whnf' [Env.DontUnfoldAttr [Parser.Const.do_not_unrefine_attr]] env typ in if Tm_refine? (SS.compress typ_norm).n then (* It is indeed a refinement, normalize again to remove them. *) diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fst b/src/tactics/FStarC.Tactics.V2.Basic.fst index 01909d49aff..b3a1f2fe3f8 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fst +++ b/src/tactics/FStarC.Tactics.V2.Basic.fst @@ -2223,6 +2223,10 @@ let ext_getv (k:string) : tac string = return () ;! return (Options.Ext.get k) +let ext_enabled (k:string) : tac bool + = return () ;! + return (Options.Ext.enabled k) + let ext_getns (ns:string) : tac (list (string & string)) = return () ;! return (Options.Ext.getns ns) diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fsti b/src/tactics/FStarC.Tactics.V2.Basic.fsti index fa02b229630..474d268d08a 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fsti +++ b/src/tactics/FStarC.Tactics.V2.Basic.fsti @@ -122,6 +122,7 @@ val free_uvars : term -> tac (list Z.t) val all_ext_options : unit -> tac (list (string & string)) val ext_getv : string -> tac string +val ext_enabled : string -> tac bool val ext_getns : string -> tac (list (string & string)) val alloc : 'a -> tac (tref 'a) diff --git a/src/tactics/FStarC.Tactics.V2.Primops.fst b/src/tactics/FStarC.Tactics.V2.Primops.fst index 49d2f64e234..e37b1406e91 100644 --- a/src/tactics/FStarC.Tactics.V2.Primops.fst +++ b/src/tactics/FStarC.Tactics.V2.Primops.fst @@ -224,6 +224,7 @@ let ops = [ mk_tac_step_1 0 "free_uvars" free_uvars free_uvars; mk_tac_step_1 0 "all_ext_options" all_ext_options all_ext_options; mk_tac_step_1 0 "ext_getv" ext_getv ext_getv; + mk_tac_step_1 0 "ext_enabled" ext_enabled ext_enabled; mk_tac_step_1 0 "ext_getns" ext_getns ext_getns; mk_tac_step_2 1 "alloc" diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fst b/src/typechecker/FStarC.TypeChecker.Cfg.fst index f2b7593dfa3..08c9df18cf4 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fst +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fst @@ -430,7 +430,7 @@ let config' psteps s e = memoize_lazy = true; normalize_pure_lets = (not steps.pure_subterms_within_computations) || Options.normalize_pure_terms_for_extraction(); reifying = false; - compat_memo_ignore_cfg = Options.Ext.get "compat:normalizer_memo_ignore_cfg" <> ""; + compat_memo_ignore_cfg = Options.Ext.enabled "compat:normalizer_memo_ignore_cfg"; } let config s e = config' [] s e diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index b51bb586032..0b14f2373fa 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -2210,7 +2210,7 @@ let rec solve (probs :worklist) : solution = | _ -> false in let maybe_expand (tp:tprob) : tprob = - if Options.Ext.get "__unrefine" <> "" && tp.relation = SUB && is_expand_uvar tp.rhs + if Options.Ext.enabled "__unrefine" && tp.relation = SUB && is_expand_uvar tp.rhs then let lhs = tp.lhs in let lhs_norm = N.unfold_whnf' [Env.DontUnfoldAttr [PC.do_not_unrefine_attr]] (p_env probs hd) lhs in @@ -5642,7 +5642,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) BU.print1 "Deferring implicit due to open ctx/typ %s\n" (show ctx_u); until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl ) else if is_open && not (meta_tac_allowed_for_open_problem tac) - && Options.Ext.get "compat:open_metas" = "" then ( // i.e. compat option unset + && not (Options.Ext.enabled "compat:open_metas") then ( // i.e. compat option unset (* If the tactic is not explicitly whitelisted to run with open problems, then defer. *) until_fixpoint ((hd, Implicit_unresolved)::out, changed, defer_open_metas) tl diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index 9e145dc2e67..c883d904e5c 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -478,6 +478,10 @@ val all_ext_options : unit -> Tac (list (string & string)) is returned if the key was unset. *) val ext_getv (k:string) : Tac string +(* Returns true iff the extension flag is enabled. I.e. it's a non-empty +string that is not 0/off/false. *) +val ext_enabled (k:string) : Tac bool + (* Return all k/v pairs in the state which are within the given namespace. *) val ext_getns (ns:string) : Tac (list (string & string)) diff --git a/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml index 7d1bf2ef51f..f47e475f23a 100644 --- a/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml +++ b/ulib/ml/plugin/FStarC_Tactics_V2_Builtins.ml @@ -136,6 +136,7 @@ let t_smt_sync = from_tac_1 "B.t_smt_sync" B.t_smt_sync let free_uvars = from_tac_1 "B.free_uvars" B.free_uvars let all_ext_options = from_tac_1 "B.all_ext_options" B.all_ext_options let ext_getv = from_tac_1 "B.ext_getv" B.ext_getv +let ext_enabled = from_tac_1 "B.ext_enabled" B.ext_enabled let ext_getns = from_tac_1 "B.ext_getns" B.ext_getns let alloc x = from_tac_1 "B.alloc" B.alloc x