diff options
author | Jason Gross <jagro@google.com> | 2018-06-04 12:01:40 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-06-14 16:37:49 -0400 |
commit | edc8f44af48b8bde22750af3ab3b2f855bbdb6f9 (patch) | |
tree | cfffd1f7d43368e1e65798e2c49552d0d086afe6 /src/Util | |
parent | 330e5af93e537710ae61364867b0303d2fe1315e (diff) |
Add notations for cpsbind, cps_option_bind
Diffstat (limited to 'src/Util')
-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. |