From b55e813f8166b9cfd440e1e1492b25bde63159ed Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Fri, 28 Jul 2023 06:43:26 +0000 Subject: [PATCH] snap --- src/ocaml/plugin/PulseSyntaxWrapper.ml | 4 +- src/ocaml/plugin/generated/PulseDesugar.ml | 4 +- src/ocaml/plugin/generated/Pulse_Checker.ml | 495 +++++++------ .../plugin/generated/Pulse_Checker_Exists.ml | 629 +++------------- .../Pulse_Checker_Prover_IntroExists.ml | 233 +++--- .../plugin/generated/Pulse_Checker_Pure.ml | 695 ++++++++++-------- .../plugin/generated/Pulse_Elaborate_Core.ml | 10 - .../plugin/generated/Pulse_Syntax_Base.ml | 6 +- .../plugin/generated/Pulse_Syntax_Builder.ml | 18 +- .../plugin/generated/Pulse_Syntax_Naming.ml | 7 +- .../plugin/generated/Pulse_Syntax_Printer.ml | 91 +-- src/ocaml/plugin/generated/Pulse_Typing.ml | 6 +- .../generated/Pulse_Typing_Metatheory_Base.ml | 15 - src/syntax_extension/PulseDesugar.fst | 2 +- src/syntax_extension/PulseSyntaxWrapper.fsti | 2 +- 15 files changed, 865 insertions(+), 1352 deletions(-) diff --git a/src/ocaml/plugin/PulseSyntaxWrapper.ml b/src/ocaml/plugin/PulseSyntaxWrapper.ml index 08c24674a..3cf984ee0 100755 --- a/src/ocaml/plugin/PulseSyntaxWrapper.ml +++ b/src/ocaml/plugin/PulseSyntaxWrapper.ml @@ -124,8 +124,8 @@ let tm_if (head:term) (returns_annot:vprop option) (then_:st_term) (else_:st_ter let tm_match (sc:term) (returns_:vprop option) (brs:branch list) r : st_term = PSB.(with_range (tm_match sc returns_ brs) r) -let tm_intro_exists (erased:bool) (p:vprop) (witnesses:term list) r : st_term = - PSB.(with_range (tm_intro_exists erased p witnesses) r) +let tm_intro_exists (p:vprop) (witnesses:term list) r : st_term = + PSB.(with_range (tm_intro_exists p witnesses) r) let is_tm_intro_exists (s:st_term) : bool = match s.term1 with diff --git a/src/ocaml/plugin/generated/PulseDesugar.ml b/src/ocaml/plugin/generated/PulseDesugar.ml index 1e0a03c30..5dbeabfe1 100644 --- a/src/ocaml/plugin/generated/PulseDesugar.ml +++ b/src/ocaml/plugin/generated/PulseDesugar.ml @@ -853,8 +853,8 @@ let rec (desugar_stmt : op_let_Question uu___2 (fun witnesses1 -> let uu___3 = - PulseSyntaxWrapper.tm_intro_exists false vp - witnesses1 s.PulseSugar.range1 in + PulseSyntaxWrapper.tm_intro_exists vp witnesses1 + s.PulseSugar.range1 in return uu___3))) | PulseSugar.Parallel { PulseSugar.p1 = p1; PulseSugar.p2 = p2; PulseSugar.q1 = q1; diff --git a/src/ocaml/plugin/generated/Pulse_Checker.ml b/src/ocaml/plugin/generated/Pulse_Checker.ml index b6cf9779e..24f4f5bc3 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker.ml @@ -178,7 +178,7 @@ let (instantiate_unknown_witnesses : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" (Prims.of_int (76)) - (Prims.of_int (51)) (Prims.of_int (76)) (Prims.of_int (57))))) + (Prims.of_int (43)) (Prims.of_int (76)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" (Prims.of_int (74)) @@ -189,8 +189,7 @@ let (instantiate_unknown_witnesses : (fun uu___ -> match uu___ with | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = erased; - Pulse_Syntax_Base.p2 = p; + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = ws;_} -> Obj.magic @@ -203,7 +202,7 @@ let (instantiate_unknown_witnesses : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (76)) (Prims.of_int (60)) + (Prims.of_int (76)) (Prims.of_int (52)) (Prims.of_int (98)) (Prims.of_int (10))))) (Obj.magic (gen_names_for_unknowns g p ws)) (fun uu___1 -> @@ -280,8 +279,6 @@ let (instantiate_unknown_witnesses : = (Pulse_Syntax_Base.Tm_IntroExists { - Pulse_Syntax_Base.erased - = erased; Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses @@ -295,154 +292,140 @@ let (instantiate_unknown_witnesses : Pulse_Syntax_Base.range2 = (t.Pulse_Syntax_Base.range2) })))))) uu___) -let (maybe_intro_exists_erased : - Pulse_Syntax_Base.st_term -> Pulse_Syntax_Base.st_term) = - fun t -> - let uu___ = t.Pulse_Syntax_Base.term1 in - match uu___ with - | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = erased; Pulse_Syntax_Base.p2 = p; - Pulse_Syntax_Base.witnesses = w::[];_} - -> - (match Pulse_Syntax_Pure.unreveal w with - | FStar_Pervasives_Native.Some w1 -> - let t' = - Pulse_Syntax_Base.Tm_IntroExists - { - Pulse_Syntax_Base.erased = true; - Pulse_Syntax_Base.p2 = p; - Pulse_Syntax_Base.witnesses = [w1] - } in - { - Pulse_Syntax_Base.term1 = t'; - Pulse_Syntax_Base.range2 = (t.Pulse_Syntax_Base.range2) - } - | uu___1 -> t) let rec (transform_to_unary_intro_exists : Pulse_Typing_Env.env -> Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term Prims.list -> - (Pulse_Syntax_Base.st_term, unit) FStar_Tactics_Effect.tac_repr) + FStar_Range.range -> + (Pulse_Syntax_Base.st_term, unit) FStar_Tactics_Effect.tac_repr) = - fun uu___2 -> - fun uu___1 -> - fun uu___ -> - (fun g -> - fun t -> - fun ws -> - match ws with - | [] -> - Obj.magic - (Obj.repr - (Pulse_Typing_Env.fail g - (FStar_Pervasives_Native.Some - (t.Pulse_Syntax_Base.range1)) - "intro exists with empty witnesses")) - | w::[] -> - Obj.magic - (Obj.repr - (if - Pulse_Syntax_Base.uu___is_Tm_ExistsSL - t.Pulse_Syntax_Base.t - then - Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun uu___ -> - Pulse_Typing.wr - (Pulse_Syntax_Base.Tm_IntroExists - { - Pulse_Syntax_Base.erased = false; - Pulse_Syntax_Base.p2 = t; - Pulse_Syntax_Base.witnesses = [w] - }))) - else - Obj.repr - (Pulse_Typing_Env.fail g - (FStar_Pervasives_Native.Some - (t.Pulse_Syntax_Base.range1)) - "intro exists with non-existential"))) - | w::ws1 -> - Obj.magic - (Obj.repr - (match t.Pulse_Syntax_Base.t with - | Pulse_Syntax_Base.Tm_ExistsSL (u, b, body) -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.fst" - (Prims.of_int (122)) - (Prims.of_int (17)) - (Prims.of_int (122)) - (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.fst" - (Prims.of_int (122)) - (Prims.of_int (46)) - (Prims.of_int (128)) - (Prims.of_int (35))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___ -> - Pulse_Syntax_Naming.subst_term body - [Pulse_Syntax_Naming.DT - (Prims.int_zero, w)])) - (fun uu___ -> - (fun body1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.fst" - (Prims.of_int (123)) - (Prims.of_int (15)) - (Prims.of_int (123)) - (Prims.of_int (56))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.fst" - (Prims.of_int (126)) - (Prims.of_int (6)) - (Prims.of_int (128)) - (Prims.of_int (35))))) - (Obj.magic - (transform_to_unary_intro_exists - g body1 ws1)) - (fun st -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___ -> - Pulse_Typing.wr - (Pulse_Syntax_Base.Tm_Bind - { - Pulse_Syntax_Base.binder - = - (Pulse_Syntax_Base.null_binder - Pulse_Typing.tm_unit); - Pulse_Syntax_Base.head1 - = st; - Pulse_Syntax_Base.body1 - = - (Pulse_Typing.wr - (Pulse_Syntax_Base.Tm_IntroExists - { - Pulse_Syntax_Base.erased - = true; - Pulse_Syntax_Base.p2 - = t; - Pulse_Syntax_Base.witnesses - = - [w] - })) - }))))) uu___) - | uu___ -> - Pulse_Typing_Env.fail g + fun uu___3 -> + fun uu___2 -> + fun uu___1 -> + fun uu___ -> + (fun g -> + fun t -> + fun ws -> + fun r -> + match ws with + | [] -> + Obj.magic + (Obj.repr + (Pulse_Typing_Env.fail g (FStar_Pervasives_Native.Some (t.Pulse_Syntax_Base.range1)) - "intro exists with non-existential"))) uu___2 - uu___1 uu___ + "intro exists with empty witnesses")) + | w::[] -> + Obj.magic + (Obj.repr + (if + Pulse_Syntax_Base.uu___is_Tm_ExistsSL + t.Pulse_Syntax_Base.t + then + Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___ -> + { + Pulse_Syntax_Base.term1 = + (Pulse_Syntax_Base.Tm_IntroExists + { + Pulse_Syntax_Base.p2 = t; + Pulse_Syntax_Base.witnesses = + [w] + }); + Pulse_Syntax_Base.range2 = r + })) + else + Obj.repr + (Pulse_Typing_Env.fail g + (FStar_Pervasives_Native.Some + (t.Pulse_Syntax_Base.range1)) + "intro exists with non-existential"))) + | w::ws1 -> + Obj.magic + (Obj.repr + (match t.Pulse_Syntax_Base.t with + | Pulse_Syntax_Base.Tm_ExistsSL (u, b, body) -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.fst" + (Prims.of_int (122)) + (Prims.of_int (17)) + (Prims.of_int (122)) + (Prims.of_int (43))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.fst" + (Prims.of_int (122)) + (Prims.of_int (46)) + (Prims.of_int (129)) + (Prims.of_int (19))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___ -> + Pulse_Syntax_Naming.subst_term body + [Pulse_Syntax_Naming.DT + (Prims.int_zero, w)])) + (fun uu___ -> + (fun body1 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.fst" + (Prims.of_int (123)) + (Prims.of_int (15)) + (Prims.of_int (123)) + (Prims.of_int (58))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.fst" + (Prims.of_int (126)) + (Prims.of_int (8)) + (Prims.of_int (129)) + (Prims.of_int (17))))) + (Obj.magic + (transform_to_unary_intro_exists + g body1 ws1 r)) + (fun st -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___ -> + { + Pulse_Syntax_Base.term1 + = + (Pulse_Syntax_Base.Tm_Bind + { + Pulse_Syntax_Base.binder + = + (Pulse_Syntax_Base.null_binder + Pulse_Typing.tm_unit); + Pulse_Syntax_Base.head1 + = st; + Pulse_Syntax_Base.body1 + = + (Pulse_Typing.wr + ( + Pulse_Syntax_Base.Tm_IntroExists + { + Pulse_Syntax_Base.p2 + = t; + Pulse_Syntax_Base.witnesses + = [w] + })) + }); + Pulse_Syntax_Base.range2 + = r + })))) uu___) + | uu___ -> + Pulse_Typing_Env.fail g + (FStar_Pervasives_Native.Some + (t.Pulse_Syntax_Base.range1)) + "intro exists with non-existential"))) + uu___3 uu___2 uu___1 uu___ let rec (check : Pulse_Checker_Base.check_t) = fun g0 -> fun pre0 -> @@ -454,13 +437,13 @@ let rec (check : Pulse_Checker_Base.check_t) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (148)) (Prims.of_int (4)) - (Prims.of_int (148)) (Prims.of_int (55))))) + (Prims.of_int (149)) (Prims.of_int (4)) + (Prims.of_int (149)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (139)) (Prims.of_int (60)) - (Prims.of_int (256)) (Prims.of_int (50))))) + (Prims.of_int (140)) (Prims.of_int (60)) + (Prims.of_int (258)) (Prims.of_int (50))))) (Obj.magic (Pulse_Checker_Prover_ElimPure.elim_pure g0 pre0 ())) (fun uu___ -> @@ -474,17 +457,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (150)) + (Prims.of_int (151)) (Prims.of_int (44)) - (Prims.of_int (252)) + (Prims.of_int (254)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (253)) + (Prims.of_int (255)) (Prims.of_int (4)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (50))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -492,17 +475,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (151)) + (Prims.of_int (152)) (Prims.of_int (12)) - (Prims.of_int (151)) + (Prims.of_int (152)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (152)) + (Prims.of_int (153)) (Prims.of_int (4)) - (Prims.of_int (252)) + (Prims.of_int (254)) (Prims.of_int (48))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -542,10 +525,7 @@ let rec (check : Pulse_Checker_Base.check_t) = g1 pre () post_hint res_ppname t)) | Pulse_Syntax_Base.Tm_IntroExists - { - Pulse_Syntax_Base.erased = - uu___1; - Pulse_Syntax_Base.p2 = p; + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses;_} -> @@ -556,79 +536,109 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (165)) - (Prims.of_int (13)) - (Prims.of_int (165)) - (Prims.of_int (46))))) + (Prims.of_int (166)) + (Prims.of_int (14)) + (Prims.of_int (166)) + (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (165)) + (Prims.of_int (167)) (Prims.of_int (6)) - (Prims.of_int (175)) + (Prims.of_int (177)) (Prims.of_int (57))))) - (Obj.magic - (instantiate_unknown_witnesses - g1 t)) - (fun uu___2 -> - (fun uu___2 -> - match uu___2 - with - | FStar_Pervasives_Native.Some - t1 -> - Obj.magic - (check g1 + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> + t.Pulse_Syntax_Base.range2)) + (fun uu___1 -> + (fun r -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.fst" + (Prims.of_int (167)) + (Prims.of_int (13)) + (Prims.of_int (167)) + (Prims.of_int (46))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.fst" + (Prims.of_int (167)) + (Prims.of_int (6)) + (Prims.of_int (177)) + (Prims.of_int (57))))) + (Obj.magic + (instantiate_unknown_witnesses + g1 t)) + (fun uu___1 + -> + (fun + uu___1 -> + match uu___1 + with + | + FStar_Pervasives_Native.Some + t1 -> + Obj.magic + (check g1 pre () post_hint res_ppname t1) - | FStar_Pervasives_Native.None - -> - (match witnesses - with - | [] -> + | + FStar_Pervasives_Native.None + -> + (match witnesses + with + | + [] -> Obj.magic (Pulse_Typing_Env.fail g1 (FStar_Pervasives_Native.Some (t.Pulse_Syntax_Base.range2)) "intro exists with empty witnesses") - | uu___3::[] + | + uu___2::[] -> Obj.magic (Pulse_Checker_Exists.check_intro_exists g1 pre () post_hint res_ppname - (maybe_intro_exists_erased - t) + t FStar_Pervasives_Native.None) - | uu___3 -> + | + uu___2 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (174)) + (Prims.of_int (176)) (Prims.of_int (19)) - (Prims.of_int (174)) - (Prims.of_int (64))))) + (Prims.of_int (176)) + (Prims.of_int (66))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (175)) + (Prims.of_int (177)) (Prims.of_int (11)) - (Prims.of_int (175)) + (Prims.of_int (177)) (Prims.of_int (56))))) (Obj.magic (transform_to_unary_intro_exists g1 p - witnesses)) + witnesses + r)) (fun - uu___4 -> + uu___3 -> (fun t1 -> Obj.magic @@ -637,8 +647,9 @@ let rec (check : Pulse_Checker_Base.check_t) = post_hint res_ppname t1)) - uu___4)))) - uu___2))) + uu___3)))) + uu___1))) + uu___1))) | Pulse_Syntax_Base.Tm_Bind uu___1 -> Obj.magic @@ -667,17 +678,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (184)) + (Prims.of_int (186)) (Prims.of_int (8)) - (Prims.of_int (200)) + (Prims.of_int (202)) (Prims.of_int (97))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (201)) + (Prims.of_int (203)) (Prims.of_int (8)) - (Prims.of_int (204)) + (Prims.of_int (206)) (Prims.of_int (29))))) (match (post_if, post_hint) @@ -715,18 +726,18 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (190)) + (Prims.of_int (192)) (Prims.of_int (12)) - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (37))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (189)) + (Prims.of_int (191)) (Prims.of_int (10)) - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (37))))) ( Obj.magic @@ -735,17 +746,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (16)) - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (190)) + (Prims.of_int (192)) (Prims.of_int (12)) - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (37))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -760,17 +771,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (190)) + (Prims.of_int (192)) (Prims.of_int (12)) - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (37))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (190)) + (Prims.of_int (192)) (Prims.of_int (12)) - (Prims.of_int (195)) + (Prims.of_int (197)) (Prims.of_int (37))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -778,9 +789,9 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (194)) + (Prims.of_int (196)) (Prims.of_int (16)) - (Prims.of_int (194)) + (Prims.of_int (196)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic @@ -844,17 +855,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (203)) + (Prims.of_int (205)) (Prims.of_int (8)) - (Prims.of_int (203)) + (Prims.of_int (205)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (201)) + (Prims.of_int (203)) (Prims.of_int (8)) - (Prims.of_int (204)) + (Prims.of_int (206)) (Prims.of_int (29))))) (Obj.magic (Pulse_Checker_If.check @@ -901,17 +912,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (212)) + (Prims.of_int (214)) (Prims.of_int (8)) - (Prims.of_int (228)) + (Prims.of_int (230)) (Prims.of_int (97))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (229)) + (Prims.of_int (231)) (Prims.of_int (8)) - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (30))))) (match (post_match, post_hint) @@ -949,18 +960,18 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (12)) - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (37))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (217)) + (Prims.of_int (219)) (Prims.of_int (10)) - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (37))))) ( Obj.magic @@ -969,17 +980,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (16)) - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (12)) - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (37))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -994,17 +1005,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (12)) - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (37))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (12)) - (Prims.of_int (223)) + (Prims.of_int (225)) (Prims.of_int (37))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1012,9 +1023,9 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (222)) + (Prims.of_int (224)) (Prims.of_int (16)) - (Prims.of_int (222)) + (Prims.of_int (224)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic @@ -1078,17 +1089,17 @@ let rec (check : Pulse_Checker_Base.check_t) = (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (231)) + (Prims.of_int (233)) (Prims.of_int (8)) - (Prims.of_int (231)) + (Prims.of_int (233)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.fst" - (Prims.of_int (229)) + (Prims.of_int (231)) (Prims.of_int (8)) - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (30))))) (Obj.magic (Pulse_Checker_Match.check diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml b/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml index 163f54254..024682814 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml @@ -598,8 +598,8 @@ let (intro_exists_witness_singleton : fun st -> match st.Pulse_Syntax_Base.term1 with | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = uu___; Pulse_Syntax_Base.p2 = uu___1; - Pulse_Syntax_Base.witnesses = uu___2::[];_} + { Pulse_Syntax_Base.p2 = uu___; + Pulse_Syntax_Base.witnesses = uu___1::[];_} -> true | uu___ -> false let (intro_exists_vprop : @@ -607,396 +607,9 @@ let (intro_exists_vprop : fun st -> match st.Pulse_Syntax_Base.term1 with | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = uu___; Pulse_Syntax_Base.p2 = p; - Pulse_Syntax_Base.witnesses = uu___1;_} - -> p -let (is_intro_exists_erased : Pulse_Syntax_Base.st_term -> Prims.bool) = - fun st -> - match st.Pulse_Syntax_Base.term1 with - | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = erased; Pulse_Syntax_Base.p2 = uu___; - Pulse_Syntax_Base.witnesses = uu___1;_} - -> erased - | uu___ -> false -let (check_intro_exists_erased : - Pulse_Typing_Env.env -> - Pulse_Syntax_Base.term -> - unit -> - unit Pulse_Typing.post_hint_opt -> - Pulse_Syntax_Base.ppname -> - Pulse_Syntax_Base.st_term -> - unit FStar_Pervasives_Native.option -> - ((unit, unit, unit) Pulse_Checker_Base.checker_result_t, - unit) FStar_Tactics_Effect.tac_repr) - = - fun g -> - fun pre -> - fun pre_typing -> - fun post_hint -> - fun res_ppname -> - fun st -> - fun vprop_typing -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (91)) (Prims.of_int (10)) - (Prims.of_int (91)) (Prims.of_int (78))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (91)) (Prims.of_int (81)) - (Prims.of_int (112)) (Prims.of_int (85))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___ -> - Pulse_Typing_Env.push_context g - "check_intro_exists_erased" - st.Pulse_Syntax_Base.range2)) - (fun uu___ -> - (fun g1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (93)) (Prims.of_int (46)) - (Prims.of_int (93)) (Prims.of_int (53))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (91)) (Prims.of_int (81)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___ -> st.Pulse_Syntax_Base.term1)) - (fun uu___ -> - (fun uu___ -> - match uu___ with - | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = uu___1; - Pulse_Syntax_Base.p2 = t; - Pulse_Syntax_Base.witnesses = e::[];_} - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (95)) - (Prims.of_int (4)) - (Prims.of_int (97)) - (Prims.of_int (26))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (93)) - (Prims.of_int (56)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (match vprop_typing with - | FStar_Pervasives_Native.Some - typing -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Prims.Mkdtuple2 - (t, ())))) - | uu___2 -> - Obj.magic - (Obj.repr - (Pulse_Checker_Pure.check_vprop - g1 t))) - (fun uu___2 -> - (fun uu___2 -> - match uu___2 with - | Prims.Mkdtuple2 - (t1, t_typing) -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (100)) - (Prims.of_int (2)) - (Prims.of_int (103)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (103)) - (Prims.of_int (34)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (if - Prims.op_Negation - (Pulse_Syntax_Base.uu___is_Tm_ExistsSL - t1.Pulse_Syntax_Base.t) - then - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (102)) - (Prims.of_int (9)) - (Prims.of_int (103)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (101)) - (Prims.of_int (7)) - (Prims.of_int (103)) - (Prims.of_int (33))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (103)) - (Prims.of_int (12)) - (Prims.of_int (103)) - (Prims.of_int (32))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (Pulse_Syntax_Printer.term_to_string - t1)) - (fun - uu___3 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> - Prims.strcat - "check_intro_exists_erased: vprop " - (Prims.strcat - uu___3 - " is not an existential"))))) - (fun - uu___3 -> - (fun - uu___3 -> - Obj.magic - (Pulse_Typing_Env.fail - g1 - (FStar_Pervasives_Native.Some - (st.Pulse_Syntax_Base.range2)) - uu___3)) - uu___3))) - else - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> - ())))) - (fun uu___3 -> - (fun uu___3 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (105)) - (Prims.of_int (26)) - (Prims.of_int (105)) - (Prims.of_int (39))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (103)) - (Prims.of_int (34)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> - t1.Pulse_Syntax_Base.t)) - (fun - uu___4 -> - (fun - uu___4 -> - match uu___4 - with - | - Pulse_Syntax_Base.Tm_ExistsSL - (u, b, p) - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (108)) - (Prims.of_int (21)) - (Prims.of_int (108)) - (Prims.of_int (92))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (107)) - (Prims.of_int (47)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___5 -> - Pulse_Typing_Metatheory_Base.tm_exists_inversion - g1 u - b.Pulse_Syntax_Base.binder_ty - p () - (Pulse_Typing_Env.fresh - g1))) - (fun - uu___5 -> - (fun - uu___5 -> - match uu___5 - with - | - (ty_typing, - uu___6) - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (110)) - (Prims.of_int (4)) - (Prims.of_int (110)) - (Prims.of_int (63))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (108)) - (Prims.of_int (95)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (Obj.magic - (Pulse_Checker_Pure.check_term_with_expected_type - g1 e - (Pulse_Typing.mk_erased - u - b.Pulse_Syntax_Base.binder_ty))) - (fun - uu___7 -> - (fun - uu___7 -> - match uu___7 - with - | - Prims.Mkdtuple2 - (e1, - e_typing) - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (111)) - (Prims.of_int (10)) - (Prims.of_int (111)) - (Prims.of_int (71))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (112)) - (Prims.of_int (2)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___8 -> - Pulse_Typing.T_IntroExistsErased - (g1, u, - b, p, e1, - (), (), - ()))) - (fun - uu___8 -> - (fun d -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (112)) - (Prims.of_int (18)) - (Prims.of_int (112)) - (Prims.of_int (57))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Exists.fst" - (Prims.of_int (112)) - (Prims.of_int (2)) - (Prims.of_int (112)) - (Prims.of_int (85))))) - (Obj.magic - (Pulse_Checker_Prover.try_frame_pre - g pre () - (Pulse_Typing.wr - (Pulse_Syntax_Base.Tm_IntroExists - { - Pulse_Syntax_Base.erased - = true; - Pulse_Syntax_Base.p2 - = - (Pulse_Syntax_Base.tm_exists_sl - u b p); - Pulse_Syntax_Base.witnesses - = [e1] - })) - (Pulse_Typing.comp_intro_exists_erased - u b p e1) - d - res_ppname)) - (fun - uu___8 -> - (fun - uu___8 -> - Obj.magic - (Pulse_Checker_Prover.prove_post_hint - g pre - uu___8 - post_hint - t1.Pulse_Syntax_Base.range1)) - uu___8))) - uu___8))) - uu___7))) - uu___5))) - uu___4))) - uu___3))) - uu___2))) uu___))) uu___) -let (check_intro_exists_non_erased : + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = uu___;_} -> + p +let (check_intro_exists : Pulse_Typing_Env.env -> Pulse_Syntax_Base.term -> unit -> @@ -1018,13 +631,13 @@ let (check_intro_exists_non_erased : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (125)) (Prims.of_int (10)) - (Prims.of_int (125)) (Prims.of_int (82))))) + (Prims.of_int (119)) (Prims.of_int (10)) + (Prims.of_int (119)) (Prims.of_int (82))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (125)) (Prims.of_int (85)) - (Prims.of_int (147)) (Prims.of_int (85))))) + (Prims.of_int (119)) (Prims.of_int (85)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context g @@ -1038,17 +651,17 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (127)) + (Prims.of_int (121)) (Prims.of_int (52)) - (Prims.of_int (127)) + (Prims.of_int (121)) (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (125)) + (Prims.of_int (119)) (Prims.of_int (85)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> st.Pulse_Syntax_Base.term1)) @@ -1056,8 +669,7 @@ let (check_intro_exists_non_erased : (fun uu___ -> match uu___ with | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = uu___1; - Pulse_Syntax_Base.p2 = t; + { Pulse_Syntax_Base.p2 = t; Pulse_Syntax_Base.witnesses = witness::[];_} -> @@ -1067,17 +679,17 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (129)) + (Prims.of_int (123)) (Prims.of_int (4)) - (Prims.of_int (131)) + (Prims.of_int (125)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (127)) + (Prims.of_int (121)) (Prims.of_int (62)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (match vprop_typing with | FStar_Pervasives_Native.Some @@ -1085,17 +697,17 @@ let (check_intro_exists_non_erased : Obj.magic (Obj.repr (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> + (fun uu___1 -> Prims.Mkdtuple2 (t, ())))) - | uu___2 -> + | uu___1 -> Obj.magic (Obj.repr (Pulse_Checker_Pure.check_vprop g1 t))) - (fun uu___2 -> - (fun uu___2 -> - match uu___2 with + (fun uu___1 -> + (fun uu___1 -> + match uu___1 with | Prims.Mkdtuple2 (t1, t_typing) -> Obj.magic @@ -1104,17 +716,17 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (134)) + (Prims.of_int (128)) (Prims.of_int (2)) - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (34)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (if Prims.op_Negation @@ -1128,17 +740,17 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (136)) + (Prims.of_int (130)) (Prims.of_int (9)) - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (135)) + (Prims.of_int (129)) (Prims.of_int (7)) - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (33))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1146,9 +758,9 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (12)) - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic @@ -1162,62 +774,62 @@ let (check_intro_exists_non_erased : (Pulse_Syntax_Printer.term_to_string t1)) (fun - uu___3 -> + uu___2 -> FStar_Tactics_Effect.lift_div_tac (fun - uu___4 -> + uu___3 -> Prims.strcat "check_intro_exists_non_erased: vprop " (Prims.strcat - uu___3 + uu___2 " is not an existential"))))) (fun - uu___3 -> + uu___2 -> (fun - uu___3 -> + uu___2 -> Obj.magic (Pulse_Typing_Env.fail g1 (FStar_Pervasives_Native.Some (st.Pulse_Syntax_Base.range2)) - uu___3)) - uu___3))) + uu___2)) + uu___2))) else Obj.magic (Obj.repr (FStar_Tactics_Effect.lift_div_tac (fun - uu___4 -> + uu___3 -> ())))) - (fun uu___3 -> - (fun uu___3 -> + (fun uu___2 -> + (fun uu___2 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (139)) + (Prims.of_int (133)) (Prims.of_int (26)) - (Prims.of_int (139)) + (Prims.of_int (133)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (137)) + (Prims.of_int (131)) (Prims.of_int (34)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___4 -> + uu___3 -> t1.Pulse_Syntax_Base.t)) (fun - uu___4 -> + uu___3 -> (fun - uu___4 -> - match uu___4 + uu___3 -> + match uu___3 with | Pulse_Syntax_Base.Tm_ExistsSL @@ -1229,21 +841,21 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (142)) + (Prims.of_int (136)) (Prims.of_int (21)) - (Prims.of_int (142)) + (Prims.of_int (136)) (Prims.of_int (92))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (141)) + (Prims.of_int (135)) (Prims.of_int (47)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___5 -> + uu___4 -> Pulse_Typing_Metatheory_Base.tm_exists_inversion g1 u b.Pulse_Syntax_Base.binder_ty @@ -1251,14 +863,14 @@ let (check_intro_exists_non_erased : (Pulse_Typing_Env.fresh g1))) (fun - uu___5 -> + uu___4 -> (fun - uu___5 -> - match uu___5 + uu___4 -> + match uu___4 with | (ty_typing, - uu___6) + uu___5) -> Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1266,28 +878,28 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (144)) + (Prims.of_int (138)) (Prims.of_int (4)) - (Prims.of_int (144)) - (Prims.of_int (55))))) + (Prims.of_int (138)) + (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (142)) + (Prims.of_int (136)) (Prims.of_int (95)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (Obj.magic - (Pulse_Checker_Pure.check_term_with_expected_type + (Pulse_Checker_Pure.check_ghost_term_with_expected_type g1 witness b.Pulse_Syntax_Base.binder_ty)) (fun - uu___7 -> + uu___6 -> (fun - uu___7 -> - match uu___7 + uu___6 -> + match uu___6 with | Prims.Mkdtuple2 @@ -1300,21 +912,21 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (145)) + (Prims.of_int (139)) (Prims.of_int (10)) - (Prims.of_int (145)) - (Prims.of_int (77))))) + (Prims.of_int (139)) + (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (145)) - (Prims.of_int (80)) - (Prims.of_int (147)) + (Prims.of_int (139)) + (Prims.of_int (76)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___8 -> + uu___7 -> Pulse_Typing.T_IntroExists (g1, u, b, p, @@ -1322,7 +934,7 @@ let (check_intro_exists_non_erased : (), (), ()))) (fun - uu___8 -> + uu___7 -> (fun d -> Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1330,31 +942,31 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (146)) + (Prims.of_int (140)) (Prims.of_int (45)) - (Prims.of_int (146)) + (Prims.of_int (140)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (145)) - (Prims.of_int (80)) - (Prims.of_int (147)) + (Prims.of_int (139)) + (Prims.of_int (76)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___8 -> + uu___7 -> Prims.Mkdtuple2 ((Pulse_Typing.comp_intro_exists u b p witness1), d))) (fun - uu___8 -> + uu___7 -> (fun - uu___8 -> - match uu___8 + uu___7 -> + match uu___7 with | Prims.Mkdtuple2 @@ -1366,43 +978,43 @@ let (check_intro_exists_non_erased : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (2)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (2)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___9 -> - uu___8)) + uu___8 -> + uu___7)) (fun - uu___9 -> + uu___8 -> (fun - uu___9 -> + uu___8 -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (18)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Exists.fst" - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (2)) - (Prims.of_int (147)) + (Prims.of_int (141)) (Prims.of_int (85))))) (Obj.magic (Pulse_Checker_Prover.try_frame_pre @@ -1410,8 +1022,6 @@ let (check_intro_exists_non_erased : (Pulse_Typing.wr (Pulse_Syntax_Base.Tm_IntroExists { - Pulse_Syntax_Base.erased - = false; Pulse_Syntax_Base.p2 = (Pulse_Syntax_Base.tm_exists_sl @@ -1422,48 +1032,21 @@ let (check_intro_exists_non_erased : })) c d1 res_ppname)) (fun - uu___10 - -> + uu___9 -> (fun - uu___10 - -> + uu___9 -> Obj.magic (Pulse_Checker_Prover.prove_post_hint g pre - uu___10 + uu___9 post_hint t1.Pulse_Syntax_Base.range1)) - uu___10))) uu___9))) uu___8))) - uu___8))) uu___7))) - uu___5))) + uu___7))) + uu___6))) uu___4))) - uu___3))) - uu___2))) uu___))) uu___) -let (check_intro_exists : - Pulse_Typing_Env.env -> - Pulse_Syntax_Base.term -> - unit -> - unit Pulse_Typing.post_hint_opt -> - Pulse_Syntax_Base.ppname -> - Pulse_Syntax_Base.st_term -> - unit FStar_Pervasives_Native.option -> - ((unit, unit, unit) Pulse_Checker_Base.checker_result_t, - unit) FStar_Tactics_Effect.tac_repr) - = - fun g -> - fun pre -> - fun pre_typing -> - fun post_hint -> - fun res_ppname -> - fun st -> - fun vprop_typing -> - if is_intro_exists_erased st - then - check_intro_exists_erased g pre () post_hint res_ppname st - vprop_typing - else - check_intro_exists_non_erased g pre () post_hint res_ppname - st vprop_typing \ No newline at end of file + uu___3))) + uu___2))) + uu___1))) uu___))) uu___) \ No newline at end of file diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroExists.ml b/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroExists.ml index 67892515c..d743636e7 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroExists.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroExists.ml @@ -30,19 +30,18 @@ let (k_intro_exists : (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" (Prims.of_int (27)) (Prims.of_int (10)) - (Prims.of_int (29)) (Prims.of_int (49))))) + (Prims.of_int (28)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (29)) (Prims.of_int (52)) - (Prims.of_int (68)) (Prims.of_int (30))))) + (Prims.of_int (28)) (Prims.of_int (52)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing.wr (Pulse_Syntax_Base.Tm_IntroExists { - Pulse_Syntax_Base.erased = false; Pulse_Syntax_Base.p2 = (Pulse_Syntax_Base.tm_exists_sl u b p); Pulse_Syntax_Base.witnesses = [e] @@ -55,17 +54,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (31)) + (Prims.of_int (30)) (Prims.of_int (10)) - (Prims.of_int (31)) + (Prims.of_int (30)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (31)) + (Prims.of_int (30)) (Prims.of_int (38)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -78,17 +77,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (33)) + (Prims.of_int (32)) (Prims.of_int (17)) - (Prims.of_int (33)) + (Prims.of_int (32)) (Prims.of_int (70))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (36)) + (Prims.of_int (35)) (Prims.of_int (45)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -103,17 +102,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (38)) + (Prims.of_int (37)) (Prims.of_int (10)) - (Prims.of_int (38)) + (Prims.of_int (37)) (Prims.of_int (17))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (39)) + (Prims.of_int (38)) (Prims.of_int (52)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -127,17 +126,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (41)) + (Prims.of_int (40)) (Prims.of_int (15)) - (Prims.of_int (41)) + (Prims.of_int (40)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (41)) + (Prims.of_int (40)) (Prims.of_int (47)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -154,17 +153,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (46)) + (Prims.of_int (45)) (Prims.of_int (4)) - (Prims.of_int (46)) + (Prims.of_int (45)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (54)) + (Prims.of_int (53)) (Prims.of_int (20)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (Obj.magic (Pulse_Checker_Base.continuation_elaborator_with_bind @@ -174,8 +173,6 @@ let (k_intro_exists : (Pulse_Typing.wr (Pulse_Syntax_Base.Tm_IntroExists { - Pulse_Syntax_Base.erased - = false; Pulse_Syntax_Base.p2 = (Pulse_Syntax_Base.tm_exists_sl @@ -200,17 +197,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (55)) + (Prims.of_int (54)) (Prims.of_int (25)) - (Prims.of_int (55)) + (Prims.of_int (54)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (54)) + (Prims.of_int (53)) (Prims.of_int (20)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -232,17 +229,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (56)) + (Prims.of_int (55)) (Prims.of_int (31)) - (Prims.of_int (56)) + (Prims.of_int (55)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (56)) + (Prims.of_int (55)) (Prims.of_int (36)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -258,17 +255,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (57)) + (Prims.of_int (56)) (Prims.of_int (18)) - (Prims.of_int (57)) + (Prims.of_int (56)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (60)) + (Prims.of_int (59)) (Prims.of_int (64)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -287,17 +284,17 @@ let (k_intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (62)) + (Prims.of_int (61)) (Prims.of_int (4)) - (Prims.of_int (66)) + (Prims.of_int (65)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (2)) - (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (30))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -384,14 +381,14 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (79)) (Prims.of_int (10)) - (Prims.of_int (79)) (Prims.of_int (41))))) + (Prims.of_int (78)) (Prims.of_int (10)) + (Prims.of_int (78)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (79)) (Prims.of_int (44)) - (Prims.of_int (324)) (Prims.of_int (6))))) + (Prims.of_int (78)) (Prims.of_int (44)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Typing_Env.fresh @@ -406,17 +403,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (80)) + (Prims.of_int (79)) (Prims.of_int (11)) - (Prims.of_int (80)) + (Prims.of_int (79)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (80)) + (Prims.of_int (79)) (Prims.of_int (32)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -429,17 +426,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (82)) + (Prims.of_int (81)) (Prims.of_int (4)) - (Prims.of_int (86)) + (Prims.of_int (85)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (87)) + (Prims.of_int (86)) (Prims.of_int (6)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -476,17 +473,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (91)) + (Prims.of_int (90)) (Prims.of_int (105)) - (Prims.of_int (100)) + (Prims.of_int (99)) (Prims.of_int (18))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (102)) + (Prims.of_int (101)) (Prims.of_int (37)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -526,17 +523,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (104)) + (Prims.of_int (103)) (Prims.of_int (4)) - (Prims.of_int (113)) + (Prims.of_int (112)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (114)) + (Prims.of_int (113)) (Prims.of_int (6)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -589,17 +586,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (115)) + (Prims.of_int (114)) (Prims.of_int (16)) - (Prims.of_int (115)) + (Prims.of_int (114)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (115)) + (Prims.of_int (114)) (Prims.of_int (33)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (Obj.magic (prover @@ -616,17 +613,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (119)) + (Prims.of_int (118)) (Prims.of_int (56)) - (Prims.of_int (119)) + (Prims.of_int (118)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (119)) + (Prims.of_int (118)) (Prims.of_int (76)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -643,17 +640,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (121)) + (Prims.of_int (120)) (Prims.of_int (66)) - (Prims.of_int (129)) + (Prims.of_int (128)) (Prims.of_int (18))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (130)) + (Prims.of_int (129)) (Prims.of_int (61)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -661,17 +658,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (122)) + (Prims.of_int (121)) (Prims.of_int (12)) - (Prims.of_int (122)) + (Prims.of_int (121)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (123)) + (Prims.of_int (122)) (Prims.of_int (4)) - (Prims.of_int (129)) + (Prims.of_int (128)) (Prims.of_int (18))))) (Obj.magic (Pulse_Checker_Prover_Substs.ss_to_nt_substs @@ -715,17 +712,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (135)) + (Prims.of_int (134)) (Prims.of_int (4)) - (Prims.of_int (135)) + (Prims.of_int (134)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (137)) + (Prims.of_int (136)) (Prims.of_int (48)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -742,17 +739,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (141)) + (Prims.of_int (140)) (Prims.of_int (59)) - (Prims.of_int (141)) + (Prims.of_int (140)) (Prims.of_int (89))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (141)) + (Prims.of_int (140)) (Prims.of_int (92)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -769,17 +766,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (145)) + (Prims.of_int (144)) (Prims.of_int (48)) - (Prims.of_int (145)) + (Prims.of_int (144)) (Prims.of_int (96))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (145)) + (Prims.of_int (144)) (Prims.of_int (99)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -796,17 +793,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (150)) + (Prims.of_int (149)) (Prims.of_int (4)) - (Prims.of_int (150)) + (Prims.of_int (149)) (Prims.of_int (13))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (150)) + (Prims.of_int (149)) (Prims.of_int (16)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -822,17 +819,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (157)) + (Prims.of_int (156)) (Prims.of_int (4)) - (Prims.of_int (157)) + (Prims.of_int (156)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (157)) + (Prims.of_int (156)) (Prims.of_int (50)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -874,17 +871,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (164)) + (Prims.of_int (163)) (Prims.of_int (4)) - (Prims.of_int (164)) + (Prims.of_int (163)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (166)) + (Prims.of_int (165)) (Prims.of_int (84)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -901,17 +898,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (167)) + (Prims.of_int (166)) (Prims.of_int (16)) - (Prims.of_int (167)) + (Prims.of_int (166)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (168)) + (Prims.of_int (167)) (Prims.of_int (94)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -931,17 +928,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (175)) + (Prims.of_int (174)) (Prims.of_int (4)) - (Prims.of_int (175)) + (Prims.of_int (174)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (175)) + (Prims.of_int (174)) (Prims.of_int (25)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -958,17 +955,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (184)) + (Prims.of_int (183)) (Prims.of_int (4)) - (Prims.of_int (184)) + (Prims.of_int (183)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (184)) + (Prims.of_int (183)) (Prims.of_int (50)) - (Prims.of_int (324)) + (Prims.of_int (323)) (Prims.of_int (6))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1030,17 +1027,17 @@ let (intro_exists : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (194)) + (Prims.of_int (193)) (Prims.of_int (4)) - (Prims.of_int (203)) + (Prims.of_int (202)) (Prims.of_int (16))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.IntroExists.fst" - (Prims.of_int (312)) + (Prims.of_int (311)) (Prims.of_int (4)) - (Prims.of_int (321)) + (Prims.of_int (320)) (Prims.of_int (26))))) (Obj.magic (k_intro_exists diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml b/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml index 9a2d21d04..bd7fb1b6e 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml @@ -513,116 +513,118 @@ let (rtb_core_check_term_at_type : FStar_Reflection_Types.env -> FStar_Reflection_Types.term -> FStar_Reflection_Types.term -> - (((unit, unit, unit) FStar_Tactics_Types.typing_token - FStar_Pervasives_Native.option * FStar_Tactics_Types.issues), - unit) FStar_Tactics_Effect.tac_repr) + FStar_Tactics_Types.tot_or_ghost -> + (((unit, unit, unit) FStar_Tactics_Types.typing_token + FStar_Pervasives_Native.option * FStar_Tactics_Types.issues), + unit) FStar_Tactics_Effect.tac_repr) = fun g -> fun f -> fun e -> fun t -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (53)) (Prims.of_int (2)) - (Prims.of_int (55)) (Prims.of_int (60))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (55)) (Prims.of_int (61)) - (Prims.of_int (57)) (Prims.of_int (5))))) - (Obj.magic - (debug g - (fun uu___ -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (55)) (Prims.of_int (39)) - (Prims.of_int (55)) (Prims.of_int (59))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (53)) (Prims.of_int (20)) - (Prims.of_int (55)) (Prims.of_int (59))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string t)) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (53)) - (Prims.of_int (20)) - (Prims.of_int (55)) - (Prims.of_int (59))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (53)) - (Prims.of_int (20)) - (Prims.of_int (55)) - (Prims.of_int (59))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (54)) - (Prims.of_int (39)) - (Prims.of_int (54)) - (Prims.of_int (59))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Printf.fst" - (Prims.of_int (121)) - (Prims.of_int (8)) - (Prims.of_int (123)) - (Prims.of_int (44))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - e)) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> - fun x -> - Prims.strcat - (Prims.strcat - "Calling core_check_term on " - (Prims.strcat uu___2 - " and ")) - (Prims.strcat x ""))))) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> uu___2 uu___1)))) - uu___1)))) - (fun uu___ -> - (fun uu___ -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (56)) (Prims.of_int (12)) - (Prims.of_int (56)) (Prims.of_int (47))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (56)) (Prims.of_int (6)) - (Prims.of_int (56)) (Prims.of_int (9))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.core_check_term f e t - FStar_Tactics_Types.E_Total)) - (fun res -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___1 -> res)))) uu___) + fun eff -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (53)) (Prims.of_int (2)) + (Prims.of_int (55)) (Prims.of_int (60))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (55)) (Prims.of_int (61)) + (Prims.of_int (57)) (Prims.of_int (5))))) + (Obj.magic + (debug g + (fun uu___ -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (55)) (Prims.of_int (39)) + (Prims.of_int (55)) (Prims.of_int (59))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (53)) (Prims.of_int (20)) + (Prims.of_int (55)) (Prims.of_int (59))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.term_to_string t)) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (53)) + (Prims.of_int (20)) + (Prims.of_int (55)) + (Prims.of_int (59))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (53)) + (Prims.of_int (20)) + (Prims.of_int (55)) + (Prims.of_int (59))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (54)) + (Prims.of_int (39)) + (Prims.of_int (54)) + (Prims.of_int (59))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Printf.fst" + (Prims.of_int (121)) + (Prims.of_int (8)) + (Prims.of_int (123)) + (Prims.of_int (44))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.term_to_string + e)) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> + fun x -> + Prims.strcat + (Prims.strcat + "Calling core_check_term on " + (Prims.strcat uu___2 + " and ")) + (Prims.strcat x ""))))) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> uu___2 uu___1)))) + uu___1)))) + (fun uu___ -> + (fun uu___ -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (56)) (Prims.of_int (12)) + (Prims.of_int (56)) (Prims.of_int (41))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (56)) (Prims.of_int (6)) + (Prims.of_int (56)) (Prims.of_int (9))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.core_check_term f e t + eff)) + (fun res -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> res)))) uu___) let (mk_squash : FStar_Reflection_Types.term -> FStar_Reflection_Types.term) = fun t -> @@ -2053,148 +2055,153 @@ let (check_term_and_type : tok)))))) uu___1))) uu___))) uu___))) uu___) -let (check_term_with_expected_type : +let (check_term_with_expected_type_aux : Pulse_Typing_Env.env -> Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term -> - ((Pulse_Syntax_Base.term, (unit, unit, unit) Pulse_Typing.typing) - Prims.dtuple2, - unit) FStar_Tactics_Effect.tac_repr) + FStar_Tactics_Types.tot_or_ghost -> + ((Pulse_Syntax_Base.term, + (unit, unit, unit) FStar_Reflection_Typing.typing) Prims.dtuple2, + unit) FStar_Tactics_Effect.tac_repr) = fun g -> fun e -> fun t -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (199)) (Prims.of_int (13)) - (Prims.of_int (199)) (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (197)) (Prims.of_int (35)) - (Prims.of_int (214)) (Prims.of_int (74))))) - (Obj.magic (instantiate_term_implicits g e)) - (fun uu___ -> - (fun uu___ -> - match uu___ with - | (e1, uu___1) -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (201)) (Prims.of_int (11)) - (Prims.of_int (201)) (Prims.of_int (21))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (201)) (Prims.of_int (24)) - (Prims.of_int (214)) (Prims.of_int (74))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> Pulse_Typing.elab_env g)) - (fun uu___2 -> - (fun fg -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (202)) - (Prims.of_int (11)) - (Prims.of_int (202)) - (Prims.of_int (22))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (202)) - (Prims.of_int (25)) - (Prims.of_int (214)) - (Prims.of_int (74))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Pulse_Elaborate_Pure.elab_term e1)) - (fun uu___2 -> - (fun re -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (203)) - (Prims.of_int (11)) - (Prims.of_int (203)) - (Prims.of_int (22))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (203)) - (Prims.of_int (25)) - (Prims.of_int (214)) - (Prims.of_int (74))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Pulse_Elaborate_Pure.elab_term - t)) - (fun uu___2 -> - (fun rt -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (206)) - (Prims.of_int (4)) - (Prims.of_int (209)) - (Prims.of_int (16))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Pure.fst" - (Prims.of_int (203)) - (Prims.of_int (25)) - (Prims.of_int (214)) - (Prims.of_int (74))))) - (Obj.magic - (catch_all - (fun uu___2 - -> - rtb_core_check_term_at_type + fun eff -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (198)) (Prims.of_int (13)) + (Prims.of_int (198)) (Prims.of_int (43))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (196)) (Prims.of_int (78)) + (Prims.of_int (213)) (Prims.of_int (74))))) + (Obj.magic (instantiate_term_implicits g e)) + (fun uu___ -> + (fun uu___ -> + match uu___ with + | (e1, uu___1) -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (200)) (Prims.of_int (11)) + (Prims.of_int (200)) (Prims.of_int (21))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (200)) (Prims.of_int (24)) + (Prims.of_int (213)) (Prims.of_int (74))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> Pulse_Typing.elab_env g)) + (fun uu___2 -> + (fun fg -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (201)) + (Prims.of_int (11)) + (Prims.of_int (201)) + (Prims.of_int (22))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (201)) + (Prims.of_int (25)) + (Prims.of_int (213)) + (Prims.of_int (74))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Pulse_Elaborate_Pure.elab_term e1)) + (fun uu___2 -> + (fun re -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (202)) + (Prims.of_int (11)) + (Prims.of_int (202)) + (Prims.of_int (22))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (202)) + (Prims.of_int (25)) + (Prims.of_int (213)) + (Prims.of_int (74))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Pulse_Elaborate_Pure.elab_term + t)) + (fun uu___2 -> + (fun rt -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (205)) + (Prims.of_int (4)) + (Prims.of_int (208)) + (Prims.of_int (20))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Pure.fst" + (Prims.of_int (202)) + (Prims.of_int (25)) + (Prims.of_int (213)) + (Prims.of_int (74))))) + (Obj.magic + (catch_all + (fun uu___2 + -> + rtb_core_check_term_at_type (Pulse_Typing_Env.push_context g "check_term_with_expected_type" (FStar_Reflection_V2_Builtins.range_of_term rt)) fg - re rt))) - (fun uu___2 -> - (fun uu___2 -> - match uu___2 - with - | (topt, - issues) -> + re rt eff))) + (fun uu___2 -> + (fun uu___2 -> + match uu___2 + with + | (topt, + issues) + -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (210)) + (Prims.of_int (209)) (Prims.of_int (2)) - (Prims.of_int (210)) + (Prims.of_int (209)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (211)) + (Prims.of_int (210)) (Prims.of_int (2)) - (Prims.of_int (214)) + (Prims.of_int (213)) (Prims.of_int (74))))) (Obj.magic (FStar_Tactics_V2_Builtins.log_issues @@ -2215,17 +2222,17 @@ let (check_term_with_expected_type : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (213)) + (Prims.of_int (212)) (Prims.of_int (26)) - (Prims.of_int (213)) + (Prims.of_int (212)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (213)) + (Prims.of_int (212)) (Prims.of_int (4)) - (Prims.of_int (213)) + (Prims.of_int (212)) (Prims.of_int (58))))) (Obj.magic (ill_typed_term @@ -2256,12 +2263,53 @@ let (check_term_with_expected_type : (e1, (FStar_Reflection_Typing.T_Token (fg, re, - (FStar_Tactics_Types.E_Total, - rt), ()))))))) + (eff, rt), + ()))))))) uu___3))) - uu___2))) - uu___2))) uu___2))) - uu___2))) uu___) + uu___2))) + uu___2))) uu___2))) + uu___2))) uu___) +let (check_term_with_expected_type : + Pulse_Typing_Env.env -> + Pulse_Syntax_Base.term -> + Pulse_Syntax_Base.term -> + ((Pulse_Syntax_Base.term, (unit, unit, unit) Pulse_Typing.typing) + Prims.dtuple2, + unit) FStar_Tactics_Effect.tac_repr) + = + fun g -> + fun e -> + fun t -> + check_term_with_expected_type_aux g e t FStar_Tactics_Types.E_Total +let (check_ghost_term_with_expected_type : + Pulse_Typing_Env.env -> + Pulse_Syntax_Base.term -> + Pulse_Syntax_Base.typ -> + ((Pulse_Syntax_Base.term, unit) Prims.dtuple2, unit) + FStar_Tactics_Effect.tac_repr) + = + fun g -> + fun e -> + fun t -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (219)) (Prims.of_int (19)) + (Prims.of_int (219)) (Prims.of_int (68))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Checker.Pure.fst" + (Prims.of_int (218)) (Prims.of_int (47)) + (Prims.of_int (220)) (Prims.of_int (14))))) + (Obj.magic + (check_term_with_expected_type_aux g e t + FStar_Tactics_Types.E_Ghost)) + (fun uu___ -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> + match uu___ with + | Prims.Mkdtuple2 (e1, d) -> Prims.Mkdtuple2 (e1, ()))) let (tc_with_core : Pulse_Typing_Env.env -> FStar_Reflection_Types.env -> @@ -2279,13 +2327,13 @@ let (tc_with_core : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (218)) (Prims.of_int (23)) - (Prims.of_int (218)) (Prims.of_int (117))))) + (Prims.of_int (224)) (Prims.of_int (23)) + (Prims.of_int (224)) (Prims.of_int (117))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (218)) (Prims.of_int (3)) - (Prims.of_int (222)) (Prims.of_int (71))))) + (Prims.of_int (224)) (Prims.of_int (3)) + (Prims.of_int (228)) (Prims.of_int (71))))) (Obj.magic (catch_all (fun uu___ -> @@ -2321,13 +2369,13 @@ let (core_check_term : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (227)) (Prims.of_int (13)) - (Prims.of_int (227)) (Prims.of_int (23))))) + (Prims.of_int (233)) (Prims.of_int (13)) + (Prims.of_int (233)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (227)) (Prims.of_int (26)) - (Prims.of_int (239)) (Prims.of_int (23))))) + (Prims.of_int (233)) (Prims.of_int (26)) + (Prims.of_int (245)) (Prims.of_int (23))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing.elab_env g)) (fun uu___ -> @@ -2337,13 +2385,13 @@ let (core_check_term : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (228)) (Prims.of_int (13)) - (Prims.of_int (228)) (Prims.of_int (24))))) + (Prims.of_int (234)) (Prims.of_int (13)) + (Prims.of_int (234)) (Prims.of_int (24))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (228)) (Prims.of_int (27)) - (Prims.of_int (239)) (Prims.of_int (23))))) + (Prims.of_int (234)) (Prims.of_int (27)) + (Prims.of_int (245)) (Prims.of_int (23))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Elaborate_Pure.elab_term t)) (fun uu___ -> @@ -2354,17 +2402,17 @@ let (core_check_term : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (229)) + (Prims.of_int (235)) (Prims.of_int (22)) - (Prims.of_int (229)) + (Prims.of_int (235)) (Prims.of_int (94))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (228)) + (Prims.of_int (234)) (Prims.of_int (27)) - (Prims.of_int (239)) + (Prims.of_int (245)) (Prims.of_int (23))))) (Obj.magic (tc_with_core @@ -2382,17 +2430,17 @@ let (core_check_term : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (230)) + (Prims.of_int (236)) (Prims.of_int (4)) - (Prims.of_int (230)) + (Prims.of_int (236)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (231)) + (Prims.of_int (237)) (Prims.of_int (4)) - (Prims.of_int (239)) + (Prims.of_int (245)) (Prims.of_int (23))))) (Obj.magic (FStar_Tactics_V2_Builtins.log_issues @@ -2409,17 +2457,17 @@ let (core_check_term : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (233)) + (Prims.of_int (239)) (Prims.of_int (28)) - (Prims.of_int (233)) + (Prims.of_int (239)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (233)) + (Prims.of_int (239)) (Prims.of_int (6)) - (Prims.of_int (233)) + (Prims.of_int (239)) (Prims.of_int (56))))) (Obj.magic (ill_typed_term @@ -2452,17 +2500,17 @@ let (core_check_term : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (237)) + (Prims.of_int (243)) (Prims.of_int (32)) - (Prims.of_int (237)) + (Prims.of_int (243)) (Prims.of_int (54))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (237)) + (Prims.of_int (243)) (Prims.of_int (10)) - (Prims.of_int (237)) + (Prims.of_int (243)) (Prims.of_int (54))))) (Obj.magic (readback_failure @@ -2502,13 +2550,13 @@ let (core_check_term_with_expected_type : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (242)) (Prims.of_int (11)) - (Prims.of_int (242)) (Prims.of_int (21))))) + (Prims.of_int (248)) (Prims.of_int (11)) + (Prims.of_int (248)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (242)) (Prims.of_int (24)) - (Prims.of_int (254)) (Prims.of_int (65))))) + (Prims.of_int (248)) (Prims.of_int (24)) + (Prims.of_int (260)) (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing.elab_env g)) (fun uu___ -> @@ -2518,13 +2566,13 @@ let (core_check_term_with_expected_type : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (243)) (Prims.of_int (11)) - (Prims.of_int (243)) (Prims.of_int (22))))) + (Prims.of_int (249)) (Prims.of_int (11)) + (Prims.of_int (249)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (243)) (Prims.of_int (25)) - (Prims.of_int (254)) (Prims.of_int (65))))) + (Prims.of_int (249)) (Prims.of_int (25)) + (Prims.of_int (260)) (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Elaborate_Pure.elab_term e)) (fun uu___ -> @@ -2535,17 +2583,17 @@ let (core_check_term_with_expected_type : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (244)) + (Prims.of_int (250)) (Prims.of_int (11)) - (Prims.of_int (244)) + (Prims.of_int (250)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (244)) + (Prims.of_int (250)) (Prims.of_int (25)) - (Prims.of_int (254)) + (Prims.of_int (260)) (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -2558,17 +2606,17 @@ let (core_check_term_with_expected_type : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (246)) + (Prims.of_int (252)) (Prims.of_int (4)) - (Prims.of_int (249)) - (Prims.of_int (16))))) + (Prims.of_int (255)) + (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (244)) + (Prims.of_int (250)) (Prims.of_int (25)) - (Prims.of_int (254)) + (Prims.of_int (260)) (Prims.of_int (65))))) (Obj.magic (catch_all @@ -2578,7 +2626,8 @@ let (core_check_term_with_expected_type : g "core_check_term_with_expected_type" (FStar_Reflection_V2_Builtins.range_of_term - rt)) fg re rt))) + rt)) fg re rt + FStar_Tactics_Types.E_Total))) (fun uu___ -> (fun uu___ -> match uu___ with @@ -2589,17 +2638,17 @@ let (core_check_term_with_expected_type : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (250)) + (Prims.of_int (256)) (Prims.of_int (2)) - (Prims.of_int (250)) + (Prims.of_int (256)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (251)) + (Prims.of_int (257)) (Prims.of_int (2)) - (Prims.of_int (254)) + (Prims.of_int (260)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_V2_Builtins.log_issues @@ -2617,17 +2666,17 @@ let (core_check_term_with_expected_type : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (253)) + (Prims.of_int (259)) (Prims.of_int (26)) - (Prims.of_int (253)) + (Prims.of_int (259)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (253)) + (Prims.of_int (259)) (Prims.of_int (4)) - (Prims.of_int (253)) + (Prims.of_int (259)) (Prims.of_int (58))))) (Obj.magic (ill_typed_term @@ -2676,13 +2725,13 @@ let (check_vprop : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (260)) (Prims.of_int (4)) (Prims.of_int (260)) + (Prims.of_int (266)) (Prims.of_int (4)) (Prims.of_int (266)) (Prims.of_int (84))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (258)) (Prims.of_int (46)) - (Prims.of_int (261)) (Prims.of_int (21))))) + (Prims.of_int (264)) (Prims.of_int (46)) + (Prims.of_int (267)) (Prims.of_int (21))))) (Obj.magic (check_term_with_expected_type (Pulse_Typing_Env.push_context_no_range g "check_vprop") t @@ -2702,12 +2751,12 @@ let (check_vprop_with_core : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (268)) (Prims.of_int (17)) - (Prims.of_int (268)) (Prims.of_int (112))))) + (Prims.of_int (274)) (Prims.of_int (17)) + (Prims.of_int (274)) (Prims.of_int (112))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (269)) (Prims.of_int (2)) (Prims.of_int (269)) + (Prims.of_int (275)) (Prims.of_int (2)) (Prims.of_int (275)) (Prims.of_int (12))))) (Obj.magic (core_check_term_with_expected_type @@ -2728,13 +2777,13 @@ let (get_non_informative_witness : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (274)) (Prims.of_int (6)) - (Prims.of_int (276)) (Prims.of_int (52))))) + (Prims.of_int (280)) (Prims.of_int (6)) + (Prims.of_int (282)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (276)) (Prims.of_int (55)) - (Prims.of_int (303)) (Prims.of_int (16))))) + (Prims.of_int (282)) (Prims.of_int (55)) + (Prims.of_int (309)) (Prims.of_int (16))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> fun uu___1 -> @@ -2742,21 +2791,21 @@ let (get_non_informative_witness : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (275)) (Prims.of_int (13)) - (Prims.of_int (276)) (Prims.of_int (52))))) + (Prims.of_int (281)) (Prims.of_int (13)) + (Prims.of_int (282)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (274)) (Prims.of_int (6)) - (Prims.of_int (276)) (Prims.of_int (52))))) + (Prims.of_int (280)) (Prims.of_int (6)) + (Prims.of_int (282)) (Prims.of_int (52))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (276)) (Prims.of_int (31)) - (Prims.of_int (276)) (Prims.of_int (51))))) + (Prims.of_int (282)) (Prims.of_int (31)) + (Prims.of_int (282)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "prims.fst" @@ -2783,13 +2832,13 @@ let (get_non_informative_witness : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (277)) (Prims.of_int (14)) - (Prims.of_int (296)) (Prims.of_int (17))))) + (Prims.of_int (283)) (Prims.of_int (14)) + (Prims.of_int (302)) (Prims.of_int (17))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (298)) (Prims.of_int (4)) - (Prims.of_int (303)) (Prims.of_int (16))))) + (Prims.of_int (304)) (Prims.of_int (4)) + (Prims.of_int (309)) (Prims.of_int (16))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> match Pulse_Syntax_Pure.is_fvar_app t with @@ -2857,17 +2906,17 @@ let (get_non_informative_witness : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (302)) + (Prims.of_int (308)) (Prims.of_int (8)) - (Prims.of_int (302)) + (Prims.of_int (308)) (Prims.of_int (126))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (300)) + (Prims.of_int (306)) (Prims.of_int (15)) - (Prims.of_int (303)) + (Prims.of_int (309)) (Prims.of_int (16))))) (Obj.magic (check_term_with_expected_type @@ -2897,13 +2946,13 @@ let (check_prop_validity : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (307)) (Prims.of_int (24)) - (Prims.of_int (307)) (Prims.of_int (76))))) + (Prims.of_int (313)) (Prims.of_int (24)) + (Prims.of_int (313)) (Prims.of_int (76))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (307)) (Prims.of_int (3)) - (Prims.of_int (314)) (Prims.of_int (20))))) + (Prims.of_int (313)) (Prims.of_int (3)) + (Prims.of_int (320)) (Prims.of_int (20))))) (Obj.magic (rtb_check_prop_validity g (Pulse_Typing.elab_env g) (Pulse_Elaborate_Pure.elab_term p))) @@ -2916,13 +2965,13 @@ let (check_prop_validity : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (308)) (Prims.of_int (4)) - (Prims.of_int (308)) (Prims.of_int (23))))) + (Prims.of_int (314)) (Prims.of_int (4)) + (Prims.of_int (314)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (309)) (Prims.of_int (4)) - (Prims.of_int (314)) (Prims.of_int (20))))) + (Prims.of_int (315)) (Prims.of_int (4)) + (Prims.of_int (320)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Builtins.log_issues issues)) (fun uu___2 -> @@ -2936,17 +2985,17 @@ let (check_prop_validity : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (312)) + (Prims.of_int (318)) (Prims.of_int (13)) - (Prims.of_int (313)) + (Prims.of_int (319)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (311)) + (Prims.of_int (317)) (Prims.of_int (6)) - (Prims.of_int (313)) + (Prims.of_int (319)) (Prims.of_int (62))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2954,9 +3003,9 @@ let (check_prop_validity : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Pure.fst" - (Prims.of_int (313)) + (Prims.of_int (319)) (Prims.of_int (22)) - (Prims.of_int (313)) + (Prims.of_int (319)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic diff --git a/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml b/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml index 29172d313..d7cf79f62 100644 --- a/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml +++ b/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml @@ -396,16 +396,6 @@ let rec (elab_st_typing : Pulse_Reflection_Util.mk_intro_exists ru rt (Pulse_Reflection_Util.mk_abs rt FStar_Reflection_V2_Data.Q_Explicit rp) re - | Pulse_Typing.T_IntroExistsErased - (uu___, u, b, p, e, uu___1, uu___2, uu___3) -> - let ru = u in - let rt = - Pulse_Elaborate_Pure.elab_term b.Pulse_Syntax_Base.binder_ty in - let rp = Pulse_Elaborate_Pure.elab_term p in - let re = Pulse_Elaborate_Pure.elab_term e in - Pulse_Reflection_Util.mk_intro_exists_erased ru rt - (Pulse_Reflection_Util.mk_abs rt - FStar_Reflection_V2_Data.Q_Explicit rp) re | Pulse_Typing.T_While (uu___, inv, uu___1, uu___2, uu___3, cond_typing, body_typing) -> diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml index ba293735d..12ef42955 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml @@ -268,7 +268,6 @@ and st_term'__Tm_ElimExists__payload = { p1: vprop } and st_term'__Tm_IntroExists__payload = { - erased: Prims.bool ; p2: vprop ; witnesses: term Prims.list } and st_term'__Tm_While__payload = @@ -506,9 +505,8 @@ let rec (eq_st_term : st_term -> st_term -> Prims.bool) = { head2 = t21; body2 = k2;_}) -> (eq_tm t11 t21) && (eq_st_term k1 k2) | (Tm_IntroPure { p = p1;_}, Tm_IntroPure { p = p2;_}) -> eq_tm p1 p2 - | (Tm_IntroExists { erased = b1; p2 = p1; witnesses = l1;_}, - Tm_IntroExists { erased = b2; p2; witnesses = l2;_}) -> - ((b1 = b2) && (eq_tm p1 p2)) && (eq_tm_list l1 l2) + | (Tm_IntroExists { p2 = p1; witnesses = l1;_}, Tm_IntroExists + { p2; witnesses = l2;_}) -> (eq_tm p1 p2) && (eq_tm_list l1 l2) | (Tm_ElimExists { p1;_}, Tm_ElimExists { p1 = p2;_}) -> eq_tm p1 p2 | (Tm_If { b1 = g1; then_ = ethen1; else_ = eelse1; post1 = p1;_}, Tm_If { b1 = g2; then_ = ethen2; else_ = eelse2; post1 = p2;_}) -> diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Builder.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Builder.ml index 9fc528410..b5427bcff 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Builder.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Builder.ml @@ -114,19 +114,13 @@ let (tm_match : let (tm_elim_exists : Pulse_Syntax_Base.vprop -> Pulse_Syntax_Base.st_term') = fun p -> Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = p } let (tm_intro_exists : - Prims.bool -> - Pulse_Syntax_Base.vprop -> - Pulse_Syntax_Base.term Prims.list -> Pulse_Syntax_Base.st_term') + Pulse_Syntax_Base.vprop -> + Pulse_Syntax_Base.term Prims.list -> Pulse_Syntax_Base.st_term') = - fun erased -> - fun p -> - fun witnesses -> - Pulse_Syntax_Base.Tm_IntroExists - { - Pulse_Syntax_Base.erased = erased; - Pulse_Syntax_Base.p2 = p; - Pulse_Syntax_Base.witnesses = witnesses - } + fun p -> + fun witnesses -> + Pulse_Syntax_Base.Tm_IntroExists + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses } let (tm_while : Pulse_Syntax_Base.term -> Pulse_Syntax_Base.st_term -> diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Naming.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Naming.ml index 58c124092..b87ad99b4 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Naming.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Naming.ml @@ -104,7 +104,7 @@ let rec (freevars_st : | Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = p;_} -> freevars p | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = uu___; Pulse_Syntax_Base.p2 = p; + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses;_} -> FStar_Set.union (freevars p) (freevars_list witnesses) | Pulse_Syntax_Base.Tm_While @@ -248,7 +248,7 @@ let rec (ln_st' : Pulse_Syntax_Base.st_term -> Prims.int -> Prims.bool) = | Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = p;_} -> ln' p i | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = uu___; Pulse_Syntax_Base.p2 = p; + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses;_} -> (ln' p i) && (ln_list' witnesses i) | Pulse_Syntax_Base.Tm_While @@ -600,12 +600,11 @@ let rec (subst_st_term : Pulse_Syntax_Base.Tm_ElimExists { Pulse_Syntax_Base.p1 = (subst_term p ss) } | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = erased; Pulse_Syntax_Base.p2 = p; + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses;_} -> Pulse_Syntax_Base.Tm_IntroExists { - Pulse_Syntax_Base.erased = erased; Pulse_Syntax_Base.p2 = (subst_term p ss); Pulse_Syntax_Base.witnesses = (subst_term_list witnesses ss) } diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml index 9d0d220be..5c03f65be 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml @@ -1938,7 +1938,7 @@ let rec (st_term_to_string' : (fun uu___1 -> Prims.strcat "elim_exists " (Prims.strcat uu___ ""))) | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = false; Pulse_Syntax_Base.p2 = p; + { Pulse_Syntax_Base.p2 = p; Pulse_Syntax_Base.witnesses = witnesses;_} -> FStar_Tactics_Effect.tac_bind @@ -2026,95 +2026,6 @@ let rec (st_term_to_string' : (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> uu___1 uu___)))) uu___) - | Pulse_Syntax_Base.Tm_IntroExists - { Pulse_Syntax_Base.erased = true; Pulse_Syntax_Base.p2 = p; - Pulse_Syntax_Base.witnesses = witnesses;_} - -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Syntax.Printer.fst" - (Prims.of_int (212)) (Prims.of_int (8)) - (Prims.of_int (212)) (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Syntax.Printer.fst" - (Prims.of_int (208)) (Prims.of_int (6)) - (Prims.of_int (212)) (Prims.of_int (43))))) - (Obj.magic (term_list_to_string " " witnesses)) - (fun uu___ -> - (fun uu___ -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Syntax.Printer.fst" - (Prims.of_int (208)) (Prims.of_int (6)) - (Prims.of_int (212)) (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "Pulse.Syntax.Printer.fst" - (Prims.of_int (208)) (Prims.of_int (6)) - (Prims.of_int (212)) (Prims.of_int (43))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Syntax.Printer.fst" - (Prims.of_int (208)) (Prims.of_int (6)) - (Prims.of_int (212)) - (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Syntax.Printer.fst" - (Prims.of_int (208)) (Prims.of_int (6)) - (Prims.of_int (212)) - (Prims.of_int (43))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Syntax.Printer.fst" - (Prims.of_int (210)) - (Prims.of_int (8)) - (Prims.of_int (210)) - (Prims.of_int (42))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Printf.fst" - (Prims.of_int (121)) - (Prims.of_int (8)) - (Prims.of_int (123)) - (Prims.of_int (44))))) - (Obj.magic - (term_to_string' (indent level) p)) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - fun x -> - fun x1 -> - Prims.strcat - (Prims.strcat - (Prims.strcat - (Prims.strcat - "introduce (erased)\n" - (Prims.strcat - (indent level) - "")) - (Prims.strcat uu___1 - "\n")) - (Prims.strcat x "with ")) - (Prims.strcat x1 ""))))) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> uu___1 level)))) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> uu___1 uu___)))) uu___) | Pulse_Syntax_Base.Tm_While { Pulse_Syntax_Base.invariant = invariant; Pulse_Syntax_Base.condition = condition; diff --git a/src/ocaml/plugin/generated/Pulse_Typing.ml b/src/ocaml/plugin/generated/Pulse_Typing.ml index af88b5d4b..e9a1b4f51 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing.ml @@ -714,6 +714,7 @@ let (comp_admit : type ('g, 'e, 't) typing = (unit, unit, unit) FStar_Reflection_Typing.tot_typing type ('g, 'e, 't) tot_typing = unit +type ('g, 'e, 't) ghost_typing = unit type ('g, 't, 'u) universe_of = unit type ('g, 'u, 't) non_informative_t = (Pulse_Syntax_Base.term, unit) Prims.dtuple2 @@ -869,9 +870,6 @@ type ('dummyV0, 'dummyV1, 'dummyV2) st_typing = | T_IntroExists of Pulse_Typing_Env.env * Pulse_Syntax_Base.universe * Pulse_Syntax_Base.binder * Pulse_Syntax_Base.term * Pulse_Syntax_Base.term * unit * unit * unit - | T_IntroExistsErased of Pulse_Typing_Env.env * Pulse_Syntax_Base.universe - * Pulse_Syntax_Base.binder * Pulse_Syntax_Base.term * - Pulse_Syntax_Base.term * unit * unit * unit | T_While of Pulse_Typing_Env.env * Pulse_Syntax_Base.term * Pulse_Syntax_Base.st_term * Pulse_Syntax_Base.st_term * unit * (unit, unit, unit) st_typing * (unit, unit, unit) st_typing @@ -932,8 +930,6 @@ let uu___is_T_ElimExists uu___2 uu___1 uu___ uu___3 = match uu___3 with | T_ElimExists _ -> true | _ -> false let uu___is_T_IntroExists uu___2 uu___1 uu___ uu___3 = match uu___3 with | T_IntroExists _ -> true | _ -> false -let uu___is_T_IntroExistsErased uu___2 uu___1 uu___ uu___3 = - match uu___3 with | T_IntroExistsErased _ -> true | _ -> false let uu___is_T_While uu___2 uu___1 uu___ uu___3 = match uu___3 with | T_While _ -> true | _ -> false let uu___is_T_Par uu___2 uu___1 uu___ uu___3 = diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml b/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml index 1f7c22734..11a0872be 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Metatheory_Base.ml @@ -416,12 +416,6 @@ let rec (st_typing_weakening : ((Pulse_Typing_Env.push_env (Pulse_Typing_Env.push_env g g1) g'), u, b, p, e, (), (), ()) - | Pulse_Typing.T_IntroExistsErased - (uu___, u, b, p, e, uu___1, uu___2, uu___3) -> - Pulse_Typing.T_IntroExistsErased - ((Pulse_Typing_Env.push_env - (Pulse_Typing_Env.push_env g g1) g'), u, b, p, e, (), - (), ()) | Pulse_Typing.T_While (uu___, inv, cond, body, uu___1, cond_typing, body_typing) -> @@ -912,15 +906,6 @@ let rec (st_typing_subst : (Pulse_Syntax_Naming.subst_term p ss), (Pulse_Syntax_Naming.subst_term e2 ss), (), (), ()) - | Pulse_Typing.T_IntroExistsErased - (uu___, u, b, p, e2, uu___1, uu___2, uu___3) -> - Pulse_Typing.T_IntroExistsErased - ((Pulse_Typing_Env.push_env g - (Pulse_Typing_Env.subst_env g' (nt x e))), u, - (Pulse_Syntax_Naming.subst_binder b ss), - (Pulse_Syntax_Naming.subst_term p ss), - (Pulse_Syntax_Naming.subst_term e2 ss), (), (), - ()) | Pulse_Typing.T_While (uu___, inv, cond, body, uu___1, cond_typing, body_typing) diff --git a/src/syntax_extension/PulseDesugar.fst b/src/syntax_extension/PulseDesugar.fst index 150e3a88e..dc65871bb 100755 --- a/src/syntax_extension/PulseDesugar.fst +++ b/src/syntax_extension/PulseDesugar.fst @@ -402,7 +402,7 @@ let rec desugar_stmt (env:env_t) (s:Sugar.stmt) | VPropExists _ -> let? vp = desugar_vprop env vprop in let? witnesses = map_err (desugar_term env) witnesses in - return (SW.tm_intro_exists false vp witnesses s.range) + return (SW.tm_intro_exists vp witnesses s.range) ) diff --git a/src/syntax_extension/PulseSyntaxWrapper.fsti b/src/syntax_extension/PulseSyntaxWrapper.fsti index 5862b4d36..db6561bd1 100755 --- a/src/syntax_extension/PulseSyntaxWrapper.fsti +++ b/src/syntax_extension/PulseSyntaxWrapper.fsti @@ -65,7 +65,7 @@ val tm_let_mut (x:binder) (v:term) (k:st_term) (_:range) : st_term val tm_while (head:st_term) (invariant: (ident & vprop)) (body:st_term) (_:range) : st_term val tm_if (head:term) (returns_annot:option vprop) (then_ else_:st_term) (_:range) : st_term val tm_match (head:term) (returns_:option vprop) (brs:list branch) (_:range) : st_term -val tm_intro_exists (erased:bool) (vp:vprop) (witnesses:list term) (_:range) : st_term +val tm_intro_exists (vp:vprop) (witnesses:list term) (_:range) : st_term val is_tm_intro_exists (x:st_term) : bool val tm_protect (s:st_term) : st_term val tm_par (p1:term) (p2:term) (q1:term) (q2:term) (b1:st_term) (b2:st_term) (_:range) : st_term