Options.Ext: refactor, and allow turning off boolean extensions by se…

…tting to 0/off/false instead of just empty

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

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)

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

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

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. *)

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
                             )

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))
   // );

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 =

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 =

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 (

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. *)

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)

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)

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"

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

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

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))

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