(* ********************************************************************** *)
(* 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/aux_bases.ma".
-include "freescale/word16.ma".
-include "freescale/theory.ma".
+include "num/word16.ma".
(* ********************************************** *)
(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
| MODE_SRT : bitrigesim → instr_mode
.
-ndefinition eq_instrmode ≝
+ndefinition eq_im ≝
λi1,i2:instr_mode.
match i1 with
[ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
| MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
| MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
| MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]
- | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bitrig t1 t2 | _ ⇒ false ]
+ | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
].
(* enumerazione delle istruzioni di tutte le ALU *)