Ignore:
Timestamp:
Mar 10, 2011, 11:48:33 AM (9 years ago)
Author:
mulligan
Message:

Changed output of Intel HEX files so we no longer have those gargantuan blocks of zeroes at the end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Demo-March-2011/matita/Arithmetic.ma

    r644 r664  
    3131                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3232
    33 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝
    34   λb: BitVector eight.
    35   λc: BitVector eight.
     33ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
     34  λn: Nat.
     35  λb: BitVector n.
     36  λc: BitVector n.
    3637  λcarry: Bool.
    37     let b_as_nat ≝ nat_of_bitvector eight b in
    38     let c_as_nat ≝ nat_of_bitvector eight c in
    39     let carry_as_nat ≝ nat_of_bool carry in
    40     let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
    41     let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in
    42     let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≲ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≲ carry_as_nat)) in
    43     let old_result_1 ≝ b_as_nat - c_as_nat in
    44     let old_result_2 ≝ old_result_1 - carry_as_nat in
    45     let ov_flag ≝ exclusive_disjunction carry bit_six in
    46       match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
    47         [ false ⇒
    48            let cy_flag ≝ false in
    49             〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉
    50         | true ⇒
    51            let cy_flag ≝ true in
    52            let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
    53             〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉
    54         ].
     38     let b_as_nat ≝ nat_of_bitvector n b in
     39     let c_as_nat ≝ nat_of_bitvector n c in
     40     let carry_as_nat ≝ nat_of_bool carry in
     41     let temporary ≝ (b_as_nat mod (two * n)) - (c_as_nat mod (two * n)) in
     42     let ac_flag ≝ less_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two * n)) + carry_as_nat) in
     43     let bit_six ≝ less_than_b (b_as_nat mod (two^(n - one))) ((c_as_nat mod (two^(n - one))) + carry_as_nat) in
     44     let 〈b',cy_flag〉 ≝
     45       if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then
     46         〈b_as_nat, false〉
     47       else
     48         〈b_as_nat + (two^n), true〉
     49     in
     50       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
     51         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.
     52
     53
     54ndefinition sub_8_with_carry ≝ sub_n_with_carry eight.
     55ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen.
    5556         
    5657ndefinition add_8_with_carry ≝ add_n_with_carry eight.
Note: See TracChangeset for help on using the changeset viewer.