From 3bda01324867ec86fb39bfb9e6a9399e3e4e0ce7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 26 Aug 2024 16:07:38 -0700 Subject: [PATCH] All: use `defer_to` for binders marked `framing_implicit` In preparation for an F* change. --- lib/steel/Steel.Effect.Atomic.fst | 18 +-- lib/steel/Steel.Effect.Atomic.fsti | 78 ++++++------- lib/steel/Steel.Effect.fst | 18 +-- lib/steel/Steel.Effect.fsti | 70 ++++++------ lib/steel/Steel.Primitive.ForkJoin.Unix.fst | 28 ++--- lib/steel/Steel.ST.Coercions.fst | 10 +- lib/steel/Steel.ST.Coercions.fsti | 16 +-- lib/steel/Steel.ST.Effect.AtomicAndGhost.fst | 76 ++++++------- lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti | 104 +++++++++--------- lib/steel/Steel.ST.Effect.Ghost.fst | 8 +- lib/steel/Steel.ST.Effect.Ghost.fsti | 8 +- lib/steel/Steel.ST.Effect.fst | 68 ++++++------ lib/steel/Steel.ST.Effect.fsti | 96 ++++++++-------- lib/steel/Steel.ST.GenElim.fsti | 20 ++-- lib/steel/Steel.ST.GenElim1.fsti | 20 ++-- share/steel/examples/steel/DList.fst | 46 ++++---- 16 files changed, 342 insertions(+), 342 deletions(-) diff --git a/lib/steel/Steel.Effect.Atomic.fst b/lib/steel/Steel.Effect.Atomic.fst index 233b10c66..20c343365 100644 --- a/lib/steel/Steel.Effect.Atomic.fst +++ b/lib/steel/Steel.Effect.Atomic.fst @@ -286,15 +286,15 @@ val subcomp_opaque (a:Type) (o2:eqtype_as_type observability) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f) - (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] pr : prop) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] pr : prop) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f opened o1 pre_f post_f req_f ens_f) : Pure (repr a framed_g opened o2 pre_g post_g req_g ens_g) (requires (o1 = Unobservable || o2 = Observable) /\ diff --git a/lib/steel/Steel.Effect.Atomic.fsti b/lib/steel/Steel.Effect.Atomic.fsti index 8b9dc2698..c3f754450 100644 --- a/lib/steel/Steel.Effect.Atomic.fsti +++ b/lib/steel/Steel.Effect.Atomic.fsti @@ -59,7 +59,7 @@ let return_ens (a:Type) (x:a) (p:a -> vprop) : ens_t (p x) a p = val return_ (a:Type u#a) (x:a) (opened_invariants:inames) - (#[@@@ framing_implicit] p:a -> vprop) + (#[@@@ defer_to framing_implicit] p:a -> vprop) : repr a true opened_invariants Unobservable (return_pre (p x)) p (return_req (p x)) (return_ens a x p) @@ -133,18 +133,18 @@ val bind (a:Type) (b:Type) (o2:eqtype_as_type observability) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f) - (#[@@@ framing_implicit] pre_g:a -> pre_t) (#[@@@ framing_implicit] post_g:a -> post_t b) - (#[@@@ framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x))) - (#[@@@ framing_implicit] frame_f:vprop) (#[@@@ framing_implicit] frame_g:a -> vprop) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) - (#[@@@ framing_implicit] pr:a -> prop) - (#[@@@ framing_implicit] p1:squash (can_be_split_forall_dep pr + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) (#[@@@ defer_to framing_implicit] post_g:a -> post_t b) + (#[@@@ defer_to framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ defer_to framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x))) + (#[@@@ defer_to framing_implicit] frame_f:vprop) (#[@@@ defer_to framing_implicit] frame_g:a -> vprop) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) + (#[@@@ defer_to framing_implicit] pr:a -> prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x))) - (#[@@@ framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f) (g:(x:a -> repr b framed_g opened_invariants o2 (pre_g x) (post_g x) (req_g x) (ens_g x))) : Pure (repr b true opened_invariants (join_obs o1 o2) @@ -203,15 +203,15 @@ val subcomp (a:Type) (o2:eqtype_as_type observability) (#framed_f: eqtype_as_type bool) (#framed_g: eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f) - (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p: prop) - (#[@@@ framing_implicit] p1:squash (can_be_split_dep p pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p: prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep p pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f) : Pure (repr a framed_g opened_invariants o2 pre_g post_g req_g ens_g) (requires (o1 = Unobservable || o2 = Observable) /\ @@ -259,17 +259,17 @@ let if_then_else (a:Type) (o:inames) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_then:req_t pre_f) (#[@@@ framing_implicit] ens_then:ens_t pre_f a post_f) - (#[@@@ framing_implicit] req_else:req_t pre_g) (#[@@@ framing_implicit] ens_else:ens_t pre_g a post_g) - (#[@@@ framing_implicit] frame_f : vprop) - (#[@@@ framing_implicit] frame_g : vprop) - (#[@@@ framing_implicit] pr : prop) - (#[@@@ framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) - (#[@@@ framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g))) - (#[@@@ framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_then:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_then:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] req_else:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_else:ens_t pre_g a post_g) + (#[@@@ defer_to framing_implicit] frame_f : vprop) + (#[@@@ defer_to framing_implicit] frame_g : vprop) + (#[@@@ defer_to framing_implicit] pr : prop) + (#[@@@ defer_to framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) + (#[@@@ defer_to framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g))) + (#[@@@ defer_to framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) (f:repr a framed_f o Unobservable pre_f post_f req_then ens_then) (g:repr a framed_g o Unobservable pre_g post_g req_else ens_else) (p:bool) @@ -372,10 +372,10 @@ let bind_pure_steel__ens (#a:Type) (#b:Type) val bind_pure_steela_ (a:Type) (b:Type) (opened_invariants:inames) (o:eqtype_as_type observability) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed: eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> req_t pre) (#[@@@ framing_implicit] ens:a -> ens_t pre b post) + (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> req_t pre) (#[@@@ defer_to framing_implicit] ens:a -> ens_t pre b post) (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed opened_invariants o pre post (req x) (ens x))) : repr b framed opened_invariants o @@ -455,8 +455,8 @@ val lift_ghost_atomic (a:Type) (opened:inames) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:req_t pre) (#[@@@ framing_implicit] ens:ens_t pre a post) + (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:req_t pre) (#[@@@ defer_to framing_implicit] ens:ens_t pre a post) (f:repr a framed opened Unobservable pre post req ens) : repr a framed opened Unobservable pre post req ens @@ -470,8 +470,8 @@ val lift_atomic_steel (a:Type) (o:eqtype_as_type observability) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:req_t pre) (#[@@@ framing_implicit] ens:ens_t pre a post) + (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:req_t pre) (#[@@@ defer_to framing_implicit] ens:ens_t pre a post) (f:repr a framed Set.empty o pre post req ens) : Steel.Effect.repr a framed pre post req ens diff --git a/lib/steel/Steel.Effect.fst b/lib/steel/Steel.Effect.fst index 36a336b1b..20344fb80 100644 --- a/lib/steel/Steel.Effect.fst +++ b/lib/steel/Steel.Effect.fst @@ -443,15 +443,15 @@ let subcomp_pre_opaque (#a:Type) val subcomp_opaque (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f) - (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] pr : prop) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] pr : prop) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f pre_f post_f req_f ens_f) : Pure (repr a framed_g pre_g post_g req_g ens_g) (requires subcomp_pre_opaque req_f ens_f req_g ens_g p1 p2) diff --git a/lib/steel/Steel.Effect.fsti b/lib/steel/Steel.Effect.fsti index d699e50da..0e6df034c 100644 --- a/lib/steel/Steel.Effect.fsti +++ b/lib/steel/Steel.Effect.fsti @@ -52,7 +52,7 @@ let return_ens (a:Type) (x:a) (p:a -> vprop) : ens_t (p x) a p = /// Monadic return combinator for the Steel effect. It is parametric in the postcondition /// The vprop precondition is annotated with the return_pre predicate to enable special handling, /// as explained in Steel.Effect.Common -val return_ (a:Type) (x:a) (#[@@@ framing_implicit] p:a -> vprop) +val return_ (a:Type) (x:a) (#[@@@ defer_to framing_implicit] p:a -> vprop) : repr a true (return_pre (p x)) p (return_req (p x)) (return_ens a x p) /// Logical precondition for the composition (bind) of two Steel computations: @@ -120,18 +120,18 @@ let bind_ens (#a:Type) (#b:Type) val bind (a:Type) (b:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f) - (#[@@@ framing_implicit] pre_g:a -> pre_t) (#[@@@ framing_implicit] post_g:a -> post_t b) - (#[@@@ framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x))) - (#[@@@ framing_implicit] frame_f:vprop) (#[@@@ framing_implicit] frame_g:a -> vprop) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) - (#[@@@ framing_implicit] pr:a -> prop) - (#[@@@ framing_implicit] p1:squash (can_be_split_forall_dep pr + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) (#[@@@ defer_to framing_implicit] post_g:a -> post_t b) + (#[@@@ defer_to framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ defer_to framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x))) + (#[@@@ defer_to framing_implicit] frame_f:vprop) (#[@@@ defer_to framing_implicit] frame_g:a -> vprop) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) + (#[@@@ defer_to framing_implicit] pr:a -> prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x))) - (#[@@@ framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) (f:repr a framed_f pre_f post_f req_f ens_f) (g:(x:a -> repr b framed_g (pre_g x) (post_g x) (req_g x) (ens_g x))) : repr b @@ -182,15 +182,15 @@ let subcomp_pre (#a:Type) val subcomp (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f) - (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] pr : prop) - (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_f:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_g:ens_t pre_g a post_g) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] pr : prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f pre_f post_f req_f ens_f) : Pure (repr a framed_g pre_g post_g req_g ens_g) (requires subcomp_pre req_f ens_f req_g ens_g p1 p2) @@ -231,17 +231,17 @@ let if_then_else_ens (#a:Type) let if_then_else (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_then:req_t pre_f) (#[@@@ framing_implicit] ens_then:ens_t pre_f a post_f) - (#[@@@ framing_implicit] req_else:req_t pre_g) (#[@@@ framing_implicit] ens_else:ens_t pre_g a post_g) - (#[@@@ framing_implicit] frame_f : vprop) - (#[@@@ framing_implicit] frame_g : vprop) - (#[@@@ framing_implicit] pr : prop) - (#[@@@ framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) - (#[@@@ framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g))) - (#[@@@ framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_then:req_t pre_f) (#[@@@ defer_to framing_implicit] ens_then:ens_t pre_f a post_f) + (#[@@@ defer_to framing_implicit] req_else:req_t pre_g) (#[@@@ defer_to framing_implicit] ens_else:ens_t pre_g a post_g) + (#[@@@ defer_to framing_implicit] frame_f : vprop) + (#[@@@ defer_to framing_implicit] frame_g : vprop) + (#[@@@ defer_to framing_implicit] pr : prop) + (#[@@@ defer_to framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) + (#[@@@ defer_to framing_implicit] s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g))) + (#[@@@ defer_to framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) (f:repr a framed_f pre_f post_f req_then ens_then) (g:repr a framed_g pre_g post_g req_else ens_else) (p:bool) @@ -306,10 +306,10 @@ let bind_pure_steel__ens (#a:Type) (#b:Type) /// The composition combinator. val bind_pure_steel_ (a:Type) (b:Type) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> req_t pre) (#[@@@ framing_implicit] ens:a -> ens_t pre b post) + (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> req_t pre) (#[@@@ defer_to framing_implicit] ens:a -> ens_t pre b post) (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed pre post (req x) (ens x))) : repr b framed diff --git a/lib/steel/Steel.Primitive.ForkJoin.Unix.fst b/lib/steel/Steel.Primitive.ForkJoin.Unix.fst index e3479435d..f9e2aca72 100644 --- a/lib/steel/Steel.Primitive.ForkJoin.Unix.fst +++ b/lib/steel/Steel.Primitive.ForkJoin.Unix.fst @@ -52,7 +52,7 @@ type steelK (t:Type u#aa) (framed:bool) (pre : vprop) (post:t->vprop) = SteelT unit (frame `star` pre) (fun _ -> postf) (* The classic continuation monad *) -let return_ a (x:a) (#[@@@ framing_implicit] p: a -> vprop) : steelK a true (return_pre (p x)) p = +let return_ a (x:a) (#[@@@ defer_to framing_implicit] p: a -> vprop) : steelK a true (return_pre (p x)) p = fun k -> k x private @@ -84,13 +84,13 @@ let can_be_split_forall_frame (#a:Type) (p q:post_t a) (frame:vprop) (x:a) let bind (a:Type) (b:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] pre_g:a -> pre_t) (#[@@@ framing_implicit] post_g:post_t b) - (#[@@@ framing_implicit] frame_f:vprop) (#[@@@ framing_implicit] frame_g:vprop) - (#[@@@ framing_implicit] p:squash (can_be_split_forall + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t b) + (#[@@@ defer_to framing_implicit] frame_f:vprop) (#[@@@ defer_to framing_implicit] frame_g:vprop) + (#[@@@ defer_to framing_implicit] p:squash (can_be_split_forall (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g))) - (#[@@@ framing_implicit] m1 : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] m2:squash (maybe_emp framed_g frame_g)) + (#[@@@ defer_to framing_implicit] m1 : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] m2:squash (maybe_emp framed_g frame_g)) (f:steelK a framed_f pre_f post_f) (g:(x:a -> steelK b framed_g (pre_g x) post_g)) : steelK b @@ -118,10 +118,10 @@ let bind (a:Type) (b:Type) let subcomp (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] p1:squash (can_be_split pre_g pre_f)) - (#[@@@ framing_implicit] p2:squash (can_be_split_forall post_f post_g)) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split pre_g pre_f)) + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_forall post_f post_g)) (f:steelK a framed_f pre_f post_f) : Tot (steelK a framed_g pre_g post_g) = fun #frame #postf (k:(x:a -> SteelT unit (frame `star` post_g x) (fun _ -> postf))) -> @@ -131,8 +131,8 @@ let subcomp (a:Type) k x) <: (x:a -> SteelT unit (frame `star` post_f x) (fun _ -> postf))) // let if_then_else (a:Type u#aa) -// (#[@@@ framing_implicit] pre1:pre_t) -// (#[@@@ framing_implicit] post1:post_t a) +// (#[@@@ defer_to framing_implicit] pre1:pre_t) +// (#[@@@ defer_to framing_implicit] post1:post_t a) // (f : steelK a pre1 post1) // (g : steelK a pre1 post1) // (p:Type0) : Type = @@ -164,7 +164,7 @@ effect SteelKF (a:Type) (pre:pre_t) (post:post_t a) = let bind_tot_steelK_ (a:Type) (b:Type) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) (#[@@@ framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] pre:pre_t) (#[@@@ defer_to framing_implicit] post:post_t b) (f:eqtype_as_type unit -> Tot a) (g:(x:a -> steelK b framed pre post)) : steelK b framed diff --git a/lib/steel/Steel.ST.Coercions.fst b/lib/steel/Steel.ST.Coercions.fst index b2bbf9047..ccfb4536c 100644 --- a/lib/steel/Steel.ST.Coercions.fst +++ b/lib/steel/Steel.ST.Coercions.fst @@ -55,12 +55,12 @@ let bind_div_st_ens (#a:Type) (#b:Type) = fun y -> wp (fun _ -> True) /\ (exists x. ens_g x y) let bind_div_st_ (a:Type) (b:Type) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> Type0) - (#[@@@ framing_implicit] ens:a -> b -> Type0) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> Type0) + (#[@@@ defer_to framing_implicit] ens:a -> b -> Type0) (f:eqtype_as_type unit -> DIV a wp) (g:(x:a -> STF.repr b framed pre post (req x) (ens x))) : STF.repr b diff --git a/lib/steel/Steel.ST.Coercions.fsti b/lib/steel/Steel.ST.Coercions.fsti index a63ceb574..cd26d6801 100644 --- a/lib/steel/Steel.ST.Coercions.fsti +++ b/lib/steel/Steel.ST.Coercions.fsti @@ -98,10 +98,10 @@ val coerce_ghostF (#a:Type) val lift_st_steel (a:Type) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:pure_pre) - (#[@@@ framing_implicit] ens:pure_post a) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:pure_pre) + (#[@@@ defer_to framing_implicit] ens:pure_post a) (f:STF.repr a framed pre post req ens) : SF.repr a framed pre post (fun _ -> req) (fun _ x _ -> ens x) @@ -112,10 +112,10 @@ val lift_sta_sa (#framed:eqtype_as_type bool) (#o:inames) (#obs:eqtype_as_type observability) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:Type0) - (#[@@@ framing_implicit] ens:a -> Type0) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:Type0) + (#[@@@ defer_to framing_implicit] ens:a -> Type0) (f:STAG.repr a framed o obs pre post req ens) : SA.repr a framed o obs pre post (fun _ -> req) (fun _ x _ -> ens x) diff --git a/lib/steel/Steel.ST.Effect.AtomicAndGhost.fst b/lib/steel/Steel.ST.Effect.AtomicAndGhost.fst index 5e03174ce..76bb60cda 100644 --- a/lib/steel/Steel.ST.Effect.AtomicAndGhost.fst +++ b/lib/steel/Steel.ST.Effect.AtomicAndGhost.fst @@ -110,7 +110,7 @@ let weaken_repr #a #framed #o #g let return_ (a:Type u#a) (x:a) (opened_invariants:inames) - (#[@@@ framing_implicit] p:a -> vprop) + (#[@@@ defer_to framing_implicit] p:a -> vprop) : repr a true opened_invariants Unobservable (return_pre (p x)) p True @@ -124,25 +124,25 @@ let bind (a:Type) (b:Type) (o2:eqtype_as_type observability) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:Type0) - (#[@@@ framing_implicit] ens_f:a -> Type0) - (#[@@@ framing_implicit] pre_g:a -> pre_t) - (#[@@@ framing_implicit] post_g:a -> post_t b) - (#[@@@ framing_implicit] req_g:(a -> Type0)) - (#[@@@ framing_implicit] ens_g:(a -> b -> Type0)) - (#[@@@ framing_implicit] frame_f:vprop) - (#[@@@ framing_implicit] frame_g:a -> vprop) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] _x1 : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] _x2 : squash (maybe_emp_dep framed_g frame_g)) - (#[@@@ framing_implicit] pr:a -> prop) - (#[@@@ framing_implicit] p1:squash + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:Type0) + (#[@@@ defer_to framing_implicit] ens_f:a -> Type0) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) + (#[@@@ defer_to framing_implicit] post_g:a -> post_t b) + (#[@@@ defer_to framing_implicit] req_g:(a -> Type0)) + (#[@@@ defer_to framing_implicit] ens_g:(a -> b -> Type0)) + (#[@@@ defer_to framing_implicit] frame_f:vprop) + (#[@@@ defer_to framing_implicit] frame_g:a -> vprop) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] _x1 : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] _x2 : squash (maybe_emp_dep framed_g frame_g)) + (#[@@@ defer_to framing_implicit] pr:a -> prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x))) - (#[@@@ framing_implicit] p2:squash + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f) @@ -174,18 +174,18 @@ let subcomp (a:Type) (o2:eqtype_as_type observability) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:Type0) - (#[@@@ framing_implicit] ens_f:a -> Type0) - (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:Type0) - (#[@@@ framing_implicit] ens_g:a -> Type0) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] _x : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p1:squash (can_be_split pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:Type0) + (#[@@@ defer_to framing_implicit] ens_f:a -> Type0) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:Type0) + (#[@@@ defer_to framing_implicit] ens_g:a -> Type0) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] _x : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f) : Pure (repr a framed_g opened_invariants o2 pre_g post_g req_g ens_g) (requires @@ -214,12 +214,12 @@ let subcomp (a:Type) let bind_pure_stag (a:Type) (b:Type) (opened_invariants:inames) (o:eqtype_as_type observability) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> Type0) - (#[@@@ framing_implicit] ens:a -> b -> Type0) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> Type0) + (#[@@@ defer_to framing_implicit] ens:a -> b -> Type0) (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed opened_invariants o pre post (req x) (ens x))) = FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; @@ -229,10 +229,10 @@ let lift_atomic_st (a:Type) (o:eqtype_as_type observability) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:Type0) - (#[@@@ framing_implicit] ens:a -> Type0) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:Type0) + (#[@@@ defer_to framing_implicit] ens:a -> Type0) (f:repr a framed Set.empty o pre post req ens) : Steel.ST.Effect.repr a framed pre post req ens = let ff : Steel.Effect.repr a framed pre post (fun _ -> req) (fun _ x _ -> ens x) diff --git a/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti b/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti index 085a6ad24..3a0538494 100644 --- a/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti +++ b/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti @@ -61,7 +61,7 @@ val repr (a:Type u#a) //result type val return_ (a:Type u#a) (x:a) (opened_invariants:inames) - (#[@@@ framing_implicit] p:a -> vprop) + (#[@@@ defer_to framing_implicit] p:a -> vprop) : repr a true opened_invariants Unobservable (return_pre (p x)) p True @@ -75,25 +75,25 @@ val bind (a:Type) (b:Type) (o2:eqtype_as_type observability) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:pure_pre) - (#[@@@ framing_implicit] ens_f:pure_post a) - (#[@@@ framing_implicit] pre_g:a -> pre_t) - (#[@@@ framing_implicit] post_g:a -> post_t b) - (#[@@@ framing_implicit] req_g:a -> pure_pre) - (#[@@@ framing_implicit] ens_g:(a -> pure_post b)) - (#[@@@ framing_implicit] frame_f:vprop) - (#[@@@ framing_implicit] frame_g:a -> vprop) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) - (#[@@@ framing_implicit] pr:a -> prop) - (#[@@@ framing_implicit] p1:squash + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:pure_pre) + (#[@@@ defer_to framing_implicit] ens_f:pure_post a) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) + (#[@@@ defer_to framing_implicit] post_g:a -> post_t b) + (#[@@@ defer_to framing_implicit] req_g:a -> pure_pre) + (#[@@@ defer_to framing_implicit] ens_g:(a -> pure_post b)) + (#[@@@ defer_to framing_implicit] frame_f:vprop) + (#[@@@ defer_to framing_implicit] frame_g:a -> vprop) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) + (#[@@@ defer_to framing_implicit] pr:a -> prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x))) - (#[@@@ framing_implicit] p2:squash + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f) @@ -117,18 +117,18 @@ val subcomp (a:Type) (o2:eqtype_as_type observability) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:pure_pre) - (#[@@@ framing_implicit] ens_f:pure_post a) - (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:pure_pre) - (#[@@@ framing_implicit] ens_g:pure_post a) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p1:squash (can_be_split pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:pure_pre) + (#[@@@ defer_to framing_implicit] ens_f:pure_post a) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:pure_pre) + (#[@@@ defer_to framing_implicit] ens_g:pure_post a) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f opened_invariants o1 pre_f post_f req_f ens_f) : Pure (repr a framed_g opened_invariants o2 pre_g post_g req_g ens_g) (requires @@ -141,21 +141,21 @@ let if_then_else (a:Type) (o:inames) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_then:pure_pre) - (#[@@@ framing_implicit] ens_then:pure_post a) - (#[@@@ framing_implicit] req_else:pure_pre) - (#[@@@ framing_implicit] ens_else:pure_post a) - (#[@@@ framing_implicit] frame_f : vprop) - (#[@@@ framing_implicit] frame_g : vprop) - (#[@@@ framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) - (#[@@@ framing_implicit] s_pre: squash ( + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_then:pure_pre) + (#[@@@ defer_to framing_implicit] ens_then:pure_post a) + (#[@@@ defer_to framing_implicit] req_else:pure_pre) + (#[@@@ defer_to framing_implicit] ens_else:pure_post a) + (#[@@@ defer_to framing_implicit] frame_f : vprop) + (#[@@@ defer_to framing_implicit] frame_g : vprop) + (#[@@@ defer_to framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) + (#[@@@ defer_to framing_implicit] s_pre: squash ( can_be_split (pre_f `star` frame_f) (pre_g `star` frame_g))) - (#[@@@ framing_implicit] s_post: squash ( + (#[@@@ defer_to framing_implicit] s_post: squash ( equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) (f:repr a framed_f o Unobservable pre_f post_f req_then ens_then) (g:repr a framed_g o Unobservable pre_g post_g req_else ens_else) @@ -194,12 +194,12 @@ effect { val bind_pure_stag (a:Type) (b:Type) (opened_invariants:inames) (o:eqtype_as_type observability) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> pure_pre) - (#[@@@ framing_implicit] ens:a -> pure_post b) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> pure_pre) + (#[@@@ defer_to framing_implicit] ens:a -> pure_post b) (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed opened_invariants o pre post (req x) (ens x))) : repr b @@ -216,9 +216,9 @@ val lift_atomic_st (a:Type) (o:eqtype_as_type observability) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:pure_pre) - (#[@@@ framing_implicit] ens:pure_post a) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:pure_pre) + (#[@@@ defer_to framing_implicit] ens:pure_post a) (f:repr a framed Set.empty o pre post req ens) : Steel.ST.Effect.repr a framed pre post req ens diff --git a/lib/steel/Steel.ST.Effect.Ghost.fst b/lib/steel/Steel.ST.Effect.Ghost.fst index 3e473a902..08eb34569 100644 --- a/lib/steel/Steel.ST.Effect.Ghost.fst +++ b/lib/steel/Steel.ST.Effect.Ghost.fst @@ -29,10 +29,10 @@ let lift_ghost_atomic (a:Type) (opened:inames) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:Type0) - (#[@@@ framing_implicit] ens:a -> Type0) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:Type0) + (#[@@@ defer_to framing_implicit] ens:a -> Type0) (f:STAG.repr a framed opened Unobservable pre post req ens) : STAG.repr a framed opened Unobservable pre post req ens = f diff --git a/lib/steel/Steel.ST.Effect.Ghost.fsti b/lib/steel/Steel.ST.Effect.Ghost.fsti index fae822c0c..c0429a77f 100644 --- a/lib/steel/Steel.ST.Effect.Ghost.fsti +++ b/lib/steel/Steel.ST.Effect.Ghost.fsti @@ -87,10 +87,10 @@ val lift_ghost_atomic (a:Type) (opened:inames) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t a) - (#[@@@ framing_implicit] req:pure_pre) - (#[@@@ framing_implicit] ens:pure_post a) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t a) + (#[@@@ defer_to framing_implicit] req:pure_pre) + (#[@@@ defer_to framing_implicit] ens:pure_post a) (f:STAG.repr a framed opened Unobservable pre post req ens) : STAG.repr a framed opened Unobservable pre post req ens diff --git a/lib/steel/Steel.ST.Effect.fst b/lib/steel/Steel.ST.Effect.fst index 6fc723ae4..58496bca0 100644 --- a/lib/steel/Steel.ST.Effect.fst +++ b/lib/steel/Steel.ST.Effect.fst @@ -95,7 +95,7 @@ let weaken_repr a framed let return_ (a:Type) (x:a) - (#[@@@ framing_implicit] p:a -> vprop) + (#[@@@ defer_to framing_implicit] p:a -> vprop) : Tot (repr a true (return_pre (p x)) p True (fun v -> v == x)) = let k : Steel.Effect.repr a true (p x) @@ -109,25 +109,25 @@ let return_ (a:Type) let bind (a:Type) (b:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:Type0) - (#[@@@ framing_implicit] ens_f:a -> Type0) - (#[@@@ framing_implicit] pre_g:a -> pre_t) - (#[@@@ framing_implicit] post_g:a -> post_t b) - (#[@@@ framing_implicit] req_g:(a -> Type0)) - (#[@@@ framing_implicit] ens_g:(a -> b -> Type0)) - (#[@@@ framing_implicit] frame_f:vprop) - (#[@@@ framing_implicit] frame_g:a -> vprop) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] _x1: squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] _x2: squash (maybe_emp_dep framed_g frame_g)) - (#[@@@ framing_implicit] pr:a -> prop) - (#[@@@ framing_implicit] p1:squash + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:Type0) + (#[@@@ defer_to framing_implicit] ens_f:a -> Type0) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) + (#[@@@ defer_to framing_implicit] post_g:a -> post_t b) + (#[@@@ defer_to framing_implicit] req_g:(a -> Type0)) + (#[@@@ defer_to framing_implicit] ens_g:(a -> b -> Type0)) + (#[@@@ defer_to framing_implicit] frame_f:vprop) + (#[@@@ defer_to framing_implicit] frame_g:a -> vprop) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] _x1: squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] _x2: squash (maybe_emp_dep framed_g frame_g)) + (#[@@@ defer_to framing_implicit] pr:a -> prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x))) - (#[@@@ framing_implicit] p2:squash + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) (f:repr a framed_f pre_f post_f req_f ens_f) (g:(x:a -> repr b framed_g (pre_g x) (post_g x) (req_g x) (ens_g x))) @@ -155,19 +155,19 @@ let bind (a:Type) (b:Type) let subcomp (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:Type0) - (#[@@@ framing_implicit] ens_f:a -> Type0) - (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:Type0) - (#[@@@ framing_implicit] ens_g:a -> Type0) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] _x1 : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p1:squash ( + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:Type0) + (#[@@@ defer_to framing_implicit] ens_f:a -> Type0) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:Type0) + (#[@@@ defer_to framing_implicit] ens_g:a -> Type0) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] _x1 : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p1:squash ( can_be_split pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash ( + (#[@@@ defer_to framing_implicit] p2:squash ( equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f pre_f post_f req_f ens_f) : Pure (repr a framed_g pre_g post_g req_g ens_g) @@ -196,12 +196,12 @@ let subcomp (a:Type) () () let bind_pure_st_ (a:Type) (b:Type) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> Type0) - (#[@@@ framing_implicit] ens:a -> b -> Type0) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> Type0) + (#[@@@ defer_to framing_implicit] ens:a -> b -> Type0) (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed pre post (req x) (ens x))) : repr b diff --git a/lib/steel/Steel.ST.Effect.fsti b/lib/steel/Steel.ST.Effect.fsti index 94ea23a46..5d0857ce0 100644 --- a/lib/steel/Steel.ST.Effect.fsti +++ b/lib/steel/Steel.ST.Effect.fsti @@ -38,7 +38,7 @@ val repr (a:Type) val return_ (a:Type) (x:a) - (#[@@@ framing_implicit] p:a -> vprop) + (#[@@@ defer_to framing_implicit] p:a -> vprop) : repr a true (return_pre (p x)) p True (fun v -> v == x) unfold @@ -59,25 +59,25 @@ let bind_ens (a:Type) (b:Type) val bind (a:Type) (b:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:pure_pre) - (#[@@@ framing_implicit] ens_f:pure_post a) - (#[@@@ framing_implicit] pre_g:a -> pre_t) - (#[@@@ framing_implicit] post_g:a -> post_t b) - (#[@@@ framing_implicit] req_g:a -> pure_pre) - (#[@@@ framing_implicit] ens_g:(a -> pure_post b)) - (#[@@@ framing_implicit] frame_f:vprop) - (#[@@@ framing_implicit] frame_g:a -> vprop) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) - (#[@@@ framing_implicit] pr:a -> prop) - (#[@@@ framing_implicit] p1:squash + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:pure_pre) + (#[@@@ defer_to framing_implicit] ens_f:pure_post a) + (#[@@@ defer_to framing_implicit] pre_g:a -> pre_t) + (#[@@@ defer_to framing_implicit] post_g:a -> post_t b) + (#[@@@ defer_to framing_implicit] req_g:a -> pure_pre) + (#[@@@ defer_to framing_implicit] ens_g:(a -> pure_post b)) + (#[@@@ defer_to framing_implicit] frame_f:vprop) + (#[@@@ defer_to framing_implicit] frame_g:a -> vprop) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g)) + (#[@@@ defer_to framing_implicit] pr:a -> prop) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x))) - (#[@@@ framing_implicit] p2:squash + (#[@@@ defer_to framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post)) (f:repr a framed_f pre_f post_f req_f ens_f) (g:(x:a -> repr b framed_g (pre_g x) (post_g x) (req_g x) (ens_g x))) @@ -91,18 +91,18 @@ val bind (a:Type) (b:Type) val subcomp (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] req_f:pure_pre) - (#[@@@ framing_implicit] ens_f:pure_post a) - (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_g:pure_pre) - (#[@@@ framing_implicit] ens_g:pure_post a) - (#[@@@ framing_implicit] frame:vprop) - (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame)) - (#[@@@ framing_implicit] p1:squash (can_be_split pre_g (pre_f `star` frame))) - (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] req_f:pure_pre) + (#[@@@ defer_to framing_implicit] ens_f:pure_post a) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_g:pure_pre) + (#[@@@ defer_to framing_implicit] ens_g:pure_post a) + (#[@@@ defer_to framing_implicit] frame:vprop) + (#[@@@ defer_to framing_implicit] _ : squash (maybe_emp framed_f frame)) + (#[@@@ defer_to framing_implicit] p1:squash (can_be_split pre_g (pre_f `star` frame))) + (#[@@@ defer_to framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame))) (f:repr a framed_f pre_f post_f req_f ens_f) : Pure (repr a framed_g pre_g post_g req_g ens_g) (requires @@ -129,20 +129,20 @@ let if_then_else_ens (a:Type) let if_then_else (a:Type) (#framed_f:eqtype_as_type bool) (#framed_g:eqtype_as_type bool) - (#[@@@ framing_implicit] pre_f:pre_t) - (#[@@@ framing_implicit] pre_g:pre_t) - (#[@@@ framing_implicit] post_f:post_t a) - (#[@@@ framing_implicit] post_g:post_t a) - (#[@@@ framing_implicit] req_then:pure_pre) - (#[@@@ framing_implicit] ens_then:pure_post a) - (#[@@@ framing_implicit] req_else:pure_pre) - (#[@@@ framing_implicit] ens_else:pure_post a) - (#[@@@ framing_implicit] frame_f : vprop) - (#[@@@ framing_implicit] frame_g : vprop) - (#[@@@ framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) - (#[@@@ framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) - (#[@@@ framing_implicit] s_pre: squash (can_be_split (pre_f `star` frame_f) (pre_g `star` frame_g))) - (#[@@@ framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) + (#[@@@ defer_to framing_implicit] pre_f:pre_t) + (#[@@@ defer_to framing_implicit] pre_g:pre_t) + (#[@@@ defer_to framing_implicit] post_f:post_t a) + (#[@@@ defer_to framing_implicit] post_g:post_t a) + (#[@@@ defer_to framing_implicit] req_then:pure_pre) + (#[@@@ defer_to framing_implicit] ens_then:pure_post a) + (#[@@@ defer_to framing_implicit] req_else:pure_pre) + (#[@@@ defer_to framing_implicit] ens_else:pure_post a) + (#[@@@ defer_to framing_implicit] frame_f : vprop) + (#[@@@ defer_to framing_implicit] frame_g : vprop) + (#[@@@ defer_to framing_implicit] me1 : squash (maybe_emp framed_f frame_f)) + (#[@@@ defer_to framing_implicit] me2 : squash (maybe_emp framed_g frame_g)) + (#[@@@ defer_to framing_implicit] s_pre: squash (can_be_split (pre_f `star` frame_f) (pre_g `star` frame_g))) + (#[@@@ defer_to framing_implicit] s_post: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g))) (f:repr a framed_f pre_f post_f req_then ens_then) (g:repr a framed_g pre_g post_g req_else ens_else) (p:bool) @@ -206,12 +206,12 @@ let bind_pure_st_ens (#a:Type) /// The composition combinator. val bind_pure_st_ (a:Type) (b:Type) - (#[@@@ framing_implicit] wp:pure_wp a) + (#[@@@ defer_to framing_implicit] wp:pure_wp a) (#framed:eqtype_as_type bool) - (#[@@@ framing_implicit] pre:pre_t) - (#[@@@ framing_implicit] post:post_t b) - (#[@@@ framing_implicit] req:a -> pure_pre) - (#[@@@ framing_implicit] ens:a -> pure_post b) + (#[@@@ defer_to framing_implicit] pre:pre_t) + (#[@@@ defer_to framing_implicit] post:post_t b) + (#[@@@ defer_to framing_implicit] req:a -> pure_pre) + (#[@@@ defer_to framing_implicit] ens:a -> pure_post b) (f:eqtype_as_type unit -> PURE a wp) (g:(x:a -> repr b framed pre post (req x) (ens x))) : repr b diff --git a/lib/steel/Steel.ST.GenElim.fsti b/lib/steel/Steel.ST.GenElim.fsti index ac620e765..42daf6de5 100644 --- a/lib/steel/Steel.ST.GenElim.fsti +++ b/lib/steel/Steel.ST.GenElim.fsti @@ -16,20 +16,20 @@ val gen_elim' val gen_elim (#opened: _) - (#[@@@ framing_implicit] p: vprop) - (#[@@@ framing_implicit] a: Type0) - (#[@@@ framing_implicit] q: Ghost.erased a -> Tot vprop) - (#[@@@ framing_implicit] post: Ghost.erased a -> Tot prop) - (#[@@@ framing_implicit] sq: squash (gen_elim_prop_placeholder true p a q post)) + (#[@@@ defer_to framing_implicit] p: vprop) + (#[@@@ defer_to framing_implicit] a: Type0) + (#[@@@ defer_to framing_implicit] q: Ghost.erased a -> Tot vprop) + (#[@@@ defer_to framing_implicit] post: Ghost.erased a -> Tot prop) + (#[@@@ defer_to framing_implicit] sq: squash (gen_elim_prop_placeholder true p a q post)) (_: unit) : STGhostF (Ghost.erased a) opened p (fun x -> guard_vprop (q x)) ( (T.with_tactic solve_gen_elim_prop) (squash (gen_elim_prop true p a q post))) post val gen_elim_dep (#opened: _) - (#[@@@ framing_implicit] p: vprop) - (#[@@@ framing_implicit] a: Type0) - (#[@@@ framing_implicit] q: Ghost.erased a -> Tot vprop) - (#[@@@ framing_implicit] post: Ghost.erased a -> Tot prop) - (#[@@@ framing_implicit] sq: squash (gen_elim_prop_placeholder false p a q post)) + (#[@@@ defer_to framing_implicit] p: vprop) + (#[@@@ defer_to framing_implicit] a: Type0) + (#[@@@ defer_to framing_implicit] q: Ghost.erased a -> Tot vprop) + (#[@@@ defer_to framing_implicit] post: Ghost.erased a -> Tot prop) + (#[@@@ defer_to framing_implicit] sq: squash (gen_elim_prop_placeholder false p a q post)) (_: unit) : STGhostF (Ghost.erased a) opened p (fun x -> guard_vprop (q x)) ( (T.with_tactic solve_gen_elim_prop) (squash (gen_elim_prop false p a q post))) post diff --git a/lib/steel/Steel.ST.GenElim1.fsti b/lib/steel/Steel.ST.GenElim1.fsti index 0a0970fe7..d6d8d92da 100644 --- a/lib/steel/Steel.ST.GenElim1.fsti +++ b/lib/steel/Steel.ST.GenElim1.fsti @@ -16,20 +16,20 @@ val gen_elim' val gen_elim (#opened: _) - (#[@@@ framing_implicit] p: vprop) - (#[@@@ framing_implicit] a: Type) - (#[@@@ framing_implicit] q: Ghost.erased a -> Tot vprop) - (#[@@@ framing_implicit] post: Ghost.erased a -> Tot prop) - (#[@@@ framing_implicit] sq: squash (gen_elim_prop_placeholder true p a q post)) + (#[@@@ defer_to framing_implicit] p: vprop) + (#[@@@ defer_to framing_implicit] a: Type) + (#[@@@ defer_to framing_implicit] q: Ghost.erased a -> Tot vprop) + (#[@@@ defer_to framing_implicit] post: Ghost.erased a -> Tot prop) + (#[@@@ defer_to framing_implicit] sq: squash (gen_elim_prop_placeholder true p a q post)) (_: unit) : STGhostF (Ghost.erased a) opened p (fun x -> guard_vprop (q x)) ( (T.with_tactic solve_gen_elim_prop) (squash (gen_elim_prop true p a q post))) post val gen_elim_dep (#opened: _) - (#[@@@ framing_implicit] p: vprop) - (#[@@@ framing_implicit] a: Type) - (#[@@@ framing_implicit] q: Ghost.erased a -> Tot vprop) - (#[@@@ framing_implicit] post: Ghost.erased a -> Tot prop) - (#[@@@ framing_implicit] sq: squash (gen_elim_prop_placeholder false p a q post)) + (#[@@@ defer_to framing_implicit] p: vprop) + (#[@@@ defer_to framing_implicit] a: Type) + (#[@@@ defer_to framing_implicit] q: Ghost.erased a -> Tot vprop) + (#[@@@ defer_to framing_implicit] post: Ghost.erased a -> Tot prop) + (#[@@@ defer_to framing_implicit] sq: squash (gen_elim_prop_placeholder false p a q post)) (_: unit) : STGhostF (Ghost.erased a) opened p (fun x -> guard_vprop (q x)) ( (T.with_tactic solve_gen_elim_prop) (squash (gen_elim_prop false p a q post))) post diff --git a/share/steel/examples/steel/DList.fst b/share/steel/examples/steel/DList.fst index 6714131ef..1e03f4a6a 100644 --- a/share/steel/examples/steel/DList.fst +++ b/share/steel/examples/steel/DList.fst @@ -28,8 +28,8 @@ let new_dlist (#a:Type) (init:a) pc let read_norefine (#a:Type) - (#[@@@ framing_implicit] p:perm) - (#[@@@ framing_implicit] v:Ghost.erased a) + (#[@@@ defer_to framing_implicit] p:perm) + (#[@@@ defer_to framing_implicit] v:Ghost.erased a) (r:ref a) : Steel a (pts_to r p v) (fun x -> pts_to r p v) (requires fun _ -> True) @@ -137,13 +137,13 @@ let concat_nil_l (#a:Type) return l let concat_t a = - (#[@@@ framing_implicit] from0:t a) -> - (#[@@@ framing_implicit] to0: t a) -> - (#[@@@ framing_implicit] hd0:cell a) -> - (#[@@@ framing_implicit] tl0:list (cell a)) -> - (#[@@@ framing_implicit] from1:t a) -> - (#[@@@ framing_implicit] hd1:cell a) -> - (#[@@@ framing_implicit] tl1:list (cell a)) -> + (#[@@@ defer_to framing_implicit] from0:t a) -> + (#[@@@ defer_to framing_implicit] to0: t a) -> + (#[@@@ defer_to framing_implicit] hd0:cell a) -> + (#[@@@ defer_to framing_implicit] tl0:list (cell a)) -> + (#[@@@ defer_to framing_implicit] from1:t a) -> + (#[@@@ defer_to framing_implicit] hd1:cell a) -> + (#[@@@ defer_to framing_implicit] tl1:list (cell a)) -> (ptr0:t a) -> (ptr1:t a) -> SteelT (list (cell a)) @@ -175,13 +175,13 @@ let concat_cons (#a:Type) (aux:concat_t a) c0::l let rec concat (#a:Type) - (#[@@@ framing_implicit] from0:t a) - (#[@@@ framing_implicit] to0: t a) - (#[@@@ framing_implicit] hd0:cell a) - (#[@@@ framing_implicit] tl0:list (cell a)) - (#[@@@ framing_implicit] from1:t a) - (#[@@@ framing_implicit] hd1:cell a) - (#[@@@ framing_implicit] tl1:list (cell a)) + (#[@@@ defer_to framing_implicit] from0:t a) + (#[@@@ defer_to framing_implicit] to0: t a) + (#[@@@ defer_to framing_implicit] hd0:cell a) + (#[@@@ defer_to framing_implicit] tl0:list (cell a)) + (#[@@@ defer_to framing_implicit] from1:t a) + (#[@@@ defer_to framing_implicit] hd1:cell a) + (#[@@@ defer_to framing_implicit] tl1:list (cell a)) (ptr0:t a) (ptr1:t a) : SteelT (list (cell a)) @@ -238,10 +238,10 @@ let rec concat (#a:Type) let snoc (#a:Type) - (#[@@@ framing_implicit] from0:t a) - (#[@@@ framing_implicit] to0: t a) - (#[@@@ framing_implicit] hd0:cell a) - (#[@@@ framing_implicit] l0:list (cell a)) + (#[@@@ defer_to framing_implicit] from0:t a) + (#[@@@ defer_to framing_implicit] to0: t a) + (#[@@@ defer_to framing_implicit] hd0:cell a) + (#[@@@ defer_to framing_implicit] l0:list (cell a)) (ptr0:t a) (v:a) : SteelT (list (cell a)) @@ -273,9 +273,9 @@ let cons (#a:Type) fst pc, l let rec length (#a:Type) - (#[@@@ framing_implicit] from:t a) - (#[@@@ framing_implicit] to: t a) - (#[@@@ framing_implicit] rep:list (cell a)) + (#[@@@ defer_to framing_implicit] from:t a) + (#[@@@ defer_to framing_implicit] to: t a) + (#[@@@ defer_to framing_implicit] rep:list (cell a)) (p:t a) : Steel nat (dlist from p to rep)