X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fopcodes%2FIP2022_instr_mode.ma;h=1998586e90cac1162d7adfd1cce4109ac97230a2;hb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;hp=45548e7b1250e6b79cc35cd7d0b35bb997b513f0;hpb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma
index 45548e7b1..1998586e9 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode.ma
@@ -30,6 +30,10 @@ include "num/word16.ma".
 ninductive IP2022_instr_mode: Type ≝
   (* nessun operando : formato xxxxxxxx xxxxxxxx *)
   MODE_INH  : IP2022_instr_mode
+  (* operando implicito [ADDR] : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDR : IP2022_instr_mode
+  (* operando implicito [ADDR]/ADDR+=2 : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDRpp : IP2022_instr_mode
 
   (* #lit3 → / : formato xxxxxxxx xxxxxkkk *)
 | MODE_IMM3 : oct → IP2022_instr_mode
@@ -57,6 +61,8 @@ ndefinition eq_IP2022_im ≝
 λi1,i2:IP2022_instr_mode.
  match i1 with
   [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+  | MODE_INHADDR ⇒ match i2 with [ MODE_INHADDR ⇒ true | _ ⇒ false ]
+  | MODE_INHADDRpp ⇒ match i2 with [ MODE_INHADDRpp ⇒ true | _ ⇒ false ]
   | MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
   | MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ]
   | MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
@@ -68,9 +74,10 @@ ndefinition eq_IP2022_im ≝
   | MODE_FR1n o1 ⇒ match i2 with [ MODE_FR1n o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
   ].
 
-(* iteratore sulle modalita' *)
 ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool.
   P MODE_INH
+⊗ P MODE_INHADDR
+⊗ P MODE_INHADDRpp
 ⊗ forall_oct (λo.P (MODE_IMM3 o))
 ⊗ P MODE_IMM8
 ⊗ forall_bit (λt.P (MODE_IMM13 t))