Changeset 1624 for src/ASM


Ignore:
Timestamp:
Dec 16, 2011, 3:44:02 PM (9 years ago)
Author:
mulligan
Message:

commit for claudio

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r1623 r1624  
    176176qed.
    177177
     178lemma 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  //
     187qed.
     188
    178189let rec member_addressing_mode_tag
    179190  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
    … …  
    189200    (Q: addressing_mode → T → Prop)
    190201      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)           → 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 ≝
     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 ≝
    210221  match v return λm: nat. λv': Vector addressing_mode_tag m. m = n → v ≃ v' → ? with
    211222  [ VEmpty         ⇒ λm_refl. λv_refl.
    … …  
    216227      ∀addr. ∀p: is_in … v addr.
    217228        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
     229        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
    232243        | 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
     244        | 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
    238249        ] p)
    239250  | VCons n' hd tl ⇒ λm_refl. λv_refl.
    … …  
    247258          (? p_acc_pc) (? p_ext_indirect_dptr) (? p_indirect_dptr) (? p_carry)
    248259            (? 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 ?))*)
    256260    in
    257261    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
     262    [ 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
    271275    | 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
     276    | 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
    277281    ] (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 ]
    287344qed.
    288345
     346axiom 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(*
    289356lemma subaddressing_mode_elim:
    290357  ∀T:Type[2].
    … …  
    321388  * try #x1 try #x2 try #x3 try #x4
    322389  try (@⊥ assumption) normalize @x4
    323 qed.
     390qed. *)
    324391
    325392include alias "arithmetics/nat.ma".
    … …  
    387454    cases FETCH normalize nodelta
    388455    cases instr normalize nodelta
    389     @subaddressing_mode_elim #new_addr
     456    @(subaddressing_mode_elim Prop 1 [[ addr11 ]]) try //
     457    [2: normalize // #new_addr
    390458    cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta
    391459    cases (split … 3 8 new_addr) #thr #eig normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.