X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Ftranslation%2Ftranslation.ma;h=4cd470862e77c701c76ac0c2e3daaae250e37812;hb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;hp=64bda08ecc6a5947e5c5267bc562069697c0d86a;hpb=0f13d14b63b012e0ea8ce0d0e71bf808fdd444eb;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma
index 64bda08ec..4cd470862 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma
@@ -24,6 +24,7 @@ include "emulator/translation/HC05_translation.ma".
 include "emulator/translation/HC08_translation.ma".
 include "emulator/translation/HCS08_translation.ma".
 include "emulator/translation/RS08_translation.ma".
+include "emulator/translation/IP2022_translation.ma".
 
 (* ******************************************************* *)
 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
@@ -39,6 +40,7 @@ ndefinition MA_check ≝
   | HC08 ⇒ HC08_MA_check
   | HCS08 ⇒ HCS08_MA_check
   | RS08 ⇒ RS08_MA_check
+  | IP2022 ⇒ IP2022_MA_check
   ].
 
 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
@@ -52,6 +54,7 @@ ndefinition args_picker ≝
   | HC08 ⇒ HC08_args_picker
   | HCS08 ⇒ HCS08_args_picker
   | RS08 ⇒ RS08_args_picker
+  | IP2022 ⇒ IP2022_args_picker
   ].
 
 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
@@ -95,37 +98,10 @@ ndefinition compile ≝
   ].
 
 (* detipatore del compilato: (t_byte8 m) → byte8 *)
-nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
+nlet rec source_to_byte8_aux (m:mcu_type) (p2:list byte8) (p1:list (t_byte8 m))  on p1 ≝
  match p1 with
   [ nil ⇒ p2
-  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
+  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_aux m (p2@[b]) tl ]
   ].
 
-nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
- match p1 with
-  [ nil ⇒ p2
-  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
-  ].
-
-nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
- match p1 with
-  [ nil ⇒ p2
-  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
-  ].
-
-nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
- match p1 with
-  [ nil ⇒ p2
-  | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
-  ].
-
-ndefinition source_to_byte8 ≝
-λm:mcu_type.
- match m
-  return λm:mcu_type.list (t_byte8 m) → list byte8
- with
-  [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
-  | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
-  | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
-  | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []
-  ].
+ndefinition source_to_byte8 ≝ λm:mcu_type.source_to_byte8_aux m [].