Changeset 1599 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (9 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1485 r1599  
    2222         of add_with_carries *)
    2323     if last_carry then
    24       let bit ≝ exclusive_disjunction (exclusive_disjunction b c) true in
     24      let bit ≝ xorb (xorb b c) true in
    2525      let carry ≝ carry_of b c true in
    2626       〈bit:::lower_bits, carry:::carries〉
    2727     else
    28       let bit ≝ exclusive_disjunction (exclusive_disjunction b c) false in
     28      let bit ≝ xorb (xorb b c) false in
    2929      let carry ≝ carry_of b c false in
    3030       〈bit:::lower_bits, carry:::carries〉     
     
    4343     let 〈lower_bits, borrows〉 ≝ r in
    4444     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
    45      let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in
     45     let bit ≝ xorb (xorb b c) last_borrow in
    4646     let borrow ≝ borrow_of b c last_borrow in
    4747       〈bit:::lower_bits, borrow:::borrows〉
     
    6060    let 〈result, carries〉 ≝ add_with_carries n b c carry in
    6161    let cy_flag ≝ get_index_v ?? carries 0 ? in
    62     let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     62    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    6363    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
    6464      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     
    7676    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
    7777    let cy_flag ≝ get_index_v ?? carries 0 ? in
    78     let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
     78    let ov_flag ≝ xorb cy_flag (get_index_v ?? carries 1 ?) in
    7979    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
    8080      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
     
    311311      [ VEmpty ⇒ false
    312312      | VCons _ bwpn _ ⇒
    313         if exclusive_disjunction bwn bwpn then
     313        if xorb bwn bwpn then
    314314          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
    315315        else
     
    349349        let 〈c1,r〉 ≝ d in
    350350          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
    351            (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
     351           (xorb (xorb b1 b2) c1) ::: r〉)
    352352     〈d, [[ ]]〉 ? b c.
    353353   
Note: See TracChangeset for help on using the changeset viewer.