Changeset 875


Ignore:
Timestamp:
Jun 3, 2011, 11:21:12 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r874 r875  
    442442  λi, j: instruction.
    443443    true.
     444   
     445let rec list_addressing_mode_tags_elim_prop
     446  (n: nat) (l: Vector addressing_mode_tag (S n))
     447  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     448  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     449  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     450  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     451  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     452  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     453  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     454  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     455  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     456  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     457  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     458  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     459  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     460  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     461  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     462  (if is_in ? l direct then ∀x. P (DIRECT x) else True) →
     463  (if is_in ? l relative then ∀x. P (RELATIVE x) else True) →
     464  (if is_in ? l addr11 then ∀x. P (ADDR11 x) else True) →
     465  (if is_in ? l addr16 then ∀x. P (ADDR16 x) else True) →
     466  (P: addressing_mode → Prop) (x: l)
     467   on l : P x ≝
     468  match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
     469   (l → bool) → bool ] with
     470  [ VEmpty      ⇒  true 
     471  | VCons len hd tl ⇒ λP.
     472    let process_hd ≝
     473      match hd return λhd. ∀P: hd:::tl → bool. bool with
     474      [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
     475      | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
     476      | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
     477      | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
     478      | acc_a ⇒ λP.P ACC_A
     479      | acc_b ⇒ λP.P ACC_B
     480      | dptr ⇒ λP.P DPTR
     481      | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
     482      | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
     483      | acc_dptr ⇒ λP.P ACC_DPTR
     484      | acc_pc ⇒ λP.P ACC_PC
     485      | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
     486      | indirect_dptr ⇒ λP.P INDIRECT_DPTR
     487      | carry ⇒ λP.P CARRY
     488      | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
     489      | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
     490      | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
     491      | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
     492      | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
     493      ]
     494    in
     495      andb (process_hd P)
     496       (match len return λx. x = len → bool with
     497         [ O ⇒ λprf. true
     498         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
     499  ].
     500  try %
     501  [ 2: cases (sym_eq ??? prf); @tl
     502  | generalize in match H; generalize in match tl; cases prf;
     503    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
     504    #tl
     505    normalize in ⊢ (∀_: %. ?)
     506    # H
     507    whd
     508    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
     509    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
     510qed.
     511
    444512(*
    445513lemma test:
     
    461529      let 〈instr_pc, ticks〉 ≝ fetched in
    462530        eq_instruction (\fst instr_pc)) i = true.
    463  [ @ (instruction_elim_complete )
     531 [ #i cases i #arg try #arg2 whd in ⊢ (??%?)
     532   [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?)
     533       cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
     534       whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?)
     535 
     536   [2: #addr whd in ⊢ (??%?)
     537 
     538   @ (instruction_elim_complete )
    464539 | @ zero
    465540 ]
Note: See TracChangeset for help on using the changeset viewer.