From c31be3f30e58323076ddb43d9dfeccc216849147 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 7 Oct 2024 23:06:17 -0700 Subject: [PATCH 1/9] Tc: make other components of guards also catenable lists --- src/typechecker/FStar.TypeChecker.Common.fst | 24 +- src/typechecker/FStar.TypeChecker.Common.fsti | 5 +- .../FStar.TypeChecker.DeferredImplicits.fst | 7 +- src/typechecker/FStar.TypeChecker.Env.fst | 42 ++-- src/typechecker/FStar.TypeChecker.Rel.fst | 217 +++++++++--------- .../FStar.TypeChecker.TcInductive.fst | 3 +- src/typechecker/FStar.TypeChecker.Util.fst | 8 +- 7 files changed, 161 insertions(+), 145 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Common.fst b/src/typechecker/FStar.TypeChecker.Common.fst index 0ae4934e82d..9f4fd677701 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fst +++ b/src/typechecker/FStar.TypeChecker.Common.fst @@ -215,13 +215,15 @@ let implicits_to_string imps = let imp_to_string i = show i.imp_uvar.ctx_uvar_head in FStar.Common.string_of_list imp_to_string imps -let trivial_guard = { - guard_f=Trivial; - deferred_to_tac=[]; - deferred=[]; - univ_ineqs=([], []); - implicits=Class.Listlike.empty; -} +let trivial_guard = + let open FStar.Class.Listlike in + { + guard_f=Trivial; + deferred_to_tac=empty; + deferred=empty; + univ_ineqs=(empty, empty); + implicits=empty; + } let conj_guard_f g1 g2 = match g1, g2 with | Trivial, g @@ -230,10 +232,10 @@ let conj_guard_f g1 g2 = match g1, g2 with let binop_guard f g1 g2 = { guard_f=f g1.guard_f g2.guard_f; - deferred_to_tac=g1.deferred_to_tac@g2.deferred_to_tac; - deferred=g1.deferred@g2.deferred; - univ_ineqs=(fst g1.univ_ineqs@fst g2.univ_ineqs, - snd g1.univ_ineqs@snd g2.univ_ineqs); + deferred_to_tac=g1.deferred_to_tac ++ g2.deferred_to_tac; + deferred=g1.deferred ++ g2.deferred; + univ_ineqs=(fst g1.univ_ineqs ++ fst g2.univ_ineqs, + snd g1.univ_ineqs ++ snd g2.univ_ineqs); implicits=g1.implicits ++ g2.implicits; } let conj_guard g1 g2 = binop_guard conj_guard_f g1 g2 diff --git a/src/typechecker/FStar.TypeChecker.Common.fsti b/src/typechecker/FStar.TypeChecker.Common.fsti index cd36830e764..922ef60c010 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fsti +++ b/src/typechecker/FStar.TypeChecker.Common.fsti @@ -27,6 +27,7 @@ open FStar.Ident open FStar.Class.Show open FStar.Class.Monoid +open FStar.Compiler.CList module CList = FStar.Compiler.CList (* Bring instances in scope *) @@ -92,7 +93,7 @@ type deferred_reason = instance val showable_deferred_reason : showable deferred_reason -type deferred = list (deferred_reason & string & prob) +type deferred = clist (deferred_reason & string & prob) type univ_ineq = universe & universe @@ -166,7 +167,7 @@ type guard_t = { deferred_to_tac: deferred; //This field maintains problems that are to be dispatched to a tactic //They are never attempted by the unification engine in Rel deferred: deferred; - univ_ineqs: list universe & list univ_ineq; + univ_ineqs: clist universe & clist univ_ineq; implicits: implicits_t; } diff --git a/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst b/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst index 4a4f2667606..fa74616c2d8 100644 --- a/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst +++ b/src/typechecker/FStar.TypeChecker.DeferredImplicits.fst @@ -39,6 +39,7 @@ module TEQ = FStar.TypeChecker.TermEqAndSimplify open FStar.Class.Setlike open FStar.Class.Show +module Listlike = FStar.Class.Listlike let is_flex t = let head, _args = U.head_and_args_full t in @@ -258,7 +259,7 @@ let solve_deferred_to_tactic_goals env g = failwith "Unexpected problem deferred to tactic" in //Turn all the deferred problems into equality goals - let eqs = List.map prob_as_implicit g.deferred_to_tac in + let eqs = List.map prob_as_implicit (Listlike.to_list g.deferred_to_tac) in //Also take any unsolved uvars in the guard implicits that are tagged //with attributes let more, imps = @@ -274,7 +275,7 @@ let solve_deferred_to_tactic_goals env g = more, imp::imps | Some se -> (imp, se)::more, imps) - (Class.Listlike.to_list g.implicits) + (Listlike.to_list g.implicits) ([], []) in (** Each implicit is associated with a sigelt. @@ -299,4 +300,4 @@ let solve_deferred_to_tactic_goals env g = let buckets = bucketize (eqs@more) in // Dispatch each bucket of implicits to their respective tactic List.iter (fun (imps, sigel) -> solve_goals_with_tac env g imps sigel) buckets; - { g with deferred_to_tac=[]; implicits = Class.Listlike.from_list imps} + { g with deferred_to_tac=Listlike.empty; implicits = Class.Listlike.from_list imps} diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index 4c61a15cbc0..c12032c0da3 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -1884,24 +1884,36 @@ let string_of_proof_ns env = (* ------------------------------------------------*) (* Operations on guard_formula *) (* ------------------------------------------------*) -let guard_of_guard_formula g = { - guard_f=g; - deferred=[]; - deferred_to_tac=[]; - univ_ineqs=([], []); - implicits=Class.Listlike.empty; -} +let guard_of_guard_formula g = + let open FStar.Class.Listlike in + { + guard_f=g; + deferred=empty; + deferred_to_tac=empty; + univ_ineqs=(empty, empty); + implicits=empty; + } let guard_form g = g.guard_f -let is_trivial g = match g with - | {guard_f=Trivial; deferred=[]; univ_ineqs=([], []); implicits=i} -> - i |> CList.for_all (fun imp -> - (Allow_unresolved? (U.ctx_uvar_should_check imp.imp_uvar)) - || (match Unionfind.find imp.imp_uvar.ctx_uvar_head with - | Some _ -> true - | None -> false)) - | _ -> false +let is_trivial g = + let open FStar.Class.Listlike in + (* This is cumbersome due to not having view patterns. *) + // match g with + // | {guard_f=Trivial; deferred=[]; univ_ineqs=([], []); implicits=i} -> + if + Trivial? g.guard_f && + is_empty g.deferred && + is_empty (fst g.univ_ineqs) && + is_empty (snd g.univ_ineqs) + then + g.implicits |> CList.for_all (fun imp -> + (Allow_unresolved? (U.ctx_uvar_should_check imp.imp_uvar)) + || (match Unionfind.find imp.imp_uvar.ctx_uvar_head with + | Some _ -> true + | None -> false)) + else + false let is_trivial_guard_formula g = match g with | {guard_f=Trivial} -> true diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index 6128b527554..eda6974b3ff 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -44,6 +44,8 @@ open FStar.Class.Setlike open FStar.Class.Listlike open FStar.Class.Monoid module Setlike = FStar.Class.Setlike +open FStar.Class.Listlike +open FStar.Compiler.CList module Listlike = FStar.Class.Listlike module BU = FStar.Compiler.Util //basic util @@ -134,8 +136,8 @@ instance _ : showable defer_ok_t = { (* The set of problems currently being addressed *) type worklist = { attempting: probs; - wl_deferred: list (int & deferred_reason & lstring & prob); //flex-flex cases, non patterns, and subtyping constraints involving a unification variable, - wl_deferred_to_tac: list (int & deferred_reason & lstring & prob); //problems that should be dispatched to a user-provided tactics + wl_deferred: clist (int & deferred_reason & lstring & prob); //flex-flex cases, non patterns, and subtyping constraints involving a unification variable, + wl_deferred_to_tac: clist (int & deferred_reason & lstring & prob); //problems that should be dispatched to a user-provided tactics ctr: int; //a counter incremented each time we extend subst, used to detect if we've made progress defer_ok: defer_ok_t; //whether or not carrying constraints is ok---at the top-level, this flag is NoDefer smt_ok: bool; //whether or not falling back to the SMT solver is permitted @@ -172,11 +174,11 @@ with the problem being tackled. The uses of push_bv/push_binder should be few. *) -let as_deferred (wl_def:list (int & deferred_reason & lstring & prob)) : deferred = - List.map (fun (_, reason, m, p) -> reason, Thunk.force m, p) wl_def +let as_deferred (wl_def:clist (int & deferred_reason & lstring & prob)) : deferred = + CList.map (fun (_, reason, m, p) -> reason, Thunk.force m, p) wl_def -let as_wl_deferred wl (d:deferred): list (int & deferred_reason & lstring & prob) = - List.map (fun (reason, m, p) -> wl.ctr, reason, Thunk.mkv m, p) d +let as_wl_deferred wl (d:deferred): clist (int & deferred_reason & lstring & prob) = + CList.map (fun (reason, m, p) -> wl.ctr, reason, Thunk.mkv m, p) d (* --------------------------------------------------------- *) (* Generating new unification variables/patterns *) @@ -227,8 +229,8 @@ type solution = | Failed of prob & lstring let extend_wl (wl:worklist) (defers:deferred) (defer_to_tac:deferred) (imps:implicits_t) = - {wl with wl_deferred=wl.wl_deferred@(as_wl_deferred wl defers); - wl_deferred_to_tac=wl.wl_deferred_to_tac@(as_wl_deferred wl defer_to_tac); + {wl with wl_deferred=wl.wl_deferred ++ as_wl_deferred wl defers; + wl_deferred_to_tac=wl.wl_deferred_to_tac ++ as_wl_deferred wl defer_to_tac; wl_implicits=wl.wl_implicits ++ imps} type variance = @@ -413,8 +415,8 @@ let uvis_to_string env uvis = FStar.Common.string_of_list (uvi_to_string env) uv (* ------------------------------------------------*) let empty_worklist env = { attempting=[]; - wl_deferred=[]; - wl_deferred_to_tac=[]; + wl_deferred=empty; + wl_deferred_to_tac=empty; ctr=0; tcenv=env; defer_ok=DeferAny; @@ -439,7 +441,7 @@ let giveup_lit wl (reason : string) prob = let singleton wl prob smt_ok = {wl with attempting=[prob]; smt_ok = smt_ok} let wl_of_guard env g = {empty_worklist env with attempting=List.map (fun (_, _, p) -> p) g} -let defer reason msg prob wl = {wl with wl_deferred=(wl.ctr, reason, msg, prob)::wl.wl_deferred} +let defer reason msg prob wl = {wl with wl_deferred= cons (wl.ctr, reason, msg, prob) wl.wl_deferred} let defer_lit reason msg prob wl = defer reason (Thunk.mkv msg) prob wl let attempt probs wl = List.iter (def_check_prob "attempt") probs; @@ -856,10 +858,14 @@ let wl_to_string wl = let probs_to_string (ps:list prob) = List.map (prob_to_string' wl) ps |> String.concat "\n\t" in + let cprobs_to_string (ps:clist prob) = + (* meh ... *) + CList.map (prob_to_string' wl) ps |> to_list |> String.concat "\n\t" + in BU.format2 "{ attempting = [ %s ];\n\ deferred = [ %s ] }\n" (probs_to_string wl.attempting) - (probs_to_string (List.map (fun (_, _, _, x) -> x) wl.wl_deferred)) + (cprobs_to_string (CList.map (fun (_, _, _, x) -> x) wl.wl_deferred)) instance showable_wl : showable worklist = { show = wl_to_string; @@ -2234,20 +2240,20 @@ let rec solve (probs :worklist) : solution = | None -> begin - match probs.wl_deferred with - | [] -> - Success ([], as_deferred probs.wl_deferred_to_tac, probs.wl_implicits) //Yay ... done! - - | _ -> - let attempt, rest = probs.wl_deferred |> List.partition (fun (c, _, _, _) -> c < probs.ctr) in - match attempt with - | [] -> //can't solve yet; defer the rest + match view probs.wl_deferred with + | VNil -> + Success (empty, as_deferred probs.wl_deferred_to_tac, probs.wl_implicits) //Yay ... done! + + | VCons _ _ -> + let attempt, rest = probs.wl_deferred |> CList.partition (fun (c, _, _, _) -> c < probs.ctr) in + match view attempt with + | VNil -> //can't solve yet; defer the rest Success(as_deferred probs.wl_deferred, as_deferred probs.wl_deferred_to_tac, probs.wl_implicits) | _ -> - solve ({probs with attempting=attempt |> List.map (fun (_, _, _, y) -> y); wl_deferred=rest}) + solve ({probs with attempting=attempt |> to_list |> List.map (fun (_, _, _, y) -> y); wl_deferred=rest}) end and solve_one_universe_eq (orig:prob) (u1:universe) (u2:universe) (wl:worklist) : solution = @@ -2315,9 +2321,7 @@ and defer_to_user_tac (orig:prob) reason (wl:worklist) : solution = if !dbg_Rel then BU.print1 "\n\t\tDeferring %s to a tactic\n" (prob_to_string wl.tcenv orig); let wl = solve_prob orig None [] wl in - let wl = {wl with wl_deferred_to_tac=(wl.ctr, - Deferred_to_user_tac, - Thunk.mkv reason, orig)::wl.wl_deferred_to_tac} in + let wl = {wl with wl_deferred_to_tac=cons (wl.ctr, Deferred_to_user_tac, Thunk.mkv reason, orig) wl.wl_deferred_to_tac} in solve wl and maybe_defer_to_user_tac prob reason wl : solution = @@ -2420,13 +2424,13 @@ and solve_rigid_flex_or_flex_rigid_subtyping let wl' = {wl with defer_ok=NoDefer; smt_ok=false; attempting=probs; - wl_deferred=[]; - wl_implicits=Listlike.empty} in + wl_deferred=empty; + wl_implicits=empty} in let tx = UF.new_transaction () in match solve wl' with | Success (_, defer_to_tac, imps) -> UF.commit tx; - Some (extend_wl wl [] defer_to_tac imps) + Some (extend_wl wl empty defer_to_tac imps) | Failed _ -> UF.rollback tx; @@ -2616,11 +2620,11 @@ and solve_rigid_flex_or_flex_rigid_subtyping List.iter (def_check_prob "meet_or_join3_sub") sub_probs; match solve_t eq_prob ({wl' with defer_ok=NoDefer; wl_implicits = Listlike.empty; - wl_deferred = []; + wl_deferred = empty; attempting=sub_probs}) with | Success (_, defer_to_tac, imps) -> let wl = {wl' with attempting=rest} in - let wl = extend_wl wl [] defer_to_tac imps in + let wl = extend_wl wl empty defer_to_tac imps in let g = List.fold_left (fun g p -> U.mk_conj g (p_guard p)) eq_prob.logical_guard sub_probs in @@ -2827,13 +2831,13 @@ and try_solve_without_smt_or_else smt_ok=false; umax_heuristic_ok=false; attempting=[]; - wl_deferred=[]; + wl_deferred=empty; wl_implicits=Listlike.empty} in let tx = UF.new_transaction () in match try_solve wl' with | Success (_, defer_to_tac, imps) -> UF.commit tx; - let wl = extend_wl wl [] defer_to_tac imps in + let wl = extend_wl wl empty defer_to_tac imps in solve wl | Failed (p, s) -> UF.rollback tx; @@ -2848,13 +2852,13 @@ and try_solve_then_or_else let empty_wl = {wl with defer_ok=NoDefer; attempting=[]; - wl_deferred=[]; - wl_implicits=Listlike.empty} in + wl_deferred=empty; + wl_implicits=empty} in let tx = UF.new_transaction () in match try_solve empty_wl with | Success (_, defer_to_tac, imps) -> UF.commit tx; - let wl = extend_wl wl [] defer_to_tac imps in + let wl = extend_wl wl empty defer_to_tac imps in then_solve wl | Failed (p, s) -> UF.rollback tx; @@ -2869,11 +2873,11 @@ and try_solve_probs_without_smt smt_ok=false; umax_heuristic_ok=false; attempting=probs; - wl_deferred=[]; + wl_deferred=empty; wl_implicits=Listlike.empty} in match solve wl' with | Success (_, defer_to_tac, imps) -> - let wl = extend_wl wl [] defer_to_tac imps in + let wl = extend_wl wl empty defer_to_tac imps in Inl wl | Failed (_, ls) -> @@ -3231,11 +3235,11 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) let wl' = { wl with defer_ok = NoDefer; smt_ok = false; attempting = sub_probs; - wl_deferred = []; + wl_deferred = empty; wl_implicits = Listlike.empty } in match solve wl' with | Success (_, defer_to_tac, imps) -> - let wl = extend_wl wl [] defer_to_tac imps in + let wl = extend_wl wl empty defer_to_tac imps in UF.commit tx; Inr wl | Failed (_, lstring) -> @@ -3743,7 +3747,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = let wl' = extend_wl ({wl with defer_ok=NoDefer; smt_ok=false; attempting=[TProb prob]; - wl_deferred=[]; + wl_deferred=empty; wl_implicits=Listlike.empty}) g_pat_term.deferred g_pat_term.deferred_to_tac @@ -3756,8 +3760,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = | Success (_, defer_to_tac', imps') -> UF.commit tx; Some (extend_wl wl - [] - (defer_to_tac@defer_to_tac') + empty + (defer_to_tac ++ defer_to_tac') (imps ++ imps' ++ g_pat_as_exp.implicits ++ g_pat_term.implicits)) | Failed _ -> @@ -4118,7 +4122,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = match solve ({wl with defer_ok=NoDefer; wl_implicits=Listlike.empty; attempting=[ref_prob]; - wl_deferred=[]}) with + wl_deferred=empty}) with | Failed (prob, msg) -> UF.rollback tx; if ((not env.uvar_subtyping && has_uvars) @@ -4134,7 +4138,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = (p_guard ref_prob |> guard_on_element wl problem x1) in let wl = solve_prob orig (Some guard) [] wl in let wl = {wl with ctr=wl.ctr+1} in - let wl = extend_wl wl [] defer_to_tac imps in + let wl = extend_wl wl empty defer_to_tac imps in solve (attempt [base_prob] wl) else fallback() @@ -4434,28 +4438,30 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = EQ (S.mk (S.Tm_type u2) Range.dummyRange) "effect universes" in - (univ_sub_probs@[p]), wl) ([], wl) c1_comp.comp_univs c2_comp.comp_univs in + (univ_sub_probs ++ cons p empty), wl) (empty, wl) c1_comp.comp_univs c2_comp.comp_univs in let ret_sub_prob, wl = sub_prob wl c1_comp.result_typ EQ c2_comp.result_typ "effect ret type" in let arg_sub_probs, wl = List.fold_right2 (fun (a1, _) (a2, _) (arg_sub_probs, wl) -> let p, wl = sub_prob wl a1 EQ a2 "effect arg" in - p::arg_sub_probs, wl) + cons p arg_sub_probs, wl) c1_comp.effect_args c2_comp.effect_args - ([], wl) + (empty, wl) + in + let sub_probs : clist _ = + univ_sub_probs ++ + (cons ret_sub_prob <| + arg_sub_probs ++ + (g_lift.deferred |> CList.map (fun (_, _, p) -> p))) in - let sub_probs = - univ_sub_probs@ - [ret_sub_prob]@ - arg_sub_probs @ - (g_lift.deferred |> List.map (fun (_, _, p) -> p)) in + let sub_probs : list _ = to_list sub_probs in let guard = let guard = U.mk_conj_l (List.map p_guard sub_probs) in match g_lift.guard_f with | Trivial -> guard | NonTrivial f -> U.mk_conj guard f in - let wl = { wl with wl_implicits =g_lift.implicits ++ wl.wl_implicits } in + let wl = { wl with wl_implicits = g_lift.implicits ++ wl.wl_implicits } in let wl = solve_prob orig (Some guard) [] wl in solve (attempt sub_probs wl) in @@ -4780,40 +4786,32 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = (* top-level interface *) (* -------------------------------------------------------- *) let print_pending_implicits g = - to_list g.implicits |> List.map (fun i -> show i.imp_uvar) |> show - -let ineqs_to_string (ineqs : list universe & list (universe & universe)) = - let vars = - fst ineqs - |> List.map show - |> String.concat ", " in - let ineqs = - snd ineqs - |> List.map (fun (u1, u2) -> - BU.format2 "%s < %s" - (show u1) - (show u2)) - |> String.concat ", " in - BU.format2 "Solving for {%s}; inequalities are {%s}" - vars ineqs + g.implicits |> CList.map (fun i -> show i.imp_uvar) |> show + +let ineqs_to_string (ineqs : clist universe & clist (universe & universe)) = + let (vars, ineqs) = ineqs in + let ineqs = ineqs |> CList.map (fun (u1, u2) -> BU.format2 "%s < %s" (show u1) (show u2)) in + BU.format2 "Solving for %s; inequalities are %s" + (show vars) (show ineqs) let guard_to_string (env:env) g = - match g.guard_f, g.deferred, g.univ_ineqs with - | Trivial, [], (_, []) when not (Options.print_implicits ()) -> "{}" - | _ -> - let form = match g.guard_f with - | Trivial -> "trivial" - | NonTrivial f -> - if !dbg_Rel - || Debug.extreme () - || Options.print_implicits () - then N.term_to_string env f - else "non-trivial" in - let carry defs = List.map (fun (_, msg, x) -> msg ^ ": " ^ prob_to_string env x) defs |> String.concat ",\n" in - let imps = print_pending_implicits g in - BU.format5 "\n\t{guard_f=%s;\n\t deferred={\n%s};\n\t deferred_to_tac={\n%s};\n\t univ_ineqs={%s};\n\t implicits=%s}\n" - form (carry g.deferred) (carry g.deferred_to_tac) - (ineqs_to_string g.univ_ineqs) imps + match g.guard_f, view g.deferred with + | Trivial, VNil when not (Options.print_implicits ()) && is_empty (snd g.univ_ineqs) -> "{}" + | _ -> + let form = match g.guard_f with + | Trivial -> "trivial" + | NonTrivial f -> + if !dbg_Rel + || Debug.extreme () + || Options.print_implicits () + then N.term_to_string env f + else "non-trivial" + in + let carry defs = CList.map (fun (_, msg, x) -> msg ^ ": " ^ prob_to_string env x) defs |> to_list |> String.concat ",\n" in + let imps = print_pending_implicits g in + BU.format5 "\n\t{guard_f=%s;\n\t deferred={\n%s};\n\t deferred_to_tac={\n%s};\n\t univ_ineqs={%s};\n\t implicits=%s}\n" + form (carry g.deferred) (carry g.deferred_to_tac) + (ineqs_to_string g.univ_ineqs) imps let new_t_problem wl env lhs rel rhs elt loc = let reason = if !dbg_ExplainRel @@ -4865,7 +4863,7 @@ let with_guard env prob dopt = ({guard_f=(p_guard prob |> NonTrivial); deferred=deferred; deferred_to_tac=defer_to_tac; - univ_ineqs=([], []); + univ_ineqs=(empty, empty); implicits=implicits}) let try_teq smt_ok env t1 t2 : option guard_t = @@ -4950,6 +4948,7 @@ let eq_comp env c1 c2 = sub_or_eq_comp env true c1 c2 ) +val solve_universe_inequalities' (tx:UF.tx) (env : env_t) (vs_ineqs : clist S.universe & clist (S.universe & S.universe)) : unit let solve_universe_inequalities' tx env (variables, ineqs) : unit = //variables: ?u1, ..., ?un are the universes of the inductive types we're trying to compute //ineqs: u1 < v1, ..., un < vn are inequality constraints gathered from checking the inductive definition @@ -4968,27 +4967,27 @@ let solve_universe_inequalities' tx env (variables, ineqs) : unit = | U_unif v0, U_unif v0' -> UF.univ_equiv v0 v0' | _ -> false in - let sols = variables |> List.collect (fun v -> + let sols : clist (S.universe & S.universe) = variables |> CList.collect (fun v -> match SS.compress_univ v with | U_unif _ -> //if it really is a variable, that try to solve it - let lower_bounds_of_v = //lower bounds of v, excluding the other variables - ineqs |> List.collect (fun (u, v') -> + let lower_bounds_of_v : clist S.universe = //lower bounds of v, excluding the other variables + ineqs |> CList.collect (fun (u, v') -> if equiv v v' - then if variables |> BU.for_some (equiv u) - then [] - else [u] - else []) + then if variables |> CList.existsb (equiv u) + then empty + else cons u empty + else empty) in - let lb = N.normalize_universe env (U_max lower_bounds_of_v) in - [(lb, v)] + let lb = N.normalize_universe env (U_max (lower_bounds_of_v |> to_list)) in + Listlike.singleton (lb, v) | _ -> //it may not actually be a variable in case the user provided an explicit universe annnotation //see, e.g., ulib/FStar.Universe.fst - []) in + empty) in //apply all the solutions let _ = let wl = {empty_worklist env with defer_ok=NoDefer} in - sols |> List.map (fun (lb, v) -> + sols |> CList.map (fun (lb, v) -> // printfn "Setting %s to its lower bound %s" (show v) (show lb); match solve_universe_eq (-1) wl lb v with | USolved wl -> () @@ -5009,7 +5008,7 @@ let solve_universe_inequalities' tx env (variables, ineqs) : unit = | _, U_max vs -> vs |> BU.for_some (fun v -> check_ineq (u, v)) | _ -> false in - if ineqs |> BU.for_all (fun (u, v) -> + if ineqs |> CList.for_all (fun (u, v) -> if check_ineq (u, v) then true else (if !dbg_GenUniverses @@ -5051,9 +5050,10 @@ let try_solve_deferred_constraints (defer_ok:defer_ok_t) smt_ok deferred_to_tac_ else [] | _ -> []) |> Setlike.from_list in - let wl = {wl_of_guard env g.deferred with defer_ok=defer_ok - ; smt_ok=smt_ok - ; typeclass_variables } in + let wl = { wl_of_guard env (to_list g.deferred) + with defer_ok=defer_ok + ; smt_ok=smt_ok + ; typeclass_variables } in let fail (d,s) = let msg = explain wl d s in raise_error (p_loc d) Errors.Fatal_ErrorInSolveDeferredConstraints msg @@ -5066,12 +5066,12 @@ let try_solve_deferred_constraints (defer_ok:defer_ok_t) smt_ok deferred_to_tac_ (show (List.length imps_l)); let g = match solve_and_commit wl fail with - | Some (_::_, _, _) when (defer_ok = NoDefer) -> + | Some (deferred, _, _) when VCons? (view deferred) && defer_ok = NoDefer -> failwith "Impossible: Unexpected deferred constraints remain" | Some (deferred, defer_to_tac, imps) -> {g with deferred=deferred; - deferred_to_tac=g.deferred_to_tac@defer_to_tac; + deferred_to_tac=g.deferred_to_tac ++ defer_to_tac; implicits = g.implicits ++ imps} | _ -> @@ -5089,7 +5089,7 @@ let try_solve_deferred_constraints (defer_ok:defer_ok_t) smt_ok deferred_to_tac_ then BU.print2 "ResolveImplicitsHook: Solved deferred to tactic goals, remaining guard is\n%s (and %s implicits)\n" (guard_to_string env g) (show (List.length (Listlike.to_list g.implicits))); - {g with univ_ineqs=([], [])} + {g with univ_ineqs=(empty, empty)} ) (Some (Ident.string_of_lid (Env.current_module env))) "FStar.TypeChecker.Rel.try_solve_deferred_constraints") @@ -5469,16 +5469,13 @@ let check_implicit_solution_and_discharge_guard env end) in if (not force_univ_constraints) && - (List.existsb (fun (reason, _, _) -> reason = Deferred_univ_constraint) g.deferred) + (CList.existsb (fun (reason, _, _) -> reason = Deferred_univ_constraint) g.deferred) then None else let g' = match discharge_guard' (Some (fun () -> BU.format4 "%s (Introduced at %s for %s resolved at %s)" - (show imp_tm) - (Range.string_of_range imp_range) - imp_reason - (Range.string_of_range imp_tm.pos))) + (show imp_tm) (show imp_range) imp_reason (show imp_tm.pos))) env g true with | Some g -> g | None -> failwith "Impossible, with use_smt = true, discharge_guard' must return Some" in @@ -5525,7 +5522,7 @@ let pick_a_univ_deffered_implicit (out : tagged_implicits) let is_tac_implicit_resolved (env:env) (i:implicit) : bool = i.imp_tm |> Free.uvars - |> for_all (fun uv -> Allow_unresolved? (U.ctx_uvar_should_check uv)) + |> Setlike.for_all (fun uv -> Allow_unresolved? (U.ctx_uvar_should_check uv)) // is_tac: this is a call from within the tactic engine, hence do not use @@ -5787,4 +5784,4 @@ let layered_effect_teq env (t1:term) (t2:term) (reason:option string) : guard_t let universe_inequality (u1:universe) (u2:universe) : guard_t = //Printf.printf "Universe inequality %s <= %s\n" (show u1) (show u2); - {trivial_guard with univ_ineqs=([], [u1,u2])} + {trivial_guard with univ_ineqs=(empty, cons (u1,u2) empty)} diff --git a/src/typechecker/FStar.TypeChecker.TcInductive.fst b/src/typechecker/FStar.TypeChecker.TcInductive.fst index 07bf1d3ec7f..83ee3156cf7 100644 --- a/src/typechecker/FStar.TypeChecker.TcInductive.fst +++ b/src/typechecker/FStar.TypeChecker.TcInductive.fst @@ -45,6 +45,7 @@ module PP = FStar.Syntax.Print module C = FStar.Parser.Const open FStar.Class.Show +open FStar.Class.Listlike let dbg_GenUniverses = Debug.get_toggle "GenUniverses" let dbg_LogTypes = Debug.get_toggle "LogTypes" @@ -868,7 +869,7 @@ let check_inductive_well_typedness (env:env_t) (ses:list sigelt) (quals:list qua (* Generalize their universes if not already annotated *) let tcs, datas = let tc_universe_vars = List.map snd tcs in - let g = {g with univ_ineqs=tc_universe_vars, snd (g.univ_ineqs)} in + let g = {g with univ_ineqs = Class.Listlike.from_list (tc_universe_vars), snd (g.univ_ineqs)} in if !dbg_GenUniverses then BU.print1 "@@@@@@Guard before (possible) generalization: %s\n" (Rel.guard_to_string env g); diff --git a/src/typechecker/FStar.TypeChecker.Util.fst b/src/typechecker/FStar.TypeChecker.Util.fst index da545facaf6..cb7dadf055c 100644 --- a/src/typechecker/FStar.TypeChecker.Util.fst +++ b/src/typechecker/FStar.TypeChecker.Util.fst @@ -38,6 +38,8 @@ open FStar.Class.Show open FStar.Class.PP open FStar.Class.Monoid +module Listlike = FStar.Class.Listlike + module SS = FStar.Syntax.Subst module S = FStar.Syntax.Syntax module BU = FStar.Compiler.Util @@ -75,7 +77,7 @@ let close_guard_implicits env solve_deferred (xs:binders) (g:guard_t) : guard_t || solve_deferred then let solve_now, defer = - g.deferred |> List.partition (fun (_, _, p) -> Rel.flex_prob_closing env xs p) + g.deferred |> Listlike.to_list |> List.partition (fun (_, _, p) -> Rel.flex_prob_closing env xs p) in if !dbg_Rel then begin @@ -85,8 +87,8 @@ let close_guard_implicits env solve_deferred (xs:binders) (g:guard_t) : guard_t List.iter (fun (_, s, p) -> BU.print2 "%s: %s\n" s (Rel.prob_to_string env p)) defer; BU.print_string "END\n" end; - let g = Rel.solve_non_tactic_deferred_constraints false env ({g with deferred=solve_now}) in - let g = {g with deferred=defer} in + let g = Rel.solve_non_tactic_deferred_constraints false env ({g with deferred = Listlike.from_list solve_now}) in + let g = {g with deferred = Listlike.from_list defer} in g else g From f8acd55f8c27e7feaef7cb1aa0ab39d194770441 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 7 Oct 2024 23:19:28 -0700 Subject: [PATCH 2/9] snap --- .../generated/FStar_TypeChecker_Common.ml | 63 +- .../FStar_TypeChecker_DeferredImplicits.ml | 12 +- .../generated/FStar_TypeChecker_Env.ml | 67 +- .../generated/FStar_TypeChecker_Rel.ml | 634 +++++++++++++----- .../FStar_TypeChecker_TcInductive.ml | 13 +- .../generated/FStar_TypeChecker_Util.ml | 27 +- 6 files changed, 583 insertions(+), 233 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml index 79cae739e3e..7654a987bed 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml @@ -263,7 +263,8 @@ let (showable_deferred_reason : deferred_reason FStar_Class_Show.showable) = | Deferred_delay_match_heuristic -> "Deferred_delay_match_heuristic" | Deferred_to_user_tac -> "Deferred_to_user_tac") } -type deferred = (deferred_reason * Prims.string * prob) Prims.list +type deferred = + (deferred_reason * Prims.string * prob) FStar_Compiler_CList.clist type univ_ineq = (FStar_Syntax_Syntax.universe * FStar_Syntax_Syntax.universe) type identifier_info = @@ -599,7 +600,9 @@ type guard_t = deferred_to_tac: deferred ; deferred: deferred ; univ_ineqs: - (FStar_Syntax_Syntax.universe Prims.list * univ_ineq Prims.list) ; + (FStar_Syntax_Syntax.universe FStar_Compiler_CList.clist * univ_ineq + FStar_Compiler_CList.clist) + ; implicits: implicits_t } let (__proj__Mkguard_t__item__guard_f : guard_t -> guard_formula) = fun projectee -> @@ -617,7 +620,9 @@ let (__proj__Mkguard_t__item__deferred : guard_t -> deferred) = | { guard_f; deferred_to_tac; deferred = deferred1; univ_ineqs; implicits = implicits1;_} -> deferred1 let (__proj__Mkguard_t__item__univ_ineqs : - guard_t -> (FStar_Syntax_Syntax.universe Prims.list * univ_ineq Prims.list)) + guard_t -> + (FStar_Syntax_Syntax.universe FStar_Compiler_CList.clist * univ_ineq + FStar_Compiler_CList.clist)) = fun projectee -> match projectee with @@ -631,9 +636,21 @@ let (__proj__Mkguard_t__item__implicits : guard_t -> implicits_t) = let (trivial_guard : guard_t) = { guard_f = Trivial; - deferred_to_tac = []; - deferred = []; - univ_ineqs = ([], []); + deferred_to_tac = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); + deferred = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); + univ_ineqs = + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))), + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ()))))); implicits = (Obj.magic (FStar_Class_Listlike.empty () @@ -656,21 +673,33 @@ let (binop_guard : fun g2 -> let uu___ = f g1.guard_f g2.guard_f in let uu___1 = + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) g1.deferred_to_tac + g2.deferred_to_tac in + let uu___2 = + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) g1.deferred g2.deferred in + let uu___3 = + let uu___4 = + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) + (FStar_Pervasives_Native.fst g1.univ_ineqs) + (FStar_Pervasives_Native.fst g2.univ_ineqs) in + let uu___5 = + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) + (FStar_Pervasives_Native.snd g1.univ_ineqs) + (FStar_Pervasives_Native.snd g2.univ_ineqs) in + (uu___4, uu___5) in + let uu___4 = FStar_Class_Monoid.op_Plus_Plus (FStar_Compiler_CList.monoid_clist ()) g1.implicits g2.implicits in { guard_f = uu___; - deferred_to_tac = - (FStar_Compiler_List.op_At g1.deferred_to_tac g2.deferred_to_tac); - deferred = (FStar_Compiler_List.op_At g1.deferred g2.deferred); - univ_ineqs = - ((FStar_Compiler_List.op_At - (FStar_Pervasives_Native.fst g1.univ_ineqs) - (FStar_Pervasives_Native.fst g2.univ_ineqs)), - (FStar_Compiler_List.op_At - (FStar_Pervasives_Native.snd g1.univ_ineqs) - (FStar_Pervasives_Native.snd g2.univ_ineqs))); - implicits = uu___1 + deferred_to_tac = uu___1; + deferred = uu___2; + univ_ineqs = uu___3; + implicits = uu___4 } let (conj_guard : guard_t -> guard_t -> guard_t) = fun g1 -> fun g2 -> binop_guard conj_guard_f g1 g2 diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml index dc30f21cd73..47df6d8b151 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_DeferredImplicits.ml @@ -691,8 +691,11 @@ let (solve_deferred_to_tactic_goals : FStar_Compiler_Effect.failwith "Unexpected problem deferred to tactic") in let eqs = - FStar_Compiler_List.map prob_as_implicit - g.FStar_TypeChecker_Common.deferred_to_tac in + let uu___1 = + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist ()) + g.FStar_TypeChecker_Common.deferred_to_tac in + FStar_Compiler_List.map prob_as_implicit uu___1 in let uu___1 = let uu___2 = FStar_Class_Listlike.to_list @@ -758,7 +761,10 @@ let (solve_deferred_to_tactic_goals : { FStar_TypeChecker_Common.guard_f = (g.FStar_TypeChecker_Common.guard_f); - FStar_TypeChecker_Common.deferred_to_tac = []; + FStar_TypeChecker_Common.deferred_to_tac = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); FStar_TypeChecker_Common.deferred = (g.FStar_TypeChecker_Common.deferred); FStar_TypeChecker_Common.univ_ineqs = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index 0e5330250a6..c8a4d39969d 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -6861,9 +6861,21 @@ let (guard_of_guard_formula : fun g -> { FStar_TypeChecker_Common.guard_f = g; - FStar_TypeChecker_Common.deferred_to_tac = []; - FStar_TypeChecker_Common.deferred = []; - FStar_TypeChecker_Common.univ_ineqs = ([], []); + FStar_TypeChecker_Common.deferred_to_tac = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); + FStar_TypeChecker_Common.deferred = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); + FStar_TypeChecker_Common.univ_ineqs = + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))), + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ()))))); FStar_TypeChecker_Common.implicits = (Obj.magic (FStar_Class_Listlike.empty () @@ -6873,25 +6885,38 @@ let (guard_form : guard_t -> FStar_TypeChecker_Common.guard_formula) = fun g -> g.FStar_TypeChecker_Common.guard_f let (is_trivial : guard_t -> Prims.bool) = fun g -> - match g with - | { FStar_TypeChecker_Common.guard_f = FStar_TypeChecker_Common.Trivial; - FStar_TypeChecker_Common.deferred_to_tac = uu___; - FStar_TypeChecker_Common.deferred = []; - FStar_TypeChecker_Common.univ_ineqs = ([], []); - FStar_TypeChecker_Common.implicits = i;_} -> - FStar_Compiler_CList.for_all - (fun imp -> + let uu___ = + (((FStar_TypeChecker_Common.uu___is_Trivial + g.FStar_TypeChecker_Common.guard_f) + && + (FStar_Class_Listlike.is_empty + (FStar_Compiler_CList.listlike_clist ()) + g.FStar_TypeChecker_Common.deferred)) + && + (FStar_Class_Listlike.is_empty + (FStar_Compiler_CList.listlike_clist ()) + (FStar_Pervasives_Native.fst + g.FStar_TypeChecker_Common.univ_ineqs))) + && + (FStar_Class_Listlike.is_empty + (FStar_Compiler_CList.listlike_clist ()) + (FStar_Pervasives_Native.snd g.FStar_TypeChecker_Common.univ_ineqs)) in + if uu___ + then + FStar_Compiler_CList.for_all + (fun imp -> + (let uu___1 = + FStar_Syntax_Util.ctx_uvar_should_check + imp.FStar_TypeChecker_Common.imp_uvar in + FStar_Syntax_Syntax.uu___is_Allow_unresolved uu___1) || (let uu___1 = - FStar_Syntax_Util.ctx_uvar_should_check - imp.FStar_TypeChecker_Common.imp_uvar in - FStar_Syntax_Syntax.uu___is_Allow_unresolved uu___1) || - (let uu___1 = - FStar_Syntax_Unionfind.find - (imp.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head in - match uu___1 with - | FStar_Pervasives_Native.Some uu___2 -> true - | FStar_Pervasives_Native.None -> false)) i - | uu___ -> false + FStar_Syntax_Unionfind.find + (imp.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head in + match uu___1 with + | FStar_Pervasives_Native.Some uu___2 -> true + | FStar_Pervasives_Native.None -> false)) + g.FStar_TypeChecker_Common.implicits + else false let (is_trivial_guard_formula : guard_t -> Prims.bool) = fun g -> match g with diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index eaff6fdc088..cba963b8727 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -184,11 +184,11 @@ type worklist = attempting: FStar_TypeChecker_Common.probs ; wl_deferred: (Prims.int * FStar_TypeChecker_Common.deferred_reason * lstring * - FStar_TypeChecker_Common.prob) Prims.list + FStar_TypeChecker_Common.prob) FStar_Compiler_CList.clist ; wl_deferred_to_tac: (Prims.int * FStar_TypeChecker_Common.deferred_reason * lstring * - FStar_TypeChecker_Common.prob) Prims.list + FStar_TypeChecker_Common.prob) FStar_Compiler_CList.clist ; ctr: Prims.int ; defer_ok: defer_ok_t ; @@ -208,7 +208,7 @@ let (__proj__Mkworklist__item__attempting : let (__proj__Mkworklist__item__wl_deferred : worklist -> (Prims.int * FStar_TypeChecker_Common.deferred_reason * lstring * - FStar_TypeChecker_Common.prob) Prims.list) + FStar_TypeChecker_Common.prob) FStar_Compiler_CList.clist) = fun projectee -> match projectee with @@ -218,7 +218,7 @@ let (__proj__Mkworklist__item__wl_deferred : let (__proj__Mkworklist__item__wl_deferred_to_tac : worklist -> (Prims.int * FStar_TypeChecker_Common.deferred_reason * lstring * - FStar_TypeChecker_Common.prob) Prims.list) + FStar_TypeChecker_Common.prob) FStar_Compiler_CList.clist) = fun projectee -> match projectee with @@ -279,11 +279,11 @@ let (__proj__Mkworklist__item__typeclass_variables : typeclass_variables;_} -> typeclass_variables let (as_deferred : (Prims.int * FStar_TypeChecker_Common.deferred_reason * lstring * - FStar_TypeChecker_Common.prob) Prims.list -> + FStar_TypeChecker_Common.prob) FStar_Compiler_CList.clist -> FStar_TypeChecker_Common.deferred) = fun wl_def -> - FStar_Compiler_List.map + FStar_Compiler_CList.map (fun uu___ -> match uu___ with | (uu___1, reason, m, p) -> @@ -292,11 +292,11 @@ let (as_wl_deferred : worklist -> FStar_TypeChecker_Common.deferred -> (Prims.int * FStar_TypeChecker_Common.deferred_reason * lstring * - FStar_TypeChecker_Common.prob) Prims.list) + FStar_TypeChecker_Common.prob) FStar_Compiler_CList.clist) = fun wl -> fun d -> - FStar_Compiler_List.map + FStar_Compiler_CList.map (fun uu___ -> match uu___ with | (reason, m, p) -> @@ -543,10 +543,13 @@ let (extend_wl : fun imps -> let uu___ = let uu___1 = as_wl_deferred wl defers in - FStar_Compiler_List.op_At wl.wl_deferred uu___1 in + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) wl.wl_deferred uu___1 in let uu___1 = let uu___2 = as_wl_deferred wl defer_to_tac in - FStar_Compiler_List.op_At wl.wl_deferred_to_tac uu___2 in + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) wl.wl_deferred_to_tac + uu___2 in let uu___2 = FStar_Class_Monoid.op_Plus_Plus (FStar_Compiler_CList.monoid_clist ()) wl.wl_implicits imps in @@ -1162,8 +1165,14 @@ let (empty_worklist : FStar_TypeChecker_Env.env -> worklist) = FStar_Syntax_Free.ord_ctx_uvar)) ()) in { attempting = []; - wl_deferred = []; - wl_deferred_to_tac = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); + wl_deferred_to_tac = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); ctr = Prims.int_zero; defer_ok = DeferAny; smt_ok = true; @@ -1246,9 +1255,14 @@ let (defer : fun msg -> fun prob -> fun wl -> + let uu___ = + Obj.magic + (FStar_Class_Listlike.cons () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())) + ((wl.ctr), reason, msg, prob) (Obj.magic wl.wl_deferred)) in { attempting = (wl.attempting); - wl_deferred = (((wl.ctr), reason, msg, prob) :: (wl.wl_deferred)); + wl_deferred = uu___; wl_deferred_to_tac = (wl.wl_deferred_to_tac); ctr = (wl.ctr); defer_ok = (wl.defer_ok); @@ -2212,13 +2226,19 @@ let (wl_to_string : worklist -> Prims.string) = let probs_to_string ps = let uu___ = FStar_Compiler_List.map (prob_to_string' wl) ps in FStar_Compiler_String.concat "\n\t" uu___ in + let cprobs_to_string ps = + let uu___ = + let uu___1 = FStar_Compiler_CList.map (prob_to_string' wl) ps in + FStar_Class_Listlike.to_list (FStar_Compiler_CList.listlike_clist ()) + uu___1 in + FStar_Compiler_String.concat "\n\t" uu___ in let uu___ = probs_to_string wl.attempting in let uu___1 = let uu___2 = - FStar_Compiler_List.map + FStar_Compiler_CList.map (fun uu___3 -> match uu___3 with | (uu___4, uu___5, uu___6, x) -> x) wl.wl_deferred in - probs_to_string uu___2 in + cprobs_to_string uu___2 in FStar_Compiler_Util.format2 "{ attempting = [ %s ];\ndeferred = [ %s ] }\n" uu___ uu___1 let (showable_wl : worklist FStar_Class_Show.showable) = @@ -5438,38 +5458,55 @@ let rec (solve : worklist -> solution) = solve_rigid_flex_or_flex_rigid_subtyping rank1 tp1 probs1))) | FStar_Pervasives_Native.None -> - (match probs.wl_deferred with - | [] -> - let uu___3 = - let uu___4 = as_deferred probs.wl_deferred_to_tac in - ([], uu___4, (probs.wl_implicits)) in - Success uu___3 - | uu___3 -> + let uu___3 = + Obj.magic + (FStar_Class_Listlike.view () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())) + (Obj.magic probs.wl_deferred)) in + (match uu___3 with + | FStar_Class_Listlike.VNil -> let uu___4 = - FStar_Compiler_List.partition - (fun uu___5 -> - match uu___5 with - | (c, uu___6, uu___7, uu___8) -> c < probs.ctr) + let uu___5 = as_deferred probs.wl_deferred_to_tac in + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))), + uu___5, (probs.wl_implicits)) in + Success uu___4 + | FStar_Class_Listlike.VCons (uu___4, uu___5) -> + let uu___6 = + FStar_Compiler_CList.partition + (fun uu___7 -> + match uu___7 with + | (c, uu___8, uu___9, uu___10) -> c < probs.ctr) probs.wl_deferred in - (match uu___4 with + (match uu___6 with | (attempt1, rest) -> - (match attempt1 with - | [] -> - let uu___5 = - let uu___6 = as_deferred probs.wl_deferred in - let uu___7 = as_deferred probs.wl_deferred_to_tac in - (uu___6, uu___7, (probs.wl_implicits)) in - Success uu___5 - | uu___5 -> - let uu___6 = - let uu___7 = + let uu___7 = + Obj.magic + (FStar_Class_Listlike.view () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())) + (Obj.magic attempt1)) in + (match uu___7 with + | FStar_Class_Listlike.VNil -> + let uu___8 = + let uu___9 = as_deferred probs.wl_deferred in + let uu___10 = as_deferred probs.wl_deferred_to_tac in + (uu___9, uu___10, (probs.wl_implicits)) in + Success uu___8 + | uu___8 -> + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist ()) + attempt1 in FStar_Compiler_List.map - (fun uu___8 -> - match uu___8 with - | (uu___9, uu___10, uu___11, y) -> y) - attempt1 in + (fun uu___12 -> + match uu___12 with + | (uu___13, uu___14, uu___15, y) -> y) + uu___11 in { - attempting = uu___7; + attempting = uu___10; wl_deferred = rest; wl_deferred_to_tac = (probs.wl_deferred_to_tac); ctr = (probs.ctr); @@ -5482,7 +5519,7 @@ let rec (solve : worklist -> solution) = (probs.repr_subcomp_allowed); typeclass_variables = (probs.typeclass_variables) } in - solve uu___6)))) + solve uu___9)))) and (solve_one_universe_eq : FStar_TypeChecker_Common.prob -> FStar_Syntax_Syntax.universe -> @@ -5574,7 +5611,7 @@ and (giveup_or_defer : FStar_Compiler_Util.print2 "\n\t\tDeferring %s\n\t\tBecause %s\n" uu___2 uu___3 else ()); - solve (defer reason msg orig wl)) + (let uu___1 = defer reason msg orig wl in solve uu___1)) else giveup wl msg orig and (giveup_or_defer_flex_flex : FStar_TypeChecker_Common.prob -> @@ -5595,7 +5632,7 @@ and (giveup_or_defer_flex_flex : FStar_Compiler_Util.print2 "\n\t\tDeferring %s\n\t\tBecause %s\n" uu___2 uu___3 else ()); - solve (defer reason msg orig wl)) + (let uu___1 = defer reason msg orig wl in solve uu___1)) else giveup wl msg orig and (defer_to_user_tac : FStar_TypeChecker_Common.prob -> Prims.string -> worklist -> solution) = @@ -5616,7 +5653,10 @@ and (defer_to_user_tac : let uu___3 = FStar_Thunk.mkv reason in ((wl1.ctr), FStar_TypeChecker_Common.Deferred_to_user_tac, uu___3, orig) in - uu___2 :: (wl1.wl_deferred_to_tac) in + Obj.magic + (FStar_Class_Listlike.cons () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())) uu___2 + (Obj.magic wl1.wl_deferred_to_tac)) in { attempting = (wl1.attempting); wl_deferred = (wl1.wl_deferred); @@ -5785,7 +5825,13 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : let wl' = { attempting = probs; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))); wl_deferred_to_tac = (wl4.wl_deferred_to_tac); ctr = (wl4.ctr); @@ -5818,7 +5864,13 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : (FStar_Syntax_Unionfind.commit tx; (let uu___11 = - extend_wl wl4 [] + extend_wl wl4 + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) defer_to_tac imps in FStar_Pervasives_Native.Some uu___11)) @@ -6279,7 +6331,13 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : { attempting = sub_probs; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))); wl_deferred_to_tac = (wl'.wl_deferred_to_tac); @@ -6337,7 +6395,13 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : (wl'.typeclass_variables) } in let wl3 = - extend_wl wl2 [] + extend_wl wl2 + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) defer_to_tac imps in let g = FStar_Compiler_List.fold_left @@ -6937,7 +7001,10 @@ and (try_solve_without_smt_or_else : let wl' = { attempting = []; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); wl_deferred_to_tac = (wl.wl_deferred_to_tac); ctr = (wl.ctr); defer_ok = NoDefer; @@ -6956,7 +7023,13 @@ and (try_solve_without_smt_or_else : match uu___ with | Success (uu___1, defer_to_tac, imps) -> (FStar_Syntax_Unionfind.commit tx; - (let wl1 = extend_wl wl [] defer_to_tac imps in solve wl1)) + (let wl1 = + extend_wl wl + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))) + defer_to_tac imps in + solve wl1)) | Failed (p, s) -> (FStar_Syntax_Unionfind.rollback tx; else_solve wl (p, s)) and (try_solve_then_or_else : @@ -6971,7 +7044,10 @@ and (try_solve_then_or_else : let empty_wl = { attempting = []; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); wl_deferred_to_tac = (wl.wl_deferred_to_tac); ctr = (wl.ctr); defer_ok = NoDefer; @@ -6990,7 +7066,13 @@ and (try_solve_then_or_else : match uu___ with | Success (uu___1, defer_to_tac, imps) -> (FStar_Syntax_Unionfind.commit tx; - (let wl1 = extend_wl wl [] defer_to_tac imps in then_solve wl1)) + (let wl1 = + extend_wl wl + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))) + defer_to_tac imps in + then_solve wl1)) | Failed (p, s) -> (FStar_Syntax_Unionfind.rollback tx; else_solve wl) and (try_solve_probs_without_smt : @@ -7006,7 +7088,10 @@ and (try_solve_probs_without_smt : let wl'1 = { attempting = probs1; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))); wl_deferred_to_tac = (wl.wl_deferred_to_tac); ctr = (wl.ctr); defer_ok = NoDefer; @@ -7023,7 +7108,12 @@ and (try_solve_probs_without_smt : let uu___1 = solve wl'1 in (match uu___1 with | Success (uu___2, defer_to_tac, imps) -> - let wl1 = extend_wl wl [] defer_to_tac imps in + let wl1 = + extend_wl wl + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))) + defer_to_tac imps in FStar_Pervasives.Inl wl1 | Failed (uu___2, ls) -> FStar_Pervasives.Inr ls) and (solve_t : tprob -> worklist -> solution) = @@ -7742,7 +7832,13 @@ and (solve_t_flex_rigid_eq : { attempting = sub_probs; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))); wl_deferred_to_tac = (wl5.wl_deferred_to_tac); @@ -7774,7 +7870,13 @@ and (solve_t_flex_rigid_eq : imps) -> let wl6 = - extend_wl wl5 [] + extend_wl wl5 + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) defer_to_tac imps in (FStar_Syntax_Unionfind.commit @@ -9018,7 +9120,13 @@ and (solve_t' : tprob -> worklist -> solution) = attempting = [FStar_TypeChecker_Common.TProb prob]; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))); wl_deferred_to_tac = (wl4.wl_deferred_to_tac); ctr = (wl4.ctr); @@ -9082,24 +9190,32 @@ and (solve_t' : tprob -> worklist -> solution) = tx; (let uu___13 = let uu___14 = - let uu___15 = - let uu___16 = + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist + ()) defer_to_tac + defer_to_tac' in + let uu___15 = + let uu___16 = + let uu___17 = FStar_Class_Monoid.op_Plus_Plus (FStar_Compiler_CList.monoid_clist ()) imps imps' in FStar_Class_Monoid.op_Plus_Plus (FStar_Compiler_CList.monoid_clist - ()) uu___16 + ()) uu___17 g_pat_as_exp.FStar_TypeChecker_Common.implicits in FStar_Class_Monoid.op_Plus_Plus (FStar_Compiler_CList.monoid_clist - ()) uu___15 + ()) uu___16 g_pat_term.FStar_TypeChecker_Common.implicits in - extend_wl wl4 [] - (FStar_Compiler_List.op_At - defer_to_tac - defer_to_tac') - uu___14 in + extend_wl wl4 + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) + uu___14 uu___15 in FStar_Pervasives_Native.Some uu___13)) | Failed uu___11 -> @@ -10156,7 +10272,13 @@ and (solve_t' : tprob -> worklist -> solution) = solve { attempting = [ref_prob1]; - wl_deferred = []; + wl_deferred = + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))); wl_deferred_to_tac = (wl2.wl_deferred_to_tac); ctr = (wl2.ctr); @@ -10236,7 +10358,13 @@ and (solve_t' : tprob -> worklist -> solution) = (wl3.typeclass_variables) } in let wl5 = - extend_wl wl4 [] + extend_wl wl4 + (Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) defer_to_tac imps in let uu___16 = attempt [base_prob] wl5 in @@ -13054,9 +13182,25 @@ and (solve_c : "effect universes" in (match uu___6 with | (p, wl2) -> - ((FStar_Compiler_List.op_At univ_sub_probs - [p]), wl2))) ([], wl) - c1_comp.FStar_Syntax_Syntax.comp_univs + let uu___7 = + let uu___8 = + Obj.magic + (FStar_Class_Listlike.cons () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())) p + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) in + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) + univ_sub_probs uu___8 in + (uu___7, wl2))) + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))), + wl) c1_comp.FStar_Syntax_Syntax.comp_univs c2_comp.FStar_Syntax_Syntax.comp_univs in match uu___4 with | (univ_sub_probs, wl1) -> @@ -13081,29 +13225,52 @@ and (solve_c : "effect arg" in (match uu___12 with | (p, wl4) -> - ((p :: arg_sub_probs), wl4))) + let uu___13 = + Obj.magic + (FStar_Class_Listlike.cons () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())) p + (Obj.magic arg_sub_probs)) in + (uu___13, wl4))) c1_comp.FStar_Syntax_Syntax.effect_args - c2_comp.FStar_Syntax_Syntax.effect_args ([], wl2) in + c2_comp.FStar_Syntax_Syntax.effect_args + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist ())))), + wl2) in (match uu___6 with | (arg_sub_probs, wl3) -> let sub_probs = let uu___7 = let uu___8 = let uu___9 = - FStar_Compiler_List.map + FStar_Compiler_CList.map (fun uu___10 -> match uu___10 with | (uu___11, uu___12, p) -> p) g_lift.FStar_TypeChecker_Common.deferred in - FStar_Compiler_List.op_At arg_sub_probs - uu___9 in - FStar_Compiler_List.op_At [ret_sub_prob] - uu___8 in - FStar_Compiler_List.op_At univ_sub_probs uu___7 in + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) + arg_sub_probs uu___9 in + Obj.magic + (FStar_Class_Listlike.cons () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())) ret_sub_prob + (Obj.magic uu___8)) in + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) + univ_sub_probs uu___7 in + let sub_probs1 = + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist ()) + sub_probs in let guard = let guard1 = let uu___7 = - FStar_Compiler_List.map p_guard sub_probs in + FStar_Compiler_List.map p_guard sub_probs1 in FStar_Syntax_Util.mk_conj_l uu___7 in match g_lift.FStar_TypeChecker_Common.guard_f with @@ -13134,7 +13301,7 @@ and (solve_c : let wl5 = solve_prob orig (FStar_Pervasives_Native.Some guard) [] wl4 in - let uu___7 = attempt sub_probs wl5 in + let uu___7 = attempt sub_probs1 wl5 in solve uu___7)))) in let should_fail_since_repr_subcomp_not_allowed repr_subcomp_allowed c11 c21 = @@ -14053,86 +14220,103 @@ let (print_pending_implicits : FStar_TypeChecker_Common.guard_t -> Prims.string) = fun g -> let uu___ = - let uu___1 = - FStar_Class_Listlike.to_list (FStar_Compiler_CList.listlike_clist ()) - g.FStar_TypeChecker_Common.implicits in - FStar_Compiler_List.map + FStar_Compiler_CList.map (fun i -> FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu - i.FStar_TypeChecker_Common.imp_uvar) uu___1 in + i.FStar_TypeChecker_Common.imp_uvar) + g.FStar_TypeChecker_Common.implicits in FStar_Class_Show.show - (FStar_Class_Show.show_list + (FStar_Compiler_CList.showable_clist (FStar_Class_Show.printableshow FStar_Class_Printable.printable_string)) uu___ let (ineqs_to_string : - (FStar_Syntax_Syntax.universe Prims.list * (FStar_Syntax_Syntax.universe * - FStar_Syntax_Syntax.universe) Prims.list) -> Prims.string) + (FStar_Syntax_Syntax.universe FStar_Compiler_CList.clist * + (FStar_Syntax_Syntax.universe * FStar_Syntax_Syntax.universe) + FStar_Compiler_CList.clist) -> Prims.string) = fun ineqs -> - let vars = - let uu___ = - FStar_Compiler_List.map - (FStar_Class_Show.show FStar_Syntax_Print.showable_univ) - (FStar_Pervasives_Native.fst ineqs) in - FStar_Compiler_String.concat ", " uu___ in - let ineqs1 = - let uu___ = - FStar_Compiler_List.map - (fun uu___1 -> - match uu___1 with - | (u1, u2) -> - let uu___2 = - FStar_Class_Show.show FStar_Syntax_Print.showable_univ u1 in - let uu___3 = - FStar_Class_Show.show FStar_Syntax_Print.showable_univ u2 in - FStar_Compiler_Util.format2 "%s < %s" uu___2 uu___3) - (FStar_Pervasives_Native.snd ineqs) in - FStar_Compiler_String.concat ", " uu___ in - FStar_Compiler_Util.format2 "Solving for {%s}; inequalities are {%s}" - vars ineqs1 + let uu___ = ineqs in + match uu___ with + | (vars, ineqs1) -> + let ineqs2 = + FStar_Compiler_CList.map + (fun uu___1 -> + match uu___1 with + | (u1, u2) -> + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ + u1 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ + u2 in + FStar_Compiler_Util.format2 "%s < %s" uu___2 uu___3) + ineqs1 in + let uu___1 = + FStar_Class_Show.show + (FStar_Compiler_CList.showable_clist + FStar_Syntax_Print.showable_univ) vars in + let uu___2 = + FStar_Class_Show.show + (FStar_Compiler_CList.showable_clist + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string)) ineqs2 in + FStar_Compiler_Util.format2 "Solving for %s; inequalities are %s" + uu___1 uu___2 let (guard_to_string : FStar_TypeChecker_Env.env -> FStar_TypeChecker_Common.guard_t -> Prims.string) = fun env -> fun g -> - match ((g.FStar_TypeChecker_Common.guard_f), - (g.FStar_TypeChecker_Common.deferred), - (g.FStar_TypeChecker_Common.univ_ineqs)) - with - | (FStar_TypeChecker_Common.Trivial, [], (uu___, [])) when - let uu___1 = FStar_Options.print_implicits () in - Prims.op_Negation uu___1 -> "{}" - | uu___ -> + let uu___ = + let uu___1 = + Obj.magic + (FStar_Class_Listlike.view () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())) + (Obj.magic g.FStar_TypeChecker_Common.deferred)) in + ((g.FStar_TypeChecker_Common.guard_f), uu___1) in + match uu___ with + | (FStar_TypeChecker_Common.Trivial, FStar_Class_Listlike.VNil) when + (let uu___1 = FStar_Options.print_implicits () in + Prims.op_Negation uu___1) && + (FStar_Class_Listlike.is_empty + (FStar_Compiler_CList.listlike_clist ()) + (FStar_Pervasives_Native.snd + g.FStar_TypeChecker_Common.univ_ineqs)) + -> "{}" + | uu___1 -> let form = match g.FStar_TypeChecker_Common.guard_f with | FStar_TypeChecker_Common.Trivial -> "trivial" | FStar_TypeChecker_Common.NonTrivial f -> - let uu___1 = + let uu___2 = ((FStar_Compiler_Effect.op_Bang dbg_Rel) || (FStar_Compiler_Debug.extreme ())) || (FStar_Options.print_implicits ()) in - if uu___1 + if uu___2 then FStar_TypeChecker_Normalize.term_to_string env f else "non-trivial" in let carry defs = - let uu___1 = - FStar_Compiler_List.map - (fun uu___2 -> - match uu___2 with - | (uu___3, msg, x) -> - let uu___4 = - let uu___5 = prob_to_string env x in - Prims.strcat ": " uu___5 in - Prims.strcat msg uu___4) defs in - FStar_Compiler_String.concat ",\n" uu___1 in + let uu___2 = + let uu___3 = + FStar_Compiler_CList.map + (fun uu___4 -> + match uu___4 with + | (uu___5, msg, x) -> + let uu___6 = + let uu___7 = prob_to_string env x in + Prims.strcat ": " uu___7 in + Prims.strcat msg uu___6) defs in + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist ()) uu___3 in + FStar_Compiler_String.concat ",\n" uu___2 in let imps = print_pending_implicits g in - let uu___1 = carry g.FStar_TypeChecker_Common.deferred in - let uu___2 = carry g.FStar_TypeChecker_Common.deferred_to_tac in - let uu___3 = ineqs_to_string g.FStar_TypeChecker_Common.univ_ineqs in + let uu___2 = carry g.FStar_TypeChecker_Common.deferred in + let uu___3 = carry g.FStar_TypeChecker_Common.deferred_to_tac in + let uu___4 = ineqs_to_string g.FStar_TypeChecker_Common.univ_ineqs in FStar_Compiler_Util.format5 "\n\t{guard_f=%s;\n\t deferred={\n%s};\n\t deferred_to_tac={\n%s};\n\t univ_ineqs={%s};\n\t implicits=%s}\n" - form uu___1 uu___2 uu___3 imps + form uu___2 uu___3 uu___4 imps let (new_t_problem : worklist -> FStar_TypeChecker_Env.env -> @@ -14279,7 +14463,15 @@ let (with_guard : (FStar_TypeChecker_Common.NonTrivial (p_guard prob)); FStar_TypeChecker_Common.deferred_to_tac = defer_to_tac; FStar_TypeChecker_Common.deferred = deferred; - FStar_TypeChecker_Common.univ_ineqs = ([], []); + FStar_TypeChecker_Common.univ_ineqs = + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist ())))), + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist ()))))); FStar_TypeChecker_Common.implicits = implicits } in FStar_Pervasives_Native.Some uu___1)) @@ -14580,10 +14772,10 @@ let (eq_comp : sub_or_eq_comp env true c1 c2) let (solve_universe_inequalities' : FStar_Syntax_Unionfind.tx -> - FStar_TypeChecker_Env.env -> - (FStar_Syntax_Syntax.universe Prims.list * + FStar_TypeChecker_Env.env_t -> + (FStar_Syntax_Syntax.universe FStar_Compiler_CList.clist * (FStar_Syntax_Syntax.universe * FStar_Syntax_Syntax.universe) - Prims.list) -> unit) + FStar_Compiler_CList.clist) -> unit) = fun tx -> fun env -> @@ -14613,29 +14805,73 @@ let (solve_universe_inequalities' : v0') -> FStar_Syntax_Unionfind.univ_equiv v0 v0' | uu___2 -> false in let sols = - FStar_Compiler_List.collect - (fun v -> - let uu___1 = FStar_Syntax_Subst.compress_univ v in - match uu___1 with - | FStar_Syntax_Syntax.U_unif uu___2 -> - let lower_bounds_of_v = - FStar_Compiler_List.collect - (fun uu___3 -> - match uu___3 with - | (u, v') -> - let uu___4 = equiv v v' in - if uu___4 - then - let uu___5 = - FStar_Compiler_Util.for_some (equiv u) - variables in - (if uu___5 then [] else [u]) - else []) ineqs in - let lb = - FStar_TypeChecker_Normalize.normalize_universe env - (FStar_Syntax_Syntax.U_max lower_bounds_of_v) in - [(lb, v)] - | uu___2 -> []) variables in + FStar_Compiler_CList.collect + (fun uu___1 -> + (fun v -> + let uu___1 = FStar_Syntax_Subst.compress_univ v in + match uu___1 with + | FStar_Syntax_Syntax.U_unif uu___2 -> + Obj.magic + (Obj.repr + (let lower_bounds_of_v = + FStar_Compiler_CList.collect + (fun uu___3 -> + (fun uu___3 -> + match uu___3 with + | (u, v') -> + let uu___4 = equiv v v' in + if uu___4 + then + let uu___5 = + FStar_Compiler_CList.existsb + (equiv u) variables in + (if uu___5 + then + Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ()))) + else + Obj.magic + (FStar_Class_Listlike.cons + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())) u + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ()))))) + else + Obj.magic + (FStar_Class_Listlike.empty + () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())))) uu___3) + ineqs in + let lb = + let uu___3 = + let uu___4 = + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist + ()) lower_bounds_of_v in + FStar_Syntax_Syntax.U_max uu___4 in + FStar_TypeChecker_Normalize.normalize_universe + env uu___3 in + FStar_Class_Listlike.singleton + (FStar_Compiler_CList.listlike_clist ()) + (lb, v))) + | uu___2 -> + Obj.magic + (Obj.repr + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist ()))))) + uu___1) variables in let uu___1 = let wl = let uu___2 = empty_worklist env in @@ -14652,7 +14888,7 @@ let (solve_universe_inequalities' : repr_subcomp_allowed = (uu___2.repr_subcomp_allowed); typeclass_variables = (uu___2.typeclass_variables) } in - FStar_Compiler_List.map + FStar_Compiler_CList.map (fun uu___2 -> match uu___2 with | (lb, v) -> @@ -14690,7 +14926,7 @@ let (solve_universe_inequalities' : (fun v2 -> check_ineq (u1, v2)) vs | uu___3 -> false) in let uu___2 = - FStar_Compiler_Util.for_all + FStar_Compiler_CList.for_all (fun uu___3 -> match uu___3 with | (u, v) -> @@ -14734,9 +14970,10 @@ let (solve_universe_inequalities' : (Obj.magic "Failed to solve universe inequalities for inductives")) let (solve_universe_inequalities : - FStar_TypeChecker_Env.env -> - (FStar_Syntax_Syntax.universe Prims.list * (FStar_Syntax_Syntax.universe - * FStar_Syntax_Syntax.universe) Prims.list) -> unit) + FStar_TypeChecker_Env.env_t -> + (FStar_Syntax_Syntax.universe FStar_Compiler_CList.clist * + (FStar_Syntax_Syntax.universe * FStar_Syntax_Syntax.universe) + FStar_Compiler_CList.clist) -> unit) = fun env -> fun ineqs -> @@ -14811,7 +15048,11 @@ let (try_solve_deferred_constraints : FStar_Syntax_Free.ord_ctx_uvar)) uu___3) in let wl = let uu___3 = - wl_of_guard env g.FStar_TypeChecker_Common.deferred in + let uu___4 = + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist ()) + g.FStar_TypeChecker_Common.deferred in + wl_of_guard env uu___4 in { attempting = (uu___3.attempting); wl_deferred = (uu___3.wl_deferred); @@ -14860,13 +15101,26 @@ let (try_solve_deferred_constraints : let uu___4 = solve_and_commit wl fail in match uu___4 with | FStar_Pervasives_Native.Some - (uu___5::uu___6, uu___7, uu___8) when - defer_ok = NoDefer -> + (deferred, uu___5, uu___6) when + (let uu___7 = + Obj.magic + (FStar_Class_Listlike.view () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ())) (Obj.magic deferred)) in + FStar_Class_Listlike.uu___is_VCons uu___7) && + (defer_ok = NoDefer) + -> FStar_Compiler_Effect.failwith "Impossible: Unexpected deferred constraints remain" | FStar_Pervasives_Native.Some (deferred, defer_to_tac, imps) -> let uu___5 = + FStar_Class_Monoid.op_Plus_Plus + (FStar_Compiler_CList.monoid_clist ()) + g.FStar_TypeChecker_Common.deferred_to_tac + defer_to_tac in + let uu___6 = FStar_Class_Monoid.op_Plus_Plus (FStar_Compiler_CList.monoid_clist ()) g.FStar_TypeChecker_Common.implicits imps in @@ -14874,13 +15128,11 @@ let (try_solve_deferred_constraints : FStar_TypeChecker_Common.guard_f = (g.FStar_TypeChecker_Common.guard_f); FStar_TypeChecker_Common.deferred_to_tac = - (FStar_Compiler_List.op_At - g.FStar_TypeChecker_Common.deferred_to_tac - defer_to_tac); + uu___5; FStar_TypeChecker_Common.deferred = deferred; FStar_TypeChecker_Common.univ_ineqs = (g.FStar_TypeChecker_Common.univ_ineqs); - FStar_TypeChecker_Common.implicits = uu___5 + FStar_TypeChecker_Common.implicits = uu___6 } | uu___5 -> FStar_Compiler_Effect.failwith @@ -14929,7 +15181,16 @@ let (try_solve_deferred_constraints : (g2.FStar_TypeChecker_Common.deferred_to_tac); FStar_TypeChecker_Common.deferred = (g2.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = ([], []); + FStar_TypeChecker_Common.univ_ineqs = + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist ())))), + (Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic + (FStar_Compiler_CList.listlike_clist + ()))))); FStar_TypeChecker_Common.implicits = (g2.FStar_TypeChecker_Common.implicits) }))) uu___1 @@ -15814,7 +16075,7 @@ let (check_implicit_solution_and_discharge_guard : (Obj.magic uu___5))) in let uu___2 = (Prims.op_Negation force_univ_constraints) && - (FStar_Compiler_List.existsb + (FStar_Compiler_CList.existsb (fun uu___3 -> match uu___3 with | (reason, uu___4, uu___5) -> @@ -15833,10 +16094,12 @@ let (check_implicit_solution_and_discharge_guard : FStar_Class_Show.show FStar_Syntax_Print.showable_term imp_tm in let uu___7 = - FStar_Compiler_Range_Ops.string_of_range + FStar_Class_Show.show + FStar_Compiler_Range_Ops.showable_range imp_range in let uu___8 = - FStar_Compiler_Range_Ops.string_of_range + FStar_Class_Show.show + FStar_Compiler_Range_Ops.showable_range imp_tm.FStar_Syntax_Syntax.pos in FStar_Compiler_Util.format4 "%s (Introduced at %s for %s resolved at %s)" @@ -16747,6 +17010,17 @@ let (universe_inequality : = fun u1 -> fun u2 -> + let uu___ = + let uu___1 = + Obj.magic + (FStar_Class_Listlike.cons () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())) (u1, u2) + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))) in + ((Obj.magic + (FStar_Class_Listlike.empty () + (Obj.magic (FStar_Compiler_CList.listlike_clist ())))), + uu___1) in { FStar_TypeChecker_Common.guard_f = (FStar_TypeChecker_Common.trivial_guard.FStar_TypeChecker_Common.guard_f); @@ -16754,7 +17028,7 @@ let (universe_inequality : (FStar_TypeChecker_Common.trivial_guard.FStar_TypeChecker_Common.deferred_to_tac); FStar_TypeChecker_Common.deferred = (FStar_TypeChecker_Common.trivial_guard.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = ([], [(u1, u2)]); + FStar_TypeChecker_Common.univ_ineqs = uu___; FStar_TypeChecker_Common.implicits = (FStar_TypeChecker_Common.trivial_guard.FStar_TypeChecker_Common.implicits) } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcInductive.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcInductive.ml index c55093f1e83..33e8b5e0046 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcInductive.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcInductive.ml @@ -2375,6 +2375,14 @@ let (check_inductive_well_typedness : FStar_Compiler_List.map FStar_Pervasives_Native.snd tcs in let g3 = + let uu___5 = + let uu___6 = + FStar_Class_Listlike.from_list + (FStar_Compiler_CList.listlike_clist ()) + tc_universe_vars in + (uu___6, + (FStar_Pervasives_Native.snd + g2.FStar_TypeChecker_Common.univ_ineqs)) in { FStar_TypeChecker_Common.guard_f = (g2.FStar_TypeChecker_Common.guard_f); @@ -2382,10 +2390,7 @@ let (check_inductive_well_typedness : (g2.FStar_TypeChecker_Common.deferred_to_tac); FStar_TypeChecker_Common.deferred = (g2.FStar_TypeChecker_Common.deferred); - FStar_TypeChecker_Common.univ_ineqs = - (tc_universe_vars, - (FStar_Pervasives_Native.snd - g2.FStar_TypeChecker_Common.univ_ineqs)); + FStar_TypeChecker_Common.univ_ineqs = uu___5; FStar_TypeChecker_Common.implicits = (g2.FStar_TypeChecker_Common.implicits) } in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml index bd1ee0d13de..8644b5a8dec 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Util.ml @@ -58,12 +58,16 @@ let (close_guard_implicits : if uu___ then let uu___1 = + let uu___2 = + FStar_Class_Listlike.to_list + (FStar_Compiler_CList.listlike_clist ()) + g.FStar_TypeChecker_Common.deferred in FStar_Compiler_List.partition - (fun uu___2 -> - match uu___2 with - | (uu___3, uu___4, p) -> + (fun uu___3 -> + match uu___3 with + | (uu___4, uu___5, p) -> FStar_TypeChecker_Rel.flex_prob_closing env xs p) - g.FStar_TypeChecker_Common.deferred in + uu___2 in match uu___1 with | (solve_now, defer) -> ((let uu___3 = FStar_Compiler_Effect.op_Bang dbg_Rel in @@ -92,26 +96,33 @@ let (close_guard_implicits : FStar_Compiler_Util.print_string "END\n") else ()); (let g1 = - FStar_TypeChecker_Rel.solve_non_tactic_deferred_constraints - false env + let uu___3 = + let uu___4 = + FStar_Class_Listlike.from_list + (FStar_Compiler_CList.listlike_clist ()) solve_now in { FStar_TypeChecker_Common.guard_f = (g.FStar_TypeChecker_Common.guard_f); FStar_TypeChecker_Common.deferred_to_tac = (g.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = solve_now; + FStar_TypeChecker_Common.deferred = uu___4; FStar_TypeChecker_Common.univ_ineqs = (g.FStar_TypeChecker_Common.univ_ineqs); FStar_TypeChecker_Common.implicits = (g.FStar_TypeChecker_Common.implicits) } in + FStar_TypeChecker_Rel.solve_non_tactic_deferred_constraints + false env uu___3 in let g2 = + let uu___3 = + FStar_Class_Listlike.from_list + (FStar_Compiler_CList.listlike_clist ()) defer in { FStar_TypeChecker_Common.guard_f = (g1.FStar_TypeChecker_Common.guard_f); FStar_TypeChecker_Common.deferred_to_tac = (g1.FStar_TypeChecker_Common.deferred_to_tac); - FStar_TypeChecker_Common.deferred = defer; + FStar_TypeChecker_Common.deferred = uu___3; FStar_TypeChecker_Common.univ_ineqs = (g1.FStar_TypeChecker_Common.univ_ineqs); FStar_TypeChecker_Common.implicits = From c3a6cf2d4fb053752599db1bb97a1854fe0c6ad3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 15:10:40 -0700 Subject: [PATCH 3/9] ulib: reducing some warnings --- ulib/FStar.Int.fsti | 2 -- ulib/FStar.LexicographicOrdering.fst | 2 +- ulib/FStar.Math.Lemmas.fst | 2 +- ulib/FStar.UInt128.fst | 3 +++ ulib/FStar.WellFounded.Util.fst | 2 +- ulib/FStar.WellFounded.fst | 2 +- ulib/LowStar.BufferView.Down.fst | 12 +++--------- ulib/LowStar.Monotonic.Buffer.fst | 1 + ulib/experimental/FStar.InteractiveHelpers.Base.fst | 2 +- .../FStar.InteractiveHelpers.Effectful.fst | 2 +- .../FStar.InteractiveHelpers.ExploreTerm.fst | 2 +- .../experimental/FStar.InteractiveHelpers.Output.fst | 2 +- .../FStar.InteractiveHelpers.PostProcess.fst | 2 +- .../FStar.InteractiveHelpers.Propositions.fst | 2 +- ulib/experimental/FStar.Sequence.Permutation.fst | 3 +++ 15 files changed, 20 insertions(+), 21 deletions(-) diff --git a/ulib/FStar.Int.fsti b/ulib/FStar.Int.fsti index e96633055bb..eb4ba64e0d1 100644 --- a/ulib/FStar.Int.fsti +++ b/ulib/FStar.Int.fsti @@ -183,8 +183,6 @@ let gte #n (a:int_t n) (b:int_t n) : Tot bool = a >= b let lt #n (a:int_t n) (b:int_t n) : Tot bool = a < b let lte #n (a:int_t n) (b:int_t n) : Tot bool = a <= b -#push-options "--initial_fuel 1 --max_fuel 1" - /// Casts let to_uint (#n:pos) (x:int_t n) : Tot (UInt.uint_t n) = diff --git a/ulib/FStar.LexicographicOrdering.fst b/ulib/FStar.LexicographicOrdering.fst index ba97a583e9a..ef1349c1151 100644 --- a/ulib/FStar.LexicographicOrdering.fst +++ b/ulib/FStar.LexicographicOrdering.fst @@ -17,7 +17,7 @@ *) module FStar.LexicographicOrdering -#push-options "--warn_error -242" //no inner let recs in SMT +#set-options "--warn_error -242" //no inner let recs in SMT open FStar.ReflexiveTransitiveClosure open FStar.WellFounded diff --git a/ulib/FStar.Math.Lemmas.fst b/ulib/FStar.Math.Lemmas.fst index 3dc80828f8b..7f3cbbc03f5 100644 --- a/ulib/FStar.Math.Lemmas.fst +++ b/ulib/FStar.Math.Lemmas.fst @@ -18,7 +18,7 @@ module FStar.Math.Lemmas open FStar.Mul open FStar.Math.Lib -#push-options "--fuel 0 --ifuel 0" +#set-options "--fuel 0 --ifuel 0" (* Lemma: definition of Euclidean division *) let euclidean_div_axiom a b = () diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index 537beb35331..444ce8b0882 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -337,6 +337,8 @@ let sub_mod_wrap1_ok a b = () end #pop-options +#pop-options + let sum_lt (a1 a2 b1 b2:nat) : Lemma (requires (a1 + a2 < b1 + b2 /\ a1 >= b1)) @@ -372,6 +374,7 @@ let sub_mod (a b: t) : Pure t else sub_mod_wrap_ok a b); sub_mod_impl a b #pop-options + #restart-solver val shift_bound : #n:nat -> num:UInt.uint_t n -> n':nat -> diff --git a/ulib/FStar.WellFounded.Util.fst b/ulib/FStar.WellFounded.Util.fst index a738123731b..98661a47d84 100644 --- a/ulib/FStar.WellFounded.Util.fst +++ b/ulib/FStar.WellFounded.Util.fst @@ -1,7 +1,7 @@ module FStar.WellFounded.Util open FStar.WellFounded -#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok +#set-options "--warn_error -242" //inner let recs not encoded to SMT; ok let intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a) : Lemma diff --git a/ulib/FStar.WellFounded.fst b/ulib/FStar.WellFounded.fst index 97ee6223a4b..eab78d99e16 100644 --- a/ulib/FStar.WellFounded.fst +++ b/ulib/FStar.WellFounded.fst @@ -22,7 +22,7 @@ module FStar.WellFounded -#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok +#set-options "--warn_error -242" //inner let recs not encoded to SMT; ok let binrel (a:Type) = a -> a -> Type diff --git a/ulib/LowStar.BufferView.Down.fst b/ulib/LowStar.BufferView.Down.fst index 2ce8aee0578..b5ecee6fc50 100644 --- a/ulib/LowStar.BufferView.Down.fst +++ b/ulib/LowStar.BufferView.Down.fst @@ -209,6 +209,7 @@ let sel'_tail #a #b v es i = FStar.Math.Lemmas.lemma_mod_sub i n 1; FStar.Math.Lemmas.add_div_mod_1 j n; assert (j / n == (i / n) - 1) +#pop-options val as_seq'_sel' (#a #b: _) (v:view a b) @@ -220,13 +221,6 @@ val as_seq'_sel' (#a #b: _) sel' v es i == Seq.index (as_seq' es v) i)) (decreases (Seq.length es)) -//flaky -#reset-options -#set-options "--smtencoding.elim_box true" -#set-options "--smtencoding.l_arith_repr native" -#set-options "--smtencoding.nl_arith_repr wrapped" -#set-options "--z3rlimit_factor 10" //just being conservative -#set-options "--initial_fuel 1 --max_fuel 1 --max_ifuel 0" let rec as_seq'_sel' #a #b v es i = as_seq'_len es v; let n : pos = View?.n v in @@ -251,7 +245,6 @@ let rec as_seq'_sel' #a #b v es i = Seq.index (as_seq' as' v) j); sel'_tail v es i end -#reset-options let as_seq_sel #b h vb i = indexing vb i; @@ -349,7 +342,7 @@ let rec upd_seq'_spec (#a #b: _) (v:view a b) (s:Seq.seq b{Seq.length s % View?. assert (es `Seq.equal` Seq.cons (View?.put v pfx) as'); as_seq'_cons v (View?.put v pfx) as' -#set-options "--z3rlimit 20" +#push-options "--z3rlimit 20" let upd_seq_spec (#b: _) (h:HS.mem) (vb:buffer b{live h vb}) (s:Seq.seq b{Seq.length s = length vb}) = let h' = upd_seq h vb s in Math.cancel_mul_mod (B.length (as_buffer vb)) (View?.n (get_view vb)); @@ -367,3 +360,4 @@ let upd_seq_spec (#b: _) (h:HS.mem) (vb:buffer b{live h vb}) (s:Seq.seq b{Seq.le FStar.Classical.forall_intro_2 (fun as1 as2 -> Classical.move_requires (as_seq'_injective v as1) as2 <: Lemma ((as_seq' as1 v `Seq.equal` as_seq' as2 v) ==> (as1 `Seq.equal` as2))) +#pop-options diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst index dc5596024b2..684ff260f0d 100644 --- a/ulib/LowStar.Monotonic.Buffer.fst +++ b/ulib/LowStar.Monotonic.Buffer.fst @@ -1876,6 +1876,7 @@ let blit #a #rrel1 #rrel2 #rel1 #rel2 src idx_src dst idx_dst len = assert (h1 == g_upd_seq dst (Seq.slice s2' 0 (U32.v length2)) h); g_upd_seq_as_seq dst (Seq.slice s2' 0 (U32.v length2)) h //for modifies clause | _, _ -> () +#pop-options #restart-solver #push-options "--z3rlimit 256 --max_fuel 0 --max_ifuel 1 --initial_ifuel 1 --z3cliopt smt.qi.EAGER_THRESHOLD=4" diff --git a/ulib/experimental/FStar.InteractiveHelpers.Base.fst b/ulib/experimental/FStar.InteractiveHelpers.Base.fst index 902544301c9..ee4baabf472 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Base.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Base.fst @@ -4,7 +4,7 @@ open FStar.List.Tot open FStar.Tactics open FStar.Mul -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Utilities *) val bv_eq : bv -> bv -> Tot bool diff --git a/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst b/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst index 7c5fa630a69..301763e6ad6 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst @@ -14,7 +14,7 @@ let term_eq = FStar.Reflection.TermEq.Simple.term_eq /// Effectful term analysis: retrieve information about an effectful term, including /// its return type, its arguments, its correctly instantiated pre/postcondition, etc. -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Effectful term analysis *) diff --git a/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst b/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst index 29179443ac9..86795c53b76 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst @@ -5,7 +5,7 @@ open FStar.Tactics open FStar.Mul open FStar.InteractiveHelpers.Base -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Types and effects *) /// Define utilities to handle and carry types and effects diff --git a/ulib/experimental/FStar.InteractiveHelpers.Output.fst b/ulib/experimental/FStar.InteractiveHelpers.Output.fst index acdf34a1ee6..2407760edc3 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Output.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Output.fst @@ -10,7 +10,7 @@ open FStar.InteractiveHelpers.Propositions /// Facilities to output results to the IDE/emacs/whatever. /// Contains datatypes and functions to carry information. -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Convert terms to string *) /// The important point is to handle variable shadowing properly, so that the diff --git a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst index fefe2ca91ec..cf8f9122c77 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst @@ -13,7 +13,7 @@ open FStar.InteractiveHelpers.Output /// information from the context and generate output which can be exploited /// on the IDE side. -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** General utilities *) /// We declare some identifiers that we will use to guide the meta processing diff --git a/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst b/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst index d9b94e4b269..c0537d1e81f 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst @@ -17,7 +17,7 @@ let term_eq = FStar.Reflection.TermEq.Simple.term_eq /// [> let z = x / y in // term of interest /// [> assert(...); // post assertion -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" /// Analyze a term to retrieve its effectful information diff --git a/ulib/experimental/FStar.Sequence.Permutation.fst b/ulib/experimental/FStar.Sequence.Permutation.fst index f12cf8637f5..5d721c380b9 100644 --- a/ulib/experimental/FStar.Sequence.Permutation.fst +++ b/ulib/experimental/FStar.Sequence.Permutation.fst @@ -196,6 +196,8 @@ let rec permutation_from_equal_counts (#a:eqtype) (s0:seq a) (s1:seq a{(forall x ) ); reveal_is_permutation_nopats s0 s1 f; f) +#pop-options + #restart-solver module CM = FStar.Algebra.CommMonoid @@ -254,6 +256,7 @@ let rec foldm_back_append #a (m:CM.cm a) (s1 s2: seq a) m.mult (foldm_back m s1) (foldm_back m s2); } ) +#pop-options let foldm_back_sym #a (m:CM.cm a) (s1 s2: seq a) : Lemma From db0a9cce71c3d9accc36d5e48e735ea0b3e9fe44 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 10:53:37 -0700 Subject: [PATCH 4/9] Parser.Dep: Clearer error on dep cycle --- src/parser/FStar.Parser.Dep.fst | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index b3b14ac08c4..f1735a0b45d 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/src/parser/FStar.Parser.Dep.fst @@ -1521,8 +1521,10 @@ let collect (all_cmd_line_files: list file_name) with_file_outchannel fn (fun outc -> print_graph outc fn dep_graph); print_string "\n"; - raise_error0 Errors.Fatal_CyclicDependence - (BU.format1 "Recursive dependency on module %s\n" filename) + raise_error0 Errors.Fatal_CyclicDependence [ + text (BU.format1 "Recursive dependency on module %s." filename); + text "A full dependency graph was written to dep.graph."; + ] in (* full_cycle_detection finds cycles across interface boundaries that can otherwise be exploited to From 4f402e91137cea4da3312f0fef4b3207ae3c1488 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 10:54:39 -0700 Subject: [PATCH 5/9] Desugar: Simpler error on module not found It's really not helpful to print every module in scope. --- src/syntax/FStar.Syntax.DsEnv.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/syntax/FStar.Syntax.DsEnv.fst b/src/syntax/FStar.Syntax.DsEnv.fst index a12e10bc23c..95215f4ec36 100644 --- a/src/syntax/FStar.Syntax.DsEnv.fst +++ b/src/syntax/FStar.Syntax.DsEnv.fst @@ -1492,8 +1492,8 @@ let fail_or env lookup lid = match resolve_module_name env modul true with | None -> let opened_modules = String.concat ", " opened_modules |> Errors.text in - msg @ [Errors.text (BU.format1 "Module %s does not belong to the list of modules in scope, namely:" - (string_of_lid modul)) ^^ subdoc opened_modules] + msg @ [Errors.text (BU.format1 "Could not resolve module name %s" + (string_of_lid modul))] | Some modul' when (not (List.existsb (fun m -> m = (string_of_lid modul')) opened_modules)) -> let opened_modules = String.concat ", " opened_modules |> Errors.text in msg @ [Errors.text (BU.format2 "Module %s resolved into %s, which does not belong to the list of modules in scope, namely:" From cad84d9ae7790759640bbe8e1c95856928612f3f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 15:17:22 -0700 Subject: [PATCH 6/9] snap --- ocaml/fstar-lib/generated/FStar_Parser_Dep.ml | 15 ++++++++++++--- ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml | 12 ++++-------- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index 1db21a42d54..c4a863519e3 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -2245,11 +2245,20 @@ let (collect : (fun outc -> print_graph outc fn dep_graph1); FStar_Compiler_Util.print_string "\n"; (let uu___4 = - FStar_Compiler_Util.format1 - "Recursive dependency on module %s\n" filename in + let uu___5 = + let uu___6 = + FStar_Compiler_Util.format1 + "Recursive dependency on module %s." filename in + FStar_Errors_Msg.text uu___6 in + let uu___6 = + let uu___7 = + FStar_Errors_Msg.text + "A full dependency graph was written to dep.graph." in + [uu___7] in + uu___5 :: uu___6 in FStar_Errors.raise_error0 FStar_Errors_Codes.Fatal_CyclicDependence () - (Obj.magic FStar_Errors_Msg.is_error_message_string) + (Obj.magic FStar_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___4))) in let full_cycle_detection all_command_line_files file_system_map1 = let dep_graph1 = dep_graph_copy dep_graph in diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml index 2a9f566e574..18c0cc8c3bc 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_DsEnv.ml @@ -4015,14 +4015,10 @@ let fail_or : let uu___4 = let uu___5 = let uu___6 = - let uu___7 = - let uu___8 = FStar_Ident.string_of_lid modul in - FStar_Compiler_Util.format1 - "Module %s does not belong to the list of modules in scope, namely:" - uu___8 in - FStar_Errors_Msg.text uu___7 in - let uu___7 = subdoc opened_modules1 in - FStar_Pprint.op_Hat_Hat uu___6 uu___7 in + let uu___7 = FStar_Ident.string_of_lid modul in + FStar_Compiler_Util.format1 + "Could not resolve module name %s" uu___7 in + FStar_Errors_Msg.text uu___6 in [uu___5] in FStar_Compiler_List.op_At msg uu___4 | FStar_Pervasives_Native.Some modul' when From 53ab508daf08418fa7e4904b3d0ba3df689275ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 16:10:28 -0700 Subject: [PATCH 7/9] Extraction: not extracting tactics unless backend is Plugin --- src/extraction/FStar.Extraction.ML.Modul.fst | 24 ++++++++++++++++---- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index e9bc4f85d8e..085fe0a0e34 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -998,10 +998,18 @@ let extract_bundle env se = | _ -> failwith "Unexpected signature element" -let lb_irrelevant (g:env_t) (lb:letbinding) : bool = - Env.non_informative (tcenv_of_uenv g) lb.lbtyp && // result type is non informative - not (Term.is_arity g lb.lbtyp) && // but not a type definition - U.is_pure_or_ghost_effect lb.lbeff // and not top-level effectful +let lb_is_irrelevant (g:env_t) (lb:letbinding) : bool = + Env.non_informative (tcenv_of_uenv g) lb.lbtyp && // result type is non informative + not (Term.is_arity g lb.lbtyp) && // but not a type definition + U.is_pure_or_ghost_effect lb.lbeff // and not top-level effectful + +let lb_is_tactic (g:env_t) (lb:letbinding) : bool = + if U.is_pure_effect lb.lbeff then // not top-level effectful + let bs, c = U.arrow_formals_comp_ln lb.lbtyp in + let c_eff_name = c |> U.comp_effect_name |> Env.norm_eff_name (tcenv_of_uenv g) in + lid_equals c_eff_name PC.effect_TAC_lid + else + false (*****************************************************************************) (* Extracting the top-level definitions in a module *) @@ -1039,7 +1047,13 @@ let rec extract_sig (g:env_t) (se:sigelt) : env_t & list mlmodule1 = g, [] (* Ignore all non-informative sigelts *) - | Sig_let {lbs=(_, lbs)} when List.for_all (lb_irrelevant g) lbs -> + | Sig_let {lbs=(_, lbs)} when List.for_all (lb_is_irrelevant g) lbs -> + g, [] + + (* Ignore tactics whenever we're not extracting plugins *) + | Sig_let {lbs=(_, lbs)} + when Options.codegen () <> Some (Options.Plugin) && + List.for_all (lb_is_tactic g) lbs -> g, [] | Sig_declare_typ {lid; us=univs; t} when Term.is_arity g t -> //lid is a type From 1d7dfefae8aceb9d526143f85d210c06433b603f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 16:28:52 -0700 Subject: [PATCH 8/9] Syntax.Util: remove unused function --- src/syntax/FStar.Syntax.Util.fst | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst index 299cc0c6ec2..85c56cda831 100644 --- a/src/syntax/FStar.Syntax.Util.fst +++ b/src/syntax/FStar.Syntax.Util.fst @@ -951,15 +951,6 @@ let is_fstar_tactics_by_tactic t = | Tm_fvar fv -> fv_eq_lid fv PC.by_tactic_lid | _ -> false -let is_builtin_tactic md = - let path = Ident.path_of_lid md in - if List.length(path) > 2 then - match fst (List.splitAt 2 path) with - | ["FStar"; "Tactics"] - | ["FStar"; "Reflection"] -> true - | _ -> false - else false - (********************************************************************************) (*********************** Constructors of common terms **************************) (********************************************************************************) From 9a4bb7d12ce0b84ac9657105072b52d54724baba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 16:32:29 -0700 Subject: [PATCH 9/9] snap --- .../generated/FStar_Extraction_ML_Modul.ml | 35 +++++++++++++++++-- .../fstar-lib/generated/FStar_Syntax_Util.ml | 13 ------- 2 files changed, 32 insertions(+), 16 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml index d3af331777d..ffd839d8e47 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_ML_Modul.ml @@ -2180,7 +2180,8 @@ let (extract_bundle : (env2, uu___5))) | uu___ -> FStar_Compiler_Effect.failwith "Unexpected signature element" -let (lb_irrelevant : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = +let (lb_is_irrelevant : + env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = fun g -> fun lb -> ((let uu___ = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in @@ -2193,6 +2194,25 @@ let (lb_irrelevant : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = && (FStar_Syntax_Util.is_pure_or_ghost_effect lb.FStar_Syntax_Syntax.lbeff) +let (lb_is_tactic : env_t -> FStar_Syntax_Syntax.letbinding -> Prims.bool) = + fun g -> + fun lb -> + let uu___ = + FStar_Syntax_Util.is_pure_effect lb.FStar_Syntax_Syntax.lbeff in + if uu___ + then + let uu___1 = + FStar_Syntax_Util.arrow_formals_comp_ln + lb.FStar_Syntax_Syntax.lbtyp in + match uu___1 with + | (bs, c) -> + let c_eff_name = + let uu___2 = FStar_Extraction_ML_UEnv.tcenv_of_uenv g in + FStar_TypeChecker_Env.norm_eff_name uu___2 + (FStar_Syntax_Util.comp_effect_name c) in + FStar_Ident.lid_equals c_eff_name + FStar_Parser_Const.effect_TAC_lid + else false let rec (extract_sig : env_t -> FStar_Syntax_Syntax.sigelt -> @@ -2264,8 +2284,17 @@ let rec (extract_sig : | FStar_Syntax_Syntax.Sig_let { FStar_Syntax_Syntax.lbs1 = (uu___5, lbs); FStar_Syntax_Syntax.lids1 = uu___6;_} - when FStar_Compiler_List.for_all (lb_irrelevant g) lbs -> - (g, []) + when FStar_Compiler_List.for_all (lb_is_irrelevant g) lbs + -> (g, []) + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = (uu___5, lbs); + FStar_Syntax_Syntax.lids1 = uu___6;_} + when + (let uu___7 = FStar_Options.codegen () in + uu___7 <> + (FStar_Pervasives_Native.Some FStar_Options.Plugin)) + && (FStar_Compiler_List.for_all (lb_is_tactic g) lbs) + -> (g, []) | FStar_Syntax_Syntax.Sig_declare_typ { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = univs; diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index 1d8e82e9256..9f7bb809e9a 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -1945,19 +1945,6 @@ let (is_fstar_tactics_by_tactic : FStar_Syntax_Syntax.term -> Prims.bool) = | FStar_Syntax_Syntax.Tm_fvar fv -> FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.by_tactic_lid | uu___1 -> false -let (is_builtin_tactic : FStar_Ident.lident -> Prims.bool) = - fun md -> - let path = FStar_Ident.path_of_lid md in - if (FStar_Compiler_List.length path) > (Prims.of_int (2)) - then - let uu___ = - let uu___1 = FStar_Compiler_List.splitAt (Prims.of_int (2)) path in - FStar_Pervasives_Native.fst uu___1 in - match uu___ with - | "FStar"::"Tactics"::[] -> true - | "FStar"::"Reflection"::[] -> true - | uu___1 -> false - else false let (ktype : FStar_Syntax_Syntax.term) = FStar_Syntax_Syntax.mk (FStar_Syntax_Syntax.Tm_type FStar_Syntax_Syntax.U_unknown)