diff options
Diffstat (limited to 'src/Util/CPSNotations.v')
-rw-r--r-- | src/Util/CPSNotations.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/CPSNotations.v b/src/Util/CPSNotations.v index 29f7252ba..0f49176c5 100644 --- a/src/Util/CPSNotations.v +++ b/src/Util/CPSNotations.v @@ -34,3 +34,11 @@ Notation "A ~> R" := (A -> ~>R) : type_scope. Definition cpsreturn {T} (x:T) := x. (** [return x] passes [x] to the continuation implicit in the previous notations. *) Notation "'return' x" := (cpsreturn (fun {T} (continuation:_->T) => continuation x)) : cps_scope. + +Definition cpsbind {A B} (v:~> A) (f:A ~> B) : ~> B + := fun T k => (a <- v; fa <- f a; k fa)%cps. +Notation "x' <--- v ; C" := (cpsbind v%cps (fun x' => C%cps)) : cps_scope. + +Definition cps_option_bind {A B} (v:~> option A) (f:A ~> option B) : ~> option B + := cpsbind v (fun x' T k => match x' with Some x' => f x' T k | None => k None end). +Notation "x' <-- v ; C" := (cps_option_bind v%cps (fun x' => C%cps)) : cps_scope. |