X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Ftranslation.ma;h=0463cff55a25cf15797f17560fa496b5d7183495;hb=c78a913e4e45c1128b59ca8be9d53fc0c36fc9e0;hp=dae2b5fd511a6b11ed22e1fe060f9fc417c00c41;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/translation.ma b/helm/software/matita/library/freescale/translation.ma
index dae2b5fd5..0463cff55 100644
--- a/helm/software/matita/library/freescale/translation.ma
+++ b/helm/software/matita/library/freescale/translation.ma
@@ -24,15 +24,9 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/translation/".
-
-(*include "/media/VIRTUOSO/freescale/table_HC05.ma".*)
 include "freescale/table_HC05.ma".
-(*include "/media/VIRTUOSO/freescale/table_HC08.ma".*)
 include "freescale/table_HC08.ma".
-(*include "/media/VIRTUOSO/freescale/table_HCS08.ma".*)
 include "freescale/table_HCS08.ma".
-(*include "/media/VIRTUOSO/freescale/table_RS08.ma".*)
 include "freescale/table_RS08.ma".
 
 (* ***************************** *)
@@ -87,7 +81,11 @@ inductive MA_check : instr_mode → Type ≝
 | maINHA             : MA_check MODE_INHA
 | maINHX             : MA_check MODE_INHX
 | maINHH             : MA_check MODE_INHH
+| maINHX0ADD         : MA_check MODE_INHX0ADD
+| maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
+| maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
 | maIMM1             : byte8  → MA_check MODE_IMM1
+| maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
 | maIMM2             : word16 → MA_check MODE_IMM2
 | maDIR1             : byte8  → MA_check MODE_DIR1
 | maDIR2             : word16 → MA_check MODE_DIR2
@@ -131,8 +129,13 @@ definition args_picker ≝
   | maINHA   ⇒ nil ? 
   | maINHX   ⇒ nil ? 
   | maINHH   ⇒ nil ?
+  (* inherent address: legale se nessun operando/1 byte/1 word *)
+  | maINHX0ADD ⇒ nil ?
+  | maINHX1ADD b ⇒ [ TByte m b ]
+  | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]    
   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
   | maIMM1 b ⇒ [ TByte m b ]
+  | maIMM1EXT b ⇒ [ TByte m b ]
   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
   | maDIR1 b ⇒ [ TByte m b ]
   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]