(* *)
(* ********************************************************************** *)
-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".
(* ******************************************************* *)
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
].
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).
(* ****************************** *)
(* 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