diff --git a/share/pulse/examples/Assume.fst b/share/pulse/examples/Assume.fst new file mode 100644 index 000000000..cf9d3f446 --- /dev/null +++ b/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; +} diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml index d46a77d16..14c677a7e 100644 --- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml +++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml @@ -2640,6 +2640,45 @@ 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 uu___1 = + PulseSyntaxExtension_SyntaxWrapper.tm_st_app + assume_ FStar_Pervasives_Native.None + p1 r in + Obj.magic + (PulseSyntaxExtension_Err.return + uu___1)) 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/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..540293807 100644 --- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst +++ b/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 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