Support destructuring dlet and slet

The current way to support it is a kludge around the fact that `x
binder` only works for recursive notations

8 files changed, 34 insertions, 32 deletions

diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v
index 035d7fb49..a79628cb2 100644
--- a/src/Compilers/Named/Syntax.v
+++ b/src/Compilers/Named/Syntax.v
@@ -85,7 +85,7 @@ Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _.
 Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _.
 Global Arguments Interp {_ _ _ _ _ interp_op t} _ _.
 
-Notation "'slet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope.
+Notation "'nlet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope.
 Notation "'λn'  x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope.
 Notation "( x , y , .. , z )" := (Pair .. (Pair x%nexpr y%nexpr) .. z%nexpr) : nexpr_scope.
 Notation "()" := TT : nexpr_scope.
diff --git a/src/Compilers/Syntax.v b/src/Compilers/Syntax.v
index d8b88e560..0e8f924da 100644
--- a/src/Compilers/Syntax.v
+++ b/src/Compilers/Syntax.v
@@ -143,7 +143,7 @@ Module Export Notations.
   Notation "()" := (@Unit _) : ctype_scope.
   Notation "A * B" := (@Prod _ A B) : ctype_scope.
   Notation "A -> B" := (@Arrow _ A B) : ctype_scope.
-  Notation "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope.
+  Notation "'slet' x .. y := A 'in' b" := (LetIn A%expr (fun x => .. (fun y => b%expr) .. )) : expr_scope.
   Notation "'λ'  x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope.
   Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope.
   Notation "( )" := TT : expr_scope.
diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v
index bee9c784d..ec71cbc95 100644
--- a/src/Spec/MxDH.v
+++ b/src/Spec/MxDH.v
@@ -31,23 +31,23 @@ Module MxDH. (* from RFC7748 *)
       Context (F4 : Type)
               (pair4 : F -> F -> F -> F -> F4)
               (let_in : F -> (F -> F4) -> F4).
-      Local Notation "'slet' x := y 'in' z" := (let_in y (fun x => z)).
+      Local Notation "'llet' x := y 'in' z" := (let_in y (fun x => z)).
       Definition ladderstep_gen (X1:F) (P1 P2:F * F) : F4 :=
         let '(X2, Z2) := P1 in
         let '(X3, Z3) := P2 in
-        slet A := X2+Z2 in
-        slet AA := A^2 in
-        slet B := X2-Z2 in
-        slet BB := B^2 in
-        slet E := AA-BB in
-        slet C := X3+Z3 in
-        slet D := X3-Z3 in
-        slet DA := D*A in
-        slet CB := C*B in
-        slet X5 := (DA+CB)^2 in
-        slet Z5 := X1*(DA-CB)^2 in
-        slet X4 := AA*BB in
-        slet Z4 := E*(AA + a24*E) in
+        llet A := X2+Z2 in
+        llet AA := A^2 in
+        llet B := X2-Z2 in
+        llet BB := B^2 in
+        llet E := AA-BB in
+        llet C := X3+Z3 in
+        llet D := X3-Z3 in
+        llet DA := D*A in
+        llet CB := C*B in
+        llet X5 := (DA+CB)^2 in
+        llet Z5 := X1*(DA-CB)^2 in
+        llet X4 := AA*BB in
+        llet Z4 := E*(AA + a24*E) in
         pair4 X4 Z4 X5 Z5.
     End generic.
 
diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v
index 263bc82ba..6bd97b10c 100644
--- a/src/Specific/FancyMachine256/Barrett.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -129,9 +129,9 @@ Print compiled_syntax.
 (* compiled_syntax =
 fun ops : fancy_machine.instructions (2 * 128) =>
 λn (RegMod, RegMuLow, x, xHigh),
-slet RegMod := RegMod in
-slet RegMuLow := RegMuLow in
-slet RegZero := ldi 0 in
+nlet RegMod := RegMod in
+nlet RegMuLow := RegMuLow in
+nlet RegZero := ldi 0 in
 c.Rshi(tmp, xHigh, x, 250),
 c.Mul128(q, c.LowerHalf(tmp), c.LowerHalf(RegMuLow)),
 c.Mul128(qHigh, c.UpperHalf(tmp), c.UpperHalf(RegMuLow)),
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 517644572..0d521ae17 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -255,7 +255,7 @@ Open Scope core_scope.
 Notation Return x := (Var x).
 Notation Const z := (Op (@OPconst _ _ z) TT).
 Notation ldi z := (Op OPldi (Const z%Z)).
-Notation "'slet' x := A 'in' b" := (LetIn _ x (Op OPldi (Var A%nexpr)) b%nexpr) : nexpr_scope.
+Notation "'nlet' x := A 'in' b" := (LetIn _ x (Op OPldi (Var A%nexpr)) b%nexpr) : nexpr_scope.
 Notation "'c.Rshi' ( x , A , B , C ) , b" :=
   (LetIn _ x (Op OPshrd (Pair (Pair (Var A) (Var B)) (Const C%Z))) b)
     (at level 200, b at level 200, format "'c.Rshi' ( x ,  A ,  B ,  C ) , '//' b").
diff --git a/src/Specific/FancyMachine256/Montgomery.v b/src/Specific/FancyMachine256/Montgomery.v
index e6af32aab..1f0655ac9 100644
--- a/src/Specific/FancyMachine256/Montgomery.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -129,9 +129,9 @@ Print compiled_syntax.
 (* compiled_syntax =
 fun ops : fancy_machine.instructions (2 * 128) =>
 λn (RegMod, RegPInv, lo, hi),
-slet RegMod := RegMod in
-slet RegPInv := RegPInv in
-slet RegZero := ldi 0 in
+nlet RegMod := RegMod in
+nlet RegPInv := RegPInv in
+nlet RegZero := ldi 0 in
 c.Mul128(y, c.LowerHalf(lo), c.LowerHalf(RegPInv)),
 c.Mul128(t1, c.UpperHalf(lo), c.LowerHalf(RegPInv)),
 c.Add(y, y, c.LeftShifted{t1, 128}),
diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v
index 69cacd75e..92c7b51ad 100644
--- a/src/Util/LetIn.v
+++ b/src/Util/LetIn.v
@@ -5,12 +5,12 @@ Require Import Crypto.Util.Notations.
 
 Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
 Definition Let_In_pf {A P} (x : A) (f : forall a : A, a = x -> P a) : P x := let y := x in f y eq_refl.
-Notation "'dlet_nd' x := y 'in' f" := (Let_In (P:=fun _ => _) y (fun x => f)) (only parsing).
-Notation "'dlet' x := y 'in' f" := (Let_In y (fun x => f)).
+Notation "'dlet_nd' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )) (only parsing).
+Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
 Notation "'pflet' x , pf := y 'in' f" := (Let_In_pf y (fun x pf => f)).
 
 Module Bug5107WorkAround.
-  Notation "'dlet' x := y 'in' f" := (Let_In (P:=fun _ => _) y (fun x => f)).
+  Notation "'dlet' x .. y := v 'in' f" := (Let_In (P:=fun _ => _) v (fun x => .. (fun y => f) .. )).
 End Bug5107WorkAround.
 
 Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R}
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index ca593edac..feffc0f4b 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -69,17 +69,19 @@ Reserved Notation "u {{ i }}" (at level 30).
 Reserved Notation "a # b" (at level 55, no associativity). (* match with theories/QArith/QArith_base.v *)
 Reserved Notation "'plet' x := y 'in' z"
          (at level 200, z at level 200, format "'plet'  x  :=  y  'in' '//' z").
-Reserved Notation "'slet' x := A 'in' b"
-         (at level 200, b at level 200, format "'slet'  x  :=  A  'in' '//' b").
+Reserved Notation "'nlet' x := A 'in' b"
+         (at level 200, b at level 200, format "'nlet'  x  :=  A  'in' '//' b").
+Reserved Notation "'slet' x .. y := A 'in' b"
+         (at level 200, x binder, y binder, b at level 200, format "'slet'  x .. y  :=  A  'in' '//' b").
 Reserved Notation "'llet' x := A 'in' b"
          (at level 200, b at level 200, format "'llet'  x  :=  A  'in' '//' b").
 Reserved Notation "'mlet' x := A 'in' b"
          (at level 200, b at level 200, format "'mlet'  x  :=  A  'in' '//' b").
 (* Note that making [Let] a keyword breaks the vernacular [Let] in Coq 8.4 *)
-Reserved Notation "'dlet_nd' x := y 'in' f"
-         (at level 200, f at level 200, format "'dlet_nd'  x  :=  y  'in' '//' f").
-Reserved Notation "'dlet' x := y 'in' f"
-         (at level 200, f at level 200, format "'dlet'  x  :=  y  'in' '//' f").
+Reserved Notation "'dlet_nd' x .. y := v 'in' f"
+         (at level 200, x binder, y binder, f at level 200, format "'dlet_nd'  x .. y  :=  v  'in' '//' f").
+Reserved Notation "'dlet' x .. y := v 'in' f"
+         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
 Reserved Notation "'pflet' x , pf := y 'in' f"
          (at level 200, f at level 200, format "'pflet'  x ,  pf  :=  y  'in' '//' f").
 Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity, format "'λ'  x .. y , '//' t").