From 01874b3bfe5d9788d7c3dfd2432993e99c4595da Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 30 Mar 2017 16:43:23 -0400 Subject: rename [Sorted] to [Columns] --- src/SaturatedBaseSystem.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/SaturatedBaseSystem.v') diff --git a/src/SaturatedBaseSystem.v b/src/SaturatedBaseSystem.v index c389644c7..f5f1b22fd 100644 --- a/src/SaturatedBaseSystem.v +++ b/src/SaturatedBaseSystem.v @@ -16,8 +16,8 @@ saturated limbs. Compatible with mixed-radix bases. ***) -Module Sorted. - Section Sorted. +Module Columns. + Section Columns. Context {weight : nat->Z} {weight_0 : weight 0%nat = 1} {weight_nonzero : forall i, weight i <> 0} @@ -256,8 +256,8 @@ Module Sorted. (fun P => B.Positional.to_associational_cps weight q (fun Q => from_associational_cps n (P++Q) f)). - End Sorted. -End Sorted. + End Columns. +End Columns. (* (* Just some pretty-printing *) @@ -268,17 +268,17 @@ Local Notation "snd~ a" := (let (_,y) := a in y) (at level 40, only printing). Definition base10 i := Eval compute in 10^(Z.of_nat i). Eval cbv -[runtime_add runtime_mul Let_In] in (fun adc a0 a1 a2 b0 b1 b2 => - Sorted.mul_cps (weight := base10) (n:=3) (a2,a1,a0) (b2,b1,b0) (fun ab => Sorted.compact (n:=5) (add_get_carry:=adc) (weight:=base10) ab)). + Columns.mul_cps (weight := base10) (n:=3) (a2,a1,a0) (b2,b1,b0) (fun ab => Columns.compact (n:=5) (add_get_carry:=adc) (weight:=base10) ab)). (* More complex example : base 2^56, 8 limbs *) Definition base2pow56 i := Eval compute in 2^(56*Z.of_nat i). Time Eval cbv -[runtime_add runtime_mul Let_In] in (fun adc a0 a1 a2 a3 a4 a5 a6 a7 b0 b1 b2 b3 b4 b5 b6 b7 => - Sorted.mul_cps (weight := base2pow56) (n:=8) (a7,a6,a5,a4,a3,a2,a1,a0) (b7,b6,b5,b4,b3,b2,b1,b0) (fun ab => Sorted.compact (n:=15) (add_get_carry:=adc) (weight:=base2pow56) ab)). (* Finished transaction in 151.392 secs *) + Columns.mul_cps (weight := base2pow56) (n:=8) (a7,a6,a5,a4,a3,a2,a1,a0) (b7,b6,b5,b4,b3,b2,b1,b0) (fun ab => Columns.compact (n:=15) (add_get_carry:=adc) (weight:=base2pow56) ab)). (* Finished transaction in 151.392 secs *) (* Mixed-radix example : base 2^25.5, 10 limbs *) Definition base2pow25p5 i := Eval compute in 2^(25*Z.of_nat i + ((Z.of_nat i + 1) / 2)). Time Eval cbv -[runtime_add runtime_mul Let_In] in (fun adc a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 => - Sorted.mul_cps (weight := base2pow25p5) (n:=10) (a9,a8,a7,a6,a5,a4,a3,a2,a1,a0) (b9,b8,b7,b6,b5,b4,b3,b2,b1,b0) (fun ab => Sorted.compact (n:=19) (add_get_carry:=adc) (weight:=base2pow25p5) ab)). (* Finished transaction in 97.341 secs *) + Columns.mul_cps (weight := base2pow25p5) (n:=10) (a9,a8,a7,a6,a5,a4,a3,a2,a1,a0) (b9,b8,b7,b6,b5,b4,b3,b2,b1,b0) (fun ab => Columns.compact (n:=19) (add_get_carry:=adc) (weight:=base2pow25p5) ab)). (* Finished transaction in 97.341 secs *) *) \ No newline at end of file -- cgit v1.2.3