From 8b42079ca228f5bd483c042f5f7d23513cbb3bea Mon Sep 17 00:00:00 2001 From: Aseem Rastogi Date: Tue, 25 Jul 2023 12:49:11 +0000 Subject: [PATCH] snap --- share/steel/examples/pulse/CustomSyntax.fst | 718 ++++++------ .../plugin/generated/Pulse_Checker_Base.ml | 1003 +++++------------ .../plugin/generated/Pulse_Checker_If.ml | 225 ++-- .../plugin/generated/Pulse_Checker_Match.ml | 264 ++--- .../generated/Pulse_Typing_Combinators.ml | 2 +- 5 files changed, 825 insertions(+), 1387 deletions(-) diff --git a/share/steel/examples/pulse/CustomSyntax.fst b/share/steel/examples/pulse/CustomSyntax.fst index 789c31c7b..09b80e821 100755 --- a/share/steel/examples/pulse/CustomSyntax.fst +++ b/share/steel/examples/pulse/CustomSyntax.fst @@ -12,417 +12,399 @@ open Pulse.Steel.Wrapper #push-options "--using_facts_from 'Prims FStar.Pervasives FStar.UInt FStar.UInt32 FStar.Ghost Pulse.Steel.Wrapper CustomSyntax'" #push-options "--ide_id_info_off" +assume val p : vprop +assume val g : unit -> stt unit emp (fun _ -> p) + +let folded_pts_to (r:ref U32.t) (n:erased U32.t) : vprop = pts_to r full_perm n + ```pulse -fn test_write_10 (x:ref U32.t) +fn unfold_test (r:ref U32.t) (n:erased U32.t) + requires folded_pts_to r n + ensures folded_pts_to r n +{ + with n. unfold (folded_pts_to r n); + with n. fold (folded_pts_to r n) +} +``` +```pulse +fn test_write_10 (x:ref U32.t) (#n:erased U32.t) - requires pts_to x full_perm n - ensures pts_to x full_perm 0ul - { - x := 1ul; - - x := 2ul; - + x := 0ul; } ``` -// assume val p : vprop -// assume val g : unit -> stt unit emp (fun _ -> p) - -// let folded_pts_to (r:ref U32.t) (n:erased U32.t) : vprop = pts_to r full_perm n - -// ```pulse -// fn unfold_test (r:ref U32.t) (n:erased U32.t) -// requires folded_pts_to r n -// ensures folded_pts_to r n -// { -// with n. unfold (folded_pts_to r n); -// with n. fold (folded_pts_to r n) -// } -// ``` - -// ```pulse -// fn test_write_10 (x:ref U32.t) -// (#n:erased U32.t) -// requires pts_to x full_perm n -// ensures pts_to x full_perm 0ul -// { -// x := 1ul; -// x := 0ul; -// } -// ``` - -// ```pulse -// fn test_read (r:ref U32.t) -// (#n:erased U32.t) -// (#p:perm) -// requires pts_to r p n -// returns x : U32.t -// ensures pts_to r p x -// { -// !r -// } -// ``` +```pulse +fn test_read (r:ref U32.t) + (#n:erased U32.t) + (#p:perm) + requires pts_to r p n + returns x : U32.t + ensures pts_to r p x +{ + !r +} +``` -// ```pulse -// fn swap (r1 r2:ref U32.t) -// (#n1 #n2:erased U32.t) -// requires -// (pts_to r1 full_perm n1 `star` -// pts_to r2 full_perm n2) -// ensures -// (pts_to r1 full_perm n2 `star` -// pts_to r2 full_perm n1) -// { -// let x = !r1; -// let y = !r2; -// r1 := y; -// r2 := x -// } -// ``` +```pulse +fn swap (r1 r2:ref U32.t) + (#n1 #n2:erased U32.t) + requires + (pts_to r1 full_perm n1 `star` + pts_to r2 full_perm n2) + ensures + (pts_to r1 full_perm n2 `star` + pts_to r2 full_perm n1) +{ + let x = !r1; + let y = !r2; + r1 := y; + r2 := x +} +``` -// ```pulse -// fn call_swap2 (r1 r2:ref U32.t) -// (#n1 #n2:erased U32.t) -// requires -// (pts_to r1 full_perm n1 `star` -// pts_to r2 full_perm n2) -// ensures -// (pts_to r1 full_perm n1 `star` -// pts_to r2 full_perm n2) -// { -// swap r1 r2; -// swap r1 r2 -// } -// ``` +```pulse +fn call_swap2 (r1 r2:ref U32.t) + (#n1 #n2:erased U32.t) + requires + (pts_to r1 full_perm n1 `star` + pts_to r2 full_perm n2) + ensures + (pts_to r1 full_perm n1 `star` + pts_to r2 full_perm n2) +{ + swap r1 r2; + swap r1 r2 +} +``` -// ```pulse -// fn swap_with_elim_pure (r1 r2:ref U32.t) -// (#n1 #n2:erased U32.t) -// requires -// (pts_to r1 full_perm n1 `star` -// pts_to r2 full_perm n2) -// ensures -// (pts_to r1 full_perm n2 `star` -// pts_to r2 full_perm n1) -// { -// let x = !r1; -// let y = !r2; -// r1 := y; -// r2 := x -// } -// ``` +```pulse +fn swap_with_elim_pure (r1 r2:ref U32.t) + (#n1 #n2:erased U32.t) + requires + (pts_to r1 full_perm n1 `star` + pts_to r2 full_perm n2) + ensures + (pts_to r1 full_perm n2 `star` + pts_to r2 full_perm n1) +{ + let x = !r1; + let y = !r2; + r1 := y; + r2 := x +} +``` -// ```pulse -// fn intro_pure_example (r:ref U32.t) -// (#n1 #n2:erased U32.t) -// requires -// (pts_to r full_perm n1 `star` -// pure (reveal n1 == reveal n2)) -// ensures -// (pts_to r full_perm n2 `star` -// pure (reveal n2 == reveal n1)) -// { -// () -// } -// ``` +```pulse +fn intro_pure_example (r:ref U32.t) + (#n1 #n2:erased U32.t) + requires + (pts_to r full_perm n1 `star` + pure (reveal n1 == reveal n2)) + ensures + (pts_to r full_perm n2 `star` + pure (reveal n2 == reveal n1)) +{ + () +} +``` -// ```pulse -// fn if_example (r:ref U32.t) -// (n:(n:erased U32.t{U32.v (reveal n) == 1})) -// (b:bool) -// requires -// pts_to r full_perm n -// ensures -// pts_to r full_perm (U32.add (reveal n) 2ul) -// { -// let x = read_atomic r; -// if b -// { -// r := U32.add x 2ul -// } -// else -// { -// write_atomic r 3ul -// } -// } -// ``` +```pulse +fn if_example (r:ref U32.t) + (n:(n:erased U32.t{U32.v (reveal n) == 1})) + (b:bool) + requires + pts_to r full_perm n + ensures + pts_to r full_perm (U32.add (reveal n) 2ul) +{ + let x = read_atomic r; + if b + { + r := U32.add x 2ul + } + else + { + write_atomic r 3ul + } +} +``` -// ```pulse -// ghost -// fn elim_intro_exists2 (r:ref U32.t) -// requires -// exists n. pts_to r full_perm n -// ensures -// exists n. pts_to r full_perm n -// { -// introduce exists n. pts_to r full_perm n with _ -// } -// ``` +```pulse +ghost +fn elim_intro_exists2 (r:ref U32.t) + requires + exists n. pts_to r full_perm n + ensures + exists n. pts_to r full_perm n +{ + introduce exists n. pts_to r full_perm n with _ +} +``` -// assume -// val pred (b:bool) : vprop -// assume -// val read_pred (_:unit) (#b:erased bool) -// : stt bool (pred b) (fun r -> pred r) +assume +val pred (b:bool) : vprop +assume +val read_pred (_:unit) (#b:erased bool) + : stt bool (pred b) (fun r -> pred r) -// ```pulse -// fn while_test_alt (r:ref U32.t) -// requires -// exists b n. -// (pts_to r full_perm n `star` -// pred b) -// ensures -// exists n. (pts_to r full_perm n `star` -// pred false) -// { -// while (read_pred ()) -// invariant b . exists n. (pts_to r full_perm n `star` pred b) -// { -// () -// } -// } -// ``` +```pulse +fn while_test_alt (r:ref U32.t) + requires + exists b n. + (pts_to r full_perm n `star` + pred b) + ensures + exists n. (pts_to r full_perm n `star` + pred false) +{ + while (read_pred ()) + invariant b . exists n. (pts_to r full_perm n `star` pred b) + { + () + } +} +``` -// ```pulse -// fn infer_read_ex (r:ref U32.t) -// requires -// exists n. pts_to r full_perm n -// ensures exists n. pts_to r full_perm n -// { -// let x = !r; -// () -// } -// ``` +```pulse +fn infer_read_ex (r:ref U32.t) + requires + exists n. pts_to r full_perm n + ensures exists n. pts_to r full_perm n +{ + let x = !r; + () +} +``` -// ```pulse -// fn while_count2 (r:ref U32.t) -// requires exists (n:U32.t). (pts_to r full_perm n) -// ensures (pts_to r full_perm 10ul) -// { -// open FStar.UInt32; -// while (let x = !r; (x <> 10ul)) -// invariant b. -// exists n. (pts_to r full_perm n `star` -// pure (b == (n <> 10ul))) -// { -// let x = !r; -// if (x <^ 10ul) -// { -// r := x +^ 1ul -// } -// else -// { -// r := x -^ 1ul -// } -// } -// } -// ``` +```pulse +fn while_count2 (r:ref U32.t) + requires exists (n:U32.t). (pts_to r full_perm n) + ensures (pts_to r full_perm 10ul) +{ + open FStar.UInt32; + while (let x = !r; (x <> 10ul)) + invariant b. + exists n. (pts_to r full_perm n `star` + pure (b == (n <> 10ul))) + { + let x = !r; + if (x <^ 10ul) + { + r := x +^ 1ul + } + else + { + r := x -^ 1ul + } + } +} +``` -// ```pulse -// fn test_par (r1 r2:ref U32.t) -// (#n1 #n2:erased U32.t) -// requires -// (pts_to r1 full_perm n1 `star` -// pts_to r2 full_perm n2) -// ensures -// (pts_to r1 full_perm 1ul `star` -// pts_to r2 full_perm 1ul) -// { -// parallel -// requires (pts_to r1 full_perm n1) -// and (pts_to r2 full_perm n2) -// ensures (pts_to r1 full_perm 1ul) -// and (pts_to r2 full_perm 1ul) -// { -// r1 := 1ul -// } -// { -// r2 := 1ul -// }; -// () -// } -// ``` +```pulse +fn test_par (r1 r2:ref U32.t) + (#n1 #n2:erased U32.t) + requires + (pts_to r1 full_perm n1 `star` + pts_to r2 full_perm n2) + ensures + (pts_to r1 full_perm 1ul `star` + pts_to r2 full_perm 1ul) +{ + parallel + requires (pts_to r1 full_perm n1) + and (pts_to r2 full_perm n2) + ensures (pts_to r1 full_perm 1ul) + and (pts_to r2 full_perm 1ul) + { + r1 := 1ul + } + { + r2 := 1ul + }; + () +} +``` -// // A test for rewrite -// let mpts_to (r:ref U32.t) (n:erased U32.t) : vprop = pts_to r full_perm n +// A test for rewrite +let mpts_to (r:ref U32.t) (n:erased U32.t) : vprop = pts_to r full_perm n -// ```pulse -// fn rewrite_test (r:ref U32.t) -// (#n:erased U32.t) -// requires (mpts_to r n) -// ensures (mpts_to r 1ul) -// { -// rewrite (mpts_to r n) -// as (pts_to r full_perm n); -// r := 1ul; -// rewrite (pts_to r full_perm 1ul) -// as (mpts_to r 1ul) -// } -// ``` +```pulse +fn rewrite_test (r:ref U32.t) + (#n:erased U32.t) + requires (mpts_to r n) + ensures (mpts_to r 1ul) +{ + rewrite (mpts_to r n) + as (pts_to r full_perm n); + r := 1ul; + rewrite (pts_to r full_perm 1ul) + as (mpts_to r 1ul) +} +``` -// ```pulse -// fn test_local (r:ref U32.t) -// (#n:erased U32.t) -// requires (pts_to r full_perm n) -// ensures (pts_to r full_perm 0ul) -// { -// let mut x = 0ul; -// let y = !x; -// r := y -// } -// ``` +```pulse +fn test_local (r:ref U32.t) + (#n:erased U32.t) + requires (pts_to r full_perm n) + ensures (pts_to r full_perm 0ul) +{ + let mut x = 0ul; + let y = !x; + r := y +} +``` -// ```pulse -// fn count_local (r:ref int) (n:int) -// requires (pts_to r full_perm (hide 0)) -// ensures (pts_to r full_perm n) -// { -// let mut i = 0; -// while -// (let m = !i; (m <> n)) -// invariant b. exists m. -// (pts_to i full_perm m `star` -// pure (b == (m <> n))) -// { -// let m = !i; -// i := m + 1 -// }; -// let x = !i; -// r := x -// } -// ``` +```pulse +fn count_local (r:ref int) (n:int) + requires (pts_to r full_perm (hide 0)) + ensures (pts_to r full_perm n) +{ + let mut i = 0; + while + (let m = !i; (m <> n)) + invariant b. exists m. + (pts_to i full_perm m `star` + pure (b == (m <> n))) + { + let m = !i; + i := m + 1 + }; + let x = !i; + r := x +} +``` -// let rec sum_spec (n:nat) : nat = -// if n = 0 then 0 else n + sum_spec (n - 1) +let rec sum_spec (n:nat) : nat = + if n = 0 then 0 else n + sum_spec (n - 1) -// let zero : nat = 0 +let zero : nat = 0 -// ```pulse -// fn sum (r:ref nat) (n:nat) -// requires exists i. (pts_to r full_perm i) -// ensures (pts_to r full_perm (sum_spec n)) -// { -// let mut i = zero; -// let mut sum = zero; -// introduce exists b m s. ( -// pts_to i full_perm m `star` -// pts_to sum full_perm s `star` -// pure (s == sum_spec m /\ -// b == (m <> n))) -// with (zero <> n); +```pulse +fn sum (r:ref nat) (n:nat) + requires exists i. (pts_to r full_perm i) + ensures (pts_to r full_perm (sum_spec n)) +{ + let mut i = zero; + let mut sum = zero; + introduce exists b m s. ( + pts_to i full_perm m `star` + pts_to sum full_perm s `star` + pure (s == sum_spec m /\ + b == (m <> n))) + with (zero <> n); -// while (let m = !i; (m <> n)) -// invariant b . exists m s. ( -// pts_to i full_perm m `star` -// pts_to sum full_perm s `star` -// pure (s == sum_spec m /\ -// b == (m <> n))) -// { -// let m = !i; -// let s = !sum; -// i := (m + 1); -// sum := s + m + 1; -// introduce exists b m s. ( -// pts_to i full_perm m `star` -// pts_to sum full_perm s `star` -// pure (s == sum_spec m /\ -// b == (m <> n))) -// with (m + 1 <> n) -// }; -// let s = !sum; -// r := s; -// introduce exists m. (pts_to i full_perm m) -// with _; -// introduce exists s. (pts_to sum full_perm s) -// with _ -// } -// ``` + while (let m = !i; (m <> n)) + invariant b . exists m s. ( + pts_to i full_perm m `star` + pts_to sum full_perm s `star` + pure (s == sum_spec m /\ + b == (m <> n))) + { + let m = !i; + let s = !sum; + i := (m + 1); + sum := s + m + 1; + introduce exists b m s. ( + pts_to i full_perm m `star` + pts_to sum full_perm s `star` + pure (s == sum_spec m /\ + b == (m <> n))) + with (m + 1 <> n) + }; + let s = !sum; + r := s; + introduce exists m. (pts_to i full_perm m) + with _; + introduce exists s. (pts_to sum full_perm s) + with _ +} +``` -// ```pulse -// fn sum2 (r:ref nat) (n:nat) -// requires exists i. pts_to r full_perm i -// ensures pts_to r full_perm (sum_spec n) -// { -// let mut i = zero; -// let mut sum = zero; -// while (let m = !i; (m <> n)) -// invariant b . exists m s. -// pts_to i full_perm m ** -// pts_to sum full_perm s ** -// pure (s == sum_spec m /\ b == (m <> n)) -// { -// let m = !i; -// let s = !sum; -// i := (m + 1); -// sum := s + m + 1; -// () -// }; -// let s = !sum; -// r := s; -// () -// } -// ``` +```pulse +fn sum2 (r:ref nat) (n:nat) + requires exists i. pts_to r full_perm i + ensures pts_to r full_perm (sum_spec n) +{ + let mut i = zero; + let mut sum = zero; + while (let m = !i; (m <> n)) + invariant b . exists m s. + pts_to i full_perm m ** + pts_to sum full_perm s ** + pure (s == sum_spec m /\ b == (m <> n)) + { + let m = !i; + let s = !sum; + i := (m + 1); + sum := s + m + 1; + () + }; + let s = !sum; + r := s; + () +} +``` + +```pulse +fn if_then_else_in_specs (r:ref U32.t) + requires `@(if true + then pts_to r full_perm 0ul + else pts_to r full_perm 1ul) + ensures `@(if true + then pts_to r full_perm 1ul + else pts_to r full_perm 0ul) +{ + // need this for typechecking !r on the next line, + // with inference of implicits + rewrite `@(if true then pts_to r full_perm 0ul else pts_to r full_perm 1ul) + as (pts_to r full_perm 0ul); + let x = !r; + r := U32.add x 1ul +} +``` +```pulse +fn test_tot_let (r:ref U32.t) + requires (pts_to r full_perm 0ul) + ensures (pts_to r full_perm 2ul) +{ + let x = 1ul; + let y = 1ul; + r := U32.add x y +} +``` + +// Ascriptions coming in the way // ```pulse -// fn if_then_else_in_specs (r:ref U32.t) -// requires `@(if true -// then pts_to r full_perm 0ul -// else pts_to r full_perm 1ul) -// ensures `@(if true -// then pts_to r full_perm 1ul -// else pts_to r full_perm 0ul) +// fn if_then_else_in_specs2 (r:ref U32.t) (b:bool) +// requires (pts_to r full_perm (if b then 0ul else 1ul)) +// ensures (pts_to r full_perm (if b then 1ul else 2ul)) // { -// // need this for typechecking !r on the next line, -// // with inference of implicits -// rewrite `@(if true then pts_to r full_perm 0ul else pts_to r full_perm 1ul) -// as (pts_to r full_perm 0ul); // let x = !r; // r := U32.add x 1ul // } // ``` -// ```pulse -// fn test_tot_let (r:ref U32.t) -// requires (pts_to r full_perm 0ul) -// ensures (pts_to r full_perm 2ul) -// { -// let x = 1ul; -// let y = 1ul; -// r := U32.add x y -// } -// ``` - -// // Ascriptions coming in the way -// // ```pulse -// // fn if_then_else_in_specs2 (r:ref U32.t) (b:bool) -// // requires (pts_to r full_perm (if b then 0ul else 1ul)) -// // ensures (pts_to r full_perm (if b then 1ul else 2ul)) -// // { -// // let x = !r; -// // r := U32.add x 1ul -// // } -// // ``` - -// ```pulse -// fn incr (x:nat) -// requires emp -// returns r : (r:nat { r > x }) -// ensures emp -// { -// let y = x + 1; -// ( y <: r:nat { r > x } ) -// } -// ``` +```pulse +fn incr (x:nat) + requires emp + returns r : (r:nat { r > x }) + ensures emp +{ + let y = x + 1; + ( y <: r:nat { r > x } ) +} +``` diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Base.ml b/src/ocaml/plugin/generated/Pulse_Checker_Base.ml index 69d95daa7..1a9911f3e 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Base.ml @@ -635,7 +635,7 @@ let (k_elab_equiv_continutation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" (Prims.of_int (138)) (Prims.of_int (4)) - (Prims.of_int (148)) (Prims.of_int (34))))) + (Prims.of_int (146)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> FStar_Pervasives.Mkdtuple3 @@ -658,8 +658,8 @@ let (k_elab_equiv_continutation : "Pulse.Checker.Base.fst" (Prims.of_int (138)) (Prims.of_int (4)) - (Prims.of_int (148)) - (Prims.of_int (34))))) + (Prims.of_int (146)) + (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> res)) (fun uu___ -> @@ -667,86 +667,72 @@ let (k_elab_equiv_continutation : match uu___ with | FStar_Pervasives.Mkdtuple3 (st, c, st_d) -> - if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp - c) - then - Obj.magic - (k post_hint - (FStar_Pervasives.Mkdtuple3 - (st, c, st_d))) - else - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (143)) - (Prims.of_int (18)) - (Prims.of_int (143)) - (Prims.of_int (95))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (141)) - (Prims.of_int (6)) - (Prims.of_int (148)) - (Prims.of_int (34))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Pulse_Typing_Metatheory.st_comp_typing_inversion - g2 - (Pulse_Syntax_Base.st_comp_of_comp - c) - (Pulse_Typing_Metatheory.comp_typing_inversion - g2 c - (Pulse_Typing_Metatheory.st_typing_correctness - g2 st c st_d)))) - (fun uu___2 -> - (fun uu___2 -> - match uu___2 with - | FStar_Pervasives.Mkdtuple4 - (uu___3, - pre_typing, - uu___4, uu___5) - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - ( - Obj.magic + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Base.fst" + (Prims.of_int (141)) + (Prims.of_int (16)) + (Prims.of_int (141)) + (Prims.of_int (93))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "Pulse.Checker.Base.fst" + (Prims.of_int (139)) + (Prims.of_int (32)) + (Prims.of_int (146)) + (Prims.of_int (32))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> + Pulse_Typing_Metatheory.st_comp_typing_inversion + g2 + (Pulse_Syntax_Base.st_comp_of_comp + c) + (Pulse_Typing_Metatheory.comp_typing_inversion + g2 c + (Pulse_Typing_Metatheory.st_typing_correctness + g2 st c st_d)))) + (fun uu___1 -> + (fun uu___1 -> + match uu___1 with + | FStar_Pervasives.Mkdtuple4 + (uu___2, + pre_typing, + uu___3, uu___4) + -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (145)) - (Prims.of_int (6)) - (Prims.of_int (145)) - (Prims.of_int (73))))) - (FStar_Sealed.seal - ( - Obj.magic + (Prims.of_int (143)) + (Prims.of_int (4)) + (Prims.of_int (143)) + (Prims.of_int (71))))) + (FStar_Sealed.seal + (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (143)) - (Prims.of_int (99)) - (Prims.of_int (148)) - (Prims.of_int (34))))) - (FStar_Tactics_Effect.lift_div_tac - ( - fun - uu___6 -> + (Prims.of_int (141)) + (Prims.of_int (97)) + (Prims.of_int (146)) + (Prims.of_int (32))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___5 + -> Pulse_Typing_Combinators.apply_frame g2 st ctxt1 () c st_d framing_token)) - (fun uu___6 + (fun uu___5 -> + (fun uu___5 -> - (fun - uu___6 -> - match uu___6 + match uu___5 with | Prims.Mkdtuple2 @@ -758,28 +744,28 @@ let (k_elab_equiv_continutation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (147)) - (Prims.of_int (16)) - (Prims.of_int (147)) - (Prims.of_int (49))))) + (Prims.of_int (145)) + (Prims.of_int (14)) + (Prims.of_int (145)) + (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (148)) - (Prims.of_int (4)) - (Prims.of_int (148)) - (Prims.of_int (34))))) + (Prims.of_int (146)) + (Prims.of_int (2)) + (Prims.of_int (146)) + (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___7 -> + uu___6 -> simplify_post g2 st c' st_d' (Pulse_Syntax_Base.comp_post c))) (fun - uu___7 -> + uu___6 -> (fun st_d'1 -> Obj.magic @@ -792,10 +778,9 @@ let (k_elab_equiv_continutation : (Pulse_Syntax_Base.comp_post c)), st_d'1)))) - uu___7))) uu___6))) - uu___2))) uu___))) - uu___) + uu___5))) + uu___1))) uu___))) uu___) let (k_elab_equiv_prefix : Pulse_Typing_Env.env -> @@ -819,13 +804,13 @@ let (k_elab_equiv_prefix : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (164)) (Prims.of_int (60)) - (Prims.of_int (166)) (Prims.of_int (31))))) + (Prims.of_int (162)) (Prims.of_int (60)) + (Prims.of_int (164)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (167)) (Prims.of_int (4)) - (Prims.of_int (182)) (Prims.of_int (11))))) + (Prims.of_int (165)) (Prims.of_int (4)) + (Prims.of_int (179)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> FStar_Pervasives.Mkdtuple3 @@ -838,18 +823,18 @@ let (k_elab_equiv_prefix : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (168)) + (Prims.of_int (166)) (Prims.of_int (12)) - (Prims.of_int (168)) + (Prims.of_int (166)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (168)) + (Prims.of_int (166)) (Prims.of_int (30)) - (Prims.of_int (182)) - (Prims.of_int (11))))) + (Prims.of_int (179)) + (Prims.of_int (5))))) (Obj.magic (k post_hint res)) (fun res1 -> FStar_Tactics_Effect.lift_div_tac @@ -857,45 +842,35 @@ let (k_elab_equiv_prefix : match res1 with | FStar_Pervasives.Mkdtuple3 (st, c, st_d) -> - if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp - c) - then - FStar_Pervasives.Mkdtuple3 - (st, c, st_d) - else - (match Pulse_Typing_Metatheory.st_comp_typing_inversion - g1 - (Pulse_Syntax_Base.st_comp_of_comp - c) - (Pulse_Typing_Metatheory.comp_typing_inversion - g1 c - (Pulse_Typing_Metatheory.st_typing_correctness - g1 st c st_d)) - with - | FStar_Pervasives.Mkdtuple4 - (uu___2, pre_typing, - uu___3, uu___4) - -> - (match Pulse_Typing_Combinators.apply_frame - g1 st ctxt2 () c - st_d - framing_token - with - | Prims.Mkdtuple2 - (c', st_d') -> - FStar_Pervasives.Mkdtuple3 - (st, - (comp_st_with_post - c' - (Pulse_Syntax_Base.comp_post - c)), - (simplify_post - g1 st c' - st_d' - (Pulse_Syntax_Base.comp_post - c))))))))) + (match Pulse_Typing_Metatheory.st_comp_typing_inversion + g1 + (Pulse_Syntax_Base.st_comp_of_comp + c) + (Pulse_Typing_Metatheory.comp_typing_inversion + g1 c + (Pulse_Typing_Metatheory.st_typing_correctness + g1 st c st_d)) + with + | FStar_Pervasives.Mkdtuple4 + (uu___1, pre_typing, + uu___2, uu___3) + -> + (match Pulse_Typing_Combinators.apply_frame + g1 st ctxt2 () c + st_d framing_token + with + | Prims.Mkdtuple2 + (c', st_d') -> + FStar_Pervasives.Mkdtuple3 + (st, + (comp_st_with_post + c' + (Pulse_Syntax_Base.comp_post + c)), + (simplify_post g1 + st c' st_d' + (Pulse_Syntax_Base.comp_post + c))))))))) uu___) let (k_elab_equiv : Pulse_Typing_Env.env -> @@ -981,17 +956,17 @@ let (continuation_elaborator_with_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (228)) + (Prims.of_int (225)) (Prims.of_int (34)) - (Prims.of_int (228)) + (Prims.of_int (225)) (Prims.of_int (37))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (227)) + (Prims.of_int (224)) (Prims.of_int (24)) - (Prims.of_int (263)) + (Prims.of_int (253)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___3 -> res)) @@ -1003,155 +978,30 @@ let (continuation_elaborator_with_bind : (e2, c2, e2_typing) -> - if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp - c2) - then - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (231)) - (Prims.of_int (11)) - (Prims.of_int (233)) - (Prims.of_int (36))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (230)) - (Prims.of_int (9)) - (Prims.of_int (233)) - (Prims.of_int (36))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (233)) - (Prims.of_int (14)) - (Prims.of_int (233)) - (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (231)) - (Prims.of_int (11)) - (Prims.of_int (233)) - (Prims.of_int (36))))) - (Obj.magic - (Pulse_Syntax_Printer.comp_to_string - c2)) - (fun - uu___4 -> - (fun - uu___4 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (231)) - (Prims.of_int (11)) - (Prims.of_int (233)) - (Prims.of_int (36))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (231)) - (Prims.of_int (11)) - (Prims.of_int (233)) - (Prims.of_int (36))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind + Obj.magic + (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (232)) - (Prims.of_int (14)) - (Prims.of_int (232)) - (Prims.of_int (38))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Printf.fst" - (Prims.of_int (121)) - (Prims.of_int (8)) - (Prims.of_int (123)) - (Prims.of_int (44))))) - (Obj.magic - (Pulse_Syntax_Printer.st_term_to_string - e2)) - (fun - uu___5 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___6 -> - fun x1 -> - Prims.strcat - (Prims.strcat - "bind elaborator: continuation term " - (Prims.strcat - uu___5 - " is not stateful (c: ")) - (Prims.strcat - x1 ")"))))) - (fun - uu___5 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___6 -> - uu___5 - uu___4)))) - uu___4))) - (fun - uu___4 -> - (fun - uu___4 -> - Obj.magic - (Pulse_Typing_Env.fail - (Pulse_Typing_Env.push_binding - g x - Pulse_Syntax_Base.ppname_default - (Pulse_Syntax_Base.comp_res - c1)) - (FStar_Pervasives_Native.Some - (e2.Pulse_Syntax_Base.range2)) - uu___4)) - uu___4)) - else - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (235)) - (Prims.of_int (43)) - (Prims.of_int (235)) - (Prims.of_int (52))))) + (Prims.of_int (226)) + (Prims.of_int (41)) + (Prims.of_int (226)) + (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (235)) - (Prims.of_int (55)) - (Prims.of_int (262)) - (Prims.of_int (7))))) + (Prims.of_int (226)) + (Prims.of_int (53)) + (Prims.of_int (253)) + (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___5 -> + uu___4 -> e2_typing)) (fun - uu___5 -> + uu___4 -> (fun e2_typing1 -> @@ -1161,25 +1011,25 @@ let (continuation_elaborator_with_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (236)) - (Prims.of_int (22)) - (Prims.of_int (236)) - (Prims.of_int (40))))) + (Prims.of_int (227)) + (Prims.of_int (20)) + (Prims.of_int (227)) + (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (247)) - (Prims.of_int (6)) - (Prims.of_int (262)) - (Prims.of_int (7))))) + (Prims.of_int (238)) + (Prims.of_int (4)) + (Prims.of_int (253)) + (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun - uu___5 -> + uu___4 -> Pulse_Syntax_Naming.close_st_term e2 x)) (fun - uu___5 -> + uu___4 -> (fun e2_closed -> @@ -1206,18 +1056,18 @@ let (continuation_elaborator_with_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (251)) - (Prims.of_int (10)) - (Prims.of_int (251)) - (Prims.of_int (94))))) + (Prims.of_int (242)) + (Prims.of_int (8)) + (Prims.of_int (242)) + (Prims.of_int (92))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (249)) - (Prims.of_int (11)) - (Prims.of_int (262)) - (Prims.of_int (7))))) + (Prims.of_int (240)) + (Prims.of_int (9)) + (Prims.of_int (253)) + (Prims.of_int (5))))) (Obj.magic (Pulse_Typing_Combinators.bind_res_and_post_typing g @@ -1225,10 +1075,10 @@ let (continuation_elaborator_with_bind : c2) x post_hint)) (fun - uu___6 -> + uu___5 -> (fun - uu___6 -> - match uu___6 + uu___5 -> + match uu___5 with | (t_typing, @@ -1240,18 +1090,18 @@ let (continuation_elaborator_with_bind : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (253)) - (Prims.of_int (10)) - (Prims.of_int (259)) - (Prims.of_int (23))))) + (Prims.of_int (244)) + (Prims.of_int (8)) + (Prims.of_int (250)) + (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (251)) - (Prims.of_int (97)) - (Prims.of_int (261)) - (Prims.of_int (28))))) + (Prims.of_int (242)) + (Prims.of_int (95)) + (Prims.of_int (252)) + (Prims.of_int (26))))) (Obj.magic (Pulse_Typing_Combinators.mk_bind g @@ -1268,11 +1118,11 @@ let (continuation_elaborator_with_bind : e2_typing1 () ())) (fun - uu___7 -> + uu___6 -> FStar_Tactics_Effect.lift_div_tac (fun - uu___8 -> - match uu___7 + uu___7 -> + match uu___6 with | FStar_Pervasives.Mkdtuple3 @@ -1282,9 +1132,9 @@ let (continuation_elaborator_with_bind : FStar_Pervasives.Mkdtuple3 (e, c, e_typing))))) - uu___6))) - uu___5))) uu___5))) + uu___4))) + uu___4))) uu___3)))))) uu___6 uu___5 uu___4 uu___3 uu___2 uu___1 uu___ let (continuation_elaborator_with_tot_bind : @@ -1315,177 +1165,37 @@ let (continuation_elaborator_with_tot_bind : Obj.magic (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> - fun post_hint -> - fun uu___1 -> - match uu___1 with - | FStar_Pervasives.Mkdtuple3 - (e2, c2, d2) -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (283)) - (Prims.of_int (2)) - (Prims.of_int (287)) - (Prims.of_int (36))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (318)) - (Prims.of_int (2)) - (Prims.of_int (318)) - (Prims.of_int (15))))) - (if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp - c2) - then - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (285)) - (Prims.of_int (11)) - (Prims.of_int (287)) - (Prims.of_int (36))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (284)) - (Prims.of_int (7)) - (Prims.of_int (287)) - (Prims.of_int (36))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (287)) - (Prims.of_int (14)) - (Prims.of_int (287)) - (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (285)) - (Prims.of_int (11)) - (Prims.of_int (287)) - (Prims.of_int (36))))) - (Obj.magic - (Pulse_Syntax_Printer.comp_to_string - c2)) - (fun uu___2 - -> - (fun - uu___2 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (285)) - (Prims.of_int (11)) - (Prims.of_int (287)) - (Prims.of_int (36))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (285)) - (Prims.of_int (11)) - (Prims.of_int (287)) - (Prims.of_int (36))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (286)) - (Prims.of_int (14)) - (Prims.of_int (286)) - (Prims.of_int (38))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Printf.fst" - (Prims.of_int (121)) - (Prims.of_int (8)) - (Prims.of_int (123)) - (Prims.of_int (44))))) - (Obj.magic - (Pulse_Syntax_Printer.st_term_to_string - e2)) - (fun - uu___3 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> - fun x1 -> - Prims.strcat - (Prims.strcat - "tot bind elaborator: continuation term " - (Prims.strcat - uu___3 - " is not stateful (c: ")) - (Prims.strcat - x1 ")"))))) - (fun - uu___3 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> - uu___3 - uu___2)))) - uu___2))) - (fun uu___2 -> - (fun uu___2 -> - Obj.magic - ( - Pulse_Typing_Env.fail - g - (FStar_Pervasives_Native.Some - (e2.Pulse_Syntax_Base.range2)) - uu___2)) - uu___2))) - else - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> ())))) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> - FStar_Pervasives.Mkdtuple3 - ((Pulse_Typing.wr - (Pulse_Syntax_Base.Tm_TotBind - { + (fun uu___ -> + fun post_hint -> + fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + match uu___1 with + | FStar_Pervasives.Mkdtuple3 + (e2, c2, d2) -> + FStar_Pervasives.Mkdtuple3 + ((Pulse_Typing.wr + (Pulse_Syntax_Base.Tm_TotBind + { Pulse_Syntax_Base.head2 = e1; Pulse_Syntax_Base.body2 = (Pulse_Syntax_Naming.close_st_term e2 x) - })), - (Pulse_Syntax_Naming.open_comp_with - (Pulse_Syntax_Naming.close_comp - c2 x) e1), - (Pulse_Typing.T_TotBind - (g, e1, - (Pulse_Syntax_Naming.close_st_term + })), + (Pulse_Syntax_Naming.open_comp_with + (Pulse_Syntax_Naming.close_comp + c2 x) e1), + (Pulse_Typing.T_TotBind + (g, e1, + (Pulse_Syntax_Naming.close_st_term e2 x), - t1, c2, x, - (), d2)))))))) - uu___6 uu___5 uu___4 uu___3 uu___2 uu___1 uu___ + t1, c2, x, + (), d2)))))) + uu___))) uu___6 uu___5 uu___4 uu___3 + uu___2 uu___1 uu___ let rec (check_equiv_emp : Pulse_Typing_Env.env -> Pulse_Syntax_Base.term -> unit FStar_Pervasives_Native.option) @@ -1533,13 +1243,13 @@ let (intro_comp_typing : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (347)) (Prims.of_int (8)) - (Prims.of_int (347)) (Prims.of_int (52))))) + (Prims.of_int (330)) (Prims.of_int (8)) + (Prims.of_int (330)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (349)) (Prims.of_int (4)) - (Prims.of_int (364)) (Prims.of_int (44))))) + (Prims.of_int (332)) (Prims.of_int (4)) + (Prims.of_int (347)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> fun uu___ -> @@ -1560,17 +1270,17 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (351)) + (Prims.of_int (334)) (Prims.of_int (16)) - (Prims.of_int (351)) + (Prims.of_int (334)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (352)) + (Prims.of_int (335)) (Prims.of_int (6)) - (Prims.of_int (352)) + (Prims.of_int (335)) (Prims.of_int (19))))) (Obj.magic (intro_st_comp_typing st)) (fun stc -> @@ -1584,17 +1294,17 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (354)) + (Prims.of_int (337)) (Prims.of_int (16)) - (Prims.of_int (354)) + (Prims.of_int (337)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (354)) + (Prims.of_int (337)) (Prims.of_int (42)) - (Prims.of_int (358)) + (Prims.of_int (341)) (Prims.of_int (45))))) (Obj.magic (intro_st_comp_typing st)) (fun uu___ -> @@ -1605,17 +1315,17 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (355)) + (Prims.of_int (338)) (Prims.of_int (31)) - (Prims.of_int (355)) + (Prims.of_int (338)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (354)) + (Prims.of_int (337)) (Prims.of_int (42)) - (Prims.of_int (358)) + (Prims.of_int (341)) (Prims.of_int (45))))) (Obj.magic (Pulse_Checker_Pure.core_check_term @@ -1639,18 +1349,18 @@ let (intro_comp_typing : ( FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (357)) + (Prims.of_int (340)) (Prims.of_int (23)) - (Prims.of_int (357)) + (Prims.of_int (340)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic ( FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (357)) + (Prims.of_int (340)) (Prims.of_int (11)) - (Prims.of_int (357)) + (Prims.of_int (340)) (Prims.of_int (87))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1659,9 +1369,9 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (357)) + (Prims.of_int (340)) (Prims.of_int (66)) - (Prims.of_int (357)) + (Prims.of_int (340)) (Prims.of_int (86))))) ( FStar_Sealed.seal @@ -1711,17 +1421,17 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (360)) + (Prims.of_int (343)) (Prims.of_int (16)) - (Prims.of_int (360)) + (Prims.of_int (343)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (360)) + (Prims.of_int (343)) (Prims.of_int (42)) - (Prims.of_int (364)) + (Prims.of_int (347)) (Prims.of_int (44))))) (Obj.magic (intro_st_comp_typing st)) (fun uu___ -> @@ -1732,17 +1442,17 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (361)) + (Prims.of_int (344)) (Prims.of_int (31)) - (Prims.of_int (361)) + (Prims.of_int (344)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (360)) + (Prims.of_int (343)) (Prims.of_int (42)) - (Prims.of_int (364)) + (Prims.of_int (347)) (Prims.of_int (44))))) (Obj.magic (Pulse_Checker_Pure.core_check_term @@ -1766,18 +1476,18 @@ let (intro_comp_typing : ( FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (363)) + (Prims.of_int (346)) (Prims.of_int (23)) - (Prims.of_int (363)) + (Prims.of_int (346)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic ( FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (363)) + (Prims.of_int (346)) (Prims.of_int (11)) - (Prims.of_int (363)) + (Prims.of_int (346)) (Prims.of_int (87))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1786,9 +1496,9 @@ let (intro_comp_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (363)) + (Prims.of_int (346)) (Prims.of_int (66)) - (Prims.of_int (363)) + (Prims.of_int (346)) (Prims.of_int (86))))) ( FStar_Sealed.seal @@ -1891,13 +1601,13 @@ let (apply_checker_result_k : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (403)) (Prims.of_int (35)) - (Prims.of_int (403)) (Prims.of_int (36))))) + (Prims.of_int (386)) (Prims.of_int (35)) + (Prims.of_int (386)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (400)) (Prims.of_int (55)) - (Prims.of_int (410)) (Prims.of_int (22))))) + (Prims.of_int (383)) (Prims.of_int (55)) + (Prims.of_int (393)) (Prims.of_int (22))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> r)) (fun uu___ -> (fun uu___ -> @@ -1909,14 +1619,14 @@ let (apply_checker_result_k : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (405)) (Prims.of_int (29)) - (Prims.of_int (405)) (Prims.of_int (70))))) + (Prims.of_int (388)) (Prims.of_int (29)) + (Prims.of_int (388)) (Prims.of_int (70))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (403)) (Prims.of_int (39)) - (Prims.of_int (410)) (Prims.of_int (22))))) + (Prims.of_int (386)) (Prims.of_int (39)) + (Prims.of_int (393)) (Prims.of_int (22))))) (Obj.magic (Pulse_Checker_Pure.check_universe g1 ty_y)) (fun uu___1 -> @@ -1929,17 +1639,17 @@ let (apply_checker_result_k : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (408)) + (Prims.of_int (391)) (Prims.of_int (4)) - (Prims.of_int (408)) + (Prims.of_int (391)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (410)) + (Prims.of_int (393)) (Prims.of_int (2)) - (Prims.of_int (410)) + (Prims.of_int (393)) (Prims.of_int (22))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -1970,13 +1680,13 @@ let (checker_result_for_st_typing : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (417)) (Prims.of_int (22)) - (Prims.of_int (417)) (Prims.of_int (23))))) + (Prims.of_int (400)) (Prims.of_int (22)) + (Prims.of_int (400)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (415)) (Prims.of_int (47)) - (Prims.of_int (445)) (Prims.of_int (35))))) + (Prims.of_int (398)) (Prims.of_int (47)) + (Prims.of_int (422)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> d)) (fun uu___ -> (fun uu___ -> @@ -1988,237 +1698,97 @@ let (checker_result_for_st_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (419)) (Prims.of_int (2)) - (Prims.of_int (423)) (Prims.of_int (33))))) + (Prims.of_int (402)) (Prims.of_int (10)) + (Prims.of_int (402)) (Prims.of_int (17))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (423)) (Prims.of_int (34)) - (Prims.of_int (445)) (Prims.of_int (35))))) - (if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp c) - then - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (421)) - (Prims.of_int (9)) - (Prims.of_int (423)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (420)) - (Prims.of_int (7)) - (Prims.of_int (423)) - (Prims.of_int (33))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (423)) - (Prims.of_int (12)) - (Prims.of_int (423)) - (Prims.of_int (32))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (421)) - (Prims.of_int (9)) - (Prims.of_int (423)) - (Prims.of_int (33))))) - (Obj.magic - (Pulse_Syntax_Printer.comp_to_string - c)) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (421)) - (Prims.of_int (9)) - (Prims.of_int (423)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (421)) - (Prims.of_int (9)) - (Prims.of_int (423)) - (Prims.of_int (33))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (422)) - (Prims.of_int (12)) - (Prims.of_int (422)) - (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Printf.fst" - (Prims.of_int (121)) - (Prims.of_int (8)) - (Prims.of_int (123)) - (Prims.of_int (44))))) - (Obj.magic - (Pulse_Syntax_Printer.st_term_to_string - t)) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 - -> - fun x -> - Prims.strcat - (Prims.strcat - "checker_result_for_st_typing: input term " - (Prims.strcat - uu___2 - " is not stateful (c: ")) - (Prims.strcat - x ")"))))) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> - uu___2 uu___1)))) - uu___1))) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (Pulse_Typing_Env.fail g - FStar_Pervasives_Native.None - uu___1)) uu___1))) - else - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> ())))) + (Prims.of_int (402)) (Prims.of_int (20)) + (Prims.of_int (422)) (Prims.of_int (35))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> Pulse_Typing_Env.fresh g)) (fun uu___1 -> - (fun uu___1 -> + (fun x -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (425)) - (Prims.of_int (10)) - (Prims.of_int (425)) - (Prims.of_int (17))))) + (Prims.of_int (404)) + (Prims.of_int (11)) + (Prims.of_int (404)) + (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (425)) - (Prims.of_int (20)) - (Prims.of_int (445)) + (Prims.of_int (404)) + (Prims.of_int (58)) + (Prims.of_int (422)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Pulse_Typing_Env.fresh g)) - (fun uu___2 -> - (fun x -> + (fun uu___1 -> + Pulse_Typing_Env.push_binding g x + Pulse_Syntax_Base.ppname_default + (Pulse_Syntax_Base.comp_res c))) + (fun uu___1 -> + (fun g' -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (427)) - (Prims.of_int (11)) - (Prims.of_int (427)) - (Prims.of_int (55))))) + (Prims.of_int (405)) + (Prims.of_int (14)) + (Prims.of_int (405)) + (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (427)) - (Prims.of_int (58)) - (Prims.of_int (445)) + (Prims.of_int (405)) + (Prims.of_int (63)) + (Prims.of_int (422)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Pulse_Typing_Env.push_binding - g x - Pulse_Syntax_Base.ppname_default - (Pulse_Syntax_Base.comp_res - c))) - (fun uu___2 -> - (fun g' -> + (fun uu___1 -> + Pulse_Syntax_Naming.open_term_nv + (Pulse_Syntax_Base.comp_post + c) + (Pulse_Syntax_Base.ppname_default, + x))) + (fun uu___1 -> + (fun ctxt' -> Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (428)) - (Prims.of_int (14)) - (Prims.of_int (428)) - (Prims.of_int (60))))) + (Prims.of_int (410)) + (Prims.of_int (4)) + (Prims.of_int (410)) + (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Base.fst" - (Prims.of_int (428)) - (Prims.of_int (63)) - (Prims.of_int (445)) - (Prims.of_int (35))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Pulse_Syntax_Naming.open_term_nv - ( - Pulse_Syntax_Base.comp_post - c) - (Pulse_Syntax_Base.ppname_default, - x))) - (fun uu___2 -> - (fun ctxt' -> - Obj.magic - ( - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (433)) - (Prims.of_int (4)) - (Prims.of_int (433)) - (Prims.of_int (59))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Base.fst" - (Prims.of_int (445)) + (Prims.of_int (422)) (Prims.of_int (2)) - (Prims.of_int (445)) + (Prims.of_int (422)) (Prims.of_int (35))))) - (Obj.magic - (continuation_elaborator_with_bind - g - Pulse_Syntax_Base.tm_emp - c t d1 () - x)) - (fun k -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___2 -> + (Obj.magic + (continuation_elaborator_with_bind + g + Pulse_Syntax_Base.tm_emp + c t d1 () x)) + (fun k -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___1 + -> FStar_Pervasives.Mkdtuple5 (x, (Pulse_Syntax_Base.comp_res @@ -2238,6 +1808,5 @@ let (checker_result_for_st_typing : Pulse_Syntax_Base.tm_emp) ctxt' k () ())))))) - uu___2))) - uu___2))) uu___2))) + uu___1))) uu___1))) uu___1))) uu___) \ No newline at end of file diff --git a/src/ocaml/plugin/generated/Pulse_Checker_If.ml b/src/ocaml/plugin/generated/Pulse_Checker_If.ml index acd01d161..389cd442a 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_If.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_If.ml @@ -711,7 +711,7 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" (Prims.of_int (97)) (Prims.of_int (64)) - (Prims.of_int (158)) (Prims.of_int (32))))) + (Prims.of_int (154)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context g "check_if" @@ -734,7 +734,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (97)) (Prims.of_int (64)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (Obj.magic (Pulse_Checker_Pure.check_term_with_expected_type @@ -759,7 +759,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (102)) (Prims.of_int (30)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -782,7 +782,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (103)) (Prims.of_int (22)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -808,7 +808,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (106)) (Prims.of_int (4)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) ( FStar_Tactics_Effect.lift_div_tac @@ -837,15 +837,15 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (111)) (Prims.of_int (47)) - (Prims.of_int (130)) + (Prims.of_int (126)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (131)) + (Prims.of_int (127)) (Prims.of_int (4)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -871,7 +871,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (112)) (Prims.of_int (37)) - (Prims.of_int (130)) + (Prims.of_int (126)) (Prims.of_int (23))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -899,7 +899,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (117)) (Prims.of_int (6)) - (Prims.of_int (130)) + (Prims.of_int (126)) (Prims.of_int (23))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -926,7 +926,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (118)) (Prims.of_int (65)) - (Prims.of_int (130)) + (Prims.of_int (126)) (Prims.of_int (23))))) (Obj.magic (check1 @@ -954,7 +954,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (118)) (Prims.of_int (65)) - (Prims.of_int (130)) + (Prims.of_int (126)) (Prims.of_int (23))))) (Obj.magic (Pulse_Checker_Base.apply_checker_result_k @@ -988,7 +988,7 @@ let (check : "Pulse.Checker.If.fst" (Prims.of_int (123)) (Prims.of_int (4)) - (Prims.of_int (130)) + (Prims.of_int (126)) (Prims.of_int (23))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1024,83 +1024,12 @@ let (check : else Obj.magic (Obj.repr - (if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp - c) - then - Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.If.fst" - (Prims.of_int (128)) - (Prims.of_int (11)) - (Prims.of_int (129)) - (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.If.fst" - (Prims.of_int (127)) - (Prims.of_int (9)) - (Prims.of_int (129)) - (Prims.of_int (43))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.If.fst" - (Prims.of_int (129)) - (Prims.of_int (22)) - (Prims.of_int (129)) - (Prims.of_int (42))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (Pulse_Syntax_Printer.comp_to_string - c)) - (fun - uu___4 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___5 -> - Prims.strcat - (Prims.strcat - "check_if: " - (Prims.strcat - br_name - " branch does not have a stateful computation type (c: ")) - (Prims.strcat - uu___4 - ")"))))) - (fun - uu___4 -> - (fun - uu___4 -> - Obj.magic - (Pulse_Typing_Env.fail - g1 - (FStar_Pervasives_Native.Some - (br1.Pulse_Syntax_Base.range2)) - uu___4)) - uu___4)) - else - Obj.repr (FStar_Tactics_Effect.lift_div_tac (fun - uu___5 -> + uu___4 -> FStar_Pervasives.Mkdtuple3 (br1, c, - d)))))) + d))))) uu___3))) uu___2))) uu___2))) @@ -1117,17 +1046,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (133)) + (Prims.of_int (129)) (Prims.of_int (32)) - (Prims.of_int (133)) + (Prims.of_int (129)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (131)) + (Prims.of_int (127)) (Prims.of_int (4)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (Obj.magic (check_branch @@ -1150,17 +1079,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (134)) + (Prims.of_int (130)) (Prims.of_int (32)) - (Prims.of_int (134)) + (Prims.of_int (130)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (133)) + (Prims.of_int (129)) (Prims.of_int (63)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (Obj.magic (check_branch @@ -1183,17 +1112,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (136)) + (Prims.of_int (132)) (Prims.of_int (4)) - (Prims.of_int (136)) + (Prims.of_int (132)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (134)) + (Prims.of_int (130)) (Prims.of_int (65)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (Obj.magic (combine_if_branches @@ -1223,17 +1152,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (138)) + (Prims.of_int (134)) (Prims.of_int (16)) - (Prims.of_int (152)) + (Prims.of_int (148)) (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (153)) + (Prims.of_int (149)) (Prims.of_int (4)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1241,17 +1170,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (139)) + (Prims.of_int (135)) (Prims.of_int (12)) - (Prims.of_int (139)) + (Prims.of_int (135)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (140)) + (Prims.of_int (136)) (Prims.of_int (4)) - (Prims.of_int (152)) + (Prims.of_int (148)) (Prims.of_int (88))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1296,17 +1225,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (145)) + (Prims.of_int (141)) (Prims.of_int (9)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1314,17 +1243,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (81)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (114))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -1339,17 +1268,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1357,17 +1286,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (45)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -1382,17 +1311,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1400,17 +1329,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1418,17 +1347,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (148)) + (Prims.of_int (144)) (Prims.of_int (76)) - (Prims.of_int (148)) + (Prims.of_int (144)) (Prims.of_int (108))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (Pulse_Syntax_Printer.term_to_string @@ -1444,17 +1373,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (146)) + (Prims.of_int (142)) (Prims.of_int (11)) - (Prims.of_int (149)) + (Prims.of_int (145)) (Prims.of_int (115))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1462,9 +1391,9 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (148)) + (Prims.of_int (144)) (Prims.of_int (44)) - (Prims.of_int (148)) + (Prims.of_int (144)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic @@ -1559,17 +1488,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (151)) + (Prims.of_int (147)) (Prims.of_int (26)) - (Prims.of_int (151)) + (Prims.of_int (147)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (152)) + (Prims.of_int (148)) (Prims.of_int (8)) - (Prims.of_int (152)) + (Prims.of_int (148)) (Prims.of_int (88))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1600,17 +1529,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (156)) + (Prims.of_int (152)) (Prims.of_int (4)) - (Prims.of_int (156)) + (Prims.of_int (152)) (Prims.of_int (84))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.If.fst" - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (2)) - (Prims.of_int (158)) + (Prims.of_int (154)) (Prims.of_int (32))))) (FStar_Tactics_Effect.lift_div_tac (fun diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml index c4abf63b5..d13533f1d 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml @@ -413,7 +413,7 @@ let (check_branch : (FStar_Range.mk_range "Pulse.Checker.Match.fst" (Prims.of_int (218)) (Prims.of_int (27)) - (Prims.of_int (242)) (Prims.of_int (58))))) + (Prims.of_int (240)) (Prims.of_int (58))))) (match readback_pat p0 with | FStar_Pervasives_Native.Some p -> Obj.magic @@ -445,7 +445,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (221)) (Prims.of_int (54)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -469,7 +469,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (222)) (Prims.of_int (38)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -493,7 +493,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (223)) (Prims.of_int (27)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -517,7 +517,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (225)) (Prims.of_int (2)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -544,7 +544,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (227)) (Prims.of_int (2)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (if Prims.op_Negation @@ -585,7 +585,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (228)) (Prims.of_int (80)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (if FStar_Reflection_V2_Data.uu___is_Tv_Unknown @@ -628,7 +628,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (230)) (Prims.of_int (89)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -661,7 +661,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (231)) (Prims.of_int (109)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -698,7 +698,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (232)) (Prims.of_int (39)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (Obj.magic (open_st_term_bs @@ -724,7 +724,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (233)) (Prims.of_int (64)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -751,7 +751,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (234)) (Prims.of_int (92)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -778,7 +778,7 @@ let (check_branch : "Pulse.Checker.Match.fst" (Prims.of_int (234)) (Prims.of_int (92)) - (Prims.of_int (242)) + (Prims.of_int (240)) (Prims.of_int (58))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -816,56 +816,15 @@ let (check_branch : uu___2))) (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac (fun - uu___2 -> + uu___3 -> match uu___2 with | FStar_Pervasives.Mkdtuple3 (e2, c, e_d) -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Match.fst" - (Prims.of_int (239)) - (Prims.of_int (2)) - (Prims.of_int (240)) - (Prims.of_int (62))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "Pulse.Checker.Match.fst" - (Prims.of_int (242)) - (Prims.of_int (2)) - (Prims.of_int (242)) - (Prims.of_int (58))))) - (if - Prims.op_Negation - (Pulse_Syntax_Base.stateful_comp - c) - then - Obj.magic - (Obj.repr - (Pulse_Typing_Env.fail - g - (FStar_Pervasives_Native.Some - (e2.Pulse_Syntax_Base.range2)) - "Branch computation is not stateful")) - else - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> - ())))) - (fun - uu___3 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___4 -> FStar_Pervasives.Mkdtuple4 (p, (Pulse_Syntax_Naming.close_st_term_n @@ -888,7 +847,6 @@ let (check_branch : uu___2))) uu___2))) uu___2))) - uu___2))) uu___1))) uu___))) uu___))) @@ -928,13 +886,13 @@ let (check_branches : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (258)) (Prims.of_int (2)) - (Prims.of_int (258)) (Prims.of_int (50))))) + (Prims.of_int (256)) (Prims.of_int (2)) + (Prims.of_int (256)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (258)) (Prims.of_int (51)) - (Prims.of_int (291)) (Prims.of_int (18))))) + (Prims.of_int (256)) (Prims.of_int (51)) + (Prims.of_int (289)) (Prims.of_int (18))))) (if FStar_List_Tot_Base.isEmpty brs0 then Obj.magic @@ -954,17 +912,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (259)) + (Prims.of_int (257)) (Prims.of_int (22)) - (Prims.of_int (259)) + (Prims.of_int (257)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (258)) + (Prims.of_int (256)) (Prims.of_int (51)) - (Prims.of_int (291)) + (Prims.of_int (289)) (Prims.of_int (18))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> brs0)) @@ -978,17 +936,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (260)) + (Prims.of_int (258)) (Prims.of_int (26)) - (Prims.of_int (260)) + (Prims.of_int (258)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (259)) + (Prims.of_int (257)) (Prims.of_int (29)) - (Prims.of_int (291)) + (Prims.of_int (289)) (Prims.of_int (18))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___3 -> bnds)) @@ -1004,18 +962,18 @@ let (check_branches : Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (261)) + (Prims.of_int (259)) (Prims.of_int (29)) - (Prims.of_int (261)) + (Prims.of_int (259)) (Prims.of_int (100))))) (FStar_Sealed.seal ( Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (260)) + (Prims.of_int (258)) (Prims.of_int (33)) - (Prims.of_int (291)) + (Prims.of_int (289)) (Prims.of_int (18))))) (Obj.magic ( @@ -1044,17 +1002,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (264)) + (Prims.of_int (262)) (Prims.of_int (3)) - (Prims.of_int (276)) + (Prims.of_int (274)) (Prims.of_int (5))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (291)) + (Prims.of_int (289)) (Prims.of_int (2)) - (Prims.of_int (291)) + (Prims.of_int (289)) (Prims.of_int (18))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1062,17 +1020,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (267)) + (Prims.of_int (265)) (Prims.of_int (5)) - (Prims.of_int (272)) + (Prims.of_int (270)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (273)) + (Prims.of_int (271)) (Prims.of_int (6)) - (Prims.of_int (276)) + (Prims.of_int (274)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1085,17 +1043,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (268)) + (Prims.of_int (266)) (Prims.of_int (19)) - (Prims.of_int (268)) + (Prims.of_int (266)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (267)) + (Prims.of_int (265)) (Prims.of_int (5)) - (Prims.of_int (272)) + (Prims.of_int (270)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1116,17 +1074,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (269)) + (Prims.of_int (267)) (Prims.of_int (20)) - (Prims.of_int (269)) + (Prims.of_int (267)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (268)) + (Prims.of_int (266)) (Prims.of_int (23)) - (Prims.of_int (272)) + (Prims.of_int (270)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1147,17 +1105,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (270)) + (Prims.of_int (268)) (Prims.of_int (29)) - (Prims.of_int (270)) + (Prims.of_int (268)) (Prims.of_int (95))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (269)) + (Prims.of_int (267)) (Prims.of_int (26)) - (Prims.of_int (272)) + (Prims.of_int (270)) (Prims.of_int (20))))) (Obj.magic (check_branch @@ -1194,17 +1152,17 @@ let (check_branches : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (274)) + (Prims.of_int (272)) (Prims.of_int (12)) - (Prims.of_int (274)) + (Prims.of_int (272)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (274)) + (Prims.of_int (272)) (Prims.of_int (8)) - (Prims.of_int (274)) + (Prims.of_int (272)) (Prims.of_int (9))))) (Obj.magic (Pulse_Common.zipWith @@ -1273,13 +1231,13 @@ let (check : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (304)) (Prims.of_int (10)) - (Prims.of_int (304)) (Prims.of_int (64))))) + (Prims.of_int (302)) (Prims.of_int (10)) + (Prims.of_int (302)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (304)) (Prims.of_int (67)) - (Prims.of_int (352)) (Prims.of_int (44))))) + (Prims.of_int (302)) (Prims.of_int (67)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Pulse_Typing_Env.push_context_no_range g @@ -1292,17 +1250,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (306)) + (Prims.of_int (304)) (Prims.of_int (17)) - (Prims.of_int (306)) + (Prims.of_int (304)) (Prims.of_int (25))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (306)) + (Prims.of_int (304)) (Prims.of_int (28)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> sc.Pulse_Syntax_Base.range1)) @@ -1314,17 +1272,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (307)) + (Prims.of_int (305)) (Prims.of_int (17)) - (Prims.of_int (307)) + (Prims.of_int (305)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (307)) + (Prims.of_int (305)) (Prims.of_int (23)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> brs)) @@ -1336,17 +1294,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (308)) + (Prims.of_int (306)) (Prims.of_int (12)) - (Prims.of_int (308)) + (Prims.of_int (306)) (Prims.of_int (24))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (308)) + (Prims.of_int (306)) (Prims.of_int (27)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -1361,18 +1319,18 @@ let (check : ( FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (310)) + (Prims.of_int (308)) (Prims.of_int (55)) - (Prims.of_int (310)) + (Prims.of_int (308)) (Prims.of_int (79))))) (FStar_Sealed.seal (Obj.magic ( FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (308)) + (Prims.of_int (306)) (Prims.of_int (27)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (Obj.magic (Pulse_Checker_Pure.check_term_and_type @@ -1396,17 +1354,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (311)) + (Prims.of_int (309)) (Prims.of_int (18)) - (Prims.of_int (311)) + (Prims.of_int (309)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (316)) + (Prims.of_int (314)) (Prims.of_int (4)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1427,17 +1385,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (323)) + (Prims.of_int (321)) (Prims.of_int (4)) - (Prims.of_int (326)) + (Prims.of_int (324)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (316)) + (Prims.of_int (314)) (Prims.of_int (4)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1445,17 +1403,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (323)) + (Prims.of_int (321)) (Prims.of_int (10)) - (Prims.of_int (323)) + (Prims.of_int (321)) (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (323)) + (Prims.of_int (321)) (Prims.of_int (4)) - (Prims.of_int (326)) + (Prims.of_int (324)) (Prims.of_int (75))))) (Obj.magic (FStar_Tactics_V2_Builtins.check_match_complete @@ -1527,17 +1485,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (327)) + (Prims.of_int (325)) (Prims.of_int (4)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (327)) + (Prims.of_int (325)) (Prims.of_int (4)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1553,17 +1511,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (328)) + (Prims.of_int (326)) (Prims.of_int (17)) - (Prims.of_int (328)) + (Prims.of_int (326)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (329)) + (Prims.of_int (327)) (Prims.of_int (2)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1582,17 +1540,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (329)) + (Prims.of_int (327)) (Prims.of_int (2)) - (Prims.of_int (330)) + (Prims.of_int (328)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (330)) + (Prims.of_int (328)) (Prims.of_int (61)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (if FStar_Pervasives_Native.uu___is_None @@ -1622,17 +1580,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (331)) + (Prims.of_int (329)) (Prims.of_int (12)) - (Prims.of_int (331)) + (Prims.of_int (329)) (Prims.of_int (66))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (344)) + (Prims.of_int (342)) (Prims.of_int (50)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (Obj.magic (Pulse_Common.zipWith @@ -1668,17 +1626,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (346)) + (Prims.of_int (344)) (Prims.of_int (28)) - (Prims.of_int (346)) + (Prims.of_int (344)) (Prims.of_int (116))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (344)) + (Prims.of_int (342)) (Prims.of_int (50)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (Obj.magic (check_branches @@ -1707,17 +1665,17 @@ let (check : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (351)) + (Prims.of_int (349)) (Prims.of_int (10)) - (Prims.of_int (351)) + (Prims.of_int (349)) (Prims.of_int (83))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (2)) - (Prims.of_int (352)) + (Prims.of_int (350)) (Prims.of_int (44))))) (FStar_Tactics_Effect.lift_div_tac (fun diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml b/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml index 38003210f..2e7156952 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml @@ -1190,7 +1190,7 @@ let (apply_frame : t_typing1, st_equiv) in Prims.Mkdtuple2 (c'', t_typing2)) type ('g, 'ctxt, 'postuhint) st_typing_in_ctxt = - (Pulse_Syntax_Base.st_term, Pulse_Syntax_Base.comp, + (Pulse_Syntax_Base.st_term, Pulse_Syntax_Base.comp_st, (unit, unit, unit) Pulse_Typing.st_typing) FStar_Pervasives.dtuple3 let rec (vprop_as_list : Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term Prims.list) =