(* ********************************************************************** *)
(* 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
nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
nrewrite < H;
nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
nqed.
(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
(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 ⇒