(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
include "freescale/table_HC08.ma".
include "freescale/table_HCS08.ma".
include "freescale/table_RS08.ma".
-include "freescale/option.ma".
+include "common/option.ma".
(* ***************************** *)
(* TRADUZIONE ESADECIMALE → INFO *)
match param with
[ nil ⇒ None ?
| cons hd tl ⇒
- match thd4T ???? hd with
+ match thd4T … hd with
[ Byte b ⇒ match borw with
[ Byte borw' ⇒ match eq_b8 borw' b with
[ true ⇒ Some ? hd
ninductive t_byte8 (m:mcu_type) : Type ≝
TByte : byte8 → t_byte8 m.
-nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
- #m; #b1; #b2; #H;
- nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
- nrewrite < H;
- nnormalize;
- napply (refl_eq ??).
-nqed.
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+ [ TByte b1 ⇒ match tb2 with
+ [ TByte b2 ⇒ eq_b8 b1 b2 ]].
(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
ninductive MA_check : instr_mode → Type ≝
(param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
match param with
[ nil ⇒ None ? | cons hd tl ⇒
- match (eq_anyop m o (fst4T ???? hd)) ⊗ (eq_instrmode i (snd4T ???? hd)) with
- [ true ⇒ match thd4T ???? hd with
+ match (eq_anyop m o (fst4T … hd)) ⊗ (eq_im i (snd4T … hd)) with
+ [ true ⇒ match thd4T … hd with
[ Byte isab ⇒
Some ? ([ (TByte m isab) ]@(args_picker m i p))
| Word isaw ⇒