freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / opcodes / opcode.ma

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma
index a1b696d839a9577d0f7bab26b387fe2e1aa9a703..4c3f8c849e7747eff0132f77b7a37781bc80d17b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode.ma
@@ -27,6 +27,8 @@ include "emulator/opcodes/HC08_instr_mode.ma".
 include "emulator/opcodes/HCS08_opcode.ma".
 include "emulator/opcodes/RS08_opcode.ma".
 include "emulator/opcodes/RS08_instr_mode.ma".
+include "emulator/opcodes/IP2022_opcode.ma".
+include "emulator/opcodes/IP2022_instr_mode.ma".
 include "emulator/opcodes/byte_or_word.ma".
 include "common/list.ma".
 
@@ -36,10 +38,11 @@ include "common/list.ma".
 
 (* enumerazione delle ALU *)
 ninductive mcu_type: Type ≝
-  HC05  : mcu_type
-| HC08  : mcu_type
-| HCS08 : mcu_type
-| RS08  : mcu_type.
+  HC05   : mcu_type
+| HC08   : mcu_type
+| HCS08  : mcu_type
+| RS08   : mcu_type
+| IP2022 : mcu_type.
 
 ndefinition eq_mcutype ≝
 λm1,m2:mcu_type.
@@ -48,6 +51,7 @@ ndefinition eq_mcutype ≝
   | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
   | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
   | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
+  | IP2022 ⇒ match m2 with [ IP2022 ⇒ true | _ ⇒ false ]
   ].
 
 ndefinition aux_op_type ≝
@@ -56,6 +60,7 @@ ndefinition aux_op_type ≝
  | HC08 ⇒ HC08_opcode
  | HCS08 ⇒ HCS08_opcode
  | RS08 ⇒ RS08_opcode
+ | IP2022 ⇒ IP2022_opcode
  ].
 
 ndefinition aux_im_type ≝
@@ -64,6 +69,7 @@ ndefinition aux_im_type ≝
  | HC08 ⇒ HC08_instr_mode
  | HCS08 ⇒ HC08_instr_mode
  | RS08 ⇒ RS08_instr_mode
+ | IP2022 ⇒ IP2022_instr_mode
  ].
 
 ndefinition eq_op ≝
@@ -75,6 +81,7 @@ ndefinition eq_op ≝
   | HC08 ⇒ eq_HC08_op
   | HCS08 ⇒ eq_HCS08_op
   | RS08 ⇒ eq_RS08_op
+  | IP2022 ⇒ eq_IP2022_op
   ].
 
 ndefinition eq_im ≝
@@ -86,6 +93,7 @@ ndefinition eq_im ≝
   | HC08 ⇒ eq_HC08_im
   | HCS08 ⇒ eq_HC08_im
   | RS08 ⇒ eq_RS08_im
+  | IP2022 ⇒ eq_IP2022_im
   ].
 
 ndefinition forall_op ≝
@@ -97,6 +105,7 @@ ndefinition forall_op ≝
   | HC08 ⇒ forall_HC08_op
   | HCS08 ⇒ forall_HCS08_op
   | RS08 ⇒ forall_RS08_op
+  | IP2022 ⇒ forall_IP2022_op
   ].
 
 ndefinition forall_im ≝
@@ -108,6 +117,7 @@ ndefinition forall_im ≝
   | HC08 ⇒ forall_HC08_im
   | HCS08 ⇒ forall_HC08_im
   | RS08 ⇒ forall_RS08_im
+  | IP2022 ⇒ forall_IP2022_im
   ].
 
 (* ********************************************* *)
@@ -129,15 +139,15 @@ nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_typ
    ]
   ].
 
-(* su tutta la lista quante volte compare la word (0x9E+byte) *)
-nlet rec get_word_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
+(* su tutta la lista quante volte compare la word *)
+nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒ match thd4T … hd with
-   [ Byte _ ⇒ get_word_count m b c tl
-   | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
-    [ true ⇒ get_word_count m b (succ_w16 c) tl
-    | false ⇒ get_word_count m b c tl
+   [ Byte _ ⇒ get_word_count m w c tl
+   | Word w' ⇒ match eq_w16 w w' with
+    [ true ⇒ get_word_count m w (succ_w16 c) tl
+    | false ⇒ get_word_count m w c tl
     ]
    ]
   ].
@@ -172,26 +182,6 @@ nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
    ]
   ].
 
-(* o e' non implementato? *)
-nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_op_type m) (l:list (aux_op_type m)) on l ≝
- match l with
-  [ nil ⇒ false
-  | cons hd tl ⇒ match eq_op m o hd with
-   [ true ⇒ true
-   | false ⇒ test_not_impl_pseudo m o tl
-   ]
-  ].
-
-(* i e' non implementato? *)
-nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
- match l with
-  [ nil ⇒ false
-  | cons hd tl ⇒ match eq_im m i hd with
-   [ true ⇒ true
-   | false ⇒ test_not_impl_mode m i tl
-   ]
-  ].
-
 (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
 nlet rec get_OpIm_count (m:mcu_type) (o:aux_op_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
  match l with