diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-05-14 22:12:27 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-05-14 22:12:27 -0400 |
commit | c3b995c787948453c51b8b609d8bab43954d5875 (patch) | |
tree | f2093358b4eb637bf5d0b68218bceb3b4d411e29 /src/Compilers | |
parent | 2eefc10c76edd1d80056bb17742279893a2c918b (diff) | |
parent | 0cfe07ebe12e97707feef3d5acca50c30e59531e (diff) |
Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into return-notation
Diffstat (limited to 'src/Compilers')
-rw-r--r-- | src/Compilers/Z/CNotations.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v index 0fcee43e0..7503f6c34 100644 --- a/src/Compilers/Z/CNotations.v +++ b/src/Compilers/Z/CNotations.v @@ -4,13 +4,23 @@ Require Export Crypto.Compilers.Z.HexNotationConstants. Require Export Crypto.Util.Notations. Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T x = A ; '//' b"). +Reserved Notation "T x = A ; 'return' b" (at level 200, b at level 200, format "T x = A ; '//' 'return' b"). +Reserved Notation "T x = A ; 'return' ( b0 , b1 , .. , b2 )" (at level 200, format "T x = A ; '//' 'return' ( b0 , b1 , .. , b2 )"). Reserved Notation "T0 x , T1 y = A ; b" (at level 200, b at level 200, format "T0 x , T1 y = A ; '//' b"). +Reserved Notation "T0 x , T1 y = A ; 'return' b" (at level 200, b at level 200, format "T0 x , T1 y = A ; '//' 'return' b"). +Reserved Notation "T0 x , T1 y = A ; 'return' ( b0 , b1 , .. , b2 )" (at level 200, format "T0 x , T1 y = A ; '//' 'return' ( b0 , b1 , .. , b2 )"). Reserved Notation "x & y" (at level 40). Global Open Scope expr_scope. Notation "T x = A ; b" := (LetIn (tx:=T) A (fun x => b)) : expr_scope. +Notation "T x = A ; 'return' b" := (LetIn (tx:=T) A (fun x => Var b)) : expr_scope. +Notation "T x = A ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A (fun x => Pair .. (Pair b0%expr b1%expr) .. b2%expr)) : expr_scope. +Notation "T x = A ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=T) A (fun x => Pair .. (Pair (Var b0) (Var b1)) .. (Var b2))) : expr_scope. Notation "T0 x , T1 y = A ; b" := (LetIn (tx:=Prod T0 T1) A (fun '((x, y)%core) => b)) : expr_scope. +Notation "T0 x , T1 y = A ; 'return' b" := (LetIn (tx:=Prod T0 T1) A (fun '((x, y)%core) => Var b)) : expr_scope. +(*Notation "T0 x , T1 y = A ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=Prod T0 T1) A (fun '((x, y)%core) => (Pair .. (Pair b0%expr b1%expr) .. b2%expr))) : expr_scope.*) (* Error: Unsupported construction in recursive notations., https://coq.inria.fr/bugs/show_bug.cgi?id=5523 *) +(*Notation "T0 x , T1 y = A ; 'return' ( b0 , b1 , .. , b2 )" := (LetIn (tx:=Prod T0 T1) A (fun '((x, y)%core) => (Pair .. (Pair (Var b0) (Var b1)) .. (Var b2)))) : expr_scope.*) (* Error: Unsupported construction in recursive notations., https://coq.inria.fr/bugs/show_bug.cgi?id=5523 *) (* python: << #!/usr/bin/env python |