diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 13:58:46 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-13 13:58:46 -0400 |
| commit | 2854cff14f95693819d42b611fe75a4904d9c77d (patch) | |
| tree | c105298f538c87a2bd0ac19d1a4e273827e0709d /src/Specific | |
| parent | de7a98b8711f13f9b9bba016c1d19db730479c8e (diff) | |
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
Diffstat (limited to 'src/Specific')
| -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 |
3 files changed, 7 insertions, 7 deletions
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}), |