Parser/Syntax: support assume keyword, desugaring to assume_

share/pulse/examples/Assume.fst

@@ -0,0 +1,21 @@
+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;
+}

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

src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -702,6 +702,15 @@ 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
+      return (SW.tm_st_app assume_ None p 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

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"

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