Changeset 1485 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Nov 2, 2011, 6:58:23 PM (8 years ago)
Author:
sacerdot
Message:

Less nice definitiion of add_with_carries that avoids a quadratic blow-up of
the whd normal form.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1426 r1485  
    1919     let 〈lower_bits, carries〉 ≝ r in
    2020     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
    21      let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in
    22      let carry ≝ carry_of b c last_carry in
     21      (* Next if-then-else just to avoid a quadratic blow-up of the whd of an application
     22         of add_with_carries *)
     23     if last_carry then
     24      let bit ≝ exclusive_disjunction (exclusive_disjunction b c) true in
     25      let carry ≝ carry_of b c true in
    2326       〈bit:::lower_bits, carry:::carries〉
     27     else
     28      let bit ≝ exclusive_disjunction (exclusive_disjunction b c) false in
     29      let carry ≝ carry_of b c false in
     30       〈bit:::lower_bits, carry:::carries〉     
    2431   )
    2532   〈[[ ]], [[ ]]〉 n x y.
Note: See TracChangeset for help on using the changeset viewer.