diff options
| author |  Jason Gross <jagro@google.com> | 2018-05-31 13:51:36 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-06-01 14:38:05 -0400 |
| commit | e19e55d62139056c2c2455b8075d845d88f4e93e (patch) | |
| tree | 6171b284adb9c6ac6f76900c473af7ebacac9c2e /src/Util/CPSNotations.v | |
| parent | 7fdc9bb220448f050cabd90133bedcd8ce0dd4b0 (diff) | |
Move cps notations into a scope
Diffstat (limited to 'src/Util/CPSNotations.v')
| -rw-r--r-- | src/Util/CPSNotations.v | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/Util/CPSNotations.v b/src/Util/CPSNotations.v index f6fa31f5e..29f7252ba 100644 --- a/src/Util/CPSNotations.v +++ b/src/Util/CPSNotations.v @@ -3,10 +3,12 @@ Require Import Crypto.Util.Notations. (** [x <- f ; C] encodes a call to function [f] with [C] as the continuation. In [C], [x] refers to the output of [f]. *) +Delimit Scope cps_scope with cps. + (* [cpscall] is a marker to get Coq to print code using this notation only when it was actually used *) Definition cpscall {R} (f:forall{T}(continuation:R->T),T) {T} (continuation:R->T) := @f T continuation. -Notation "x' <- v ; C" := (cpscall v (fun x' => C)). +Notation "x' <- v ; C" := (cpscall v%cps (fun x' => C%cps)) : cps_scope. (** A value of type [~>R] accepts a continuation that takes an argument of type [R]. It is meant to be used in [Definition] and @@ -18,7 +20,7 @@ Notation "x' <- v ; C" := (cpscall v (fun x' => C)). [~> R] is universally quantified over the possible return types of the continuations that it can be applied to. *) -Notation "~> R" := (forall {T} (_:R->T), T). +Notation "~> R" := (forall {T} (_:R->T), T) : type_scope. (** The type [A ~> R] contains functions that takes an argument of type [A] and pass a value of type [R] to the continuation. Functions @@ -26,9 +28,9 @@ Notation "~> R" := (forall {T} (_:R->T), T). ~> B ~>C] -- the first form requires both arguments to be specified before its output can be CPS-bound, the latter must be bound once it is partially applied to one argument. *) -Notation "A ~> R" := (A -> ~>R). +Notation "A ~> R" := (A -> ~>R) : type_scope. (* [cpsreturn] is a marker to get Coq to print loop notations before a [return] *) 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)).
\ No newline at end of file +Notation "'return' x" := (cpsreturn (fun {T} (continuation:_->T) => continuation x)) : cps_scope. |