diff --git a/share/pulse/examples/Assume.fst b/share/pulse/examples/Assume.fst new file mode 100644 index 000000000..c6b999374 --- /dev/null +++ b/share/pulse/examples/Assume.fst @@ -0,0 +1,37 @@ +module Assume + +#lang-pulse +open Pulse + +assume val foo : int -> slprop + +fn test0 (x:int) + requires emp + ensures foo 1 +{ + assume foo 1; +} + +[@@expect_failure] +fn test1 (x:int) + requires emp + ensures foo 1 +{ + with a. assume foo 1; +} + +fn test2 (x:int) + requires emp + ensures foo 1 ** foo 2 +{ + assume foo 1; + assume foo 2; +} + +[@@expect_failure] +fn test3 (x:int) + requires emp + ensures foo 1 ** foo 2 +{ + assume foo 2; +} diff --git a/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst b/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst index 6bef19f53..dc01dddb2 100644 --- a/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst +++ b/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst @@ -30,3 +30,18 @@ ensures emp { id x y } + +fn f (x: nat) +requires emp +ensures emp +{ + () +} + +[@@expect_failure] +fn test4 () +requires emp +ensures emp +{ + f true +} diff --git a/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected b/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected index c394d7b29..df00f4946 100644 --- a/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected +++ b/share/pulse/examples/bug-reports/error-messages/Bug.DesugaringError.fst.expected @@ -24,6 +24,15 @@ - Expected expression of type Prims.nat got expression y of type Prims.bool - Raised within Tactics.refl_instantiate_implicits +>>] +>> Got issues: [ +* Error 228 at Bug.DesugaringError.fst(46,2-46,2): + - Could not check term: Bug.DesugaringError.f true + +* Error 189 at Bug.DesugaringError.fst(46,4-46,8): + - Expected expression of type Prims.nat got expression true of type Prims.bool + - Raised within Tactics.refl_instantiate_implicits + >>] Verified module: Bug.DesugaringError All verification conditions discharged successfully diff --git a/src/checker/Pulse.Checker.Abs.fst b/src/checker/Pulse.Checker.Abs.fst index c2ed0fd7f..021517720 100644 --- a/src/checker/Pulse.Checker.Abs.fst +++ b/src/checker/Pulse.Checker.Abs.fst @@ -41,16 +41,6 @@ let debug_abs g (s: unit -> T.Tac string) : T.Tac unit = (* Infers the the type of the binders from the specification alone, not the body *) -let range_of_st_comp (st:st_comp) = - RU.union_ranges (RU.range_of_term st.pre) (RU.range_of_term st.post) - -let range_of_comp (c:comp) = - match c with - | C_Tot t -> RU.range_of_term t - | C_ST st -> range_of_st_comp st - | C_STAtomic _ _ st -> range_of_st_comp st - | C_STGhost _ st -> range_of_st_comp st - let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term }) : T.Tac (term & t:st_term { Tm_Abs? t.term }) = let Tm_Abs { b; q; ascription; body } = prog.term in @@ -69,8 +59,7 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term }) let arr, body = arrow_of_abs env body in let arr = close_term arr x in let body = close_st_term body x in - let ty : term = wr (tm_arrow b q (C_Tot arr)) - (RU.union_ranges (RU.range_of_term b.binder_ty) (RU.range_of_term arr)) in + let ty : term = tm_arrow b q (C_Tot arr) in let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body}} in ty, prog @@ -82,8 +71,7 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term }) //retain the original annotation, so that we check it wrt the inferred type in maybe_rewrite_body_typing let t = close_term t x in let annot = close_comp c x in - let ty : term = wr (tm_arrow b q (C_Tot t)) - (RU.union_ranges (RU.range_of_term b.binder_ty) (RU.range_of_term t)) in + let ty : term = tm_arrow b q (C_Tot t) in let ascription = { annotated = Some annot; elaborated = None } in let body = close_st_term body x in let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in @@ -104,8 +92,7 @@ let rec arrow_of_abs (env:_) (prog:st_term { Tm_Abs? prog.term }) Env.fail env (Some prog.range) "Unannotated function body" | Some c -> ( //we're taking the annotation as is; remove it from the abstraction to avoid rechecking it - let ty : term = wr (tm_arrow b q c) - (RU.union_ranges (RU.range_of_term b.binder_ty) (range_of_comp c)) in + let ty : term = tm_arrow b q c in let ascription = empty_ascription in let body = close_st_term body x in let prog : st_term = { prog with term = Tm_Abs { b; q; ascription; body} } in diff --git a/src/checker/Pulse.Checker.Match.fst b/src/checker/Pulse.Checker.Match.fst index 8b7906a15..5565a7473 100644 --- a/src/checker/Pulse.Checker.Match.fst +++ b/src/checker/Pulse.Checker.Match.fst @@ -246,7 +246,7 @@ let check_branch fail g (Some e.range) "should not happen: pattern elaborated to Tv_Unknown"; // T.print ("Elaborated pattern = " ^ T.term_to_string (fst (Some?.v elab_p))); let elab_p_tm = fst (Some?.v elab_p) in - let eq_typ = mk_sq_eq2 sc_u sc_ty sc (wr elab_p_tm Range.range_0) in + let eq_typ = mk_sq_eq2 sc_u sc_ty sc elab_p_tm in let g' = push_binding g' hyp_var ({name = Sealed.seal "branch equality"; range = Range.range_0 }) eq_typ in let e = open_st_term_bs e pulse_bs in let e = diff --git a/src/checker/Pulse.Elaborate.Core.fst b/src/checker/Pulse.Elaborate.Core.fst index 1336b65f4..46a6afe09 100644 --- a/src/checker/Pulse.Elaborate.Core.fst +++ b/src/checker/Pulse.Elaborate.Core.fst @@ -143,6 +143,7 @@ let elab_lift #g #c1 #c2 (d:lift_comp g c1 c2) (e:R.term) let intro_pure_tm (p:term) = let open Pulse.Reflection.Util in + let rng = R.range_of_term p in wtag (Some STT_Ghost) (Tm_STApp { head = @@ -150,7 +151,7 @@ let intro_pure_tm (p:term) = None p; arg_qual = None; - arg = S.wr (`()) Range.range_0 }) + arg = S.wr (`()) rng }) let simple_arr (t1 t2 : R.term) : R.term = let b = R.pack_binder { diff --git a/src/checker/Pulse.Syntax.Base.fst b/src/checker/Pulse.Syntax.Base.fst index 366991350..a3c2a81aa 100644 --- a/src/checker/Pulse.Syntax.Base.fst +++ b/src/checker/Pulse.Syntax.Base.fst @@ -20,6 +20,16 @@ module RT = FStar.Reflection.Typing module R = FStar.Reflection.V2 module T = FStar.Tactics.V2 +let range_of_st_comp (st:st_comp) = + RU.union_ranges (RU.range_of_term st.pre) (RU.range_of_term st.post) + +let range_of_comp (c:comp) = + match c with + | C_Tot t -> RU.range_of_term t + | C_ST st -> range_of_st_comp st + | C_STAtomic _ _ st -> range_of_st_comp st + | C_STGhost _ st -> range_of_st_comp st + let eq_univ (u1 u2:universe) : b:bool{b <==> u1 == u2} = let open FStar.Reflection.TermEq in assume (faithful_univ u1); diff --git a/src/checker/Pulse.Syntax.Base.fsti b/src/checker/Pulse.Syntax.Base.fsti index 0cd28e909..f61ca239e 100644 --- a/src/checker/Pulse.Syntax.Base.fsti +++ b/src/checker/Pulse.Syntax.Base.fsti @@ -113,6 +113,8 @@ type comp = | C_STAtomic : inames:term -> obs:observability -> st_comp -> comp | C_STGhost : inames:term -> st_comp -> comp +val range_of_st_comp (st:st_comp) : R.range +val range_of_comp (c:comp) : R.range let comp_st = c:comp {not (C_Tot? c) } diff --git a/src/checker/Pulse.Syntax.Pure.fst b/src/checker/Pulse.Syntax.Pure.fst index 24c7ca347..ee2dd3255 100644 --- a/src/checker/Pulse.Syntax.Pure.fst +++ b/src/checker/Pulse.Syntax.Pure.fst @@ -62,27 +62,27 @@ let tm_uinst (l:fv) (us:list universe) : term = l.fv_range let tm_constant (c:constant) : term = - set_range (R.pack_ln (R.Tv_Const c)) FStar.Range.range_0 + R.pack_ln (R.Tv_Const c) -let tm_refine (b:binder) (t:term) : term = +let tm_refine (b:binder) (t:term) rng : term = let rb : R.simple_binder = RT.mk_simple_binder b.binder_ppname.name b.binder_ty in set_range (R.pack_ln (R.Tv_Refine rb t)) - FStar.Range.range_0 + rng -let tm_let (t e1 e2:term) : term = +let tm_let (t e1 e2:term) rng : term = let rb : R.simple_binder = RT.mk_simple_binder RT.pp_name_default t in set_range (R.pack_ln (R.Tv_Let false [] rb e1 e2)) - FStar.Range.range_0 + rng let tm_pureapp (head:term) (q:option qualifier) (arg:term) : term = set_range (R.mk_app head [(arg, elab_qual q)]) - FStar.Range.range_0 + (union_ranges (range_of_term head) (range_of_term arg)) -let tm_pureabs (ppname:R.ppname_t) (ty : term) (q : option qualifier) (body:term) : term = +let tm_pureabs (ppname:R.ppname_t) (ty : term) (q : option qualifier) (body:term) rng : term = let open R in let open T in let b : T.binder = { @@ -95,12 +95,12 @@ let tm_pureabs (ppname:R.ppname_t) (ty : term) (q : option qualifier) (body:term in let r = pack (Tv_Abs b body) in assume (~(R.Tv_Unknown? (R.inspect_ln r))); // NamedView API doesn't ensure this, it should - set_range r FStar.Range.range_0 + set_range r rng let tm_arrow (b:binder) (q:option qualifier) (c:comp) : term = set_range (mk_arrow_with_name b.binder_ppname.name (b.binder_ty, elab_qual q) (elab_comp c)) - FStar.Range.range_0 + (union_ranges (range_of_term b.binder_ty) (range_of_comp c)) let tm_type (u:universe) : term = RT.tm_type u diff --git a/src/checker/Pulse.Typing.fst b/src/checker/Pulse.Typing.fst index dc1ed2f78..9d6b82ba8 100644 --- a/src/checker/Pulse.Typing.fst +++ b/src/checker/Pulse.Typing.fst @@ -60,7 +60,7 @@ let mk_hide (u:universe) (t:term) (e:term) : term = let mk_eq2 (u:universe) (t:term) - (e0 e1:term) + (e0 e1:term) : term = tm_pureapp (tm_pureapp (tm_pureapp (tm_uinst (as_fv R.eq2_qn) [u]) (Some Implicit) t) @@ -426,7 +426,7 @@ let comp_withlocal_body_pre (pre:slprop) (init_t:term) (r:term) (init:term) : sl tm_star pre (mk_pts_to init_t r init) let comp_withlocal_body_post (post:term) (init_t:term) (r:term) : term = - tm_star post (tm_exists_sl u0 (as_binder init_t) (mk_pts_to init_t r (null_bvar 0))) + tm_star post (tm_exists_sl u0 (as_binder init_t) (mk_pts_to init_t r (null_bvar 0))) let comp_withlocal_body (r:var) (init_t:term) (init:term) (c:comp{C_ST? c}) : comp = let r = null_var r in diff --git a/src/ocaml/plugin/Pulse_Extract_CompilerLib.ml b/src/ocaml/plugin/Pulse_Extract_CompilerLib.ml index 887e22498..52837e682 100644 --- a/src/ocaml/plugin/Pulse_Extract_CompilerLib.ml +++ b/src/ocaml/plugin/Pulse_Extract_CompilerLib.ml @@ -85,12 +85,6 @@ let mle_name (x:mlpath) : mlexpr = as_expr (ML.MLE_Name x) let mle_let (x:mlletbinding) (b:mlexpr) : mlexpr = - (* Set the CInline attribute on *every* letbinding. This makes - generated C code much more compact. - See https://github.com/FStarLang/karamel/pull/470 *) - let flavors, lbs = x in - let lbs = lbs |> List.map (fun lb -> { lb with ML.mllb_meta = CInline :: lb.ML.mllb_meta }) in - let x = (flavors, lbs) in as_expr (ML.MLE_Let (x, b)) let mle_app (x:mlexpr) (args:mlexpr list) : mlexpr = diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml index d46a77d16..78937a528 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml @@ -2640,6 +2640,78 @@ and (desugar_proof_hint_with_binders : fun k -> fun r -> match s1.PulseSyntaxExtension_Sugar.s with + | PulseSyntaxExtension_Sugar.ProofHintWithBinders + { + PulseSyntaxExtension_Sugar.hint_type = + PulseSyntaxExtension_Sugar.ASSUME p; + PulseSyntaxExtension_Sugar.binders = [];_} + -> + Obj.magic + (Obj.repr + (let assume_fv = + PulseSyntaxExtension_SyntaxWrapper.mk_fv + PulseSyntaxExtension_Env.assume_lid r in + let assume_ = + PulseSyntaxExtension_SyntaxWrapper.tm_fvar + assume_fv in + let uu___ = desugar_slprop env p in + FStar_Class_Monad.op_let_Bang + PulseSyntaxExtension_Err.err_monad () () + (Obj.magic uu___) + (fun uu___1 -> + (fun p1 -> + let p1 = Obj.magic p1 in + let s11 = + PulseSyntaxExtension_SyntaxWrapper.tm_st_app + assume_ FStar_Pervasives_Native.None + p1 r in + let uu___1 = + match k with + | FStar_Pervasives_Native.None -> + let uu___2 = + let uu___3 = + PulseSyntaxExtension_SyntaxWrapper.tm_expr + FStar_Syntax_Syntax.unit_const + r in + PulseSyntaxExtension_SyntaxWrapper.tm_ghost_return + uu___3 r in + PulseSyntaxExtension_Err.return + uu___2 + | FStar_Pervasives_Native.Some s2 -> + desugar_stmt env s2 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + PulseSyntaxExtension_Err.err_monad + () () (Obj.magic uu___1) + (fun uu___2 -> + (fun s2 -> + let s2 = Obj.magic s2 in + let annot = + let uu___2 = + FStar_Ident.id_of_text + "_" in + let uu___3 = + PulseSyntaxExtension_SyntaxWrapper.tm_unknown + r in + PulseSyntaxExtension_SyntaxWrapper.mk_binder + uu___2 uu___3 in + let uu___2 = + mk_bind annot s11 s2 r in + Obj.magic + (PulseSyntaxExtension_Err.return + uu___2)) uu___2))) + uu___1))) + | PulseSyntaxExtension_Sugar.ProofHintWithBinders + { + PulseSyntaxExtension_Sugar.hint_type = + PulseSyntaxExtension_Sugar.ASSUME uu___; + PulseSyntaxExtension_Sugar.binders = b1::uu___1;_} + -> + Obj.magic + (Obj.repr + (PulseSyntaxExtension_Err.fail + "'assume' cannot have binders" + b1.FStar_Parser_AST.brange)) | PulseSyntaxExtension_Sugar.ProofHintWithBinders { PulseSyntaxExtension_Sugar.hint_type = hint_type; PulseSyntaxExtension_Sugar.binders = bs;_} diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Env.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Env.ml index c5c8c9aa7..6f4e0e305 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Env.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Env.ml @@ -11,6 +11,7 @@ let (pulse_lib_ref_lid : Prims.string -> FStar_Ident.lident) = fun l -> FStar_Ident.lid_of_path (FStar_List_Tot_Base.op_At ["Pulse"; "Lib"; "Reference"] [l]) r_ +let (assume_lid : FStar_Ident.lident) = pulse_lib_core_lid "assume_" let (prims_exists_lid : FStar_Ident.lident) = FStar_Ident.lid_of_path ["Prims"; "l_Exists"] r_ let (prims_forall_lid : FStar_Ident.lident) = diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml index bec044ff6..765ac5971 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml @@ -92,6 +92,7 @@ let (showable_mut_or_ref : mut_or_ref FStar_Class_Show.showable) = } type hint_type = | ASSERT of slprop + | ASSUME of slprop | UNFOLD of (FStar_Ident.lident Prims.list FStar_Pervasives_Native.option * slprop) | FOLD of (FStar_Ident.lident Prims.list FStar_Pervasives_Native.option * @@ -107,6 +108,10 @@ let (uu___is_ASSERT : hint_type -> Prims.bool) = fun projectee -> match projectee with | ASSERT _0 -> true | uu___ -> false let (__proj__ASSERT__item___0 : hint_type -> slprop) = fun projectee -> match projectee with | ASSERT _0 -> _0 +let (uu___is_ASSUME : hint_type -> Prims.bool) = + fun projectee -> match projectee with | ASSUME _0 -> true | uu___ -> false +let (__proj__ASSUME__item___0 : hint_type -> slprop) = + fun projectee -> match projectee with | ASSUME _0 -> _0 let (uu___is_UNFOLD : hint_type -> Prims.bool) = fun projectee -> match projectee with | UNFOLD _0 -> true | uu___ -> false let (__proj__UNFOLD__item___0 : @@ -156,6 +161,9 @@ let (showable_hint_type : hint_type FStar_Class_Show.showable) = | ASSERT s -> let uu___ = FStar_Class_Show.show showable_slprop s in Prims.strcat "ASSERT " uu___ + | ASSUME s -> + let uu___ = FStar_Class_Show.show showable_slprop s in + Prims.strcat "ASSUME " uu___ | UNFOLD (ns, s) -> let uu___ = let uu___1 = @@ -1210,6 +1218,7 @@ and (eq_hint_type : hint_type -> hint_type -> Prims.bool) = fun h2 -> match (h1, h2) with | (ASSERT s1, ASSERT s2) -> eq_slprop s1 s2 + | (ASSUME s1, ASSUME s2) -> eq_slprop s1 s2 | (UNFOLD (ns1, s1), UNFOLD (ns2, s2)) -> (eq_opt (forall2 eq_lident) ns1 ns2) && (eq_slprop s1 s2) | (FOLD (ns1, s1), FOLD (ns2, s2)) -> @@ -1406,6 +1415,7 @@ and (scan_hint_type : fun h -> match h with | ASSERT s -> scan_slprop cbs s + | ASSUME s -> scan_slprop cbs s | UNFOLD (ns, s) -> scan_slprop cbs s | FOLD (ns, s) -> scan_slprop cbs s | RENAME (ts, g, t) -> diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml index 2b594d03f..d9dd75675 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml @@ -35,18 +35,6 @@ let (debug_abs : (Obj.repr (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> ())))) uu___1 uu___ -let (range_of_st_comp : Pulse_Syntax_Base.st_comp -> FStar_Range.range) = - fun st -> - Pulse_RuntimeUtils.union_ranges - (Pulse_RuntimeUtils.range_of_term st.Pulse_Syntax_Base.pre) - (Pulse_RuntimeUtils.range_of_term st.Pulse_Syntax_Base.post) -let (range_of_comp : Pulse_Syntax_Base.comp -> FStar_Range.range) = - fun c -> - match c with - | Pulse_Syntax_Base.C_Tot t -> Pulse_RuntimeUtils.range_of_term t - | Pulse_Syntax_Base.C_ST st -> range_of_st_comp st - | Pulse_Syntax_Base.C_STAtomic (uu___, uu___1, st) -> range_of_st_comp st - | Pulse_Syntax_Base.C_STGhost (uu___, st) -> range_of_st_comp st let rec (arrow_of_abs : Pulse_Typing_Env.env -> Pulse_Syntax_Base.st_term -> @@ -59,12 +47,12 @@ let rec (arrow_of_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (56)) (Prims.of_int (44)) (Prims.of_int (56)) + (Prims.of_int (46)) (Prims.of_int (44)) (Prims.of_int (46)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (56)) (Prims.of_int (3)) (Prims.of_int (114)) + (Prims.of_int (46)) (Prims.of_int (3)) (Prims.of_int (101)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> prog.Pulse_Syntax_Base.term1)) @@ -81,13 +69,13 @@ let rec (arrow_of_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (57)) (Prims.of_int (12)) - (Prims.of_int (57)) (Prims.of_int (21))))) + (Prims.of_int (47)) (Prims.of_int (12)) + (Prims.of_int (47)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (57)) (Prims.of_int (24)) - (Prims.of_int (114)) (Prims.of_int (5))))) + (Prims.of_int (47)) (Prims.of_int (24)) + (Prims.of_int (101)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> Pulse_Typing_Env.fresh env)) (fun uu___1 -> @@ -98,17 +86,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (58)) + (Prims.of_int (48)) (Prims.of_int (13)) - (Prims.of_int (58)) + (Prims.of_int (48)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (58)) + (Prims.of_int (48)) (Prims.of_int (34)) - (Prims.of_int (114)) + (Prims.of_int (101)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -122,17 +110,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (59)) + (Prims.of_int (49)) (Prims.of_int (14)) - (Prims.of_int (59)) + (Prims.of_int (49)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (59)) + (Prims.of_int (49)) (Prims.of_int (56)) - (Prims.of_int (114)) + (Prims.of_int (101)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -149,17 +137,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (60)) + (Prims.of_int (50)) (Prims.of_int (15)) - (Prims.of_int (60)) + (Prims.of_int (50)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (60)) + (Prims.of_int (50)) (Prims.of_int (41)) - (Prims.of_int (114)) + (Prims.of_int (101)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -173,17 +161,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (61)) + (Prims.of_int (51)) (Prims.of_int (16)) - (Prims.of_int (61)) + (Prims.of_int (51)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (62)) + (Prims.of_int (52)) (Prims.of_int (4)) - (Prims.of_int (114)) + (Prims.of_int (101)) (Prims.of_int (5))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -199,17 +187,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (62)) + (Prims.of_int (52)) (Prims.of_int (4)) - (Prims.of_int (63)) + (Prims.of_int (53)) (Prims.of_int (86))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (64)) + (Prims.of_int (54)) (Prims.of_int (4)) - (Prims.of_int (114)) + (Prims.of_int (101)) (Prims.of_int (5))))) (if FStar_Pervasives_Native.uu___is_Some @@ -249,17 +237,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (69)) + (Prims.of_int (59)) (Prims.of_int (24)) - (Prims.of_int (69)) + (Prims.of_int (59)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (67)) + (Prims.of_int (57)) (Prims.of_int (15)) - (Prims.of_int (75)) + (Prims.of_int (64)) (Prims.of_int (16))))) (Obj.magic (arrow_of_abs @@ -275,18 +263,11 @@ let rec (arrow_of_abs : | (arr, body2) -> - ((Pulse_Syntax_Pure.wr - (Pulse_Syntax_Pure.tm_arrow + ((Pulse_Syntax_Pure.tm_arrow b q (Pulse_Syntax_Base.C_Tot (Pulse_Syntax_Naming.close_term - arr x))) - (Pulse_RuntimeUtils.union_ranges - (Pulse_RuntimeUtils.range_of_term - b.Pulse_Syntax_Base.binder_ty) - (Pulse_RuntimeUtils.range_of_term - (Pulse_Syntax_Naming.close_term - arr x)))), + arr x))), { Pulse_Syntax_Base.term1 = @@ -319,17 +300,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (78)) + (Prims.of_int (67)) (Prims.of_int (16)) - (Prims.of_int (78)) + (Prims.of_int (67)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (79)) + (Prims.of_int (68)) (Prims.of_int (8)) - (Prims.of_int (98)) + (Prims.of_int (86)) (Prims.of_int (37))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -352,24 +333,14 @@ let rec (arrow_of_abs : (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> - ((Pulse_Syntax_Pure.wr - (Pulse_Syntax_Pure.tm_arrow + ((Pulse_Syntax_Pure.tm_arrow b q (Pulse_Syntax_Base.C_Tot (Pulse_Syntax_Naming.close_term (Pulse_RuntimeUtils.hnf_lax (Pulse_Typing.elab_env env1) - tannot) x))) - (Pulse_RuntimeUtils.union_ranges - (Pulse_RuntimeUtils.range_of_term - b.Pulse_Syntax_Base.binder_ty) - (Pulse_RuntimeUtils.range_of_term - (Pulse_Syntax_Naming.close_term - (Pulse_RuntimeUtils.hnf_lax - (Pulse_Typing.elab_env - env1) - tannot) x)))), + tannot) x))), { Pulse_Syntax_Base.term1 = @@ -412,17 +383,17 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (97)) + (Prims.of_int (85)) (Prims.of_int (12)) - (Prims.of_int (98)) + (Prims.of_int (86)) (Prims.of_int (37))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (94)) + (Prims.of_int (82)) (Prims.of_int (10)) - (Prims.of_int (98)) + (Prims.of_int (86)) (Prims.of_int (37))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -430,9 +401,9 @@ let rec (arrow_of_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (98)) + (Prims.of_int (86)) (Prims.of_int (16)) - (Prims.of_int (98)) + (Prims.of_int (86)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic @@ -487,14 +458,8 @@ let rec (arrow_of_abs : (FStar_Tactics_Effect.lift_div_tac (fun uu___3 -> - ((Pulse_Syntax_Pure.wr - (Pulse_Syntax_Pure.tm_arrow - b q c) - (Pulse_RuntimeUtils.union_ranges - (Pulse_RuntimeUtils.range_of_term - b.Pulse_Syntax_Base.binder_ty) - (range_of_comp - c))), + ((Pulse_Syntax_Pure.tm_arrow + b q c), { Pulse_Syntax_Base.term1 = @@ -585,13 +550,13 @@ let rec (rebuild_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (127)) (Prims.of_int (4)) - (Prims.of_int (129)) (Prims.of_int (41))))) + (Prims.of_int (114)) (Prims.of_int (4)) + (Prims.of_int (116)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (130)) (Prims.of_int (4)) - (Prims.of_int (179)) (Prims.of_int (47))))) + (Prims.of_int (117)) (Prims.of_int (4)) + (Prims.of_int (166)) (Prims.of_int (47))))) (Obj.magic (debug_abs g (fun uu___ -> @@ -599,13 +564,13 @@ let rec (rebuild_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (129)) (Prims.of_int (16)) - (Prims.of_int (129)) (Prims.of_int (40))))) + (Prims.of_int (116)) (Prims.of_int (16)) + (Prims.of_int (116)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (127)) (Prims.of_int (26)) - (Prims.of_int (129)) (Prims.of_int (40))))) + (Prims.of_int (114)) (Prims.of_int (26)) + (Prims.of_int (116)) (Prims.of_int (40))))) (Obj.magic (FStar_Tactics_V2_Builtins.term_to_string annot)) (fun uu___1 -> @@ -616,17 +581,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (127)) + (Prims.of_int (114)) (Prims.of_int (26)) - (Prims.of_int (129)) + (Prims.of_int (116)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (127)) + (Prims.of_int (114)) (Prims.of_int (26)) - (Prims.of_int (129)) + (Prims.of_int (116)) (Prims.of_int (40))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -634,9 +599,9 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (128)) + (Prims.of_int (115)) (Prims.of_int (16)) - (Prims.of_int (128)) + (Prims.of_int (115)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic @@ -677,13 +642,13 @@ let rec (rebuild_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (132)) (Prims.of_int (15)) - (Prims.of_int (132)) (Prims.of_int (34))))) + (Prims.of_int (119)) (Prims.of_int (15)) + (Prims.of_int (119)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (133)) (Prims.of_int (6)) - (Prims.of_int (173)) (Prims.of_int (41))))) + (Prims.of_int (120)) (Prims.of_int (6)) + (Prims.of_int (160)) (Prims.of_int (41))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> FStar_Reflection_V2_Builtins.inspect_binder b')) @@ -695,17 +660,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (133)) + (Prims.of_int (120)) (Prims.of_int (6)) - (Prims.of_int (133)) + (Prims.of_int (120)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (133)) + (Prims.of_int (120)) (Prims.of_int (57)) - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (41))))) (Obj.magic (qualifier_compat g @@ -719,17 +684,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (134)) + (Prims.of_int (121)) (Prims.of_int (15)) - (Prims.of_int (134)) + (Prims.of_int (121)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (134)) + (Prims.of_int (121)) (Prims.of_int (25)) - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (41))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -742,17 +707,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (135)) + (Prims.of_int (122)) (Prims.of_int (17)) - (Prims.of_int (135)) + (Prims.of_int (122)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (136)) + (Prims.of_int (123)) (Prims.of_int (6)) - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (41))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -776,17 +741,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (140)) + (Prims.of_int (127)) (Prims.of_int (18)) - (Prims.of_int (140)) + (Prims.of_int (127)) (Prims.of_int (72))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (140)) + (Prims.of_int (127)) (Prims.of_int (75)) - (Prims.of_int (143)) + (Prims.of_int (130)) (Prims.of_int (64))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -805,17 +770,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (141)) + (Prims.of_int (128)) (Prims.of_int (21)) - (Prims.of_int (141)) + (Prims.of_int (128)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (143)) + (Prims.of_int (130)) (Prims.of_int (12)) - (Prims.of_int (143)) + (Prims.of_int (130)) (Prims.of_int (63))))) (Obj.magic (rebuild_abs @@ -871,17 +836,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (149)) + (Prims.of_int (136)) (Prims.of_int (14)) - (Prims.of_int (150)) + (Prims.of_int (137)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (148)) + (Prims.of_int (135)) (Prims.of_int (12)) - (Prims.of_int (150)) + (Prims.of_int (137)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -889,9 +854,9 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (150)) + (Prims.of_int (137)) (Prims.of_int (18)) - (Prims.of_int (150)) + (Prims.of_int (137)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic @@ -935,17 +900,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (152)) + (Prims.of_int (139)) (Prims.of_int (18)) - (Prims.of_int (152)) + (Prims.of_int (139)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (151)) + (Prims.of_int (138)) (Prims.of_int (31)) - (Prims.of_int (162)) + (Prims.of_int (149)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_NamedView.inspect @@ -967,17 +932,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (155)) + (Prims.of_int (142)) (Prims.of_int (25)) - (Prims.of_int (155)) + (Prims.of_int (142)) (Prims.of_int (91))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (154)) + (Prims.of_int (141)) (Prims.of_int (14)) - (Prims.of_int (155)) + (Prims.of_int (142)) (Prims.of_int (91))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -985,9 +950,9 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (155)) + (Prims.of_int (142)) (Prims.of_int (68)) - (Prims.of_int (155)) + (Prims.of_int (142)) (Prims.of_int (90))))) (FStar_Sealed.seal (Obj.magic @@ -1028,17 +993,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (159)) + (Prims.of_int (146)) (Prims.of_int (20)) - (Prims.of_int (161)) + (Prims.of_int (148)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (158)) + (Prims.of_int (145)) (Prims.of_int (16)) - (Prims.of_int (161)) + (Prims.of_int (148)) (Prims.of_int (52))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1046,9 +1011,9 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (161)) + (Prims.of_int (148)) (Prims.of_int (22)) - (Prims.of_int (161)) + (Prims.of_int (148)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic @@ -1132,17 +1097,17 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (172)) + (Prims.of_int (159)) (Prims.of_int (12)) - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (171)) + (Prims.of_int (158)) (Prims.of_int (8)) - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (41))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1150,9 +1115,9 @@ let rec (rebuild_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (16)) - (Prims.of_int (173)) + (Prims.of_int (160)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic @@ -1194,22 +1159,22 @@ let rec (rebuild_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (178)) (Prims.of_int (16)) - (Prims.of_int (179)) (Prims.of_int (47))))) + (Prims.of_int (165)) (Prims.of_int (16)) + (Prims.of_int (166)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (177)) (Prims.of_int (6)) - (Prims.of_int (179)) (Prims.of_int (47))))) + (Prims.of_int (164)) (Prims.of_int (6)) + (Prims.of_int (166)) (Prims.of_int (47))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (179)) + (Prims.of_int (166)) (Prims.of_int (22)) - (Prims.of_int (179)) + (Prims.of_int (166)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic @@ -1245,12 +1210,12 @@ let (preprocess_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (185)) (Prims.of_int (19)) - (Prims.of_int (185)) (Prims.of_int (35))))) + (Prims.of_int (172)) (Prims.of_int (19)) + (Prims.of_int (172)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (185)) (Prims.of_int (3)) (Prims.of_int (190)) + (Prims.of_int (172)) (Prims.of_int (3)) (Prims.of_int (177)) (Prims.of_int (7))))) (Obj.magic (arrow_of_abs g t)) (fun uu___ -> (fun uu___ -> @@ -1261,13 +1226,13 @@ let (preprocess_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (186)) (Prims.of_int (4)) - (Prims.of_int (186)) (Prims.of_int (88))))) + (Prims.of_int (173)) (Prims.of_int (4)) + (Prims.of_int (173)) (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (186)) (Prims.of_int (89)) - (Prims.of_int (190)) (Prims.of_int (7))))) + (Prims.of_int (173)) (Prims.of_int (89)) + (Prims.of_int (177)) (Prims.of_int (7))))) (Obj.magic (debug_abs g (fun uu___1 -> @@ -1276,9 +1241,9 @@ let (preprocess_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (186)) + (Prims.of_int (173)) (Prims.of_int (63)) - (Prims.of_int (186)) + (Prims.of_int (173)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic @@ -1303,17 +1268,17 @@ let (preprocess_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (187)) + (Prims.of_int (174)) (Prims.of_int (19)) - (Prims.of_int (187)) + (Prims.of_int (174)) (Prims.of_int (77))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (186)) + (Prims.of_int (173)) (Prims.of_int (89)) - (Prims.of_int (190)) + (Prims.of_int (177)) (Prims.of_int (7))))) (Obj.magic (Pulse_Checker_Pure.instantiate_term_implicits @@ -1328,17 +1293,17 @@ let (preprocess_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (188)) + (Prims.of_int (175)) (Prims.of_int (14)) - (Prims.of_int (188)) + (Prims.of_int (175)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (189)) + (Prims.of_int (176)) (Prims.of_int (4)) - (Prims.of_int (190)) + (Prims.of_int (177)) (Prims.of_int (7))))) (Obj.magic (rebuild_abs g t1 annot1)) @@ -1350,17 +1315,17 @@ let (preprocess_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (189)) + (Prims.of_int (176)) (Prims.of_int (4)) - (Prims.of_int (189)) + (Prims.of_int (176)) (Prims.of_int (88))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (188)) + (Prims.of_int (175)) (Prims.of_int (8)) - (Prims.of_int (188)) + (Prims.of_int (175)) (Prims.of_int (11))))) (Obj.magic (debug_abs g @@ -1371,9 +1336,9 @@ let (preprocess_abs : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (189)) + (Prims.of_int (176)) (Prims.of_int (62)) - (Prims.of_int (189)) + (Prims.of_int (176)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic @@ -1481,13 +1446,13 @@ let (check_effect_annotation : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (214)) (Prims.of_int (12)) - (Prims.of_int (214)) (Prims.of_int (42))))) + (Prims.of_int (201)) (Prims.of_int (12)) + (Prims.of_int (201)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (215)) (Prims.of_int (2)) - (Prims.of_int (264)) (Prims.of_int (7))))) + (Prims.of_int (202)) (Prims.of_int (2)) + (Prims.of_int (251)) (Prims.of_int (7))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> Prims.Mkdtuple2 @@ -1529,17 +1494,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (233)) + (Prims.of_int (220)) (Prims.of_int (14)) - (Prims.of_int (233)) + (Prims.of_int (220)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (233)) + (Prims.of_int (220)) (Prims.of_int (53)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1554,17 +1519,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (234)) + (Prims.of_int (221)) (Prims.of_int (16)) - (Prims.of_int (234)) + (Prims.of_int (221)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (234)) + (Prims.of_int (221)) (Prims.of_int (39)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1578,17 +1543,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (235)) + (Prims.of_int (222)) (Prims.of_int (19)) - (Prims.of_int (235)) + (Prims.of_int (222)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (235)) + (Prims.of_int (222)) (Prims.of_int (51)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1604,17 +1569,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (238)) + (Prims.of_int (225)) (Prims.of_int (16)) - (Prims.of_int (238)) + (Prims.of_int (225)) (Prims.of_int (89))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (239)) + (Prims.of_int (226)) (Prims.of_int (6)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.with_policy @@ -1633,17 +1598,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (239)) + (Prims.of_int (226)) (Prims.of_int (6)) - (Prims.of_int (246)) + (Prims.of_int (233)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (246)) + (Prims.of_int (233)) (Prims.of_int (8)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (if FStar_Pervasives_Native.uu___is_None @@ -1656,17 +1621,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (241)) + (Prims.of_int (228)) (Prims.of_int (47)) - (Prims.of_int (245)) + (Prims.of_int (232)) (Prims.of_int (9))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (241)) + (Prims.of_int (228)) (Prims.of_int (8)) - (Prims.of_int (245)) + (Prims.of_int (232)) (Prims.of_int (9))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1674,17 +1639,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (241)) + (Prims.of_int (228)) (Prims.of_int (47)) - (Prims.of_int (245)) + (Prims.of_int (232)) (Prims.of_int (9))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1692,17 +1657,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1710,17 +1675,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (74)) - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (80))))) (Obj.magic (Pulse_PP.pp @@ -1747,17 +1712,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1765,17 +1730,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (93))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1783,17 +1748,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (87)) - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (93))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (93))))) (Obj.magic (Pulse_PP.pp @@ -1904,17 +1869,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (233)) + (Prims.of_int (220)) (Prims.of_int (14)) - (Prims.of_int (233)) + (Prims.of_int (220)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (233)) + (Prims.of_int (220)) (Prims.of_int (53)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1929,17 +1894,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (234)) + (Prims.of_int (221)) (Prims.of_int (16)) - (Prims.of_int (234)) + (Prims.of_int (221)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (234)) + (Prims.of_int (221)) (Prims.of_int (39)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> @@ -1953,17 +1918,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (235)) + (Prims.of_int (222)) (Prims.of_int (19)) - (Prims.of_int (235)) + (Prims.of_int (222)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (235)) + (Prims.of_int (222)) (Prims.of_int (51)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1979,17 +1944,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (238)) + (Prims.of_int (225)) (Prims.of_int (16)) - (Prims.of_int (238)) + (Prims.of_int (225)) (Prims.of_int (89))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (239)) + (Prims.of_int (226)) (Prims.of_int (6)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.with_policy @@ -2008,17 +1973,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (239)) + (Prims.of_int (226)) (Prims.of_int (6)) - (Prims.of_int (246)) + (Prims.of_int (233)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (246)) + (Prims.of_int (233)) (Prims.of_int (8)) - (Prims.of_int (255)) + (Prims.of_int (242)) (Prims.of_int (20))))) (if FStar_Pervasives_Native.uu___is_None @@ -2031,17 +1996,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (241)) + (Prims.of_int (228)) (Prims.of_int (47)) - (Prims.of_int (245)) + (Prims.of_int (232)) (Prims.of_int (9))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (241)) + (Prims.of_int (228)) (Prims.of_int (8)) - (Prims.of_int (245)) + (Prims.of_int (232)) (Prims.of_int (9))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2049,17 +2014,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (241)) + (Prims.of_int (228)) (Prims.of_int (47)) - (Prims.of_int (245)) + (Prims.of_int (232)) (Prims.of_int (9))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2067,17 +2032,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2085,17 +2050,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (74)) - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (80))))) (Obj.magic (Pulse_PP.pp @@ -2122,17 +2087,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (242)) + (Prims.of_int (229)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2140,17 +2105,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (93))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (244)) + (Prims.of_int (231)) (Prims.of_int (27))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2158,17 +2123,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (87)) - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (93))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (10)) - (Prims.of_int (243)) + (Prims.of_int (230)) (Prims.of_int (93))))) (Obj.magic (Pulse_PP.pp @@ -2269,17 +2234,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (259)) + (Prims.of_int (246)) (Prims.of_int (26)) - (Prims.of_int (264)) + (Prims.of_int (251)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (259)) + (Prims.of_int (246)) (Prims.of_int (6)) - (Prims.of_int (264)) + (Prims.of_int (251)) (Prims.of_int (7))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2287,17 +2252,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (260)) + (Prims.of_int (247)) (Prims.of_int (8)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (259)) + (Prims.of_int (246)) (Prims.of_int (26)) - (Prims.of_int (264)) + (Prims.of_int (251)) (Prims.of_int (7))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2305,17 +2270,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (260)) + (Prims.of_int (247)) (Prims.of_int (8)) - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (260)) + (Prims.of_int (247)) (Prims.of_int (8)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2323,17 +2288,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (22)) - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (58))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (260)) + (Prims.of_int (247)) (Prims.of_int (8)) - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (58))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2341,17 +2306,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (40)) - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (22)) - (Prims.of_int (261)) + (Prims.of_int (248)) (Prims.of_int (58))))) (Obj.magic (Pulse_Syntax_Printer.tag_of_comp @@ -2379,17 +2344,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (262)) + (Prims.of_int (249)) (Prims.of_int (8)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (260)) + (Prims.of_int (247)) (Prims.of_int (8)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2397,17 +2362,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (22)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (262)) + (Prims.of_int (249)) (Prims.of_int (8)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2415,17 +2380,17 @@ let (check_effect_annotation : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (40)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (66))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (22)) - (Prims.of_int (263)) + (Prims.of_int (250)) (Prims.of_int (67))))) (Obj.magic (Pulse_Syntax_Printer.tag_of_comp @@ -2503,17 +2468,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (278)) + (Prims.of_int (265)) (Prims.of_int (19)) - (Prims.of_int (278)) + (Prims.of_int (265)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (277)) + (Prims.of_int (264)) (Prims.of_int (20)) - (Prims.of_int (291)) + (Prims.of_int (278)) (Prims.of_int (7))))) (Obj.magic (Pulse_Checker_Pure.instantiate_term_implicits @@ -2528,17 +2493,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (279)) + (Prims.of_int (266)) (Prims.of_int (32)) - (Prims.of_int (279)) + (Prims.of_int (266)) (Prims.of_int (69))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (278)) + (Prims.of_int (265)) (Prims.of_int (76)) - (Prims.of_int (290)) + (Prims.of_int (277)) (Prims.of_int (26))))) (Obj.magic (Pulse_Checker_Pure.check_universe @@ -2555,17 +2520,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (280)) + (Prims.of_int (267)) (Prims.of_int (14)) - (Prims.of_int (281)) + (Prims.of_int (268)) (Prims.of_int (51))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (280)) + (Prims.of_int (267)) (Prims.of_int (8)) - (Prims.of_int (290)) + (Prims.of_int (277)) (Prims.of_int (26))))) (Obj.magic (Pulse_Checker_Base.norm_st_typing_inverse @@ -2597,17 +2562,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (286)) + (Prims.of_int (273)) (Prims.of_int (10)) - (Prims.of_int (289)) + (Prims.of_int (276)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (290)) + (Prims.of_int (277)) (Prims.of_int (10)) - (Prims.of_int (290)) + (Prims.of_int (277)) (Prims.of_int (26))))) (Obj.magic (debug_abs @@ -2619,17 +2584,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (289)) + (Prims.of_int (276)) (Prims.of_int (14)) - (Prims.of_int (289)) + (Prims.of_int (276)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (287)) + (Prims.of_int (274)) (Prims.of_int (22)) - (Prims.of_int (289)) + (Prims.of_int (276)) (Prims.of_int (42))))) (Obj.magic (Pulse_Syntax_Printer.comp_to_string @@ -2645,17 +2610,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (287)) + (Prims.of_int (274)) (Prims.of_int (22)) - (Prims.of_int (289)) + (Prims.of_int (276)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (287)) + (Prims.of_int (274)) (Prims.of_int (22)) - (Prims.of_int (289)) + (Prims.of_int (276)) (Prims.of_int (42))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -2663,9 +2628,9 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (288)) + (Prims.of_int (275)) (Prims.of_int (14)) - (Prims.of_int (288)) + (Prims.of_int (275)) (Prims.of_int (34))))) (FStar_Sealed.seal (Obj.magic @@ -2723,17 +2688,17 @@ let (maybe_rewrite_body_typing : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (296)) + (Prims.of_int (283)) (Prims.of_int (15)) - (Prims.of_int (296)) + (Prims.of_int (283)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (297)) + (Prims.of_int (284)) (Prims.of_int (6)) - (Prims.of_int (297)) + (Prims.of_int (284)) (Prims.of_int (92))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> @@ -2782,13 +2747,13 @@ let rec (check_abs_core : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (312)) (Prims.of_int (14)) - (Prims.of_int (312)) (Prims.of_int (21))))) + (Prims.of_int (299)) (Prims.of_int (14)) + (Prims.of_int (299)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (313)) (Prims.of_int (2)) - (Prims.of_int (447)) (Prims.of_int (29))))) + (Prims.of_int (300)) (Prims.of_int (2)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> t.Pulse_Syntax_Base.range1)) (fun uu___ -> @@ -2809,13 +2774,13 @@ let rec (check_abs_core : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (316)) (Prims.of_int (24)) - (Prims.of_int (316)) (Prims.of_int (49))))) + (Prims.of_int (303)) (Prims.of_int (24)) + (Prims.of_int (303)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (314)) (Prims.of_int (99)) - (Prims.of_int (447)) (Prims.of_int (29))))) + (Prims.of_int (301)) (Prims.of_int (99)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (Pulse_Checker_Pure.compute_tot_term_type g t1)) (fun uu___ -> @@ -2829,17 +2794,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (317)) + (Prims.of_int (304)) (Prims.of_int (28)) - (Prims.of_int (317)) + (Prims.of_int (304)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (316)) + (Prims.of_int (303)) (Prims.of_int (52)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (Pulse_Checker_Pure.check_universe @@ -2855,17 +2820,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (318)) + (Prims.of_int (305)) (Prims.of_int (12)) - (Prims.of_int (318)) + (Prims.of_int (305)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (318)) + (Prims.of_int (305)) (Prims.of_int (22)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___4 -> @@ -2879,17 +2844,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (319)) + (Prims.of_int (306)) (Prims.of_int (13)) - (Prims.of_int (319)) + (Prims.of_int (306)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (319)) + (Prims.of_int (306)) (Prims.of_int (25)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2906,17 +2871,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (320)) + (Prims.of_int (307)) (Prims.of_int (14)) - (Prims.of_int (320)) + (Prims.of_int (307)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (320)) + (Prims.of_int (307)) (Prims.of_int (53)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2938,17 +2903,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (321)) + (Prims.of_int (308)) (Prims.of_int (13)) - (Prims.of_int (321)) + (Prims.of_int (308)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (321)) + (Prims.of_int (308)) (Prims.of_int (41)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2966,17 +2931,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (322)) + (Prims.of_int (309)) (Prims.of_int (22)) - (Prims.of_int (322)) + (Prims.of_int (309)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (322)) + (Prims.of_int (309)) (Prims.of_int (48)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2994,17 +2959,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (323)) + (Prims.of_int (310)) (Prims.of_int (14)) - (Prims.of_int (323)) + (Prims.of_int (310)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (324)) + (Prims.of_int (311)) (Prims.of_int (4)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3027,17 +2992,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (327)) + (Prims.of_int (314)) (Prims.of_int (44)) - (Prims.of_int (327)) + (Prims.of_int (314)) (Prims.of_int (79))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (325)) + (Prims.of_int (312)) (Prims.of_int (17)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (Obj.magic (check_abs_core @@ -3062,17 +3027,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (331)) + (Prims.of_int (318)) (Prims.of_int (8)) - (Prims.of_int (335)) + (Prims.of_int (322)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (327)) + (Prims.of_int (314)) (Prims.of_int (82)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3080,17 +3045,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (331)) + (Prims.of_int (318)) (Prims.of_int (14)) - (Prims.of_int (331)) + (Prims.of_int (318)) (Prims.of_int (54))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (331)) + (Prims.of_int (318)) (Prims.of_int (8)) - (Prims.of_int (335)) + (Prims.of_int (322)) (Prims.of_int (35))))) (Obj.magic (sub_effect_comp @@ -3142,17 +3107,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (336)) + (Prims.of_int (323)) (Prims.of_int (8)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (336)) + (Prims.of_int (323)) (Prims.of_int (8)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3168,17 +3133,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (340)) + (Prims.of_int (327)) (Prims.of_int (32)) - (Prims.of_int (340)) + (Prims.of_int (327)) (Prims.of_int (80))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (336)) + (Prims.of_int (323)) (Prims.of_int (8)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (Obj.magic (check_effect_annotation @@ -3202,17 +3167,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (341)) + (Prims.of_int (328)) (Prims.of_int (24)) - (Prims.of_int (341)) + (Prims.of_int (328)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (341)) + (Prims.of_int (328)) (Prims.of_int (58)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3235,17 +3200,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (345)) + (Prims.of_int (332)) (Prims.of_int (38)) - (Prims.of_int (345)) + (Prims.of_int (332)) (Prims.of_int (79))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (341)) + (Prims.of_int (328)) (Prims.of_int (58)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (Obj.magic (maybe_rewrite_body_typing @@ -3270,17 +3235,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (348)) + (Prims.of_int (335)) (Prims.of_int (24)) - (Prims.of_int (348)) + (Prims.of_int (335)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (349)) + (Prims.of_int (336)) (Prims.of_int (50)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3300,17 +3265,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (353)) + (Prims.of_int (340)) (Prims.of_int (8)) - (Prims.of_int (356)) + (Prims.of_int (343)) (Prims.of_int (28))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (6)) - (Prims.of_int (361)) + (Prims.of_int (348)) (Prims.of_int (29))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3318,17 +3283,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (353)) + (Prims.of_int (340)) (Prims.of_int (8)) - (Prims.of_int (355)) + (Prims.of_int (342)) (Prims.of_int (92))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (353)) + (Prims.of_int (340)) (Prims.of_int (8)) - (Prims.of_int (356)) + (Prims.of_int (343)) (Prims.of_int (28))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3336,17 +3301,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (353)) + (Prims.of_int (340)) (Prims.of_int (8)) - (Prims.of_int (354)) + (Prims.of_int (341)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (353)) + (Prims.of_int (340)) (Prims.of_int (8)) - (Prims.of_int (355)) + (Prims.of_int (342)) (Prims.of_int (92))))) (Obj.magic (FStar_Tactics_Unseal.unseal @@ -3366,17 +3331,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (355)) + (Prims.of_int (342)) (Prims.of_int (30)) - (Prims.of_int (355)) + (Prims.of_int (342)) (Prims.of_int (84))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (355)) + (Prims.of_int (342)) (Prims.of_int (30)) - (Prims.of_int (355)) + (Prims.of_int (342)) (Prims.of_int (91))))) (Obj.magic (Pulse_Checker_Pure.instantiate_term_implicits @@ -3478,17 +3443,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (364)) + (Prims.of_int (351)) (Prims.of_int (8)) - (Prims.of_int (398)) + (Prims.of_int (385)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (362)) + (Prims.of_int (349)) (Prims.of_int (10)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (match asc1.Pulse_Syntax_Base.elaborated @@ -3512,17 +3477,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (371)) + (Prims.of_int (358)) (Prims.of_int (21)) - (Prims.of_int (373)) + (Prims.of_int (360)) (Prims.of_int (53))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (369)) + (Prims.of_int (356)) (Prims.of_int (28)) - (Prims.of_int (374)) + (Prims.of_int (361)) (Prims.of_int (9))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -3530,9 +3495,9 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (373)) + (Prims.of_int (360)) (Prims.of_int (24)) - (Prims.of_int (373)) + (Prims.of_int (360)) (Prims.of_int (52))))) (FStar_Sealed.seal (Obj.magic @@ -3575,17 +3540,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (378)) + (Prims.of_int (365)) (Prims.of_int (12)) - (Prims.of_int (386)) + (Prims.of_int (373)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (394)) + (Prims.of_int (381)) (Prims.of_int (10)) - (Prims.of_int (398)) + (Prims.of_int (385)) (Prims.of_int (47))))) (if (Pulse_Syntax_Base.uu___is_C_STGhost @@ -3600,17 +3565,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (379)) + (Prims.of_int (366)) (Prims.of_int (26)) - (Prims.of_int (379)) + (Prims.of_int (366)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (379)) + (Prims.of_int (366)) (Prims.of_int (60)) - (Prims.of_int (384)) + (Prims.of_int (371)) (Prims.of_int (19))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3628,17 +3593,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (380)) + (Prims.of_int (367)) (Prims.of_int (26)) - (Prims.of_int (382)) + (Prims.of_int (369)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (380)) + (Prims.of_int (367)) (Prims.of_int (17)) - (Prims.of_int (380)) + (Prims.of_int (367)) (Prims.of_int (23))))) (Obj.magic (FStar_Tactics_V2_Builtins.norm_well_typed_term @@ -3720,17 +3685,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (400)) + (Prims.of_int (387)) (Prims.of_int (41)) - (Prims.of_int (400)) + (Prims.of_int (387)) (Prims.of_int (67))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (399)) + (Prims.of_int (386)) (Prims.of_int (8)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (Pulse_Checker_Pure.check_slprop @@ -3753,17 +3718,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (401)) + (Prims.of_int (388)) (Prims.of_int (16)) - (Prims.of_int (401)) + (Prims.of_int (388)) (Prims.of_int (39))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (401)) + (Prims.of_int (388)) (Prims.of_int (42)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3781,17 +3746,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (403)) + (Prims.of_int (390)) (Prims.of_int (8)) - (Prims.of_int (416)) + (Prims.of_int (403)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (417)) + (Prims.of_int (404)) (Prims.of_int (8)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (match post_hint_body with @@ -3815,17 +3780,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (410)) + (Prims.of_int (397)) (Prims.of_int (14)) - (Prims.of_int (414)) + (Prims.of_int (401)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (416)) + (Prims.of_int (403)) (Prims.of_int (10)) - (Prims.of_int (416)) + (Prims.of_int (403)) (Prims.of_int (31))))) (Obj.magic (Pulse_Checker_Base.intro_post_hint @@ -3854,17 +3819,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (419)) + (Prims.of_int (406)) (Prims.of_int (23)) - (Prims.of_int (419)) + (Prims.of_int (406)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (419)) + (Prims.of_int (406)) (Prims.of_int (52)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3882,17 +3847,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (420)) + (Prims.of_int (407)) (Prims.of_int (15)) - (Prims.of_int (420)) + (Prims.of_int (407)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (420)) + (Prims.of_int (407)) (Prims.of_int (77)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (check g' @@ -3909,17 +3874,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (422)) + (Prims.of_int (409)) (Prims.of_int (8)) - (Prims.of_int (422)) + (Prims.of_int (409)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (420)) + (Prims.of_int (407)) (Prims.of_int (77)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (Pulse_Checker_Base.apply_checker_result_k @@ -3946,17 +3911,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (422)) + (Prims.of_int (409)) (Prims.of_int (68)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (422)) + (Prims.of_int (409)) (Prims.of_int (68)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -3972,17 +3937,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (424)) + (Prims.of_int (411)) (Prims.of_int (41)) - (Prims.of_int (424)) + (Prims.of_int (411)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (424)) + (Prims.of_int (411)) (Prims.of_int (106)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -4008,17 +3973,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (428)) + (Prims.of_int (415)) (Prims.of_int (8)) - (Prims.of_int (432)) + (Prims.of_int (419)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (424)) + (Prims.of_int (411)) (Prims.of_int (106)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -4026,17 +3991,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (428)) + (Prims.of_int (415)) (Prims.of_int (14)) - (Prims.of_int (428)) + (Prims.of_int (415)) (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (428)) + (Prims.of_int (415)) (Prims.of_int (8)) - (Prims.of_int (432)) + (Prims.of_int (419)) (Prims.of_int (35))))) (Obj.magic (sub_effect_comp @@ -4089,17 +4054,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (433)) + (Prims.of_int (420)) (Prims.of_int (8)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (433)) + (Prims.of_int (420)) (Prims.of_int (8)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -4117,17 +4082,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (435)) + (Prims.of_int (422)) (Prims.of_int (32)) - (Prims.of_int (435)) + (Prims.of_int (422)) (Prims.of_int (85))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (433)) + (Prims.of_int (420)) (Prims.of_int (8)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (check_effect_annotation @@ -4153,17 +4118,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (436)) + (Prims.of_int (423)) (Prims.of_int (24)) - (Prims.of_int (436)) + (Prims.of_int (423)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (436)) + (Prims.of_int (423)) (Prims.of_int (58)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -4188,17 +4153,17 @@ let rec (check_abs_core : (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (438)) + (Prims.of_int (425)) (Prims.of_int (38)) - (Prims.of_int (438)) + (Prims.of_int (425)) (Prims.of_int (79))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (436)) + (Prims.of_int (423)) (Prims.of_int (58)) - (Prims.of_int (447)) + (Prims.of_int (434)) (Prims.of_int (29))))) (Obj.magic (maybe_rewrite_body_typing @@ -4312,13 +4277,13 @@ let (check_abs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (451)) (Prims.of_int (10)) - (Prims.of_int (451)) (Prims.of_int (28))))) + (Prims.of_int (438)) (Prims.of_int (10)) + (Prims.of_int (438)) (Prims.of_int (28))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Abs.fst" - (Prims.of_int (452)) (Prims.of_int (2)) - (Prims.of_int (452)) (Prims.of_int (26))))) + (Prims.of_int (439)) (Prims.of_int (2)) + (Prims.of_int (439)) (Prims.of_int (26))))) (Obj.magic (preprocess_abs g t)) (fun uu___ -> (fun t1 -> Obj.magic (check_abs_core g t1 check)) uu___) \ No newline at end of file diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml index 0a7c9e90a..4fdbbd98e 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml @@ -649,13 +649,13 @@ let (check_branch : (Prims.of_int (249)) (Prims.of_int (15)) (Prims.of_int (249)) - (Prims.of_int (67))))) + (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Checker.Match.fst" (Prims.of_int (249)) - (Prims.of_int (70)) + (Prims.of_int (51)) (Prims.of_int (274)) (Prims.of_int (58))))) (FStar_Tactics_Effect.lift_div_tac @@ -664,9 +664,7 @@ let (check_branch : Pulse_Typing.mk_sq_eq2 sc_u sc_ty sc - (Pulse_Syntax_Pure.wr - elab_p_tm - FStar_Range.range_0))) + elab_p_tm)) (fun uu___2 -> (fun diff --git a/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml b/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml index 15f6c443d..95ae234cd 100644 --- a/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml +++ b/src/ocaml/plugin/generated/Pulse_Elaborate_Core.ml @@ -170,6 +170,7 @@ let (elab_lift : (Pulse_Syntax_Base.comp_post c1)) e let (intro_pure_tm : Pulse_Syntax_Base.term -> Pulse_Syntax_Base.st_term) = fun p -> + let rng = FStar_Reflection_V2_Builtins.range_of_term p in Pulse_Typing.wtag (FStar_Pervasives_Native.Some Pulse_Syntax_Base.STT_Ghost) (Pulse_Syntax_Base.Tm_STApp @@ -185,7 +186,7 @@ let (intro_pure_tm : Pulse_Syntax_Base.term -> Pulse_Syntax_Base.st_term) = (Pulse_Syntax_Pure.wr (FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_Const - FStar_Reflection_V2_Data.C_Unit)) FStar_Range.range_0) + FStar_Reflection_V2_Data.C_Unit)) rng) }) let (simple_arr : FStar_Reflection_Types.term -> diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml index 5ae8593aa..5547aec28 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml @@ -127,6 +127,17 @@ let (__proj__C_STGhost__item__inames : comp -> term) = fun projectee -> match projectee with | C_STGhost (inames, _1) -> inames let (__proj__C_STGhost__item___1 : comp -> st_comp) = fun projectee -> match projectee with | C_STGhost (inames, _1) -> _1 +let (range_of_st_comp : st_comp -> FStar_Range.range) = + fun st -> + Pulse_RuntimeUtils.union_ranges (Pulse_RuntimeUtils.range_of_term st.pre) + (Pulse_RuntimeUtils.range_of_term st.post) +let (range_of_comp : comp -> FStar_Range.range) = + fun c -> + match c with + | C_Tot t -> Pulse_RuntimeUtils.range_of_term t + | C_ST st -> range_of_st_comp st + | C_STAtomic (uu___, uu___1, st) -> range_of_st_comp st + | C_STGhost (uu___, st) -> range_of_st_comp st type comp_st = comp type pattern = | Pat_Cons of fv * (pattern * Prims.bool) Prims.list @@ -889,32 +900,32 @@ let (ppname_for_uvar : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Syntax.Base.fsti" - (Prims.of_int (414)) (Prims.of_int (18)) (Prims.of_int (414)) + (Prims.of_int (416)) (Prims.of_int (18)) (Prims.of_int (416)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Syntax.Base.fsti" - (Prims.of_int (414)) (Prims.of_int (4)) (Prims.of_int (414)) + (Prims.of_int (416)) (Prims.of_int (4)) (Prims.of_int (416)) (Prims.of_int (49))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Syntax.Base.fsti" - (Prims.of_int (414)) (Prims.of_int (25)) - (Prims.of_int (414)) (Prims.of_int (48))))) + (Prims.of_int (416)) (Prims.of_int (25)) + (Prims.of_int (416)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Syntax.Base.fsti" - (Prims.of_int (414)) (Prims.of_int (18)) - (Prims.of_int (414)) (Prims.of_int (48))))) + (Prims.of_int (416)) (Prims.of_int (18)) + (Prims.of_int (416)) (Prims.of_int (48))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "Pulse.Syntax.Base.fsti" - (Prims.of_int (414)) (Prims.of_int (32)) - (Prims.of_int (414)) (Prims.of_int (47))))) + (Prims.of_int (416)) (Prims.of_int (32)) + (Prims.of_int (416)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "prims.fst" diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Pure.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Pure.ml index ec28b038a..71dd88928 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Pure.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Pure.ml @@ -80,37 +80,37 @@ let (tm_uinst : l.Pulse_Syntax_Base.fv_range let (tm_constant : Pulse_Syntax_Base.constant -> Pulse_Syntax_Base.term) = fun c -> - Pulse_RuntimeUtils.set_range - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_Const c)) FStar_Range.range_0 + FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_Const c) let (tm_refine : Pulse_Syntax_Base.binder -> - Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term) + Pulse_Syntax_Base.term -> FStar_Range.range -> Pulse_Syntax_Base.term) = fun b -> fun t -> - let rb = - FStar_Reflection_Typing.mk_simple_binder - (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name - b.Pulse_Syntax_Base.binder_ty in - Pulse_RuntimeUtils.set_range - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_Refine (rb, t))) FStar_Range.range_0 + fun rng -> + let rb = + FStar_Reflection_Typing.mk_simple_binder + (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name + b.Pulse_Syntax_Base.binder_ty in + Pulse_RuntimeUtils.set_range + (FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_Refine (rb, t))) rng let (tm_let : Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term -> - Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term) + Pulse_Syntax_Base.term -> FStar_Range.range -> Pulse_Syntax_Base.term) = fun t -> fun e1 -> fun e2 -> - let rb = - FStar_Reflection_Typing.mk_simple_binder - FStar_Reflection_Typing.pp_name_default t in - Pulse_RuntimeUtils.set_range - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_Let (false, [], rb, e1, e2))) - FStar_Range.range_0 + fun rng -> + let rb = + FStar_Reflection_Typing.mk_simple_binder + FStar_Reflection_Typing.pp_name_default t in + Pulse_RuntimeUtils.set_range + (FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_Let (false, [], rb, e1, e2))) rng let (tm_pureapp : Pulse_Syntax_Base.term -> Pulse_Syntax_Base.qualifier FStar_Pervasives_Native.option -> @@ -121,30 +121,34 @@ let (tm_pureapp : fun arg -> Pulse_RuntimeUtils.set_range (FStar_Reflection_V2_Derived.mk_app head - [(arg, (Pulse_Elaborate_Pure.elab_qual q))]) FStar_Range.range_0 + [(arg, (Pulse_Elaborate_Pure.elab_qual q))]) + (Pulse_RuntimeUtils.union_ranges + (Pulse_RuntimeUtils.range_of_term head) + (Pulse_RuntimeUtils.range_of_term arg)) let (tm_pureabs : FStar_Reflection_V2_Data.ppname_t -> Pulse_Syntax_Base.term -> Pulse_Syntax_Base.qualifier FStar_Pervasives_Native.option -> - Pulse_Syntax_Base.term -> Pulse_Syntax_Base.term) + Pulse_Syntax_Base.term -> FStar_Range.range -> Pulse_Syntax_Base.term) = fun ppname -> fun ty -> fun q -> fun body -> - let b = - { - FStar_Tactics_NamedView.uniq = Prims.int_zero; - FStar_Tactics_NamedView.ppname = ppname; - FStar_Tactics_NamedView.sort = ty; - FStar_Tactics_NamedView.qual = - (Pulse_Elaborate_Pure.elab_qual q); - FStar_Tactics_NamedView.attrs = [] - } in - let r = - FStar_Tactics_NamedView.pack - (FStar_Tactics_NamedView.Tv_Abs (b, body)) in - Pulse_RuntimeUtils.set_range r FStar_Range.range_0 + fun rng -> + let b = + { + FStar_Tactics_NamedView.uniq = Prims.int_zero; + FStar_Tactics_NamedView.ppname = ppname; + FStar_Tactics_NamedView.sort = ty; + FStar_Tactics_NamedView.qual = + (Pulse_Elaborate_Pure.elab_qual q); + FStar_Tactics_NamedView.attrs = [] + } in + let r = + FStar_Tactics_NamedView.pack + (FStar_Tactics_NamedView.Tv_Abs (b, body)) in + Pulse_RuntimeUtils.set_range r rng let (tm_arrow : Pulse_Syntax_Base.binder -> Pulse_Syntax_Base.qualifier FStar_Pervasives_Native.option -> @@ -158,7 +162,10 @@ let (tm_arrow : (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name ((b.Pulse_Syntax_Base.binder_ty), (Pulse_Elaborate_Pure.elab_qual q)) - (Pulse_Elaborate_Pure.elab_comp c)) FStar_Range.range_0 + (Pulse_Elaborate_Pure.elab_comp c)) + (Pulse_RuntimeUtils.union_ranges + (Pulse_RuntimeUtils.range_of_term b.Pulse_Syntax_Base.binder_ty) + (Pulse_Syntax_Base.range_of_comp c)) let (tm_type : Pulse_Syntax_Base.universe -> Pulse_Syntax_Base.term) = fun u -> FStar_Reflection_Typing.tm_type u let (mk_bvar : diff --git a/src/ocaml/plugin/pulseparser.mly b/src/ocaml/plugin/pulseparser.mly index 43eee8eb5..5a300a3e6 100644 --- a/src/ocaml/plugin/pulseparser.mly +++ b/src/ocaml/plugin/pulseparser.mly @@ -255,6 +255,8 @@ pulseStmtNoSeq: } | bs=withBindersOpt ASSERT p=pulseSLProp { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) bs } + | bs=withBindersOpt ASSUME p=pulseSLProp + { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) bs } | bs=withBindersOpt UNFOLD ns=option(names) p=pulseSLProp { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) bs } | bs=withBindersOpt FOLD ns=option(names) p=pulseSLProp diff --git a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst index b29ebf0e4..05ae1a729 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst @@ -702,6 +702,21 @@ and desugar_sequence (env:env_t) (s1 s2:Sugar.stmt) r and desugar_proof_hint_with_binders (env:env_t) (s1:Sugar.stmt) (k:option Sugar.stmt) r : err SW.st_term = match s1.s with + | Sugar.ProofHintWithBinders { hint_type = Sugar.ASSUME p; binders=[] } -> + let assume_fv = SW.(mk_fv assume_lid r) in + let assume_ : SW.term = SW.(tm_fvar assume_fv) in + let! p = desugar_slprop env p in + let s1 = SW.tm_st_app assume_ None p r in + let! s2 = + match k with + | None -> return (SW.tm_ghost_return (SW.tm_expr S.unit_const r) r) + | Some s2 -> desugar_stmt env s2 in + let annot = SW.mk_binder (Ident.id_of_text "_") (SW.tm_unknown r) in + return (mk_bind annot s1 s2 r) + + | Sugar.ProofHintWithBinders { hint_type = Sugar.ASSUME _; binders=b1::_ } -> + fail "'assume' cannot have binders" b1.brange + | Sugar.ProofHintWithBinders { hint_type; binders=bs } -> //; slprop=v } -> let! env, binders, bvs = desugar_binders env bs in let vars = L.map #_ #nat (fun bv -> bv.S.index) bvs in diff --git a/src/syntax_extension/PulseSyntaxExtension.Env.fst b/src/syntax_extension/PulseSyntaxExtension.Env.fst index 04f12bdf5..28cc30070 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Env.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Env.fst @@ -40,6 +40,7 @@ let r_ = FStar.Compiler.Range.dummyRange let admit_lid = Ident.lid_of_path ["Prims"; "admit"] r_ let pulse_lib_core_lid l = Ident.lid_of_path (["Pulse"; "Lib"; "Core"]@[l]) r_ let pulse_lib_ref_lid l = Ident.lid_of_path (["Pulse"; "Lib"; "Reference"]@[l]) r_ +let assume_lid = pulse_lib_core_lid "assume_" let prims_exists_lid = Ident.lid_of_path ["Prims"; "l_Exists"] r_ let prims_forall_lid = Ident.lid_of_path ["Prims"; "l_Forall"] r_ let unreachable_lid = pulse_lib_core_lid "unreachable" diff --git a/src/syntax_extension/PulseSyntaxExtension.Sugar.fst b/src/syntax_extension/PulseSyntaxExtension.Sugar.fst index 3a3cc9c3b..cc6684010 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Sugar.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Sugar.fst @@ -64,6 +64,7 @@ instance showable_mut_or_ref : showable mut_or_ref = { type hint_type = | ASSERT of slprop + | ASSUME of slprop | UNFOLD of option (list lident) & slprop | FOLD of option (list lident) & slprop | RENAME of @@ -85,6 +86,7 @@ instance showable_slprop : showable slprop = { instance showable_hint_type : showable hint_type = { show = (fun i -> match i with | ASSERT s -> "ASSERT " ^ show s + | ASSUME s -> "ASSUME " ^ show s | UNFOLD (ns, s) -> "UNFOLD " ^ show ns ^ " " ^ show s | FOLD (ns, s) -> "FOLD " ^ show ns ^ " " ^ show s | RENAME (ts, g, t) -> "RENAME " ^ show ts ^ " " ^ show g ^ " " ^ show t @@ -460,6 +462,7 @@ and eq_array_init (a1 a2:array_init) = and eq_hint_type (h1 h2:hint_type) = match h1, h2 with | ASSERT s1, ASSERT s2 -> eq_slprop s1 s2 + | ASSUME s1, ASSUME s2 -> eq_slprop s1 s2 | UNFOLD (ns1, s1), UNFOLD (ns2, s2) -> eq_opt (forall2 eq_lident) ns1 ns2 && eq_slprop s1 s2 @@ -589,6 +592,7 @@ and scan_ensures_slprop (cbs:A.dep_scan_callbacks) (e:ensures_slprop) = and scan_hint_type (cbs:A.dep_scan_callbacks) (h:hint_type) = match h with | ASSERT s -> scan_slprop cbs s + | ASSUME s -> scan_slprop cbs s | UNFOLD (ns, s) -> scan_slprop cbs s | FOLD (ns, s) -> scan_slprop cbs s | RENAME (ts, g, t) -> iter (fun (t1, t2) -> cbs.scan_term t1; cbs.scan_term t2) ts; iopt (scan_slprop cbs) g; iopt cbs.scan_term t