 Timestamp:
 Dec 16, 2011, 2:07:44 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1622 r1623 182 182 [ VEmpty ⇒ False 183 183  VCons n' hd tl ⇒ 184 match eq_a hd a with 185 [ true ⇒ True 186  false ⇒ member_addressing_mode_tag n' tl a 187 ] 184 bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a 188 185 ]. 189 186 … … 192 189 (Q: addressing_mode → T → Prop) 193 190 on v: 194 (∀ n. ∀v. Word11 → member_addressing_mode_tag n v addr11→ T) →195 (∀ n. ∀v. Word → member_addressing_mode_tag n v addr16→ T) →196 (∀ n. ∀v. Byte → member_addressing_mode_tag n v direct→ T) →197 (∀ n. ∀v. Bit → member_addressing_mode_tag n v indirect→ T) →198 (∀ n. ∀v. Bit → member_addressing_mode_tag n v ext_indirect→ T) →199 ( ∀n. ∀v. member_addressing_mode_tag n v acc_a→ T) →200 (∀ n. ∀v. BitVector 3 → member_addressing_mode_tag n v registr→ T) →201 ( ∀n. ∀v. member_addressing_mode_tag n v acc_b→ T) →202 ( ∀n. ∀v. member_addressing_mode_tag n v dptr→ T) →203 (∀ n. ∀v. Byte → member_addressing_mode_tag n v data→ T) →204 (∀ n. ∀v. Word → member_addressing_mode_tag n v data16→ T) →205 ( ∀n. ∀v. member_addressing_mode_tag n v acc_dptr→ T) →206 ( ∀n. ∀v. member_addressing_mode_tag n v acc_pc→ T) →207 ( ∀n. ∀v. member_addressing_mode_tag n v ext_indirect_dptr→ T) →208 ( ∀n. ∀v. member_addressing_mode_tag n v indirect_dptr→ T) →209 ( ∀n. ∀v. member_addressing_mode_tag n v carry→ T) →210 (∀ n. ∀v. Byte → member_addressing_mode_tag n v bit_addr→ T) →211 (∀ n. ∀v. Byte → member_addressing_mode_tag n v n_bit_addr→ T) →212 (∀ n. ∀v. Byte → member_addressing_mode_tag n v relative→ T) → Prop ≝213 match v return λm: nat. λv': Vector addressing_mode_tag m. v ≃ v' → ? with214 [ VEmpty ⇒ λ v_refl.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) → T) → 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 ≝ 210 match v return λm: nat. λv': Vector addressing_mode_tag m. m = n → v ≃ v' → ? with 211 [ VEmpty ⇒ λm_refl. λv_refl. 215 212 λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. 216 213 λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. 217 214 λp_ext_indirect_dptr. λp_indirect_dptr. λp_carry. λp_bit_addr. 218 λp_n_bit_addr. λp_relative. False 219 (* ∀addr:v. Q addr (match addr with *) 220  VCons n' hd tl ⇒ λv_refl. 221 λp_addr11. λp_addr16: ∀n. ∀v. Word → member_addressing_mode_tag n v addr16 → T. 215 λp_n_bit_addr. λp_relative. 216 ∀addr. ∀p: is_in … v addr. 217 Q addr ( 218 match addr return λx:addressing_mode. is_in n v x → T with 219 [ ADDR11 x ⇒ p_addr11 x 220  ADDR16 x ⇒ p_addr16 x 221  DIRECT x ⇒ p_direct x 222  INDIRECT x ⇒ p_indirect x 223  EXT_INDIRECT x ⇒ p_ext_indirect x 224  ACC_A ⇒ p_acc_a 225  REGISTER x ⇒ p_register x 226  ACC_B ⇒ p_acc_b 227  DPTR ⇒ p_dptr 228  DATA x ⇒ p_data x 229  DATA16 x ⇒ p_data16 x 230  ACC_DPTR ⇒ p_acc_dptr 231  ACC_PC ⇒ p_acc_pc 232  EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr 233  INDIRECT_DPTR ⇒ p_indirect_dptr 234  CARRY ⇒ p_carry 235  BIT_ADDR x ⇒ p_bit_addr x 236  N_BIT_ADDR x ⇒ p_n_bit_addr x 237  RELATIVE x ⇒ p_relative x 238 ] p) 239  VCons n' hd tl ⇒ λm_refl. λv_refl. 240 λp_addr11. λp_addr16: (∀w: Word. is_in n v (ADDR16 w) → T). 222 241 λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b. 223 242 λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr. 224 243 λp_indirect_dptr. λp_carry. λp_bit_addr. λp_n_bit_addr. λp_relative. 225 match hd return λa: addressing_mode_tag. a = hd → Prop with 226 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 n v w ?)) → 227 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 228 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 229 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 230 p_relative) 231  addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 n v w ?)) → 232 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 233 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 234 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 235 p_relative) 236  direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct n v w ?)) → 237 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 238 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 239 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 240 p_relative) 241  indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect n v w ?)) → 242 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 243 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 244 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 245 p_relative) 246  ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect n v w ?)) → 247 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 248 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 249 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 250 p_relative) 251  acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a n v ?)) → 252 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 253 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 254 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 255 p_relative) 256  registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register n v w ?)) → 257 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 258 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 259 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 260 p_relative) 261  acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b n v ?)) → 262 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 263 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 264 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 265 p_relative) 266  dptr ⇒ λhd_refl. (Q DPTR (p_dptr n v ?)) → 267 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 268 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 269 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 270 p_relative) 271  data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data n v w ?)) → 272 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 273 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 274 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 275 p_relative) 276  data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 n v w ?)) → 277 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 278 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 279 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 280 p_relative) 281  acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr n v ?)) → 282 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 283 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 284 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 285 p_relative) 286  acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc n v ?)) → 287 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 288 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 289 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 290 p_relative) 291  ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr n v ?)) → 292 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 293 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 294 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 295 p_relative) 296  indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr n v ?)) → 297 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 298 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 299 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 300 p_relative) 301  carry ⇒ λhd_refl. (Q CARRY (p_carry n v ?)) → 302 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 303 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 304 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 305 p_relative) 306  bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr n v w ?)) → 307 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 308 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 309 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 310 p_relative) 311  n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr n v w ?)) → 312 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 313 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 314 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 315 p_relative) 316  relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative n v w ?)) → 317 (subaddressing_mode_elim_type T n' tl Q p_addr11 p_addr16 p_direct p_indirect 318 p_ext_indirect p_acc_a p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 319 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry p_bit_addr p_n_bit_addr 320 p_relative) 244 let tail_call ≝ subaddressing_mode_elim_type T n' tl Q (? p_addr11) 245 (? p_addr16) (? p_direct) (? p_indirect) (? p_ext_indirect) (? p_acc_a) 246 (? p_register) (? p_acc_b) (? p_dptr) (? p_data) (? p_data16) (? p_acc_dptr) 247 (? p_acc_pc) (? p_ext_indirect_dptr) (? p_indirect_dptr) (? p_carry) 248 (? 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 in 257 match hd return λa: addressing_mode_tag. a = hd → ? with 258 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call 259  addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call 260  direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call 261  indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call 262  ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call 263  acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call 264  registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call 265  acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call 266  dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call 267  data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call 268  data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call 269  acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call 270  acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call 271  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_call 273  carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call 274  bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call 275  n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call 276  relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call 321 277 ] (refl … hd) 322 ] (refl_jmeq … v). 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/ 287 qed. 323 288 324 289 lemma subaddressing_mode_elim:
Note: See TracChangeset
for help on using the changeset viewer.