diff options
-rw-r--r-- | src/Compilers/Named/Syntax.v | 2 | ||||
-rw-r--r-- | src/Compilers/Syntax.v | 2 | ||||
-rw-r--r-- | src/Spec/MxDH.v | 28 | ||||
-rw-r--r-- | src/Specific/FancyMachine256/Barrett.v | 6 | ||||
-rw-r--r-- | src/Specific/FancyMachine256/Core.v | 2 | ||||
-rw-r--r-- | src/Specific/FancyMachine256/Montgomery.v | 6 | ||||
-rw-r--r-- | src/Util/LetIn.v | 6 | ||||
-rw-r--r-- | src/Util/Notations.v | 14 |
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"). |