From 5f172853779daa9ef58fae6acfb0c05427ce6611 Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Tue, 25 Jul 2023 17:29:48 +0000 Subject: [PATCH] snap --- src/ocaml/plugin/generated/Pulse_Checker.ml | 7 +- .../Pulse_Checker_AssertWithBinders.ml | 7 +- .../plugin/generated/Pulse_Checker_Base.ml | 82 ++- .../plugin/generated/Pulse_Checker_Bind.ml | 172 ++--- .../plugin/generated/Pulse_Checker_Prover.ml | 639 +++++++++--------- 5 files changed, 486 insertions(+), 421 deletions(-) diff --git a/src/ocaml/plugin/generated/Pulse_Checker.ml b/src/ocaml/plugin/generated/Pulse_Checker.ml index d1f52cf98..07cd39201 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker.ml @@ -1130,9 +1130,10 @@ let rec (check : Pulse_Checker_Base.check_t) = (fun uu___1 -> match r with | FStar_Pervasives.Mkdtuple5 - (x, t1, pre', g1, k) -> + (x, g1, t1, pre', k) -> FStar_Pervasives.Mkdtuple5 - (x, t1, pre', g1, + (x, g1, t1, pre', (Pulse_Checker_Base.k_elab_trans - g0 g g1 pre0 pre pre' + g0 g g1 pre0 pre + (FStar_Pervasives.dfst pre') k_elim_pure k)))))) uu___) \ No newline at end of file diff --git a/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml index be7bd2622..d125a6c37 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml @@ -1953,13 +1953,14 @@ let (check : pre'', g2, (Pulse_Checker_Base.k_elab_trans - g g11 g2 - pre + g g11 + x_ty pre (Pulse_Checker_Prover_Base.op_Star (Pulse_Checker_Prover_Substs.nt_subst_term v2 nts) pre') - pre'' + (FStar_Pervasives.dfst + g2) k_frame k)))))) uu___4))) uu___3))) diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Base.ml b/src/ocaml/plugin/generated/Pulse_Checker_Base.ml index 1a9911f3e..3ffb92e71 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Base.ml @@ -1211,9 +1211,13 @@ let rec (check_equiv_emp : | (uu___, uu___1) -> FStar_Pervasives_Native.None) | uu___ -> FStar_Pervasives_Native.None type ('g, 'postuhint, 'x, 't, 'ctxtu) checker_res_matches_post_hint = Obj.t +type ('g, 'postuhint, 'x, 'g1, 't, 'ctxtu) checker_result_inv = Obj.t type ('g, 'ctxt, 'postuhint) checker_result_t = - (Pulse_Syntax_Base.var, Pulse_Syntax_Base.term, Pulse_Syntax_Base.vprop, - Pulse_Typing_Env.env, (unit, unit, unit, unit) continuation_elaborator) + (Pulse_Syntax_Base.var, Pulse_Typing_Env.env, + (Pulse_Syntax_Base.universe, Pulse_Syntax_Base.typ, unit) + FStar_Pervasives.dtuple3, + (Pulse_Syntax_Base.vprop, unit) Prims.dtuple2, + (unit, unit, unit, unit) continuation_elaborator) FStar_Pervasives.dtuple5 type check_t = Pulse_Typing_Env.env -> @@ -1601,8 +1605,8 @@ let (apply_checker_result_k : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (386)) (Prims.of_int (35)) - (Prims.of_int (386)) (Prims.of_int (36))))) + (Prims.of_int (386)) (Prims.of_int (64)) + (Prims.of_int (386)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" @@ -1612,7 +1616,11 @@ let (apply_checker_result_k : (fun uu___ -> (fun uu___ -> match uu___ with - | FStar_Pervasives.Mkdtuple5 (y, ty_y, pre', g1, k) -> + | FStar_Pervasives.Mkdtuple5 + (y, g1, FStar_Pervasives.Mkdtuple3 + (u_ty, ty_y, d_ty_y), Prims.Mkdtuple2 (pre', uu___1), + k) + -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -1625,14 +1633,14 @@ let (apply_checker_result_k : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (386)) (Prims.of_int (39)) + (Prims.of_int (386)) (Prims.of_int (68)) (Prims.of_int (393)) (Prims.of_int (22))))) (Obj.magic (Pulse_Checker_Pure.check_universe g1 ty_y)) - (fun uu___1 -> - (fun uu___1 -> - match uu___1 with - | Prims.Mkdtuple2 (u_ty_y, d_ty_y) -> + (fun uu___2 -> + (fun uu___2 -> + match uu___2 with + | Prims.Mkdtuple2 (u_ty_y, d_ty_y1) -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -1652,18 +1660,18 @@ let (apply_checker_result_k : (Prims.of_int (393)) (Prims.of_int (22))))) (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> + (fun uu___3 -> return_in_ctxt g1 y u_ty_y ty_y pre' () (FStar_Pervasives_Native.Some post_hint))) - (fun uu___2 -> + (fun uu___3 -> (fun d -> Obj.magic (k (FStar_Pervasives_Native.Some - post_hint) d)) uu___2))) - uu___1))) uu___) + post_hint) d)) uu___3))) + uu___2))) uu___) let (checker_result_for_st_typing : Pulse_Typing_Env.env -> Pulse_Syntax_Base.vprop -> @@ -1686,7 +1694,7 @@ let (checker_result_for_st_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" (Prims.of_int (398)) (Prims.of_int (47)) - (Prims.of_int (422)) (Prims.of_int (35))))) + (Prims.of_int (429)) (Prims.of_int (72))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> d)) (fun uu___ -> (fun uu___ -> @@ -1705,7 +1713,7 @@ let (checker_result_for_st_typing : (FStar_Range.mk_range "Pulse.Checker.Base.fst" (Prims.of_int (402)) (Prims.of_int (20)) - (Prims.of_int (422)) (Prims.of_int (35))))) + (Prims.of_int (429)) (Prims.of_int (72))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Typing_Env.fresh g)) (fun uu___1 -> @@ -1726,8 +1734,8 @@ let (checker_result_for_st_typing : "Pulse.Checker.Base.fst" (Prims.of_int (404)) (Prims.of_int (58)) - (Prims.of_int (422)) - (Prims.of_int (35))))) + (Prims.of_int (429)) + (Prims.of_int (72))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Typing_Env.push_binding g x @@ -1751,8 +1759,8 @@ let (checker_result_for_st_typing : "Pulse.Checker.Base.fst" (Prims.of_int (405)) (Prims.of_int (63)) - (Prims.of_int (422)) - (Prims.of_int (35))))) + (Prims.of_int (429)) + (Prims.of_int (72))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Syntax_Naming.open_term_nv @@ -1776,10 +1784,10 @@ let (checker_result_for_st_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (422)) - (Prims.of_int (2)) - (Prims.of_int (422)) - (Prims.of_int (35))))) + (Prims.of_int (420)) + (Prims.of_int (30)) + (Prims.of_int (429)) + (Prims.of_int (72))))) (Obj.magic (continuation_elaborator_with_bind g @@ -1789,12 +1797,30 @@ let (checker_result_for_st_typing : FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> + match + Pulse_Typing_Metatheory.st_comp_typing_inversion_cofinite + g + (Pulse_Syntax_Base.st_comp_of_comp + c) + (Pulse_Typing_Metatheory.comp_typing_inversion + g c + (Pulse_Typing_Metatheory.st_typing_correctness + g t c d1)) + with + | + (comp_res_typing, + uu___2, + f) -> FStar_Pervasives.Mkdtuple5 - (x, - (Pulse_Syntax_Base.comp_res + (x, g', + (FStar_Pervasives.Mkdtuple3 + ((Pulse_Syntax_Base.comp_u c), - ctxt', - g', + (Pulse_Syntax_Base.comp_res + c), ())), + (Prims.Mkdtuple2 + (ctxt', + ())), (k_elab_equiv g g' (Pulse_Syntax_Base.tm_star diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml b/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml index 76b173dcb..cdf8f808b 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml @@ -27,7 +27,7 @@ let (check_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" (Prims.of_int (29)) (Prims.of_int (2)) - (Prims.of_int (45)) (Prims.of_int (32))))) + (Prims.of_int (44)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context g "check_bind" @@ -47,7 +47,7 @@ let (check_bind : (FStar_Range.mk_range "Pulse.Checker.Bind.fst" (Prims.of_int (32)) (Prims.of_int (2)) - (Prims.of_int (45)) (Prims.of_int (32))))) + (Prims.of_int (44)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover g1 (fun uu___ -> @@ -93,7 +93,7 @@ let (check_bind : "Pulse.Checker.Bind.fst" (Prims.of_int (33)) (Prims.of_int (90)) - (Prims.of_int (45)) + (Prims.of_int (44)) (Prims.of_int (32))))) (if FStar_Pervasives_Native.uu___is_None @@ -128,7 +128,7 @@ let (check_bind : "Pulse.Checker.Bind.fst" (Prims.of_int (33)) (Prims.of_int (90)) - (Prims.of_int (45)) + (Prims.of_int (44)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -161,7 +161,7 @@ let (check_bind : "Pulse.Checker.Bind.fst" (Prims.of_int (35)) (Prims.of_int (53)) - (Prims.of_int (45)) + (Prims.of_int (44)) (Prims.of_int (32))))) (Obj.magic (check g1 @@ -176,27 +176,29 @@ let (check_bind : with | FStar_Pervasives.Mkdtuple5 - (x, ty, - ctxt', - g11, k1) - -> + (x, g11, + uu___4, + Prims.Mkdtuple2 + (ctxt', + ctxt'_typing), + k1) -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (41)) + (Prims.of_int (40)) (Prims.of_int (4)) - (Prims.of_int (41)) - (Prims.of_int (86))))) + (Prims.of_int (40)) + (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (41)) - (Prims.of_int (89)) - (Prims.of_int (45)) + (Prims.of_int (40)) + (Prims.of_int (91)) + (Prims.of_int (44)) (Prims.of_int (32))))) (Obj.magic (check @@ -208,7 +210,7 @@ let (check_bind : ((binder.Pulse_Syntax_Base.binder_ppname), x)))) (fun - uu___4 -> + uu___5 -> (fun r -> Obj.magic (FStar_Tactics_Effect.tac_bind @@ -216,17 +218,17 @@ let (check_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (42)) + (Prims.of_int (41)) (Prims.of_int (49)) - (Prims.of_int (42)) + (Prims.of_int (41)) (Prims.of_int (100))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (42)) + (Prims.of_int (41)) (Prims.of_int (103)) - (Prims.of_int (45)) + (Prims.of_int (44)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Base.apply_checker_result_k @@ -235,7 +237,7 @@ let (check_bind : post_hint) r)) (fun - uu___4 -> + uu___5 -> (fun d -> Obj.magic (FStar_Tactics_Effect.tac_bind @@ -243,24 +245,24 @@ let (check_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (43)) + (Prims.of_int (42)) (Prims.of_int (47)) - (Prims.of_int (43)) + (Prims.of_int (42)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (45)) + (Prims.of_int (44)) (Prims.of_int (2)) - (Prims.of_int (45)) + (Prims.of_int (44)) (Prims.of_int (32))))) (Obj.magic (k1 post_hint d)) (fun - uu___4 -> + uu___5 -> (fun d1 -> Obj.magic @@ -268,9 +270,9 @@ let (check_bind : g1 ctxt post_hint d1)) - uu___4))) - uu___4))) - uu___4))) + uu___5))) + uu___5))) + uu___5))) uu___3))) uu___2))) uu___1))) uu___))) uu___) @@ -294,13 +296,13 @@ let (check_tot_bind : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (56)) (Prims.of_int (10)) - (Prims.of_int (56)) (Prims.of_int (62))))) + (Prims.of_int (55)) (Prims.of_int (10)) + (Prims.of_int (55)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (58)) (Prims.of_int (2)) - (Prims.of_int (83)) (Prims.of_int (32))))) + (Prims.of_int (57)) (Prims.of_int (2)) + (Prims.of_int (82)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context g "check_bind" @@ -313,14 +315,14 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (58)) (Prims.of_int (2)) - (Prims.of_int (59)) (Prims.of_int (93))))) + (Prims.of_int (57)) (Prims.of_int (2)) + (Prims.of_int (58)) (Prims.of_int (93))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (59)) (Prims.of_int (94)) - (Prims.of_int (83)) (Prims.of_int (32))))) + (Prims.of_int (58)) (Prims.of_int (94)) + (Prims.of_int (82)) (Prims.of_int (32))))) (if FStar_Pervasives_Native.uu___is_None post_hint then Obj.magic @@ -342,17 +344,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (61)) + (Prims.of_int (60)) (Prims.of_int (40)) - (Prims.of_int (61)) + (Prims.of_int (60)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (59)) + (Prims.of_int (58)) (Prims.of_int (94)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -373,17 +375,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (62)) + (Prims.of_int (61)) (Prims.of_int (48)) - (Prims.of_int (62)) + (Prims.of_int (61)) (Prims.of_int (72))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (61)) + (Prims.of_int (60)) (Prims.of_int (49)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Pure.check_term_and_type @@ -403,18 +405,18 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (63)) + (Prims.of_int (62)) (Prims.of_int (10)) - (Prims.of_int (66)) + (Prims.of_int (65)) (Prims.of_int (21))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (66)) + (Prims.of_int (65)) (Prims.of_int (24)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) ( FStar_Tactics_Effect.lift_div_tac @@ -444,17 +446,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (70)) + (Prims.of_int (69)) (Prims.of_int (4)) - (Prims.of_int (70)) + (Prims.of_int (69)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (66)) + (Prims.of_int (65)) (Prims.of_int (24)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Pure.check_term_with_expected_type @@ -477,17 +479,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (72)) + (Prims.of_int (71)) (Prims.of_int (10)) - (Prims.of_int (72)) + (Prims.of_int (71)) (Prims.of_int (17))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (72)) + (Prims.of_int (71)) (Prims.of_int (20)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -503,17 +505,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (74)) + (Prims.of_int (73)) (Prims.of_int (10)) - (Prims.of_int (74)) + (Prims.of_int (73)) (Prims.of_int (74))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (74)) + (Prims.of_int (73)) (Prims.of_int (77)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Base.continuation_elaborator_with_tot_bind @@ -529,17 +531,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (76)) + (Prims.of_int (75)) (Prims.of_int (11)) - (Prims.of_int (76)) + (Prims.of_int (75)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (76)) + (Prims.of_int (75)) (Prims.of_int (23)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -556,17 +558,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (77)) + (Prims.of_int (76)) (Prims.of_int (11)) - (Prims.of_int (77)) + (Prims.of_int (76)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (77)) + (Prims.of_int (76)) (Prims.of_int (42)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -585,17 +587,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (79)) + (Prims.of_int (78)) (Prims.of_int (4)) - (Prims.of_int (79)) + (Prims.of_int (78)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (79)) + (Prims.of_int (78)) (Prims.of_int (54)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -612,17 +614,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (80)) + (Prims.of_int (79)) (Prims.of_int (10)) - (Prims.of_int (80)) + (Prims.of_int (79)) (Prims.of_int (68))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (80)) + (Prims.of_int (79)) (Prims.of_int (71)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (Obj.magic (check g' @@ -639,17 +641,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (81)) + (Prims.of_int (80)) (Prims.of_int (10)) - (Prims.of_int (81)) + (Prims.of_int (80)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (81)) + (Prims.of_int (80)) (Prims.of_int (64)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Base.apply_checker_result_k @@ -666,17 +668,17 @@ let (check_tot_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (82)) + (Prims.of_int (81)) (Prims.of_int (10)) - (Prims.of_int (82)) + (Prims.of_int (81)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Bind.fst" - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (2)) - (Prims.of_int (83)) + (Prims.of_int (82)) (Prims.of_int (32))))) (Obj.magic (k diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml b/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml index ccfb64b83..27cb7971e 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml @@ -171,17 +171,17 @@ let rec (match_q : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (75)) + (Prims.of_int (77)) (Prims.of_int (12)) - (Prims.of_int (75)) + (Prims.of_int (77)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (75)) + (Prims.of_int (77)) (Prims.of_int (38)) - (Prims.of_int (84)) + (Prims.of_int (86)) (Prims.of_int (38))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___3 -> @@ -195,17 +195,17 @@ let rec (match_q : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (77)) + (Prims.of_int (79)) (Prims.of_int (6)) - (Prims.of_int (77)) + (Prims.of_int (79)) (Prims.of_int (69))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (78)) + (Prims.of_int (80)) (Prims.of_int (4)) - (Prims.of_int (84)) + (Prims.of_int (86)) (Prims.of_int (38))))) (Obj.magic (Pulse_Checker_Prover_Match.match_step @@ -236,17 +236,17 @@ let rec (match_q : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (82)) + (Prims.of_int (84)) (Prims.of_int (8)) - (Prims.of_int (83)) + (Prims.of_int (85)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (84)) + (Prims.of_int (86)) (Prims.of_int (6)) - (Prims.of_int (84)) + (Prims.of_int (86)) (Prims.of_int (38))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -299,13 +299,13 @@ let rec (prove_pures : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (93)) (Prims.of_int (18)) - (Prims.of_int (93)) (Prims.of_int (57))))) + (Prims.of_int (95)) (Prims.of_int (18)) + (Prims.of_int (95)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (94)) (Prims.of_int (4)) - (Prims.of_int (102)) (Prims.of_int (12))))) + (Prims.of_int (96)) (Prims.of_int (4)) + (Prims.of_int (104)) (Prims.of_int (12))))) (Obj.magic (Pulse_Checker_Prover_IntroPure.intro_pure preamble pst p unsolved' ())) @@ -319,17 +319,17 @@ let rec (prove_pures : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (96)) + (Prims.of_int (98)) (Prims.of_int (24)) - (Prims.of_int (96)) + (Prims.of_int (98)) (Prims.of_int (100))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (96)) + (Prims.of_int (98)) (Prims.of_int (7)) - (Prims.of_int (96)) + (Prims.of_int (98)) (Prims.of_int (100))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -337,9 +337,9 @@ let rec (prove_pures : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (96)) + (Prims.of_int (98)) (Prims.of_int (79)) - (Prims.of_int (96)) + (Prims.of_int (98)) (Prims.of_int (99))))) (FStar_Sealed.seal (Obj.magic @@ -373,17 +373,17 @@ let rec (prove_pures : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (98)) + (Prims.of_int (100)) (Prims.of_int (18)) - (Prims.of_int (98)) + (Prims.of_int (100)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (98)) + (Prims.of_int (100)) (Prims.of_int (11)) - (Prims.of_int (98)) + (Prims.of_int (100)) (Prims.of_int (15))))) (Obj.magic (prove_pures preamble pst1)) (fun pst2 -> @@ -396,21 +396,21 @@ let rec (prove_pures : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (105)) (Prims.of_int (6)) - (Prims.of_int (106)) (Prims.of_int (48))))) + (Prims.of_int (107)) (Prims.of_int (6)) + (Prims.of_int (108)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (104)) (Prims.of_int (4)) - (Prims.of_int (106)) (Prims.of_int (48))))) + (Prims.of_int (106)) (Prims.of_int (4)) + (Prims.of_int (108)) (Prims.of_int (48))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (106)) (Prims.of_int (9)) - (Prims.of_int (106)) + (Prims.of_int (108)) (Prims.of_int (9)) + (Prims.of_int (108)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic @@ -449,12 +449,12 @@ let rec (prover : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (115)) (Prims.of_int (2)) (Prims.of_int (118)) + (Prims.of_int (117)) (Prims.of_int (2)) (Prims.of_int (120)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (120)) (Prims.of_int (2)) (Prims.of_int (166)) + (Prims.of_int (122)) (Prims.of_int (2)) (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover @@ -464,13 +464,13 @@ let rec (prover : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (118)) (Prims.of_int (6)) - (Prims.of_int (118)) (Prims.of_int (54))))) + (Prims.of_int (120)) (Prims.of_int (6)) + (Prims.of_int (120)) (Prims.of_int (54))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (116)) (Prims.of_int (4)) - (Prims.of_int (118)) (Prims.of_int (54))))) + (Prims.of_int (118)) (Prims.of_int (4)) + (Prims.of_int (120)) (Prims.of_int (54))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string (Pulse_Typing_Combinators.list_as_vprop @@ -483,17 +483,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (116)) - (Prims.of_int (4)) (Prims.of_int (118)) + (Prims.of_int (4)) + (Prims.of_int (120)) (Prims.of_int (54))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (116)) - (Prims.of_int (4)) (Prims.of_int (118)) + (Prims.of_int (4)) + (Prims.of_int (120)) (Prims.of_int (54))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -501,9 +501,9 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (117)) + (Prims.of_int (119)) (Prims.of_int (6)) - (Prims.of_int (117)) + (Prims.of_int (119)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic @@ -546,14 +546,14 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (123)) (Prims.of_int (14)) - (Prims.of_int (123)) (Prims.of_int (45))))) + (Prims.of_int (125)) (Prims.of_int (14)) + (Prims.of_int (125)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (125)) (Prims.of_int (4)) - (Prims.of_int (166)) (Prims.of_int (32))))) + (Prims.of_int (127)) (Prims.of_int (4)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_ElimExists.elim_exists_pst preamble pst0)) @@ -565,17 +565,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (125)) - (Prims.of_int (4)) (Prims.of_int (127)) + (Prims.of_int (4)) + (Prims.of_int (129)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (127)) + (Prims.of_int (129)) (Prims.of_int (63)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover @@ -586,9 +586,9 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (127)) + (Prims.of_int (129)) (Prims.of_int (8)) - (Prims.of_int (127)) + (Prims.of_int (129)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic @@ -617,17 +617,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (129)) + (Prims.of_int (131)) (Prims.of_int (14)) - (Prims.of_int (129)) + (Prims.of_int (131)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (131)) + (Prims.of_int (133)) (Prims.of_int (4)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_ElimPure.elim_pure_pst @@ -640,17 +640,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (131)) - (Prims.of_int (4)) (Prims.of_int (133)) + (Prims.of_int (4)) + (Prims.of_int (135)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (133)) + (Prims.of_int (135)) (Prims.of_int (63)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover @@ -662,9 +662,9 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (133)) + (Prims.of_int (135)) (Prims.of_int (8)) - (Prims.of_int (133)) + (Prims.of_int (135)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic @@ -696,17 +696,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (135)) + (Prims.of_int (137)) (Prims.of_int (29)) - (Prims.of_int (135)) + (Prims.of_int (137)) (Prims.of_int (82))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (133)) + (Prims.of_int (135)) (Prims.of_int (63)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -733,17 +733,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (137)) - (Prims.of_int (4)) (Prims.of_int (139)) + (Prims.of_int (4)) + (Prims.of_int (141)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (88)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover @@ -755,17 +755,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (47)) - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (86))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (138)) + (Prims.of_int (140)) (Prims.of_int (6)) - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (86))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -781,17 +781,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (138)) + (Prims.of_int (140)) (Prims.of_int (6)) - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (86))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (138)) + (Prims.of_int (140)) (Prims.of_int (6)) - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (86))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -799,9 +799,9 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (8)) - (Prims.of_int (139)) + (Prims.of_int (141)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic @@ -847,17 +847,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (141)) + (Prims.of_int (143)) (Prims.of_int (14)) - (Prims.of_int (141)) + (Prims.of_int (143)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (143)) + (Prims.of_int (145)) (Prims.of_int (4)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -878,17 +878,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (143)) - (Prims.of_int (4)) (Prims.of_int (145)) + (Prims.of_int (4)) + (Prims.of_int (147)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (147)) + (Prims.of_int (149)) (Prims.of_int (4)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover @@ -900,9 +900,9 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (145)) + (Prims.of_int (147)) (Prims.of_int (8)) - (Prims.of_int (145)) + (Prims.of_int (147)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic @@ -958,17 +958,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (151)) + (Prims.of_int (153)) (Prims.of_int (33)) - (Prims.of_int (151)) + (Prims.of_int (153)) (Prims.of_int (85))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (150)) + (Prims.of_int (152)) (Prims.of_int (10)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -995,17 +995,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (152)) + (Prims.of_int (154)) (Prims.of_int (16)) - (Prims.of_int (152)) + (Prims.of_int (154)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (153)) + (Prims.of_int (155)) (Prims.of_int (6)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1044,17 +1044,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (156)) + (Prims.of_int (158)) (Prims.of_int (22)) - (Prims.of_int (156)) + (Prims.of_int (158)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (157)) + (Prims.of_int (159)) (Prims.of_int (8)) - (Prims.of_int (166)) + (Prims.of_int (168)) (Prims.of_int (32))))) (Obj.magic (match_q @@ -1078,17 +1078,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (165)) + (Prims.of_int (167)) (Prims.of_int (10)) - (Prims.of_int (165)) + (Prims.of_int (167)) (Prims.of_int (30))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1096,17 +1096,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (12)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -1121,17 +1121,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1139,17 +1139,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (163)) + (Prims.of_int (165)) (Prims.of_int (12)) - (Prims.of_int (163)) + (Prims.of_int (165)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -1166,17 +1166,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1184,17 +1184,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (162)) + (Prims.of_int (164)) (Prims.of_int (12)) - (Prims.of_int (162)) + (Prims.of_int (164)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -1212,17 +1212,17 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (159)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (164)) + (Prims.of_int (166)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1230,9 +1230,9 @@ let rec (prover : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (161)) + (Prims.of_int (163)) (Prims.of_int (12)) - (Prims.of_int (161)) + (Prims.of_int (163)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic @@ -1370,13 +1370,13 @@ let (prove : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (190)) (Prims.of_int (2)) - (Prims.of_int (192)) (Prims.of_int (55))))) + (Prims.of_int (192)) (Prims.of_int (2)) + (Prims.of_int (194)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (192)) (Prims.of_int (56)) - (Prims.of_int (256)) (Prims.of_int (97))))) + (Prims.of_int (194)) (Prims.of_int (56)) + (Prims.of_int (258)) (Prims.of_int (97))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover g (fun uu___ -> @@ -1385,14 +1385,14 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (192)) (Prims.of_int (30)) - (Prims.of_int (192)) (Prims.of_int (54))))) + (Prims.of_int (194)) (Prims.of_int (30)) + (Prims.of_int (194)) (Prims.of_int (54))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (191)) (Prims.of_int (4)) - (Prims.of_int (192)) (Prims.of_int (54))))) + (Prims.of_int (193)) (Prims.of_int (4)) + (Prims.of_int (194)) (Prims.of_int (54))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string goals)) (fun uu___1 -> @@ -1403,17 +1403,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (191)) + (Prims.of_int (193)) (Prims.of_int (4)) - (Prims.of_int (192)) + (Prims.of_int (194)) (Prims.of_int (54))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (191)) + (Prims.of_int (193)) (Prims.of_int (4)) - (Prims.of_int (192)) + (Prims.of_int (194)) (Prims.of_int (54))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1421,9 +1421,9 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (192)) + (Prims.of_int (194)) (Prims.of_int (6)) - (Prims.of_int (192)) + (Prims.of_int (194)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic @@ -1459,14 +1459,14 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (194)) (Prims.of_int (15)) - (Prims.of_int (194)) (Prims.of_int (33))))) + (Prims.of_int (196)) (Prims.of_int (15)) + (Prims.of_int (196)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (208)) (Prims.of_int (6)) - (Prims.of_int (256)) (Prims.of_int (97))))) + (Prims.of_int (210)) (Prims.of_int (6)) + (Prims.of_int (258)) (Prims.of_int (97))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Typing_Combinators.vprop_as_list ctxt)) @@ -1478,17 +1478,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (209)) + (Prims.of_int (211)) (Prims.of_int (61)) - (Prims.of_int (209)) + (Prims.of_int (211)) (Prims.of_int (69))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (209)) + (Prims.of_int (211)) (Prims.of_int (72)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (97))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> ())) @@ -1500,17 +1500,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (211)) + (Prims.of_int (213)) (Prims.of_int (6)) - (Prims.of_int (215)) + (Prims.of_int (217)) (Prims.of_int (12))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (218)) + (Prims.of_int (220)) (Prims.of_int (43)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (97))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1535,17 +1535,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (220)) + (Prims.of_int (222)) (Prims.of_int (6)) - (Prims.of_int (229)) + (Prims.of_int (231)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (230)) + (Prims.of_int (232)) (Prims.of_int (8)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (97))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1604,17 +1604,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (14)) - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (25))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (232)) + (Prims.of_int (234)) (Prims.of_int (28)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (97))))) (Obj.magic (prover @@ -1630,17 +1630,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (15)) - (Prims.of_int (234)) + (Prims.of_int (236)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (236)) + (Prims.of_int (238)) (Prims.of_int (4)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (97))))) (Obj.magic (Pulse_Checker_Prover_Substs.ss_to_nt_substs @@ -1657,17 +1657,17 @@ let (prove : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (236)) + (Prims.of_int (238)) (Prims.of_int (4)) - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (237)) + (Prims.of_int (239)) (Prims.of_int (66)) - (Prims.of_int (256)) + (Prims.of_int (258)) (Prims.of_int (97))))) (if FStar_Pervasives_Native.uu___is_None @@ -1757,13 +1757,13 @@ let (try_frame_pre_uvs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (266)) (Prims.of_int (10)) - (Prims.of_int (266)) (Prims.of_int (48))))) + (Prims.of_int (268)) (Prims.of_int (10)) + (Prims.of_int (268)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (266)) (Prims.of_int (51)) - (Prims.of_int (304)) (Prims.of_int (27))))) + (Prims.of_int (268)) (Prims.of_int (51)) + (Prims.of_int (324)) (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context g "try_frame_pre" @@ -1776,17 +1776,17 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (269)) (Prims.of_int (4)) - (Prims.of_int (269)) + (Prims.of_int (271)) (Prims.of_int (4)) + (Prims.of_int (271)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (266)) + (Prims.of_int (268)) (Prims.of_int (51)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (Obj.magic (prove g1 ctxt () uvs (Pulse_Syntax_Base.comp_pre c) ())) @@ -1801,18 +1801,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (273)) + (Prims.of_int (275)) (Prims.of_int (4)) - (Prims.of_int (273)) + (Prims.of_int (275)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (275)) + (Prims.of_int (277)) (Prims.of_int (82)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Checker_Prover_Util.st_typing_weakening @@ -1825,18 +1825,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (276)) + (Prims.of_int (278)) (Prims.of_int (10)) - (Prims.of_int (276)) + (Prims.of_int (278)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (276)) + (Prims.of_int (278)) (Prims.of_int (38)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Checker_Prover_Substs.nt_subst_st_term @@ -1849,18 +1849,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (277)) + (Prims.of_int (279)) (Prims.of_int (10)) - (Prims.of_int (277)) + (Prims.of_int (279)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (277)) + (Prims.of_int (279)) (Prims.of_int (35)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1876,18 +1876,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (280)) + (Prims.of_int (282)) (Prims.of_int (4)) - (Prims.of_int (280)) + (Prims.of_int (282)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (280)) + (Prims.of_int (282)) (Prims.of_int (50)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1904,18 +1904,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (282)) + (Prims.of_int (284)) (Prims.of_int (82)) - (Prims.of_int (282)) + (Prims.of_int (284)) (Prims.of_int (102))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (282)) + (Prims.of_int (284)) (Prims.of_int (105)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1933,18 +1933,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (284)) + (Prims.of_int (286)) (Prims.of_int (10)) - (Prims.of_int (284)) + (Prims.of_int (286)) (Prims.of_int (18))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (284)) + (Prims.of_int (286)) (Prims.of_int (21)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1959,18 +1959,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (11)) - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (285)) + (Prims.of_int (287)) (Prims.of_int (24)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1986,18 +1986,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (286)) + (Prims.of_int (288)) (Prims.of_int (11)) - (Prims.of_int (286)) + (Prims.of_int (288)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (287)) + (Prims.of_int (289)) (Prims.of_int (31)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -2015,18 +2015,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (288)) + (Prims.of_int (290)) (Prims.of_int (14)) - (Prims.of_int (288)) + (Prims.of_int (290)) (Prims.of_int (79))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (288)) + (Prims.of_int (290)) (Prims.of_int (82)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -2047,18 +2047,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (290)) + (Prims.of_int (292)) (Prims.of_int (29)) - (Prims.of_int (290)) + (Prims.of_int (292)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (290)) + (Prims.of_int (292)) (Prims.of_int (65)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (324)) + (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -2075,18 +2075,18 @@ let (try_frame_pre_uvs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (295)) + (Prims.of_int (297)) (Prims.of_int (4)) - (Prims.of_int (295)) + (Prims.of_int (297)) (Prims.of_int (67))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" (Prims.of_int (304)) - (Prims.of_int (2)) - (Prims.of_int (304)) - (Prims.of_int (27))))) + (Prims.of_int (35)) + (Prims.of_int (324)) + (Prims.of_int (65))))) (Obj.magic (Pulse_Checker_Base.continuation_elaborator_with_bind g11 @@ -2097,10 +2097,30 @@ let (try_frame_pre_uvs : FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> + match + Pulse_Typing_Metatheory.st_comp_typing_inversion_cofinite + g11 + (Pulse_Syntax_Base.st_comp_of_comp + c1) + (Pulse_Typing_Metatheory.comp_typing_inversion + g11 c1 + (Pulse_Typing_Metatheory.st_typing_correctness + g11 t1 c1 + d3)) + with + | + (comp_res_typing_in_g1, + uu___2, + f) -> FStar_Pervasives.Mkdtuple5 - (x, ty, - ctxt', - g2, + (x, g2, + (FStar_Pervasives.Mkdtuple3 + ((Pulse_Syntax_Base.comp_u + c1), ty, + ())), + (Prims.Mkdtuple2 + (ctxt', + ())), (Pulse_Checker_Base.k_elab_trans g1 g11 g2 ctxt @@ -2153,13 +2173,13 @@ let (try_frame_pre : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (312)) (Prims.of_int (12)) - (Prims.of_int (312)) (Prims.of_int (32))))) + (Prims.of_int (332)) (Prims.of_int (12)) + (Prims.of_int (332)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (314)) (Prims.of_int (2)) - (Prims.of_int (314)) (Prims.of_int (37))))) + (Prims.of_int (334)) (Prims.of_int (2)) + (Prims.of_int (334)) (Prims.of_int (37))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.mk_env (Pulse_Typing_Env.fstar_env g))) @@ -2185,13 +2205,13 @@ let (prove_post_hint : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (323)) (Prims.of_int (10)) - (Prims.of_int (323)) (Prims.of_int (46))))) + (Prims.of_int (343)) (Prims.of_int (10)) + (Prims.of_int (343)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (325)) (Prims.of_int (2)) - (Prims.of_int (360)) (Prims.of_int (64))))) + (Prims.of_int (345)) (Prims.of_int (2)) + (Prims.of_int (388)) (Prims.of_int (102))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context g "prove_post_hint" rng)) @@ -2211,43 +2231,47 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (328)) - (Prims.of_int (36)) - (Prims.of_int (328)) - (Prims.of_int (37))))) + (Prims.of_int (348)) + (Prims.of_int (79)) + (Prims.of_int (348)) + (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (327)) + (Prims.of_int (347)) (Prims.of_int (21)) - (Prims.of_int (360)) - (Prims.of_int (64))))) + (Prims.of_int (388)) + (Prims.of_int (102))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> r)) (fun uu___ -> (fun uu___ -> match uu___ with | FStar_Pervasives.Mkdtuple5 - (x, ty, ctxt', g2, k) -> + (x, g2, FStar_Pervasives.Mkdtuple3 + (u_ty, ty, ty_typing), + Prims.Mkdtuple2 + (ctxt', ctxt'_typing), k) + -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (330)) + (Prims.of_int (350)) (Prims.of_int (27)) - (Prims.of_int (330)) + (Prims.of_int (350)) (Prims.of_int (74))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (333)) + (Prims.of_int (353)) (Prims.of_int (4)) - (Prims.of_int (360)) - (Prims.of_int (64))))) + (Prims.of_int (388)) + (Prims.of_int (102))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Syntax_Naming.open_term_nv @@ -2269,17 +2293,17 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (335)) + (Prims.of_int (355)) (Prims.of_int (11)) - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (334)) + (Prims.of_int (354)) (Prims.of_int (9)) - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (50))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2287,17 +2311,17 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (14)) - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (335)) + (Prims.of_int (355)) (Prims.of_int (11)) - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (50))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -2312,17 +2336,17 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (335)) + (Prims.of_int (355)) (Prims.of_int (11)) - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (335)) + (Prims.of_int (355)) (Prims.of_int (11)) - (Prims.of_int (338)) + (Prims.of_int (358)) (Prims.of_int (50))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2330,9 +2354,9 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (337)) + (Prims.of_int (357)) (Prims.of_int (14)) - (Prims.of_int (337)) + (Prims.of_int (357)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic @@ -2391,9 +2415,13 @@ let (prove_post_hint : fun uu___2 -> FStar_Pervasives.Mkdtuple5 - (x, ty, - post_hint_opened, - g2, k))) + (x, g2, + (FStar_Pervasives.Mkdtuple3 + (u_ty, + ty, ())), + (Prims.Mkdtuple2 + (ctxt', + ())), k))) else Obj.repr (FStar_Tactics_Effect.tac_bind @@ -2402,19 +2430,19 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (343)) + (Prims.of_int (363)) (Prims.of_int (8)) - (Prims.of_int (343)) - (Prims.of_int (88))))) + (Prims.of_int (363)) + (Prims.of_int (90))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (341)) + (Prims.of_int (361)) (Prims.of_int (8)) - (Prims.of_int (360)) - (Prims.of_int (64))))) + (Prims.of_int (388)) + (Prims.of_int (102))))) ( Obj.magic (prove g2 @@ -2443,18 +2471,18 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (348)) + (Prims.of_int (368)) (Prims.of_int (8)) - (Prims.of_int (348)) + (Prims.of_int (368)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (350)) + (Prims.of_int (370)) (Prims.of_int (6)) - (Prims.of_int (360)) - (Prims.of_int (64))))) + (Prims.of_int (388)) + (Prims.of_int (102))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___4 -> @@ -2480,17 +2508,17 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (353)) + (Prims.of_int (373)) (Prims.of_int (10)) - (Prims.of_int (355)) + (Prims.of_int (375)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (352)) + (Prims.of_int (372)) (Prims.of_int (8)) - (Prims.of_int (355)) + (Prims.of_int (375)) (Prims.of_int (47))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2498,9 +2526,9 @@ let (prove_post_hint : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Prover.fst" - (Prims.of_int (355)) + (Prims.of_int (375)) (Prims.of_int (13)) - (Prims.of_int (355)) + (Prims.of_int (375)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic @@ -2543,13 +2571,20 @@ let (prove_post_hint : (fun uu___4 -> FStar_Pervasives.Mkdtuple5 - (x, ty, - post_hint_opened, - g3, + (x, g3, + (FStar_Pervasives.Mkdtuple3 + (u_ty, + ty, ())), + (Prims.Mkdtuple2 + (post_hint_opened, + ())), (Pulse_Checker_Base.k_elab_trans g g2 g3 ctxt - ctxt' + (FStar_Pervasives.dfst + (Prims.Mkdtuple2 + (ctxt', + ()))) post_hint_opened k (Pulse_Checker_Base.k_elab_equiv