Changeset 2032 for src/ASM/ASM.ma


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r1882 r2032  
    7575      ].
    7676
     77lemma eq_a_to_eq:
     78  ∀a,b.
     79    eq_a a b = true → a = b.
     80 #a #b
     81 cases a cases b
     82 #K
     83 try cases (eq_true_false K)
     84 %
     85qed.
     86
     87lemma eq_a_reflexive:
     88  ∀a. eq_a a a = true.
     89  #a cases a %
     90qed.
     91
     92let rec member_addressing_mode_tag
     93  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
     94    on v: Prop ≝
     95  match v with
     96  [ VEmpty ⇒ False
     97  | VCons n' hd tl ⇒
     98      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
     99  ].
     100
     101lemma mem_decidable:
     102  ∀n: nat.
     103  ∀v: Vector addressing_mode_tag n.
     104  ∀element: addressing_mode_tag.
     105    mem … eq_a n v element = true ∨
     106      mem … eq_a … v element = false.
     107  #n #v #element //
     108qed.
     109
     110lemma eq_a_elim:
     111  ∀tag.
     112  ∀hd.
     113  ∀P: bool → Prop.
     114    (tag = hd → P (true)) →
     115      (tag ≠ hd → P (false)) →
     116        P (eq_a tag hd).
     117  #tag #hd #P
     118  cases tag
     119  cases hd
     120  #true_hyp #false_hyp
     121  try @false_hyp
     122  try @true_hyp
     123  try %
     124  #absurd destruct(absurd)
     125qed.
     126
    77127(* to avoid expansion... *)
    78128let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
     
    99149   ].
    100150
     151lemma is_a_decidable:
     152  ∀hd.
     153  ∀element.
     154    is_a hd element = true ∨ is_a hd element = false.
     155  #hd #element //
     156qed.
    101157
    102158let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
     
    106162     is_a he A ∨ is_in ? tl A ].
    107163
     164lemma is_a_to_mem_to_is_in:
     165 ∀he,a,m,q.
     166   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
     167 #he #a #m #q
     168 elim q
     169 [1:
     170   #_ #K assumption
     171 |2:
     172   #m' #t #q' #II #H1 #H2
     173   normalize
     174   change with (orb ??) in H2:(??%?);
     175   cases (inclusive_disjunction_true … H2)
     176   [1:
     177     #K
     178     <(eq_a_to_eq … K) >H1 %
     179   |2:
     180     #K
     181     >II
     182     try assumption
     183     cases (is_a t a)
     184     normalize
     185     %
     186   ]
     187 ]
     188qed.
     189
     190lemma is_a_true_to_is_in:
     191  ∀n: nat.
     192  ∀x: addressing_mode.
     193  ∀tag: addressing_mode_tag.
     194  ∀supervector: Vector addressing_mode_tag n.
     195  mem addressing_mode_tag eq_a n supervector tag →
     196    is_a tag x = true →
     197      is_in … supervector x.
     198  #n #x #tag #supervector
     199  elim supervector
     200  [1:
     201    #absurd cases absurd
     202  |2:
     203    #n' #hd #tl #inductive_hypothesis
     204    whd in match (mem … eq_a (S n') (hd:::tl) tag);
     205    @eq_a_elim normalize nodelta
     206    [1:
     207      #tag_hd_eq #irrelevant
     208      whd in match (is_in (S n') (hd:::tl) x);
     209      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
     210      @I
     211    |2:
     212      #tag_hd_neq
     213      whd in match (is_in (S n') (hd:::tl) x);
     214      change with (
     215        mem … eq_a n' tl tag)
     216          in match (fold_right … n' ? false tl);
     217      #mem_hyp #is_a_hyp
     218      cases(is_a hd x)
     219      [1:
     220        normalize nodelta //
     221      |2:
     222        normalize nodelta
     223        @inductive_hypothesis assumption
     224      ]
     225    ]
     226  ]
     227qed.
     228
    108229record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
    109230{
     
    119240  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
    120241 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
     242
     243lemma is_in_subvector_is_in_supervector:
     244  ∀m, n: nat.
     245  ∀subvector: Vector addressing_mode_tag m.
     246  ∀supervector: Vector addressing_mode_tag n.
     247  ∀element: addressing_mode.
     248    subvector_with … eq_a subvector supervector →
     249      is_in m subvector element → is_in n supervector element.
     250  #m #n #subvector #supervector #element
     251  elim subvector
     252  [1:
     253    #subvector_with_proof #is_in_proof
     254    cases is_in_proof
     255  |2:
     256    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
     257    whd in match (is_in … (hd':::tl') element);
     258    cases (is_a_decidable hd' element)
     259    [1:
     260      #is_a_true >is_a_true
     261      #irrelevant
     262      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
     263      @(is_a_true_to_is_in … is_a_true)
     264      lapply(subvector_with_proof)
     265      cases(mem … eq_a n supervector hd') //
     266    |2:
     267      #is_a_false >is_a_false normalize nodelta
     268      #assm
     269      @inductive_hypothesis
     270      [1:
     271        generalize in match subvector_with_proof;
     272        whd in match (subvector_with … eq_a (hd':::tl') supervector);
     273        cases(mem_decidable n supervector hd')
     274        [1:
     275          #mem_true >mem_true normalize nodelta
     276          #assm assumption
     277        |2:
     278          #mem_false >mem_false #absurd
     279          cases absurd
     280        ]
     281      |2:
     282        assumption
     283      ]
     284    ]
     285  ]
     286qed.
     287
     288
     289let rec subaddressing_mode_elim_type
     290  (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v)
     291    (Q: fixed_v → Prop)
     292     (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
     293       on v: Prop ≝
     294  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
     295  [ VEmpty         ⇒ λm_refl. λv_refl. Q origaddr
     296  | VCons n' hd tl ⇒ λm_refl. λv_refl.
     297    let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ?
     298    in
     299    match hd return λa: addressing_mode_tag. a = hd → ? with
     300    [ addr11            ⇒ λhd_refl. (∀w: Word11.      Q (ADDR11 w)) → tail_call
     301    | addr16            ⇒ λhd_refl. (∀w: Word.        Q (ADDR16 w)) → tail_call
     302    | direct            ⇒ λhd_refl. (∀w: Byte.        Q (DIRECT w)) → tail_call
     303    | indirect          ⇒ λhd_refl. (∀w: Bit.         Q (INDIRECT w)) → tail_call
     304    | ext_indirect      ⇒ λhd_refl. (∀w: Bit.         Q (EXT_INDIRECT w)) → tail_call
     305    | acc_a             ⇒ λhd_refl.                  Q ACC_A → tail_call
     306    | registr           ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call
     307    | acc_b             ⇒ λhd_refl.                  Q ACC_B → tail_call
     308    | dptr              ⇒ λhd_refl.                  Q DPTR → tail_call
     309    | data              ⇒ λhd_refl. (∀w: Byte.        Q (DATA w))  → tail_call
     310    | data16            ⇒ λhd_refl. (∀w: Word.        Q (DATA16 w)) → tail_call
     311    | acc_dptr          ⇒ λhd_refl.                  Q ACC_DPTR → tail_call
     312    | acc_pc            ⇒ λhd_refl.                  Q ACC_PC → tail_call
     313    | ext_indirect_dptr ⇒ λhd_refl.                  Q EXT_INDIRECT_DPTR → tail_call
     314    | indirect_dptr     ⇒ λhd_refl.                  Q INDIRECT_DPTR → tail_call
     315    | carry             ⇒ λhd_refl.                  Q CARRY → tail_call
     316    | bit_addr          ⇒ λhd_refl. (∀w: Byte.        Q (BIT_ADDR w)) → tail_call
     317    | n_bit_addr        ⇒ λhd_refl. (∀w: Byte.        Q (N_BIT_ADDR w)) → tail_call
     318    | relative          ⇒ λhd_refl. (∀w: Byte.        Q (RELATIVE w)) → tail_call
     319    ] (refl … hd)
     320  ] (refl … n) (refl_jmeq … v).
     321  [20:
     322    generalize in match proof; destruct
     323    whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
     324    cases (mem … eq_a ? fixed_v hd) normalize nodelta
     325    [1:
     326      whd in match (subvector_with … eq_a tl fixed_v);
     327      #assm assumption
     328    |2:
     329      normalize in ⊢ (% → ?);
     330      #absurd cases absurd
     331    ]
     332  ]
     333  @(is_in_subvector_is_in_supervector … proof)
     334  destruct @I
     335qed.
     336
     337lemma subaddressing_mode_elim0:
     338  ∀n: nat.
     339  ∀v: Vector addressing_mode_tag (S n).
     340  ∀addr: v.
     341  ∀Q: v → Prop.
     342  ∀m,w,H.
     343  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
     344   subaddressing_mode_elim_type n v addr Q m w H.
     345 #n #v #addr #Q #m #w elim w
     346 [ /2/
     347 | #n' #hd #tl #IH cases hd #H
     348   #INV whd #PO @IH #xaddr cases xaddr *
     349   try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
     350   @ALREADYSEEN ]
     351qed.
     352
     353lemma subaddressing_mode_elim:
     354  ∀n: nat.
     355  ∀v: Vector addressing_mode_tag (S n).
     356  ∀addr: v.
     357  ∀Q: v → Prop.
     358   subaddressing_mode_elim_type n v addr Q (S n) v ?.
     359[ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
     360| @subvector_with_refl @eq_a_reflexive
     361]
     362qed.
    121363 
    122364inductive preinstruction (A: Type[0]) : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.