From 93a8fe55d67db12210673286f64fd4beb4aa616e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 25 Sep 2024 15:03:36 -0700 Subject: [PATCH 1/7] Tc: tweak debug messages Reduce verbosity a bit --- src/typechecker/FStar.TypeChecker.Tc.fst | 2 +- src/typechecker/FStar.TypeChecker.TcTerm.fst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst index e23f51d29a2..bda62ae7500 100644 --- a/src/typechecker/FStar.TypeChecker.Tc.fst +++ b/src/typechecker/FStar.TypeChecker.Tc.fst @@ -892,7 +892,7 @@ let tc_decl env se: list sigelt & list sigelt & Env.env = in if Debug.any () then BU.print1 "Processing %s\n" (Print.sigelt_to_string_short se); - if Debug.low () then + if Debug.medium () then BU.print2 ">>>>>>>>>>>>>>tc_decl admit=%s %s\n" (show env.admit) (show se); let result = if se.sigmeta.sigmeta_already_checked then diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst index 395dfb95750..35f9e38b193 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst @@ -3167,7 +3167,7 @@ and tc_pat env (pat_t:typ) (p0:pat) : & guard_t & bool = if !dbg_Patterns - then BU.print2 "Checking pattern %s at type %s\n" (show p) (show t); + then BU.print2 "Checking nested pattern %s at type %s\n" (show p) (show t); let id t = mk_Tm_app (S.fvar Const.id_lid None) From 285e0761c8950ae858c273a3ebbf04e634a581e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 24 Apr 2024 15:11:40 -0700 Subject: [PATCH 2/7] MkProjectors: nits --- ulib/FStar.Tactics.MkProjectors.fst | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/ulib/FStar.Tactics.MkProjectors.fst b/ulib/FStar.Tactics.MkProjectors.fst index 1823343fdc0..3970ee6a8e1 100644 --- a/ulib/FStar.Tactics.MkProjectors.fst +++ b/ulib/FStar.Tactics.MkProjectors.fst @@ -152,19 +152,20 @@ let mk_proj_decl (is_method:bool) in (* The method is just defined based on the projector. *) let lb_def = - (`(_ by (mk_one_method - (`#(embed_string (implode_qn nm))) - (`#(embed_int np))))) - (* NB: if we wanted a 'direct' definition of the method, - using a match instead of calling the projector, the following - will do. The same mk_one_projector tactic should handle it - well. - - (`(_ by (mk_one_projector - (`#unfold_names_tm) - (`#(embed_int np)) - (`#(embed_int idx))))) - *) + if true + then + (* This generates a method defined to be equal to the projector + i.e. method {| c |} = c.method *) + (`(_ by (mk_one_method + (`#(embed_string (implode_qn nm))) + (`#(embed_int np))))) + else + (* This defines the method in the same way as the projector + i.e. method {| c |} = match c with | Mk ... method ... -> method *) + (`(_ by (mk_one_projector + (`#unfold_names_tm) + (`#(embed_int np)) + (`#(embed_int idx))))) in (* dump ("returning se with name " ^ unseal field.ppname); *) (* dump ("def = " ^ term_to_string lb_def); *) @@ -198,7 +199,7 @@ let mk_proj_decl (is_method:bool) [@@plugin] let mk_projs (is_class:bool) (tyname:string) : Tac decls = - print ("!! mk_projs tactic called on: " ^ tyname); + debug (fun () -> "!! mk_projs tactic called on: " ^ tyname); let tyqn = explode_qn tyname in match lookup_typ (top_env ()) tyqn with | None -> From 8ebc142bf7cd2963a1c0a2b948a0b770693a51e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 25 Sep 2024 14:44:27 -0700 Subject: [PATCH 3/7] Tactics: no whnf on destruct_eq This is unnecessarily slow. --- src/tactics/FStar.Tactics.V2.Basic.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index 5c650fbd1e8..b9b37972c81 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -202,14 +202,14 @@ let destruct_eq' (typ : typ) : option (term & term) = let destruct_eq (env : Env.env) (typ : typ) : option (term & term) = // TODO: unascribe? - let typ = whnf env typ in + (* let typ = whnf env typ in *) match destruct_eq' typ with | Some t -> Some t | None -> // Retry for a squashed one begin match U.un_squash typ with | Some typ -> - let typ = whnf env typ in + (* let typ = whnf env typ in *) destruct_eq' typ | None -> None end From 7b27a3d315aa8f1645211ea638a0cea3607ddb5b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 25 Sep 2024 14:44:49 -0700 Subject: [PATCH 4/7] Syntax.Util: optimizing head_and_args_full --- src/syntax/FStar.Syntax.Util.fst | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst index b3a4784ed42..299cc0c6ec2 100644 --- a/src/syntax/FStar.Syntax.Util.fst +++ b/src/syntax/FStar.Syntax.Util.fst @@ -362,18 +362,17 @@ let head_and_args t = | Tm_app {hd=head; args} -> head, args | _ -> t, [] -let rec __head_and_args_full unmeta t = +let rec __head_and_args_full acc unmeta t = let t = compress t in match t.n with | Tm_app {hd=head; args} -> - let (head, args') = __head_and_args_full unmeta head - in (head, args'@args) + __head_and_args_full (args@acc) unmeta head | Tm_meta {tm} when unmeta -> - __head_and_args_full unmeta tm - | _ -> t, [] + __head_and_args_full acc unmeta tm + | _ -> t, acc -let head_and_args_full t = __head_and_args_full false t -let head_and_args_full_unmeta t = __head_and_args_full true t +let head_and_args_full t = __head_and_args_full [] false t +let head_and_args_full_unmeta t = __head_and_args_full [] true t let rec leftmost_head t = let t = compress t in From d579a3e7aaa0e2b3875c71b09e79755bdef0637c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 25 Sep 2024 14:45:19 -0700 Subject: [PATCH 5/7] Tactics: avoiding some unneeded normalization --- src/tactics/FStar.Tactics.V2.Basic.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index b9b37972c81..20a0b3b0d37 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -773,7 +773,7 @@ let intro () : tac RD.binding = wrap_err "intro" <| ( *) set_solution goal sol ;! let g = mk_goal env' ctx_uvar goal.opts goal.is_guard goal.label in - bnorm_and_replace g ;! + replace_cur g ;! return (binder_to_binding b) | None -> fail1 "goal is not an arrow (%s)" (tts (goal_env goal) (goal_type goal)) @@ -807,7 +807,7 @@ let intros (max:Z.t) : tac (list RD.binding) = wrap_err "intros" <| ( let sol = U.abs bs body (Some (U.residual_comp_of_comp c)) in set_solution goal sol ;! let g = mk_goal env' ctx_uvar goal.opts goal.is_guard goal.label in - bnorm_and_replace g ;! + replace_cur g ;! return (List.map binder_to_binding bs) ) From 28476a791c87d37f507148495b6e08220bd0afee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 25 Sep 2024 14:46:18 -0700 Subject: [PATCH 6/7] MkProjectors: optimizing --- ulib/FStar.Tactics.MkProjectors.fst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ulib/FStar.Tactics.MkProjectors.fst b/ulib/FStar.Tactics.MkProjectors.fst index 3970ee6a8e1..e512e890ad1 100644 --- a/ulib/FStar.Tactics.MkProjectors.fst +++ b/ulib/FStar.Tactics.MkProjectors.fst @@ -26,14 +26,14 @@ let debug (f : unit -> Tac string) : Tac unit = [@@plugin] let mk_one_projector (unf:list string) (np:nat) (i:nat) : Tac unit = debug (fun () -> dump "ENTRY mk_one_projector"; ""); - let _params = repeatn np intro in + let _params = Stubs.Tactics.V2.Builtins.intros np in let thing : binding = intro () in let r = t_destruct thing in match r with | [(cons, arity)] -> begin if (i >= arity) then fail "proj: bad index in mk_one_projector"; - let _ = repeatn i intro in + let _ = Stubs.Tactics.V2.Builtins.intros i in let the_b = intro () in let _ = Stubs.Tactics.V2.Builtins.intros (arity-i-1) in let eq_b : binding = intro () in @@ -216,13 +216,13 @@ let mk_projs (is_class:bool) (tyname:string) : Tac decls = (* dump ("ityp = " ^ term_to_string typ); *) (* dump ("ctor_t = " ^ term_to_string ctor_t); *) let (fields, _) = collect_arr_bs ctor_t in - let unfold_names_tm = `(Nil #string) in + let unfold_names_tm = `(Nil u#0 #string) in let (decls, _, _, _) = fold_left (fun (decls, smap, unfold_names_tm, idx) (field : binder) -> let (ds, fv) = mk_proj_decl is_class tyqn ctorname univs params idx field unfold_names_tm smap in (decls @ ds, (binder_to_namedv field, fv)::smap, - (`(Cons #string (`#(embed_string (implode_qn (inspect_fv fv)))) (`#unfold_names_tm))), + (`(Cons u#0 #string (`#(embed_string (implode_qn (inspect_fv fv)))) (`#unfold_names_tm))), idx+1)) ([], [], unfold_names_tm, 0) fields From f55a7a1038a512d0dbb16921a967af5071045f3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 25 Sep 2024 15:05:40 -0700 Subject: [PATCH 7/7] snap --- .../fstar-lib/generated/FStar_Syntax_Util.ml | 50 ++-- .../generated/FStar_Tactics_MkProjectors.ml | 213 +++++++++--------- .../generated/FStar_Tactics_V2_Basic.ml | 13 +- .../generated/FStar_TypeChecker_Tc.ml | 2 +- .../generated/FStar_TypeChecker_TcTerm.ml | 4 +- 5 files changed, 147 insertions(+), 135 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index 0c77d46fbf6..1d8e82e9256 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -657,39 +657,43 @@ let (head_and_args : -> (head, args) | uu___ -> (t1, []) let rec (__head_and_args_full : - Prims.bool -> - FStar_Syntax_Syntax.term -> - (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' - FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier - FStar_Pervasives_Native.option) Prims.list)) - = - fun unmeta1 -> - fun t -> - let t1 = FStar_Syntax_Subst.compress t in - match t1.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_app - { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_} - -> - let uu___ = __head_and_args_full unmeta1 head in - (match uu___ with - | (head1, args') -> - (head1, (FStar_Compiler_List.op_At args' args))) - | FStar_Syntax_Syntax.Tm_meta - { FStar_Syntax_Syntax.tm2 = tm; FStar_Syntax_Syntax.meta = uu___;_} - when unmeta1 -> __head_and_args_full unmeta1 tm - | uu___ -> (t1, []) + (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * + FStar_Syntax_Syntax.arg_qualifier FStar_Pervasives_Native.option) + Prims.list -> + Prims.bool -> + FStar_Syntax_Syntax.term -> + (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' + FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier + FStar_Pervasives_Native.option) Prims.list)) + = + fun acc -> + fun unmeta1 -> + fun t -> + let t1 = FStar_Syntax_Subst.compress t in + match t1.FStar_Syntax_Syntax.n with + | FStar_Syntax_Syntax.Tm_app + { FStar_Syntax_Syntax.hd = head; + FStar_Syntax_Syntax.args = args;_} + -> + __head_and_args_full (FStar_Compiler_List.op_At args acc) unmeta1 + head + | FStar_Syntax_Syntax.Tm_meta + { FStar_Syntax_Syntax.tm2 = tm; + FStar_Syntax_Syntax.meta = uu___;_} + when unmeta1 -> __head_and_args_full acc unmeta1 tm + | uu___ -> (t1, acc) let (head_and_args_full : FStar_Syntax_Syntax.term -> (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier FStar_Pervasives_Native.option) Prims.list)) - = fun t -> __head_and_args_full false t + = fun t -> __head_and_args_full [] false t let (head_and_args_full_unmeta : FStar_Syntax_Syntax.term -> (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier FStar_Pervasives_Native.option) Prims.list)) - = fun t -> __head_and_args_full true t + = fun t -> __head_and_args_full [] true t let rec (leftmost_head : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) = fun t -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml index f49541880d6..6dea1ae6794 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml @@ -90,9 +90,7 @@ let (mk_one_projector : (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> - let uu___2 = - FStar_Tactics_Util.repeatn np - FStar_Tactics_V2_Builtins.intro in + let uu___2 = FStar_Tactics_V2_Builtins.intros np in Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -100,12 +98,12 @@ let (mk_one_projector : (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" (Prims.of_int (29)) (Prims.of_int (16)) - (Prims.of_int (29)) (Prims.of_int (32))))) + (Prims.of_int (29)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (29)) (Prims.of_int (35)) + (Prims.of_int (29)) (Prims.of_int (54)) (Prims.of_int (48)) (Prims.of_int (41))))) (Obj.magic uu___2) (fun uu___3 -> @@ -198,9 +196,8 @@ let (mk_one_projector : -> let uu___7 = - FStar_Tactics_Util.repeatn - i - FStar_Tactics_V2_Builtins.intro in + FStar_Tactics_V2_Builtins.intros + i in Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -210,13 +207,13 @@ let (mk_one_projector : (Prims.of_int (36)) (Prims.of_int (17)) (Prims.of_int (36)) - (Prims.of_int (32))))) + (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" (Prims.of_int (36)) - (Prims.of_int (35)) + (Prims.of_int (54)) (Prims.of_int (46)) (Prims.of_int (15))))) (Obj.magic @@ -741,7 +738,7 @@ let (mk_proj_decl : (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" (Prims.of_int (113)) (Prims.of_int (2)) - (Prims.of_int (197)) (Prims.of_int (35))))) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -789,7 +786,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (113)) (Prims.of_int (63)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___2) (fun uu___3 -> @@ -816,7 +813,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (114)) (Prims.of_int (27)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___4) (fun uu___5 -> @@ -843,7 +840,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (115)) (Prims.of_int (28)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___5) (fun uu___6 -> @@ -1081,7 +1078,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (116)) (Prims.of_int (105)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___6) @@ -1113,7 +1110,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (117)) (Prims.of_int (24)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___7) @@ -1157,7 +1154,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (121)) (Prims.of_int (4)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___8) @@ -1185,7 +1182,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (122)) (Prims.of_int (39)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___9) @@ -1253,7 +1250,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (127)) (Prims.of_int (2)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___10) @@ -1317,7 +1314,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (127)) (Prims.of_int (58)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___11) @@ -1413,7 +1410,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (143)) (Prims.of_int (4)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___13) @@ -1597,7 +1594,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (147)) (Prims.of_int (68)) - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (8))))) (Obj.magic uu___17) @@ -1654,7 +1651,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (148)) (Prims.of_int (66)) - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (8))))) (Obj.magic uu___18) @@ -1722,7 +1719,7 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (152)) (Prims.of_int (6)) - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (8))))) (Obj.magic uu___19) @@ -1793,15 +1790,15 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (155)) (Prims.of_int (6)) - (Prims.of_int (157)) - (Prims.of_int (38))))) + (Prims.of_int (168)) + (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (168)) + (Prims.of_int (169)) (Prims.of_int (6)) - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (8))))) (Obj.magic uu___20) @@ -1837,17 +1834,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (171)) + (Prims.of_int (172)) (Prims.of_int (13)) - (Prims.of_int (178)) + (Prims.of_int (179)) (Prims.of_int (9))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (4)) - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (8))))) (Obj.magic uu___21) @@ -1869,15 +1866,15 @@ let (mk_proj_decl : "FStar.Tactics.MkProjectors.fst" (Prims.of_int (145)) (Prims.of_int (4)) - (Prims.of_int (180)) + (Prims.of_int (181)) (Prims.of_int (8))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (2)) - (Prims.of_int (197)) + (Prims.of_int (198)) (Prims.of_int (35))))) (Obj.magic uu___14) @@ -1918,19 +1915,25 @@ let (mk_projs : fun is_class -> fun tyname -> let uu___ = - FStar_Tactics_V2_Builtins.print - (Prims.strcat "!! mk_projs tactic called on: " tyname) in + debug + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Prims.strcat "!! mk_projs tactic called on: " tyname))) + uu___1) in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (201)) (Prims.of_int (2)) (Prims.of_int (201)) - (Prims.of_int (51))))) + (Prims.of_int (202)) (Prims.of_int (2)) (Prims.of_int (202)) + (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (201)) (Prims.of_int (52)) - (Prims.of_int (231)) (Prims.of_int (29))))) + (Prims.of_int (202)) (Prims.of_int (62)) + (Prims.of_int (232)) (Prims.of_int (29))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -1945,14 +1948,14 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (202)) (Prims.of_int (13)) - (Prims.of_int (202)) (Prims.of_int (30))))) + (Prims.of_int (203)) (Prims.of_int (13)) + (Prims.of_int (203)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) (Prims.of_int (2)) - (Prims.of_int (231)) (Prims.of_int (29))))) + (Prims.of_int (204)) (Prims.of_int (2)) + (Prims.of_int (232)) (Prims.of_int (29))))) (Obj.magic uu___2) (fun uu___3 -> (fun tyqn -> @@ -1963,16 +1966,16 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) + (Prims.of_int (204)) (Prims.of_int (19)) - (Prims.of_int (203)) + (Prims.of_int (204)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) (Prims.of_int (8)) - (Prims.of_int (203)) + (Prims.of_int (204)) (Prims.of_int (8)) + (Prims.of_int (204)) (Prims.of_int (36))))) (Obj.magic uu___4) (fun uu___5 -> @@ -1986,17 +1989,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) + (Prims.of_int (204)) (Prims.of_int (8)) - (Prims.of_int (203)) + (Prims.of_int (204)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) + (Prims.of_int (204)) (Prims.of_int (2)) - (Prims.of_int (231)) + (Prims.of_int (232)) (Prims.of_int (29))))) (Obj.magic uu___3) (fun uu___4 -> @@ -2018,17 +2021,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (207)) + (Prims.of_int (208)) (Prims.of_int (10)) - (Prims.of_int (207)) + (Prims.of_int (208)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (207)) + (Prims.of_int (208)) (Prims.of_int (4)) - (Prims.of_int (231)) + (Prims.of_int (232)) (Prims.of_int (29))))) (Obj.magic uu___5) (fun uu___6 -> @@ -2069,17 +2072,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (209)) - (Prims.of_int (6)) (Prims.of_int (210)) + (Prims.of_int (6)) + (Prims.of_int (211)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (211)) (Prims.of_int (58)) - (Prims.of_int (229)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___7) @@ -2098,17 +2101,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (212)) (Prims.of_int (24)) - (Prims.of_int (211)) + (Prims.of_int (212)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (212)) (Prims.of_int (20)) - (Prims.of_int (211)) + (Prims.of_int (212)) (Prims.of_int (44))))) (Obj.magic uu___10) @@ -2127,17 +2130,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (212)) (Prims.of_int (20)) - (Prims.of_int (211)) + (Prims.of_int (212)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (212)) + (Prims.of_int (213)) (Prims.of_int (6)) - (Prims.of_int (229)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___9) @@ -2168,17 +2171,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (212)) - (Prims.of_int (6)) (Prims.of_int (213)) + (Prims.of_int (6)) + (Prims.of_int (214)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (213)) + (Prims.of_int (214)) (Prims.of_int (43)) - (Prims.of_int (229)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___10) @@ -2201,17 +2204,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (214)) + (Prims.of_int (215)) (Prims.of_int (33)) - (Prims.of_int (214)) + (Prims.of_int (215)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (213)) + (Prims.of_int (214)) (Prims.of_int (43)) - (Prims.of_int (229)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___12) @@ -2237,17 +2240,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (217)) + (Prims.of_int (218)) (Prims.of_int (24)) - (Prims.of_int (217)) + (Prims.of_int (218)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (214)) + (Prims.of_int (215)) (Prims.of_int (41)) - (Prims.of_int (229)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___14) @@ -2273,10 +2276,13 @@ let (mk_projs : FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_App ((FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv + (FStar_Reflection_V2_Data.Tv_UInst + ((FStar_Reflection_V2_Builtins.pack_fv ["Prims"; - "Nil"]))), + "Nil"]), + [ + FStar_Reflection_V2_Builtins.pack_universe + FStar_Reflection_V2_Data.Uv_Zero]))), ((FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_FVar (FStar_Reflection_V2_Builtins.pack_fv @@ -2289,17 +2295,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (218)) + (Prims.of_int (219)) (Prims.of_int (28)) - (Prims.of_int (218)) - (Prims.of_int (42))))) + (Prims.of_int (219)) + (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (218)) - (Prims.of_int (45)) - (Prims.of_int (229)) + (Prims.of_int (219)) + (Prims.of_int (49)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___17) @@ -2340,17 +2346,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (221)) + (Prims.of_int (222)) (Prims.of_int (25)) - (Prims.of_int (221)) + (Prims.of_int (222)) (Prims.of_int (104))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (220)) + (Prims.of_int (221)) (Prims.of_int (78)) - (Prims.of_int (225)) + (Prims.of_int (226)) (Prims.of_int (17))))) (Obj.magic uu___20) @@ -2379,10 +2385,13 @@ let (mk_projs : ((FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_App ((FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv + (FStar_Reflection_V2_Data.Tv_UInst + ((FStar_Reflection_V2_Builtins.pack_fv ["Prims"; - "Cons"]))), + "Cons"]), + [ + FStar_Reflection_V2_Builtins.pack_universe + FStar_Reflection_V2_Data.Uv_Zero]))), ((FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_FVar (FStar_Reflection_V2_Builtins.pack_fv @@ -2408,17 +2417,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (220)) + (Prims.of_int (221)) (Prims.of_int (8)) - (Prims.of_int (227)) + (Prims.of_int (228)) (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (218)) - (Prims.of_int (45)) - (Prims.of_int (229)) + (Prims.of_int (219)) + (Prims.of_int (49)) + (Prims.of_int (230)) (Prims.of_int (11))))) (Obj.magic uu___18) diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index 7add28d56f5..89712a5e9aa 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -364,15 +364,13 @@ let (destruct_eq : = fun env1 -> fun typ -> - let typ1 = whnf env1 typ in - let uu___ = destruct_eq' typ1 in + let uu___ = destruct_eq' typ in match uu___ with | FStar_Pervasives_Native.Some t -> FStar_Pervasives_Native.Some t | FStar_Pervasives_Native.None -> - let uu___1 = FStar_Syntax_Util.un_squash typ1 in + let uu___1 = FStar_Syntax_Util.un_squash typ in (match uu___1 with - | FStar_Pervasives_Native.Some typ2 -> - let typ3 = whnf env1 typ2 in destruct_eq' typ3 + | FStar_Pervasives_Native.Some typ1 -> destruct_eq' typ1 | FStar_Pervasives_Native.None -> FStar_Pervasives_Native.None) let (get_guard_policy : unit -> FStar_Tactics_Types.guard_policy FStar_Tactics_Monad.tac) = @@ -2800,7 +2798,8 @@ let (intro : goal.FStar_Tactics_Types.is_guard goal.FStar_Tactics_Types.label in let uu___7 = - bnorm_and_replace g in + FStar_Tactics_Monad.replace_cur + g in Obj.magic (FStar_Class_Monad.op_let_Bang FStar_Tactics_Monad.monad_tac @@ -2948,7 +2947,7 @@ let (intros : goal.FStar_Tactics_Types.label in let uu___10 = - bnorm_and_replace + FStar_Tactics_Monad.replace_cur g in Obj.magic (FStar_Class_Monad.op_let_Bang diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index 0a741de1f4c..0278024672d 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -4280,7 +4280,7 @@ let (tc_decl : let uu___2 = FStar_Syntax_Print.sigelt_to_string_short se in FStar_Compiler_Util.print1 "Processing %s\n" uu___2 else ()); - (let uu___2 = FStar_Compiler_Debug.low () in + (let uu___2 = FStar_Compiler_Debug.medium () in if uu___2 then let uu___3 = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml index 69b88525266..ef11a87eec3 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml @@ -8994,8 +8994,8 @@ and (tc_pat : FStar_Class_Show.show FStar_Syntax_Print.showable_pat p in let uu___3 = FStar_Class_Show.show FStar_Syntax_Print.showable_term t in - FStar_Compiler_Util.print2 "Checking pattern %s at type %s\n" - uu___2 uu___3 + FStar_Compiler_Util.print2 + "Checking nested pattern %s at type %s\n" uu___2 uu___3 else ()); (let id t1 = let uu___1 =