Changeset 367 for Deliverables


Ignore:
Timestamp:
Dec 2, 2010, 5:13:22 PM (9 years ago)
Author:
mulligan
Message:

Added decidable equality for addressing_mode_tags.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r357 r367  
    4444| addr11: addressing_mode_tag
    4545| addr16: addressing_mode_tag.
     46
     47ndefinition eq_a ≝
     48  λa, b: addressing_mode_tag.
     49    match a with
     50      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
     51      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
     52      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
     53      | register ⇒ match b with [ register ⇒ true | _ ⇒ false ]
     54      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
     55      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
     56      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
     57      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
     58      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
     59      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
     60      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
     61      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
     62      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
     63      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
     64      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
     65      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
     66      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
     67      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
     68      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
     69      ].
    4670
    4771(* to avoid expansion... *)
  • Deliverables/D4.1/Matita/Interpret.ma

    r364 r367  
    88naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool.
    99   
    10 nlemma execute_1_technical:
     10naxiom execute_1_technical:
    1111  ∀n,m: Nat.
    1212  ∀v: Vector addressing_mode_tag (S n).
     
    1616    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    1717    bool_to_Prop (is_in ? q a).
    18   #n m v q a.
    19   ncases a.
    20   nnormalize.
    2118   
    2219ndefinition execute_1: Status → Status ≝
     
    512509          nnormalize
    513510          //);
    514     ##|
     511    ##| napply (execute_1_technical ? ? [[ acc_a ]]
     512                                        [[ direct; indirect; register;
     513                                           acc_a; acc_b; data; acc_dptr;
     514                                           acc_pc; ext_indirect;
     515                                           ext_indirect_dptr ]] ACC_A).
    515516nqed.
    516517
Note: See TracChangeset for help on using the changeset viewer.