Changeset 337
 Timestamp:
 Nov 30, 2010, 12:26:45 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r330 r337 29 29 (* ===================================== *) 30 30 31 ndefinition get_index ≝31 ndefinition get_index_bv ≝ 32 32 λn: Nat. 33 33 λb: BitVector n. … … 38 38 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). 39 39 40 ndefinition set_index ≝40 ndefinition set_index_bv ≝ 41 41 λn: Nat. 42 42 λb: BitVector n. … … 120 120 'exclusive_disjunction b c = (exclusive_disjunction ? b c). 121 121 122 ndefinition negation ≝122 ndefinition negation_bv ≝ 123 123 λn: Nat. 124 124 λb: BitVector n. … … 131 131 (* ===================================== *) 132 132 133 ndefinition rotate_left ≝134 λ m, n: Nat.133 ndefinition rotate_left_bv ≝ 134 λn, m: Nat. 135 135 λb: BitVector n. 136 136 rotate_left Bool n m b. 137 137 138 ndefinition rotate_right ≝139 λ m, n: Nat.138 ndefinition rotate_right_bv ≝ 139 λn, m: Nat. 140 140 λb: BitVector n. 141 141 rotate_right Bool n m b. 142 142 143 ndefinition shift_left ≝144 λ m, n: Nat.143 ndefinition shift_left_bv ≝ 144 λn, m: Nat. 145 145 λb: BitVector n. 146 146 λc: Bool. 147 147 shift_left Bool n m b c. 148 148 149 ndefinition shift_right ≝150 λ m, n: Nat.149 ndefinition shift_right_bv ≝ 150 λn, m: Nat. 151 151 λb: BitVector n. 152 152 λc: Bool. 
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 
Deliverables/D4.1/Matita/Status.ma
r331 r337 658 658 λs: Status. 659 659 λr: BitVector three. 660 let b ≝ get_index ? r Z ? in661 let c ≝ get_index ? r one ? in662 let d ≝ get_index ? r two ? in660 let b ≝ get_index_bv ? r Z ? in 661 let c ≝ get_index_bv ? r one ? in 662 let d ≝ get_index_bv ? r two ? in 663 663 let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 664 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_indexfour un three ?) in664 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_bv four un two ?) (get_index_bv four un three ?) in 665 665 let offset ≝ 666 666 if conjunction (negation r1) (negation r0) then
Note: See TracChangeset
for help on using the changeset viewer.