Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into return-notation

6 files changed, 15 insertions, 5 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
diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log
index 9ccfe2be2..c60adbe6e 100644
--- a/src/Specific/IntegrationTestLadderstep130Display.log
+++ b/src/Specific/IntegrationTestLadderstep130Display.log
@@ -363,7 +363,7 @@ let (a, b) := Interp-η
  uint128_t x391 = x390 >> 0x55;
  uint128_t x392 = x390 & 0x1fffffffffffffffffffffL;
  uint128_t x393 = x391 + x385;
- (Return x140, Return x139, Return x136, (Return x201, Return x200, Return x197), (Return x315, Return x314, Return x311, (Return x393, Return x392, Return x389))))
+ return (Return x140, Return x139, Return x136, (Return x201, Return x200, Return x197), (Return x315, Return x314, Return x311, (Return x393, Return x392, Return x389))))
 (x, (x0, x1), (x2, x3))%core in
 (let (a0, b0) := a in
 (a0, b0), let (a0, b0) := b in
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.log b/src/Specific/IntegrationTestLadderstepDisplay.log
index beac5d641..eac4db307 100644
--- a/src/Specific/IntegrationTestLadderstepDisplay.log
+++ b/src/Specific/IntegrationTestLadderstepDisplay.log
@@ -660,7 +660,7 @@ let (a, b) := Interp-η
  uint64_t x708 = x707 >> 0x33;
  uint64_t x709 = x707 & 0x7ffffffffffff;
  uint64_t x710 = x708 + x696;
- (Return x238, Return x235, Return x246, Return x245, Return x242, (Return x351, Return x348, Return x359, Return x358, Return x355), (Return x567, Return x564, Return x575, Return x574, Return x571, (Return x702, Return x699, Return x710, Return x709, Return x706))))
+ return (Return x238, Return x235, Return x246, Return x245, Return x242, (Return x351, Return x348, Return x359, Return x358, Return x355), (Return x567, Return x564, Return x575, Return x574, Return x571, (Return x702, Return x699, Return x710, Return x709, Return x706))))
 (x, (x0, x1), (x2, x3))%core in
 (let (a0, b0) := a in
 (a0, b0), let (a0, b0) := b in
diff --git a/src/Specific/IntegrationTestMulDisplay.log b/src/Specific/IntegrationTestMulDisplay.log
index 5f2d7c372..87da411a0 100644
--- a/src/Specific/IntegrationTestMulDisplay.log
+++ b/src/Specific/IntegrationTestMulDisplay.log
@@ -73,6 +73,6 @@ Interp-η
  uint64_t x88 = x87 >> 0x33;
  uint64_t x89 = x87 & 0x7ffffffffffff;
  uint64_t x90 = x88 + x76;
- (Return x82, Return x79, Return x90, Return x89, Return x86))
+ return (x82, x79, x90, x89, x86))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/IntegrationTestSquareDisplay.log b/src/Specific/IntegrationTestSquareDisplay.log
index 385cc6b06..488850576 100644
--- a/src/Specific/IntegrationTestSquareDisplay.log
+++ b/src/Specific/IntegrationTestSquareDisplay.log
@@ -56,6 +56,6 @@ Interp-η
  uint64_t x60 = x59 >> 0x33;
  uint64_t x61 = x59 & 0x7ffffffffffff;
  uint64_t x62 = x60 + x48;
- (Return x54, Return x51, Return x62, Return x61, Return x58))
+ return (x54, x51, x62, x61, x58))
 x
      : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/IntegrationTestSubDisplay.log b/src/Specific/IntegrationTestSubDisplay.log
index d341daa26..7bf04267e 100644
--- a/src/Specific/IntegrationTestSubDisplay.log
+++ b/src/Specific/IntegrationTestSubDisplay.log
@@ -34,6 +34,6 @@ Interp-η
  uint64_t x49 = x48 >> 0x33;
  uint64_t x50 = x48 & 0x7ffffffffffff;
  uint64_t x51 = x49 + x37;
- (Return x43, Return x40, Return x51, Return x50, Return x47))
+ return (x43, x40, x51, x50, x47))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)