From 0079e9a94925a781cc96df59b7b45ec551c94c29 Mon Sep 17 00:00:00 2001 From: jadep Date: Sun, 18 Jun 2017 12:02:07 -0400 Subject: make scmul discard its carry in a saner way; rather than concatenating it in and then dropping it, we just ignore it --- src/Arithmetic/Saturated.v | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'src/Arithmetic/Saturated.v') diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index f3cd09569..0904e6332 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -734,15 +734,10 @@ Section API. Definition scmul_cps {n} (c : Z) (p : T n) {R} (f:T (S n)->R) := Columns.mul_cps (n1:=1) (n3:=S n) (uweight bound) bound c p - (fun carry_result => - Tuple.left_append_cps (fst carry_result) (snd carry_result) (* The carry that comes out of Columns.mul_cps will be 0, since (S n) limbs is enough to hold the result of the - multiplication. To make this extra limb disappear, we could - convert to and from associational, simply indicating that we - only need to have (S n) limbs when converting back, but we - don't, instead dropping it later. *) - (fun v => drop_high_cps v f)). + multiplication, so we can safely discard it. *) + (fun carry_result =>f (snd carry_result)). Definition scmul {n} c p : T (S n) := @scmul_cps n c p _ id. Definition add_cps {n m pred_nm} (p : T n) (q : T m) {R} (f:T (S pred_nm)->R) := -- cgit v1.2.3