Changeset 272


Ignore:
Timestamp:
Nov 24, 2010, 1:43:28 PM (9 years ago)
Author:
mulligan
Message:

Changes from this morning.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r260 r272  
    6262nqed.
    6363
    64 (*
     64naxiom less_than_b: Nat → Nat → Bool.
     65
    6566ndefinition sub_8_with_carry ≝
    6667  λb: BitVector eight.
     
    7071    let c_as_nat ≝ nat_of_bitvector eight c in
    7172    let carry_as_nat ≝ nat_of_bool carry in
    72     let result_old_1 ≝ subtraction_underflow b_as_nat c_as_nat in
    73       match result_old_1 with
    74         [ Nothing ⇒
    75           let ac_flag ≝ True in
    76          
    77         | Just result_old_1' ⇒
    78         ]
    79 *)
     73    let result_old_1 ≝ minus (minus b_as_nat c_as_nat) carry_as_nat in
     74    let modulus_1 ≝ (modulus b_as_nat sixteen) - (modulus c_as_nat sixteen) in
     75      match less_than_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) with
     76        [ true ⇒
     77          let ac_flag ≝ true in
     78          let result_old_2 ≝ (minus (modulus b_as_nat one_hundred_and_twenty_eight)
     79                                   (modulus c_as_nat one_hundred_and_twenty_eight)) in
     80            match less_than_b (modulus b_as_nat one_hundred_and_twenty_eight)
     81                              (modulus c_as_nat one_hundred_and_twenty_eight) with
     82            [ true ⇒
     83              let bit_six ≝ true in
     84              let result_carry ≝ mk_Cartesian … result_old_1 false in
     85              let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
     86                mk_Cartesian … (first … result_carry) (second … result_carry :: ac_flag :: ov_flag :: Empty Bool)
     87            | false ⇒ ?
     88            ]
     89        | false ⇒ ?
     90        ].
     91   
    8092   
    8193ndefinition add_8_with_carry ≝ add_n_with_carry eight.
  • Deliverables/D4.1/Matita/Assembly.ma

    r271 r272  
    7474      [ ADDR11 w ⇒ λ_.
    7575         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
    76           [ (v1 @ [[true; false; false; false; true]]) ; v2 ]
     76          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    7777      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    7878  | ADD addr1 addr2 ⇒
  • Deliverables/D4.1/Matita/Vector.ma

    r269 r272  
    237237    ].
    238238   
    239 interpretation "Vector append" 'append v1 v2 = (append ??? v1 v2).
     239notation "hvbox(l break @@ r)"
     240  right associative with precedence 47
     241  for @{ 'vappend $l $r }.
     242   
     243interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
    240244   
    241245nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.