From e165e689116095ec73b66990b338043b543ce46d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 18 Sep 2024 23:36:03 -0700 Subject: [PATCH] snap --- .../fstar-lib/generated/FStar_Syntax_Util.ml | 31 +- .../generated/FStar_Tactics_Hooks.ml | 36 +- .../generated/FStar_Tactics_MkProjectors.ml | 382 ++++++------ .../generated/FStar_Tactics_V2_Basic.ml | 151 +++++ .../generated/FStar_Tactics_V2_Derived.ml | 2 +- .../generated/FStar_Tactics_V2_Primops.ml | 576 +++++++++--------- .../FStar_Tactics_V2_SyntaxHelpers.ml | 221 +++++-- .../generated/FStar_ToSyntax_ToSyntax.ml | 5 +- 8 files changed, 868 insertions(+), 536 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index 342c4b0c2c1..988ceab41f7 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -1394,7 +1394,7 @@ let (abs : } in FStar_Syntax_Syntax.Tm_abs uu___3 in FStar_Syntax_Syntax.mk uu___2 t.FStar_Syntax_Syntax.pos) -let (arrow : +let (arrow_ln : FStar_Syntax_Syntax.binder Prims.list -> FStar_Syntax_Syntax.comp' FStar_Syntax_Syntax.syntax -> FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax) @@ -1405,25 +1405,28 @@ let (arrow : | [] -> comp_result c | uu___ -> let uu___1 = - let uu___2 = - let uu___3 = FStar_Syntax_Subst.close_binders bs in - let uu___4 = FStar_Syntax_Subst.close_comp bs c in - { - FStar_Syntax_Syntax.bs1 = uu___3; - FStar_Syntax_Syntax.comp = uu___4 - } in - FStar_Syntax_Syntax.Tm_arrow uu___2 in - let uu___2 = FStar_Compiler_List.fold_left (fun a -> fun b -> FStar_Compiler_Range_Ops.union_ranges a ((b.FStar_Syntax_Syntax.binder_bv).FStar_Syntax_Syntax.sort).FStar_Syntax_Syntax.pos) c.FStar_Syntax_Syntax.pos bs in - FStar_Syntax_Syntax.mk uu___1 uu___2 + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_arrow + { FStar_Syntax_Syntax.bs1 = bs; FStar_Syntax_Syntax.comp = c }) + uu___1 +let (arrow : + FStar_Syntax_Syntax.binders -> + FStar_Syntax_Syntax.comp -> + FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax) + = + fun bs -> + fun c -> + let c1 = FStar_Syntax_Subst.close_comp bs c in + let bs1 = FStar_Syntax_Subst.close_binders bs in arrow_ln bs1 c1 let (flat_arrow : - FStar_Syntax_Syntax.binder Prims.list -> - FStar_Syntax_Syntax.comp' FStar_Syntax_Syntax.syntax -> + FStar_Syntax_Syntax.binders -> + FStar_Syntax_Syntax.comp -> FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax) = fun bs -> @@ -1834,7 +1837,7 @@ let (close_univs_and_mk_letbinding : let (open_univ_vars_binders_and_comp : FStar_Syntax_Syntax.univ_names -> FStar_Syntax_Syntax.binder Prims.list -> - FStar_Syntax_Syntax.comp' FStar_Syntax_Syntax.syntax -> + FStar_Syntax_Syntax.comp -> (FStar_Syntax_Syntax.univ_names * FStar_Syntax_Syntax.binder Prims.list * FStar_Syntax_Syntax.comp)) = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml index d673374114c..60b15f1aee6 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml @@ -2386,22 +2386,40 @@ let (splice : then let uu___12 = let uu___13 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_qualifier - q in + let uu___14 = + let uu___15 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_qualifier + q in + FStar_Compiler_Util.format1 + "The qualifier %s is internal." + uu___15 in + FStar_Errors_Msg.text + uu___14 in let uu___14 = - FStar_Syntax_Print.sigelt_to_string_short - se in - FStar_Compiler_Util.format2 - "The qualifier %s is internal, it cannot be attached to spliced sigelt `%s`." - uu___13 uu___14 in + let uu___15 = + let uu___16 = + FStar_Errors_Msg.text + "It cannot be attached to spliced declaration:" in + let uu___17 = + let uu___18 = + FStar_Syntax_Print.sigelt_to_string_short + se in + FStar_Pprint.arbitrary_string + uu___18 in + FStar_Pprint.prefix + (Prims.of_int (2)) + Prims.int_one uu___16 + uu___17 in + [uu___15] in + uu___13 :: uu___14 in FStar_Errors.raise_error FStar_Class_HasRange.hasRange_range rng FStar_Errors_Codes.Error_InternalQualifier () (Obj.magic - FStar_Errors_Msg.is_error_message_string) + FStar_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___12) else ()) se.FStar_Syntax_Syntax.sigquals) diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml index 687dda88955..f49541880d6 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml @@ -256,11 +256,10 @@ let (mk_one_projector : the_b -> let uu___10 = - FStar_Tactics_Util.repeatn + FStar_Tactics_V2_Builtins.intros ((arity - i) - - Prims.int_one) - FStar_Tactics_V2_Builtins.intro in + Prims.int_one) in Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -270,13 +269,13 @@ let (mk_one_projector : (Prims.of_int (38)) (Prims.of_int (17)) (Prims.of_int (38)) - (Prims.of_int (42))))) + (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" (Prims.of_int (38)) - (Prims.of_int (45)) + (Prims.of_int (64)) (Prims.of_int (46)) (Prims.of_int (15))))) (Obj.magic @@ -674,6 +673,11 @@ let (embed_string : Prims.string -> FStar_Tactics_NamedView.term) = FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_Const (FStar_Reflection_V2_Data.C_String s)) +let (substitute_attr : FStar_Tactics_NamedView.term) = + FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["FStar"; "Pervasives"; "Substitute"])) let (mk_proj_decl : Prims.bool -> FStar_Reflection_Types.name -> @@ -709,9 +713,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (107)) + (Prims.of_int (112)) (Prims.of_int (41)) - (Prims.of_int (107)) + (Prims.of_int (112)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic @@ -730,14 +734,14 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (107)) (Prims.of_int (2)) - (Prims.of_int (107)) (Prims.of_int (61))))) + (Prims.of_int (112)) (Prims.of_int (2)) + (Prims.of_int (112)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) (Prims.of_int (2)) - (Prims.of_int (190)) (Prims.of_int (35))))) + (Prims.of_int (113)) (Prims.of_int (2)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -752,9 +756,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) + (Prims.of_int (113)) (Prims.of_int (36)) - (Prims.of_int (108)) + (Prims.of_int (113)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic @@ -775,17 +779,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) + (Prims.of_int (113)) (Prims.of_int (2)) - (Prims.of_int (108)) + (Prims.of_int (113)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) + (Prims.of_int (113)) (Prims.of_int (63)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___2) (fun uu___3 -> @@ -802,17 +806,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (109)) + (Prims.of_int (114)) (Prims.of_int (11)) - (Prims.of_int (109)) + (Prims.of_int (114)) (Prims.of_int (24))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (109)) + (Prims.of_int (114)) (Prims.of_int (27)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___4) (fun uu___5 -> @@ -829,17 +833,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (110)) + (Prims.of_int (115)) (Prims.of_int (13)) - (Prims.of_int (110)) + (Prims.of_int (115)) (Prims.of_int (25))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (110)) + (Prims.of_int (115)) (Prims.of_int (28)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___5) (fun uu___6 -> @@ -854,18 +858,18 @@ let (mk_proj_decl : Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (31))))) (FStar_Sealed.seal ( Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (102))))) (Obj.magic uu___7) @@ -888,17 +892,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (48)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (66))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (48)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (101))))) (Obj.magic uu___12) @@ -919,9 +923,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (82)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -949,9 +953,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (69)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -979,9 +983,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (48)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -1008,17 +1012,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (35)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (34)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (102))))) (Obj.magic uu___10) @@ -1036,17 +1040,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (34)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (102))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (102))))) (Obj.magic uu___9) @@ -1067,17 +1071,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (102))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (116)) (Prims.of_int (105)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___6) @@ -1099,17 +1103,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (112)) + (Prims.of_int (117)) (Prims.of_int (11)) - (Prims.of_int (112)) + (Prims.of_int (117)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (112)) + (Prims.of_int (117)) (Prims.of_int (24)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___7) @@ -1143,17 +1147,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (113)) + (Prims.of_int (118)) (Prims.of_int (18)) - (Prims.of_int (115)) + (Prims.of_int (120)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (116)) + (Prims.of_int (121)) (Prims.of_int (4)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___8) @@ -1171,17 +1175,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (117)) + (Prims.of_int (122)) (Prims.of_int (20)) - (Prims.of_int (117)) + (Prims.of_int (122)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (117)) + (Prims.of_int (122)) (Prims.of_int (39)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___9) @@ -1204,17 +1208,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (120)) + (Prims.of_int (125)) (Prims.of_int (26)) - (Prims.of_int (120)) + (Prims.of_int (125)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (123)) (Prims.of_int (15)) - (Prims.of_int (120)) + (Prims.of_int (125)) (Prims.of_int (73))))) (Obj.magic uu___11) @@ -1239,17 +1243,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (123)) (Prims.of_int (15)) - (Prims.of_int (120)) + (Prims.of_int (125)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (127)) (Prims.of_int (2)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___10) @@ -1273,9 +1277,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (127)) (Prims.of_int (35)) - (Prims.of_int (122)) + (Prims.of_int (127)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic @@ -1303,17 +1307,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (127)) (Prims.of_int (2)) - (Prims.of_int (122)) + (Prims.of_int (127)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (127)) (Prims.of_int (58)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___11) @@ -1399,17 +1403,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (123)) + (Prims.of_int (128)) (Prims.of_int (16)) - (Prims.of_int (137)) + (Prims.of_int (142)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (138)) + (Prims.of_int (143)) (Prims.of_int (4)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___13) @@ -1466,17 +1470,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (27)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (26)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (65))))) (Obj.magic uu___19) @@ -1497,17 +1501,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (44)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (43)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (64))))) (Obj.magic uu___22) @@ -1525,17 +1529,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (43)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (26)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (65))))) (Obj.magic uu___21) @@ -1555,17 +1559,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (26)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (18)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (65))))) (Obj.magic uu___18) @@ -1583,17 +1587,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (18)) - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (147)) (Prims.of_int (68)) - (Prims.of_int (173)) + (Prims.of_int (180)) (Prims.of_int (8))))) (Obj.magic uu___17) @@ -1640,17 +1644,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (143)) + (Prims.of_int (148)) (Prims.of_int (15)) - (Prims.of_int (143)) + (Prims.of_int (148)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (143)) + (Prims.of_int (148)) (Prims.of_int (66)) - (Prims.of_int (173)) + (Prims.of_int (180)) (Prims.of_int (8))))) (Obj.magic uu___18) @@ -1673,17 +1677,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (146)) + (Prims.of_int (151)) (Prims.of_int (28)) - (Prims.of_int (146)) + (Prims.of_int (151)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (144)) + (Prims.of_int (149)) (Prims.of_int (17)) - (Prims.of_int (146)) + (Prims.of_int (151)) (Prims.of_int (75))))) (Obj.magic uu___20) @@ -1708,17 +1712,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (144)) + (Prims.of_int (149)) (Prims.of_int (17)) - (Prims.of_int (146)) + (Prims.of_int (151)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (147)) + (Prims.of_int (152)) (Prims.of_int (6)) - (Prims.of_int (173)) + (Prims.of_int (180)) (Prims.of_int (8))))) (Obj.magic uu___19) @@ -1787,17 +1791,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (155)) (Prims.of_int (6)) - (Prims.of_int (152)) + (Prims.of_int (157)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (166)) - (Prims.of_int (4)) - (Prims.of_int (173)) + (Prims.of_int (168)) + (Prims.of_int (6)) + (Prims.of_int (180)) (Prims.of_int (8))))) (Obj.magic uu___20) @@ -1833,28 +1837,26 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (166)) - (Prims.of_int (5)) - (Prims.of_int (173)) - (Prims.of_int (7))))) + (Prims.of_int (171)) + (Prims.of_int (13)) + (Prims.of_int (178)) + (Prims.of_int (9))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (166)) + (Prims.of_int (180)) (Prims.of_int (4)) - (Prims.of_int (173)) + (Prims.of_int (180)) (Prims.of_int (8))))) (Obj.magic uu___21) - (fun - uu___22 + (fun se -> FStar_Tactics_Effect.lift_div_tac (fun - uu___23 - -> - [uu___22])))) + uu___22 + -> [se])))) uu___21))) uu___20))) uu___19))) @@ -1865,17 +1867,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (140)) + (Prims.of_int (145)) (Prims.of_int (4)) - (Prims.of_int (173)) + (Prims.of_int (180)) (Prims.of_int (8))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (2)) - (Prims.of_int (190)) + (Prims.of_int (197)) (Prims.of_int (35))))) (Obj.magic uu___14) @@ -1889,7 +1891,9 @@ let (mk_proj_decl : ((( FStar_Reflection_V2_Builtins.set_sigelt_attrs (FStar_List_Tot_Base.op_At - field.FStar_Tactics_NamedView.attrs + (substitute_attr + :: + (field.FStar_Tactics_NamedView.attrs)) (FStar_Reflection_V2_Builtins.sigelt_attrs se_proj)) se_proj) @@ -1920,13 +1924,13 @@ let (mk_projs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (194)) (Prims.of_int (2)) (Prims.of_int (194)) + (Prims.of_int (201)) (Prims.of_int (2)) (Prims.of_int (201)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (194)) (Prims.of_int (52)) - (Prims.of_int (224)) (Prims.of_int (29))))) + (Prims.of_int (201)) (Prims.of_int (52)) + (Prims.of_int (231)) (Prims.of_int (29))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -1941,14 +1945,14 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (195)) (Prims.of_int (13)) - (Prims.of_int (195)) (Prims.of_int (30))))) + (Prims.of_int (202)) (Prims.of_int (13)) + (Prims.of_int (202)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) (Prims.of_int (2)) - (Prims.of_int (224)) (Prims.of_int (29))))) + (Prims.of_int (203)) (Prims.of_int (2)) + (Prims.of_int (231)) (Prims.of_int (29))))) (Obj.magic uu___2) (fun uu___3 -> (fun tyqn -> @@ -1959,16 +1963,16 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (203)) (Prims.of_int (19)) - (Prims.of_int (196)) + (Prims.of_int (203)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) (Prims.of_int (8)) - (Prims.of_int (196)) + (Prims.of_int (203)) (Prims.of_int (8)) + (Prims.of_int (203)) (Prims.of_int (36))))) (Obj.magic uu___4) (fun uu___5 -> @@ -1982,17 +1986,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (203)) (Prims.of_int (8)) - (Prims.of_int (196)) + (Prims.of_int (203)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (203)) (Prims.of_int (2)) - (Prims.of_int (224)) + (Prims.of_int (231)) (Prims.of_int (29))))) (Obj.magic uu___3) (fun uu___4 -> @@ -2014,17 +2018,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (200)) + (Prims.of_int (207)) (Prims.of_int (10)) - (Prims.of_int (200)) + (Prims.of_int (207)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (200)) + (Prims.of_int (207)) (Prims.of_int (4)) - (Prims.of_int (224)) + (Prims.of_int (231)) (Prims.of_int (29))))) (Obj.magic uu___5) (fun uu___6 -> @@ -2065,17 +2069,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (202)) + (Prims.of_int (209)) (Prims.of_int (6)) - (Prims.of_int (203)) + (Prims.of_int (210)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) + (Prims.of_int (210)) (Prims.of_int (58)) - (Prims.of_int (222)) + (Prims.of_int (229)) (Prims.of_int (11))))) (Obj.magic uu___7) @@ -2094,17 +2098,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (211)) (Prims.of_int (24)) - (Prims.of_int (204)) + (Prims.of_int (211)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (211)) (Prims.of_int (20)) - (Prims.of_int (204)) + (Prims.of_int (211)) (Prims.of_int (44))))) (Obj.magic uu___10) @@ -2123,17 +2127,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (211)) (Prims.of_int (20)) - (Prims.of_int (204)) + (Prims.of_int (211)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (205)) + (Prims.of_int (212)) (Prims.of_int (6)) - (Prims.of_int (222)) + (Prims.of_int (229)) (Prims.of_int (11))))) (Obj.magic uu___9) @@ -2164,17 +2168,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (205)) + (Prims.of_int (212)) (Prims.of_int (6)) - (Prims.of_int (206)) + (Prims.of_int (213)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (206)) + (Prims.of_int (213)) (Prims.of_int (43)) - (Prims.of_int (222)) + (Prims.of_int (229)) (Prims.of_int (11))))) (Obj.magic uu___10) @@ -2197,17 +2201,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (207)) + (Prims.of_int (214)) (Prims.of_int (33)) - (Prims.of_int (207)) + (Prims.of_int (214)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (206)) + (Prims.of_int (213)) (Prims.of_int (43)) - (Prims.of_int (222)) + (Prims.of_int (229)) (Prims.of_int (11))))) (Obj.magic uu___12) @@ -2233,17 +2237,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (217)) (Prims.of_int (24)) - (Prims.of_int (210)) + (Prims.of_int (217)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (207)) + (Prims.of_int (214)) (Prims.of_int (41)) - (Prims.of_int (222)) + (Prims.of_int (229)) (Prims.of_int (11))))) (Obj.magic uu___14) @@ -2285,17 +2289,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (218)) (Prims.of_int (28)) - (Prims.of_int (211)) + (Prims.of_int (218)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (218)) (Prims.of_int (45)) - (Prims.of_int (222)) + (Prims.of_int (229)) (Prims.of_int (11))))) (Obj.magic uu___17) @@ -2336,17 +2340,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (214)) + (Prims.of_int (221)) (Prims.of_int (25)) - (Prims.of_int (214)) + (Prims.of_int (221)) (Prims.of_int (104))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (213)) + (Prims.of_int (220)) (Prims.of_int (78)) - (Prims.of_int (218)) + (Prims.of_int (225)) (Prims.of_int (17))))) (Obj.magic uu___20) @@ -2404,17 +2408,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (213)) - (Prims.of_int (8)) (Prims.of_int (220)) + (Prims.of_int (8)) + (Prims.of_int (227)) (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (218)) (Prims.of_int (45)) - (Prims.of_int (222)) + (Prims.of_int (229)) (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 339e1467592..7add28d56f5 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -2830,6 +2830,157 @@ let (intro : tts uu___4 uu___5 in fail1 "goal is not an arrow (%s)" uu___3))) uu___2)) in FStar_Tactics_Monad.wrap_err "intro" uu___1 +let (intros : + FStar_BigInt.t -> + FStar_Reflection_V2_Data.binding Prims.list FStar_Tactics_Monad.tac) + = + fun max -> + let uu___ = + let max1 = FStar_BigInt.to_int_fs max in + Obj.magic + (FStar_Class_Monad.op_let_Bang FStar_Tactics_Monad.monad_tac () () + (Obj.magic FStar_Tactics_Monad.cur_goal) + (fun uu___1 -> + (fun goal -> + let goal = Obj.magic goal in + let uu___1 = + let uu___2 = FStar_Tactics_Types.goal_type goal in + FStar_Syntax_Util.arrow_formals_comp_ln uu___2 in + match uu___1 with + | (bs, c) -> + let uu___2 = + if max1 >= Prims.int_zero + then + let uu___3 = FStar_Compiler_List.splitAt max1 bs in + match uu___3 with + | (bs0, bs1) -> + let c1 = + let uu___4 = FStar_Syntax_Util.arrow_ln bs1 c in + FStar_Syntax_Syntax.mk_Total uu___4 in + (bs0, c1) + else (bs, c) in + (match uu___2 with + | (bs1, c1) -> + let uu___3 = + let uu___4 = FStar_Tactics_Types.goal_env goal in + FStar_TypeChecker_Core.open_binders_in_comp + uu___4 bs1 c1 in + (match uu___3 with + | (env', bs2, c2) -> + let uu___4 = + let uu___5 = + let uu___6 = + FStar_Syntax_Util.is_pure_comp c2 in + Prims.op_Negation uu___6 in + if uu___5 + then + let uu___6 = + let uu___7 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_comp c2 in + Prims.strcat "Codomain is effectful: " + uu___7 in + FStar_Tactics_Monad.fail uu___6 + else + FStar_Class_Monad.return + FStar_Tactics_Monad.monad_tac () + (Obj.repr ()) in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac () () + uu___4 + (fun uu___5 -> + (fun uu___5 -> + let uu___5 = Obj.magic uu___5 in + let typ' = + FStar_Syntax_Util.comp_result c2 in + let uu___6 = + let uu___7 = + let uu___8 = + should_check_goal_uvar goal in + FStar_Pervasives_Native.Some + uu___8 in + let uu___8 = + FStar_Tactics_Monad.goal_typedness_deps + goal in + FStar_Tactics_Monad.new_uvar + "intros" env' typ' uu___7 + uu___8 (rangeof goal) in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac + () () (Obj.magic uu___6) + (fun uu___7 -> + (fun uu___7 -> + let uu___7 = + Obj.magic uu___7 in + match uu___7 with + | (body, ctx_uvar) -> + let sol = + let uu___8 = + let uu___9 = + FStar_Syntax_Util.residual_comp_of_comp + c2 in + FStar_Pervasives_Native.Some + uu___9 in + FStar_Syntax_Util.abs + bs2 body uu___8 in + let uu___8 = + set_solution goal + sol in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac + () () uu___8 + (fun uu___9 -> + (fun uu___9 + -> + let uu___9 + = + Obj.magic + uu___9 in + let g = + FStar_Tactics_Types.mk_goal + env' + ctx_uvar + goal.FStar_Tactics_Types.opts + goal.FStar_Tactics_Types.is_guard + goal.FStar_Tactics_Types.label in + let uu___10 + = + bnorm_and_replace + g in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac + () () + uu___10 + (fun + uu___11 + -> + (fun + uu___11 + -> + let uu___11 + = + Obj.magic + uu___11 in + let uu___12 + = + FStar_Compiler_List.map + binder_to_binding + bs2 in + Obj.magic + (FStar_Class_Monad.return + FStar_Tactics_Monad.monad_tac + () + (Obj.magic + uu___12))) + uu___11))) + uu___9))) + uu___7))) uu___5))))) + uu___1)) in + FStar_Tactics_Monad.wrap_err "intros" uu___ let (intro_rec : unit -> (FStar_Reflection_V2_Data.binding * FStar_Reflection_V2_Data.binding) diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml index b832803338e..95416a32bd4 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml @@ -3159,7 +3159,7 @@ let (intros : unit -> (FStar_Tactics_NamedView.binding Prims.list, unit) FStar_Tactics_Effect.tac_repr) - = fun uu___ -> repeat FStar_Tactics_V2_Builtins.intro + = fun uu___ -> FStar_Tactics_V2_Builtins.intros (Prims.of_int (-1)) let (intros' : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = fun uu___ -> let uu___1 = intros () in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml index dc85721ef21..e1d79806377 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml @@ -261,154 +261,168 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = let uu___37 = let uu___38 = FStar_Tactics_InterpFuns.mk_tac_step_1 - Prims.int_zero "intro_rec" - FStar_Syntax_Embeddings.e_unit - (FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V2_Embeddings.e_binding + Prims.int_zero "intros" + FStar_Syntax_Embeddings.e_int + (FStar_Syntax_Embeddings.e_list FStar_Reflection_V2_Embeddings.e_binding) - FStar_TypeChecker_NBETerm.e_unit - (FStar_TypeChecker_NBETerm.e_tuple2 - FStar_Reflection_V2_NBEEmbeddings.e_binding + FStar_TypeChecker_NBETerm.e_int + (FStar_TypeChecker_NBETerm.e_list FStar_Reflection_V2_NBEEmbeddings.e_binding) - FStar_Tactics_V2_Basic.intro_rec - FStar_Tactics_V2_Basic.intro_rec in + FStar_Tactics_V2_Basic.intros + FStar_Tactics_V2_Basic.intros in let uu___39 = let uu___40 = FStar_Tactics_InterpFuns.mk_tac_step_1 - Prims.int_zero "norm" - (FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_norm_step) + Prims.int_zero "intro_rec" FStar_Syntax_Embeddings.e_unit - (FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_norm_step) + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Reflection_V2_Embeddings.e_binding + FStar_Reflection_V2_Embeddings.e_binding) FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.norm - FStar_Tactics_V2_Basic.norm in + (FStar_TypeChecker_NBETerm.e_tuple2 + FStar_Reflection_V2_NBEEmbeddings.e_binding + FStar_Reflection_V2_NBEEmbeddings.e_binding) + FStar_Tactics_V2_Basic.intro_rec + FStar_Tactics_V2_Basic.intro_rec in let uu___41 = let uu___42 = - FStar_Tactics_InterpFuns.mk_tac_step_3 - Prims.int_zero - "norm_term_env" - FStar_Reflection_V2_Embeddings.e_env + FStar_Tactics_InterpFuns.mk_tac_step_1 + Prims.int_zero "norm" (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_norm_step) - uu___2 uu___2 - FStar_Reflection_V2_NBEEmbeddings.e_env + FStar_Syntax_Embeddings.e_unit (FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_norm_step) - FStar_Reflection_V2_NBEEmbeddings.e_attribute - FStar_Reflection_V2_NBEEmbeddings.e_attribute - FStar_Tactics_V2_Basic.norm_term_env - FStar_Tactics_V2_Basic.norm_term_env in + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.norm + FStar_Tactics_V2_Basic.norm in let uu___43 = let uu___44 = - FStar_Tactics_InterpFuns.mk_tac_step_2 + FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero - "norm_binding_type" + "norm_term_env" + FStar_Reflection_V2_Embeddings.e_env (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_norm_step) - FStar_Reflection_V2_Embeddings.e_binding - FStar_Syntax_Embeddings.e_unit + uu___2 uu___2 + FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_norm_step) - FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.norm_binding_type - FStar_Tactics_V2_Basic.norm_binding_type in + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Tactics_V2_Basic.norm_term_env + FStar_Tactics_V2_Basic.norm_term_env in let uu___45 = let uu___46 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero - "rename_to" + "norm_binding_type" + (FStar_Syntax_Embeddings.e_list + FStar_Syntax_Embeddings.e_norm_step) FStar_Reflection_V2_Embeddings.e_binding - FStar_Syntax_Embeddings.e_string - FStar_Reflection_V2_Embeddings.e_binding - FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_TypeChecker_NBETerm.e_string + FStar_Syntax_Embeddings.e_unit + (FStar_TypeChecker_NBETerm.e_list + FStar_TypeChecker_NBETerm.e_norm_step) FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_Tactics_V2_Basic.rename_to - FStar_Tactics_V2_Basic.rename_to in + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.norm_binding_type + FStar_Tactics_V2_Basic.norm_binding_type in let uu___47 = let uu___48 = - FStar_Tactics_InterpFuns.mk_tac_step_1 + FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero - "var_retype" + "rename_to" FStar_Reflection_V2_Embeddings.e_binding - FStar_Syntax_Embeddings.e_unit + FStar_Syntax_Embeddings.e_string + FStar_Reflection_V2_Embeddings.e_binding + FStar_Reflection_V2_NBEEmbeddings.e_binding + FStar_TypeChecker_NBETerm.e_string FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.var_retype - FStar_Tactics_V2_Basic.var_retype in + FStar_Tactics_V2_Basic.rename_to + FStar_Tactics_V2_Basic.rename_to in let uu___49 = let uu___50 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "revert" + "var_retype" + FStar_Reflection_V2_Embeddings.e_binding FStar_Syntax_Embeddings.e_unit - FStar_Syntax_Embeddings.e_unit - FStar_TypeChecker_NBETerm.e_unit + FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.revert - FStar_Tactics_V2_Basic.revert in + FStar_Tactics_V2_Basic.var_retype + FStar_Tactics_V2_Basic.var_retype in let uu___51 = let uu___52 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "clear_top" + "revert" FStar_Syntax_Embeddings.e_unit FStar_Syntax_Embeddings.e_unit FStar_TypeChecker_NBETerm.e_unit FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.clear_top - FStar_Tactics_V2_Basic.clear_top in + FStar_Tactics_V2_Basic.revert + FStar_Tactics_V2_Basic.revert in let uu___53 = let uu___54 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "clear" - FStar_Reflection_V2_Embeddings.e_binding + "clear_top" + FStar_Syntax_Embeddings.e_unit FStar_Syntax_Embeddings.e_unit - FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.clear - FStar_Tactics_V2_Basic.clear in + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.clear_top + FStar_Tactics_V2_Basic.clear_top in let uu___55 = let uu___56 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "rewrite" + "clear" FStar_Reflection_V2_Embeddings.e_binding FStar_Syntax_Embeddings.e_unit FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.rewrite - FStar_Tactics_V2_Basic.rewrite in + FStar_Tactics_V2_Basic.clear + FStar_Tactics_V2_Basic.clear in let uu___57 = let uu___58 = - FStar_Tactics_InterpFuns.mk_tac_step_2 + FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "grewrite" - uu___2 uu___2 + "rewrite" + FStar_Reflection_V2_Embeddings.e_binding FStar_Syntax_Embeddings.e_unit - FStar_Reflection_V2_NBEEmbeddings.e_attribute - FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.grewrite - FStar_Tactics_V2_Basic.grewrite in + FStar_Tactics_V2_Basic.rewrite + FStar_Tactics_V2_Basic.rewrite in let uu___59 = let uu___60 = - FStar_Tactics_InterpFuns.mk_tac_step_1 + FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero - "refine_intro" - FStar_Syntax_Embeddings.e_unit + "grewrite" + uu___2 + uu___2 FStar_Syntax_Embeddings.e_unit + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_TypeChecker_NBETerm.e_unit - FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.refine_intro - FStar_Tactics_V2_Basic.refine_intro in + FStar_Tactics_V2_Basic.grewrite + FStar_Tactics_V2_Basic.grewrite in let uu___61 = let uu___62 = - FStar_Tactics_InterpFuns.mk_tac_step_3 + FStar_Tactics_InterpFuns.mk_tac_step_1 + Prims.int_zero + "refine_intro" + FStar_Syntax_Embeddings.e_unit + FStar_Syntax_Embeddings.e_unit + FStar_TypeChecker_NBETerm.e_unit + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.refine_intro + FStar_Tactics_V2_Basic.refine_intro in + let uu___63 = + let uu___64 + = + FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero "t_exact" FStar_Syntax_Embeddings.e_bool @@ -421,8 +435,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_exact FStar_Tactics_V2_Basic.t_exact in - let uu___63 = - let uu___64 + let uu___65 + = + let uu___66 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -439,9 +454,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_apply FStar_Tactics_V2_Basic.t_apply in - let uu___65 + let uu___67 = - let uu___66 + let uu___68 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -456,9 +471,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_apply_lemma FStar_Tactics_V2_Basic.t_apply_lemma in - let uu___67 + let uu___69 = - let uu___68 + let uu___70 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -469,9 +484,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_options FStar_Tactics_V2_Basic.set_options in - let uu___69 + let uu___71 = - let uu___70 + let uu___72 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -484,9 +499,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_comp FStar_Tactics_V2_Basic.tcc FStar_Tactics_V2_Basic.tcc in - let uu___71 + let uu___73 = - let uu___72 + let uu___74 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -499,9 +514,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.tc FStar_Tactics_V2_Basic.tc in - let uu___73 + let uu___75 = - let uu___74 + let uu___76 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -512,9 +527,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.unshelve FStar_Tactics_V2_Basic.unshelve in - let uu___75 + let uu___77 = - let uu___76 + let uu___78 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -527,16 +542,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_any FStar_Tactics_V2_Basic.unquote (fun - uu___77 + uu___79 -> fun - uu___78 + uu___80 -> FStar_Compiler_Effect.failwith "NBE unquote") in - let uu___77 + let uu___79 = - let uu___78 + let uu___80 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -547,9 +562,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.prune FStar_Tactics_V2_Basic.prune in - let uu___79 + let uu___81 = - let uu___80 + let uu___82 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -560,9 +575,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.addns FStar_Tactics_V2_Basic.addns in - let uu___81 + let uu___83 = - let uu___82 + let uu___84 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -573,9 +588,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.print FStar_Tactics_V2_Basic.print in - let uu___83 + let uu___85 = - let uu___84 + let uu___86 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -586,9 +601,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.debugging FStar_Tactics_V2_Basic.debugging in - let uu___85 + let uu___87 = - let uu___86 + let uu___88 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -599,9 +614,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.ide FStar_Tactics_V2_Basic.ide in - let uu___87 + let uu___89 = - let uu___88 + let uu___90 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -612,9 +627,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dump FStar_Tactics_V2_Basic.dump in - let uu___89 + let uu___91 = - let uu___90 + let uu___92 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -627,9 +642,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dump_all FStar_Tactics_V2_Basic.dump_all in - let uu___91 + let uu___93 = - let uu___92 + let uu___94 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -642,29 +657,29 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dump_uvars_of FStar_Tactics_V2_Basic.dump_uvars_of in - let uu___93 + let uu___95 = - let uu___94 + let uu___96 = - let uu___95 + let uu___97 = FStar_Tactics_Interpreter.e_tactic_1 FStar_Reflection_V2_Embeddings.e_term (FStar_Syntax_Embeddings.e_tuple2 FStar_Syntax_Embeddings.e_bool FStar_Tactics_Embedding.e_ctrl_flag) in - let uu___96 + let uu___98 = FStar_Tactics_Interpreter.e_tactic_thunk FStar_Syntax_Embeddings.e_unit in - let uu___97 + let uu___99 = FStar_Tactics_Interpreter.e_tactic_nbe_1 FStar_Reflection_V2_NBEEmbeddings.e_term (FStar_TypeChecker_NBETerm.e_tuple2 FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_Embedding.e_ctrl_flag_nbe) in - let uu___98 + let uu___100 = FStar_Tactics_Interpreter.e_tactic_nbe_thunk FStar_TypeChecker_NBETerm.e_unit in @@ -672,18 +687,18 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "ctrl_rewrite" FStar_Tactics_Embedding.e_direction - uu___95 - uu___96 - FStar_Syntax_Embeddings.e_unit - FStar_Tactics_Embedding.e_direction_nbe uu___97 uu___98 + FStar_Syntax_Embeddings.e_unit + FStar_Tactics_Embedding.e_direction_nbe + uu___99 + uu___100 FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_CtrlRewrite.ctrl_rewrite FStar_Tactics_CtrlRewrite.ctrl_rewrite in - let uu___95 + let uu___97 = - let uu___96 + let uu___98 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -694,9 +709,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_trefl FStar_Tactics_V2_Basic.t_trefl in - let uu___97 + let uu___99 = - let uu___98 + let uu___100 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -707,9 +722,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dup FStar_Tactics_V2_Basic.dup in - let uu___99 + let uu___101 = - let uu___100 + let uu___102 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -720,9 +735,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.tadmit_t FStar_Tactics_V2_Basic.tadmit_t in - let uu___101 + let uu___103 = - let uu___102 + let uu___104 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -733,9 +748,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.join FStar_Tactics_V2_Basic.join in - let uu___103 + let uu___105 = - let uu___104 + let uu___106 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -752,9 +767,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int)) FStar_Tactics_V2_Basic.t_destruct FStar_Tactics_V2_Basic.t_destruct in - let uu___105 + let uu___107 = - let uu___106 + let uu___108 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -765,9 +780,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Tactics_V2_Basic.top_env FStar_Tactics_V2_Basic.top_env in - let uu___107 + let uu___109 = - let uu___108 + let uu___110 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -778,9 +793,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int FStar_Tactics_V2_Basic.fresh FStar_Tactics_V2_Basic.fresh in - let uu___109 + let uu___111 = - let uu___110 + let uu___112 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -791,9 +806,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int FStar_Tactics_V2_Basic.curms FStar_Tactics_V2_Basic.curms in - let uu___111 + let uu___113 = - let uu___112 + let uu___114 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -808,9 +823,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.uvar_env FStar_Tactics_V2_Basic.uvar_env in - let uu___113 + let uu___115 = - let uu___114 + let uu___116 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -823,9 +838,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.ghost_uvar_env FStar_Tactics_V2_Basic.ghost_uvar_env in - let uu___115 + let uu___117 = - let uu___116 + let uu___118 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -836,9 +851,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.fresh_universe_uvar FStar_Tactics_V2_Basic.fresh_universe_uvar in - let uu___117 + let uu___119 = - let uu___118 + let uu___120 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -853,9 +868,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.unify_env FStar_Tactics_V2_Basic.unify_env in - let uu___119 + let uu___121 = - let uu___120 + let uu___122 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -870,9 +885,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.unify_guard_env FStar_Tactics_V2_Basic.unify_guard_env in - let uu___121 + let uu___123 = - let uu___122 + let uu___124 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -887,9 +902,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.match_env FStar_Tactics_V2_Basic.match_env in - let uu___123 + let uu___125 = - let uu___124 + let uu___126 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -904,9 +919,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.launch_process FStar_Tactics_V2_Basic.launch_process in - let uu___125 + let uu___127 = - let uu___126 + let uu___128 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -917,9 +932,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.change FStar_Tactics_V2_Basic.change in - let uu___127 + let uu___129 = - let uu___128 + let uu___130 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -930,9 +945,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_Embedding.e_guard_policy_nbe FStar_Tactics_V2_Basic.get_guard_policy FStar_Tactics_V2_Basic.get_guard_policy in - let uu___129 + let uu___131 = - let uu___130 + let uu___132 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -943,9 +958,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_guard_policy FStar_Tactics_V2_Basic.set_guard_policy in - let uu___131 + let uu___133 = - let uu___132 + let uu___134 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -956,9 +971,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.lax_on FStar_Tactics_V2_Basic.lax_on in - let uu___133 + let uu___135 = - let uu___134 + let uu___136 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -971,16 +986,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_any FStar_Tactics_V2_Basic.lget (fun - uu___135 + uu___137 -> fun - uu___136 + uu___138 -> FStar_Tactics_Monad.fail "sorry, `lget` does not work in NBE") in - let uu___135 + let uu___137 = - let uu___136 + let uu___138 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_one @@ -995,19 +1010,19 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.lset (fun - uu___137 + uu___139 -> fun - uu___138 + uu___140 -> fun - uu___139 + uu___141 -> FStar_Tactics_Monad.fail "sorry, `lset` does not work in NBE") in - let uu___137 + let uu___139 = - let uu___138 + let uu___140 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_one @@ -1018,9 +1033,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_urgency FStar_Tactics_V2_Basic.set_urgency in - let uu___139 + let uu___141 = - let uu___140 + let uu___142 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_one @@ -1031,9 +1046,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_dump_on_failure FStar_Tactics_V2_Basic.set_dump_on_failure in - let uu___141 + let uu___143 = - let uu___142 + let uu___144 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_one @@ -1044,9 +1059,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_commute_applied_match FStar_Tactics_V2_Basic.t_commute_applied_match in - let uu___143 + let uu___145 = - let uu___144 + let uu___146 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1057,9 +1072,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.gather_explicit_guards_for_resolved_goals FStar_Tactics_V2_Basic.gather_explicit_guards_for_resolved_goals in - let uu___145 + let uu___147 = - let uu___146 + let uu___148 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1072,9 +1087,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.string_to_term FStar_Tactics_V2_Basic.string_to_term in - let uu___147 + let uu___149 = - let uu___148 + let uu___150 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1091,9 +1106,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_binding) FStar_Tactics_V2_Basic.push_bv_dsenv FStar_Tactics_V2_Basic.push_bv_dsenv in - let uu___149 + let uu___151 = - let uu___150 + let uu___152 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1104,9 +1119,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.term_to_string FStar_Tactics_V2_Basic.term_to_string in - let uu___151 + let uu___153 = - let uu___152 + let uu___154 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1117,9 +1132,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.comp_to_string FStar_Tactics_V2_Basic.comp_to_string in - let uu___153 + let uu___155 = - let uu___154 + let uu___156 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1130,9 +1145,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_document FStar_Tactics_V2_Basic.term_to_doc FStar_Tactics_V2_Basic.term_to_doc in - let uu___155 + let uu___157 = - let uu___156 + let uu___158 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1143,9 +1158,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_document FStar_Tactics_V2_Basic.comp_to_doc FStar_Tactics_V2_Basic.comp_to_doc in - let uu___157 + let uu___159 = - let uu___158 + let uu___160 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1156,9 +1171,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.range_to_string FStar_Tactics_V2_Basic.range_to_string in - let uu___159 + let uu___161 = - let uu___160 + let uu___162 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1171,15 +1186,15 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.term_eq_old FStar_Tactics_V2_Basic.term_eq_old in - let uu___161 + let uu___163 = - let uu___162 + let uu___164 = - let uu___163 + let uu___165 = FStar_Tactics_Interpreter.e_tactic_thunk FStar_Syntax_Embeddings.e_any in - let uu___164 + let uu___166 = FStar_Tactics_Interpreter.e_tactic_nbe_thunk FStar_TypeChecker_NBETerm.e_any in @@ -1188,23 +1203,23 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = "with_compat_pre_core" FStar_Syntax_Embeddings.e_any FStar_Syntax_Embeddings.e_int - uu___163 + uu___165 FStar_Syntax_Embeddings.e_any FStar_TypeChecker_NBETerm.e_any FStar_TypeChecker_NBETerm.e_int - uu___164 + uu___166 FStar_TypeChecker_NBETerm.e_any (fun - uu___165 + uu___167 -> FStar_Tactics_V2_Basic.with_compat_pre_core) (fun - uu___165 + uu___167 -> FStar_Tactics_V2_Basic.with_compat_pre_core) in - let uu___163 + let uu___165 = - let uu___164 + let uu___166 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1215,9 +1230,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_vconfig FStar_Tactics_V2_Basic.get_vconfig FStar_Tactics_V2_Basic.get_vconfig in - let uu___165 + let uu___167 = - let uu___166 + let uu___168 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1228,9 +1243,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_vconfig FStar_Tactics_V2_Basic.set_vconfig in - let uu___167 + let uu___169 = - let uu___168 + let uu___170 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1241,9 +1256,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_smt_sync FStar_Tactics_V2_Basic.t_smt_sync in - let uu___169 + let uu___171 = - let uu___170 + let uu___172 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1256,9 +1271,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int) FStar_Tactics_V2_Basic.free_uvars FStar_Tactics_V2_Basic.free_uvars in - let uu___171 + let uu___173 = - let uu___172 + let uu___174 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1275,9 +1290,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string)) FStar_Tactics_V2_Basic.all_ext_options FStar_Tactics_V2_Basic.all_ext_options in - let uu___173 + let uu___175 = - let uu___174 + let uu___176 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1288,9 +1303,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.ext_getv FStar_Tactics_V2_Basic.ext_getv in - let uu___175 + let uu___177 = - let uu___176 + let uu___178 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1307,9 +1322,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string)) FStar_Tactics_V2_Basic.ext_getns FStar_Tactics_V2_Basic.ext_getns in - let uu___177 + let uu___179 = - let uu___178 + let uu___180 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -1323,16 +1338,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = (FStar_Tactics_Embedding.e_tref_nbe ()) (fun - uu___179 + uu___181 -> FStar_Tactics_V2_Basic.alloc) (fun - uu___179 + uu___181 -> FStar_Tactics_V2_Basic.alloc) in - let uu___179 + let uu___181 = - let uu___180 + let uu___182 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -1346,16 +1361,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = ()) FStar_TypeChecker_NBETerm.e_any (fun - uu___181 + uu___183 -> FStar_Tactics_V2_Basic.read) (fun - uu___181 + uu___183 -> FStar_Tactics_V2_Basic.read) in - let uu___181 + let uu___183 = - let uu___182 + let uu___184 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_one @@ -1371,16 +1386,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_any FStar_TypeChecker_NBETerm.e_unit (fun - uu___183 + uu___185 -> FStar_Tactics_V2_Basic.write) (fun - uu___183 + uu___185 -> FStar_Tactics_V2_Basic.write) in - let uu___183 + let uu___185 = - let uu___184 + let uu___186 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1401,9 +1416,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_is_non_informative FStar_Tactics_V2_Basic.refl_is_non_informative in - let uu___185 + let uu___187 = - let uu___186 + let uu___188 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1426,9 +1441,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_check_subtyping FStar_Tactics_V2_Basic.refl_check_subtyping in - let uu___187 + let uu___189 = - let uu___188 + let uu___190 = FStar_Tactics_InterpFuns.mk_tac_step_5 Prims.int_zero @@ -1455,9 +1470,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.t_refl_check_equiv FStar_Tactics_V2_Basic.t_refl_check_equiv in - let uu___189 + let uu___191 = - let uu___190 + let uu___192 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1482,9 +1497,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_core_compute_term_type FStar_Tactics_V2_Basic.refl_core_compute_term_type in - let uu___191 + let uu___193 = - let uu___192 + let uu___194 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -1509,9 +1524,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_core_check_term FStar_Tactics_V2_Basic.refl_core_check_term in - let uu___193 + let uu___195 = - let uu___194 + let uu___196 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1534,9 +1549,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_core_check_term_at_type FStar_Tactics_V2_Basic.refl_core_check_term_at_type in - let uu___195 + let uu___197 = - let uu___196 + let uu___198 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1565,9 +1580,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_tc_term FStar_Tactics_V2_Basic.refl_tc_term in - let uu___197 + let uu___199 = - let uu___198 + let uu___200 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1588,9 +1603,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_universe_of FStar_Tactics_V2_Basic.refl_universe_of in - let uu___199 + let uu___201 = - let uu___200 + let uu___202 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1611,9 +1626,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_check_prop_validity FStar_Tactics_V2_Basic.refl_check_prop_validity in - let uu___201 + let uu___203 = - let uu___202 + let uu___204 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -1644,11 +1659,11 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_binding)))) FStar_Tactics_V2_Basic.refl_check_match_complete FStar_Tactics_V2_Basic.refl_check_match_complete in - let uu___203 + let uu___205 = - let uu___204 + let uu___206 = - let uu___205 + let uu___207 = e_ret_t (FStar_Syntax_Embeddings.e_tuple3 @@ -1661,7 +1676,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = uu___2) (solve uu___2)) in - let uu___206 + let uu___208 = nbe_e_ret_t (FStar_TypeChecker_NBETerm.e_tuple3 @@ -1681,26 +1696,26 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = uu___2 (FStar_Syntax_Embeddings.e_option uu___2) - uu___205 + uu___207 FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute (FStar_TypeChecker_NBETerm.e_option FStar_Reflection_V2_NBEEmbeddings.e_attribute) - uu___206 + uu___208 FStar_Tactics_V2_Basic.refl_instantiate_implicits FStar_Tactics_V2_Basic.refl_instantiate_implicits in - let uu___205 + let uu___207 = - let uu___206 + let uu___208 = - let uu___207 + let uu___209 = e_ret_t (FStar_Syntax_Embeddings.e_list (FStar_Syntax_Embeddings.e_tuple2 FStar_Reflection_V2_Embeddings.e_namedv FStar_Reflection_V2_Embeddings.e_term)) in - let uu___208 + let uu___210 = nbe_e_ret_t (FStar_TypeChecker_NBETerm.e_list @@ -1717,7 +1732,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_Embeddings.e_term)) uu___2 uu___2 - uu___207 + uu___209 FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_list (FStar_TypeChecker_NBETerm.e_tuple2 @@ -1725,12 +1740,12 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_term)) FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute - uu___208 + uu___210 FStar_Tactics_V2_Basic.refl_try_unify FStar_Tactics_V2_Basic.refl_try_unify in - let uu___207 + let uu___209 = - let uu___208 + let uu___210 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1753,9 +1768,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_maybe_relate_after_unfolding FStar_Tactics_V2_Basic.refl_maybe_relate_after_unfolding in - let uu___209 + let uu___211 = - let uu___210 + let uu___212 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1776,9 +1791,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_maybe_unfold_head FStar_Tactics_V2_Basic.refl_maybe_unfold_head in - let uu___211 + let uu___213 = - let uu___212 + let uu___214 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1795,9 +1810,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.refl_norm_well_typed_term FStar_Tactics_V2_Basic.refl_norm_well_typed_term in - let uu___213 + let uu___215 = - let uu___214 + let uu___216 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1810,9 +1825,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Tactics_V2_Basic.push_open_namespace FStar_Tactics_V2_Basic.push_open_namespace in - let uu___215 + let uu___217 = - let uu___216 + let uu___218 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1827,9 +1842,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Tactics_V2_Basic.push_module_abbrev FStar_Tactics_V2_Basic.push_module_abbrev in - let uu___217 + let uu___219 = - let uu___218 + let uu___220 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1850,9 +1865,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_fv))) FStar_Tactics_V2_Basic.resolve_name FStar_Tactics_V2_Basic.resolve_name in - let uu___219 + let uu___221 = - let uu___220 + let uu___222 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1865,15 +1880,15 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.log_issues FStar_Tactics_V2_Basic.log_issues in - let uu___221 + let uu___223 = - let uu___222 + let uu___224 = - let uu___223 + let uu___225 = FStar_Tactics_Interpreter.e_tactic_thunk FStar_Syntax_Embeddings.e_unit in - let uu___224 + let uu___226 = FStar_Tactics_Interpreter.e_tactic_nbe_thunk FStar_TypeChecker_NBETerm.e_unit in @@ -1881,7 +1896,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "call_subtac" FStar_Reflection_V2_Embeddings.e_env - uu___223 + uu___225 FStar_Reflection_V2_Embeddings.e_universe uu___2 (FStar_Syntax_Embeddings.e_tuple2 @@ -1890,7 +1905,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue)) FStar_Reflection_V2_NBEEmbeddings.e_env - uu___224 + uu___226 FStar_Reflection_V2_NBEEmbeddings.e_universe FStar_Reflection_V2_NBEEmbeddings.e_attribute (FStar_TypeChecker_NBETerm.e_tuple2 @@ -1900,9 +1915,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.call_subtac FStar_Tactics_V2_Basic.call_subtac in - let uu___223 + let uu___225 = - let uu___224 + let uu___226 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -1927,7 +1942,10 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.call_subtac_tm FStar_Tactics_V2_Basic.call_subtac_tm in - [uu___224] in + [uu___226] in + uu___224 + :: + uu___225 in uu___222 :: uu___223 in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_SyntaxHelpers.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_SyntaxHelpers.ml index 642450a30b2..5ac08771b55 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_SyntaxHelpers.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_SyntaxHelpers.ml @@ -57,18 +57,33 @@ let (collect_arr_bs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (26)) (Prims.of_int (18)) (Prims.of_int (26)) + (Prims.of_int (25)) (Prims.of_int (18)) (Prims.of_int (25)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (25)) (Prims.of_int (22)) (Prims.of_int (27)) + (Prims.of_int (24)) (Prims.of_int (22)) (Prims.of_int (26)) (Prims.of_int (29))))) (Obj.magic uu___) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> match uu___1 with | (bs, c) -> ((FStar_List_Tot_Base.rev bs), c))) +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.collect_arr_bs" (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.V2.SyntaxHelpers.collect_arr_bs (plugin)" + (FStar_Tactics_Native.from_tactic_1 collect_arr_bs) + FStar_Reflection_V2_Embeddings.e_term + (FStar_Syntax_Embeddings.e_tuple2 + (FStar_Syntax_Embeddings.e_list + FStar_Tactics_NamedView.e_binder) + FStar_Reflection_V2_Embeddings.e_comp_view) psc ncb us args) let (collect_arr : FStar_Reflection_Types.typ -> ((FStar_Reflection_Types.typ Prims.list * FStar_Tactics_NamedView.comp), @@ -80,12 +95,12 @@ let (collect_arr : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (31)) (Prims.of_int (18)) (Prims.of_int (31)) + (Prims.of_int (29)) (Prims.of_int (18)) (Prims.of_int (29)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (30)) (Prims.of_int (19)) (Prims.of_int (33)) + (Prims.of_int (28)) (Prims.of_int (19)) (Prims.of_int (31)) (Prims.of_int (29))))) (Obj.magic uu___) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac @@ -95,6 +110,21 @@ let (collect_arr : ((FStar_List_Tot_Base.rev (FStar_List_Tot_Base.map (fun b -> b.FStar_Tactics_NamedView.sort) bs)), c))) +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.collect_arr" (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.V2.SyntaxHelpers.collect_arr (plugin)" + (FStar_Tactics_Native.from_tactic_1 collect_arr) + FStar_Reflection_V2_Embeddings.e_term + (FStar_Syntax_Embeddings.e_tuple2 + (FStar_Syntax_Embeddings.e_list + FStar_Reflection_V2_Embeddings.e_term) + FStar_Reflection_V2_Embeddings.e_comp_view) psc ncb us args) let rec (collect_abs' : FStar_Tactics_NamedView.binder Prims.list -> FStar_Tactics_NamedView.term -> @@ -109,12 +139,12 @@ let rec (collect_abs' : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (37)) (Prims.of_int (10)) (Prims.of_int (37)) + (Prims.of_int (35)) (Prims.of_int (10)) (Prims.of_int (35)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (37)) (Prims.of_int (4)) (Prims.of_int (40)) + (Prims.of_int (35)) (Prims.of_int (4)) (Prims.of_int (38)) (Prims.of_int (18))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -138,18 +168,33 @@ let (collect_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (44)) (Prims.of_int (19)) (Prims.of_int (44)) + (Prims.of_int (41)) (Prims.of_int (19)) (Prims.of_int (41)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (43)) (Prims.of_int (19)) (Prims.of_int (45)) + (Prims.of_int (40)) (Prims.of_int (19)) (Prims.of_int (42)) (Prims.of_int (30))))) (Obj.magic uu___) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> match uu___1 with | (bs, t') -> ((FStar_List_Tot_Base.rev bs), t'))) +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.collect_abs" (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.V2.SyntaxHelpers.collect_abs (plugin)" + (FStar_Tactics_Native.from_tactic_1 collect_abs) + FStar_Reflection_V2_Embeddings.e_term + (FStar_Syntax_Embeddings.e_tuple2 + (FStar_Syntax_Embeddings.e_list + FStar_Tactics_NamedView.e_binder) + FStar_Reflection_V2_Embeddings.e_term) psc ncb us args) let fail : 'a . Prims.string -> ('a, unit) FStar_Tactics_Effect.tac_repr = fun uu___ -> (fun m -> @@ -187,14 +232,14 @@ let rec (mk_arr : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (56)) (Prims.of_int (32)) - (Prims.of_int (56)) (Prims.of_int (47))))) + (Prims.of_int (53)) (Prims.of_int (32)) + (Prims.of_int (53)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (56)) (Prims.of_int (23)) - (Prims.of_int (56)) (Prims.of_int (48))))) + (Prims.of_int (53)) (Prims.of_int (23)) + (Prims.of_int (53)) (Prims.of_int (48))))) (Obj.magic uu___2) (fun uu___3 -> FStar_Tactics_Effect.lift_div_tac @@ -205,14 +250,14 @@ let rec (mk_arr : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (56)) (Prims.of_int (23)) - (Prims.of_int (56)) (Prims.of_int (48))))) + (Prims.of_int (53)) (Prims.of_int (23)) + (Prims.of_int (53)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (56)) (Prims.of_int (11)) - (Prims.of_int (56)) (Prims.of_int (49))))) + (Prims.of_int (53)) (Prims.of_int (11)) + (Prims.of_int (53)) (Prims.of_int (49))))) (Obj.magic uu___1) (fun uu___2 -> FStar_Tactics_Effect.lift_div_tac @@ -223,8 +268,8 @@ let rec (mk_arr : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (56)) (Prims.of_int (11)) - (Prims.of_int (56)) (Prims.of_int (49))))) + (Prims.of_int (53)) (Prims.of_int (11)) + (Prims.of_int (53)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "dummy" Prims.int_zero @@ -235,6 +280,20 @@ let rec (mk_arr : (fun uu___2 -> FStar_Tactics_NamedView.pack uu___1))))) uu___1 uu___ +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.mk_arr" (Prims.of_int (3)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_2 + "FStar.Tactics.V2.SyntaxHelpers.mk_arr (plugin)" + (FStar_Tactics_Native.from_tactic_2 mk_arr) + (FStar_Syntax_Embeddings.e_list + FStar_Tactics_NamedView.e_binder) + FStar_Reflection_V2_Embeddings.e_comp_view + FStar_Reflection_V2_Embeddings.e_term psc ncb us args) let rec (mk_tot_arr : FStar_Tactics_NamedView.binder Prims.list -> FStar_Tactics_NamedView.term -> @@ -260,14 +319,14 @@ let rec (mk_tot_arr : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (62)) (Prims.of_int (32)) - (Prims.of_int (62)) (Prims.of_int (51))))) + (Prims.of_int (59)) (Prims.of_int (32)) + (Prims.of_int (59)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (62)) (Prims.of_int (23)) - (Prims.of_int (62)) (Prims.of_int (52))))) + (Prims.of_int (59)) (Prims.of_int (23)) + (Prims.of_int (59)) (Prims.of_int (52))))) (Obj.magic uu___2) (fun uu___3 -> FStar_Tactics_Effect.lift_div_tac @@ -278,14 +337,14 @@ let rec (mk_tot_arr : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (62)) (Prims.of_int (23)) - (Prims.of_int (62)) (Prims.of_int (52))))) + (Prims.of_int (59)) (Prims.of_int (23)) + (Prims.of_int (59)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (62)) (Prims.of_int (11)) - (Prims.of_int (62)) (Prims.of_int (53))))) + (Prims.of_int (59)) (Prims.of_int (11)) + (Prims.of_int (59)) (Prims.of_int (53))))) (Obj.magic uu___1) (fun uu___2 -> FStar_Tactics_Effect.lift_div_tac @@ -296,8 +355,8 @@ let rec (mk_tot_arr : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (62)) (Prims.of_int (11)) - (Prims.of_int (62)) (Prims.of_int (53))))) + (Prims.of_int (59)) (Prims.of_int (11)) + (Prims.of_int (59)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "dummy" Prims.int_zero @@ -308,6 +367,20 @@ let rec (mk_tot_arr : (fun uu___2 -> FStar_Tactics_NamedView.pack uu___1))))) uu___1 uu___ +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.mk_tot_arr" (Prims.of_int (3)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_2 + "FStar.Tactics.V2.SyntaxHelpers.mk_tot_arr (plugin)" + (FStar_Tactics_Native.from_tactic_2 mk_tot_arr) + (FStar_Syntax_Embeddings.e_list + FStar_Tactics_NamedView.e_binder) + FStar_Reflection_V2_Embeddings.e_term + FStar_Reflection_V2_Embeddings.e_term psc ncb us args) let (lookup_lb : FStar_Tactics_NamedView.letbinding Prims.list -> FStar_Reflection_Types.name -> @@ -329,12 +402,12 @@ let (lookup_lb : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (65)) (Prims.of_int (10)) (Prims.of_int (67)) + (Prims.of_int (62)) (Prims.of_int (10)) (Prims.of_int (64)) (Prims.of_int (16))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (69)) (Prims.of_int (2)) (Prims.of_int (71)) + (Prims.of_int (66)) (Prims.of_int (2)) (Prims.of_int (68)) (Prims.of_int (59))))) (Obj.magic uu___) (fun uu___1 -> (fun o -> @@ -348,6 +421,21 @@ let (lookup_lb : (Obj.repr (fail "lookup_letbinding: Name not in let group"))) uu___1) +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.lookup_lb" (Prims.of_int (3)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_2 + "FStar.Tactics.V2.SyntaxHelpers.lookup_lb (plugin)" + (FStar_Tactics_Native.from_tactic_2 lookup_lb) + (FStar_Syntax_Embeddings.e_list + FStar_Tactics_NamedView.e_letbinding) + (FStar_Syntax_Embeddings.e_list + FStar_Syntax_Embeddings.e_string) + FStar_Tactics_NamedView.e_letbinding psc ncb us args) let rec (inspect_unascribe : FStar_Tactics_NamedView.term -> (FStar_Tactics_NamedView.term_view, unit) FStar_Tactics_Effect.tac_repr) @@ -358,12 +446,12 @@ let rec (inspect_unascribe : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (74)) (Prims.of_int (8)) (Prims.of_int (74)) + (Prims.of_int (71)) (Prims.of_int (8)) (Prims.of_int (71)) (Prims.of_int (17))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (74)) (Prims.of_int (2)) (Prims.of_int (78)) + (Prims.of_int (71)) (Prims.of_int (2)) (Prims.of_int (75)) (Prims.of_int (12))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -379,6 +467,18 @@ let rec (inspect_unascribe : (Obj.repr (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> tv)))) uu___1) +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.inspect_unascribe" (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.V2.SyntaxHelpers.inspect_unascribe (plugin)" + (FStar_Tactics_Native.from_tactic_1 inspect_unascribe) + FStar_Reflection_V2_Embeddings.e_term + FStar_Tactics_NamedView.e_named_term_view psc ncb us args) let rec (collect_app' : FStar_Reflection_V2_Data.argv Prims.list -> FStar_Tactics_NamedView.term -> @@ -393,12 +493,12 @@ let rec (collect_app' : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (83)) (Prims.of_int (10)) (Prims.of_int (83)) + (Prims.of_int (80)) (Prims.of_int (10)) (Prims.of_int (80)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (83)) (Prims.of_int (4)) (Prims.of_int (86)) + (Prims.of_int (80)) (Prims.of_int (4)) (Prims.of_int (83)) (Prims.of_int (20))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -416,6 +516,24 @@ let (collect_app : Prims.list), unit) FStar_Tactics_Effect.tac_repr) = collect_app' [] +let _ = + FStar_Tactics_Native.register_tactic + "FStar.Tactics.V2.SyntaxHelpers.collect_app" (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.V2.SyntaxHelpers.collect_app (plugin)" + (FStar_Tactics_Native.from_tactic_1 collect_app) + FStar_Reflection_V2_Embeddings.e_term + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Reflection_V2_Embeddings.e_term + (FStar_Syntax_Embeddings.e_list + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Reflection_V2_Embeddings.e_term + FStar_Reflection_V2_Embeddings.e_aqualv))) psc ncb us + args) let (hua : FStar_Tactics_NamedView.term -> ((FStar_Reflection_Types.fv * FStar_Reflection_V2_Data.universes * @@ -429,12 +547,12 @@ let (hua : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (92)) (Prims.of_int (17)) (Prims.of_int (92)) + (Prims.of_int (89)) (Prims.of_int (17)) (Prims.of_int (89)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (91)) (Prims.of_int (62)) (Prims.of_int (96)) + (Prims.of_int (88)) (Prims.of_int (62)) (Prims.of_int (93)) (Prims.of_int (13))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -447,14 +565,14 @@ let (hua : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (93)) (Prims.of_int (8)) - (Prims.of_int (93)) (Prims.of_int (18))))) + (Prims.of_int (90)) (Prims.of_int (8)) + (Prims.of_int (90)) (Prims.of_int (18))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.V2.SyntaxHelpers.fst" - (Prims.of_int (93)) (Prims.of_int (2)) - (Prims.of_int (96)) (Prims.of_int (13))))) + (Prims.of_int (90)) (Prims.of_int (2)) + (Prims.of_int (93)) (Prims.of_int (13))))) (Obj.magic uu___2) (fun uu___3 -> FStar_Tactics_Effect.lift_div_tac @@ -465,4 +583,25 @@ let (hua : | FStar_Tactics_NamedView.Tv_UInst (fv, us) -> FStar_Pervasives_Native.Some (fv, us, args) | uu___5 -> FStar_Pervasives_Native.None)))) - uu___1) \ No newline at end of file + uu___1) +let _ = + FStar_Tactics_Native.register_tactic "FStar.Tactics.V2.SyntaxHelpers.hua" + (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.V2.SyntaxHelpers.hua (plugin)" + (FStar_Tactics_Native.from_tactic_1 hua) + FStar_Reflection_V2_Embeddings.e_term + (FStar_Syntax_Embeddings.e_option + (FStar_Syntax_Embeddings.e_tuple3 + FStar_Reflection_V2_Embeddings.e_fv + (FStar_Syntax_Embeddings.e_list + FStar_Reflection_V2_Embeddings.e_universe) + (FStar_Syntax_Embeddings.e_list + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Reflection_V2_Embeddings.e_term + FStar_Reflection_V2_Embeddings.e_aqualv)))) psc + ncb us args) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 9c2bb7b228d..f30e3953114 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -5553,8 +5553,7 @@ and (desugar_comp : FStar_Compiler_Range_Type.range -> Prims.bool -> FStar_Syntax_DsEnv.env -> - FStar_Parser_AST.term -> - FStar_Syntax_Syntax.comp' FStar_Syntax_Syntax.syntax) + FStar_Parser_AST.term -> FStar_Syntax_Syntax.comp) = fun r -> fun allow_type_promotion -> @@ -6739,7 +6738,7 @@ let (mk_typ_abbrev : FStar_Parser_AST.decl -> FStar_Ident.lident -> FStar_Syntax_Syntax.univ_name Prims.list -> - FStar_Syntax_Syntax.binder Prims.list -> + FStar_Syntax_Syntax.binders -> FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option -> FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax -> FStar_Ident.lident Prims.list ->