Changeset 337 for Deliverables/D4.1/Matita/Interpret.ma
 Timestamp:
 Nov 30, 2010, 12:26:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r334 r337 107 107 else 108 108 s 109 (* 110  ANL addr1 addr2 ⇒ 111 match addr1 return λx. bool_to_Prop (is_in … [[ acc_a; 112 direct; 113 carry ]] x) → ? with 114 [ ACC_A ⇒ λacc_a: True. ? 115  DIRECT d ⇒ λdirect: True. ? 116  CARRY ⇒ λcarry: True. ? 109  CLR addr ⇒ 110 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 111 [ ACC_A ⇒ λacc_a: True. set_arg_8 s ACC_A (zero eight) 112  CARRY ⇒ λcarry: True. set_arg_1 s CARRY false 113  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false 117 114  _ ⇒ λother: False. ? 118 ] (subaddressing_modein … addr1) *) 115 ] (subaddressing_modein … addr) 116  CPL addr ⇒ 117 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 118 [ ACC_A ⇒ λacc_a: True. 119 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 120 let new_acc ≝ negation_bv ? old_acc in 121 set_8051_sfr s SFR_ACC_A new_acc 122  CARRY ⇒ λcarry: True. 123 let old_cy_flag ≝ get_arg_1 s CARRY true in 124 let new_cy_flag ≝ negation old_cy_flag in 125 set_arg_1 s CARRY new_cy_flag 126  BIT_ADDR b ⇒ λbit_addr: True. 127 let old_bit ≝ get_arg_1 s (BIT_ADDR b) true in 128 let new_bit ≝ negation old_bit in 129 set_arg_1 s (BIT_ADDR b) new_bit 130  _ ⇒ λother: False. ? 131 ] (subaddressing_modein … addr) 132  SETB b ⇒ set_arg_1 s b false 133  RL _ ⇒ (* DPM: always ACC_A *) 134 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 135 let new_acc ≝ rotate_left_bv ? one old_acc in 136 set_8051_sfr s SFR_ACC_A new_acc 137  RR _ ⇒ (* DPM: always ACC_A *) 138 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 139 let new_acc ≝ rotate_right_bv ? one old_acc in 140 set_8051_sfr s SFR_ACC_A new_acc 141  RLC _ ⇒ (* DPM: always ACC_A *) 142 let old_cy_flag ≝ get_cy_flag s in 143 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 144 let new_cy_flag ≝ get_index_bv ? old_acc Z ? in 145 let new_acc ≝ shift_left_bv eight one old_acc old_cy_flag in 146 let s ≝ set_arg_1 s CARRY new_cy_flag in 147 set_8051_sfr s SFR_ACC_A new_acc 148  RRC _ ⇒ (* DPM: always ACC_A *) 149 let old_cy_flag ≝ get_cy_flag s in 150 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 151 let new_cy_flag ≝ get_index_bv ? old_acc seven ? in 152 let new_acc ≝ shift_right_bv eight one old_acc old_cy_flag in 153 let s ≝ set_arg_1 s CARRY new_cy_flag in 154 set_8051_sfr s SFR_ACC_A new_acc 155  SWAP _ ⇒ (* DPM: always ACC_A *) 156 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 157 let 〈nu,nl〉 ≝ split ? four four old_acc in 158 let new_acc ≝ nl @@ nu in 159 set_8051_sfr s SFR_ACC_A new_acc 160  PUSH addr ⇒ 161 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 162 [ DIRECT d ⇒ λdirect: True. 163 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) in 164 let s ≝ set_8051_sfr s SFR_SP new_sp in 165 write_at_stack_pointer s d 166  _ ⇒ λother: False. ? 167 ] (subaddressing_modein … addr) 168  POP addr ⇒ 169 let contents ≝ read_at_stack_pointer s in 170 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr s SFR_SP) (bitvector_of_nat eight one) false in 171 let s ≝ set_8051_sfr s SFR_SP new_sp in 172 set_arg_8 s addr contents 173  XCH addr1 addr2 ⇒ 174 let old_addr ≝ get_arg_8 s false addr2 in 175 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 176 let s ≝ set_8051_sfr s SFR_ACC_A old_addr in 177 set_arg_8 s addr2 old_acc 178  NOP ⇒ s 119 179  _ ⇒ s 120 180 ] 121 181 in 122 182 s. 123 124
Note: See TracChangeset
for help on using the changeset viewer.