diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-06-15 10:17:35 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-06-15 10:17:35 -0400 |
commit | b319173e40cb219ab3b9b80e967b264e699851ad (patch) | |
tree | ede12875dd82acbda93385ed65e8dd1f2cc8760a /src | |
parent | 9d55a380b76b791648071e6354353e587132c119 (diff) |
move CPS notations to Util.CPSNotations
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/CPSNotations.v | 34 | ||||
-rw-r--r-- | src/Util/Loop.v | 38 |
2 files changed, 35 insertions, 37 deletions
diff --git a/src/Util/CPSNotations.v b/src/Util/CPSNotations.v new file mode 100644 index 000000000..f6fa31f5e --- /dev/null +++ b/src/Util/CPSNotations.v @@ -0,0 +1,34 @@ +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]. *) + +(* [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)). + +(** A value of type [~>R] accepts a continuation that takes an + argument of type [R]. It is meant to be used in [Definition] and + such; for example: +<< + Definition add_cps (a b:nat) : ~> nat. +>> + The return type of the continuation is not yet specified; every + [~> 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). + +(** The type [A ~> R] contains functions that takes an argument of + type [A] and pass a value of type [R] to the continuation. Functions + that take multiple arguments can be encoded as [A -> B ~> C] or [A + ~> 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). + +(* [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 diff --git a/src/Util/Loop.v b/src/Util/Loop.v index e9d66b647..26341c805 100644 --- a/src/Util/Loop.v +++ b/src/Util/Loop.v @@ -3,46 +3,10 @@ Require Import Coq.ZArith.BinInt. Require Import Coq.micromega.Lia. Require Import Coq.omega.Omega. Require Import Crypto.Util.ZUtil. -Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Notations Crypto.Util.CPSNotations. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics.SpecializeBy. -(* TODO: move *) -Module CPSNotations. - (** [x <- f ; C] encodes a call to function [f] with [C] as the - continuation. In [C], [x] refers to the output of [f]. *) - - (* [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)). - - (** A value of type [~>R] accepts a continuation that takes an - argument of type [R]. It is meant to be used in [Definition] and - such; for example: -<< - Definition add_cps (a b:nat) : ~> nat. ->> - The return type of the continuation is not yet specified; every - [~> 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). - - (** The type [A ~> R] contains functions that takes an argument of - type [A] and pass a value of type [R] to the continuation. Functions - that take multiple arguments can be encoded as [A -> B ~> C] or [A - ~> 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). - - (* [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)). -End CPSNotations. - Section with_state. Import CPSNotations. Context {state : Type}. |