Ignore:
Timestamp:
Dec 2, 2010, 11:53:49 AM (9 years ago)
Author:
sacerdot
Message:

Less ambiguous definitions.

File:
1 edited

Legend:

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

    r358 r362  
    1919            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    2020                                                   (get_arg_8 s false addr2) false in
    21             let cy_flag ≝ get_index … flags Z ? in
    22             let ac_flag ≝ get_index … flags one ? in
    23             let ov_flag ≝ get_index … flags two ? in
     21            let cy_flag ≝ get_index_v … flags Z ? in
     22            let ac_flag ≝ get_index_v … flags one ? in
     23            let ov_flag ≝ get_index_v … flags two ? in
    2424            let s ≝ set_arg_8 s ACC_A result in
    2525              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    2828            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1)
    2929                                                   (get_arg_8 s false addr2) old_cy_flag in
    30             let cy_flag ≝ get_index … flags Z ? in
    31             let ac_flag ≝ get_index … flags one ? in
    32             let ov_flag ≝ get_index … flags two ? in
     30            let cy_flag ≝ get_index_v … flags Z ? in
     31            let ac_flag ≝ get_index_v … flags one ? in
     32            let ov_flag ≝ get_index_v … flags two ? in
    3333            let s ≝ set_arg_8 s ACC_A result in
    3434              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    3737            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1)
    3838                                                   (get_arg_8 s false addr2) old_cy_flag in
    39             let cy_flag ≝ get_index … flags Z ? in
    40             let ac_flag ≝ get_index … flags one ? in
    41             let ov_flag ≝ get_index … flags two ? in
     39            let cy_flag ≝ get_index_v … flags Z ? in
     40            let ac_flag ≝ get_index_v … flags one ? in
     41            let ov_flag ≝ get_index_v … flags two ? in
    4242            let s ≝ set_arg_8 s ACC_A result in
    4343              set_flags s cy_flag (Just Bit ac_flag) ov_flag
     
    142142              if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then
    143143                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in
    144                 let cy_flag ≝ get_index ? flags Z ? in
     144                let cy_flag ≝ get_index_v … flags Z ? in
    145145                let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in
    146146                  if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then
     
    179179        | RL _ ⇒ (* DPM: always ACC_A *)
    180180            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    181             let new_acc ≝ rotate_left_bv ? one old_acc in
     181            let new_acc ≝ rotate_left … one old_acc in
    182182              set_8051_sfr s SFR_ACC_A new_acc
    183183        | RR _ ⇒ (* DPM: always ACC_A *)
    184184            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    185             let new_acc ≝ rotate_right_bv ? one old_acc in
     185            let new_acc ≝ rotate_right … one old_acc in
    186186              set_8051_sfr s SFR_ACC_A new_acc
    187187        | RLC _ ⇒ (* DPM: always ACC_A *)
    188188            let old_cy_flag ≝ get_cy_flag s in
    189189            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    190             let new_cy_flag ≝ get_index_bv ? old_acc Z ? in
    191             let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in
     190            let new_cy_flag ≝ get_index_v … old_acc Z ? in
     191            let new_acc ≝ shift_left … eight one old_acc old_cy_flag in
    192192            let s ≝ set_arg_1 s CARRY new_cy_flag in
    193193              set_8051_sfr s SFR_ACC_A new_acc
     
    195195            let old_cy_flag ≝ get_cy_flag s in
    196196            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    197             let new_cy_flag ≝ get_index_bv ? old_acc seven ? in
    198             let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in
     197            let new_cy_flag ≝ get_index_v … old_acc seven ? in
     198            let new_acc ≝ shift_right … eight one old_acc old_cy_flag in
    199199            let s ≝ set_arg_1 s CARRY new_cy_flag in
    200200              set_8051_sfr s SFR_ACC_A new_acc
     
    384384              let 〈pc_bu, pc_bl〉 ≝ split ? eight eight (program_counter s) in
    385385              let 〈nu, nl〉 ≝ split ? four four pc_bu in
    386               let bit ≝ get_index_bv ? nl Z ? in
     386              let bit ≝ get_index_v … nl Z ? in
    387387              let 〈relevant1, relevant2〉 ≝ split ? three eight a in
    388388              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
Note: See TracChangeset for help on using the changeset viewer.