From 60117c7d26c253448bf33bf4d472127c2d035353 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 27 Aug 2024 20:11:33 -0700
Subject: [PATCH 1/3] Options: fix stack handling, purify, modularize --ext,
make it faster
---
src/Makefile.boot | 2 +-
src/basic/FStar.Compiler.Range.Ops.fst | 2 +-
src/basic/FStar.Options.Ext.fst | 70 +++++++
src/basic/FStar.Options.Ext.fsti | 42 ++++
src/basic/FStar.Options.fst | 203 +++++++++----------
src/basic/FStar.Options.fsti | 11 +-
src/smtencoding/FStar.SMTEncoding.Encode.fst | 8 +-
src/tactics/FStar.Tactics.V1.Basic.fst | 6 +-
src/tactics/FStar.Tactics.V2.Basic.fst | 12 +-
src/tosyntax/FStar.ToSyntax.ToSyntax.fst | 15 +-
src/typechecker/FStar.TypeChecker.Cfg.fst | 2 +-
src/typechecker/FStar.TypeChecker.Rel.fst | 2 +-
12 files changed, 234 insertions(+), 141 deletions(-)
create mode 100644 src/basic/FStar.Options.Ext.fst
create mode 100644 src/basic/FStar.Options.Ext.fsti
diff --git a/src/Makefile.boot b/src/Makefile.boot
index 43a4145f6af..eedcf253c28 100644
--- a/src/Makefile.boot
+++ b/src/Makefile.boot
@@ -37,7 +37,7 @@ EXTRACT_NAMESPACES=FStar.Extraction FStar.Parser \
# TODO: Do we really need this anymore? Which (implementation) modules
# from src/basic are *not* extracted?
EXTRACT_MODULES=FStar.Pervasives FStar.Common FStar.Thunk \
- FStar.VConfig FStar.Options FStar.Ident FStar.Errors FStar.Errors.Codes \
+ FStar.VConfig FStar.Options FStar.Options.Ext FStar.Ident FStar.Errors FStar.Errors.Codes \
FStar.Errors.Msg FStar.Errors.Raise FStar.Const \
FStar.Compiler.Order FStar.Order FStar.Dependencies \
FStar.Interactive.CompletionTable \
diff --git a/src/basic/FStar.Compiler.Range.Ops.fst b/src/basic/FStar.Compiler.Range.Ops.fst
index 6cf7eb0afd8..937b1d24333 100644
--- a/src/basic/FStar.Compiler.Range.Ops.fst
+++ b/src/basic/FStar.Compiler.Range.Ops.fst
@@ -49,7 +49,7 @@ let string_of_pos pos =
format2 "%s,%s" (string_of_int pos.line) (string_of_int pos.col)
let string_of_file_name f =
if Options.ide () then
- if Options.ext_getv "fstar:no_absolute_paths" = "1" then
+ if Options.Ext.get "fstar:no_absolute_paths" = "1" then
basename f
else begin
try
diff --git a/src/basic/FStar.Options.Ext.fst b/src/basic/FStar.Options.Ext.fst
new file mode 100644
index 00000000000..513220713a4
--- /dev/null
+++ b/src/basic/FStar.Options.Ext.fst
@@ -0,0 +1,70 @@
+(*
+ Copyright 2008-2024 Microsoft Research
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+*)
+module FStar.Options.Ext
+
+open FStar.Compiler
+open FStar.Compiler.Effect
+open FStar.Class.Show
+module BU = FStar.Compiler.Util
+
+type ext_state =
+ | E : map : BU.psmap string -> ext_state
+
+let cur_state = BU.mk_ref (E (BU.psmap_empty ()))
+
+(* Set a key-value pair in the map *)
+let set (k:key) (v:value) : unit =
+ cur_state := E (BU.psmap_add (!cur_state).map k v)
+
+(* Get the value from the map, or return "" if not there *)
+let get (k:key) : value =
+ let r =
+ match BU.psmap_try_find (!cur_state).map k with
+ | None -> ""
+ | Some v -> v
+ in
+ r
+
+(* Find a home *)
+let is_prefix (s1 s2 : string) : ML bool =
+ let open FStar.Compiler.String in
+ let l1 = length s1 in
+ let l2 = length s2 in
+ l2 >= l1 && substring s2 0 l1 = s1
+
+(* Get a list of all KV pairs that "begin" with k, considered
+as a namespace. *)
+let getns (ns:string) : list (key & value) =
+ let f k v acc =
+ if (ns^":") `is_prefix` k
+ then (k, v) :: acc
+ else acc
+ in
+ BU.psmap_fold (!cur_state).map f []
+
+let all () : list (key & value) =
+ let f k v acc = (k, v) :: acc in
+ BU.psmap_fold (!cur_state).map f []
+
+let save () : ext_state =
+ !cur_state
+
+let restore (s:ext_state) : unit =
+ cur_state := s;
+ ()
+
+let reset () : unit =
+ cur_state := E (BU.psmap_empty ())
diff --git a/src/basic/FStar.Options.Ext.fsti b/src/basic/FStar.Options.Ext.fsti
new file mode 100644
index 00000000000..bed8dda6d90
--- /dev/null
+++ b/src/basic/FStar.Options.Ext.fsti
@@ -0,0 +1,42 @@
+(*
+ Copyright 2008-2024 Microsoft Research
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+*)
+module FStar.Options.Ext
+
+open FStar.Compiler.Effect
+
+type key = string
+type value = string
+
+new
+val ext_state : Type0
+
+(* Set a key-value pair in the map *)
+val set (k:key) (v:value) : unit
+
+(* Get the value from the map, or return "" if not there *)
+val get (k:key) : value
+
+(* Get a list of all KV pairs that "begin" with k, considered
+as a namespace. *)
+val getns (ns:string) : list (key & value)
+
+(* List all pairs *)
+val all () : list (key & value)
+
+val save () : ext_state
+val restore (s:ext_state) : unit
+
+val reset () : unit
diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst
index 3bb87f1fa1b..329ae67c17e 100644
--- a/src/basic/FStar.Options.fst
+++ b/src/basic/FStar.Options.fst
@@ -31,6 +31,8 @@ module FC = FStar.Common
module Util = FStar.Compiler.Util
module List = FStar.Compiler.List
+module Ext = FStar.Options.Ext
+
let debug_embedding = mk_ref false
let eager_embedding = mk_ref false
@@ -92,58 +94,78 @@ let copy_optionstate m = Util.smap_copy m
*
* We also keep a snapshot of the Debug module's state.
*)
-let fstar_options : ref (list (list (Debug.saved_state & optionstate))) = Util.mk_ref []
+let history1 = Debug.saved_state & Ext.ext_state & optionstate
-let internal_peek () = snd <| List.hd (List.hd !fstar_options)
-let peek () = copy_optionstate (internal_peek())
-let pop () = // already signal-atomic
- match !fstar_options with
- | []
- | [_] -> failwith "TOO MANY POPS!"
- | _::tl ->
- fstar_options := tl
+let fstar_options : ref optionstate = Util.mk_ref (Util.psmap_empty ())
-let push () = // already signal-atomic
- let new_st =
- List.hd !fstar_options |>
- List.map (fun (dbg, opts) -> (dbg, copy_optionstate opts))
- in
- fstar_options := new_st :: !fstar_options
+let history : ref (list (list history1)) =
+ Util.mk_ref [] // IRRELEVANT: see clear() below
+
+let peek () = !fstar_options
+
+let internal_push () =
+ let lev1::rest = !history in
+ let newhd = (Debug.snapshot (), Ext.save (), !fstar_options) in
+ history := (newhd :: lev1) :: rest
let internal_pop () =
- let curstack = List.hd !fstar_options in
- match curstack with
- | [] -> failwith "impossible: empty current option stack"
- | [_] -> false
- | _::tl ->
- fstar_options := tl :: List.tl !fstar_options;
- Debug.restore (fst (List.hd tl));
+ let lev1::rest = !history in
+ match lev1 with
+ | [] -> false
+ | (dbg, ext, opts)::lev1' ->
+ Debug.restore dbg;
+ Ext.restore ext;
+ fstar_options := opts;
+ history := lev1' :: rest;
true
-let internal_push () =
- let curstack = List.hd !fstar_options in
- let stack' = (Debug.snapshot (), copy_optionstate (snd <| List.hd curstack)) :: curstack in
- fstar_options := stack' :: List.tl !fstar_options
+let push () = // already signal-atomic
+ (* This turns a stack like
+
+ 4
+ 3
+ 2 1 current:5
+ into:
+ 5
+ 4 4
+ 3 3
+ 2 2 1 current:5
+
+ i.e. current state does not change, and
+ current minor stack does not change. The
+ "next" previous stack (now with 2,3,4,5)
+ has a copy of 5 at the top so we can restore regardless
+ of what we do in the current stack or the current state. *)
+
+ internal_push ();
+ let lev1::_ = !history in
+ history := lev1 :: !history;
+ ignore (internal_pop());
+ ()
+
+let pop () = // already signal-atomic
+ match !history with
+ | [] -> failwith "TOO MANY POPS!"
+ | _::levs ->
+ history := levs;
+ if not (internal_pop ()) then
+ failwith "aaa!!!"
let set o =
- match !fstar_options with
- | [] -> failwith "set on empty option stack"
- | []::_ -> failwith "set on empty current option stack"
- | ((dbg, _)::tl)::os ->
- fstar_options := (((dbg, o)::tl)::os)
+ fstar_options := o
-let snapshot () = Common.snapshot push fstar_options ()
-let rollback depth = Common.rollback pop fstar_options depth
+let snapshot () = Common.snapshot push history ()
+let rollback depth = Common.rollback pop history depth
let set_option k v =
- let map : optionstate = internal_peek() in
+ let map : optionstate = peek() in
if k = "report_assumes"
- then match Util.smap_try_find map k with
+ then match Util.psmap_try_find map k with
| Some (String "error") ->
//It's already set to error; ignore any attempt to change it
()
- | _ -> Util.smap_add map k v
- else Util.smap_add map k v
+ | _ -> fstar_options := Util.psmap_add map k v
+ else fstar_options := Util.psmap_add map k v
let set_option' (k,v) = set_option k v
let set_admit_smt_queries (b:bool) = set_option "admit_smt_queries" (Bool b)
@@ -153,7 +175,7 @@ let defaults =
("abort_on" , Int 0);
("admit_smt_queries" , Bool false);
("admit_except" , Unset);
- ("disallow_unification_guards" , Bool false);
+ ("disallow_unification_guards" , Bool false);
("already_cached" , Unset);
("cache_checked_modules" , Bool false);
("cache_dir" , Unset);
@@ -176,7 +198,7 @@ let defaults =
("eager_subtyping" , Bool false);
("error_contexts" , Bool false);
("expose_interfaces" , Bool false);
- ("ext" , List []);
+ ("ext" , Unset);
("extract" , Unset);
("extract_all" , Bool false);
("extract_module" , List []);
@@ -292,19 +314,20 @@ let defaults =
]
let init () =
- let o = internal_peek () in
- Util.smap_clear o;
- defaults |> List.iter set_option' //initialize it with the default values
+ Debug.disable_all ();
+ Ext.reset ();
+ fstar_options := Util.psmap_empty ();
+ defaults |> List.iter set_option' //initialize it with the default values
let clear () =
- let o = Util.smap_create 50 in
- fstar_options := [[(Debug.snapshot (), o)]]; //clear and reset the options stack
- init()
+ history := [[]];
+ init()
-let _run = clear()
+(* Run it now. *)
+let _ = clear ()
let get_option s =
- match Util.smap_try_find (internal_peek()) s with
+ match Util.psmap_try_find (peek ()) s with
| None -> failwith ("Impossible: option " ^s^ " not found")
| Some s -> s
@@ -335,7 +358,7 @@ let set_verification_options o =
"no_plugins";
"no_tactics";
"z3cliopt";
- "z3smtopt";
+ "z3smtopt";
"z3refresh";
"z3rlimit";
"z3rlimit_factor";
@@ -343,7 +366,7 @@ let set_verification_options o =
"z3version";
"trivial_pre_for_unannotated_effectful_fns";
] in
- List.iter (fun k -> set_option k (Util.smap_try_find o k |> Util.must)) verifopts
+ List.iter (fun k -> set_option k (Util.psmap_try_find o k |> Util.must)) verifopts
let lookup_opt s c =
c (get_option s)
@@ -372,7 +395,6 @@ let get_dump_module () = lookup_opt "dump_module"
let get_eager_subtyping () = lookup_opt "eager_subtyping" as_bool
let get_error_contexts () = lookup_opt "error_contexts" as_bool
let get_expose_interfaces () = lookup_opt "expose_interfaces" as_bool
-let get_ext () = lookup_opt "ext" (as_option (as_list as_string))
let get_extract () = lookup_opt "extract" (as_option (as_list as_string))
let get_extract_module () = lookup_opt "extract_module" (as_list as_string)
let get_extract_namespace () = lookup_opt "extract_namespace" (as_list as_string)
@@ -671,7 +693,7 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
let open FStar.Errors.Msg in
let text (s:string) : document = flow (break_ 1) (words s) in
[
- ( noshort, "abort_on",
+ ( noshort, "abort_on",
PostProcessed ((function Int x -> abort_counter := x; Int x
| x -> failwith "?"), IntStr "non-negative integer"),
text "Abort on the n-th error or warning raised. Useful in combination with --trace_error. Count starts at 1, use 0 to disable. (default 0)");
@@ -822,7 +844,17 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
( noshort,
"ext",
- ReverseAccumulated (SimpleStr "One or more semicolon separated occurrences of key-value pairs"),
+ PostProcessed (
+ (fun o ->
+ let parse_ext (s:string) : list (string & string) =
+ let exts = Util.split s ";" in
+ List.collect (fun s ->
+ match Util.split s "=" with
+ | [k;v] -> [(k,v)]
+ | _ -> [s, "1"]) exts
+ in
+ as_comma_string_list o |> List.collect parse_ext |> List.iter (fun (k, v) -> Ext.set k v);
+ o), ReverseAccumulated (SimpleStr "extension knobs")),
text "These options are set in extensions option map. Keys are usually namespaces separated by \":\". \
E.g., 'pulse:verbose=1;my:extension:option=xyz;foo:bar=baz'. \
These options are typically interpreted by extensions. \
@@ -1577,7 +1609,7 @@ let settable = function
| "using_facts_from"
| "warn_error"
| "z3cliopt"
- | "z3smtopt"
+ | "z3smtopt"
| "z3refresh"
| "z3rlimit"
| "z3rlimit_factor"
@@ -1819,15 +1851,15 @@ let parse_settings ns : list (list string & bool) =
let admit_smt_queries () = get_admit_smt_queries ()
let admit_except () = get_admit_except ()
-let compat_pre_core_should_register () =
+let compat_pre_core_should_register () =
match get_compat_pre_core() with
| Some 0 -> false
| _ -> true
-let compat_pre_core_should_check () =
+let compat_pre_core_should_check () =
match get_compat_pre_core() with
- | Some 0
+ | Some 0
| Some 1 -> false
- | _ -> true
+ | _ -> true
let compat_pre_core_set () =
match get_compat_pre_core() with
| None -> false
@@ -1898,7 +1930,7 @@ let ide () = get_ide ()
let ide_id_info_off () = get_ide_id_info_off ()
let ide_file_name_st =
let v = Util.mk_ref (None #string) in
- let set f =
+ let set f =
match !v with
| None -> v := Some f
| Some _ -> failwith "ide_file_name_st already set" in
@@ -2274,7 +2306,7 @@ let get_vconfig () =
no_plugins = get_no_plugins ();
no_tactics = get_no_tactics ();
z3cliopt = get_z3cliopt ();
- z3smtopt = get_z3smtopt ();
+ z3smtopt = get_z3smtopt ();
z3refresh = get_z3refresh ();
z3rlimit = get_z3rlimit ();
z3rlimit_factor = get_z3rlimit_factor ();
@@ -2312,7 +2344,7 @@ let set_vconfig (vcfg:vconfig) : unit =
set_option "no_plugins" (Bool vcfg.no_plugins);
set_option "no_tactics" (Bool vcfg.no_tactics);
set_option "z3cliopt" (List (List.map String vcfg.z3cliopt));
- set_option "z3smtopt" (List (List.map String vcfg.z3smtopt));
+ set_option "z3smtopt" (List (List.map String vcfg.z3smtopt));
set_option "z3refresh" (Bool vcfg.z3refresh);
set_option "z3rlimit" (Int vcfg.z3rlimit);
set_option "z3rlimit_factor" (Int vcfg.z3rlimit_factor);
@@ -2321,54 +2353,3 @@ let set_vconfig (vcfg:vconfig) : unit =
set_option "trivial_pre_for_unannotated_effectful_fns" (Bool vcfg.trivial_pre_for_unannotated_effectful_fns);
set_option "reuse_hint_for" (option_as String vcfg.reuse_hint_for);
()
-
-// --ext "ext1:opt1;ext2:opt2;ext3:opt3"
-// An entry e that is not of the form a:b
-// is treated as e:"1". We morally reserve the empty
-// string for "disabling" an option.
-//
-// This could all be much more efficient by just storing
-// a hash table in the optionstate.
-
-let parse_ext (s:string) : list (string & string) =
- let exts = Util.split s ";" in
- List.collect (fun s ->
- match Util.split s "=" with
- | [k;v] -> [(k,v)]
- | _ -> [s, "1"]) exts
-
-(* Deduplicates according to keys, favors the last occurrence (consistent
-with "ext" begin ReverseAccumulated *)
-let ext_dedup #a (l : list (string & a)) : list (string & a) =
- //fold_right (fun (k,v) rest -> (k,v) :: List.filter (fun (k', _) -> k<>k') rest) l []
- fold_right (fun (k,v) rest -> if List.existsb (fun (k', _) -> k=k') rest
- then rest
- else (k,v) :: rest) l []
-
-let all_ext_options () : list (string & string) =
- let ext = get_ext () in
- match ext with
- | None -> []
- | Some strs ->
- strs |> List.collect parse_ext
- |> ext_dedup
-
-let ext_getv (k:string) : string =
- let ext = all_ext_options () in
- (* Get the value from the map, or return "" if not there *)
- Util.dflt "" (
- Util.find_map ext (fun (k',v) -> if k = k' then Some v else None))
-
-(* Get a list of all KV pairs that "begin" with k, considered
-as a namespace. *)
-let ext_getns (ns:string) : list (string & string) =
- let is_prefix s1 s2 : ML bool =
- let l1 = length s1 in
- let l2 = length s2 in
- l2 >= l1 &&
- substring s2 0 l1 = s1
- in
- let exts = all_ext_options () in
- exts |>
- List.filter_map (fun (k',v) ->
- if k' = ns || is_prefix (ns^":") k' then Some (k',v) else None)
diff --git a/src/basic/FStar.Options.fsti b/src/basic/FStar.Options.fsti
index 7b7d94f8b2f..1821ae70c9f 100644
--- a/src/basic/FStar.Options.fsti
+++ b/src/basic/FStar.Options.fsti
@@ -21,6 +21,9 @@ open FStar.BaseTypes
open FStar.VConfig
open FStar.Compiler
+type codegen_t =
+ | OCaml | FSharp | Krml | Plugin | Extension
+
//let __test_norm_all = Util.mk_ref false
type split_queries_t = | No | OnFailure | Always
@@ -33,7 +36,7 @@ type option_val =
| List of list option_val
| Unset
-type optionstate = FStar.Compiler.Util.smap option_val
+type optionstate = FStar.Compiler.Util.psmap option_val
type opt_type =
| Const of option_val
@@ -104,8 +107,6 @@ val cache_checked_modules : unit -> bool
val cache_off : unit -> bool
val print_cache_version : unit -> bool
val cmi : unit -> bool
-type codegen_t =
- | OCaml | FSharp | Krml | Plugin | Extension
val codegen : unit -> option codegen_t
val parse_codegen : string -> option codegen_t
val codegen_libs : unit -> list (list string)
@@ -269,7 +270,3 @@ val eager_embedding: ref bool
val get_vconfig : unit -> vconfig
val set_vconfig : vconfig -> unit
-
-val all_ext_options : unit -> list (string & string)
-val ext_getv (k:string) : string
-val ext_getns (ns:string) : list (string & string)
diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fst b/src/smtencoding/FStar.SMTEncoding.Encode.fst
index c9d084b9e3e..e595f39a693 100644
--- a/src/smtencoding/FStar.SMTEncoding.Encode.fst
+++ b/src/smtencoding/FStar.SMTEncoding.Encode.fst
@@ -1040,7 +1040,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_getv "compat:injectivity" <> ""
+ || Options.Ext.get "compat:injectivity" <> ""
then (
let _, data_t = Env.lookup_datacon env.tcenv l in
let args, res = U.arrow_formals data_t in
@@ -1159,7 +1159,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_getv "compat:injectivity" <> ""
+ injective_type_params || Options.Ext.get "compat:injectivity" <> ""
in
let fields =
names |>
@@ -1322,11 +1322,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_getv "compat:2954" <> ""
+ else if Options.Ext.get "compat:2954" <> ""
then (warn_compat(); Some (bs, c)) //compatibility mode
else None
| _ ->
- if Options.ext_getv "compat:2954" <> ""
+ if Options.Ext.get "compat:2954" <> ""
then (warn_compat(); Some (bs, c)) //compatibility mode
else None
)
diff --git a/src/tactics/FStar.Tactics.V1.Basic.fst b/src/tactics/FStar.Tactics.V1.Basic.fst
index 147b424b439..32fb95710c3 100644
--- a/src/tactics/FStar.Tactics.V1.Basic.fst
+++ b/src/tactics/FStar.Tactics.V1.Basic.fst
@@ -1593,7 +1593,7 @@ let join () : tac unit =
let set_options (s : string) : tac unit = wrap_err "set_options" <| (
let! g = cur_goal in
FStar.Options.push ();
- FStar.Options.set (Util.smap_copy g.opts); // copy the map, they are not purely functional
+ FStar.Options.set g.opts;
let res = FStar.Options.set_options s in
let opts' = FStar.Options.peek () in
FStar.Options.pop ();
@@ -2248,7 +2248,7 @@ let get_vconfig () : tac vconfig =
* This is an artifact of the options API being stateful in many places,
* morally this is just (get_vconfig g.opts) *)
let vcfg = Options.with_saved_options (fun () ->
- FStar.Options.set (Util.smap_copy g.opts);
+ FStar.Options.set g.opts;
Options.get_vconfig ())
in
ret vcfg
@@ -2258,7 +2258,7 @@ let set_vconfig (vcfg : vconfig) : tac unit =
* let g' = { g with opts = set_vconfig vcfg g.opts } *)
let! g = cur_goal in
let opts' = Options.with_saved_options (fun () ->
- FStar.Options.set (Util.smap_copy g.opts);
+ FStar.Options.set g.opts;
Options.set_vconfig vcfg;
Options.peek ())
in
diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst
index 04266aac935..f824c487977 100644
--- a/src/tactics/FStar.Tactics.V2.Basic.fst
+++ b/src/tactics/FStar.Tactics.V2.Basic.fst
@@ -1621,7 +1621,7 @@ let join () : tac unit =
let set_options (s : string) : tac unit = wrap_err "set_options" <| (
let! g = cur_goal in
FStar.Options.push ();
- FStar.Options.set (Util.smap_copy g.opts); // copy the map, they are not purely functional
+ FStar.Options.set g.opts;
let res = FStar.Options.set_options s in
let opts' = FStar.Options.peek () in
FStar.Options.pop ();
@@ -2087,7 +2087,7 @@ let get_vconfig () : tac vconfig =
* This is an artifact of the options API being stateful in many places,
* morally this is just (get_vconfig g.opts) *)
let vcfg = Options.with_saved_options (fun () ->
- FStar.Options.set (Util.smap_copy g.opts);
+ FStar.Options.set g.opts;
Options.get_vconfig ())
in
return vcfg
@@ -2097,7 +2097,7 @@ let set_vconfig (vcfg : vconfig) : tac unit =
* let g' = { g with opts = set_vconfig vcfg g.opts } *)
let! g = cur_goal in
let opts' = Options.with_saved_options (fun () ->
- FStar.Options.set (Util.smap_copy g.opts);
+ FStar.Options.set g.opts;
Options.set_vconfig vcfg;
Options.peek ())
in
@@ -2140,15 +2140,15 @@ let free_uvars (tm : term) : tac (list Z.t)
let all_ext_options () : tac (list (string & string))
= return () ;!
- return (Options.all_ext_options ())
+ return (Options.Ext.all ())
let ext_getv (k:string) : tac string
= return () ;!
- return (Options.ext_getv k)
+ return (Options.Ext.get k)
let ext_getns (ns:string) : tac (list (string & string))
= return () ;!
- return (Options.ext_getns ns)
+ return (Options.Ext.getns ns)
let alloc (x:'a) : tac (tref 'a) =
return ();!
diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index 49c254bc837..d60ca8bc28e 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -4371,12 +4371,15 @@ let desugar_modul env (m:AST.modul) : env_t & Syntax.modul =
//External API for modules
/////////////////////////////////////////////////////////////////////////////////////////
let with_options (f:unit -> 'a) : 'a =
- FStar.Options.push();
- let res = f () in
- let light = FStar.Options.ml_ish() in
- FStar.Options.pop();
- if light then FStar.Options.set_ml_ish();
- res
+ let light, r =
+ Options.with_saved_options (fun () ->
+ let r = f () in
+ let light = Options.ml_ish () in
+ light, r
+ )
+ in
+ if light then Options.set_ml_ish ();
+ r
let ast_modul_to_modul modul : withenv S.modul =
fun env ->
diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst
index d5dcda9da53..d8d894f5b71 100644
--- a/src/typechecker/FStar.TypeChecker.Cfg.fst
+++ b/src/typechecker/FStar.TypeChecker.Cfg.fst
@@ -414,7 +414,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_getv "compat:normalizer_memo_ignore_cfg" <> "";
+ compat_memo_ignore_cfg = Options.Ext.get "compat:normalizer_memo_ignore_cfg" <> "";
}
let config s e = config' [] s e
diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst
index d96a5ec613c..3c18a8cf769 100644
--- a/src/typechecker/FStar.TypeChecker.Rel.fst
+++ b/src/typechecker/FStar.TypeChecker.Rel.fst
@@ -5621,7 +5621,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_getv "compat:open_metas" = "" then ( // i.e. compat option unset
+ && Options.Ext.get "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
From 9154b67ece984cd63a2babee8b6366f55e0a3d3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 27 Aug 2024 20:11:56 -0700
Subject: [PATCH 2/3] snap
---
.../generated/FStar_Compiler_Range_Ops.ml | 2 +-
ocaml/fstar-lib/generated/FStar_Options.ml | 1066 ++++++++---------
.../fstar-lib/generated/FStar_Options_Ext.ml | 67 ++
.../generated/FStar_SMTEncoding_Encode.ml | 12 +-
.../generated/FStar_Tactics_V1_Basic.ml | 14 +-
.../generated/FStar_Tactics_V2_Basic.ml | 20 +-
.../generated/FStar_ToSyntax_ToSyntax.ml | 12 +-
.../generated/FStar_TypeChecker_Cfg.ml | 2 +-
.../generated/FStar_TypeChecker_Rel.ml | 2 +-
9 files changed, 596 insertions(+), 601 deletions(-)
create mode 100644 ocaml/fstar-lib/generated/FStar_Options_Ext.ml
diff --git a/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml b/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml
index 16520664139..0e039abf53c 100644
--- a/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml
+++ b/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml
@@ -73,7 +73,7 @@ let (string_of_file_name : Prims.string -> Prims.string) =
if uu___
then
let uu___1 =
- let uu___2 = FStar_Options.ext_getv "fstar:no_absolute_paths" in
+ let uu___2 = FStar_Options_Ext.get "fstar:no_absolute_paths" in
uu___2 = "1" in
(if uu___1
then FStar_Compiler_Util.basename f
diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml
index a2974af12cb..e9db0b76695 100644
--- a/ocaml/fstar-lib/generated/FStar_Options.ml
+++ b/ocaml/fstar-lib/generated/FStar_Options.ml
@@ -1,4 +1,20 @@
open Prims
+type codegen_t =
+ | OCaml
+ | FSharp
+ | Krml
+ | Plugin
+ | Extension
+let (uu___is_OCaml : codegen_t -> Prims.bool) =
+ fun projectee -> match projectee with | OCaml -> true | uu___ -> false
+let (uu___is_FSharp : codegen_t -> Prims.bool) =
+ fun projectee -> match projectee with | FSharp -> true | uu___ -> false
+let (uu___is_Krml : codegen_t -> Prims.bool) =
+ fun projectee -> match projectee with | Krml -> true | uu___ -> false
+let (uu___is_Plugin : codegen_t -> Prims.bool) =
+ fun projectee -> match projectee with | Plugin -> true | uu___ -> false
+let (uu___is_Extension : codegen_t -> Prims.bool) =
+ fun projectee -> match projectee with | Extension -> true | uu___ -> false
type split_queries_t =
| No
| OnFailure
@@ -38,7 +54,7 @@ let (__proj__List__item___0 : option_val -> option_val Prims.list) =
fun projectee -> match projectee with | List _0 -> _0
let (uu___is_Unset : option_val -> Prims.bool) =
fun projectee -> match projectee with | Unset -> true | uu___ -> false
-type optionstate = option_val FStar_Compiler_Util.smap
+type optionstate = option_val FStar_Compiler_Util.psmap
type opt_type =
| Const of option_val
| IntStr of Prims.string
@@ -164,110 +180,83 @@ let (as_comma_string_list : option_val -> Prims.string Prims.list) =
let copy_optionstate :
'uuuuu . 'uuuuu FStar_Compiler_Util.smap -> 'uuuuu FStar_Compiler_Util.smap
= fun m -> FStar_Compiler_Util.smap_copy m
-let (fstar_options :
- (FStar_Compiler_Debug.saved_state * optionstate) Prims.list Prims.list
- FStar_Compiler_Effect.ref)
- = FStar_Compiler_Util.mk_ref []
-let (internal_peek : unit -> optionstate) =
- fun uu___ ->
- let uu___1 =
- let uu___2 =
- let uu___3 = FStar_Compiler_Effect.op_Bang fstar_options in
- FStar_Compiler_List.hd uu___3 in
- FStar_Compiler_List.hd uu___2 in
- FStar_Pervasives_Native.snd uu___1
+type history1 =
+ (FStar_Compiler_Debug.saved_state * FStar_Options_Ext.ext_state *
+ optionstate)
+let (fstar_options : optionstate FStar_Compiler_Effect.ref) =
+ let uu___ = FStar_Compiler_Util.psmap_empty () in
+ FStar_Compiler_Util.mk_ref uu___
+let (history : history1 Prims.list Prims.list FStar_Compiler_Effect.ref) =
+ FStar_Compiler_Util.mk_ref []
let (peek : unit -> optionstate) =
- fun uu___ -> let uu___1 = internal_peek () in copy_optionstate uu___1
-let (pop : unit -> unit) =
+ fun uu___ -> FStar_Compiler_Effect.op_Bang fstar_options
+let (internal_push : unit -> unit) =
fun uu___ ->
- let uu___1 = FStar_Compiler_Effect.op_Bang fstar_options in
+ let uu___1 = FStar_Compiler_Effect.op_Bang history in
match uu___1 with
- | [] -> FStar_Compiler_Effect.failwith "TOO MANY POPS!"
- | uu___2::[] -> FStar_Compiler_Effect.failwith "TOO MANY POPS!"
- | uu___2::tl -> FStar_Compiler_Effect.op_Colon_Equals fstar_options tl
+ | lev1::rest ->
+ let newhd =
+ let uu___2 = FStar_Compiler_Debug.snapshot () in
+ let uu___3 = FStar_Options_Ext.save () in
+ let uu___4 = FStar_Compiler_Effect.op_Bang fstar_options in
+ (uu___2, uu___3, uu___4) in
+ FStar_Compiler_Effect.op_Colon_Equals history ((newhd :: lev1) ::
+ rest)
+let (internal_pop : unit -> Prims.bool) =
+ fun uu___ ->
+ let uu___1 = FStar_Compiler_Effect.op_Bang history in
+ match uu___1 with
+ | lev1::rest ->
+ (match lev1 with
+ | [] -> false
+ | (dbg, ext, opts)::lev1' ->
+ (FStar_Compiler_Debug.restore dbg;
+ FStar_Options_Ext.restore ext;
+ FStar_Compiler_Effect.op_Colon_Equals fstar_options opts;
+ FStar_Compiler_Effect.op_Colon_Equals history (lev1' :: rest);
+ true))
let (push : unit -> unit) =
fun uu___ ->
- let new_st =
- let uu___1 =
- let uu___2 = FStar_Compiler_Effect.op_Bang fstar_options in
- FStar_Compiler_List.hd uu___2 in
- FStar_Compiler_List.map
- (fun uu___2 ->
- match uu___2 with
- | (dbg, opts) ->
- let uu___3 = copy_optionstate opts in (dbg, uu___3)) uu___1 in
- let uu___1 =
- let uu___2 = FStar_Compiler_Effect.op_Bang fstar_options in new_st ::
- uu___2 in
- FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___1
-let (internal_pop : unit -> Prims.bool) =
+ internal_push ();
+ (let uu___2 = FStar_Compiler_Effect.op_Bang history in
+ match uu___2 with
+ | lev1::uu___3 ->
+ ((let uu___5 =
+ let uu___6 = FStar_Compiler_Effect.op_Bang history in lev1 ::
+ uu___6 in
+ FStar_Compiler_Effect.op_Colon_Equals history uu___5);
+ (let uu___6 = internal_pop () in ())))
+let (pop : unit -> unit) =
fun uu___ ->
- let curstack =
- let uu___1 = FStar_Compiler_Effect.op_Bang fstar_options in
- FStar_Compiler_List.hd uu___1 in
- match curstack with
- | [] ->
- FStar_Compiler_Effect.failwith
- "impossible: empty current option stack"
- | uu___1::[] -> false
- | uu___1::tl ->
- ((let uu___3 =
- let uu___4 =
- let uu___5 = FStar_Compiler_Effect.op_Bang fstar_options in
- FStar_Compiler_List.tl uu___5 in
- tl :: uu___4 in
- FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___3);
+ let uu___1 = FStar_Compiler_Effect.op_Bang history in
+ match uu___1 with
+ | [] -> FStar_Compiler_Effect.failwith "TOO MANY POPS!"
+ | uu___2::levs ->
+ (FStar_Compiler_Effect.op_Colon_Equals history levs;
(let uu___4 =
- let uu___5 = FStar_Compiler_List.hd tl in
- FStar_Pervasives_Native.fst uu___5 in
- FStar_Compiler_Debug.restore uu___4);
- true)
-let (internal_push : unit -> unit) =
- fun uu___ ->
- let curstack =
- let uu___1 = FStar_Compiler_Effect.op_Bang fstar_options in
- FStar_Compiler_List.hd uu___1 in
- let stack' =
- let uu___1 =
- let uu___2 = FStar_Compiler_Debug.snapshot () in
- let uu___3 =
- let uu___4 =
- let uu___5 = FStar_Compiler_List.hd curstack in
- FStar_Pervasives_Native.snd uu___5 in
- copy_optionstate uu___4 in
- (uu___2, uu___3) in
- uu___1 :: curstack in
- let uu___1 =
- let uu___2 =
- let uu___3 = FStar_Compiler_Effect.op_Bang fstar_options in
- FStar_Compiler_List.tl uu___3 in
- stack' :: uu___2 in
- FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___1
+ let uu___5 = internal_pop () in Prims.op_Negation uu___5 in
+ if uu___4 then FStar_Compiler_Effect.failwith "aaa!!!" else ()))
let (set : optionstate -> unit) =
- fun o ->
- let uu___ = FStar_Compiler_Effect.op_Bang fstar_options in
- match uu___ with
- | [] -> FStar_Compiler_Effect.failwith "set on empty option stack"
- | []::uu___1 ->
- FStar_Compiler_Effect.failwith "set on empty current option stack"
- | ((dbg, uu___1)::tl)::os ->
- FStar_Compiler_Effect.op_Colon_Equals fstar_options (((dbg, o) :: tl)
- :: os)
+ fun o -> FStar_Compiler_Effect.op_Colon_Equals fstar_options o
let (snapshot : unit -> (Prims.int * unit)) =
- fun uu___ -> FStar_Common.snapshot push fstar_options ()
+ fun uu___ -> FStar_Common.snapshot push history ()
let (rollback : Prims.int FStar_Pervasives_Native.option -> unit) =
- fun depth -> FStar_Common.rollback pop fstar_options depth
+ fun depth -> FStar_Common.rollback pop history depth
let (set_option : Prims.string -> option_val -> unit) =
fun k ->
fun v ->
- let map = internal_peek () in
+ let map = peek () in
if k = "report_assumes"
then
- let uu___ = FStar_Compiler_Util.smap_try_find map k in
+ let uu___ = FStar_Compiler_Util.psmap_try_find map k in
match uu___ with
| FStar_Pervasives_Native.Some (String "error") -> ()
- | uu___1 -> FStar_Compiler_Util.smap_add map k v
- else FStar_Compiler_Util.smap_add map k v
+ | uu___1 ->
+ let uu___2 = FStar_Compiler_Util.psmap_add map k v in
+ FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___2
+ else
+ (let uu___1 = FStar_Compiler_Util.psmap_add map k v in
+ FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___1)
let (set_option' : (Prims.string * option_val) -> unit) =
fun uu___ -> match uu___ with | (k, v) -> set_option k v
let (set_admit_smt_queries : Prims.bool -> unit) =
@@ -298,7 +287,7 @@ let (defaults : (Prims.string * option_val) Prims.list) =
("eager_subtyping", (Bool false));
("error_contexts", (Bool false));
("expose_interfaces", (Bool false));
- ("ext", (List []));
+ ("ext", Unset);
("extract", Unset);
("extract_all", (Bool false));
("extract_module", (List []));
@@ -410,26 +399,18 @@ let (defaults : (Prims.string * option_val) Prims.list) =
("profile", Unset)]
let (init : unit -> unit) =
fun uu___ ->
- let o = internal_peek () in
- FStar_Compiler_Util.smap_clear o;
+ FStar_Compiler_Debug.disable_all ();
+ FStar_Options_Ext.reset ();
+ (let uu___4 = FStar_Compiler_Util.psmap_empty () in
+ FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___4);
FStar_Compiler_List.iter set_option' defaults
let (clear : unit -> unit) =
- fun uu___ ->
- let o = FStar_Compiler_Util.smap_create (Prims.of_int (50)) in
- (let uu___2 =
- let uu___3 =
- let uu___4 =
- let uu___5 = FStar_Compiler_Debug.snapshot () in (uu___5, o) in
- [uu___4] in
- [uu___3] in
- FStar_Compiler_Effect.op_Colon_Equals fstar_options uu___2);
- init ()
-let (_run : unit) = clear ()
+ fun uu___ -> FStar_Compiler_Effect.op_Colon_Equals history [[]]; init ()
+let (uu___154 : unit) = clear ()
let (get_option : Prims.string -> option_val) =
fun s ->
let uu___ =
- let uu___1 = internal_peek () in
- FStar_Compiler_Util.smap_try_find uu___1 s in
+ let uu___1 = peek () in FStar_Compiler_Util.psmap_try_find uu___1 s in
match uu___ with
| FStar_Pervasives_Native.None ->
let uu___1 =
@@ -468,7 +449,7 @@ let (set_verification_options : optionstate -> unit) =
FStar_Compiler_List.iter
(fun k ->
let uu___ =
- let uu___1 = FStar_Compiler_Util.smap_try_find o k in
+ let uu___1 = FStar_Compiler_Util.psmap_try_find o k in
FStar_Compiler_Util.must uu___1 in
set_option k uu___) verifopts
let lookup_opt : 'uuuuu . Prims.string -> (option_val -> 'uuuuu) -> 'uuuuu =
@@ -517,9 +498,6 @@ let (get_error_contexts : unit -> Prims.bool) =
fun uu___ -> lookup_opt "error_contexts" as_bool
let (get_expose_interfaces : unit -> Prims.bool) =
fun uu___ -> lookup_opt "expose_interfaces" as_bool
-let (get_ext :
- unit -> Prims.string Prims.list FStar_Pervasives_Native.option) =
- fun uu___ -> lookup_opt "ext" (as_option (as_list as_string))
let (get_extract :
unit -> Prims.string Prims.list FStar_Pervasives_Native.option) =
fun uu___ -> lookup_opt "extract" (as_option (as_list as_string))
@@ -1019,7 +997,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___454 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit)))
+let (uu___451 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit)))
=
let cb = FStar_Compiler_Util.mk_ref FStar_Pervasives_Native.None in
let set1 f =
@@ -1031,11 +1009,11 @@ let (uu___454 : (((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___454 with
+ match uu___451 with
| (set_option_warning_callback_aux1, option_warning_callback) ->
set_option_warning_callback_aux1
let (option_warning_callback : Prims.string -> unit) =
- match uu___454 with
+ match uu___451 with
| (set_option_warning_callback_aux1, option_warning_callback1) ->
option_warning_callback1
let (set_option_warning_callback : (Prims.string -> unit) -> unit) =
@@ -1328,9 +1306,52 @@ let rec (specs_with_types :
"These options are set in extensions option map. Keys are usually namespaces separated by \":\". E.g., 'pulse:verbose=1;my:extension:option=xyz;foo:bar=baz'. These options are typically interpreted by extensions. Any later use of --ext over the same key overrides the old value. An entry 'e' that is not of the form 'a=b' is treated as 'e=1', i.e., 'e' associated with string \"1\"." in
(FStar_Getopt.noshort,
"ext",
- (ReverseAccumulated
- (SimpleStr
- "One or more semicolon separated occurrences of key-value pairs")),
+ (PostProcessed
+ ((fun o ->
+ let parse_ext
+ s =
+ let exts =
+ FStar_Compiler_Util.split
+ s ";" in
+ FStar_Compiler_List.collect
+ (fun s1 ->
+ match
+ FStar_Compiler_Util.split
+ s1 "="
+ with
+ |
+ k::v::[]
+ ->
+ [(k, v)]
+ |
+ uu___50
+ ->
+ [
+ (s1, "1")])
+ exts in
+ (let uu___51 =
+ let uu___52
+ =
+ as_comma_string_list
+ o in
+ FStar_Compiler_List.collect
+ parse_ext
+ uu___52 in
+ FStar_Compiler_List.iter
+ (fun
+ uu___52
+ ->
+ match uu___52
+ with
+ |
+ (k, v) ->
+ FStar_Options_Ext.set
+ k v)
+ uu___51);
+ o),
+ (ReverseAccumulated
+ (SimpleStr
+ "extension knobs")))),
uu___49) in
let uu___49 =
let uu___50 =
@@ -2132,38 +2153,38 @@ let rec (specs_with_types :
=
let uu___153
=
- let uu___154
+ let uu___155
=
text
"--quake N/M repeats each query checks that it succeeds at least N out of M times, aborting early if possible" in
- let uu___155
- =
let uu___156
=
- text
- "--quake N/M/k works as above, except it will unconditionally run M times" in
let uu___157
=
+ text
+ "--quake N/M/k works as above, except it will unconditionally run M times" in
let uu___158
=
- text
- "--quake N is an alias for --quake N/N" in
let uu___159
=
+ text
+ "--quake N is an alias for --quake N/N" in
let uu___160
=
+ let uu___161
+ =
text
"--quake N/k is an alias for --quake N/N/k" in
- [uu___160] in
- uu___158
+ [uu___161] in
+ uu___159
::
- uu___159 in
- uu___156
+ uu___160 in
+ uu___157
::
- uu___157 in
- uu___154
+ uu___158 in
+ uu___155
::
- uu___155 in
+ uu___156 in
FStar_Errors_Msg.bulleted
uu___153 in
let uu___153
@@ -2249,36 +2270,36 @@ let rec (specs_with_types :
uu___153) in
let uu___153
=
- let uu___154
- =
let uu___155
=
+ let uu___156
+ =
text
"Read a checked file and dump it to standard output." in
(FStar_Getopt.noshort,
"read_checked_file",
(PathStr
"path"),
- uu___155) in
- let uu___155
- =
+ uu___156) in
let uu___156
=
let uu___157
=
+ let uu___158
+ =
text
"Read a Karamel binary file and dump it to standard output." in
(FStar_Getopt.noshort,
"read_krml_file",
(PathStr
"path"),
- uu___157) in
- let uu___157
- =
+ uu___158) in
let uu___158
=
let uu___159
=
+ let uu___160
+ =
text
"Record a database of hints for efficient proof replay" in
(FStar_Getopt.noshort,
@@ -2286,13 +2307,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___159) in
- let uu___159
- =
+ uu___160) in
let uu___160
=
let uu___161
=
+ let uu___162
+ =
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,
@@ -2300,22 +2321,22 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___161) in
- let uu___161
- =
+ uu___162) in
let uu___162
=
let uu___163
=
+ let uu___164
+ =
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___164
+ uu___165
->
- match uu___164
+ match uu___165
with
|
Int i ->
@@ -2336,32 +2357,32 @@ let rec (specs_with_types :
true);
Bool true)
|
- uu___165
+ uu___166
->
FStar_Compiler_Effect.failwith
"impos"),
(IntStr
"positive integer"))),
- uu___163) in
- let uu___163
- =
+ uu___164) in
let uu___164
=
let uu___165
=
+ let uu___166
+ =
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
(FStar_Getopt.noshort,
"reuse_hint_for",
(SimpleStr
"toplevel_name"),
- uu___165) in
- let uu___165
- =
+ uu___166) in
let uu___166
=
let uu___167
=
+ let uu___168
+ =
text
"Report every use of an escape hatch, include assume, admit, etc." in
(FStar_Getopt.noshort,
@@ -2369,13 +2390,13 @@ let rec (specs_with_types :
(EnumStr
["warn";
"error"]),
- uu___167) in
- let uu___167
- =
+ uu___168) in
let uu___168
=
let uu___169
=
+ let uu___170
+ =
text
"Disable all non-critical output" in
(FStar_Getopt.noshort,
@@ -2383,217 +2404,217 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___169) in
- let uu___169
- =
+ uu___170) in
let uu___170
=
let uu___171
=
+ let uu___172
+ =
text
"Path to the Z3 SMT solver (we could eventually support other solvers)" in
(FStar_Getopt.noshort,
"smt",
(PathStr
"path"),
- uu___171) in
- let uu___171
- =
+ uu___172) in
let uu___172
=
let uu___173
=
+ let uu___174
+ =
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___173) in
- let uu___173
- =
+ uu___174) in
let uu___174
=
let uu___175
=
let uu___176
=
- text
- "Control the representation of non-linear arithmetic functions in the SMT encoding:" in
let uu___177
=
+ text
+ "Control the representation of non-linear arithmetic functions in the SMT encoding:" in
let uu___178
=
let uu___179
=
let uu___180
=
- text
- "if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'" in
let uu___181
=
+ text
+ "if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'" in
let uu___182
=
- text
- "if 'native' use '*, div, mod'" in
let uu___183
=
+ text
+ "if 'native' use '*, div, mod'" in
let uu___184
=
+ let uu___185
+ =
text
"if 'wrapped' use '_mul, _div, _mod : Int*Int -> Int'" in
- [uu___184] in
- uu___182
+ [uu___185] in
+ uu___183
::
- uu___183 in
- uu___180
+ uu___184 in
+ uu___181
::
- uu___181 in
+ uu___182 in
FStar_Errors_Msg.bulleted
- uu___179 in
- let uu___179
+ uu___180 in
+ let uu___180
=
text
"(default 'boxwrap')" in
FStar_Pprint.op_Hat_Hat
- uu___178
- uu___179 in
+ uu___179
+ uu___180 in
FStar_Pprint.op_Hat_Hat
- uu___176
- uu___177 in
+ uu___177
+ uu___178 in
(FStar_Getopt.noshort,
"smtencoding.nl_arith_repr",
(EnumStr
["native";
"wrapped";
"boxwrap"]),
- uu___175) in
- let uu___175
- =
+ uu___176) in
let uu___176
=
let uu___177
=
let uu___178
=
- text
- "Toggle the representation of linear arithmetic functions in the SMT encoding:" in
let uu___179
=
+ text
+ "Toggle the representation of linear arithmetic functions in the SMT encoding:" in
let uu___180
=
let uu___181
=
let uu___182
=
- text
- "if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'" in
let uu___183
=
+ text
+ "if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'" in
let uu___184
=
+ let uu___185
+ =
text
"if 'native', use '+, -, -'" in
- [uu___184] in
- uu___182
+ [uu___185] in
+ uu___183
::
- uu___183 in
+ uu___184 in
FStar_Errors_Msg.bulleted
- uu___181 in
- let uu___181
+ uu___182 in
+ let uu___182
=
text
"(default 'boxwrap')" in
FStar_Pprint.op_Hat_Hat
- uu___180
- uu___181 in
+ uu___181
+ uu___182 in
FStar_Pprint.op_Hat_Hat
- uu___178
- uu___179 in
+ uu___179
+ uu___180 in
(FStar_Getopt.noshort,
"smtencoding.l_arith_repr",
(EnumStr
["native";
"boxwrap"]),
- uu___177) in
- let uu___177
- =
+ uu___178) in
let uu___178
=
let uu___179
=
+ let uu___180
+ =
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___179) in
- let uu___179
- =
+ uu___180) in
let uu___180
=
let uu___181
=
+ let uu___182
+ =
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___181) in
- let uu___181
- =
+ uu___182) in
let uu___182
=
let uu___183
=
let uu___184
=
- text
- "Split SMT verification conditions into several separate queries, one per goal. Helps with localizing errors." in
let uu___185
=
+ text
+ "Split SMT verification conditions into several separate queries, one per goal. Helps with localizing errors." in
let uu___186
=
let uu___187
=
- text
- "Use 'no' to disable (this may reduce the quality of error messages)." in
let uu___188
=
+ text
+ "Use 'no' to disable (this may reduce the quality of error messages)." in
let uu___189
=
- text
- "Use 'on_failure' to split queries and retry when discharging fails (the default)" in
let uu___190
=
+ text
+ "Use 'on_failure' to split queries and retry when discharging fails (the default)" in
let uu___191
=
+ let uu___192
+ =
text
"Use 'yes' to always split." in
- [uu___191] in
- uu___189
+ [uu___192] in
+ uu___190
::
- uu___190 in
- uu___187
+ uu___191 in
+ uu___188
::
- uu___188 in
+ uu___189 in
FStar_Errors_Msg.bulleted
- uu___186 in
+ uu___187 in
FStar_Pprint.op_Hat_Hat
- uu___184
- uu___185 in
+ uu___185
+ uu___186 in
(FStar_Getopt.noshort,
"split_queries",
(EnumStr
["no";
"on_failure";
"always"]),
- uu___183) in
- let uu___183
- =
+ uu___184) in
let uu___184
=
let uu___185
=
+ let uu___186
+ =
text
"Do not use the lexical scope of tactics to improve binder names" in
(FStar_Getopt.noshort,
@@ -2601,13 +2622,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___185) in
- let uu___185
- =
+ uu___186) in
let uu___186
=
let uu___187
=
+ let uu___188
+ =
text
"Do not recover from metaprogramming errors, and abort if one occurs" in
(FStar_Getopt.noshort,
@@ -2615,13 +2636,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___187) in
- let uu___187
- =
+ uu___188) in
let uu___188
=
let uu___189
=
+ let uu___190
+ =
text
"Print some rough information on tactics, such as the time they take to run" in
(FStar_Getopt.noshort,
@@ -2629,13 +2650,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___189) in
- let uu___189
- =
+ uu___190) in
let uu___190
=
let uu___191
=
+ let uu___192
+ =
text
"Print a depth-indexed trace of tactic execution (Warning: very verbose)" in
(FStar_Getopt.noshort,
@@ -2643,26 +2664,26 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___191) in
- let uu___191
- =
+ uu___192) in
let uu___192
=
let uu___193
=
+ let uu___194
+ =
text
"Trace tactics up to a certain binding depth" in
(FStar_Getopt.noshort,
"tactic_trace_d",
(IntStr
"positive_integer"),
- uu___193) in
- let uu___193
- =
+ uu___194) in
let uu___194
=
let uu___195
=
+ let uu___196
+ =
text
"Use NBE to evaluate metaprograms (experimental)" in
(FStar_Getopt.noshort,
@@ -2670,25 +2691,25 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___195) in
- let uu___195
- =
+ uu___196) in
let uu___196
=
let uu___197
=
+ let uu___198
+ =
text
"Attempt to normalize definitions marked as tcnorm (default 'true')" in
(FStar_Getopt.noshort,
"tcnorm",
BoolStr,
- uu___197) in
- let uu___197
- =
+ uu___198) in
let uu___198
=
let uu___199
=
+ let uu___200
+ =
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
(FStar_Getopt.noshort,
@@ -2696,13 +2717,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___199) in
- let uu___199
- =
+ uu___200) in
let uu___200
=
let uu___201
=
+ let uu___202
+ =
text
"Attach stack traces on errors" in
(FStar_Getopt.noshort,
@@ -2710,13 +2731,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___201) in
- let uu___201
- =
+ uu___202) in
let uu___202
=
let uu___203
=
+ let uu___204
+ =
text
"Emit output formatted for debugging" in
(FStar_Getopt.noshort,
@@ -2724,13 +2745,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___203) in
- let uu___203
- =
+ uu___204) in
let uu___204
=
let uu___205
=
+ let uu___206
+ =
text
"Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)" in
(FStar_Getopt.noshort,
@@ -2738,13 +2759,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___205) in
- let uu___205
- =
+ uu___206) in
let uu___206
=
let uu___207
=
+ let uu___208
+ =
text
"Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects." in
(FStar_Getopt.noshort,
@@ -2752,13 +2773,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___207) in
- let uu___207
- =
+ uu___208) in
let uu___208
=
let uu___209
=
+ let uu___210
+ =
text
"Use equality constraints when comparing higher-order types (Temporary)" in
(FStar_Getopt.noshort,
@@ -2766,13 +2787,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___209) in
- let uu___209
- =
+ uu___210) in
let uu___210
=
let uu___211
=
+ let uu___212
+ =
text
"Use a previously recorded hints database for proof replay" in
(FStar_Getopt.noshort,
@@ -2780,13 +2801,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___211) in
- let uu___211
- =
+ uu___212) in
let uu___212
=
let uu___213
=
+ let uu___214
+ =
text
"Admit queries if their hash matches the hash recorded in the hints database" in
(FStar_Getopt.noshort,
@@ -2794,26 +2815,26 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___213) in
- let uu___213
- =
+ uu___214) in
let uu___214
=
let uu___215
=
+ let uu___216
+ =
text
"Use compiled tactics from path" in
(FStar_Getopt.noshort,
"use_native_tactics",
(PathStr
"path"),
- uu___215) in
- let uu___215
- =
+ uu___216) in
let uu___216
=
let uu___217
=
+ let uu___218
+ =
text
"Do not run plugins natively and interpret them as usual instead" in
(FStar_Getopt.noshort,
@@ -2821,13 +2842,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___217) in
- let uu___217
- =
+ uu___218) in
let uu___218
=
let uu___219
=
+ let uu___220
+ =
text
"Do not run the tactic engine before discharging a VC" in
(FStar_Getopt.noshort,
@@ -2835,13 +2856,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___219) in
- let uu___219
- =
+ uu___220) in
let uu___220
=
let uu___221
=
+ let uu___222
+ =
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,
@@ -2849,13 +2870,13 @@ let rec (specs_with_types :
(ReverseAccumulated
(SimpleStr
"One or more space-separated occurrences of '[+|-]( * | namespace | fact id)'")),
- uu___221) in
- let uu___221
- =
+ uu___222) in
let uu___222
=
let uu___223
=
+ let uu___224
+ =
text
"This does nothing and will be removed" in
(FStar_Getopt.noshort,
@@ -2863,20 +2884,20 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___223) in
- let uu___223
- =
+ uu___224) in
let uu___224
=
let uu___225
=
+ let uu___226
+ =
text
"Display version number" in
(118,
"version",
(WithSideEffect
((fun
- uu___226
+ uu___227
->
display_version
();
@@ -2885,13 +2906,13 @@ let rec (specs_with_types :
(Const
(Bool
true)))),
- uu___225) in
- let uu___225
- =
+ uu___226) in
let uu___226
=
let uu___227
=
+ let uu___228
+ =
text
"Warn when (a -> b) is desugared to (a -> Tot b)" in
(FStar_Getopt.noshort,
@@ -2899,13 +2920,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___227) in
- let uu___227
- =
+ uu___228) in
let uu___228
=
let uu___229
=
+ let uu___230
+ =
text
"Z3 command line options" in
(FStar_Getopt.noshort,
@@ -2913,13 +2934,13 @@ let rec (specs_with_types :
(ReverseAccumulated
(SimpleStr
"option")),
- uu___229) in
- let uu___229
- =
+ uu___230) in
let uu___230
=
let uu___231
=
+ let uu___232
+ =
text
"Z3 options in smt2 format" in
(FStar_Getopt.noshort,
@@ -2927,13 +2948,13 @@ let rec (specs_with_types :
(ReverseAccumulated
(SimpleStr
"option")),
- uu___231) in
- let uu___231
- =
+ uu___232) in
let uu___232
=
let uu___233
=
+ let uu___234
+ =
text
"Restart Z3 after each query; useful for ensuring proof robustness" in
(FStar_Getopt.noshort,
@@ -2941,72 +2962,72 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___233) in
- let uu___233
- =
+ uu___234) in
let uu___234
=
let uu___235
=
+ let uu___236
+ =
text
"Set the Z3 per-query resource limit (default 5 units, taking roughtly 5s)" in
(FStar_Getopt.noshort,
"z3rlimit",
(IntStr
"positive_integer"),
- uu___235) in
- let uu___235
- =
+ uu___236) in
let uu___236
=
let uu___237
=
+ let uu___238
+ =
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
(FStar_Getopt.noshort,
"z3rlimit_factor",
(IntStr
"positive_integer"),
- uu___237) in
- let uu___237
- =
+ uu___238) in
let uu___238
=
let uu___239
=
+ let uu___240
+ =
text
"Set the Z3 random seed (default 0)" in
(FStar_Getopt.noshort,
"z3seed",
(IntStr
"positive_integer"),
- uu___239) in
- let uu___239
- =
+ uu___240) in
let uu___240
=
let uu___241
=
+ let uu___242
+ =
text
"Set the version of Z3 that is to be used. Default: 4.8.5" in
(FStar_Getopt.noshort,
"z3version",
(SimpleStr
"version"),
- uu___241) in
- let uu___241
- =
+ uu___242) in
let uu___242
=
let uu___243
=
+ let uu___244
+ =
text
"Don't check positivity of inductive types" in
(FStar_Getopt.noshort,
"__no_positivity",
(WithSideEffect
((fun
- uu___244
+ uu___245
->
if
warn_unsafe
@@ -3017,113 +3038,113 @@ let rec (specs_with_types :
(Const
(Bool
true)))),
- uu___243) in
- let uu___243
- =
+ uu___244) in
let uu___244
=
let uu___245
=
let uu___246
=
- text
- "The [-warn_error] option follows the OCaml syntax, namely:" in
let uu___247
=
+ text
+ "The [-warn_error] option follows the OCaml syntax, namely:" in
let uu___248
=
let uu___249
=
- text
- "[r] is a range of warnings (either a number [n], or a range [n..n])" in
let uu___250
=
+ text
+ "[r] is a range of warnings (either a number [n], or a range [n..n])" in
let uu___251
=
- text
- "[-r] silences range [r]" in
let uu___252
=
+ text
+ "[-r] silences range [r]" in
let uu___253
=
- text
- "[+r] enables range [r] as warnings (NOTE: \"enabling\" an error will downgrade it to a warning)" in
let uu___254
=
+ text
+ "[+r] enables range [r] as warnings (NOTE: \"enabling\" an error will downgrade it to a warning)" in
let uu___255
=
+ let uu___256
+ =
text
"[@r] makes range [r] fatal." in
- [uu___255] in
- uu___253
+ [uu___256] in
+ uu___254
::
- uu___254 in
- uu___251
+ uu___255 in
+ uu___252
::
- uu___252 in
- uu___249
+ uu___253 in
+ uu___250
::
- uu___250 in
+ uu___251 in
FStar_Errors_Msg.bulleted
- uu___248 in
+ uu___249 in
FStar_Pprint.op_Hat_Hat
- uu___246
- uu___247 in
+ uu___247
+ uu___248 in
(FStar_Getopt.noshort,
"warn_error",
(ReverseAccumulated
(SimpleStr
"")),
- uu___245) in
- let uu___245
- =
+ uu___246) in
let uu___246
=
let uu___247
=
+ let uu___248
+ =
text
"Use normalization by evaluation as the default normalization strategy (default 'false')" in
(FStar_Getopt.noshort,
"use_nbe",
BoolStr,
- uu___247) in
- let uu___247
- =
+ uu___248) in
let uu___248
=
let uu___249
=
+ let uu___250
+ =
text
"Use normalization by evaluation for normalizing terms before extraction (default 'false')" in
(FStar_Getopt.noshort,
"use_nbe_for_extraction",
BoolStr,
- uu___249) in
- let uu___249
- =
+ uu___250) in
let uu___250
=
let uu___251
=
+ let uu___252
+ =
text
"Enforce trivial preconditions for unannotated effectful functions (default 'true')" in
(FStar_Getopt.noshort,
"trivial_pre_for_unannotated_effectful_fns",
BoolStr,
- uu___251) in
- let uu___251
- =
+ uu___252) in
let uu___252
=
let uu___253
=
+ let uu___254
+ =
text
"Debug messages for embeddings/unembeddings of natively compiled terms" in
(FStar_Getopt.noshort,
"__debug_embedding",
(WithSideEffect
((fun
- uu___254
+ uu___255
->
FStar_Compiler_Effect.op_Colon_Equals
debug_embedding
@@ -3131,20 +3152,20 @@ let rec (specs_with_types :
(Const
(Bool
true)))),
- uu___253) in
- let uu___253
- =
+ uu___254) in
let uu___254
=
let uu___255
=
+ let uu___256
+ =
text
"Eagerly embed and unembed terms to primitive operations and plugins: not recommended except for benchmarking" in
(FStar_Getopt.noshort,
"eager_embedding",
(WithSideEffect
((fun
- uu___256
+ uu___257
->
FStar_Compiler_Effect.op_Colon_Equals
eager_embedding
@@ -3152,13 +3173,13 @@ let rec (specs_with_types :
(Const
(Bool
true)))),
- uu___255) in
- let uu___255
- =
+ uu___256) in
let uu___256
=
let uu___257
=
+ let uu___258
+ =
text
"Emit profiles grouped by declaration rather than by module" in
(FStar_Getopt.noshort,
@@ -3166,13 +3187,13 @@ let rec (specs_with_types :
(Const
(Bool
true)),
- uu___257) in
- let uu___257
- =
+ uu___258) in
let uu___258
=
let uu___259
=
+ let uu___260
+ =
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
(FStar_Getopt.noshort,
@@ -3180,13 +3201,13 @@ let rec (specs_with_types :
(Accumulated
(SimpleStr
"One or more space-separated occurrences of '[+|-]( * | namespace | module | identifier)'")),
- uu___259) in
- let uu___259
- =
+ uu___260) in
let uu___260
=
let uu___261
=
+ let uu___262
+ =
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
(FStar_Getopt.noshort,
@@ -3194,47 +3215,47 @@ let rec (specs_with_types :
(Accumulated
(SimpleStr
"One or more space-separated occurrences of '[+|-]( * | namespace | module)'")),
- uu___261) in
- let uu___261
- =
+ uu___262) in
let uu___262
=
let uu___263
=
+ let uu___264
+ =
text
"Display this information" in
(104,
"help",
(WithSideEffect
((fun
- uu___264
+ uu___265
->
(
- let uu___266
+ let uu___267
=
specs
warn_unsafe in
display_usage_aux
- uu___266);
+ uu___267);
FStar_Compiler_Effect.exit
Prims.int_zero),
(Const
(Bool
true)))),
- uu___263) in
- let uu___263
- =
+ uu___264) in
let uu___264
=
let uu___265
=
+ let uu___266
+ =
text
"List all debug keys and exit" in
(FStar_Getopt.noshort,
"list_debug_keys",
(WithSideEffect
((fun
- uu___266
+ uu___267
->
display_debug_keys
();
@@ -3243,173 +3264,173 @@ let rec (specs_with_types :
(Const
(Bool
true)))),
- uu___265) in
- [uu___264] in
- uu___262
+ uu___266) in
+ [uu___265] in
+ uu___263
::
- uu___263 in
- uu___260
+ uu___264 in
+ uu___261
::
- uu___261 in
- uu___258
+ uu___262 in
+ uu___259
::
- uu___259 in
- uu___256
+ uu___260 in
+ uu___257
::
- uu___257 in
- uu___254
+ uu___258 in
+ uu___255
::
- uu___255 in
- uu___252
+ uu___256 in
+ uu___253
::
- uu___253 in
- uu___250
+ uu___254 in
+ uu___251
::
- uu___251 in
- uu___248
+ uu___252 in
+ uu___249
::
- uu___249 in
- uu___246
+ uu___250 in
+ uu___247
::
- uu___247 in
- uu___244
+ uu___248 in
+ uu___245
::
- uu___245 in
- uu___242
+ uu___246 in
+ uu___243
::
- uu___243 in
- uu___240
+ uu___244 in
+ uu___241
::
- uu___241 in
- uu___238
+ uu___242 in
+ uu___239
::
- uu___239 in
- uu___236
+ uu___240 in
+ uu___237
::
- uu___237 in
- uu___234
+ uu___238 in
+ uu___235
::
- uu___235 in
- uu___232
+ uu___236 in
+ uu___233
::
- uu___233 in
- uu___230
+ uu___234 in
+ uu___231
::
- uu___231 in
- uu___228
+ uu___232 in
+ uu___229
::
- uu___229 in
- uu___226
+ uu___230 in
+ uu___227
::
- uu___227 in
- uu___224
+ uu___228 in
+ uu___225
::
- uu___225 in
- uu___222
+ uu___226 in
+ uu___223
::
- uu___223 in
- uu___220
+ uu___224 in
+ uu___221
::
- uu___221 in
- uu___218
+ uu___222 in
+ uu___219
::
- uu___219 in
- uu___216
+ uu___220 in
+ uu___217
::
- uu___217 in
- uu___214
+ uu___218 in
+ uu___215
::
- uu___215 in
- uu___212
+ uu___216 in
+ uu___213
::
- uu___213 in
- uu___210
+ uu___214 in
+ uu___211
::
- uu___211 in
- uu___208
+ uu___212 in
+ uu___209
::
- uu___209 in
- uu___206
+ uu___210 in
+ uu___207
::
- uu___207 in
- uu___204
+ uu___208 in
+ uu___205
::
- uu___205 in
- uu___202
+ uu___206 in
+ uu___203
::
- uu___203 in
- uu___200
+ uu___204 in
+ uu___201
::
- uu___201 in
- uu___198
+ uu___202 in
+ uu___199
::
- uu___199 in
- uu___196
+ uu___200 in
+ uu___197
::
- uu___197 in
- uu___194
+ uu___198 in
+ uu___195
::
- uu___195 in
- uu___192
+ uu___196 in
+ uu___193
::
- uu___193 in
- uu___190
+ uu___194 in
+ uu___191
::
- uu___191 in
- uu___188
+ uu___192 in
+ uu___189
::
- uu___189 in
- uu___186
+ uu___190 in
+ uu___187
::
- uu___187 in
- uu___184
+ uu___188 in
+ uu___185
::
- uu___185 in
- uu___182
+ uu___186 in
+ uu___183
::
- uu___183 in
- uu___180
+ uu___184 in
+ uu___181
::
- uu___181 in
- uu___178
+ uu___182 in
+ uu___179
::
- uu___179 in
- uu___176
+ uu___180 in
+ uu___177
::
- uu___177 in
- uu___174
+ uu___178 in
+ uu___175
::
- uu___175 in
- uu___172
+ uu___176 in
+ uu___173
::
- uu___173 in
- uu___170
+ uu___174 in
+ uu___171
::
- uu___171 in
- uu___168
+ uu___172 in
+ uu___169
::
- uu___169 in
- uu___166
+ uu___170 in
+ uu___167
::
- uu___167 in
- uu___164
+ uu___168 in
+ uu___165
::
- uu___165 in
- uu___162
+ uu___166 in
+ uu___163
::
- uu___163 in
- uu___160
+ uu___164 in
+ uu___161
::
- uu___161 in
- uu___158
+ uu___162 in
+ uu___159
::
- uu___159 in
- uu___156
+ uu___160 in
+ uu___157
::
- uu___157 in
- uu___154
+ uu___158 in
+ uu___155
::
- uu___155 in
+ uu___156 in
uu___152
::
uu___153 in
@@ -3703,7 +3724,7 @@ let (settable_specs :
(fun uu___ ->
match uu___ with | ((uu___1, x, uu___2), uu___3) -> settable x)
all_specs
-let (uu___662 :
+let (uu___672 :
(((unit -> FStar_Getopt.parse_cmdline_res) -> unit) *
(unit -> FStar_Getopt.parse_cmdline_res)))
=
@@ -3720,11 +3741,11 @@ let (uu___662 :
(set1, call)
let (set_error_flags_callback_aux :
(unit -> FStar_Getopt.parse_cmdline_res) -> unit) =
- match uu___662 with
+ match uu___672 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___662 with
+ match uu___672 with
| (set_error_flags_callback_aux1, set_error_flags1) -> set_error_flags1
let (set_error_flags_callback :
(unit -> FStar_Getopt.parse_cmdline_res) -> unit) =
@@ -4040,22 +4061,6 @@ let (cache_off : unit -> Prims.bool) = fun uu___ -> get_cache_off ()
let (print_cache_version : unit -> Prims.bool) =
fun uu___ -> get_print_cache_version ()
let (cmi : unit -> Prims.bool) = fun uu___ -> get_cmi ()
-type codegen_t =
- | OCaml
- | FSharp
- | Krml
- | Plugin
- | Extension
-let (uu___is_OCaml : codegen_t -> Prims.bool) =
- fun projectee -> match projectee with | OCaml -> true | uu___ -> false
-let (uu___is_FSharp : codegen_t -> Prims.bool) =
- fun projectee -> match projectee with | FSharp -> true | uu___ -> false
-let (uu___is_Krml : codegen_t -> Prims.bool) =
- fun projectee -> match projectee with | Krml -> true | uu___ -> false
-let (uu___is_Plugin : codegen_t -> Prims.bool) =
- fun projectee -> match projectee with | Plugin -> true | uu___ -> false
-let (uu___is_Extension : codegen_t -> Prims.bool) =
- fun projectee -> match projectee with | Extension -> true | uu___ -> false
let (parse_codegen :
Prims.string -> codegen_t FStar_Pervasives_Native.option) =
fun uu___ ->
@@ -4788,65 +4793,4 @@ let (set_vconfig : FStar_VConfig.vconfig -> unit) =
(let uu___28 =
option_as (fun uu___29 -> String uu___29)
vcfg.FStar_VConfig.reuse_hint_for in
- set_option "reuse_hint_for" uu___28)
-let (parse_ext : Prims.string -> (Prims.string * Prims.string) Prims.list) =
- fun s ->
- let exts = FStar_Compiler_Util.split s ";" in
- FStar_Compiler_List.collect
- (fun s1 ->
- match FStar_Compiler_Util.split s1 "=" with
- | k::v::[] -> [(k, v)]
- | uu___ -> [(s1, "1")]) exts
-let ext_dedup :
- 'a . (Prims.string * 'a) Prims.list -> (Prims.string * 'a) Prims.list =
- fun l ->
- FStar_Compiler_List.fold_right
- (fun uu___ ->
- fun rest ->
- match uu___ with
- | (k, v) ->
- let uu___1 =
- FStar_Compiler_List.existsb
- (fun uu___2 -> match uu___2 with | (k', uu___3) -> k = k')
- rest in
- if uu___1 then rest else (k, v) :: rest) l []
-let (all_ext_options : unit -> (Prims.string * Prims.string) Prims.list) =
- fun uu___ ->
- let ext = get_ext () in
- match ext with
- | FStar_Pervasives_Native.None -> []
- | FStar_Pervasives_Native.Some strs ->
- let uu___1 = FStar_Compiler_List.collect parse_ext strs in
- ext_dedup uu___1
-let (ext_getv : Prims.string -> Prims.string) =
- fun k ->
- let ext = all_ext_options () in
- let uu___ =
- FStar_Compiler_Util.find_map ext
- (fun uu___1 ->
- match uu___1 with
- | (k', v) ->
- if k = k'
- then FStar_Pervasives_Native.Some v
- else FStar_Pervasives_Native.None) in
- FStar_Compiler_Util.dflt "" uu___
-let (ext_getns : Prims.string -> (Prims.string * Prims.string) Prims.list) =
- fun ns ->
- let is_prefix s1 s2 =
- let l1 = FStar_Compiler_String.length s1 in
- let l2 = FStar_Compiler_String.length s2 in
- (l2 >= l1) &&
- (let uu___ = FStar_Compiler_Util.substring s2 Prims.int_zero l1 in
- uu___ = s1) in
- let exts = all_ext_options () in
- FStar_Compiler_List.filter_map
- (fun uu___ ->
- match uu___ with
- | (k', v) ->
- let uu___1 =
- (k' = ns) ||
- (let uu___2 = FStar_Compiler_String.op_Hat ns ":" in
- is_prefix uu___2 k') in
- if uu___1
- then FStar_Pervasives_Native.Some (k', v)
- else FStar_Pervasives_Native.None) exts
\ No newline at end of file
+ set_option "reuse_hint_for" uu___28)
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Options_Ext.ml b/ocaml/fstar-lib/generated/FStar_Options_Ext.ml
new file mode 100644
index 00000000000..c16437ff48b
--- /dev/null
+++ b/ocaml/fstar-lib/generated/FStar_Options_Ext.ml
@@ -0,0 +1,67 @@
+open Prims
+type key = Prims.string
+type value = Prims.string
+type ext_state =
+ | E of Prims.string FStar_Compiler_Util.psmap
+let (uu___is_E : ext_state -> Prims.bool) = fun projectee -> true
+let (__proj__E__item__map :
+ ext_state -> Prims.string FStar_Compiler_Util.psmap) =
+ fun projectee -> match projectee with | E map -> map
+let (cur_state : ext_state FStar_Compiler_Effect.ref) =
+ let uu___ = let uu___1 = FStar_Compiler_Util.psmap_empty () in E uu___1 in
+ FStar_Compiler_Util.mk_ref uu___
+let (set : key -> value -> unit) =
+ fun k ->
+ fun v ->
+ let uu___ =
+ let uu___1 =
+ let uu___2 =
+ let uu___3 = FStar_Compiler_Effect.op_Bang cur_state in
+ __proj__E__item__map uu___3 in
+ FStar_Compiler_Util.psmap_add uu___2 k v in
+ E uu___1 in
+ FStar_Compiler_Effect.op_Colon_Equals cur_state uu___
+let (get : key -> value) =
+ fun k ->
+ let r =
+ let uu___ =
+ let uu___1 =
+ let uu___2 = FStar_Compiler_Effect.op_Bang cur_state in
+ __proj__E__item__map uu___2 in
+ FStar_Compiler_Util.psmap_try_find uu___1 k in
+ match uu___ with
+ | FStar_Pervasives_Native.None -> ""
+ | FStar_Pervasives_Native.Some v -> v in
+ r
+let (is_prefix : Prims.string -> Prims.string -> Prims.bool) =
+ fun s1 ->
+ fun s2 ->
+ let l1 = FStar_Compiler_String.length s1 in
+ let l2 = FStar_Compiler_String.length s2 in
+ (l2 >= l1) &&
+ (let uu___ = FStar_Compiler_String.substring s2 Prims.int_zero l1 in
+ uu___ = s1)
+let (getns : Prims.string -> (key * value) Prims.list) =
+ fun ns ->
+ let f k v acc =
+ let uu___ = is_prefix (Prims.strcat ns ":") k in
+ if uu___ then (k, v) :: acc else acc in
+ let uu___ =
+ let uu___1 = FStar_Compiler_Effect.op_Bang cur_state in
+ __proj__E__item__map uu___1 in
+ FStar_Compiler_Util.psmap_fold uu___ f []
+let (all : unit -> (key * value) Prims.list) =
+ fun uu___ ->
+ let f k v acc = (k, v) :: acc in
+ let uu___1 =
+ let uu___2 = FStar_Compiler_Effect.op_Bang cur_state in
+ __proj__E__item__map uu___2 in
+ FStar_Compiler_Util.psmap_fold uu___1 f []
+let (save : unit -> ext_state) =
+ fun uu___ -> FStar_Compiler_Effect.op_Bang cur_state
+let (restore : ext_state -> unit) =
+ fun s -> FStar_Compiler_Effect.op_Colon_Equals cur_state s
+let (reset : unit -> unit) =
+ fun uu___ ->
+ let uu___1 = let uu___2 = FStar_Compiler_Util.psmap_empty () in E uu___2 in
+ FStar_Compiler_Effect.op_Colon_Equals cur_state uu___1
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml
index 60843db1b37..d185d691a1e 100644
--- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml
+++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml
@@ -3898,7 +3898,7 @@ let (encode_sig_inductive :
let uu___9 =
injective_type_params ||
(let uu___10 =
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:injectivity" in
uu___10 <> "") in
if uu___9
@@ -4322,7 +4322,7 @@ let (encode_datacon :
let injective_type_params1 =
injective_type_params ||
(let uu___6 =
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:injectivity" in
uu___6 <> "") in
let fields =
@@ -4920,7 +4920,7 @@ let (encode_datacon :
=
let uu___44
=
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:2954" in
uu___44
<> "" in
@@ -4940,7 +4940,7 @@ let (encode_datacon :
=
let uu___43
=
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:2954" in
uu___43
<> "" in
@@ -5660,7 +5660,7 @@ let (encode_datacon :
=
let uu___40
=
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:2954" in
uu___40
<> "" in
@@ -5680,7 +5680,7 @@ let (encode_datacon :
=
let uu___39
=
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:2954" in
uu___39
<> "" in
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml
index 2b644afe5ae..2790f921dbe 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml
@@ -6207,9 +6207,7 @@ let (set_options : Prims.string -> unit FStar_Tactics_Monad.tac) =
(fun g ->
let g = Obj.magic g in
FStar_Options.push ();
- (let uu___3 =
- FStar_Compiler_Util.smap_copy g.FStar_Tactics_Types.opts in
- FStar_Options.set uu___3);
+ FStar_Options.set g.FStar_Tactics_Types.opts;
(let res = FStar_Options.set_options s in
let opts' = FStar_Options.peek () in
FStar_Options.pop ();
@@ -9291,10 +9289,7 @@ let (get_vconfig : unit -> FStar_VConfig.vconfig FStar_Tactics_Monad.tac) =
let vcfg =
FStar_Options.with_saved_options
(fun uu___1 ->
- (let uu___3 =
- FStar_Compiler_Util.smap_copy
- g.FStar_Tactics_Types.opts in
- FStar_Options.set uu___3);
+ FStar_Options.set g.FStar_Tactics_Types.opts;
FStar_Options.get_vconfig ()) in
Obj.magic (ret vcfg)) uu___1))) uu___
let (set_vconfig : FStar_VConfig.vconfig -> unit FStar_Tactics_Monad.tac) =
@@ -9307,10 +9302,7 @@ let (set_vconfig : FStar_VConfig.vconfig -> unit FStar_Tactics_Monad.tac) =
let opts' =
FStar_Options.with_saved_options
(fun uu___ ->
- (let uu___2 =
- FStar_Compiler_Util.smap_copy
- g.FStar_Tactics_Types.opts in
- FStar_Options.set uu___2);
+ FStar_Options.set g.FStar_Tactics_Types.opts;
FStar_Options.set_vconfig vcfg;
FStar_Options.peek ()) in
let g' =
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
index b795ab75d1d..1a78da2316a 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
@@ -7050,9 +7050,7 @@ let (set_options : Prims.string -> unit FStar_Tactics_Monad.tac) =
(fun g ->
let g = Obj.magic g in
FStar_Options.push ();
- (let uu___3 =
- FStar_Compiler_Util.smap_copy g.FStar_Tactics_Types.opts in
- FStar_Options.set uu___3);
+ FStar_Options.set g.FStar_Tactics_Types.opts;
(let res = FStar_Options.set_options s in
let opts' = FStar_Options.peek () in
FStar_Options.pop ();
@@ -9877,10 +9875,7 @@ let (get_vconfig : unit -> FStar_VConfig.vconfig FStar_Tactics_Monad.tac) =
let vcfg =
FStar_Options.with_saved_options
(fun uu___1 ->
- (let uu___3 =
- FStar_Compiler_Util.smap_copy
- g.FStar_Tactics_Types.opts in
- FStar_Options.set uu___3);
+ FStar_Options.set g.FStar_Tactics_Types.opts;
FStar_Options.get_vconfig ()) in
Obj.magic
(FStar_Class_Monad.return FStar_Tactics_Monad.monad_tac
@@ -9895,10 +9890,7 @@ let (set_vconfig : FStar_VConfig.vconfig -> unit FStar_Tactics_Monad.tac) =
let opts' =
FStar_Options.with_saved_options
(fun uu___ ->
- (let uu___2 =
- FStar_Compiler_Util.smap_copy
- g.FStar_Tactics_Types.opts in
- FStar_Options.set uu___2);
+ FStar_Options.set g.FStar_Tactics_Types.opts;
FStar_Options.set_vconfig vcfg;
FStar_Options.peek ()) in
let g' =
@@ -9989,7 +9981,7 @@ let (all_ext_options :
(fun uu___2 ->
(fun uu___2 ->
let uu___2 = Obj.magic uu___2 in
- let uu___3 = FStar_Options.all_ext_options () in
+ let uu___3 = FStar_Options_Ext.all () in
Obj.magic
(FStar_Class_Monad.return FStar_Tactics_Monad.monad_tac
() (Obj.magic uu___3))) uu___2))) uu___
@@ -10005,7 +9997,7 @@ let (ext_getv : Prims.string -> Prims.string FStar_Tactics_Monad.tac) =
(fun uu___1 ->
(fun uu___1 ->
let uu___1 = Obj.magic uu___1 in
- let uu___2 = FStar_Options.ext_getv k in
+ let uu___2 = FStar_Options_Ext.get k in
Obj.magic
(FStar_Class_Monad.return FStar_Tactics_Monad.monad_tac
() (Obj.magic uu___2))) uu___1))) uu___
@@ -10024,7 +10016,7 @@ let (ext_getns :
(fun uu___1 ->
(fun uu___1 ->
let uu___1 = Obj.magic uu___1 in
- let uu___2 = FStar_Options.ext_getns ns in
+ let uu___2 = FStar_Options_Ext.getns ns in
Obj.magic
(FStar_Class_Monad.return FStar_Tactics_Monad.monad_tac
() (Obj.magic uu___2))) uu___1))) uu___
diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
index d12f0c4948c..a65eaac245c 100644
--- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml
@@ -10425,12 +10425,12 @@ let (desugar_modul :
(uu___5, modul1)))))
let with_options : 'a . (unit -> 'a) -> 'a =
fun f ->
- FStar_Options.push ();
- (let res = f () in
- let light = FStar_Options.ml_ish () in
- FStar_Options.pop ();
- if light then FStar_Options.set_ml_ish () else ();
- res)
+ let uu___ =
+ FStar_Options.with_saved_options
+ (fun uu___1 ->
+ let r = f () in let light = FStar_Options.ml_ish () in (light, r)) in
+ match uu___ with
+ | (light, r) -> (if light then FStar_Options.set_ml_ish () else (); r)
let (ast_modul_to_modul :
FStar_Parser_AST.modul ->
FStar_Syntax_Syntax.modul FStar_Syntax_DsEnv.withenv)
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
index 17167a4de7f..09db997543b 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
@@ -2501,7 +2501,7 @@ let (config' :
(FStar_Options.normalize_pure_terms_for_extraction ()) in
let uu___2 =
let uu___3 =
- FStar_Options.ext_getv "compat:normalizer_memo_ignore_cfg" in
+ FStar_Options_Ext.get "compat:normalizer_memo_ignore_cfg" in
uu___3 <> "" in
{
steps;
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
index c5a083ce8ed..e6b3cff8f98 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml
@@ -15961,7 +15961,7 @@ let (resolve_implicits' :
Prims.op_Negation uu___8))
&&
(let uu___8 =
- FStar_Options.ext_getv
+ FStar_Options_Ext.get
"compat:open_metas" in
uu___8 = "") in
if uu___7
From 0d9668aa3c898349e88295134721c34402ade24e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 27 Aug 2024 20:11:59 -0700
Subject: [PATCH 3/3] Add a test
---
tests/micro-benchmarks/Ext.fst | 41 ++++++++++++++++++++++++++++++++++
1 file changed, 41 insertions(+)
create mode 100644 tests/micro-benchmarks/Ext.fst
diff --git a/tests/micro-benchmarks/Ext.fst b/tests/micro-benchmarks/Ext.fst
new file mode 100644
index 00000000000..bb223d2faa7
--- /dev/null
+++ b/tests/micro-benchmarks/Ext.fst
@@ -0,0 +1,41 @@
+module Ext
+
+open FStar.Tactics.V2
+
+let check (k:string) (s:string) : Tac unit =
+ let r = ext_getv k in
+ if r <> s then
+ fail ("Expected '" ^ s ^ "' but got '" ^ r ^ "'")
+
+#reset-options "--ext foo=bar"
+
+let _0 = assert True by (check "foo" "bar")
+
+#reset-options ""
+
+let _1 = assert True by (check "foo" "")
+
+let _2 = assert True by (check "foo" "")
+
+#push-options "--ext foo=bar"
+
+let _3 = assert True by (check "foo" "bar"; dump "")
+
+#pop-options
+
+let _4 = assert True by (check "foo" "")
+
+#push-options "--ext foo=bar2"
+let _5 = assert True by (check "foo" "bar2")
+ #push-options "--ext goo=bar3,foo=bar3"
+ let _6 = assert True by (check "goo" "bar3")
+ let _7 = assert True by (check "foo" "bar3")
+ #pop-options
+let _8 = assert True by (check "foo" "bar2")
+#pop-options
+
+let _9 = assert True by (check "foo" "")
+
+#set-options "--ext foo=bar4"
+
+let _10 = assert True by (check "foo" "bar4")