Changeset 333 for Deliverables/D4.1/Matita/Interpret.ma
 Timestamp:
 Nov 29, 2010, 4:12:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r331 r333 14 14 match instr with 15 15 [ ADD addr1 addr2 ⇒ 16 match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with 17 [ ACC_A ⇒ λacc_a: True. 18 match addr2 return λx. bool_to_Prop (is_in … [[ register; 19 direct; 20 indirect; 21 data ]] x) → ? with 22 [ REGISTER r ⇒ λregister: True. 23 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 24 (get_arg_8 s false (REGISTER r)) false in 25 let cy_flag ≝ get_index … flags Z ? in 26 let ac_flag ≝ get_index … flags one ? in 27 let ov_flag ≝ get_index … flags two ? in 28 let s ≝ set_arg_8 s ACC_A result in 29 set_flags s cy_flag (Just Bit ac_flag) ov_flag 30  DIRECT d ⇒ λdirect: True. 31 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 32 (get_arg_8 s false (DIRECT d)) false in 33 let cy_flag ≝ get_index … flags Z ? in 34 let ac_flag ≝ get_index … flags one ? in 35 let ov_flag ≝ get_index … flags two ? in 36 let s ≝ set_arg_8 s ACC_A result in 37 set_flags s cy_flag (Just Bit ac_flag) ov_flag 38  INDIRECT i ⇒ λindirect: True. 39 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 40 (get_arg_8 s false (INDIRECT i)) false in 41 let cy_flag ≝ get_index … flags Z ? in 42 let ac_flag ≝ get_index … flags one ? in 43 let ov_flag ≝ get_index … flags two ? in 44 let s ≝ set_arg_8 s ACC_A result in 45 set_flags s cy_flag (Just Bit ac_flag) ov_flag 46  DATA d ⇒ λdata: True. 47 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 48 (get_arg_8 s false (DATA d)) false in 49 let cy_flag ≝ get_index … flags Z ? in 50 let ac_flag ≝ get_index … flags one ? in 51 let ov_flag ≝ get_index … flags two ? in 52 let s ≝ set_arg_8 s ACC_A result in 53 set_flags s cy_flag (Just Bit ac_flag) ov_flag 54  _ ⇒ λother: False. ? 55 ] (subaddressing_modein … addr2) 56  _ ⇒ λother: False. ? 57 ] (subaddressing_modein … addr1) 16 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 17 (get_arg_8 s false addr2) false in 18 let cy_flag ≝ get_index … flags Z ? in 19 let ac_flag ≝ get_index … flags one ? in 20 let ov_flag ≝ get_index … flags two ? in 21 let s ≝ set_arg_8 s ACC_A result in 22 set_flags s cy_flag (Just Bit ac_flag) ov_flag 58 23  ADDC addr1 addr2 ⇒ 59 24 let old_cy_flag ≝ get_cy_flag s in 60 match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with 25 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false addr1) 26 (get_arg_8 s false addr2) old_cy_flag in 27 let cy_flag ≝ get_index … flags Z ? in 28 let ac_flag ≝ get_index … flags one ? in 29 let ov_flag ≝ get_index … flags two ? in 30 let s ≝ set_arg_8 s ACC_A result in 31 set_flags s cy_flag (Just Bit ac_flag) ov_flag 32  SUBB addr1 addr2 ⇒ 33 let old_cy_flag ≝ get_cy_flag s in 34 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 s false addr1) 35 (get_arg_8 s false addr2) old_cy_flag in 36 let cy_flag ≝ get_index … flags Z ? in 37 let ac_flag ≝ get_index … flags one ? in 38 let ov_flag ≝ get_index … flags two ? in 39 let s ≝ set_arg_8 s ACC_A result in 40 set_flags s cy_flag (Just Bit ac_flag) ov_flag 41  INC addr ⇒ 42 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 43 register; 44 direct; 45 indirect; 46 dptr ]] x) → ? with 61 47 [ ACC_A ⇒ λacc_a: True. 62 match addr2 return λx. bool_to_Prop (is_in … [[ register; 63 direct; 64 indirect; 65 data ]] x) → ? with 66 [ REGISTER r ⇒ λregister: True. 67 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 68 (get_arg_8 s false (REGISTER r)) old_cy_flag in 69 let cy_flag ≝ get_index … flags Z ? in 70 let ac_flag ≝ get_index … flags one ? in 71 let ov_flag ≝ get_index … flags two ? in 72 let s ≝ set_arg_8 s ACC_A result in 73 set_flags s cy_flag (Just Bit ac_flag) ov_flag 74  DIRECT d ⇒ λdirect: True. 75 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 76 (get_arg_8 s false (DIRECT d)) old_cy_flag in 77 let cy_flag ≝ get_index … flags Z ? in 78 let ac_flag ≝ get_index … flags one ? in 79 let ov_flag ≝ get_index … flags two ? in 80 let s ≝ set_arg_8 s ACC_A result in 81 set_flags s cy_flag (Just Bit ac_flag) ov_flag 82  INDIRECT i ⇒ λindirect: True. 83 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 84 (get_arg_8 s false (INDIRECT i)) old_cy_flag in 85 let cy_flag ≝ get_index … flags Z ? in 86 let ac_flag ≝ get_index … flags one ? in 87 let ov_flag ≝ get_index … flags two ? in 88 let s ≝ set_arg_8 s ACC_A result in 89 set_flags s cy_flag (Just Bit ac_flag) ov_flag 90  DATA d ⇒ λdata: True. 91 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A) 92 (get_arg_8 s false (DATA d)) old_cy_flag in 93 let cy_flag ≝ get_index … flags Z ? in 94 let ac_flag ≝ get_index … flags one ? in 95 let ov_flag ≝ get_index … flags two ? in 96 let s ≝ set_arg_8 s ACC_A result in 97 set_flags s cy_flag (Just Bit ac_flag) ov_flag 98  _ ⇒ λother: False. ? 99 ] (subaddressing_modein … addr2) 100  _ ⇒ λother: False. ? 101 ] (subaddressing_modein … addr1) 48 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true ACC_A) (bitvector_of_nat eight one) in 49 set_arg_8 s ACC_A result 50  REGISTER r ⇒ λregister: True. 51 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (REGISTER r)) (bitvector_of_nat eight one) in 52 set_arg_8 s (REGISTER r) result 53  DIRECT d ⇒ λdirect: True. 54 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (DIRECT d)) (bitvector_of_nat eight one) in 55 set_arg_8 s (DIRECT d) result 56  INDIRECT i ⇒ λindirect: True. 57 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 s true (INDIRECT i)) (bitvector_of_nat eight one) in 58 set_arg_8 s (INDIRECT i) result 59  DPTR ⇒ λdptr: True. 60 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr s SFR_DPL) (bitvector_of_nat eight one) in 61 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr s SFR_DPH) (zero eight) carry in 62 let s ≝ set_8051_sfr s SFR_DPL bl in 63 set_8051_sfr s SFR_DPH bu 64  _ ⇒ λother: False. ? 65 ] (subaddressing_modein … addr) 66  DEC addr ⇒ 67 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 s true addr) (bitvector_of_nat eight one) false in 68 set_arg_8 s addr result 69  MUL addr1 addr2 ⇒ 70 let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in 71 let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in 72 let product ≝ acc_a_nat * acc_b_nat in 73 let ov_flag ≝ product ≥ two_hundred_and_fifty_six in 74 let low ≝ bitvector_of_nat eight (product mod two_hundred_and_fifty_six) in 75 let high ≝ bitvector_of_nat eight (product ÷ two_hundred_and_fifty_six) in 76 let s ≝ set_8051_sfr s SFR_ACC_A low in 77 set_8051_sfr s SFR_ACC_B high 78  DIV addr1 addr2 ⇒ 79 let acc_a_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_A) in 80 let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in 81 match acc_b_nat with 82 [ Z ⇒ set_flags s false (Nothing Bit) true 83  S o ⇒ 84 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in 85 let r ≝ bitvector_of_nat eight (acc_a_nat mod two_hundred_and_fifty_six) in 86 let s ≝ set_8051_sfr s SFR_ACC_A q in 87 let s ≝ set_8051_sfr s SFR_ACC_B r in 88 set_flags s false (Nothing Bit) false 89 ] 90 (* 91 DA addr ⇒ 92 match addr return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with 93 [ ACC_A ⇒ λacc_a: True. 94 let 〈 acc_nu, acc_nl 〉 ≝ 95  _ ⇒ λother: False. ? 96 ] (subaddressing_modein … addr) *) 102 97  _ ⇒ s 103 98 ]
Note: See TracChangeset
for help on using the changeset viewer.