diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 20:19:03 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 20:20:52 -0400 |
| commit | eb48024cb863bcf8a21ff771de94c5b69dabfd26 (patch) | |
| tree | d12d99081e7244609f14b81970547795abc8b00f /src | |
| parent | 58506ed7037dd56ef4ae44b96704812d53484320 (diff) | |
Stick 'return' at the end of printed functions
Diffstat (limited to 'src')
| -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 |