diff --git a/lib/pulse/lib/ml/Pulse_Lib_Core.ml b/lib/pulse/lib/ml/Pulse_Lib_Core.ml index 6f256def0..282ca73af 100644 --- a/lib/pulse/lib/ml/Pulse_Lib_Core.ml +++ b/lib/pulse/lib/ml/Pulse_Lib_Core.ml @@ -2,3 +2,5 @@ let while_ cond body = while (cond ()) do body () done + +let block stmt = stmt () diff --git a/src/checker/Pulse.Extract.Main.fst b/src/checker/Pulse.Extract.Main.fst index 182f71de2..37bed6f7a 100644 --- a/src/checker/Pulse.Extract.Main.fst +++ b/src/checker/Pulse.Extract.Main.fst @@ -421,6 +421,10 @@ let rec simplify_st_term (g:env) (e:st_term) : T.Tac st_term = | Tm_WithInv {body} -> simplify_st_term g body + | Tm_Block { pre; post; stmt } -> + let stmt = simplify_st_term g stmt in + { e with term = Tm_Block { pre; post; stmt } } + | Tm_Unreachable -> e and simplify_branch (g:env) (b:branch) : T.Tac branch = @@ -509,6 +513,10 @@ let rec erase_ghost_subterms (g:env) (p:st_term) : T.Tac st_term = let body = open_erase_close g binder body in ret (Tm_WithLocalArray { binder; initializer; length; body }) + | Tm_Block { pre; post; stmt } -> + let stmt = erase_ghost_subterms g stmt in + ret (Tm_Block { pre; post; stmt }) + | Tm_Unreachable -> p | Tm_Admit _ -> p @@ -666,6 +674,12 @@ let rec extract (g:env) (p:st_term) | Tm_WithInv { body } -> extract g body + | Tm_Block { pre; post; stmt } -> + let stmt, _ = extract g stmt in + let stmt = mle_fun [("_", mlty_unit, [])] stmt in + let b = mle_app (mle_name (["Pulse"; "Lib"; "Core"], "block")) [stmt] in + b, e_tag_impure + | Tm_Unreachable -> mle_app (mle_name (["Pulse"; "Lib"; "Core"], "unreachable")) [mle_unit], e_tag_impure diff --git a/src/checker/Pulse.Syntax.Base.fst b/src/checker/Pulse.Syntax.Base.fst index 1dee8bb07..065badb70 100644 --- a/src/checker/Pulse.Syntax.Base.fst +++ b/src/checker/Pulse.Syntax.Base.fst @@ -255,7 +255,13 @@ let rec eq_st_term (t1 t2:st_term) eq_univ u1 u2 && eq_tm t1 t2 && eq_tm_opt post1 post2 - + + | Tm_Block { pre=pre1; post=post1; stmt=stmt1 }, + Tm_Block { pre=pre2; post=post2; stmt=stmt2 } -> + eq_tm pre1 pre2 && + eq_tm post1 post2 && + eq_st_term stmt1 stmt2 + | Tm_Unreachable, Tm_Unreachable -> true | Tm_ProofHintWithBinders { hint_type=ht1; binders=bs1; t=t1 }, diff --git a/src/checker/Pulse.Syntax.Base.fsti b/src/checker/Pulse.Syntax.Base.fsti index cce5de765..4966823fa 100644 --- a/src/checker/Pulse.Syntax.Base.fsti +++ b/src/checker/Pulse.Syntax.Base.fsti @@ -282,6 +282,11 @@ type st_term' = typ:term; post:option term; } + | Tm_Block { + pre:vprop; + post:vprop; + stmt:st_term; + } | Tm_Unreachable | Tm_ProofHintWithBinders { hint_type:proof_hint_type; diff --git a/src/checker/Pulse.Syntax.Builder.fst b/src/checker/Pulse.Syntax.Builder.fst index fb8d1c854..c9359a6a4 100644 --- a/src/checker/Pulse.Syntax.Builder.fst +++ b/src/checker/Pulse.Syntax.Builder.fst @@ -53,6 +53,7 @@ let tm_add_inv names n r = tm_add_inv names n let tm_with_local binder initializer body = Tm_WithLocal { binder; initializer; body } let tm_with_local_array binder initializer length body = Tm_WithLocalArray { binder; initializer; length; body } let tm_admit ctag u typ post = Tm_Admit { ctag; u; typ; post } +let tm_block pre post stmt = Tm_Block { pre; post; stmt } let tm_unreachable = Tm_Unreachable let with_range t r = { term = t; range = r; effect_tag = default_effect_hint } let tm_assert_with_binders bs p t = Tm_ProofHintWithBinders { hint_type=ASSERT { p }; binders=bs; t } diff --git a/src/checker/Pulse.Syntax.Naming.fst b/src/checker/Pulse.Syntax.Naming.fst index 422cef0b6..2deecee8f 100644 --- a/src/checker/Pulse.Syntax.Naming.fst +++ b/src/checker/Pulse.Syntax.Naming.fst @@ -217,6 +217,11 @@ let rec close_open_inverse_st' (t:st_term) close_open_inverse' typ x i; close_open_inverse_opt' post x (i + 1) + | Tm_Block { pre; post; stmt } -> + close_open_inverse' pre x i; + close_open_inverse' post x i; + close_open_inverse_st' stmt x i + | Tm_Unreachable -> () | Tm_ProofHintWithBinders { binders; hint_type; t} -> diff --git a/src/checker/Pulse.Syntax.Naming.fsti b/src/checker/Pulse.Syntax.Naming.fsti index 4cd46a4e1..829a903d6 100644 --- a/src/checker/Pulse.Syntax.Naming.fsti +++ b/src/checker/Pulse.Syntax.Naming.fsti @@ -150,6 +150,11 @@ let rec freevars_st (t:st_term) Set.union (freevars typ) (freevars_term_opt post) + | Tm_Block { pre; post; stmt } -> + Set.union (freevars pre) + (Set.union (freevars post) + (freevars_st stmt)) + | Tm_Unreachable -> Set.empty @@ -338,6 +343,11 @@ let rec ln_st' (t:st_term) (i:int) ln' typ i && ln_opt' ln' post (i + 1) + | Tm_Block { pre; post; stmt } -> + ln' pre i && + ln' post i && + ln_st' stmt i + | Tm_Unreachable -> true @@ -596,6 +606,11 @@ let rec subst_st_term (t:st_term) (ss:subst) typ=subst_term typ ss; post=subst_term_opt post (shift_subst ss) } + | Tm_Block { pre; post; stmt } -> + Tm_Block { pre=subst_term pre ss; + post=subst_term post ss; + stmt=subst_st_term stmt ss } + | Tm_Unreachable -> Tm_Unreachable | Tm_ProofHintWithBinders { hint_type; binders; t} -> diff --git a/src/checker/Pulse.Syntax.Printer.fst b/src/checker/Pulse.Syntax.Printer.fst index b82ac439a..636e4b919 100644 --- a/src/checker/Pulse.Syntax.Printer.fst +++ b/src/checker/Pulse.Syntax.Printer.fst @@ -388,6 +388,17 @@ let rec st_term_to_string' (level:string) (t:st_term) | None -> "" | Some post -> sprintf " %s" (term_to_string post)) + | Tm_Block { pre; post; stmt } -> + sprintf "block\n%srequires %s\n%sensures %s\n%s{\n%s%s\n%s}" + (indent level) + (term_to_string pre) + (indent level) + (term_to_string post) + level + (indent level) + (st_term_to_string' (indent level) stmt) + level + | Tm_Unreachable -> "unreachable ()" | Tm_ProofHintWithBinders { binders; hint_type; t} -> @@ -496,6 +507,7 @@ let tag_of_st_term (t:st_term) = | Tm_WithLocalArray _ -> "Tm_WithLocalArray" | Tm_Rewrite _ -> "Tm_Rewrite" | Tm_Admit _ -> "Tm_Admit" + | Tm_Block _ -> "Tm_Block" | Tm_Unreachable -> "Tm_Unreachable" | Tm_ProofHintWithBinders _ -> "Tm_ProofHintWithBinders" | Tm_WithInv _ -> "Tm_WithInv" @@ -520,6 +532,7 @@ let rec print_st_head (t:st_term) | Tm_Match _ -> "Match" | Tm_While _ -> "While" | Tm_Admit _ -> "Admit" + | Tm_Block _ -> "Block" | Tm_Unreachable -> "Unreachable" | Tm_Par _ -> "Par" | Tm_Rewrite _ -> "Rewrite" @@ -549,6 +562,7 @@ let rec print_skel (t:st_term) = | Tm_Match _ -> "Match" | Tm_While _ -> "While" | Tm_Admit _ -> "Admit" + | Tm_Block _ -> "Block" | Tm_Unreachable -> "Unreachable" | Tm_Par _ -> "Par" | Tm_Rewrite _ -> "Rewrite" diff --git a/src/checker/Pulse.Typing.LN.fst b/src/checker/Pulse.Typing.LN.fst index de4b4c0ed..0794c8a2c 100644 --- a/src/checker/Pulse.Typing.LN.fst +++ b/src/checker/Pulse.Typing.LN.fst @@ -274,6 +274,11 @@ let rec open_st_term_ln' (e:st_term) open_term_ln' length x i; open_st_term_ln' body x (i + 1) + | Tm_Block { pre; post; stmt } -> + open_term_ln' pre x i; + open_term_ln' post x i; + open_st_term_ln' stmt x i + | Tm_Admit { typ; post } -> open_term_ln' typ x i; open_term_ln_opt' post x (i + 1) diff --git a/src/ocaml/plugin/FStar_Parser_Parse.mly b/src/ocaml/plugin/FStar_Parser_Parse.mly index 035c62a29..8c2a074c1 100644 --- a/src/ocaml/plugin/FStar_Parser_Parse.mly +++ b/src/ocaml/plugin/FStar_Parser_Parse.mly @@ -109,6 +109,7 @@ let parse_extension_blob (extension_name:string) %token FRIEND OPEN REC THEN TRUE TRY TYPE CALC CLASS INSTANCE EFFECT VAL %token INTRO ELIM %token INCLUDE +%token BLOCK %token WHEN AS RETURNS RETURNS_EQ WITH HASH AMP LPAREN RPAREN LPAREN_RPAREN COMMA LONG_LEFT_ARROW LARROW RARROW %token IFF IMPLIES CONJUNCTION DISJUNCTION %token DOT COLON COLON_COLON SEMICOLON diff --git a/src/ocaml/plugin/PulseSyntaxExtension_SyntaxWrapper.ml b/src/ocaml/plugin/PulseSyntaxExtension_SyntaxWrapper.ml index 5b7823c0d..05d453940 100755 --- a/src/ocaml/plugin/PulseSyntaxExtension_SyntaxWrapper.ml +++ b/src/ocaml/plugin/PulseSyntaxExtension_SyntaxWrapper.ml @@ -181,7 +181,10 @@ let tm_admit r : st_term = PSB.(with_range (tm_admit STT u_zero (tm_unknown r) None) r) let tm_unreachable r : st_term = PSB.(with_range (tm_unreachable) r) - + +let tm_block pre post stmt r : st_term = + PSB.(with_range (tm_block pre post stmt) r) + let close_term t v = Pulse_Syntax_Naming.close_term t v let close_st_term t v = Pulse_Syntax_Naming.close_st_term t v let close_st_term_n t v = Pulse_Syntax_Naming.close_st_term_n t v diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml index 7b28864fa..35802af01 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml @@ -1281,8 +1281,14 @@ let rec (desugar_stmt : (desugar_sequence env s1 s2 s.PulseSyntaxExtension_Sugar.range1)) | PulseSyntaxExtension_Sugar.Block - { PulseSyntaxExtension_Sugar.stmt = stmt;_} -> - Obj.magic (Obj.repr (desugar_stmt env stmt)) + { PulseSyntaxExtension_Sugar.precondition1 = precondition; + PulseSyntaxExtension_Sugar.postcondition1 = postcondition; + PulseSyntaxExtension_Sugar.stmt = stmt;_} + -> + Obj.magic + (Obj.repr + (desugar_block env precondition postcondition stmt + s.PulseSyntaxExtension_Sugar.range1)) | PulseSyntaxExtension_Sugar.If { PulseSyntaxExtension_Sugar.head1 = head; PulseSyntaxExtension_Sugar.join_vprop = join_vprop; @@ -2500,6 +2506,57 @@ and (desugar_sequence : (PulseSyntaxExtension_Err.return uu___2)) uu___2))) uu___1))) uu___3 uu___2 uu___1 uu___ +and (desugar_block : + PulseSyntaxExtension_Env.env_t -> + PulseSyntaxExtension_Sugar.vprop -> + PulseSyntaxExtension_Sugar.vprop -> + PulseSyntaxExtension_Sugar.stmt -> + PulseSyntaxExtension_Sugar.rng -> + PulseSyntaxExtension_SyntaxWrapper.st_term + PulseSyntaxExtension_Err.err) + = + fun uu___4 -> + fun uu___3 -> + fun uu___2 -> + fun uu___1 -> + fun uu___ -> + (fun env -> + fun pre -> + fun post -> + fun s -> + fun r -> + let uu___ = desugar_vprop env pre in + Obj.magic + (FStar_Class_Monad.op_let_Bang + PulseSyntaxExtension_Err.err_monad () () + (Obj.magic uu___) + (fun uu___1 -> + (fun p -> + let p = Obj.magic p in + let uu___1 = desugar_vprop env post in + Obj.magic + (FStar_Class_Monad.op_let_Bang + PulseSyntaxExtension_Err.err_monad () + () (Obj.magic uu___1) + (fun uu___2 -> + (fun q -> + let q = Obj.magic q in + let uu___2 = desugar_stmt env s in + Obj.magic + (FStar_Class_Monad.op_let_Bang + PulseSyntaxExtension_Err.err_monad + () () (Obj.magic uu___2) + (fun uu___3 -> + (fun s1 -> + let s1 = Obj.magic s1 in + let uu___3 = + PulseSyntaxExtension_SyntaxWrapper.tm_block + p q s1 r in + Obj.magic + (PulseSyntaxExtension_Err.return + uu___3)) uu___3))) + uu___2))) uu___1))) uu___4 uu___3 + uu___2 uu___1 uu___ and (desugar_proof_hint_with_binders : PulseSyntaxExtension_Env.env_t -> PulseSyntaxExtension_Sugar.stmt -> diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml index d0e32e38e..a789b238b 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Sugar.ml @@ -183,7 +183,10 @@ and stmt'__LetBinding__payload = id: FStar_Ident.ident ; typ: FStar_Parser_AST.term FStar_Pervasives_Native.option ; init1: let_init FStar_Pervasives_Native.option } -and stmt'__Block__payload = { +and stmt'__Block__payload = + { + precondition1: vprop ; + postcondition1: vprop ; stmt: stmt } and stmt'__If__payload = { @@ -306,9 +309,24 @@ let (__proj__Mkstmt'__LetBinding__payload__item__init : stmt'__LetBinding__payload -> let_init FStar_Pervasives_Native.option) = fun projectee -> match projectee with | { qualifier; id; typ; init1 = init;_} -> init +let (__proj__Mkstmt'__Block__payload__item__precondition : + stmt'__Block__payload -> vprop) = + fun projectee -> + match projectee with + | { precondition1 = precondition; postcondition1 = postcondition; + stmt = stmt1;_} -> precondition +let (__proj__Mkstmt'__Block__payload__item__postcondition : + stmt'__Block__payload -> vprop) = + fun projectee -> + match projectee with + | { precondition1 = precondition; postcondition1 = postcondition; + stmt = stmt1;_} -> postcondition let (__proj__Mkstmt'__Block__payload__item__stmt : stmt'__Block__payload -> stmt) = - fun projectee -> match projectee with | { stmt = stmt1;_} -> stmt1 + fun projectee -> + match projectee with + | { precondition1 = precondition; postcondition1 = postcondition; + stmt = stmt1;_} -> stmt1 let (__proj__Mkstmt'__If__payload__item__head : stmt'__If__payload -> FStar_Parser_AST.term) = fun projectee -> @@ -609,7 +627,9 @@ let (tag_of_stmt : stmt -> Prims.string) = | LetBinding { qualifier = uu___; id = uu___1; typ = uu___2; init1 = uu___3;_} -> "LetBinding" - | Block { stmt = uu___;_} -> "Block" + | Block + { precondition1 = uu___; postcondition1 = uu___1; stmt = uu___2;_} -> + "Block" | If { head1 = uu___; join_vprop = uu___1; then_ = uu___2; else_opt = uu___3;_} @@ -683,7 +703,16 @@ let (mk_let_binding : fun qualifier -> fun id -> fun typ -> fun init -> LetBinding { qualifier; id; typ; init1 = init } -let (mk_block : stmt -> stmt') = fun stmt1 -> Block { stmt = stmt1 } +let (mk_block : vprop -> vprop -> stmt -> stmt') = + fun precondition -> + fun postcondition -> + fun stmt1 -> + Block + { + precondition1 = precondition; + postcondition1 = postcondition; + stmt = stmt1 + } let (mk_if : FStar_Parser_AST.term -> ensures_vprop FStar_Pervasives_Native.option -> diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_TransformRValues.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_TransformRValues.ml index e610f6a86..6b0db4c4b 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_TransformRValues.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_TransformRValues.ml @@ -924,7 +924,10 @@ let rec (transform_stmt_with_reads : (PulseSyntaxExtension_Err.return (p1, needs, m2))) uu___1))) | PulseSyntaxExtension_Sugar.Block - { PulseSyntaxExtension_Sugar.stmt = stmt;_} -> + { PulseSyntaxExtension_Sugar.precondition1 = precondition; + PulseSyntaxExtension_Sugar.postcondition1 = postcondition; + PulseSyntaxExtension_Sugar.stmt = stmt;_} + -> Obj.magic (Obj.repr (let uu___ = transform_stmt m stmt in @@ -939,6 +942,10 @@ let rec (transform_stmt_with_reads : PulseSyntaxExtension_Sugar.s = (PulseSyntaxExtension_Sugar.Block { + PulseSyntaxExtension_Sugar.precondition1 + = precondition; + PulseSyntaxExtension_Sugar.postcondition1 + = postcondition; PulseSyntaxExtension_Sugar.stmt = stmt1 }); diff --git a/src/ocaml/plugin/pulseparser.mly b/src/ocaml/plugin/pulseparser.mly index 86c72461f..e050b886c 100644 --- a/src/ocaml/plugin/pulseparser.mly +++ b/src/ocaml/plugin/pulseparser.mly @@ -201,8 +201,10 @@ pulseStmtNoSeq: } | p=ifStmt { p } | p=matchStmt { p } - | LBRACE s=pulseStmt RBRACE - { PulseSyntaxExtension_Sugar.mk_block s } + | BLOCK REQUIRES p=pulseVprop + ENSURES q=pulseVprop + LBRACE s=pulseStmt RBRACE + { PulseSyntaxExtension_Sugar.mk_block p q s } matchStmt: | MATCH tm=appTermNoRecordExp c=option(ensuresVprop) LBRACE brs=list(pulseMatchBranch) RBRACE diff --git a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst index 414b91ca1..4e05d7cbf 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst @@ -445,8 +445,8 @@ let rec desugar_stmt (env:env_t) (s:Sugar.stmt) | Sequence { s1; s2 } -> desugar_sequence env s1 s2 s.range - | Block { stmt } -> - desugar_stmt env stmt + | Block { precondition; postcondition; stmt } -> + desugar_block env precondition postcondition stmt s.range | If { head; join_vprop; then_; else_opt } -> let! head = desugar_term env head in @@ -655,6 +655,13 @@ and desugar_sequence (env:env_t) (s1 s2:Sugar.stmt) r let annot = SW.mk_binder (Ident.id_of_text "_") (SW.tm_unknown r) in return (mk_bind annot s1 s2 r) +and desugar_block (env:env_t) (pre post:Sugar.vprop) (s:Sugar.stmt) r + : err SW.st_term + = let! p = desugar_vprop env pre in + let! q = desugar_vprop env post in + let! s = desugar_stmt env s in + return (SW.tm_block p q s 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 diff --git a/src/syntax_extension/PulseSyntaxExtension.Sugar.fst b/src/syntax_extension/PulseSyntaxExtension.Sugar.fst index fe489e8c7..109d316a9 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Sugar.fst +++ b/src/syntax_extension/PulseSyntaxExtension.Sugar.fst @@ -106,7 +106,9 @@ type stmt' = init:option let_init } - | Block { + | Block { + precondition:vprop; + postcondition:vprop; stmt : stmt } @@ -233,7 +235,7 @@ let mk_expr e = Expr { e } let mk_assignment id value = Assignment { lhs=id; value } let mk_array_assignment arr index value = ArrayAssignment { arr; index; value } let mk_let_binding qualifier id typ init = LetBinding { qualifier; id; typ; init } -let mk_block stmt = Block { stmt } +let mk_block precondition postcondition stmt = Block { precondition; postcondition; stmt } let mk_if head join_vprop then_ else_opt = If { head; join_vprop; then_; else_opt } let mk_match head returns_annot branches = Match { head; returns_annot; branches } let mk_while guard id invariant body = While { guard; id; invariant; body } diff --git a/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti b/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti index a255d09e7..ab4cddf98 100644 --- a/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti +++ b/src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti @@ -101,6 +101,7 @@ val is_tm_intro_exists (x:st_term) : bool val tm_protect (s:st_term) : st_term val tm_par (p1:term) (p2:term) (q1:term) (q2:term) (b1:st_term) (b2:st_term) (_:range) : st_term val tm_admit (_:range) : st_term +val tm_block (pre post:vprop) (s:st_term) (_:range) : st_term val tm_unreachable (_:range) : st_term val tm_proof_hint_with_binders (_:hint_type) (_:list binder) (body:st_term) (_:range) : st_term val tm_with_inv (iname:term) (body:st_term) (returns_:option (binder & term & term)) (_:range) : st_term diff --git a/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst b/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst index 4029acb66..ad08f02dc 100644 --- a/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst +++ b/src/syntax_extension/PulseSyntaxExtension.TransformRValues.fst @@ -268,9 +268,9 @@ let rec transform_stmt_with_reads (m:menv) (p:Sugar.stmt) return (p, needs, m) ) - | Block { stmt } -> + | Block { precondition; postcondition; stmt } -> let! stmt = transform_stmt m stmt in - let p = { p with s=Block { stmt } } in + let p = { p with s=Block { precondition; postcondition; stmt } } in return (p, [], m) | If { head; join_vprop; then_; else_opt } ->