From edc8f44af48b8bde22750af3ab3b2f855bbdb6f9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Jun 2018 12:01:40 -0400 Subject: Add notations for cpsbind, cps_option_bind --- src/Util/CPSNotations.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util/CPSNotations.v') 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. -- cgit v1.2.3