From 9fe84466425a1b4646fd5d66a8b7196044bf1e6d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 20 Oct 2023 13:08:03 -0700 Subject: [PATCH 1/7] Normalizer: introduce strict_on_args_unfold --- src/parser/FStar.Parser.Const.fst | 1 + src/typechecker/FStar.TypeChecker.Cfg.fst | 3 +- src/typechecker/FStar.TypeChecker.Env.fst | 9 +- src/typechecker/FStar.TypeChecker.Env.fsti | 4 +- src/typechecker/FStar.TypeChecker.NBE.fst | 2 +- .../FStar.TypeChecker.Normalize.fst | 307 ++++++++++++------ .../FStar.TypeChecker.Normalize.fsti | 1 + ulib/FStar.Pervasives.fst | 1 + ulib/FStar.Pervasives.fsti | 1 + 9 files changed, 228 insertions(+), 101 deletions(-) diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index 3c28d62b05f..760ef963443 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -341,6 +341,7 @@ let tcnorm_attr = p2l ["FStar"; "Pervasives"; "tcnorm"] let dm4f_bind_range_attr = p2l ["FStar"; "Pervasives"; "dm4f_bind_range"] let must_erase_for_extraction_attr = psconst "must_erase_for_extraction" let strict_on_arguments_attr = p2l ["FStar"; "Pervasives"; "strict_on_arguments"] +let strict_on_arguments_unfold_attr = p2l ["FStar"; "Pervasives"; "strict_on_arguments_unfold"] let resolve_implicits_attr_string = "FStar.Pervasives.resolve_implicits" let override_resolve_implicits_handler_lid = p2l ["FStar"; "Pervasives"; "override_resolve_implicits_handler"] let handle_smt_goals_attr = psconst "handle_smt_goals" diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst index 9b773043bf9..d0c5f7c5260 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fst +++ b/src/typechecker/FStar.TypeChecker.Cfg.fst @@ -213,7 +213,8 @@ let equality_ops = prim_from_list equality_ops_list let cfg_to_string cfg = String.concat "\n" ["{"; - BU.format1 " steps = %s" (steps_to_string cfg.steps); + BU.format1 " steps = %s;" (steps_to_string cfg.steps); + BU.format1 " delta_level = %s;" (FStar.Common.string_of_list Env.string_of_delta_level cfg.delta_level); "}" ] let cfg_env cfg = cfg.tcenv diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 71b602afdc4..f5ca66e8cc3 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -862,7 +862,14 @@ let fv_has_strict_args env fv = fst (FStar.ToSyntax.ToSyntax.parse_attr_with_list false x FStar.Parser.Const.strict_on_arguments_attr)) in - true, res + if Some? res then true, Some (false, Some?.v res) else + let res = + BU.find_map attrs (fun x -> + fst (FStar.ToSyntax.ToSyntax.parse_attr_with_list + false x FStar.Parser.Const.strict_on_arguments_unfold_attr)) + in + if Some? res then true, Some (true, Some?.v res) else + true, None in cache_in_fv_tab env.strict_args_tab fv f diff --git a/src/typechecker/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti index 34361e63563..0ef5395c6de 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fsti +++ b/src/typechecker/FStar.TypeChecker.Env.fsti @@ -207,7 +207,7 @@ and env = { tc_hooks : tcenv_hooks; (* hooks that the interactive more relies onto for symbol tracking *) dsenv : FStar.Syntax.DsEnv.env; (* The desugaring environment from the front-end *) nbe : list step -> env -> term -> term; (* Callback to the NBE function *) - strict_args_tab:BU.smap (option (list int)); (* a dictionary of fv names to strict arguments *) + strict_args_tab:BU.smap (option (bool * list int)); (* a dictionary of fv names to strict arguments *) erasable_types_tab:BU.smap bool; (* a dictionary of type names to erasable types *) enable_defer_to_tac: bool; (* Set by default; unset when running within a tactic itself, since we do not allow a tactic to defer problems to another tactic via the attribute mechanism *) @@ -316,7 +316,7 @@ val attrs_of_qninfo : qninfo -> option (list attribute) val lookup_attrs_of_lid : env -> lid -> option (list attribute) val fv_with_lid_has_attr : env -> fv_lid:lid -> attr_lid:lid -> bool val fv_has_attr : env -> fv -> attr_lid:lid -> bool -val fv_has_strict_args : env -> fv -> option (list int) +val fv_has_strict_args : env -> fv -> option (bool & list int) // bool: should_unfold val fv_has_erasable_attr : env -> fv -> bool val non_informative : env -> typ -> bool val try_lookup_effect_lid : env -> lident -> option term diff --git a/src/typechecker/FStar.TypeChecker.NBE.fst b/src/typechecker/FStar.TypeChecker.NBE.fst index 75ecae8dfdd..3c15b374632 100644 --- a/src/typechecker/FStar.TypeChecker.NBE.fst +++ b/src/typechecker/FStar.TypeChecker.NBE.fst @@ -862,7 +862,7 @@ and translate_fv (cfg: config) (bs:list t) (fvar:fv): t = let qninfo = Env.lookup_qname (Cfg.cfg_env cfg.core_cfg) (S.lid_of_fv fvar) in if is_constr qninfo || is_constr_fv fvar then mkConstruct fvar [] [] else - match N.should_unfold cfg.core_cfg (fun _ -> cfg.core_cfg.reifying) fvar qninfo with + match N.should_unfold cfg.core_cfg false (fun _ -> cfg.core_cfg.reifying) fvar qninfo with | N.Should_unfold_fully -> failwith "Not yet handled" diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index e9029d99c19..c42933eddf7 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -133,7 +133,7 @@ let set_memo cfg (r:memo (Cfg.cfg * 'a)) (t:'a) : unit = let closure_to_string = function | Clos (env, t, _, _) -> BU.format2 "(env=%s elts; %s)" (List.length env |> string_of_int) (Print.term_to_string t) - | Univ _ -> "Univ" + | Univ u -> "Univ (" ^ Print.univ_to_string u ^ ")" | Dummy -> "dummy" let env_to_string env = //BU.format1 "(%s elements)" (string_of_int <| List.length env) @@ -148,14 +148,13 @@ let stack_elt_to_string = function | Arg (c, _, _) -> BU.format1 "Closure %s" (closure_to_string c) | MemoLazy _ -> "MemoLazy" | Abs (_, bs, _, _, _) -> BU.format1 "Abs %s" (string_of_int <| List.length bs) - | UnivArgs _ -> "UnivArgs" + | UnivArgs (us, _) -> "UnivArgs (" ^ Print.univs_to_string us ^ ")" | Match _ -> "Match" | App (_, t,_,_) -> BU.format1 "App %s" (Print.term_to_string t) | CBVApp (_, t,_,_) -> BU.format1 "CBVApp %s" (Print.term_to_string t) | Meta (_, m,_) -> "Meta" | Let _ -> "Let" | Cfg _ -> "Cfg" - // | _ -> "Match" let stack_to_string s = List.map stack_elt_to_string s |> String.concat "; " @@ -210,17 +209,25 @@ let norm_universe cfg (env:env) u = match u with | U_bvar x -> begin - try match snd (List.nth env x) with - | Univ u -> - if Env.debug cfg.tcenv <| Options.Other "univ_norm" then - BU.print1 "Univ (in norm_universe): %s\n" (Print.univ_to_string u) - else (); aux u - | Dummy -> [u] - | _ -> failwith (BU.format1 "Impossible: universe variable u@%s bound to a term" - (string_of_int x)) - with _ -> if cfg.steps.allow_unbound_universes - then [U_unknown] - else failwith ("Universe variable not found: u@" ^ string_of_int x) + let vo = + try Some (snd (List.nth env x)) + with | _ -> None + in + match vo with + | Some (Univ u) -> + if Env.debug cfg.tcenv <| Options.Other "univ_norm" then + BU.print1 "Univ (in norm_universe): %s\n" (Print.univ_to_string u); + aux u + | Some Dummy -> + [u] + | Some _ -> + if cfg.steps.allow_unbound_universes + then [U_unknown] + else failwith (BU.format1 "Impossible: universe variable u@%s bound to a term" (string_of_int x)) + | None -> + if cfg.steps.allow_unbound_universes + then [U_unknown] + else failwith ("Universe variable not found: u@" ^ string_of_int x ^ " -- " ^ string_of_int (List.length env)) end | U_unif _ when cfg.steps.check_no_uvars -> [U_zero] // GM: why? @@ -905,7 +912,7 @@ let rec maybe_weakly_reduced tm : bool = Initialized below in normalize *) let plugin_unfold_warn_ctr : ref int = BU.mk_ref 0 -let should_unfold cfg should_reify fv qninfo : should_unfold_res = +let should_unfold cfg strict_ok should_reify fv qninfo : should_unfold_res = let attrs = match Env.attrs_of_qninfo qninfo with | None -> [] @@ -954,6 +961,13 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = (string_of_bool b)); if b then reif else no + // If this definition is marked strict_on_arguments, we will not + // unfold standalone occurrences of it, only applications that + // pass the strictness check. + | _ when not strict_ok && Some? (Env.fv_has_strict_args cfg.tcenv fv) -> + log_unfolding cfg (fun () -> BU.print_string " >> Not unfolding strict_on_arguments definition\n"); + no + // If it is handled primitively, then don't unfold | _ when Option.isSome (find_prim_step cfg fv) -> log_unfolding cfg (fun () -> BU.print_string " >> It's a primop, not unfolding\n"); @@ -1061,9 +1075,9 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = plugin_unfold_warn_ctr := !plugin_unfold_warn_ctr - 1 end; r -let decide_unfolding cfg stack rng fv qninfo (* : option (cfg * stack) *) = +let decide_unfolding cfg strict_ok stack rng fv qninfo (* : option (cfg * stack) *) = let res = - should_unfold cfg (fun cfg -> should_reify cfg stack) fv qninfo + should_unfold cfg strict_ok (fun cfg -> should_reify cfg stack) fv qninfo in match res with | Should_unfold_no -> @@ -1203,7 +1217,7 @@ let rec norm : cfg -> env -> stack -> term -> term = log_unfolding cfg (fun () -> BU.print1 " >> This is a constant: %s\n" (Print.term_to_string t)); rebuild cfg empty_env stack t | _ -> - match decide_unfolding cfg stack t.pos fv qninfo with + match decide_unfolding cfg false stack t.pos fv qninfo with | Some (cfg, stack) -> do_unfold_fv cfg stack t qninfo fv | None -> rebuild cfg empty_env stack t end @@ -1425,15 +1439,9 @@ let rec norm : cfg -> env -> stack -> term -> term = | [] -> fallback () end - | Tm_app {hd=head; args} -> - let strict_args = - match (head |> U.unascribe |> U.un_uinst).n with - | Tm_fvar fv -> Env.fv_has_strict_args cfg.tcenv fv - | _ -> None - in - begin - match strict_args with - | None -> + | Tm_app {hd=head; args} -> begin + let fallback () = + (* normal application *) let stack = List.fold_right (fun (a, aq) stack -> @@ -1460,44 +1468,26 @@ let rec norm : cfg -> env -> stack -> term -> term = args stack in - log cfg (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args)); + log cfg (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args)); norm cfg env stack head - - | Some strict_args -> - // BU.print2 "%s has strict args [%s]\n" - // (Print.term_to_string head) - // (List.map string_of_int strict_args |> String.concat "; "); - let norm_args = args |> List.map (fun (a, i) -> (norm cfg env [] a, i)) in - let norm_args_len = List.length norm_args in - if strict_args - |> List.for_all (fun i -> - if i >= norm_args_len then false - else - let arg_i, _ = List.nth norm_args i in - let head, _ = arg_i |> U.unmeta_safe |> U.head_and_args in - match (un_uinst head).n with - | Tm_constant _ -> true - | Tm_fvar fv -> Env.is_datacon cfg.tcenv (S.lid_of_fv fv) - | _ -> false) - then //all strict args have constant head symbols - let stack = - stack |> - List.fold_right (fun (a, aq) stack -> - Arg (Clos(env, a, BU.mk_ref (Some (cfg, ([], a))), false),aq,t.pos)::stack) - norm_args - in - log cfg (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args)); - norm cfg env stack head - else let head = closure_as_term cfg env head in - let term = S.mk_Tm_app head norm_args t.pos in - // let _ = - // BU.print3 "Rebuilding %s as %s\n%s\n" - // (Print.term_to_string t) - // (Print.term_to_string term) - // (BU.stack_dump()) - // in - rebuild cfg env stack term - end + in + let head_fv_us_opt = + let head = U.unascribe head in + let head = SS.compress head in + match head.n with + | Tm_fvar fv -> Some (head, fv, []) + | Tm_uinst ({n = Tm_fvar fv}, us) -> Some (fst (Tm_uinst?._0 head.n), fv, us) + | _ -> None + in + match head_fv_us_opt with + | None -> fallback () + | Some (head, fv, us) -> + match Env.fv_has_strict_args cfg.tcenv fv with + | Some (strict_unfold, strict_args) -> + handle_strict_application cfg env stack head fv us strict_unfold strict_args args t.pos + | None -> + fallback() + end | Tm_refine {b=x} when cfg.steps.for_extraction @@ -1765,38 +1755,163 @@ let rec norm : cfg -> env -> stack -> term -> term = (* NOTE: we do not need any environment here, since an fv does not * have any free indices. Hence, we use empty_env as environment when needed. *) and do_unfold_fv cfg stack (t0:term) (qninfo : qninfo) (f:fv) : term = - match Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo with - | None -> - log_unfolding cfg (fun () -> // printfn "delta_level = %A, qninfo=%A" cfg.delta_level qninfo; - BU.print1 " >> No definition found for %s\n" (Print.fv_to_string f)); - rebuild cfg empty_env stack t0 - - | Some (us, t) -> - begin - log_unfolding cfg (fun () -> BU.print2 " >> Unfolded %s to %s\n" - (Print.term_to_string t0) (Print.term_to_string t)); - // preserve the range info on the returned term - let t = - if cfg.steps.unfold_until = Some delta_constant - //we're really trying to compute here; no point propagating range information - //which can be expensive - then t - else Subst.set_use_range t0.pos t - in - let n = List.length us in - if n > 0 - then match stack with //universe beta reduction - | UnivArgs(us', _)::stack -> - if Env.debug cfg.tcenv <| Options.Other "univ_norm" then - List.iter (fun x -> BU.print1 "Univ (normalizer) %s\n" (Print.univ_to_string x)) us' - else (); - let env = us' |> List.fold_left (fun env u -> (None, Univ u)::env) empty_env in - norm cfg env stack t - | _ when cfg.steps.erase_universes || cfg.steps.allow_unbound_universes -> - norm cfg empty_env stack t - | _ -> failwith (BU.format1 "Impossible: missing universe instantiation on %s" (Print.lid_to_string f.fv_name.v)) - else norm cfg empty_env stack t - end + match Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo with + | None -> + log_unfolding cfg (fun () -> // printfn "delta_level = %A, qninfo=%A" cfg.delta_level qninfo; + BU.print1 " >> No definition found for %s\n" (Print.fv_to_string f)); + rebuild cfg empty_env stack t0 + + | Some (us, t) -> begin + log_unfolding cfg (fun () -> BU.print2 " >> Unfolded %s to %s\n" + (Print.term_to_string t0) (Print.term_to_string t)); + // preserve the range info on the returned term + let t = + if cfg.steps.unfold_until = Some delta_constant + //we're really trying to compute here; no point propagating range information + //which can be expensive + then t + else Subst.set_use_range t0.pos t + in + let n = List.length us in + if n > 0 then + (* Universe beta reduction *) + match stack with + | UnivArgs(us', _)::stack -> + if n <> List.length us' then + failwith "ah!!!"; + if Env.debug cfg.tcenv <| Options.Other "univ_norm" then + List.iter (fun x -> BU.print1 "Univ (normalizer) %s\n" (Print.univ_to_string x)) us'; + let env = us' |> List.fold_left (fun env u -> (None, Univ u)::env) empty_env in + norm cfg env stack t + | _ when cfg.steps.erase_universes || cfg.steps.allow_unbound_universes -> + norm cfg empty_env stack t + | _ -> + log cfg (fun () -> BU.print1 "top of stack = %s\n" (stack_to_string (fst <| firstn 4 stack))); + failwith (BU.format1 "Impossible: missing universe instantiation on %s" (Print.lid_to_string f.fv_name.v)) + else + (* Not a universe-polymorphic definition, we should not have + universe arguments on the stack. *) + match stack with + | UnivArgs(us', _)::stack -> + failwith "univ args on not-uni-poly defn?" + | _ -> + norm cfg empty_env stack t + end + +and handle_strict_application (cfg:Cfg.cfg) (env:env) stack + (head:term) + (fv:fv) (us:universes) strict_unfold strict_args args + (rng:Range.range) += + log cfg (fun () -> BU.print3 "Got strict application for %s, strict_args = %s, strict_unfold = %s\n" + (Print.fv_to_string fv) + (FStar.Common.string_of_list string_of_int strict_args) + (string_of_bool strict_unfold)); + // BU.print2 "%s has strict args [%s]\n" + // (Print.term_to_string head) + // (List.map string_of_int strict_args |> String.concat "; "); + let cfg_args = + (* For strict_on_args_unfold, we change the config to make it + possibly unfold the argument. Note that we set WHNF, as all + we need is to check if the head reduced to a constructor. *) + if strict_unfold + then { cfg with steps = { cfg.steps with + unfold_only = None + ; unfold_fully = None + ; unfold_attr = None + ; unfold_qual = None + ; unfold_namespace = None + ; unfold_until = Some delta_constant + ; weak = true + ; hnf = true + }; + delta_level = [Unfold delta_constant]; + } + else cfg + in + //let cfg_args = { cfg_args with debug = Cfg.no_debug_switches } in + let args_len = List.length args in + + (* Normalize the arguments. We take a pass through all of them, + but we only use cfg_unfold if strict_unfold is on and this is + one of the strict args. Otherwise we just normalize with the current cfg. *) + let norm_args = args |> List.mapi (fun idx (a, i) -> + let a = + log cfg (fun () -> BU.print2 "Normalizing strict arg %s (%s)\n" + (string_of_int idx) + (Print.term_to_string a)); + if strict_unfold && List.mem idx strict_args then + norm cfg_args env [] a + else + norm cfg env [] a + in + (a, i)) + in + let is_hnf (i:int) : bool = + if i >= args_len then false + else + let arg_i, _ = List.nth norm_args i in + let head, _ = arg_i |> U.unmeta_safe |> U.head_and_args in + match (un_uinst head).n with + | Tm_constant _ -> true + | Tm_fvar fv -> Env.is_datacon cfg.tcenv (S.lid_of_fv fv) + | _ -> false + in + if List.for_all is_hnf strict_args then ( + log cfg (fun () -> BU.print2 "Strict reduction kicking in for %s<%s>\n" + (Print.term_to_string head) + (Print.univs_to_string us)); + (* All strict args have constant head symbols, unfold and reduce. + We manually unfold the head fv here since the normal case + for fvars will ignore variables marked with a strict_on_arguments + attribute to prevent the unfolding of standalone occurrences. *) + let lid = fv.fv_name.v in + let qninfo = Env.lookup_qname cfg.tcenv lid in + let stack = + stack |> + List.fold_right (fun (a, aq) stack -> + Arg (Clos(env, a, BU.mk_ref (Some (cfg, ([], a))), false), aq, rng)::stack) + norm_args + in + log cfg (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args)); + let stack = + match us with + | [] -> stack + | us -> + (* This normalization is needed to close the universes wrt the env. + The stack should only hold universe values. *) + let us = List.map (norm_universe cfg env) us in + UnivArgs (us, head.pos) :: stack + in + let head = SS.compress head in + match decide_unfolding cfg true stack head.pos fv qninfo with + | Some (cfg, stack) -> + (* Push arguments and universes *) + do_unfold_fv cfg stack head qninfo fv + | None -> + (* Just rebuild *) + rebuild cfg env stack head + ) else ( + (* Stop normalizing and rebuild. *) + log cfg (fun () -> BU.print2 "Strict reduction DID NOT kick in for %s<%s>, rebuilding\n" + (Print.term_to_string head) + (Print.univs_to_string us)); + let head = + match us with + | [] -> head + | us -> mk_Tm_uinst head us + in + let head = closure_as_term cfg env head in + let term = S.mk_Tm_app head norm_args rng in + // let _ = + // BU.print3 "Rebuilding %s as %s\n%s\n" + // (Print.term_to_string t) + // (Print.term_to_string term) + // (BU.stack_dump()) + // in + rebuild cfg env stack term + ) + and reduce_impure_comp cfg env stack (head : term) // monadic term (m : either monad_name (monad_name * monad_name)) diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fsti b/src/typechecker/FStar.TypeChecker.Normalize.fsti index 7c49abfbd57..60a5ed47c98 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fsti +++ b/src/typechecker/FStar.TypeChecker.Normalize.fsti @@ -30,6 +30,7 @@ type should_unfold_res = | Should_unfold_reify val should_unfold : cfg + -> strict_ok:bool -> should_reify:(cfg -> bool) -> fv -> Env.qninfo diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index 1c5a06b74ce..c578955ee7c 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -159,6 +159,7 @@ let tcdecltime = () let unifier_hint_injective = () let strict_on_arguments _ = () +let strict_on_arguments_unfold _ = () let resolve_implicits = () diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 08028f9cd80..ae54c748db0 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -934,6 +934,7 @@ val unifier_hint_injective : unit Otherwise, [f] is not unfolded and the term is [f e0 e1 e2] reduces to [f v0 v1 v2]. *) val strict_on_arguments (x: list int) : Tot unit +val strict_on_arguments_unfold (x: list int) : Tot unit (** * An attribute to tag a tactic designated to solve any From 640e73b7c9e74b3611bb696a50ff7ceedce3f10d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 24 Oct 2023 08:36:26 -0700 Subject: [PATCH 2/7] Tc: Disabling unfolding of tcnorm definitions between phases --- src/typechecker/FStar.TypeChecker.TcTerm.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index 7f913cb6802..155baf4172d 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -3817,7 +3817,7 @@ and check_top_level_let env e = if Env.debug env Options.Medium then BU.print1 "Let binding BEFORE tcnorm: %s\n" (Print.term_to_string e1); let e1 = if Options.tcnorm () then - N.normalize [Env.UnfoldAttr [Const.tcnorm_attr]; + N.normalize [//Env.UnfoldAttr [Const.tcnorm_attr]; Env.Exclude Env.Beta; Env.Exclude Env.Zeta; Env.NoFullNorm; Env.DoNotUnfoldPureLets] env e1 else e1 From 88ebcfa51cf75d7ec367bd79f2bbe399780b35c7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 12 Nov 2023 18:53:08 -0800 Subject: [PATCH 3/7] Tc: Rel: nit --- src/typechecker/FStar.TypeChecker.Rel.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index c528cee33cc..fee7239fe89 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -4197,7 +4197,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = let head2 = U.head_and_args t2 |> fst in let _ = if debug wl (Options.Other "Rel") - then BU.print ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + then BU.print ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" [(string_of_int problem.pid); (string_of_bool wl.smt_ok); (Print.term_to_string head1); From a9589a5b51b53859ab6bcd319da888171ca5ff7c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 12 Nov 2023 15:37:30 -0800 Subject: [PATCH 4/7] Tc: Rel: allow unfolding strict definitions --- src/typechecker/FStar.TypeChecker.Cfg.fst | 2 ++ src/typechecker/FStar.TypeChecker.Cfg.fsti | 3 +++ src/typechecker/FStar.TypeChecker.Env.fsti | 5 +++++ src/typechecker/FStar.TypeChecker.Normalize.fst | 5 ++++- src/typechecker/FStar.TypeChecker.Rel.fst | 1 + 5 files changed, 15 insertions(+), 1 deletion(-) diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst index d0c5f7c5260..9022fad257b 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fst +++ b/src/typechecker/FStar.TypeChecker.Cfg.fst @@ -144,6 +144,7 @@ let fstep_add_one s fs = | Inlining -> fs // not a step // ZP : Adding qualification because of name clash | DoNotUnfoldPureLets -> { fs with do_not_unfold_pure_lets = true } | UnfoldUntil d -> { fs with unfold_until = Some d } + | UnfoldStrict -> fs // Set at the cfg level | UnfoldOnly lids -> { fs with unfold_only = Some lids } | UnfoldFully lids -> { fs with unfold_fully = Some lids } | UnfoldAttr lids -> { fs with unfold_attr = Some lids } @@ -355,6 +356,7 @@ let config' psteps s e = ; steps = steps; delta_level = d; + unfold_strict_fvs = List.mem UnfoldStrict s; primitive_steps = psteps; strong = false; memoize_lazy = true; diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fsti b/src/typechecker/FStar.TypeChecker.Cfg.fsti index 260d9109cc8..398d017f00e 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fsti +++ b/src/typechecker/FStar.TypeChecker.Cfg.fsti @@ -101,6 +101,9 @@ type cfg = { tcenv: Env.env; debug: debug_switches; delta_level: list Env.delta_level; // Controls how much unfolding of definitions should be performed + unfold_strict_fvs : bool; + // ^ Determines whether we should unconditionally unfold @@strict_on_arguments defns, + // ignoring the attribute. Used by the unifier. primitive_steps:BU.psmap primitive_step; strong : bool; // under a binder memoize_lazy : bool; diff --git a/src/typechecker/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti index 0ef5395c6de..af5fcb1b442 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fsti +++ b/src/typechecker/FStar.TypeChecker.Env.fsti @@ -45,6 +45,11 @@ type step = | UnfoldQual of list string | UnfoldNamespace of list string | UnfoldTac + // ^ Prevents unfolding of anything marked @@"tac_opaque", which are mostly + // the logical connectives. + | UnfoldStrict + // ^ Determines whether we should unconditionally unfold @@strict_on_arguments defns, + // ignoring the attribute. Used by the unifier. | PureSubtermsWithinComputations | Simplify //Simplifies some basic logical tautologies: not part of definitional equality! | EraseUniverses diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index c42933eddf7..4e4af39fdac 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -964,7 +964,7 @@ let should_unfold cfg strict_ok should_reify fv qninfo : should_unfold_res = // If this definition is marked strict_on_arguments, we will not // unfold standalone occurrences of it, only applications that // pass the strictness check. - | _ when not strict_ok && Some? (Env.fv_has_strict_args cfg.tcenv fv) -> + | _ when not strict_ok && Some? (Env.fv_has_strict_args cfg.tcenv fv) && not cfg.unfold_strict_fvs -> log_unfolding cfg (fun () -> BU.print_string " >> Not unfolding strict_on_arguments definition\n"); no @@ -1471,6 +1471,9 @@ let rec norm : cfg -> env -> stack -> term -> term = log cfg (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args)); norm cfg env stack head in + if cfg.unfold_strict_fvs then + fallback () + else let head_fv_us_opt = let head = U.unascribe head in let head = SS.compress head in diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index fee7239fe89..d8439e0aee5 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -1344,6 +1344,7 @@ let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) = | Some _ -> let basic_steps = [Env.UnfoldUntil delta_constant; + Env.UnfoldStrict; Env.Weak; Env.HNF; Env.Primops; From 78e4d9facc73f7b0bd06290a59a875f3de072e5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 24 Oct 2023 08:11:30 -0700 Subject: [PATCH 5/7] Update example --- examples/typeclasses/Inlining.fst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/examples/typeclasses/Inlining.fst b/examples/typeclasses/Inlining.fst index 59f5a1437f2..75eeedd4a4d 100644 --- a/examples/typeclasses/Inlining.fst +++ b/examples/typeclasses/Inlining.fst @@ -39,8 +39,11 @@ let elem' #a {|d : inhab a|} = [@@ tcnorm] instance inhab_unit : inhab unit = { elem = fun () -> admit #unit () } -(* This will only succeed if the found instance is inlined, sa +(* This will only succeed if the found instance is inlined, as * can be seen from the failure if one uses --tcnorm false *) +(* This now fails, since we don't unfold methods between phases, so the + * verification happens over the interface and not the definitions. *) +[@@expect_failure] let f (u:unit) = let t = elem' #unit () in assert (forall y. y == 1) From 34dceb74ebb84b55a942da940f4da7b5e351d974 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 3 Nov 2023 11:48:35 -0700 Subject: [PATCH 6/7] Add some tests --- examples/typeclasses/Add.fst | 1 + .../StrictArgsUnfoldTest1.fst | 30 +++++++ tests/micro-benchmarks/TCUnivs.fst | 79 +++++++++++++++++++ tests/micro-benchmarks/Test.Integers.fst | 7 ++ tests/micro-benchmarks/UnifyStrictArgs.fst | 26 ++++++ 5 files changed, 143 insertions(+) create mode 100644 tests/micro-benchmarks/StrictArgsUnfoldTest1.fst create mode 100644 tests/micro-benchmarks/TCUnivs.fst create mode 100644 tests/micro-benchmarks/UnifyStrictArgs.fst diff --git a/examples/typeclasses/Add.fst b/examples/typeclasses/Add.fst index 636cad9ee4a..40e924201a0 100644 --- a/examples/typeclasses/Add.fst +++ b/examples/typeclasses/Add.fst @@ -62,3 +62,4 @@ let _ = assert (plus 1 2 = 3) let _ = assert (plus false false = false) let _ = assert (plus true false = true) let _ = assert (plus [1] [2] = [1;2]) +let test #a (x y : a) = assert (plus [x] [y] == [x;y]) diff --git a/tests/micro-benchmarks/StrictArgsUnfoldTest1.fst b/tests/micro-benchmarks/StrictArgsUnfoldTest1.fst new file mode 100644 index 00000000000..b41ebe0c2fb --- /dev/null +++ b/tests/micro-benchmarks/StrictArgsUnfoldTest1.fst @@ -0,0 +1,30 @@ +module StrictArgsUnfoldTest1 + +noeq +type ordered (a:eqtype) = +{ + leq : a -> a -> bool; +} + +[@@strict_on_arguments_unfold [1]] +let leq #a (d : ordered a) : a -> a -> bool = d.leq + +let transitivity #a (d : ordered a) (x y z: a): + Lemma (requires leq d x y /\ leq d y z) + (ensures leq d x z) += admit() // p.properties + +let rec lower_bounded #a (d : ordered a) (l: list a) m: GTot bool = + match l with + | [] -> true + | t::q -> leq d m t && lower_bounded d q m + +(* Used to fail with: + Failure("Impossible: locally nameless; got t#6") +*) +let rec lower_bounded_trans #a (d : ordered a) (l: list a) m1 m2: + Lemma (requires lower_bounded d l m1 /\ leq d m2 m1) + (ensures lower_bounded d l m2) += match l with + | [] -> () + | t::q -> (transitivity d m2 m1 t; lower_bounded_trans d q m1 m2) diff --git a/tests/micro-benchmarks/TCUnivs.fst b/tests/micro-benchmarks/TCUnivs.fst new file mode 100644 index 00000000000..d3130962c5d --- /dev/null +++ b/tests/micro-benchmarks/TCUnivs.fst @@ -0,0 +1,79 @@ +module TCUnivs + +(* This caused a very hard to find failure in the normalizer due to +pushing un-evaluated universe arguments on the stack. It is a +shrunk down version of TypeclassesAlt3 from the book, but I'm keeping +a copy here just in case. -- Guido 2023/11/03 *) + +module TC = FStar.Tactics.Typeclasses + +class bounded_unsigned_int (a:Type) = { + bound : a; + as_nat : a -> nat; + from_nat : (x:nat { x <= as_nat bound }) -> a; +} + +let fits #a {| bounded_unsigned_int a |} + (op: int -> int -> int) + (x y:a) + : prop + = 0 <= op (as_nat x) (as_nat y) /\ + op (as_nat x) (as_nat y) <= as_nat #a bound + +let related_ops #a {| bounded_unsigned_int a |} + (iop: int -> int -> int) + (bop: (x:a -> y:a { fits iop x y } -> a)) + = forall (x y:a). fits iop x y ==> as_nat (bop x y) = as_nat x `iop` as_nat y + +class bounded_unsigned_int_ops (a:Type) = { + base : bounded_unsigned_int a; + add : (x:a -> y:a { fits ( + ) x y } -> a); + sub : (x:a -> y:a { fits op_Subtraction x y } -> a); + lt : (a -> a -> bool); +} + +instance ops_base #a {| d : bounded_unsigned_int_ops a |} + : bounded_unsigned_int a + = d.base + +let ( <=^ ) #a {| bounded_unsigned_int_ops a |} (x y : a) + : bool + = true + +module U32 = FStar.UInt32 +instance u32_instance_base : bounded_unsigned_int U32.t = + let open U32 in + { + bound = 0xfffffffful; + as_nat = v; + from_nat = uint_to_t; +} + +instance u32_instance_ops : bounded_unsigned_int_ops U32.t = + let open U32 in + { + base = u32_instance_base; + add = (fun x y -> add x y); + sub = (fun x y -> sub x y); + lt = (fun x y -> lt x y); + } + +module L = FStar.List.Tot +let sum #a (d : bounded_unsigned_int_ops a ) + (l:list a) (acc:a) + : option a + = admit(); + L.fold_right + (fun (x:a) (acc:option a) -> + match acc with + | None -> None + | Some y -> + if x <=^ bound `sub` y + then Some (x `add` y) + else None) + l + (Some acc) + +let testsum32' : unit = + let x = sum #U32.t u32_instance_ops [0x1ul] 0x00ul in + assert_norm (Some? x) diff --git a/tests/micro-benchmarks/Test.Integers.fst b/tests/micro-benchmarks/Test.Integers.fst index e8a5b130cfe..842cf4f0d03 100644 --- a/tests/micro-benchmarks/Test.Integers.fst +++ b/tests/micro-benchmarks/Test.Integers.fst @@ -173,3 +173,10 @@ let g5 = f1 () /// problem instance, we commit to it immediately even if the chosen /// solution is incompatible with other problems that may be in scope; /// global backtracking is too expensive and unpredictable. + +(* A test to check that we can prove that FStar.Integers.int +is equal to Prims.int with just the unifier. *) +#push-options "--no_smt" +let mk_option_int () : option int + = (); Some #int 5 +#pop-options diff --git a/tests/micro-benchmarks/UnifyStrictArgs.fst b/tests/micro-benchmarks/UnifyStrictArgs.fst new file mode 100644 index 00000000000..ea36f9ac322 --- /dev/null +++ b/tests/micro-benchmarks/UnifyStrictArgs.fst @@ -0,0 +1,26 @@ +module UnifyStrictArgs + +open FStar.Tactics + +type t (k:int) = | Mk of (x:int{x > k}) + +[@@strict_on_arguments [1]] +let f1 k (x:t k) : int = match x with | Mk n -> n + +let f2 k (x:t k) : int = match x with | Mk n -> n + +[@@strict_on_arguments [1]; tcnorm] +let f3 k (x:t k) : int = match x with | Mk n -> n + +[@@strict_on_arguments_unfold [1]; tcnorm] +let f4 k (x:t k) : int = match x with | Mk n -> n + +let _ = assert True by begin + if not (unify (`f1 _) (`f2 42)) then fail "1"; + if not (unify (`f1 _) (`f3 42)) then fail "2"; + if not (unify (`f1 _) (`f4 42)) then fail "3"; + if not (unify (`f2 _) (`f3 42)) then fail "4"; + if not (unify (`f2 _) (`f4 42)) then fail "5"; + if not (unify (`f3 _) (`f4 42)) then fail "6"; + () +end From 4a55315ddc9f316dd1a3e0fed3acad56283fa9c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 14 Nov 2023 11:55:48 -0800 Subject: [PATCH 7/7] snap --- .../fstar-lib/generated/FStar_Parser_Const.ml | 2 + .../generated/FStar_TypeChecker_Cfg.ml | 61 +- .../generated/FStar_TypeChecker_Env.ml | 32 +- .../generated/FStar_TypeChecker_NBE.ml | 12 +- .../generated/FStar_TypeChecker_Normalize.ml | 2386 ++++++++++------- .../generated/FStar_TypeChecker_Rel.ml | 25 +- .../generated/FStar_TypeChecker_TcTerm.ml | 6 +- 7 files changed, 1440 insertions(+), 1084 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index 53daf28a3a2..ed7eaa866fa 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -292,6 +292,8 @@ let (must_erase_for_extraction_attr : FStar_Ident.lident) = psconst "must_erase_for_extraction" let (strict_on_arguments_attr : FStar_Ident.lident) = p2l ["FStar"; "Pervasives"; "strict_on_arguments"] +let (strict_on_arguments_unfold_attr : FStar_Ident.lident) = + p2l ["FStar"; "Pervasives"; "strict_on_arguments_unfold"] let (resolve_implicits_attr_string : Prims.string) = "FStar.Pervasives.resolve_implicits" let (override_resolve_implicits_handler_lid : FStar_Ident.lident) = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml index 3e34844714b..3ab4b4dda81 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml @@ -991,6 +991,7 @@ let (fstep_add_one : FStar_TypeChecker_Env.step -> fsteps -> fsteps) = for_extraction = (fs.for_extraction); unrefine = (fs.unrefine) } + | FStar_TypeChecker_Env.UnfoldStrict -> fs | FStar_TypeChecker_Env.UnfoldOnly lids -> { beta = (fs.beta); @@ -1772,6 +1773,7 @@ type cfg = tcenv: FStar_TypeChecker_Env.env ; debug: debug_switches ; delta_level: FStar_TypeChecker_Env.delta_level Prims.list ; + unfold_strict_fvs: Prims.bool ; primitive_steps: FStar_TypeChecker_Primops.primitive_step FStar_Compiler_Util.psmap ; strong: Prims.bool ; @@ -1782,65 +1784,71 @@ type cfg = let (__proj__Mkcfg__item__steps : cfg -> fsteps) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> steps let (__proj__Mkcfg__item__tcenv : cfg -> FStar_TypeChecker_Env.env) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> tcenv let (__proj__Mkcfg__item__debug : cfg -> debug_switches) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> debug let (__proj__Mkcfg__item__delta_level : cfg -> FStar_TypeChecker_Env.delta_level Prims.list) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> delta_level +let (__proj__Mkcfg__item__unfold_strict_fvs : cfg -> Prims.bool) = + fun projectee -> + match projectee with + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; + compat_memo_ignore_cfg;_} -> unfold_strict_fvs let (__proj__Mkcfg__item__primitive_steps : cfg -> FStar_TypeChecker_Primops.primitive_step FStar_Compiler_Util.psmap) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> primitive_steps let (__proj__Mkcfg__item__strong : cfg -> Prims.bool) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> strong let (__proj__Mkcfg__item__memoize_lazy : cfg -> Prims.bool) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> memoize_lazy let (__proj__Mkcfg__item__normalize_pure_lets : cfg -> Prims.bool) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> normalize_pure_lets let (__proj__Mkcfg__item__reifying : cfg -> Prims.bool) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> reifying let (__proj__Mkcfg__item__compat_memo_ignore_cfg : cfg -> Prims.bool) = fun projectee -> match projectee with - | { steps; tcenv; debug; delta_level; primitive_steps; strong; - memoize_lazy; normalize_pure_lets; reifying; + | { steps; tcenv; debug; delta_level; unfold_strict_fvs; primitive_steps; + strong; memoize_lazy; normalize_pure_lets; reifying; compat_memo_ignore_cfg;_} -> compat_memo_ignore_cfg type prim_step_set = FStar_TypeChecker_Primops.primitive_step FStar_Compiler_Util.psmap @@ -1876,8 +1884,15 @@ let (cfg_to_string : cfg -> Prims.string) = let uu___1 = let uu___2 = let uu___3 = steps_to_string cfg1.steps in - FStar_Compiler_Util.format1 " steps = %s" uu___3 in - [uu___2; "}"] in + FStar_Compiler_Util.format1 " steps = %s;" uu___3 in + let uu___3 = + let uu___4 = + let uu___5 = + (FStar_Common.string_of_list ()) + FStar_TypeChecker_Env.string_of_delta_level cfg1.delta_level in + FStar_Compiler_Util.format1 " delta_level = %s;" uu___5 in + [uu___4; "}"] in + uu___2 :: uu___3 in "{" :: uu___1 in FStar_String.concat "\n" uu___ let (cfg_env : cfg -> FStar_TypeChecker_Env.env) = fun cfg1 -> cfg1.tcenv @@ -2147,6 +2162,8 @@ let (config' : tcenv = e; debug = uu___; delta_level = d1; + unfold_strict_fvs = + (FStar_Compiler_List.mem FStar_TypeChecker_Env.UnfoldStrict s); primitive_steps = psteps1; strong = false; memoize_lazy = true; diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 532ebec7589..f4e9537d0a4 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -18,6 +18,7 @@ type step = | UnfoldQual of Prims.string Prims.list | UnfoldNamespace of Prims.string Prims.list | UnfoldTac + | UnfoldStrict | PureSubtermsWithinComputations | Simplify | EraseUniverses @@ -90,6 +91,9 @@ let (__proj__UnfoldNamespace__item___0 : step -> Prims.string Prims.list) = fun projectee -> match projectee with | UnfoldNamespace _0 -> _0 let (uu___is_UnfoldTac : step -> Prims.bool) = fun projectee -> match projectee with | UnfoldTac -> true | uu___ -> false +let (uu___is_UnfoldStrict : step -> Prims.bool) = + fun projectee -> + match projectee with | UnfoldStrict -> true | uu___ -> false let (uu___is_PureSubtermsWithinComputations : step -> Prims.bool) = fun projectee -> match projectee with @@ -352,7 +356,7 @@ and env = env -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term ; strict_args_tab: - Prims.int Prims.list FStar_Pervasives_Native.option + (Prims.bool * Prims.int Prims.list) FStar_Pervasives_Native.option FStar_Compiler_Util.smap ; erasable_types_tab: Prims.bool FStar_Compiler_Util.smap ; @@ -1231,7 +1235,7 @@ let (__proj__Mkenv__item__nbe : unif_allow_ref_guards; erase_erasable_args; core_check;_} -> nbe let (__proj__Mkenv__item__strict_args_tab : env -> - Prims.int Prims.list FStar_Pervasives_Native.option + (Prims.bool * Prims.int Prims.list) FStar_Pervasives_Native.option FStar_Compiler_Util.smap) = fun projectee -> @@ -3833,7 +3837,7 @@ let (fv_has_erasable_attr : env -> FStar_Syntax_Syntax.fv -> Prims.bool) = let (fv_has_strict_args : env -> FStar_Syntax_Syntax.fv -> - Prims.int Prims.list FStar_Pervasives_Native.option) + (Prims.bool * Prims.int Prims.list) FStar_Pervasives_Native.option) = fun env1 -> fun fv -> @@ -3852,7 +3856,27 @@ let (fv_has_strict_args : FStar_ToSyntax_ToSyntax.parse_attr_with_list false x FStar_Parser_Const.strict_on_arguments_attr in FStar_Pervasives_Native.fst uu___1) in - (true, res) in + if FStar_Pervasives_Native.uu___is_Some res + then + (true, + (FStar_Pervasives_Native.Some + (false, + (FStar_Pervasives_Native.__proj__Some__item__v res)))) + else + (let res1 = + FStar_Compiler_Util.find_map attrs1 + (fun x -> + let uu___2 = + FStar_ToSyntax_ToSyntax.parse_attr_with_list false x + FStar_Parser_Const.strict_on_arguments_unfold_attr in + FStar_Pervasives_Native.fst uu___2) in + if FStar_Pervasives_Native.uu___is_Some res1 + then + (true, + (FStar_Pervasives_Native.Some + (true, + (FStar_Pervasives_Native.__proj__Some__item__v res1)))) + else (true, FStar_Pervasives_Native.None)) in cache_in_fv_tab env1.strict_args_tab fv f let (try_lookup_effect_lid : env -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml index 22ca4d5d5bd..106af7b83c3 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBE.ml @@ -112,6 +112,8 @@ let (reifying_false : config -> config) = FStar_TypeChecker_Cfg.debug = (uu___.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (uu___.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (uu___.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (uu___.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -137,6 +139,8 @@ let (reifying_true : config -> config) = FStar_TypeChecker_Cfg.debug = (uu___.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (uu___.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (uu___.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (uu___.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -225,6 +229,8 @@ let (zeta_false : config -> config) = (cfg_core.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg_core.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg_core.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg_core.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -1719,7 +1725,7 @@ and (translate_fv : then FStar_TypeChecker_NBETerm.mkConstruct fvar [] [] else (let uu___2 = - FStar_TypeChecker_Normalize.should_unfold cfg.core_cfg + FStar_TypeChecker_Normalize.should_unfold cfg.core_cfg false (fun uu___3 -> (cfg.core_cfg).FStar_TypeChecker_Cfg.reifying) fvar qninfo in match uu___2 with @@ -3347,6 +3353,8 @@ let (normalize : FStar_TypeChecker_Cfg.debug = (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -3459,6 +3467,8 @@ let (normalize_for_unit_test : FStar_TypeChecker_Cfg.debug = (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = (cfg.FStar_TypeChecker_Cfg.strong); diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index 4287f04d5a1..de31b1d634c 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -232,7 +232,11 @@ let (closure_to_string : closure -> Prims.string) = FStar_Compiler_Util.string_of_int in let uu___4 = FStar_Syntax_Print.term_to_string t in FStar_Compiler_Util.format2 "(env=%s elts; %s)" uu___3 uu___4 - | Univ uu___1 -> "Univ" + | Univ u -> + let uu___1 = + let uu___2 = FStar_Syntax_Print.univ_to_string u in + FStar_String.op_Hat uu___2 ")" in + FStar_String.op_Hat "Univ (" uu___1 | Dummy -> "dummy" let (env_to_string : (FStar_Syntax_Syntax.binder FStar_Pervasives_Native.option * closure) @@ -264,7 +268,11 @@ let (stack_elt_to_string : stack_elt -> Prims.string) = FStar_Compiler_Effect.op_Less_Bar FStar_Compiler_Util.string_of_int (FStar_Compiler_List.length bs) in FStar_Compiler_Util.format1 "Abs %s" uu___5 - | UnivArgs uu___1 -> "UnivArgs" + | UnivArgs (us, uu___1) -> + let uu___2 = + let uu___3 = FStar_Syntax_Print.univs_to_string us in + FStar_String.op_Hat uu___3 ")" in + FStar_String.op_Hat "UnivArgs (" uu___2 | Match uu___1 -> "Match" | App (uu___1, t, uu___2, uu___3) -> let uu___4 = FStar_Syntax_Print.term_to_string t in @@ -352,48 +360,59 @@ let (norm_universe : let u2 = FStar_Syntax_Subst.compress_univ u1 in match u2 with | FStar_Syntax_Syntax.U_bvar x -> - (try - (fun uu___ -> - match () with - | () -> - let uu___1 = - let uu___2 = FStar_Compiler_List.nth env1 x in - FStar_Pervasives_Native.snd uu___2 in - (match uu___1 with - | Univ u3 -> - ((let uu___3 = - FStar_Compiler_Effect.op_Less_Bar - (FStar_TypeChecker_Env.debug - cfg.FStar_TypeChecker_Cfg.tcenv) - (FStar_Options.Other "univ_norm") in - if uu___3 - then - let uu___4 = - FStar_Syntax_Print.univ_to_string u3 in - FStar_Compiler_Util.print1 - "Univ (in norm_universe): %s\n" uu___4 - else ()); - aux u3) - | Dummy -> [u2] - | uu___2 -> - let uu___3 = - let uu___4 = - FStar_Compiler_Util.string_of_int x in - FStar_Compiler_Util.format1 - "Impossible: universe variable u@%s bound to a term" - uu___4 in - failwith uu___3)) () - with - | uu___1 -> + let vo = + try + (fun uu___ -> + match () with + | () -> + let uu___1 = + let uu___2 = FStar_Compiler_List.nth env1 x in + FStar_Pervasives_Native.snd uu___2 in + FStar_Pervasives_Native.Some uu___1) () + with | uu___1 -> FStar_Pervasives_Native.None in + (match vo with + | FStar_Pervasives_Native.Some (Univ u3) -> + ((let uu___1 = + FStar_Compiler_Effect.op_Less_Bar + (FStar_TypeChecker_Env.debug + cfg.FStar_TypeChecker_Cfg.tcenv) + (FStar_Options.Other "univ_norm") in + if uu___1 + then + let uu___2 = FStar_Syntax_Print.univ_to_string u3 in + FStar_Compiler_Util.print1 + "Univ (in norm_universe): %s\n" uu___2 + else ()); + aux u3) + | FStar_Pervasives_Native.Some (Dummy) -> [u2] + | FStar_Pervasives_Native.Some uu___ -> if (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.allow_unbound_universes then [FStar_Syntax_Syntax.U_unknown] else - (let uu___3 = - let uu___4 = FStar_Compiler_Util.string_of_int x in + (let uu___2 = + let uu___3 = FStar_Compiler_Util.string_of_int x in + FStar_Compiler_Util.format1 + "Impossible: universe variable u@%s bound to a term" + uu___3 in + failwith uu___2) + | FStar_Pervasives_Native.None -> + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.allow_unbound_universes + then [FStar_Syntax_Syntax.U_unknown] + else + (let uu___1 = + let uu___2 = + let uu___3 = FStar_Compiler_Util.string_of_int x in + let uu___4 = + let uu___5 = + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length env1) in + FStar_String.op_Hat " -- " uu___5 in + FStar_String.op_Hat uu___3 uu___4 in FStar_String.op_Hat "Universe variable not found: u@" - uu___4 in - failwith uu___3)) + uu___2 in + failwith uu___1)) | FStar_Syntax_Syntax.U_unif uu___ when (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.check_no_uvars -> [FStar_Syntax_Syntax.U_zero] @@ -1659,6 +1678,8 @@ let (reduce_equality : FStar_TypeChecker_Cfg.debug = (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = FStar_TypeChecker_Cfg.equality_ops; FStar_TypeChecker_Cfg.strong = (cfg.FStar_TypeChecker_Cfg.strong); @@ -1989,936 +2010,981 @@ let (plugin_unfold_warn_ctr : Prims.int FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref Prims.int_zero let (should_unfold : FStar_TypeChecker_Cfg.cfg -> - (FStar_TypeChecker_Cfg.cfg -> Prims.bool) -> - FStar_Syntax_Syntax.fv -> - FStar_TypeChecker_Env.qninfo -> should_unfold_res) + Prims.bool -> + (FStar_TypeChecker_Cfg.cfg -> Prims.bool) -> + FStar_Syntax_Syntax.fv -> + FStar_TypeChecker_Env.qninfo -> should_unfold_res) = fun cfg -> - fun should_reify1 -> - fun fv -> - fun qninfo -> - let attrs = - let uu___ = FStar_TypeChecker_Env.attrs_of_qninfo qninfo in - match uu___ with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some ats -> ats in - let quals = - let uu___ = FStar_TypeChecker_Env.quals_of_qninfo qninfo in - match uu___ with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some quals1 -> quals1 in - let yes = (true, false, false) in - let no = (false, false, false) in - let fully = (true, true, false) in - let reif = (true, false, true) in - let yesno b = if b then yes else no in - let fullyno b = if b then fully else no in - let comb_or l = - FStar_Compiler_List.fold_right - (fun uu___ -> - fun uu___1 -> - match (uu___, uu___1) with - | ((a, b, c), (x, y, z)) -> ((a || x), (b || y), (c || z))) - l (false, false, false) in - let string_of_res uu___ = - match uu___ with - | (x, y, z) -> - let uu___1 = FStar_Compiler_Util.string_of_bool x in - let uu___2 = FStar_Compiler_Util.string_of_bool y in - let uu___3 = FStar_Compiler_Util.string_of_bool z in - FStar_Compiler_Util.format3 "(%s,%s,%s)" uu___1 uu___2 uu___3 in - let default_unfolding uu___ = - FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.fv_to_string fv in - let uu___4 = + fun strict_ok -> + fun should_reify1 -> + fun fv -> + fun qninfo -> + let attrs = + let uu___ = FStar_TypeChecker_Env.attrs_of_qninfo qninfo in + match uu___ with + | FStar_Pervasives_Native.None -> [] + | FStar_Pervasives_Native.Some ats -> ats in + let quals = + let uu___ = FStar_TypeChecker_Env.quals_of_qninfo qninfo in + match uu___ with + | FStar_Pervasives_Native.None -> [] + | FStar_Pervasives_Native.Some quals1 -> quals1 in + let yes = (true, false, false) in + let no = (false, false, false) in + let fully = (true, true, false) in + let reif = (true, false, true) in + let yesno b = if b then yes else no in + let fullyno b = if b then fully else no in + let comb_or l = + FStar_Compiler_List.fold_right + (fun uu___ -> + fun uu___1 -> + match (uu___, uu___1) with + | ((a, b, c), (x, y, z)) -> + ((a || x), (b || y), (c || z))) l + (false, false, false) in + let string_of_res uu___ = + match uu___ with + | (x, y, z) -> + let uu___1 = FStar_Compiler_Util.string_of_bool x in + let uu___2 = FStar_Compiler_Util.string_of_bool y in + let uu___3 = FStar_Compiler_Util.string_of_bool z in + FStar_Compiler_Util.format3 "(%s,%s,%s)" uu___1 uu___2 + uu___3 in + let default_unfolding uu___ = + FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___2 -> + let uu___3 = FStar_Syntax_Print.fv_to_string fv in + let uu___4 = + let uu___5 = + FStar_TypeChecker_Env.delta_depth_of_fv + cfg.FStar_TypeChecker_Cfg.tcenv fv in + FStar_Syntax_Print.delta_depth_to_string uu___5 in let uu___5 = - FStar_TypeChecker_Env.delta_depth_of_fv - cfg.FStar_TypeChecker_Cfg.tcenv fv in - FStar_Syntax_Print.delta_depth_to_string uu___5 in - let uu___5 = - (FStar_Common.string_of_list ()) - FStar_TypeChecker_Env.string_of_delta_level - cfg.FStar_TypeChecker_Cfg.delta_level in - FStar_Compiler_Util.print3 - "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n" - uu___3 uu___4 uu___5); - (let uu___2 = - FStar_Compiler_Effect.op_Bar_Greater - cfg.FStar_TypeChecker_Cfg.delta_level - (FStar_Compiler_Util.for_some - (fun uu___3 -> - match uu___3 with - | FStar_TypeChecker_Env.NoDelta -> false - | FStar_TypeChecker_Env.InliningDelta -> true - | FStar_TypeChecker_Env.Eager_unfolding_only -> true - | FStar_TypeChecker_Env.Unfold l -> - let uu___4 = - FStar_TypeChecker_Env.delta_depth_of_fv - cfg.FStar_TypeChecker_Cfg.tcenv fv in - FStar_TypeChecker_Common.delta_depth_greater_than - uu___4 l)) in - FStar_Compiler_Effect.op_Less_Bar yesno uu___2) in - let res = - if FStar_TypeChecker_Env.qninfo_is_action qninfo - then - let b = should_reify1 cfg in - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___1 -> - let uu___2 = FStar_Syntax_Print.fv_to_string fv in - let uu___3 = FStar_Compiler_Util.string_of_bool b in - FStar_Compiler_Util.print2 - "should_unfold: For DM4F action %s, should_reify = %s\n" - uu___2 uu___3); - if b then reif else no) - else - if - (let uu___ = FStar_TypeChecker_Cfg.find_prim_step cfg fv in - FStar_Compiler_Option.isSome uu___) + (FStar_Common.string_of_list ()) + FStar_TypeChecker_Env.string_of_delta_level + cfg.FStar_TypeChecker_Cfg.delta_level in + FStar_Compiler_Util.print3 + "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n" + uu___3 uu___4 uu___5); + (let uu___2 = + FStar_Compiler_Effect.op_Bar_Greater + cfg.FStar_TypeChecker_Cfg.delta_level + (FStar_Compiler_Util.for_some + (fun uu___3 -> + match uu___3 with + | FStar_TypeChecker_Env.NoDelta -> false + | FStar_TypeChecker_Env.InliningDelta -> true + | FStar_TypeChecker_Env.Eager_unfolding_only -> true + | FStar_TypeChecker_Env.Unfold l -> + let uu___4 = + FStar_TypeChecker_Env.delta_depth_of_fv + cfg.FStar_TypeChecker_Cfg.tcenv fv in + FStar_TypeChecker_Common.delta_depth_greater_than + uu___4 l)) in + FStar_Compiler_Effect.op_Less_Bar yesno uu___2) in + let res = + if FStar_TypeChecker_Env.qninfo_is_action qninfo then + let b = should_reify1 cfg in (FStar_TypeChecker_Cfg.log_unfolding cfg (fun uu___1 -> - FStar_Compiler_Util.print_string - " >> It's a primop, not unfolding\n"); - no) + let uu___2 = FStar_Syntax_Print.fv_to_string fv in + let uu___3 = FStar_Compiler_Util.string_of_bool b in + FStar_Compiler_Util.print2 + "should_unfold: For DM4F action %s, should_reify = %s\n" + uu___2 uu___3); + if b then reif else no) else - (match (qninfo, - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual), - ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace)) - with - | (FStar_Pervasives_Native.Some - (FStar_Pervasives.Inr - ({ - FStar_Syntax_Syntax.sigel = - FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); - FStar_Syntax_Syntax.lids1 = uu___1;_}; - FStar_Syntax_Syntax.sigrng = uu___2; - FStar_Syntax_Syntax.sigquals = qs; - FStar_Syntax_Syntax.sigmeta = uu___3; - FStar_Syntax_Syntax.sigattrs = uu___4; - FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; - FStar_Syntax_Syntax.sigopts = uu___6;_}, - uu___7), - uu___8), - uu___9, uu___10, uu___11, uu___12, uu___13) when - FStar_Compiler_List.contains - FStar_Syntax_Syntax.HasMaskedEffect qs - -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___15 -> - FStar_Compiler_Util.print_string - " >> HasMaskedEffect, not unfolding\n"); - no) - | (FStar_Pervasives_Native.Some - (FStar_Pervasives.Inr - ({ - FStar_Syntax_Syntax.sigel = - FStar_Syntax_Syntax.Sig_let - { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); - FStar_Syntax_Syntax.lids1 = uu___1;_}; - FStar_Syntax_Syntax.sigrng = uu___2; - FStar_Syntax_Syntax.sigquals = qs; - FStar_Syntax_Syntax.sigmeta = uu___3; - FStar_Syntax_Syntax.sigattrs = uu___4; - FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; - FStar_Syntax_Syntax.sigopts = uu___6;_}, - uu___7), - uu___8), - uu___9, uu___10, uu___11, uu___12, uu___13) when - (is_rec && - (Prims.op_Negation - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta)) - && - (Prims.op_Negation - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta_full) - -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___15 -> - FStar_Compiler_Util.print_string - " >> It's a recursive definition but we're not doing Zeta, not unfolding\n"); - no) - | (uu___, FStar_Pervasives_Native.Some uu___1, uu___2, - uu___3, uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + if + ((Prims.op_Negation strict_ok) && + (let uu___ = + FStar_TypeChecker_Env.fv_has_strict_args + cfg.FStar_TypeChecker_Cfg.tcenv fv in + FStar_Pervasives_Native.uu___is_Some uu___)) + && + (Prims.op_Negation + cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs) + then + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___1 -> + FStar_Compiler_Util.print_string + " >> Not unfolding strict_on_arguments definition\n"); + no) + else + if + (let uu___ = FStar_TypeChecker_Cfg.find_prim_step cfg fv in + FStar_Compiler_Option.isSome uu___) + then + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___1 -> + FStar_Compiler_Util.print_string + " >> It's a primop, not unfolding\n"); + no) + else + (match (qninfo, + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual), + ((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace)) + with + | (FStar_Pervasives_Native.Some + (FStar_Pervasives.Inr + ({ + FStar_Syntax_Syntax.sigel = + FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); + FStar_Syntax_Syntax.lids1 = uu___1;_}; + FStar_Syntax_Syntax.sigrng = uu___2; + FStar_Syntax_Syntax.sigquals = qs; + FStar_Syntax_Syntax.sigmeta = uu___3; + FStar_Syntax_Syntax.sigattrs = uu___4; + FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; + FStar_Syntax_Syntax.sigopts = uu___6;_}, + uu___7), + uu___8), + uu___9, uu___10, uu___11, uu___12, uu___13) when + FStar_Compiler_List.contains + FStar_Syntax_Syntax.HasMaskedEffect qs + -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___15 -> + FStar_Compiler_Util.print_string + " >> HasMaskedEffect, not unfolding\n"); + no) + | (FStar_Pervasives_Native.Some + (FStar_Pervasives.Inr + ({ + FStar_Syntax_Syntax.sigel = + FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (is_rec, uu___); + FStar_Syntax_Syntax.lids1 = uu___1;_}; + FStar_Syntax_Syntax.sigrng = uu___2; + FStar_Syntax_Syntax.sigquals = qs; + FStar_Syntax_Syntax.sigmeta = uu___3; + FStar_Syntax_Syntax.sigattrs = uu___4; + FStar_Syntax_Syntax.sigopens_and_abbrevs = uu___5; + FStar_Syntax_Syntax.sigopts = uu___6;_}, + uu___7), + uu___8), + uu___9, uu___10, uu___11, uu___12, uu___13) when + (is_rec && + (Prims.op_Negation + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta)) + && + (Prims.op_Negation + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.zeta_full) + -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___15 -> + FStar_Compiler_Util.print_string + " >> It's a recursive definition but we're not doing Zeta, not unfolding\n"); + no) + | (uu___, FStar_Pervasives_Native.Some uu___1, uu___2, + uu___3, uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - let uu___22 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr - uu___22 in - FStar_String.op_Hat - uu___21 "." in - let uu___21 = - FStar_String.op_Hat ns - "." in - FStar_Compiler_Util.starts_with - uu___20 uu___21) - namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, FStar_Pervasives_Native.Some uu___2, - uu___3, uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + let uu___22 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___22 in + FStar_String.op_Hat + uu___21 "." in + let uu___21 = + FStar_String.op_Hat + ns "." in + FStar_Compiler_Util.starts_with + uu___20 uu___21) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, FStar_Pervasives_Native.Some uu___2, + uu___3, uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - let uu___22 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr - uu___22 in - FStar_String.op_Hat - uu___21 "." in - let uu___21 = - FStar_String.op_Hat ns - "." in - FStar_Compiler_Util.starts_with - uu___20 uu___21) - namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, FStar_Pervasives_Native.Some - uu___3, uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + let uu___22 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___22 in + FStar_String.op_Hat + uu___21 "." in + let uu___21 = + FStar_String.op_Hat + ns "." in + FStar_Compiler_Util.starts_with + uu___20 uu___21) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, FStar_Pervasives_Native.Some + uu___3, uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - let uu___22 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr - uu___22 in - FStar_String.op_Hat - uu___21 "." in - let uu___21 = - FStar_String.op_Hat ns - "." in - FStar_Compiler_Util.starts_with - uu___20 uu___21) - namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, uu___3, - FStar_Pervasives_Native.Some uu___4, uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + let uu___22 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___22 in + FStar_String.op_Hat + uu___21 "." in + let uu___21 = + FStar_String.op_Hat + ns "." in + FStar_Compiler_Util.starts_with + uu___20 uu___21) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, uu___3, + FStar_Pervasives_Native.Some uu___4, uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - let uu___22 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr - uu___22 in - FStar_String.op_Hat - uu___21 "." in - let uu___21 = - FStar_String.op_Hat ns - "." in - FStar_Compiler_Util.starts_with - uu___20 uu___21) - namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, uu___3, uu___4, - FStar_Pervasives_Native.Some uu___5) -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - let uu___8 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.print1 - "should_unfold: Reached a %s with selective unfolding\n" - uu___8); - (let meets_some_criterion = - let uu___7 = - let uu___8 = - if - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction - then + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + let uu___22 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___22 in + FStar_String.op_Hat + uu___21 "." in + let uu___21 = + FStar_String.op_Hat + ns "." in + FStar_Compiler_Util.starts_with + uu___20 uu___21) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, uu___3, uu___4, + FStar_Pervasives_Native.Some uu___5) -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + let uu___8 = + FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.print1 + "should_unfold: Reached a %s with selective unfolding\n" + uu___8); + (let meets_some_criterion = + let uu___7 = + let uu___8 = + if + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction + then + let uu___9 = + let uu___10 = + FStar_TypeChecker_Env.lookup_definition_qninfo + [FStar_TypeChecker_Env.Eager_unfolding_only; + FStar_TypeChecker_Env.InliningDelta] + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v + qninfo in + FStar_Compiler_Option.isSome uu___10 in + FStar_Compiler_Effect.op_Less_Bar yesno + uu___9 + else no in let uu___9 = let uu___10 = - FStar_TypeChecker_Env.lookup_definition_qninfo - [FStar_TypeChecker_Env.Eager_unfolding_only; - FStar_TypeChecker_Env.InliningDelta] - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v - qninfo in - FStar_Compiler_Option.isSome uu___10 in - FStar_Compiler_Effect.op_Less_Bar yesno uu___9 - else no in - let uu___9 = - let uu___10 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___11 = - FStar_Compiler_Util.for_some - (FStar_Syntax_Syntax.fv_eq_lid fv) - lids in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___11 in - let uu___11 = - let uu___12 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr - with - | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some lids -> - let uu___13 = - FStar_Compiler_Util.for_some - (fun at -> - FStar_Compiler_Util.for_some - (fun lid -> - FStar_Syntax_Util.is_fvar - lid at) lids) attrs in - FStar_Compiler_Effect.op_Less_Bar yesno - uu___13 in - let uu___13 = - let uu___14 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_only with | FStar_Pervasives_Native.None -> no | FStar_Pervasives_Native.Some lids -> - let uu___15 = + let uu___11 = FStar_Compiler_Util.for_some (FStar_Syntax_Syntax.fv_eq_lid fv) lids in FStar_Compiler_Effect.op_Less_Bar - fullyno uu___15 in - let uu___15 = - let uu___16 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + yesno uu___11 in + let uu___11 = + let uu___12 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_attr with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some qs -> - let uu___17 = + | FStar_Pervasives_Native.Some lids -> + let uu___13 = FStar_Compiler_Util.for_some - (fun q -> + (fun at -> FStar_Compiler_Util.for_some - (fun qual -> - let uu___18 = - FStar_Syntax_Print.qual_to_string - qual in - uu___18 = q) quals) qs in + (fun lid -> + FStar_Syntax_Util.is_fvar + lid at) lids) attrs in FStar_Compiler_Effect.op_Less_Bar - yesno uu___17 in - let uu___17 = - let uu___18 = - match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + yesno uu___13 in + let uu___13 = + let uu___14 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_fully with | FStar_Pervasives_Native.None -> no - | FStar_Pervasives_Native.Some - namespaces -> - let uu___19 = + | FStar_Pervasives_Native.Some lids -> + let uu___15 = FStar_Compiler_Util.for_some - (fun ns -> - let uu___20 = - let uu___21 = - let uu___22 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_Ident.nsstr - uu___22 in - FStar_String.op_Hat - uu___21 "." in - let uu___21 = - FStar_String.op_Hat ns - "." in - FStar_Compiler_Util.starts_with - uu___20 uu___21) - namespaces in + (FStar_Syntax_Syntax.fv_eq_lid + fv) lids in FStar_Compiler_Effect.op_Less_Bar - yesno uu___19 in - [uu___18] in - uu___16 :: uu___17 in - uu___14 :: uu___15 in - uu___12 :: uu___13 in - uu___10 :: uu___11 in - uu___8 :: uu___9 in - comb_or uu___7 in - meets_some_criterion)) - | (uu___, uu___1, uu___2, uu___3, uu___4, uu___5) when - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac - && - (FStar_Compiler_Util.for_some - (FStar_Syntax_Util.attr_eq - FStar_Syntax_Util.tac_opaque_attr) attrs) - -> - (FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___7 -> - FStar_Compiler_Util.print_string - " >> tac_opaque, not unfolding\n"); - no) - | uu___ -> default_unfolding ()) in - FStar_TypeChecker_Cfg.log_unfolding cfg - (fun uu___1 -> - let uu___2 = FStar_Syntax_Print.fv_to_string fv in - let uu___3 = - let uu___4 = FStar_Syntax_Syntax.range_of_fv fv in - FStar_Compiler_Range_Ops.string_of_range uu___4 in - let uu___4 = string_of_res res in - FStar_Compiler_Util.print3 - "should_unfold: For %s (%s), unfolding res = %s\n" uu___2 - uu___3 uu___4); - (let r = - match res with - | (false, uu___1, uu___2) -> Should_unfold_no - | (true, false, false) -> Should_unfold_yes - | (true, true, false) -> Should_unfold_fully - | (true, false, true) -> Should_unfold_reify - | uu___1 -> - let uu___2 = - let uu___3 = string_of_res res in - FStar_Compiler_Util.format1 - "Unexpected unfolding result: %s" uu___3 in - FStar_Compiler_Effect.op_Less_Bar failwith uu___2 in - (let uu___2 = - ((((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac + fullyno uu___15 in + let uu___15 = + let uu___16 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_qual + with + | FStar_Pervasives_Native.None -> no + | FStar_Pervasives_Native.Some qs -> + let uu___17 = + FStar_Compiler_Util.for_some + (fun q -> + FStar_Compiler_Util.for_some + (fun qual -> + let uu___18 = + FStar_Syntax_Print.qual_to_string + qual in + uu___18 = q) quals) + qs in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___17 in + let uu___17 = + let uu___18 = + match (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_namespace + with + | FStar_Pervasives_Native.None -> + no + | FStar_Pervasives_Native.Some + namespaces -> + let uu___19 = + FStar_Compiler_Util.for_some + (fun ns -> + let uu___20 = + let uu___21 = + let uu___22 = + FStar_Syntax_Syntax.lid_of_fv + fv in + FStar_Ident.nsstr + uu___22 in + FStar_String.op_Hat + uu___21 "." in + let uu___21 = + FStar_String.op_Hat + ns "." in + FStar_Compiler_Util.starts_with + uu___20 uu___21) + namespaces in + FStar_Compiler_Effect.op_Less_Bar + yesno uu___19 in + [uu___18] in + uu___16 :: uu___17 in + uu___14 :: uu___15 in + uu___12 :: uu___13 in + uu___10 :: uu___11 in + uu___8 :: uu___9 in + comb_or uu___7 in + meets_some_criterion)) + | (uu___, uu___1, uu___2, uu___3, uu___4, uu___5) when + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac + && + (FStar_Compiler_Util.for_some + (FStar_Syntax_Util.attr_eq + FStar_Syntax_Util.tac_opaque_attr) attrs) + -> + (FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___7 -> + FStar_Compiler_Util.print_string + " >> tac_opaque, not unfolding\n"); + no) + | uu___ -> default_unfolding ()) in + FStar_TypeChecker_Cfg.log_unfolding cfg + (fun uu___1 -> + let uu___2 = FStar_Syntax_Print.fv_to_string fv in + let uu___3 = + let uu___4 = FStar_Syntax_Syntax.range_of_fv fv in + FStar_Compiler_Range_Ops.string_of_range uu___4 in + let uu___4 = string_of_res res in + FStar_Compiler_Util.print3 + "should_unfold: For %s (%s), unfolding res = %s\n" uu___2 + uu___3 uu___4); + (let r = + match res with + | (false, uu___1, uu___2) -> Should_unfold_no + | (true, false, false) -> Should_unfold_yes + | (true, true, false) -> Should_unfold_fully + | (true, false, true) -> Should_unfold_reify + | uu___1 -> + let uu___2 = + let uu___3 = string_of_res res in + FStar_Compiler_Util.format1 + "Unexpected unfolding result: %s" uu___3 in + FStar_Compiler_Effect.op_Less_Bar failwith uu___2 in + (let uu___2 = + ((((cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.unfold_tac + && + (let uu___3 = FStar_Options.no_plugins () in + Prims.op_Negation uu___3)) + && (r <> Should_unfold_no)) && - (let uu___3 = FStar_Options.no_plugins () in - Prims.op_Negation uu___3)) - && (r <> Should_unfold_no)) - && - (FStar_Compiler_Util.for_some - (FStar_Syntax_Util.is_fvar FStar_Parser_Const.plugin_attr) - attrs)) - && - (let uu___3 = - FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in - uu___3 > Prims.int_zero) in - if uu___2 - then - let msg = - let uu___3 = FStar_Syntax_Print.fv_to_string fv in - FStar_Compiler_Util.format1 - "Unfolding name which is marked as a plugin: %s" uu___3 in - (FStar_Errors.log_issue - (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p - (FStar_Errors_Codes.Warning_UnfoldPlugin, msg); - (let uu___4 = - let uu___5 = - FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in - uu___5 - Prims.int_one in - FStar_Compiler_Effect.op_Colon_Equals plugin_unfold_warn_ctr - uu___4)) - else ()); - r) + (FStar_Compiler_Util.for_some + (FStar_Syntax_Util.is_fvar + FStar_Parser_Const.plugin_attr) attrs)) + && + (let uu___3 = + FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in + uu___3 > Prims.int_zero) in + if uu___2 + then + let msg = + let uu___3 = FStar_Syntax_Print.fv_to_string fv in + FStar_Compiler_Util.format1 + "Unfolding name which is marked as a plugin: %s" uu___3 in + (FStar_Errors.log_issue + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.p + (FStar_Errors_Codes.Warning_UnfoldPlugin, msg); + (let uu___4 = + let uu___5 = + FStar_Compiler_Effect.op_Bang plugin_unfold_warn_ctr in + uu___5 - Prims.int_one in + FStar_Compiler_Effect.op_Colon_Equals + plugin_unfold_warn_ctr uu___4)) + else ()); + r) let decide_unfolding : 'uuuuu . FStar_TypeChecker_Cfg.cfg -> - stack_elt Prims.list -> - 'uuuuu -> - FStar_Syntax_Syntax.fv -> - FStar_TypeChecker_Env.qninfo -> - (FStar_TypeChecker_Cfg.cfg * stack_elt Prims.list) - FStar_Pervasives_Native.option + Prims.bool -> + stack_elt Prims.list -> + 'uuuuu -> + FStar_Syntax_Syntax.fv -> + FStar_TypeChecker_Env.qninfo -> + (FStar_TypeChecker_Cfg.cfg * stack_elt Prims.list) + FStar_Pervasives_Native.option = fun cfg -> - fun stack1 -> - fun rng -> - fun fv -> - fun qninfo -> - let res = - should_unfold cfg (fun cfg1 -> should_reify cfg1 stack1) fv - qninfo in - match res with - | Should_unfold_no -> FStar_Pervasives_Native.None - | Should_unfold_yes -> FStar_Pervasives_Native.Some (cfg, stack1) - | Should_unfold_fully -> - let cfg' = - { - FStar_TypeChecker_Cfg.steps = - (let uu___ = cfg.FStar_TypeChecker_Cfg.steps in - { - FStar_TypeChecker_Cfg.beta = - (uu___.FStar_TypeChecker_Cfg.beta); - FStar_TypeChecker_Cfg.iota = - (uu___.FStar_TypeChecker_Cfg.iota); - FStar_TypeChecker_Cfg.zeta = - (uu___.FStar_TypeChecker_Cfg.zeta); - FStar_TypeChecker_Cfg.zeta_full = - (uu___.FStar_TypeChecker_Cfg.zeta_full); - FStar_TypeChecker_Cfg.weak = - (uu___.FStar_TypeChecker_Cfg.weak); - FStar_TypeChecker_Cfg.hnf = - (uu___.FStar_TypeChecker_Cfg.hnf); - FStar_TypeChecker_Cfg.primops = - (uu___.FStar_TypeChecker_Cfg.primops); - FStar_TypeChecker_Cfg.do_not_unfold_pure_lets = - (uu___.FStar_TypeChecker_Cfg.do_not_unfold_pure_lets); - FStar_TypeChecker_Cfg.unfold_until = - (FStar_Pervasives_Native.Some - FStar_Syntax_Syntax.delta_constant); - FStar_TypeChecker_Cfg.unfold_only = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_fully = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_attr = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_qual = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_namespace = - FStar_Pervasives_Native.None; - FStar_TypeChecker_Cfg.unfold_tac = - (uu___.FStar_TypeChecker_Cfg.unfold_tac); - FStar_TypeChecker_Cfg.pure_subterms_within_computations - = - (uu___.FStar_TypeChecker_Cfg.pure_subterms_within_computations); - FStar_TypeChecker_Cfg.simplify = - (uu___.FStar_TypeChecker_Cfg.simplify); - FStar_TypeChecker_Cfg.erase_universes = - (uu___.FStar_TypeChecker_Cfg.erase_universes); - FStar_TypeChecker_Cfg.allow_unbound_universes = - (uu___.FStar_TypeChecker_Cfg.allow_unbound_universes); - FStar_TypeChecker_Cfg.reify_ = - (uu___.FStar_TypeChecker_Cfg.reify_); - FStar_TypeChecker_Cfg.compress_uvars = - (uu___.FStar_TypeChecker_Cfg.compress_uvars); - FStar_TypeChecker_Cfg.no_full_norm = - (uu___.FStar_TypeChecker_Cfg.no_full_norm); - FStar_TypeChecker_Cfg.check_no_uvars = - (uu___.FStar_TypeChecker_Cfg.check_no_uvars); - FStar_TypeChecker_Cfg.unmeta = - (uu___.FStar_TypeChecker_Cfg.unmeta); - FStar_TypeChecker_Cfg.unascribe = - (uu___.FStar_TypeChecker_Cfg.unascribe); - FStar_TypeChecker_Cfg.in_full_norm_request = - (uu___.FStar_TypeChecker_Cfg.in_full_norm_request); - FStar_TypeChecker_Cfg.weakly_reduce_scrutinee = - (uu___.FStar_TypeChecker_Cfg.weakly_reduce_scrutinee); - FStar_TypeChecker_Cfg.nbe_step = - (uu___.FStar_TypeChecker_Cfg.nbe_step); - FStar_TypeChecker_Cfg.for_extraction = - (uu___.FStar_TypeChecker_Cfg.for_extraction); - FStar_TypeChecker_Cfg.unrefine = - (uu___.FStar_TypeChecker_Cfg.unrefine) - }); - FStar_TypeChecker_Cfg.tcenv = - (cfg.FStar_TypeChecker_Cfg.tcenv); - FStar_TypeChecker_Cfg.debug = - (cfg.FStar_TypeChecker_Cfg.debug); - FStar_TypeChecker_Cfg.delta_level = - (cfg.FStar_TypeChecker_Cfg.delta_level); - FStar_TypeChecker_Cfg.primitive_steps = - (cfg.FStar_TypeChecker_Cfg.primitive_steps); - FStar_TypeChecker_Cfg.strong = - (cfg.FStar_TypeChecker_Cfg.strong); - FStar_TypeChecker_Cfg.memoize_lazy = - (cfg.FStar_TypeChecker_Cfg.memoize_lazy); - FStar_TypeChecker_Cfg.normalize_pure_lets = - (cfg.FStar_TypeChecker_Cfg.normalize_pure_lets); - FStar_TypeChecker_Cfg.reifying = - (cfg.FStar_TypeChecker_Cfg.reifying); - FStar_TypeChecker_Cfg.compat_memo_ignore_cfg = - (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg) - } in - let stack' = - match stack1 with - | (UnivArgs (us, r))::stack'1 -> (UnivArgs (us, r)) :: - (Cfg (cfg, FStar_Pervasives_Native.None)) :: stack'1 - | stack'1 -> (Cfg (cfg, FStar_Pervasives_Native.None)) :: - stack'1 in - FStar_Pervasives_Native.Some (cfg', stack') - | Should_unfold_reify -> - let rec push e s = - match s with - | [] -> [e] - | (UnivArgs (us, r))::t -> - let uu___ = push e t in (UnivArgs (us, r)) :: uu___ - | h::t -> e :: h :: t in - let ref = - let uu___ = - let uu___1 = - let uu___2 = FStar_Syntax_Syntax.lid_of_fv fv in - FStar_Const.Const_reflect uu___2 in - FStar_Syntax_Syntax.Tm_constant uu___1 in - FStar_Syntax_Syntax.mk uu___ - FStar_Compiler_Range_Type.dummyRange in - let stack2 = - push - (App - (empty_env, ref, FStar_Pervasives_Native.None, - FStar_Compiler_Range_Type.dummyRange)) stack1 in - FStar_Pervasives_Native.Some (cfg, stack2) + fun strict_ok -> + fun stack1 -> + fun rng -> + fun fv -> + fun qninfo -> + let res = + should_unfold cfg strict_ok + (fun cfg1 -> should_reify cfg1 stack1) fv qninfo in + match res with + | Should_unfold_no -> FStar_Pervasives_Native.None + | Should_unfold_yes -> + FStar_Pervasives_Native.Some (cfg, stack1) + | Should_unfold_fully -> + let cfg' = + { + FStar_TypeChecker_Cfg.steps = + (let uu___ = cfg.FStar_TypeChecker_Cfg.steps in + { + FStar_TypeChecker_Cfg.beta = + (uu___.FStar_TypeChecker_Cfg.beta); + FStar_TypeChecker_Cfg.iota = + (uu___.FStar_TypeChecker_Cfg.iota); + FStar_TypeChecker_Cfg.zeta = + (uu___.FStar_TypeChecker_Cfg.zeta); + FStar_TypeChecker_Cfg.zeta_full = + (uu___.FStar_TypeChecker_Cfg.zeta_full); + FStar_TypeChecker_Cfg.weak = + (uu___.FStar_TypeChecker_Cfg.weak); + FStar_TypeChecker_Cfg.hnf = + (uu___.FStar_TypeChecker_Cfg.hnf); + FStar_TypeChecker_Cfg.primops = + (uu___.FStar_TypeChecker_Cfg.primops); + FStar_TypeChecker_Cfg.do_not_unfold_pure_lets = + (uu___.FStar_TypeChecker_Cfg.do_not_unfold_pure_lets); + FStar_TypeChecker_Cfg.unfold_until = + (FStar_Pervasives_Native.Some + FStar_Syntax_Syntax.delta_constant); + FStar_TypeChecker_Cfg.unfold_only = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_fully = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_attr = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_qual = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_namespace = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_tac = + (uu___.FStar_TypeChecker_Cfg.unfold_tac); + FStar_TypeChecker_Cfg.pure_subterms_within_computations + = + (uu___.FStar_TypeChecker_Cfg.pure_subterms_within_computations); + FStar_TypeChecker_Cfg.simplify = + (uu___.FStar_TypeChecker_Cfg.simplify); + FStar_TypeChecker_Cfg.erase_universes = + (uu___.FStar_TypeChecker_Cfg.erase_universes); + FStar_TypeChecker_Cfg.allow_unbound_universes = + (uu___.FStar_TypeChecker_Cfg.allow_unbound_universes); + FStar_TypeChecker_Cfg.reify_ = + (uu___.FStar_TypeChecker_Cfg.reify_); + FStar_TypeChecker_Cfg.compress_uvars = + (uu___.FStar_TypeChecker_Cfg.compress_uvars); + FStar_TypeChecker_Cfg.no_full_norm = + (uu___.FStar_TypeChecker_Cfg.no_full_norm); + FStar_TypeChecker_Cfg.check_no_uvars = + (uu___.FStar_TypeChecker_Cfg.check_no_uvars); + FStar_TypeChecker_Cfg.unmeta = + (uu___.FStar_TypeChecker_Cfg.unmeta); + FStar_TypeChecker_Cfg.unascribe = + (uu___.FStar_TypeChecker_Cfg.unascribe); + FStar_TypeChecker_Cfg.in_full_norm_request = + (uu___.FStar_TypeChecker_Cfg.in_full_norm_request); + FStar_TypeChecker_Cfg.weakly_reduce_scrutinee = + (uu___.FStar_TypeChecker_Cfg.weakly_reduce_scrutinee); + FStar_TypeChecker_Cfg.nbe_step = + (uu___.FStar_TypeChecker_Cfg.nbe_step); + FStar_TypeChecker_Cfg.for_extraction = + (uu___.FStar_TypeChecker_Cfg.for_extraction); + FStar_TypeChecker_Cfg.unrefine = + (uu___.FStar_TypeChecker_Cfg.unrefine) + }); + FStar_TypeChecker_Cfg.tcenv = + (cfg.FStar_TypeChecker_Cfg.tcenv); + FStar_TypeChecker_Cfg.debug = + (cfg.FStar_TypeChecker_Cfg.debug); + FStar_TypeChecker_Cfg.delta_level = + (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); + FStar_TypeChecker_Cfg.primitive_steps = + (cfg.FStar_TypeChecker_Cfg.primitive_steps); + FStar_TypeChecker_Cfg.strong = + (cfg.FStar_TypeChecker_Cfg.strong); + FStar_TypeChecker_Cfg.memoize_lazy = + (cfg.FStar_TypeChecker_Cfg.memoize_lazy); + FStar_TypeChecker_Cfg.normalize_pure_lets = + (cfg.FStar_TypeChecker_Cfg.normalize_pure_lets); + FStar_TypeChecker_Cfg.reifying = + (cfg.FStar_TypeChecker_Cfg.reifying); + FStar_TypeChecker_Cfg.compat_memo_ignore_cfg = + (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg) + } in + let stack' = + match stack1 with + | (UnivArgs (us, r))::stack'1 -> (UnivArgs (us, r)) :: + (Cfg (cfg, FStar_Pervasives_Native.None)) :: stack'1 + | stack'1 -> (Cfg (cfg, FStar_Pervasives_Native.None)) :: + stack'1 in + FStar_Pervasives_Native.Some (cfg', stack') + | Should_unfold_reify -> + let rec push e s = + match s with + | [] -> [e] + | (UnivArgs (us, r))::t -> + let uu___ = push e t in (UnivArgs (us, r)) :: uu___ + | h::t -> e :: h :: t in + let ref = + let uu___ = + let uu___1 = + let uu___2 = FStar_Syntax_Syntax.lid_of_fv fv in + FStar_Const.Const_reflect uu___2 in + FStar_Syntax_Syntax.Tm_constant uu___1 in + FStar_Syntax_Syntax.mk uu___ + FStar_Compiler_Range_Type.dummyRange in + let stack2 = + push + (App + (empty_env, ref, FStar_Pervasives_Native.None, + FStar_Compiler_Range_Type.dummyRange)) stack1 in + FStar_Pervasives_Native.Some (cfg, stack2) let (on_domain_lids : FStar_Ident.lident Prims.list) = [FStar_Parser_Const.fext_on_domain_lid; FStar_Parser_Const.fext_on_dom_lid; @@ -3117,8 +3183,8 @@ let rec (norm : rebuild cfg empty_env stack2 t1) | uu___3 -> let uu___4 = - decide_unfolding cfg stack2 t1.FStar_Syntax_Syntax.pos - fv qninfo in + decide_unfolding cfg false stack2 + t1.FStar_Syntax_Syntax.pos fv qninfo in (match uu___4 with | FStar_Pervasives_Native.Some (cfg1, stack3) -> do_unfold_fv cfg1 stack3 t1 qninfo fv @@ -3240,6 +3306,8 @@ let rec (norm : FStar_TypeChecker_Cfg.delta_level = [FStar_TypeChecker_Env.Unfold FStar_Syntax_Syntax.delta_constant]; + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -3415,6 +3483,8 @@ let rec (norm : FStar_TypeChecker_Cfg.debug = (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = delta_level; + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -3579,6 +3649,8 @@ let rec (norm : (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = true; @@ -3658,166 +3730,98 @@ let rec (norm : { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_} -> - let strict_args = - let uu___2 = - let uu___3 = - let uu___4 = - FStar_Compiler_Effect.op_Bar_Greater head - FStar_Syntax_Util.unascribe in - FStar_Compiler_Effect.op_Bar_Greater uu___4 - FStar_Syntax_Util.un_uinst in - uu___3.FStar_Syntax_Syntax.n in - match uu___2 with - | FStar_Syntax_Syntax.Tm_fvar fv -> - FStar_TypeChecker_Env.fv_has_strict_args - cfg.FStar_TypeChecker_Cfg.tcenv fv - | uu___3 -> FStar_Pervasives_Native.None in - (match strict_args with - | FStar_Pervasives_Native.None -> - let stack3 = - FStar_Compiler_List.fold_right - (fun uu___2 -> - fun stack4 -> - match uu___2 with - | (a, aq) -> - let a1 = - let uu___3 = - (((let uu___4 = - FStar_TypeChecker_Cfg.cfg_env cfg in - uu___4.FStar_TypeChecker_Env.erase_erasable_args) - || - (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction) - || - (cfg.FStar_TypeChecker_Cfg.debug).FStar_TypeChecker_Cfg.erase_erasable_args) - && - (FStar_Syntax_Util.aqual_is_erasable - aq) in - if uu___3 - then FStar_Syntax_Util.exp_unit - else a in - let env2 = - let uu___3 = - let uu___4 = - FStar_Syntax_Subst.compress a1 in - uu___4.FStar_Syntax_Syntax.n in - match uu___3 with - | FStar_Syntax_Syntax.Tm_name uu___4 -> - empty_env - | FStar_Syntax_Syntax.Tm_constant uu___4 - -> empty_env - | FStar_Syntax_Syntax.Tm_lazy uu___4 -> - empty_env - | FStar_Syntax_Syntax.Tm_fvar uu___4 -> - empty_env - | uu___4 -> env1 in - let uu___3 = - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - FStar_Compiler_Util.mk_ref - FStar_Pervasives_Native.None in - (env2, a1, uu___7, false) in - Clos uu___6 in - (uu___5, aq, - (t1.FStar_Syntax_Syntax.pos)) in - Arg uu___4 in - uu___3 :: stack4) args stack2 in - (FStar_TypeChecker_Cfg.log cfg - (fun uu___3 -> - let uu___4 = - FStar_Compiler_Effect.op_Less_Bar - FStar_Compiler_Util.string_of_int - (FStar_Compiler_List.length args) in - FStar_Compiler_Util.print1 - "\tPushed %s arguments\n" uu___4); - norm cfg env1 stack3 head) - | FStar_Pervasives_Native.Some strict_args1 -> - let norm_args = - FStar_Compiler_Effect.op_Bar_Greater args - (FStar_Compiler_List.map - (fun uu___2 -> - match uu___2 with - | (a, i) -> - let uu___3 = norm cfg env1 [] a in - (uu___3, i))) in - let norm_args_len = FStar_Compiler_List.length norm_args in - let uu___2 = - FStar_Compiler_Effect.op_Bar_Greater strict_args1 - (FStar_Compiler_List.for_all - (fun i -> - if i >= norm_args_len - then false - else - (let uu___4 = - FStar_Compiler_List.nth norm_args i in - match uu___4 with - | (arg_i, uu___5) -> - let uu___6 = - let uu___7 = - FStar_Compiler_Effect.op_Bar_Greater - arg_i - FStar_Syntax_Util.unmeta_safe in - FStar_Compiler_Effect.op_Bar_Greater - uu___7 - FStar_Syntax_Util.head_and_args in - (match uu___6 with - | (head1, uu___7) -> - let uu___8 = - let uu___9 = - FStar_Syntax_Util.un_uinst - head1 in - uu___9.FStar_Syntax_Syntax.n in - (match uu___8 with - | FStar_Syntax_Syntax.Tm_constant - uu___9 -> true - | FStar_Syntax_Syntax.Tm_fvar fv - -> - let uu___9 = - FStar_Syntax_Syntax.lid_of_fv - fv in - FStar_TypeChecker_Env.is_datacon - cfg.FStar_TypeChecker_Cfg.tcenv - uu___9 - | uu___9 -> false))))) in - if uu___2 - then - let stack3 = - FStar_Compiler_Effect.op_Bar_Greater stack2 - (FStar_Compiler_List.fold_right - (fun uu___3 -> - fun stack4 -> - match uu___3 with - | (a, aq) -> - let uu___4 = - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = - FStar_Compiler_Util.mk_ref - (FStar_Pervasives_Native.Some - (cfg, ([], a))) in - (env1, a, uu___8, false) in - Clos uu___7 in - (uu___6, aq, - (t1.FStar_Syntax_Syntax.pos)) in - Arg uu___5 in - uu___4 :: stack4) norm_args) in - (FStar_TypeChecker_Cfg.log cfg - (fun uu___4 -> - let uu___5 = - FStar_Compiler_Effect.op_Less_Bar - FStar_Compiler_Util.string_of_int - (FStar_Compiler_List.length args) in - FStar_Compiler_Util.print1 - "\tPushed %s arguments\n" uu___5); - norm cfg env1 stack3 head) - else - (let head1 = closure_as_term cfg env1 head in - let term = - FStar_Syntax_Syntax.mk_Tm_app head1 norm_args - t1.FStar_Syntax_Syntax.pos in - rebuild cfg env1 stack2 term)) + let fallback uu___2 = + let stack3 = + FStar_Compiler_List.fold_right + (fun uu___3 -> + fun stack4 -> + match uu___3 with + | (a, aq) -> + let a1 = + let uu___4 = + (((let uu___5 = + FStar_TypeChecker_Cfg.cfg_env cfg in + uu___5.FStar_TypeChecker_Env.erase_erasable_args) + || + (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.for_extraction) + || + (cfg.FStar_TypeChecker_Cfg.debug).FStar_TypeChecker_Cfg.erase_erasable_args) + && + (FStar_Syntax_Util.aqual_is_erasable aq) in + if uu___4 + then FStar_Syntax_Util.exp_unit + else a in + let env2 = + let uu___4 = + let uu___5 = FStar_Syntax_Subst.compress a1 in + uu___5.FStar_Syntax_Syntax.n in + match uu___4 with + | FStar_Syntax_Syntax.Tm_name uu___5 -> + empty_env + | FStar_Syntax_Syntax.Tm_constant uu___5 -> + empty_env + | FStar_Syntax_Syntax.Tm_lazy uu___5 -> + empty_env + | FStar_Syntax_Syntax.Tm_fvar uu___5 -> + empty_env + | uu___5 -> env1 in + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Compiler_Util.mk_ref + FStar_Pervasives_Native.None in + (env2, a1, uu___8, false) in + Clos uu___7 in + (uu___6, aq, (t1.FStar_Syntax_Syntax.pos)) in + Arg uu___5 in + uu___4 :: stack4) args stack2 in + FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + FStar_Compiler_Effect.op_Less_Bar + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length args) in + FStar_Compiler_Util.print1 "\tPushed %s arguments\n" + uu___5); + norm cfg env1 stack3 head in + if cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs + then fallback () + else + (let head_fv_us_opt = + let head1 = FStar_Syntax_Util.unascribe head in + let head2 = FStar_Syntax_Subst.compress head1 in + match head2.FStar_Syntax_Syntax.n with + | FStar_Syntax_Syntax.Tm_fvar fv -> + FStar_Pervasives_Native.Some (head2, fv, []) + | FStar_Syntax_Syntax.Tm_uinst + ({ + FStar_Syntax_Syntax.n = + FStar_Syntax_Syntax.Tm_fvar fv; + FStar_Syntax_Syntax.pos = uu___3; + FStar_Syntax_Syntax.vars = uu___4; + FStar_Syntax_Syntax.hash_code = uu___5;_}, + us) + -> + FStar_Pervasives_Native.Some + ((FStar_Pervasives_Native.fst + (FStar_Syntax_Syntax.__proj__Tm_uinst__item___0 + head2.FStar_Syntax_Syntax.n)), fv, us) + | uu___3 -> FStar_Pervasives_Native.None in + match head_fv_us_opt with + | FStar_Pervasives_Native.None -> fallback () + | FStar_Pervasives_Native.Some (head1, fv, us) -> + let uu___3 = + FStar_TypeChecker_Env.fv_has_strict_args + cfg.FStar_TypeChecker_Cfg.tcenv fv in + (match uu___3 with + | FStar_Pervasives_Native.Some + (strict_unfold, strict_args) -> + handle_strict_application cfg env1 stack2 head1 fv + us strict_unfold strict_args args + t1.FStar_Syntax_Syntax.pos + | FStar_Pervasives_Native.None -> fallback ())) | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = uu___2;_} @@ -4093,6 +4097,8 @@ let rec (norm : (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -4137,6 +4143,8 @@ let rec (norm : (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = @@ -4350,6 +4358,8 @@ let rec (norm : (cfg.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = true; @@ -4758,19 +4768,22 @@ and (do_unfold_fv : then match stack1 with | (UnivArgs (us', uu___2))::stack2 -> - ((let uu___4 = + (if n <> (FStar_Compiler_List.length us') + then failwith "ah!!!" + else (); + (let uu___5 = FStar_Compiler_Effect.op_Less_Bar (FStar_TypeChecker_Env.debug cfg.FStar_TypeChecker_Cfg.tcenv) (FStar_Options.Other "univ_norm") in - if uu___4 + if uu___5 then FStar_Compiler_List.iter (fun x -> - let uu___5 = + let uu___6 = FStar_Syntax_Print.univ_to_string x in FStar_Compiler_Util.print1 - "Univ (normalizer) %s\n" uu___5) us' + "Univ (normalizer) %s\n" uu___6) us' else ()); (let env1 = FStar_Compiler_Effect.op_Bar_Greater us' @@ -4787,15 +4800,302 @@ and (do_unfold_fv : (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.allow_unbound_universes -> norm cfg empty_env stack1 t1 | uu___2 -> - let uu___3 = - let uu___4 = - FStar_Syntax_Print.lid_to_string - (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in - FStar_Compiler_Util.format1 - "Impossible: missing universe instantiation on %s" - uu___4 in - failwith uu___3 - else norm cfg empty_env stack1 t1)) + (FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + let uu___6 = + let uu___7 = + firstn (Prims.of_int (4)) stack1 in + FStar_Compiler_Effect.op_Less_Bar + FStar_Pervasives_Native.fst uu___7 in + stack_to_string uu___6 in + FStar_Compiler_Util.print1 + "top of stack = %s\n" uu___5); + (let uu___4 = + let uu___5 = + FStar_Syntax_Print.lid_to_string + (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + FStar_Compiler_Util.format1 + "Impossible: missing universe instantiation on %s" + uu___5 in + failwith uu___4)) + else + (match stack1 with + | (UnivArgs (us', uu___3))::stack2 -> + failwith "univ args on not-uni-poly defn?" + | uu___3 -> norm cfg empty_env stack1 t1))) +and (handle_strict_application : + FStar_TypeChecker_Cfg.cfg -> + env -> + stack_elt Prims.list -> + FStar_Syntax_Syntax.term -> + FStar_Syntax_Syntax.fv -> + FStar_Syntax_Syntax.universes -> + Prims.bool -> + Prims.int Prims.list -> + (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * + FStar_Syntax_Syntax.arg_qualifier + FStar_Pervasives_Native.option) Prims.list -> + FStar_Compiler_Range_Type.range -> + FStar_Syntax_Syntax.term) + = + fun cfg -> + fun env1 -> + fun stack1 -> + fun head -> + fun fv -> + fun us -> + fun strict_unfold -> + fun strict_args -> + fun args -> + fun rng -> + FStar_TypeChecker_Cfg.log cfg + (fun uu___1 -> + let uu___2 = FStar_Syntax_Print.fv_to_string fv in + let uu___3 = + (FStar_Common.string_of_list ()) + FStar_Compiler_Util.string_of_int strict_args in + let uu___4 = + FStar_Compiler_Util.string_of_bool strict_unfold in + FStar_Compiler_Util.print3 + "Got strict application for %s, strict_args = %s, strict_unfold = %s\n" + uu___2 uu___3 uu___4); + (let cfg_args = + if strict_unfold + then + { + FStar_TypeChecker_Cfg.steps = + (let uu___1 = cfg.FStar_TypeChecker_Cfg.steps in + { + FStar_TypeChecker_Cfg.beta = + (uu___1.FStar_TypeChecker_Cfg.beta); + FStar_TypeChecker_Cfg.iota = + (uu___1.FStar_TypeChecker_Cfg.iota); + FStar_TypeChecker_Cfg.zeta = + (uu___1.FStar_TypeChecker_Cfg.zeta); + FStar_TypeChecker_Cfg.zeta_full = + (uu___1.FStar_TypeChecker_Cfg.zeta_full); + FStar_TypeChecker_Cfg.weak = true; + FStar_TypeChecker_Cfg.hnf = true; + FStar_TypeChecker_Cfg.primops = + (uu___1.FStar_TypeChecker_Cfg.primops); + FStar_TypeChecker_Cfg.do_not_unfold_pure_lets + = + (uu___1.FStar_TypeChecker_Cfg.do_not_unfold_pure_lets); + FStar_TypeChecker_Cfg.unfold_until = + (FStar_Pervasives_Native.Some + FStar_Syntax_Syntax.delta_constant); + FStar_TypeChecker_Cfg.unfold_only = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_fully = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_attr = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_qual = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_namespace = + FStar_Pervasives_Native.None; + FStar_TypeChecker_Cfg.unfold_tac = + (uu___1.FStar_TypeChecker_Cfg.unfold_tac); + FStar_TypeChecker_Cfg.pure_subterms_within_computations + = + (uu___1.FStar_TypeChecker_Cfg.pure_subterms_within_computations); + FStar_TypeChecker_Cfg.simplify = + (uu___1.FStar_TypeChecker_Cfg.simplify); + FStar_TypeChecker_Cfg.erase_universes = + (uu___1.FStar_TypeChecker_Cfg.erase_universes); + FStar_TypeChecker_Cfg.allow_unbound_universes + = + (uu___1.FStar_TypeChecker_Cfg.allow_unbound_universes); + FStar_TypeChecker_Cfg.reify_ = + (uu___1.FStar_TypeChecker_Cfg.reify_); + FStar_TypeChecker_Cfg.compress_uvars = + (uu___1.FStar_TypeChecker_Cfg.compress_uvars); + FStar_TypeChecker_Cfg.no_full_norm = + (uu___1.FStar_TypeChecker_Cfg.no_full_norm); + FStar_TypeChecker_Cfg.check_no_uvars = + (uu___1.FStar_TypeChecker_Cfg.check_no_uvars); + FStar_TypeChecker_Cfg.unmeta = + (uu___1.FStar_TypeChecker_Cfg.unmeta); + FStar_TypeChecker_Cfg.unascribe = + (uu___1.FStar_TypeChecker_Cfg.unascribe); + FStar_TypeChecker_Cfg.in_full_norm_request + = + (uu___1.FStar_TypeChecker_Cfg.in_full_norm_request); + FStar_TypeChecker_Cfg.weakly_reduce_scrutinee + = + (uu___1.FStar_TypeChecker_Cfg.weakly_reduce_scrutinee); + FStar_TypeChecker_Cfg.nbe_step = + (uu___1.FStar_TypeChecker_Cfg.nbe_step); + FStar_TypeChecker_Cfg.for_extraction = + (uu___1.FStar_TypeChecker_Cfg.for_extraction); + FStar_TypeChecker_Cfg.unrefine = + (uu___1.FStar_TypeChecker_Cfg.unrefine) + }); + FStar_TypeChecker_Cfg.tcenv = + (cfg.FStar_TypeChecker_Cfg.tcenv); + FStar_TypeChecker_Cfg.debug = + (cfg.FStar_TypeChecker_Cfg.debug); + FStar_TypeChecker_Cfg.delta_level = + [FStar_TypeChecker_Env.Unfold + FStar_Syntax_Syntax.delta_constant]; + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg.FStar_TypeChecker_Cfg.unfold_strict_fvs); + FStar_TypeChecker_Cfg.primitive_steps = + (cfg.FStar_TypeChecker_Cfg.primitive_steps); + FStar_TypeChecker_Cfg.strong = + (cfg.FStar_TypeChecker_Cfg.strong); + FStar_TypeChecker_Cfg.memoize_lazy = + (cfg.FStar_TypeChecker_Cfg.memoize_lazy); + FStar_TypeChecker_Cfg.normalize_pure_lets = + (cfg.FStar_TypeChecker_Cfg.normalize_pure_lets); + FStar_TypeChecker_Cfg.reifying = + (cfg.FStar_TypeChecker_Cfg.reifying); + FStar_TypeChecker_Cfg.compat_memo_ignore_cfg = + (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg) + } + else cfg in + let args_len = FStar_Compiler_List.length args in + let norm_args = + FStar_Compiler_Effect.op_Bar_Greater args + (FStar_Compiler_List.mapi + (fun idx -> + fun uu___1 -> + match uu___1 with + | (a, i) -> + let a1 = + FStar_TypeChecker_Cfg.log cfg + (fun uu___3 -> + let uu___4 = + FStar_Compiler_Util.string_of_int + idx in + let uu___5 = + FStar_Syntax_Print.term_to_string + a in + FStar_Compiler_Util.print2 + "Normalizing strict arg %s (%s)\n" + uu___4 uu___5); + if + strict_unfold && + (FStar_Compiler_List.mem idx + strict_args) + then norm cfg_args env1 [] a + else norm cfg env1 [] a in + (a1, i))) in + let is_hnf i = + if i >= args_len + then false + else + (let uu___2 = FStar_Compiler_List.nth norm_args i in + match uu___2 with + | (arg_i, uu___3) -> + let uu___4 = + let uu___5 = + FStar_Compiler_Effect.op_Bar_Greater + arg_i FStar_Syntax_Util.unmeta_safe in + FStar_Compiler_Effect.op_Bar_Greater uu___5 + FStar_Syntax_Util.head_and_args in + (match uu___4 with + | (head1, uu___5) -> + let uu___6 = + let uu___7 = + FStar_Syntax_Util.un_uinst head1 in + uu___7.FStar_Syntax_Syntax.n in + (match uu___6 with + | FStar_Syntax_Syntax.Tm_constant + uu___7 -> true + | FStar_Syntax_Syntax.Tm_fvar fv1 -> + let uu___7 = + FStar_Syntax_Syntax.lid_of_fv fv1 in + FStar_TypeChecker_Env.is_datacon + cfg.FStar_TypeChecker_Cfg.tcenv + uu___7 + | uu___7 -> false))) in + let uu___1 = + FStar_Compiler_List.for_all is_hnf strict_args in + if uu___1 + then + (FStar_TypeChecker_Cfg.log cfg + (fun uu___3 -> + let uu___4 = + FStar_Syntax_Print.term_to_string head in + let uu___5 = + FStar_Syntax_Print.univs_to_string us in + FStar_Compiler_Util.print2 + "Strict reduction kicking in for %s<%s>\n" + uu___4 uu___5); + (let lid = + (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in + let qninfo = + FStar_TypeChecker_Env.lookup_qname + cfg.FStar_TypeChecker_Cfg.tcenv lid in + let stack2 = + FStar_Compiler_Effect.op_Bar_Greater stack1 + (FStar_Compiler_List.fold_right + (fun uu___3 -> + fun stack3 -> + match uu___3 with + | (a, aq) -> + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + let uu___8 = + FStar_Compiler_Util.mk_ref + (FStar_Pervasives_Native.Some + (cfg, ([], a))) in + (env1, a, uu___8, false) in + Clos uu___7 in + (uu___6, aq, rng) in + Arg uu___5 in + uu___4 :: stack3) norm_args) in + FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + FStar_Compiler_Effect.op_Less_Bar + FStar_Compiler_Util.string_of_int + (FStar_Compiler_List.length args) in + FStar_Compiler_Util.print1 + "\tPushed %s arguments\n" uu___5); + (let stack3 = + match us with + | [] -> stack2 + | us1 -> + let us2 = + FStar_Compiler_List.map + (norm_universe cfg env1) us1 in + (UnivArgs + (us2, (head.FStar_Syntax_Syntax.pos))) + :: stack2 in + let head1 = FStar_Syntax_Subst.compress head in + let uu___4 = + decide_unfolding cfg true stack3 + head1.FStar_Syntax_Syntax.pos fv qninfo in + match uu___4 with + | FStar_Pervasives_Native.Some (cfg1, stack4) -> + do_unfold_fv cfg1 stack4 head1 qninfo fv + | FStar_Pervasives_Native.None -> + rebuild cfg env1 stack3 head1))) + else + (FStar_TypeChecker_Cfg.log cfg + (fun uu___4 -> + let uu___5 = + FStar_Syntax_Print.term_to_string head in + let uu___6 = + FStar_Syntax_Print.univs_to_string us in + FStar_Compiler_Util.print2 + "Strict reduction DID NOT kick in for %s<%s>, rebuilding\n" + uu___5 uu___6); + (let head1 = + match us with + | [] -> head + | us1 -> + FStar_Syntax_Syntax.mk_Tm_uinst head us1 in + let head2 = closure_as_term cfg env1 head1 in + let term = + FStar_Syntax_Syntax.mk_Tm_app head2 norm_args + rng in + rebuild cfg env1 stack1 term))) and (reduce_impure_comp : FStar_TypeChecker_Cfg.cfg -> env -> @@ -8051,6 +8351,8 @@ and (do_rebuild : FStar_TypeChecker_Cfg.debug = (cfg1.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = new_delta; + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg1.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg1.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = true; @@ -8306,6 +8608,8 @@ and (do_rebuild : (cfg1.FStar_TypeChecker_Cfg.debug); FStar_TypeChecker_Cfg.delta_level = (cfg1.FStar_TypeChecker_Cfg.delta_level); + FStar_TypeChecker_Cfg.unfold_strict_fvs = + (cfg1.FStar_TypeChecker_Cfg.unfold_strict_fvs); FStar_TypeChecker_Cfg.primitive_steps = (cfg1.FStar_TypeChecker_Cfg.primitive_steps); FStar_TypeChecker_Cfg.strong = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 8c71cee8760..9e2cd35a0d0 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -3054,6 +3054,7 @@ let (head_matches_delta : let basic_steps = [FStar_TypeChecker_Env.UnfoldUntil FStar_Syntax_Syntax.delta_constant; + FStar_TypeChecker_Env.UnfoldStrict; FStar_TypeChecker_Env.Weak; FStar_TypeChecker_Env.HNF; FStar_TypeChecker_Env.Primops; @@ -10347,7 +10348,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -10483,7 +10484,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -10619,7 +10620,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -10755,7 +10756,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -10891,7 +10892,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11027,7 +11028,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11163,7 +11164,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11299,7 +11300,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11435,7 +11436,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11571,7 +11572,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11707,7 +11708,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = @@ -11843,7 +11844,7 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 :: uu___15 in uu___12 :: uu___13 in FStar_Compiler_Util.print - ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" + ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s; no_free_uvars=%s]\n" uu___11 else ()); (let equal t11 t21 = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index f1a58e816c5..d224e46272f 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -10480,10 +10480,8 @@ and (check_top_level_let : if uu___4 then FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.UnfoldAttr - [FStar_Parser_Const.tcnorm_attr]; - FStar_TypeChecker_Env.Exclude - FStar_TypeChecker_Env.Beta; + [FStar_TypeChecker_Env.Exclude + FStar_TypeChecker_Env.Beta; FStar_TypeChecker_Env.Exclude FStar_TypeChecker_Env.Zeta; FStar_TypeChecker_Env.NoFullNorm;