- Timestamp:
- Dec 16, 2011, 3:44:02 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r1623 r1624 176 176 qed. 177 177 178 lemma is_in_tail_to_is_in_cons_hd_tl: 179 ∀n: nat. 180 ∀the_vect: Vector addressing_mode_tag n. 181 ∀h: addressing_mode_tag. 182 ∀element: addressing_mode. 183 is_in n the_vect element → is_in (S n) (h:::the_vect) element. 184 #n #the_vect #h #element #assm 185 normalize cases (is_a h element) normalize nodelta 186 // 187 qed. 188 178 189 let rec member_addressing_mode_tag 179 190 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) … … 189 200 (Q: addressing_mode → T → Prop) 190 201 on v: 191 (∀w: Word11. is_in n v (ADDR11 w)→ T) →192 (∀w: Word. is_in n v (ADDR16 w)→ T) →193 (∀w: Byte. is_in n v (DIRECT w)→ T) →194 (∀w: Bit. is_in n v (INDIRECT w)→ T) →195 (∀w: Bit. is_in n v (EXT_INDIRECT w)→ T) →196 ( is_in n v ACC_A → T) →197 (∀w: BitVector 3. is_in n v (REGISTER w) 198 ( is_in n v ACC_B → T) →199 ( is_in n v DPTR → T) →200 (∀w: Byte. is_in n v (DATA w)→ T) →201 (∀w: Word. is_in n v (DATA16 w)→ T) →202 ( is_in n v ACC_DPTR → T) →203 ( is_in n v ACC_PC → T) →204 ( is_in n v EXT_INDIRECT_DPTR → T) →205 ( is_in n v INDIRECT_DPTR → T) →206 ( is_in n v CARRY→ T) →207 (∀w: Byte. is_in n v (BIT_ADDR w)→ T) →208 (∀w: Byte. is_in n v (N_BIT_ADDR w)→ T) →209 (∀w: Byte. is_in n v (RELATIVE w)→ T) → Prop ≝202 (∀w: Word11. is_in n v (ADDR11 w) → T) → 203 (∀w: Word. is_in n v (ADDR16 w) → T) → 204 (∀w: Byte. is_in n v (DIRECT w) → T) → 205 (∀w: Bit. is_in n v (INDIRECT w) → T) → 206 (∀w: Bit. is_in n v (EXT_INDIRECT w) → T) → 207 ( is_in n v ACC_A → T) → 208 (∀w: BitVector 3. is_in n v (REGISTER w) → T) → 209 ( is_in n v ACC_B → T) → 210 ( is_in n v DPTR → T) → 211 (∀w: Byte. is_in n v (DATA w) → T) → 212 (∀w: Word. is_in n v (DATA16 w) → T) → 213 ( is_in n v ACC_DPTR → T) → 214 ( is_in n v ACC_PC → T) → 215 ( is_in n v EXT_INDIRECT_DPTR → T) → 216 ( is_in n v INDIRECT_DPTR → T) → 217 ( is_in n v CARRY → T) → 218 (∀w: Byte. is_in n v (BIT_ADDR w) → T) → 219 (∀w: Byte. is_in n v (N_BIT_ADDR w) → T) → 220 (∀w: Byte. is_in n v (RELATIVE w) → T) → Prop ≝ 210 221 match v return λm: nat. λv': Vector addressing_mode_tag m. m = n → v ≃ v' → ? with 211 222 [ VEmpty ⇒ λm_refl. λv_refl. … … 216 227 ∀addr. ∀p: is_in … v addr. 217 228 Q addr ( 218 match addr return λx: addressing_mode. is_in nv x → T with219 [ ADDR11 x ⇒ p_addr11 x220 | ADDR16 x ⇒ p_addr16 x221 | DIRECT x ⇒ p_direct x222 | INDIRECT x ⇒ p_indirect x223 | EXT_INDIRECT x ⇒ p_ext_indirect x224 | ACC_A ⇒ p_acc_a225 | REGISTER x ⇒ p_register x226 | ACC_B ⇒ p_acc_b227 | DPTR ⇒ p_dptr228 | DATA x ⇒ p_data x229 | DATA16 x ⇒ p_data16 x230 | ACC_DPTR ⇒ p_acc_dptr231 | ACC_PC ⇒ p_acc_pc229 match addr return λx: addressing_mode. is_in … v x → T with 230 [ ADDR11 x ⇒ p_addr11 x 231 | ADDR16 x ⇒ p_addr16 x 232 | DIRECT x ⇒ p_direct x 233 | INDIRECT x ⇒ p_indirect x 234 | EXT_INDIRECT x ⇒ p_ext_indirect x 235 | ACC_A ⇒ p_acc_a 236 | REGISTER x ⇒ p_register x 237 | ACC_B ⇒ p_acc_b 238 | DPTR ⇒ p_dptr 239 | DATA x ⇒ p_data x 240 | DATA16 x ⇒ p_data16 x 241 | ACC_DPTR ⇒ p_acc_dptr 242 | ACC_PC ⇒ p_acc_pc 232 243 | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr 233 | INDIRECT_DPTR ⇒ p_indirect_dptr234 | CARRY ⇒ p_carry235 | BIT_ADDR x ⇒ p_bit_addr x236 | N_BIT_ADDR x ⇒ p_n_bit_addr x237 | RELATIVE x ⇒ p_relative x244 | INDIRECT_DPTR ⇒ p_indirect_dptr 245 | CARRY ⇒ p_carry 246 | BIT_ADDR x ⇒ p_bit_addr x 247 | N_BIT_ADDR x ⇒ p_n_bit_addr x 248 | RELATIVE x ⇒ p_relative x 238 249 ] p) 239 250 | VCons n' hd tl ⇒ λm_refl. λv_refl. … … 247 258 (? p_acc_pc) (? p_ext_indirect_dptr) (? p_indirect_dptr) (? p_carry) 248 259 (? p_bit_addr) (? p_n_bit_addr) (? p_relative) 249 (*250 (subaddressing_mode_elim_type T n' tl Q (λw. λH. p_addr11 w ?) (λw. λH. p_addr16 w ?)251 (λw. λH. p_direct w ?) (λw. λH. p_indirect w ?) (λw. λH. p_ext_indirect w ?)252 (λH. p_acc_a ?) (λw. λH. p_register w ?) (λH. p_acc_b ?) (λH. p_dptr ?)253 (λw. λH. p_data w ?) (λw. λH. p_data16 w ?) (λH. p_acc_dptr ?) (λH. p_acc_pc ?)254 (λH. p_ext_indirect_dptr ?) (λH. p_indirect_dptr ?) (λH. p_carry ?) (λw. λH. p_bit_addr w ?)255 (λw. λH. p_n_bit_addr w ?) (λw. λH. p_relative w ?))*)256 260 in 257 261 match hd return λa: addressing_mode_tag. a = hd → ? with 258 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call259 | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call260 | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call261 | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call262 | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call263 | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call264 | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call265 | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call266 | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call267 | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call268 | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call269 | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call270 | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call262 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call 263 | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call 264 | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call 265 | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call 266 | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call 267 | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call 268 | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call 269 | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call 270 | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call 271 | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call 272 | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call 273 | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call 274 | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call 271 275 | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call 272 | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call273 | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call274 | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call275 | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call276 | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call276 | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call 277 | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call 278 | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call 279 | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call 280 | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call 277 281 ] (refl … hd) 278 ] (refl … n) (refl_jmeq … v). 279 try (#w1 try #w2) 280 destruct 281 [ 38: 282 normalize in p_relative; 283 generalize in match p_relative; 284 destruct 285 cases (is_in (S n') (hd:::tl) (RELATIVE B)) 286 destruct whd /2 by or_introl, or_intror, I/ 282 ] (refl … n) (refl_jmeq … v). 283 try (#_ #w1 try #w2) 284 [20: 285 destruct @p_addr11 try assumption 286 @is_in_tail_to_is_in_cons_hd_tl assumption 287 |21: 288 destruct @p_addr16 try assumption 289 @is_in_tail_to_is_in_cons_hd_tl assumption 290 |22: 291 destruct @p_direct try assumption 292 @is_in_tail_to_is_in_cons_hd_tl assumption 293 |23: 294 destruct @p_indirect try assumption 295 @is_in_tail_to_is_in_cons_hd_tl assumption 296 |24: 297 destruct @p_ext_indirect try assumption 298 @is_in_tail_to_is_in_cons_hd_tl assumption 299 |25: 300 destruct @p_acc_a try assumption 301 @is_in_tail_to_is_in_cons_hd_tl assumption 302 |26: 303 destruct @p_register try assumption 304 @is_in_tail_to_is_in_cons_hd_tl assumption 305 |27: 306 destruct @p_acc_b try assumption 307 @is_in_tail_to_is_in_cons_hd_tl assumption 308 |28: 309 destruct @p_dptr try assumption 310 @is_in_tail_to_is_in_cons_hd_tl assumption 311 |29: 312 destruct @p_data try assumption 313 @is_in_tail_to_is_in_cons_hd_tl assumption 314 |30: 315 destruct @p_data16 try assumption 316 @is_in_tail_to_is_in_cons_hd_tl assumption 317 |31: 318 destruct @p_acc_dptr try assumption 319 @is_in_tail_to_is_in_cons_hd_tl assumption 320 |32: 321 destruct @p_acc_pc try assumption 322 @is_in_tail_to_is_in_cons_hd_tl assumption 323 |33: 324 destruct @p_ext_indirect_dptr try assumption 325 @is_in_tail_to_is_in_cons_hd_tl assumption 326 |34: 327 destruct @p_indirect_dptr try assumption 328 @is_in_tail_to_is_in_cons_hd_tl assumption 329 |35: 330 destruct @p_carry try assumption 331 @is_in_tail_to_is_in_cons_hd_tl assumption 332 |36: 333 destruct @p_bit_addr try assumption 334 @is_in_tail_to_is_in_cons_hd_tl assumption 335 |37: 336 destruct @p_n_bit_addr try assumption 337 @is_in_tail_to_is_in_cons_hd_tl assumption 338 |38: 339 destruct @p_relative try assumption 340 @is_in_tail_to_is_in_cons_hd_tl assumption 341 |*: 342 -tail_call destruct @I 343 ] 287 344 qed. 288 345 346 axiom subaddressing_mode_elim: 347 ∀T: Type[2]. 348 ∀n: nat. 349 ∀v: Vector addressing_mode_tag n. 350 ∀Q: addressing_mode → T → Prop. 351 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 352 subaddressing_mode_elim_type T n v Q P1 P2 P3 P4 P5 P6 P7 353 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19. 354 355 (* 289 356 lemma subaddressing_mode_elim: 290 357 ∀T:Type[2]. … … 321 388 * try #x1 try #x2 try #x3 try #x4 322 389 try (@⊥ assumption) normalize @x4 323 qed. 390 qed. *) 324 391 325 392 include alias "arithmetics/nat.ma". … … 387 454 cases FETCH normalize nodelta 388 455 cases instr normalize nodelta 389 @subaddressing_mode_elim #new_addr 456 @(subaddressing_mode_elim Prop 1 [[ addr11 ]]) try // 457 [2: normalize // #new_addr 390 458 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 391 459 cases (split … 3 8 new_addr) #thr #eig normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.