X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Ftranslation%2Ftranslation.ma;h=801c420c20e31e7cf50a4a49bc52f9bf02824d8c;hb=b31c093c364e76cc6c4657008f3f259955311911;hp=4cd470862e77c701c76ac0c2e3daaae250e37812;hpb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;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 4cd470862..801c420c2 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma
@@ -20,10 +20,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/Freescale_translation.ma".
 include "emulator/translation/IP2022_translation.ma".
 
 (* ******************************************************* *)
@@ -36,10 +33,10 @@ ndefinition MA_check ≝
  match mcu
   return λm.(aux_im_type m) → Type
  with
-  [ HC05 ⇒ HC05_MA_check
-  | HC08 ⇒ HC08_MA_check
-  | HCS08 ⇒ HCS08_MA_check
-  | RS08 ⇒ RS08_MA_check
+  [ HC05 ⇒ Freescale_MA_check
+  | HC08 ⇒ Freescale_MA_check
+  | HCS08 ⇒ Freescale_MA_check
+  | RS08 ⇒ Freescale_MA_check
   | IP2022 ⇒ IP2022_MA_check
   ].
 
@@ -50,29 +47,29 @@ ndefinition args_picker ≝
  match mcu
   return λm.Πi:(aux_im_type m).MA_check m i → ?
  with
-  [ HC05 ⇒ HC05_args_picker
-  | HC08 ⇒ HC08_args_picker
-  | HCS08 ⇒ HCS08_args_picker
-  | RS08 ⇒ RS08_args_picker
+  [ HC05 ⇒ Freescale_args_picker HC05
+  | HC08 ⇒ Freescale_args_picker HC08
+  | HCS08 ⇒ Freescale_args_picker HCS08
+  | RS08 ⇒ Freescale_args_picker RS08
   | IP2022 ⇒ IP2022_args_picker
   ].
 
 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
-nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:aux_op_type m) (i:aux_im_type m) (p:MA_check m i)
+nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:aux_pseudo_type m) (i:aux_im_type m) (p:MA_check m i)
                                              (param:list (aux_table_type m)) on param ≝
  match param with
  [ nil ⇒ None ? | cons hd tl ⇒
-  match (eq_op m o (fst4T … hd)) ⊗ (eq_im m i (snd4T … hd)) with
+  match (eq_pseudo m o (fst4T … hd)) ⊗ (eq_im m i (snd4T … hd)) with
    [ true ⇒ match thd4T … hd with 
     [ Byte isab ⇒ 
      Some ? ([ (TByte m isab) ]@(args_picker m i p))
     | Word isaw ⇒
-     Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
+     Some ? ([ (TByte m (cnH ? isaw)) ; (TByte m (cnL ? isaw)) ]@(args_picker m i p))
     ]
    | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
 
 ndefinition bytes_of_pseudo_instr_mode_param ≝
-λm:mcu_type.λo:aux_op_type m.λi:aux_im_type m.λp:MA_check m i.
+λm:mcu_type.λo:aux_pseudo_type m.λi:aux_im_type m.λp:MA_check m i.
 bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
 
 (* ****************************** *)
@@ -89,7 +86,7 @@ ndefinition defined_option ≝
 
 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
 ndefinition compile ≝
-λmcu:mcu_type.λi:aux_im_type mcu.λop:aux_op_type mcu.λarg:MA_check mcu i.
+λmcu:mcu_type.λi:aux_im_type mcu.λop:aux_pseudo_type mcu.λarg:MA_check mcu i.
  match bytes_of_pseudo_instr_mode_param mcu op i arg
   return λres:option ?.defined_option ? res → ?
  with