Changeset 1623 for src/ASM


Ignore:
Timestamp:
Dec 16, 2011, 2:07:44 PM (8 years ago)
Author:
mulligan
Message:

strange matita issue

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1622 r1623  
    182182  [ VEmpty ⇒ False
    183183  | 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
    188185  ].
    189186 
     
    192189    (Q: addressing_mode → T → Prop)
    193190      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' → ? with
    214   [ 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.
    215212    λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a.
    216213    λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc.
    217214    λ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).
    222241    λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b.
    223242    λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr.
    224243    λ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
    321277    ] (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/
     287qed.
    323288
    324289lemma subaddressing_mode_elim:
Note: See TracChangeset for help on using the changeset viewer.