From 95a0468486408cd6a02076e3ebe9e4b1dd85fdc3 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 10 Sep 2024 06:33:48 +0000 Subject: [PATCH] Generate impls for ghost functions. --- src/checker/Pulse.Extract.Main.fst | 16 +- src/checker/Pulse.Main.fst | 5 +- .../plugin/generated/Pulse_Extract_Main.ml | 209 +++-- src/ocaml/plugin/generated/Pulse_Main.ml | 765 +++++++++--------- 4 files changed, 545 insertions(+), 450 deletions(-) diff --git a/src/checker/Pulse.Extract.Main.fst b/src/checker/Pulse.Extract.Main.fst index 686f0886f..ab1e139af 100644 --- a/src/checker/Pulse.Extract.Main.fst +++ b/src/checker/Pulse.Extract.Main.fst @@ -744,10 +744,6 @@ let rec extract_dv_recursive g (p:st_term) (rec_name:R.fv) let g, x = extend_env'_binder g b in let body = open_st_term_nv body x in let body = extract_dv_recursive g body rec_name in - let attrs = - b.binder_attrs - |> T.unseal - |> T.map (term_as_mlexpr g) in ECL.mk_abs (extract_dv_binder b q) (close_term body x._2) | _ -> //last binder used for knot; replace it with the recursively bound name let body = LN.subst_st_term body [RT.DT 0 (wr R.(pack_ln (Tv_FVar rec_name)) Range.range_0)] in @@ -756,3 +752,15 @@ let rec extract_dv_recursive g (p:st_term) (rec_name:R.fv) | _ -> T.fail "Unexpected recursive definition of non-function" +let rec extract_dv_ghost g (p:st_term) + : T.Tac ECL.term + = match p.term with + | Tm_Abs { b; q; body } -> ( + let g, x = extend_env'_binder g b in + let body = open_st_term_nv body x in + let body = extract_dv_ghost g body in + ECL.mk_abs (extract_dv_binder b q) (close_term body x._2) + ) + + | _ -> ECL.unit_tm + diff --git a/src/checker/Pulse.Main.fst b/src/checker/Pulse.Main.fst index 58e4504ea..0eef90677 100644 --- a/src/checker/Pulse.Main.fst +++ b/src/checker/Pulse.Main.fst @@ -121,10 +121,11 @@ let check_fndefn let cur_module = T.cur_module () in let maybe_add_impl t (se: RT.sigelt_for (fstar_env g) t) = - if C_STGhost? comp then se else let open Pulse.Extract.Main in begin let uenv = Extract.CompilerLib.new_uenv (fstar_env g) in - if fn_d.isrec then + if C_STGhost? comp then + set_impl se false (extract_dv_ghost { uenv_inner = uenv; coreenv = Extract.CompilerLib.initial_core_env uenv } body) + else if fn_d.isrec then let impl = extract_dv_recursive { uenv_inner = uenv; coreenv = Extract.CompilerLib.initial_core_env uenv } body (R.pack_fv (cur_module @ [nm_orig])) in set_impl se true impl else diff --git a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml index c4bdac596..2f05110ee 100644 --- a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml +++ b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml @@ -6728,7 +6728,7 @@ let rec (extract_dv_recursive : "Pulse.Extract.Main.fst" (Prims.of_int (743)) (Prims.of_int (19)) - (Prims.of_int (751)) + (Prims.of_int (747)) (Prims.of_int (65))))) (Obj.magic (extend_env'_binder g b)) (fun uu___2 -> @@ -6751,7 +6751,7 @@ let rec (extract_dv_recursive : "Pulse.Extract.Main.fst" (Prims.of_int (745)) (Prims.of_int (44)) - (Prims.of_int (751)) + (Prims.of_int (747)) (Prims.of_int (65))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___3 -> @@ -6773,9 +6773,9 @@ let rec (extract_dv_recursive : (Obj.magic (FStar_Range.mk_range "Pulse.Extract.Main.fst" - (Prims.of_int (746)) - (Prims.of_int (58)) - (Prims.of_int (751)) + (Prims.of_int (747)) + (Prims.of_int (8)) + (Prims.of_int (747)) (Prims.of_int (65))))) (Obj.magic (extract_dv_recursive @@ -6790,78 +6790,25 @@ let rec (extract_dv_recursive : (Obj.magic (FStar_Range.mk_range "Pulse.Extract.Main.fst" - (Prims.of_int (748)) - (Prims.of_int (10)) - (Prims.of_int (750)) - (Prims.of_int (37))))) + (Prims.of_int (747)) + (Prims.of_int (19)) + (Prims.of_int (747)) + (Prims.of_int (42))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Extract.Main.fst" - (Prims.of_int (751)) + (Prims.of_int (747)) (Prims.of_int (8)) - (Prims.of_int (751)) + (Prims.of_int (747)) (Prims.of_int (65))))) ( Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Extract.Main.fst" - (Prims.of_int (748)) - (Prims.of_int (10)) - (Prims.of_int (749)) - (Prims.of_int (21))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Extract.Main.fst" - (Prims.of_int (748)) - (Prims.of_int (10)) - (Prims.of_int (750)) - (Prims.of_int (37))))) - (Obj.magic - (FStar_Tactics_Unseal.unseal - b.Pulse_Syntax_Base.binder_attrs)) - (fun - uu___3 -> - (fun - uu___3 -> - Obj.magic - (FStar_Tactics_Util.map - (term_as_mlexpr - g1) - uu___3)) - uu___3))) - ( - fun - uu___3 -> - (fun - attrs -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Extract.Main.fst" - (Prims.of_int (751)) - (Prims.of_int (19)) - (Prims.of_int (751)) - (Prims.of_int (42))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Extract.Main.fst" - (Prims.of_int (751)) - (Prims.of_int (8)) - (Prims.of_int (751)) - (Prims.of_int (65))))) - (Obj.magic (extract_dv_binder b q)) - (fun + ( + fun uu___3 -> FStar_Tactics_Effect.lift_div_tac (fun @@ -6872,7 +6819,6 @@ let rec (extract_dv_recursive : body2 (FStar_Pervasives_Native.__proj__Mktuple2__item___2 x)))))) - uu___3))) uu___3))) uu___3))) uu___2) | uu___1 -> @@ -6881,17 +6827,17 @@ let rec (extract_dv_recursive : (Obj.magic (FStar_Range.mk_range "Pulse.Extract.Main.fst" - (Prims.of_int (753)) + (Prims.of_int (749)) (Prims.of_int (19)) - (Prims.of_int (753)) + (Prims.of_int (749)) (Prims.of_int (100))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Extract.Main.fst" - (Prims.of_int (754)) + (Prims.of_int (750)) (Prims.of_int (8)) - (Prims.of_int (754)) + (Prims.of_int (750)) (Prims.of_int (25))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -6911,4 +6857,123 @@ let rec (extract_dv_recursive : (Obj.repr (FStar_Tactics_V2_Derived.fail "Unexpected recursive definition of non-function"))) - uu___2 uu___1 uu___ \ No newline at end of file + uu___2 uu___1 uu___ +let rec (extract_dv_ghost : + env -> + Pulse_Syntax_Base.st_term -> + (Pulse_Extract_CompilerLib.term, unit) FStar_Tactics_Effect.tac_repr) + = + fun uu___1 -> + fun uu___ -> + (fun g -> + fun p -> + match p.Pulse_Syntax_Base.term1 with + | Pulse_Syntax_Base.Tm_Abs + { Pulse_Syntax_Base.b = b; Pulse_Syntax_Base.q = q; + Pulse_Syntax_Base.ascription = uu___; + Pulse_Syntax_Base.body = body;_} + -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Extract.Main.fst" + (Prims.of_int (759)) (Prims.of_int (19)) + (Prims.of_int (759)) (Prims.of_int (41))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "Pulse.Extract.Main.fst" + (Prims.of_int (758)) (Prims.of_int (31)) + (Prims.of_int (763)) (Prims.of_int (5))))) + (Obj.magic (extend_env'_binder g b)) + (fun uu___1 -> + (fun uu___1 -> + match uu___1 with + | (g1, x) -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Extract.Main.fst" + (Prims.of_int (760)) + (Prims.of_int (19)) + (Prims.of_int (760)) + (Prims.of_int (41))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Extract.Main.fst" + (Prims.of_int (760)) + (Prims.of_int (44)) + (Prims.of_int (762)) + (Prims.of_int (65))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Pulse_Syntax_Naming.open_st_term_nv + body x)) + (fun uu___2 -> + (fun body1 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Extract.Main.fst" + (Prims.of_int (761)) + (Prims.of_int (19)) + (Prims.of_int (761)) + (Prims.of_int (42))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Extract.Main.fst" + (Prims.of_int (762)) + (Prims.of_int (8)) + (Prims.of_int (762)) + (Prims.of_int (65))))) + (Obj.magic + (extract_dv_ghost g1 + body1)) + (fun uu___2 -> + (fun body2 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Extract.Main.fst" + (Prims.of_int (762)) + (Prims.of_int (19)) + (Prims.of_int (762)) + (Prims.of_int (42))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Extract.Main.fst" + (Prims.of_int (762)) + (Prims.of_int (8)) + (Prims.of_int (762)) + (Prims.of_int (65))))) + (Obj.magic + (extract_dv_binder + b q)) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 + -> + Pulse_Extract_CompilerLib.mk_abs + uu___2 + (Pulse_Syntax_Naming.close_term + body2 + (FStar_Pervasives_Native.__proj__Mktuple2__item___2 + x)))))) + uu___2))) uu___2))) + uu___1))) + | uu___ -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> Pulse_Extract_CompilerLib.unit_tm)))) + uu___1 uu___ \ No newline at end of file diff --git a/src/ocaml/plugin/generated/Pulse_Main.ml b/src/ocaml/plugin/generated/Pulse_Main.ml index 11ba985bd..ecfda42a0 100644 --- a/src/ocaml/plugin/generated/Pulse_Main.ml +++ b/src/ocaml/plugin/generated/Pulse_Main.ml @@ -225,7 +225,7 @@ let (check_fndefn : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (83)) Prims.int_one (Prims.of_int (196)) + (Prims.of_int (83)) Prims.int_one (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> d.Pulse_Syntax_Base.d)) @@ -244,7 +244,7 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (87)) (Prims.of_int (46)) - (Prims.of_int (196)) (Prims.of_int (5))))) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> FStar_Pervasives_Native.fst @@ -268,7 +268,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (92)) (Prims.of_int (4)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (if fn_d.Pulse_Syntax_Base.isrec then @@ -300,7 +300,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (92)) (Prims.of_int (4)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -339,7 +339,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (97)) (Prims.of_int (2)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -367,7 +367,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (98)) (Prims.of_int (63)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (if Prims.uu___is_Nil @@ -407,7 +407,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (99)) (Prims.of_int (37)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (mk_abs g @@ -433,7 +433,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (101)) (Prims.of_int (2)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -459,7 +459,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (101)) (Prims.of_int (97)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (debug_main @@ -516,7 +516,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (101)) (Prims.of_int (97)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (Pulse_Checker_Abs.check_abs @@ -550,7 +550,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (109)) (Prims.of_int (2)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (Pulse_Checker_Prover_Util.debug_prover @@ -662,7 +662,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (112)) (Prims.of_int (63)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (debug_main @@ -775,7 +775,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (114)) (Prims.of_int (29)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -802,7 +802,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (116)) (Prims.of_int (90)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -831,7 +831,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (118)) (Prims.of_int (36)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -858,7 +858,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (120)) (Prims.of_int (67)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -909,7 +909,7 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (121)) (Prims.of_int (37)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -927,68 +927,92 @@ let (check_fndefn : "Pulse.Main.fst" (Prims.of_int (124)) (Prims.of_int (4)) - (Prims.of_int (132)) + (Prims.of_int (133)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (132)) + (Prims.of_int (133)) (Prims.of_int (10)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___9 -> - fun - uu___8 -> - fun - uu___7 -> - (fun uu___7 -> fun t -> fun se -> - if - Pulse_Syntax_Base.uu___is_C_STGhost - comp - then - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___8 -> - se))) - else - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind + FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (126)) + (Prims.of_int (125)) (Prims.of_int (15)) - (Prims.of_int (126)) + (Prims.of_int (125)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (127)) + (Prims.of_int (126)) (Prims.of_int (4)) - (Prims.of_int (131)) + (Prims.of_int (132)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___9 -> + uu___8 -> Pulse_Extract_CompilerLib.new_uenv (Pulse_Typing_Env.fstar_env g))) (fun - uu___9 -> + uu___8 -> (fun uenv -> if + Pulse_Syntax_Base.uu___is_C_STGhost + comp + then + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Main.fst" + (Prims.of_int (127)) + (Prims.of_int (24)) + (Prims.of_int (127)) + (Prims.of_int (122))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Main.fst" + (Prims.of_int (127)) + (Prims.of_int (6)) + (Prims.of_int (127)) + (Prims.of_int (122))))) + (Obj.magic + (Pulse_Extract_Main.extract_dv_ghost + { + Pulse_Extract_Main.uenv_inner + = uenv; + Pulse_Extract_Main.coreenv + = + (Pulse_Extract_CompilerLib.initial_core_env + uenv) + } body2)) + (fun + uu___8 -> + FStar_Tactics_Effect.lift_div_tac + (fun + uu___9 -> + set_impl + (Pulse_Typing_Env.fstar_env + g) t se + false + uu___8))) + else + if fn_d.Pulse_Syntax_Base.isrec then Obj.magic @@ -997,17 +1021,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (128)) + (Prims.of_int (129)) (Prims.of_int (17)) - (Prims.of_int (128)) + (Prims.of_int (129)) (Prims.of_int (154))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (6)) - (Prims.of_int (129)) + (Prims.of_int (130)) (Prims.of_int (27))))) (Obj.magic (Pulse_Extract_Main.extract_dv_recursive @@ -1039,17 +1063,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (131)) + (Prims.of_int (132)) (Prims.of_int (24)) - (Prims.of_int (131)) + (Prims.of_int (132)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (131)) + (Prims.of_int (132)) (Prims.of_int (6)) - (Prims.of_int (131)) + (Prims.of_int (132)) (Prims.of_int (52))))) (Obj.magic (Pulse_Extract_Main.extract_pulse_dv @@ -1067,10 +1091,7 @@ let (check_fndefn : g) t se false uu___10)))) - uu___9)))) - uu___9 - uu___8 - uu___7)) + uu___8))) (fun uu___7 -> (fun @@ -1082,17 +1103,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (136)) + (Prims.of_int (137)) (Prims.of_int (78)) - (Prims.of_int (140)) + (Prims.of_int (141)) (Prims.of_int (99))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (143)) + (Prims.of_int (144)) (Prims.of_int (2)) - (Prims.of_int (196)) + (Prims.of_int (197)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1107,17 +1128,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (137)) + (Prims.of_int (138)) (Prims.of_int (13)) - (Prims.of_int (137)) + (Prims.of_int (138)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (138)) + (Prims.of_int (139)) (Prims.of_int (4)) - (Prims.of_int (140)) + (Prims.of_int (141)) (Prims.of_int (99))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1170,17 +1191,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (152)) + (Prims.of_int (153)) (Prims.of_int (20)) - (Prims.of_int (152)) + (Prims.of_int (153)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (152)) + (Prims.of_int (153)) (Prims.of_int (45)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (Obj.magic (mk_main_decl @@ -1196,17 +1217,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (153)) + (Prims.of_int (154)) (Prims.of_int (54)) - (Prims.of_int (153)) + (Prims.of_int (154)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (153)) + (Prims.of_int (154)) (Prims.of_int (66)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1223,17 +1244,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (154)) + (Prims.of_int (155)) (Prims.of_int (23)) - (Prims.of_int (154)) + (Prims.of_int (155)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (153)) + (Prims.of_int (154)) (Prims.of_int (66)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1255,17 +1276,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (155)) + (Prims.of_int (156)) (Prims.of_int (13)) - (Prims.of_int (155)) + (Prims.of_int (156)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (155)) + (Prims.of_int (156)) (Prims.of_int (59)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1284,17 +1305,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (156)) + (Prims.of_int (157)) (Prims.of_int (20)) - (Prims.of_int (156)) + (Prims.of_int (157)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (156)) + (Prims.of_int (157)) (Prims.of_int (51)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1328,17 +1349,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (157)) + (Prims.of_int (158)) (Prims.of_int (13)) - (Prims.of_int (157)) + (Prims.of_int (158)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (157)) + (Prims.of_int (158)) (Prims.of_int (60)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1368,17 +1389,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (158)) + (Prims.of_int (159)) (Prims.of_int (13)) - (Prims.of_int (158)) + (Prims.of_int (159)) (Prims.of_int (37))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (158)) + (Prims.of_int (159)) (Prims.of_int (40)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1395,17 +1416,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (159)) + (Prims.of_int (160)) (Prims.of_int (24)) - (Prims.of_int (159)) + (Prims.of_int (160)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (159)) + (Prims.of_int (160)) (Prims.of_int (56)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1423,17 +1444,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (160)) + (Prims.of_int (161)) (Prims.of_int (20)) - (Prims.of_int (160)) + (Prims.of_int (161)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (160)) + (Prims.of_int (161)) (Prims.of_int (41)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1453,17 +1474,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (162)) + (Prims.of_int (163)) (Prims.of_int (6)) - (Prims.of_int (162)) + (Prims.of_int (163)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (4)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (Obj.magic (Pulse_Recursion.tie_knot @@ -1483,17 +1504,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (17)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (4)) - (Prims.of_int (163)) + (Prims.of_int (164)) (Prims.of_int (52))))) (Obj.magic (maybe_add_impl @@ -1525,17 +1546,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (174)) + (Prims.of_int (175)) (Prims.of_int (6)) - (Prims.of_int (189)) + (Prims.of_int (190)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (165)) + (Prims.of_int (166)) (Prims.of_int (12)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (match expected_t with @@ -1560,17 +1581,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (178)) + (Prims.of_int (179)) (Prims.of_int (18)) - (Prims.of_int (178)) + (Prims.of_int (179)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (189)) + (Prims.of_int (190)) (Prims.of_int (8)) - (Prims.of_int (189)) + (Prims.of_int (190)) (Prims.of_int (19))))) (Obj.magic (Pulse_Checker_Pure.check_subtyping @@ -1600,17 +1621,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (190)) + (Prims.of_int (191)) (Prims.of_int (6)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (190)) + (Prims.of_int (191)) (Prims.of_int (6)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1628,17 +1649,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (192)) + (Prims.of_int (193)) (Prims.of_int (20)) - (Prims.of_int (192)) + (Prims.of_int (193)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (192)) + (Prims.of_int (193)) (Prims.of_int (45)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (Obj.magic (mk_main_decl @@ -1656,17 +1677,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (193)) + (Prims.of_int (194)) (Prims.of_int (21)) - (Prims.of_int (193)) + (Prims.of_int (194)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (192)) + (Prims.of_int (193)) (Prims.of_int (45)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1691,17 +1712,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (194)) + (Prims.of_int (195)) (Prims.of_int (20)) - (Prims.of_int (194)) + (Prims.of_int (195)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (4)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1722,17 +1743,17 @@ let (check_fndefn : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (8)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (4)) - (Prims.of_int (195)) + (Prims.of_int (196)) (Prims.of_int (38))))) (Obj.magic (maybe_add_impl @@ -1781,12 +1802,12 @@ let (check_fndecl : FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (203)) - (Prims.of_int (32)) (Prims.of_int (203)) (Prims.of_int (35))))) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (204)) + (Prims.of_int (32)) (Prims.of_int (204)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (202)) - Prims.int_one (Prims.of_int (240)) (Prims.of_int (29))))) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (203)) + Prims.int_one (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> d.Pulse_Syntax_Base.d)) (fun uu___ -> @@ -1801,13 +1822,13 @@ let (check_fndecl : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (204)) (Prims.of_int (2)) - (Prims.of_int (205)) (Prims.of_int (62))))) + (Prims.of_int (205)) (Prims.of_int (2)) + (Prims.of_int (206)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (205)) (Prims.of_int (63)) - (Prims.of_int (240)) (Prims.of_int (29))))) + (Prims.of_int (206)) (Prims.of_int (63)) + (Prims.of_int (241)) (Prims.of_int (29))))) (if Prims.uu___is_Nil bs then Obj.magic @@ -1829,17 +1850,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (207)) + (Prims.of_int (208)) (Prims.of_int (11)) - (Prims.of_int (207)) + (Prims.of_int (208)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (207)) + (Prims.of_int (208)) (Prims.of_int (36)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1854,17 +1875,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (208)) + (Prims.of_int (209)) (Prims.of_int (12)) - (Prims.of_int (208)) + (Prims.of_int (209)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (208)) + (Prims.of_int (209)) (Prims.of_int (35)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1878,17 +1899,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (213)) + (Prims.of_int (214)) (Prims.of_int (4)) - (Prims.of_int (220)) + (Prims.of_int (221)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (222)) + (Prims.of_int (223)) (Prims.of_int (4)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1927,17 +1948,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (223)) + (Prims.of_int (224)) (Prims.of_int (13)) - (Prims.of_int (223)) + (Prims.of_int (224)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (223)) + (Prims.of_int (224)) (Prims.of_int (37)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic (mk_abs g @@ -1953,17 +1974,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (224)) + (Prims.of_int (225)) (Prims.of_int (12)) - (Prims.of_int (224)) + (Prims.of_int (225)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (224)) + (Prims.of_int (225)) (Prims.of_int (25)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1979,17 +2000,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (227)) + (Prims.of_int (228)) (Prims.of_int (4)) - (Prims.of_int (229)) + (Prims.of_int (230)) (Prims.of_int (5))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (224)) + (Prims.of_int (225)) (Prims.of_int (25)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic (Pulse_RuntimeUtils.with_extv @@ -2018,17 +2039,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (231)) + (Prims.of_int (232)) (Prims.of_int (12)) - (Prims.of_int (231)) + (Prims.of_int (232)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (231)) + (Prims.of_int (232)) (Prims.of_int (26)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2045,17 +2066,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (233)) + (Prims.of_int (234)) (Prims.of_int (4)) - (Prims.of_int (238)) + (Prims.of_int (239)) (Prims.of_int (5))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (2)) - (Prims.of_int (240)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2063,17 +2084,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (234)) + (Prims.of_int (235)) (Prims.of_int (4)) - (Prims.of_int (238)) + (Prims.of_int (239)) (Prims.of_int (5))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (233)) + (Prims.of_int (234)) (Prims.of_int (4)) - (Prims.of_int (238)) + (Prims.of_int (239)) (Prims.of_int (5))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2081,17 +2102,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (6)) - (Prims.of_int (237)) + (Prims.of_int (238)) (Prims.of_int (15))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (234)) + (Prims.of_int (235)) (Prims.of_int (4)) - (Prims.of_int (238)) + (Prims.of_int (239)) (Prims.of_int (5))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2099,17 +2120,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (11)) - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (6)) - (Prims.of_int (237)) + (Prims.of_int (238)) (Prims.of_int (15))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2117,17 +2138,17 @@ let (check_fndecl : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (11)) - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (24))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (11)) - (Prims.of_int (235)) + (Prims.of_int (236)) (Prims.of_int (31))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -2214,16 +2235,16 @@ let (main' : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (247)) - (Prims.of_int (6)) (Prims.of_int (248)) + (Prims.of_int (6)) + (Prims.of_int (249)) (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (89)) - (Prims.of_int (259)) + (Prims.of_int (260)) (Prims.of_int (82))))) (if Pulse_RuntimeUtils.debug_at_level @@ -2236,17 +2257,17 @@ let (main' : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (16)) - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (8)) - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (88))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2254,9 +2275,9 @@ let (main' : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (67)) - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic @@ -2294,17 +2315,17 @@ let (main' : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (249)) + (Prims.of_int (250)) (Prims.of_int (38)) - (Prims.of_int (249)) + (Prims.of_int (250)) (Prims.of_int (84))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (248)) + (Prims.of_int (249)) (Prims.of_int (89)) - (Prims.of_int (259)) + (Prims.of_int (260)) (Prims.of_int (82))))) (Obj.magic (Pulse_Checker_Pure.compute_tot_term_type @@ -2320,17 +2341,17 @@ let (main' : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (250)) - (Prims.of_int (6)) (Prims.of_int (251)) + (Prims.of_int (6)) + (Prims.of_int (252)) (Prims.of_int (110))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (251)) + (Prims.of_int (252)) (Prims.of_int (111)) - (Prims.of_int (259)) + (Prims.of_int (260)) (Prims.of_int (82))))) (if Prims.op_Negation @@ -2364,18 +2385,18 @@ let (main' : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (252)) + (Prims.of_int (253)) (Prims.of_int (52)) - (Prims.of_int (252)) + (Prims.of_int (253)) (Prims.of_int (62))))) ( FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (253)) + (Prims.of_int (254)) (Prims.of_int (6)) - (Prims.of_int (259)) + (Prims.of_int (260)) (Prims.of_int (82))))) ( FStar_Tactics_Effect.lift_div_tac @@ -2445,36 +2466,36 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (265)) - (Prims.of_int (2)) (Prims.of_int (266)) (Prims.of_int (35))))) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (266)) + (Prims.of_int (2)) (Prims.of_int (267)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (266)) - (Prims.of_int (36)) (Prims.of_int (287)) (Prims.of_int (4))))) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (267)) + (Prims.of_int (36)) (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (265)) - (Prims.of_int (5)) (Prims.of_int (265)) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (266)) + (Prims.of_int (5)) (Prims.of_int (266)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (265)) - (Prims.of_int (2)) (Prims.of_int (266)) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (266)) + (Prims.of_int (2)) (Prims.of_int (267)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (265)) (Prims.of_int (23)) - (Prims.of_int (265)) (Prims.of_int (35))))) + (Prims.of_int (266)) (Prims.of_int (23)) + (Prims.of_int (266)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (265)) (Prims.of_int (5)) - (Prims.of_int (265)) (Prims.of_int (48))))) + (Prims.of_int (266)) (Prims.of_int (5)) + (Prims.of_int (266)) (Prims.of_int (48))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env ())) (fun uu___1 -> FStar_Tactics_Effect.lift_div_tac @@ -2501,13 +2522,13 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (269)) (Prims.of_int (18)) - (Prims.of_int (269)) (Prims.of_int (30))))) + (Prims.of_int (270)) (Prims.of_int (18)) + (Prims.of_int (270)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (270)) (Prims.of_int (2)) - (Prims.of_int (287)) (Prims.of_int (4))))) + (Prims.of_int (271)) (Prims.of_int (2)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_V2_Derived.smt_goals ())) (fun uu___2 -> (fun smt_goals -> @@ -2516,30 +2537,30 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (270)) (Prims.of_int (2)) - (Prims.of_int (270)) (Prims.of_int (34))))) + (Prims.of_int (271)) (Prims.of_int (2)) + (Prims.of_int (271)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (271)) (Prims.of_int (2)) - (Prims.of_int (287)) (Prims.of_int (4))))) + (Prims.of_int (272)) (Prims.of_int (2)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (12)) - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (2)) - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (34))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2547,17 +2568,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (13)) - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (12)) - (Prims.of_int (270)) + (Prims.of_int (271)) (Prims.of_int (34))))) (Obj.magic (FStar_Tactics_V2_Derived.goals ())) @@ -2579,17 +2600,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (271)) + (Prims.of_int (272)) (Prims.of_int (2)) - (Prims.of_int (271)) + (Prims.of_int (272)) (Prims.of_int (18))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (271)) + (Prims.of_int (272)) (Prims.of_int (19)) - (Prims.of_int (287)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_V2_Builtins.set_smt_goals @@ -2602,17 +2623,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (272)) + (Prims.of_int (273)) (Prims.of_int (10)) - (Prims.of_int (272)) + (Prims.of_int (273)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (2)) - (Prims.of_int (287)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2620,17 +2641,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (272)) + (Prims.of_int (273)) (Prims.of_int (26)) - (Prims.of_int (272)) + (Prims.of_int (273)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (272)) + (Prims.of_int (273)) (Prims.of_int (10)) - (Prims.of_int (272)) + (Prims.of_int (273)) (Prims.of_int (36))))) (Obj.magic (FStar_Tactics_V2_Derived.goals @@ -2648,17 +2669,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (2)) - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (2)) - (Prims.of_int (287)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2666,17 +2687,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (9)) - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (2)) - (Prims.of_int (273)) + (Prims.of_int (274)) (Prims.of_int (22))))) (Obj.magic (FStar_Tactics_V2_Derived.repeat @@ -2696,17 +2717,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (2)) - (Prims.of_int (282)) + (Prims.of_int (283)) (Prims.of_int (3))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (2)) - (Prims.of_int (287)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2714,17 +2735,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (5)) - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (2)) - (Prims.of_int (282)) + (Prims.of_int (283)) (Prims.of_int (3))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2732,17 +2753,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (9)) - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (5)) - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (26))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2750,17 +2771,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (15)) - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (25))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (9)) - (Prims.of_int (278)) + (Prims.of_int (279)) (Prims.of_int (26))))) (Obj.magic (FStar_Tactics_V2_Derived.goals @@ -2792,17 +2813,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (280)) + (Prims.of_int (281)) (Prims.of_int (17)) - (Prims.of_int (280)) + (Prims.of_int (281)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (281)) + (Prims.of_int (282)) (Prims.of_int (4)) - (Prims.of_int (281)) + (Prims.of_int (282)) (Prims.of_int (21))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2810,17 +2831,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (280)) + (Prims.of_int (281)) (Prims.of_int (17)) - (Prims.of_int (280)) + (Prims.of_int (281)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (280)) + (Prims.of_int (281)) (Prims.of_int (17)) - (Prims.of_int (280)) + (Prims.of_int (281)) (Prims.of_int (39))))) (Obj.magic (FStar_Tactics_SMT.get_rlimit @@ -2861,17 +2882,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (284)) - (Prims.of_int (2)) (Prims.of_int (285)) + (Prims.of_int (2)) + (Prims.of_int (286)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (287)) + (Prims.of_int (288)) (Prims.of_int (2)) - (Prims.of_int (287)) + (Prims.of_int (288)) (Prims.of_int (4))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2879,17 +2900,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (5)) - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (284)) - (Prims.of_int (2)) (Prims.of_int (285)) + (Prims.of_int (2)) + (Prims.of_int (286)) (Prims.of_int (34))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2897,17 +2918,17 @@ let (join_smt_goals : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (23)) - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (5)) - (Prims.of_int (284)) + (Prims.of_int (285)) (Prims.of_int (48))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env @@ -2992,13 +3013,13 @@ let (main : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (306)) (Prims.of_int (2)) - (Prims.of_int (306)) (Prims.of_int (27))))) + (Prims.of_int (307)) (Prims.of_int (2)) + (Prims.of_int (307)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (307)) (Prims.of_int (2)) - (Prims.of_int (317)) (Prims.of_int (5))))) + (Prims.of_int (308)) (Prims.of_int (2)) + (Prims.of_int (318)) (Prims.of_int (5))))) (Obj.magic (FStar_Tactics_V2_Builtins.set_guard_policy FStar_Tactics_Types.ForceSMT)) @@ -3009,28 +3030,28 @@ let (main : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (307)) (Prims.of_int (2)) - (Prims.of_int (308)) (Prims.of_int (73))))) + (Prims.of_int (308)) (Prims.of_int (2)) + (Prims.of_int (309)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (308)) (Prims.of_int (74)) - (Prims.of_int (317)) (Prims.of_int (5))))) + (Prims.of_int (309)) (Prims.of_int (74)) + (Prims.of_int (318)) (Prims.of_int (5))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (307)) + (Prims.of_int (308)) (Prims.of_int (5)) - (Prims.of_int (307)) + (Prims.of_int (308)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (307)) - (Prims.of_int (2)) (Prims.of_int (308)) + (Prims.of_int (2)) + (Prims.of_int (309)) (Prims.of_int (73))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3038,17 +3059,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (307)) + (Prims.of_int (308)) (Prims.of_int (5)) - (Prims.of_int (307)) + (Prims.of_int (308)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (307)) + (Prims.of_int (308)) (Prims.of_int (5)) - (Prims.of_int (307)) + (Prims.of_int (308)) (Prims.of_int (40))))) (Obj.magic (FStar_Tactics_V2_Builtins.ext_getv @@ -3067,17 +3088,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (21)) - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (4)) - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (73))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3085,17 +3106,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (41)) - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (72))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (21)) - (Prims.of_int (308)) + (Prims.of_int (309)) (Prims.of_int (73))))) (Obj.magic (FStar_Tactics_V2_Builtins.ext_getv @@ -3124,17 +3145,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (310)) + (Prims.of_int (311)) (Prims.of_int (12)) - (Prims.of_int (310)) + (Prims.of_int (311)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (2)) - (Prims.of_int (317)) + (Prims.of_int (318)) (Prims.of_int (5))))) (Obj.magic (main' t pre g expected_t)) (fun uu___3 -> @@ -3145,17 +3166,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (2)) - (Prims.of_int (316)) + (Prims.of_int (317)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (310)) + (Prims.of_int (311)) (Prims.of_int (6)) - (Prims.of_int (310)) + (Prims.of_int (311)) (Prims.of_int (9))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3163,17 +3184,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (5)) - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (2)) - (Prims.of_int (316)) + (Prims.of_int (317)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3181,17 +3202,17 @@ let (main : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (5)) - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (5)) - (Prims.of_int (312)) + (Prims.of_int (313)) (Prims.of_int (32))))) (Obj.magic (FStar_Tactics_V2_Builtins.ext_getv @@ -3237,38 +3258,38 @@ let (check_pulse_core : FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (323)) - (Prims.of_int (6)) (Prims.of_int (324)) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (324)) + (Prims.of_int (6)) (Prims.of_int (325)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic - (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (325)) - (Prims.of_int (6)) (Prims.of_int (341)) + (FStar_Range.mk_range "Pulse.Main.fst" (Prims.of_int (326)) + (Prims.of_int (6)) (Prims.of_int (342)) (Prims.of_int (36))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (323)) (Prims.of_int (9)) - (Prims.of_int (323)) (Prims.of_int (48))))) + (Prims.of_int (324)) (Prims.of_int (9)) + (Prims.of_int (324)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (323)) (Prims.of_int (6)) - (Prims.of_int (324)) (Prims.of_int (33))))) + (Prims.of_int (324)) (Prims.of_int (6)) + (Prims.of_int (325)) (Prims.of_int (33))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (323)) (Prims.of_int (9)) - (Prims.of_int (323)) (Prims.of_int (41))))) + (Prims.of_int (324)) (Prims.of_int (9)) + (Prims.of_int (324)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (323)) (Prims.of_int (9)) - (Prims.of_int (323)) (Prims.of_int (48))))) + (Prims.of_int (324)) (Prims.of_int (9)) + (Prims.of_int (324)) (Prims.of_int (48))))) (Obj.magic (FStar_Tactics_V2_Builtins.ext_getv "pulse:dump_on_failure")) @@ -3295,13 +3316,13 @@ let (check_pulse_core : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (325)) (Prims.of_int (12)) - (Prims.of_int (325)) (Prims.of_int (22))))) + (Prims.of_int (326)) (Prims.of_int (12)) + (Prims.of_int (326)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (325)) (Prims.of_int (6)) - (Prims.of_int (341)) (Prims.of_int (36))))) + (Prims.of_int (326)) (Prims.of_int (6)) + (Prims.of_int (342)) (Prims.of_int (36))))) (Obj.magic (as_decl ())) (fun uu___2 -> (fun uu___2 -> @@ -3327,17 +3348,17 @@ let (check_pulse_core : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (334)) + (Prims.of_int (335)) (Prims.of_int (10)) - (Prims.of_int (338)) + (Prims.of_int (339)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (340)) - (Prims.of_int (8)) (Prims.of_int (341)) + (Prims.of_int (8)) + (Prims.of_int (342)) (Prims.of_int (36))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3345,9 +3366,9 @@ let (check_pulse_core : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (19)) - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (74))))) (FStar_Sealed.seal (Obj.magic @@ -3363,17 +3384,17 @@ let (check_pulse_core : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (19)) - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (74))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (19)) - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (74))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3381,9 +3402,9 @@ let (check_pulse_core : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (44)) - (Prims.of_int (335)) + (Prims.of_int (336)) (Prims.of_int (69))))) (FStar_Sealed.seal (Obj.magic @@ -3432,17 +3453,17 @@ let (check_pulse_core : (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (340)) + (Prims.of_int (341)) (Prims.of_int (8)) - (Prims.of_int (340)) + (Prims.of_int (341)) (Prims.of_int (24))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Main.fst" - (Prims.of_int (341)) + (Prims.of_int (342)) (Prims.of_int (8)) - (Prims.of_int (341)) + (Prims.of_int (342)) (Prims.of_int (36))))) (Obj.magic (FStar_Tactics_V2_Builtins.log_issues