Add notations for cpsbind, cps_option_bind

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.