Add an explicit block statement

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 ()

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
 

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 },

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;

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 }

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} ->

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} ->

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"

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)

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

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

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