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