num/word24_lemmas.ma num/byte8_lemmas.ma num/word24.ma
-emulator/read_write/FREESCALE_load_write_base.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma
emulator/model/HCS08_model.ma emulator/status/status.ma
common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/pseudo.ma
common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma
common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma
-emulator/translation/HCS08_translation.ma emulator/translation/translation_base.ma
emulator/memory/memory_trees.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma
-emulator/read_write/RS08_load_write.ma emulator/read_write/FREESCALE_load_write_base.ma
emulator/opcodes/Freescale_pseudo.ma num/bool.ma
-emulator/read_write/HC08_load_write.ma emulator/read_write/FREESCALE_load_write_base.ma
num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma
-emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr_mode.ma num/bool_lemmas.ma num/oct_lemmas.ma
+emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma
test_errori.ma
compiler/environment.ma common/string.ma compiler/ast_type.ma
common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma
-emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma
emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma
+emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma
emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
emulator/status/HC05_status.ma num/word16.ma
emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/Freescale_pseudo.ma num/bool_lemmas.ma
num/word16.ma num/byte8.ma
common/prod.ma num/bool.ma
emulator/opcodes/IP2022_instr_mode.ma num/word16.ma
-emulator/translation/HC08_translation.ma emulator/translation/translation_base.ma
num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
emulator/status/HC05_status_lemmas.ma emulator/status/HC05_status.ma num/word16_lemmas.ma
emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma
num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma
emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma
-emulator/translation/RS08_translation.ma emulator/translation/translation_base.ma
emulator/model/HC05_model.ma emulator/status/status.ma
emulator/status/status_setter.ma emulator/status/status.ma
-emulator/translation/HC05_translation.ma emulator/translation/translation_base.ma
num/word32.ma num/word16.ma
common/ascii.ma num/bool.ma
-emulator/read_write/load_write_base.ma emulator/read_write/read_write.ma
emulator/model/IP2022_model.ma emulator/status/status.ma
emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/pseudo.ma
emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/pseudo.ma
emulator/status/IP2022_status.ma emulator/memory/memory_struct.ma num/word16.ma num/word24.ma
+emulator/translation/Freescale_translation.ma emulator/translation/translation_base.ma
num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
emulator/memory/memory_func.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma
emulator/read_write/read_write.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/RS08_read_write.ma
emulator/translation/IP2022_translation.ma emulator/translation/translation_base.ma
universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma
num/bitrigesim.ma num/bool.ma
-emulator/read_write/HC05_load_write.ma emulator/read_write/FREESCALE_load_write_base.ma
emulator/opcodes/pseudo.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma
-emulator/translation/translation.ma emulator/translation/HC05_translation.ma emulator/translation/HC08_translation.ma emulator/translation/HCS08_translation.ma emulator/translation/IP2022_translation.ma emulator/translation/RS08_translation.ma
-emulator/read_write/fetch.ma emulator/status/status_getter.ma emulator/translation/translation_base.ma
+emulator/translation/translation.ma emulator/translation/Freescale_translation.ma emulator/translation/IP2022_translation.ma
emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/oct_lemmas.ma
num/oct.ma num/bool.ma
common/list.ma common/theory.ma
(* descrittore del click = stato di avanzamento dell'esecuzione *)
(* 1) None = istruzione eseguita, attesa del fetch *)
(* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *)
-ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_op_type m) (aux_im_type m) byte8 word16.
+ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
(* tipo processore dipendente dalla mcu, varia solo la ALU *)
nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
(forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
].
-ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_op m) (eq_im m) eq_b8 eq_w16).
+ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_pseudo m) (eq_im m) eq_b8 eq_w16).
(* generalizzazione del confronto fra stati *)
ndefinition eq_anystatus ≝
##[ ##1: napply symmetric_eqw16
##| ##2: napply symmetric_eqb8
##| ##3: napply (symmetric_eqim m)
- ##| ##4: napply (symmetric_eqop m)
+ ##| ##4: napply (symmetric_eqpseudo m)
##| ##5: napply symmetric_eqb8
##]
nqed.
##[ ##1: napply eqw16_to_eq
##| ##2: napply eqb8_to_eq
##| ##3: napply (eqim_to_eq m)
- ##| ##4: napply (eqop_to_eq m)
+ ##| ##4: napply (eqpseudo_to_eq m)
##| ##5: napply eqb8_to_eq
##]
nqed.
##[ ##1: napply eq_to_eqw16
##| ##2: napply eq_to_eqb8
##| ##3: napply (eq_to_eqim m)
- ##| ##4: napply (eq_to_eqop m)
+ ##| ##4: napply (eq_to_eqpseudo m)
##| ##5: napply eq_to_eqb8
##]
nqed.
##[ ##1: napply neqw16_to_neq
##| ##2: napply neqb8_to_neq
##| ##3: napply (neqim_to_neq m)
- ##| ##4: napply (neqop_to_neq m)
+ ##| ##4: napply (neqpseudo_to_neq m)
##| ##5: napply neqb8_to_neq
##]
nqed.
##[ ##1: napply neq_to_neqw16
##| ##2: napply neq_to_neqb8
##| ##3: napply (neq_to_neqim m)
- ##| ##4: napply (neq_to_neqop m)
+ ##| ##4: napply (neq_to_neqpseudo m)
##| ##5: napply neq_to_neqb8
##| ##6: napply decidable_w16
##| ##7: napply decidable_b8
##| ##8: napply (decidable_im m)
- ##| ##9: napply (decidable_op m)
+ ##| ##9: napply (decidable_pseudo m)
##| ##10: napply decidable_b8
##]
nqed.
##[ ##1: napply decidable_w16
##| ##2: napply decidable_b8
##| ##3: napply (decidable_im m)
- ##| ##4: napply (decidable_op m)
+ ##| ##4: napply (decidable_pseudo m)
##| ##5: napply decidable_b8
##]
nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/translation/translation_base.ma".
+
+(* ******************************************************* *)
+(* TRADUZIONE MCU+PSEUDO+MODALITA'+ARGOMENTI → ESADECIMALE *)
+(* ******************************************************* *)
+
+(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
+ninductive Freescale_MA_check : Freescale_instr_mode → Type ≝
+ maINH : Freescale_MA_check MODE_INH
+| maINHA : Freescale_MA_check MODE_INHA
+| maINHX : Freescale_MA_check MODE_INHX
+| maINHH : Freescale_MA_check MODE_INHH
+| maINHX0ADD : Freescale_MA_check MODE_INHX0ADD
+| maINHX1ADD : byte8 → Freescale_MA_check MODE_INHX1ADD
+| maINHX2ADD : word16 → Freescale_MA_check MODE_INHX2ADD
+| maIMM1 : byte8 → Freescale_MA_check MODE_IMM1
+| maIMM1EXT : byte8 → Freescale_MA_check MODE_IMM1EXT
+| maIMM2 : word16 → Freescale_MA_check MODE_IMM2
+| maDIR1 : byte8 → Freescale_MA_check MODE_DIR1
+| maDIR2 : word16 → Freescale_MA_check MODE_DIR2
+| maIX0 : Freescale_MA_check MODE_IX0
+| maIX1 : byte8 → Freescale_MA_check MODE_IX1
+| maIX2 : word16 → Freescale_MA_check MODE_IX2
+| maSP1 : byte8 → Freescale_MA_check MODE_SP1
+| maSP2 : word16 → Freescale_MA_check MODE_SP2
+| maDIR1_to_DIR1 : byte8 → byte8 → Freescale_MA_check MODE_DIR1_to_DIR1
+| maIMM1_to_DIR1 : byte8 → byte8 → Freescale_MA_check MODE_IMM1_to_DIR1
+| maIX0p_to_DIR1 : byte8 → Freescale_MA_check MODE_IX0p_to_DIR1
+| maDIR1_to_IX0p : byte8 → Freescale_MA_check MODE_DIR1_to_IX0p
+| maINHA_and_IMM1 : byte8 → Freescale_MA_check MODE_INHA_and_IMM1
+| maINHX_and_IMM1 : byte8 → Freescale_MA_check MODE_INHX_and_IMM1
+| maIMM1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_IMM1_and_IMM1
+| maDIR1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_DIR1_and_IMM1
+| maIX0_and_IMM1 : byte8 → Freescale_MA_check MODE_IX0_and_IMM1
+| maIX0p_and_IMM1 : byte8 → Freescale_MA_check MODE_IX0p_and_IMM1
+| maIX1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_IX1_and_IMM1
+| maIX1p_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_IX1p_and_IMM1
+| maSP1_and_IMM1 : byte8 → byte8 → Freescale_MA_check MODE_SP1_and_IMM1
+| maDIRn : ∀n.byte8 → Freescale_MA_check (MODE_DIRn n)
+| maDIRn_and_IMM1 : ∀n.byte8 → byte8 → Freescale_MA_check (MODE_DIRn_and_IMM1 n)
+| maTNY : ∀e.Freescale_MA_check (MODE_TNY e)
+| maSRT : ∀t.Freescale_MA_check (MODE_SRT t)
+.
+
+(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
+ MA_check i → list (t_byte8 m) *)
+ndefinition Freescale_args_picker ≝
+λm.λi:Freescale_instr_mode.λargs:Freescale_MA_check i.
+ match args with
+ (* inherent: legale se nessun operando *)
+ [ maINH ⇒ nil ?
+ | maINHA ⇒ nil ?
+ | maINHX ⇒ nil ?
+ | maINHH ⇒ nil ?
+ (* inherent address: legale se nessun operando/1 byte/1 word *)
+ | maINHX0ADD ⇒ nil ?
+ | maINHX1ADD b ⇒ [ TByte m b ]
+ | maINHX2ADD w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ (* _0/1/2: legale se nessun operando/1 byte/1 word *)
+ | maIMM1 b ⇒ [ TByte m b ]
+ | maIMM1EXT b ⇒ [ TByte m b ]
+ | maIMM2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ | maDIR1 b ⇒ [ TByte m b ]
+ | maDIR2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ | maIX0 ⇒ nil ?
+ | maIX1 b ⇒ [ TByte m b ]
+ | maIX2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ | maSP1 b ⇒ [ TByte m b ]
+ | maSP2 w ⇒ [ TByte m (cnH ? w); TByte m (cnL ? w) ]
+ (* movimento: legale se 2 operandi byte *)
+ | maDIR1_to_DIR1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIMM1_to_DIR1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIX0p_to_DIR1 b ⇒ [ TByte m b]
+ | maDIR1_to_IX0p b ⇒ [ TByte m b]
+ (* cbeq/dbnz: legale se 1/2 operandi byte *)
+ | maINHA_and_IMM1 b ⇒ [ TByte m b]
+ | maINHX_and_IMM1 b ⇒ [ TByte m b]
+ | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIX0_and_IMM1 b ⇒ [ TByte m b]
+ | maIX0p_and_IMM1 b ⇒ [ TByte m b]
+ | maIX1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ | maSP1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ (* DIRn: legale se 1 operando byte *)
+ | maDIRn _ b ⇒ [ TByte m b]
+ (* DIRn_and_IMM1: legale se 2 operandi byte *)
+ | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
+ (* TNY: legale se nessun operando *)
+ | maTNY _ ⇒ nil ?
+ (* SRT: legale se nessun operando *)
+ | maSRT _ ⇒ nil ?
+ ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
-(* *)
-(* ********************************************************************** *)
-
-include "emulator/translation/translation_base.ma".
-
-(* ******************************************************* *)
-(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
-(* ******************************************************* *)
-
-(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
-ninductive HC05_MA_check : HC05_instr_mode → Type ≝
- maINH : HC05_MA_check MODE_INH
-| maINHA : HC05_MA_check MODE_INHA
-| maINHX : HC05_MA_check MODE_INHX
-| maINHX0ADD : HC05_MA_check MODE_INHX0ADD
-| maINHX1ADD : byte8 → HC05_MA_check MODE_INHX1ADD
-| maINHX2ADD : word16 → HC05_MA_check MODE_INHX2ADD
-| maIMM1 : byte8 → HC05_MA_check MODE_IMM1
-| maIMM1EXT : byte8 → HC05_MA_check MODE_IMM1EXT
-| maIMM2 : word16 → HC05_MA_check MODE_IMM2
-| maDIR1 : byte8 → HC05_MA_check MODE_DIR1
-| maDIR2 : word16 → HC05_MA_check MODE_DIR2
-| maIX0 : HC05_MA_check MODE_IX0
-| maIX1 : byte8 → HC05_MA_check MODE_IX1
-| maIX2 : word16 → HC05_MA_check MODE_IX2
-| maDIRn : ∀n.byte8 → HC05_MA_check (MODE_DIRn n)
-| maDIRn_and_IMM1 : ∀n.byte8 → byte8 → HC05_MA_check (MODE_DIRn_and_IMM1 n)
-.
-
-(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
- MA_check i → list (t_byte8 m) *)
-ndefinition HC05_args_picker ≝
-λi:aux_im_type HC05.λargs:HC05_MA_check i.
- match args with
- (* inherent: legale se nessun operando *)
- [ maINH ⇒ nil ?
- | maINHA ⇒ nil ?
- | maINHX ⇒ nil ?
- (* inherent address: legale se nessun operando/1 byte/1 word *)
- | maINHX0ADD ⇒ nil ?
- | maINHX1ADD b ⇒ [ TByte HC05 b ]
- | maINHX2ADD w ⇒ [ TByte HC05 (cnH ? w); TByte HC05 (cnL ? w) ]
- (* _0/1/2: legale se nessun operando/1 byte/1 word *)
- | maIMM1 b ⇒ [ TByte HC05 b ]
- | maIMM1EXT b ⇒ [ TByte HC05 b ]
- | maIMM2 w ⇒ [ TByte HC05 (cnH ? w); TByte HC05 (cnL ? w) ]
- | maDIR1 b ⇒ [ TByte HC05 b ]
- | maDIR2 w ⇒ [ TByte HC05 (cnH ? w); TByte HC05 (cnL ? w) ]
- | maIX0 ⇒ nil ?
- | maIX1 b ⇒ [ TByte HC05 b ]
- | maIX2 w ⇒ [ TByte HC05 (cnH ? w); TByte HC05 (cnL ? w) ]
- (* DIRn: legale se 1 operando byte *)
- | maDIRn _ b ⇒ [ TByte HC05 b]
- (* DIRn_and_IMM1: legale se 2 operandi byte *)
- | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte HC05 b1 ; TByte HC05 b2 ]
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
-(* *)
-(* ********************************************************************** *)
-
-include "emulator/translation/translation_base.ma".
-
-(* ******************************************************* *)
-(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
-(* ******************************************************* *)
-
-(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
-ninductive HC08_MA_check : HC08_instr_mode → Type ≝
- maINH : HC08_MA_check MODE_INH
-| maINHA : HC08_MA_check MODE_INHA
-| maINHX : HC08_MA_check MODE_INHX
-| maINHH : HC08_MA_check MODE_INHH
-| maINHX0ADD : HC08_MA_check MODE_INHX0ADD
-| maINHX1ADD : byte8 → HC08_MA_check MODE_INHX1ADD
-| maINHX2ADD : word16 → HC08_MA_check MODE_INHX2ADD
-| maIMM1 : byte8 → HC08_MA_check MODE_IMM1
-| maIMM1EXT : byte8 → HC08_MA_check MODE_IMM1EXT
-| maIMM2 : word16 → HC08_MA_check MODE_IMM2
-| maDIR1 : byte8 → HC08_MA_check MODE_DIR1
-| maDIR2 : word16 → HC08_MA_check MODE_DIR2
-| maIX0 : HC08_MA_check MODE_IX0
-| maIX1 : byte8 → HC08_MA_check MODE_IX1
-| maIX2 : word16 → HC08_MA_check MODE_IX2
-| maSP1 : byte8 → HC08_MA_check MODE_SP1
-| maSP2 : word16 → HC08_MA_check MODE_SP2
-| maDIR1_to_DIR1 : byte8 → byte8 → HC08_MA_check MODE_DIR1_to_DIR1
-| maIMM1_to_DIR1 : byte8 → byte8 → HC08_MA_check MODE_IMM1_to_DIR1
-| maIX0p_to_DIR1 : byte8 → HC08_MA_check MODE_IX0p_to_DIR1
-| maDIR1_to_IX0p : byte8 → HC08_MA_check MODE_DIR1_to_IX0p
-| maINHA_and_IMM1 : byte8 → HC08_MA_check MODE_INHA_and_IMM1
-| maINHX_and_IMM1 : byte8 → HC08_MA_check MODE_INHX_and_IMM1
-| maIMM1_and_IMM1 : byte8 → byte8 → HC08_MA_check MODE_IMM1_and_IMM1
-| maDIR1_and_IMM1 : byte8 → byte8 → HC08_MA_check MODE_DIR1_and_IMM1
-| maIX0_and_IMM1 : byte8 → HC08_MA_check MODE_IX0_and_IMM1
-| maIX0p_and_IMM1 : byte8 → HC08_MA_check MODE_IX0p_and_IMM1
-| maIX1_and_IMM1 : byte8 → byte8 → HC08_MA_check MODE_IX1_and_IMM1
-| maIX1p_and_IMM1 : byte8 → byte8 → HC08_MA_check MODE_IX1p_and_IMM1
-| maSP1_and_IMM1 : byte8 → byte8 → HC08_MA_check MODE_SP1_and_IMM1
-| maDIRn : ∀n.byte8 → HC08_MA_check (MODE_DIRn n)
-| maDIRn_and_IMM1 : ∀n.byte8 → byte8 → HC08_MA_check (MODE_DIRn_and_IMM1 n)
-.
-
-(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
- MA_check i → list (t_byte8 m) *)
-ndefinition HC08_args_picker ≝
-λi:aux_im_type HC08.λargs:HC08_MA_check i.
- match args with
- (* inherent: legale se nessun operando *)
- [ maINH ⇒ nil ?
- | maINHA ⇒ nil ?
- | maINHX ⇒ nil ?
- | maINHH ⇒ nil ?
- (* inherent address: legale se nessun operando/1 byte/1 word *)
- | maINHX0ADD ⇒ nil ?
- | maINHX1ADD b ⇒ [ TByte HC08 b ]
- | maINHX2ADD w ⇒ [ TByte HC08 (cnH ? w); TByte HC08 (cnL ? w) ]
- (* _0/1/2: legale se nessun operando/1 byte/1 word *)
- | maIMM1 b ⇒ [ TByte HC08 b ]
- | maIMM1EXT b ⇒ [ TByte HC08 b ]
- | maIMM2 w ⇒ [ TByte HC08 (cnH ? w); TByte HC08 (cnL ? w) ]
- | maDIR1 b ⇒ [ TByte HC08 b ]
- | maDIR2 w ⇒ [ TByte HC08 (cnH ? w); TByte HC08 (cnL ? w) ]
- | maIX0 ⇒ nil ?
- | maIX1 b ⇒ [ TByte HC08 b ]
- | maIX2 w ⇒ [ TByte HC08 (cnH ? w); TByte HC08 (cnL ? w) ]
- | maSP1 b ⇒ [ TByte HC08 b ]
- | maSP2 w ⇒ [ TByte HC08 (cnH ? w); TByte HC08 (cnL ? w) ]
- (* movimento: legale se 2 operandi byte *)
- | maDIR1_to_DIR1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- | maIMM1_to_DIR1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- | maIX0p_to_DIR1 b ⇒ [ TByte HC08 b]
- | maDIR1_to_IX0p b ⇒ [ TByte HC08 b]
- (* cbeq/dbnz: legale se 1/2 operandi byte *)
- | maINHA_and_IMM1 b ⇒ [ TByte HC08 b]
- | maINHX_and_IMM1 b ⇒ [ TByte HC08 b]
- | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- | maIX0_and_IMM1 b ⇒ [ TByte HC08 b]
- | maIX0p_and_IMM1 b ⇒ [ TByte HC08 b]
- | maIX1_and_IMM1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- | maSP1_and_IMM1 b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- (* DIRn: legale se 1 operando byte *)
- | maDIRn _ b ⇒ [ TByte HC08 b]
- (* DIRn_and_IMM1: legale se 2 operandi byte *)
- | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte HC08 b1 ; TByte HC08 b2 ]
- ].
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
-(* *)
-(* ********************************************************************** *)
-
-include "emulator/translation/translation_base.ma".
-
-(* ******************************************************* *)
-(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
-(* ******************************************************* *)
-
-(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
-ninductive HCS08_MA_check : HC08_instr_mode → Type ≝
- maINH : HCS08_MA_check MODE_INH
-| maINHA : HCS08_MA_check MODE_INHA
-| maINHX : HCS08_MA_check MODE_INHX
-| maINHH : HCS08_MA_check MODE_INHH
-| maINHX0ADD : HCS08_MA_check MODE_INHX0ADD
-| maINHX1ADD : byte8 → HCS08_MA_check MODE_INHX1ADD
-| maINHX2ADD : word16 → HCS08_MA_check MODE_INHX2ADD
-| maIMM1 : byte8 → HCS08_MA_check MODE_IMM1
-| maIMM1EXT : byte8 → HCS08_MA_check MODE_IMM1EXT
-| maIMM2 : word16 → HCS08_MA_check MODE_IMM2
-| maDIR1 : byte8 → HCS08_MA_check MODE_DIR1
-| maDIR2 : word16 → HCS08_MA_check MODE_DIR2
-| maIX0 : HCS08_MA_check MODE_IX0
-| maIX1 : byte8 → HCS08_MA_check MODE_IX1
-| maIX2 : word16 → HCS08_MA_check MODE_IX2
-| maSP1 : byte8 → HCS08_MA_check MODE_SP1
-| maSP2 : word16 → HCS08_MA_check MODE_SP2
-| maDIR1_to_DIR1 : byte8 → byte8 → HCS08_MA_check MODE_DIR1_to_DIR1
-| maIMM1_to_DIR1 : byte8 → byte8 → HCS08_MA_check MODE_IMM1_to_DIR1
-| maIX0p_to_DIR1 : byte8 → HCS08_MA_check MODE_IX0p_to_DIR1
-| maDIR1_to_IX0p : byte8 → HCS08_MA_check MODE_DIR1_to_IX0p
-| maINHA_and_IMM1 : byte8 → HCS08_MA_check MODE_INHA_and_IMM1
-| maINHX_and_IMM1 : byte8 → HCS08_MA_check MODE_INHX_and_IMM1
-| maIMM1_and_IMM1 : byte8 → byte8 → HCS08_MA_check MODE_IMM1_and_IMM1
-| maDIR1_and_IMM1 : byte8 → byte8 → HCS08_MA_check MODE_DIR1_and_IMM1
-| maIX0_and_IMM1 : byte8 → HCS08_MA_check MODE_IX0_and_IMM1
-| maIX0p_and_IMM1 : byte8 → HCS08_MA_check MODE_IX0p_and_IMM1
-| maIX1_and_IMM1 : byte8 → byte8 → HCS08_MA_check MODE_IX1_and_IMM1
-| maIX1p_and_IMM1 : byte8 → byte8 → HCS08_MA_check MODE_IX1p_and_IMM1
-| maSP1_and_IMM1 : byte8 → byte8 → HCS08_MA_check MODE_SP1_and_IMM1
-| maDIRn : ∀n.byte8 → HCS08_MA_check (MODE_DIRn n)
-| maDIRn_and_IMM1 : ∀n.byte8 → byte8 → HCS08_MA_check (MODE_DIRn_and_IMM1 n)
-.
-
-(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
- MA_check i → list (t_byte8 m) *)
-ndefinition HCS08_args_picker ≝
-λi:aux_im_type HCS08.λargs:HCS08_MA_check i.
- match args with
- (* inherent: legale se nessun operando *)
- [ maINH ⇒ nil ?
- | maINHA ⇒ nil ?
- | maINHX ⇒ nil ?
- | maINHH ⇒ nil ?
- (* inherent address: legale se nessun operando/1 byte/1 word *)
- | maINHX0ADD ⇒ nil ?
- | maINHX1ADD b ⇒ [ TByte HCS08 b ]
- | maINHX2ADD w ⇒ [ TByte HCS08 (cnH ? w); TByte HCS08 (cnL ? w) ]
- (* _0/1/2: legale se nessun operando/1 byte/1 word *)
- | maIMM1 b ⇒ [ TByte HCS08 b ]
- | maIMM1EXT b ⇒ [ TByte HCS08 b ]
- | maIMM2 w ⇒ [ TByte HCS08 (cnH ? w); TByte HCS08 (cnL ? w) ]
- | maDIR1 b ⇒ [ TByte HCS08 b ]
- | maDIR2 w ⇒ [ TByte HCS08 (cnH ? w); TByte HCS08 (cnL ? w) ]
- | maIX0 ⇒ nil ?
- | maIX1 b ⇒ [ TByte HCS08 b ]
- | maIX2 w ⇒ [ TByte HCS08 (cnH ? w); TByte HCS08 (cnL ? w) ]
- | maSP1 b ⇒ [ TByte HCS08 b ]
- | maSP2 w ⇒ [ TByte HCS08 (cnH ? w); TByte HCS08 (cnL ? w) ]
- (* movimento: legale se 2 operandi byte *)
- | maDIR1_to_DIR1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- | maIMM1_to_DIR1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- | maIX0p_to_DIR1 b ⇒ [ TByte HCS08 b]
- | maDIR1_to_IX0p b ⇒ [ TByte HCS08 b]
- (* cbeq/dbnz: legale se 1/2 operandi byte *)
- | maINHA_and_IMM1 b ⇒ [ TByte HCS08 b]
- | maINHX_and_IMM1 b ⇒ [ TByte HCS08 b]
- | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- | maIX0_and_IMM1 b ⇒ [ TByte HCS08 b]
- | maIX0p_and_IMM1 b ⇒ [ TByte HCS08 b]
- | maIX1_and_IMM1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- | maSP1_and_IMM1 b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- (* DIRn: legale se 1 operando byte *)
- | maDIRn _ b ⇒ [ TByte HCS08 b]
- (* DIRn_and_IMM1: legale se 2 operandi byte *)
- | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte HCS08 b1 ; TByte HCS08 b2 ]
- ].
(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
MA_check i → list (t_byte8 m) *)
ndefinition IP2022_args_picker ≝
-λi:aux_im_type IP2022.λargs:IP2022_MA_check i.
+λi:IP2022_instr_mode.λargs:IP2022_MA_check i.
match args with
[ maINH ⇒ nil ?
| maIMM3 _ ⇒ nil ?
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
-(* *)
-(* ********************************************************************** *)
-
-include "emulator/translation/translation_base.ma".
-
-(* ******************************************************* *)
-(* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
-(* ******************************************************* *)
-
-(* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
-ninductive RS08_MA_check : RS08_instr_mode → Type ≝
- maINH : RS08_MA_check MODE_INH
-| maINHA : RS08_MA_check MODE_INHA
-| maIMM1 : byte8 → RS08_MA_check MODE_IMM1
-| maIMM2 : word16 → RS08_MA_check MODE_IMM2
-| maDIR1 : byte8 → RS08_MA_check MODE_DIR1
-| maDIR1_to_DIR1 : byte8 → byte8 → RS08_MA_check MODE_DIR1_to_DIR1
-| maIMM1_to_DIR1 : byte8 → byte8 → RS08_MA_check MODE_IMM1_to_DIR1
-| maINHA_and_IMM1 : byte8 → RS08_MA_check MODE_INHA_and_IMM1
-| maIMM1_and_IMM1 : byte8 → byte8 → RS08_MA_check MODE_IMM1_and_IMM1
-| maDIR1_and_IMM1 : byte8 → byte8 → RS08_MA_check MODE_DIR1_and_IMM1
-| maDIRn : ∀n.byte8 → RS08_MA_check (MODE_DIRn n)
-| maDIRn_and_IMM1 : ∀n.byte8 → byte8 → RS08_MA_check (MODE_DIRn_and_IMM1 n)
-| maTNY : ∀e.RS08_MA_check (MODE_TNY e)
-| maSRT : ∀t.RS08_MA_check (MODE_SRT t)
-.
-
-(* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
- MA_check i → list (t_byte8 m) *)
-ndefinition RS08_args_picker ≝
-λi:aux_im_type RS08.λargs:RS08_MA_check i.
- match args with
- (* inherent: legale se nessun operando *)
- [ maINH ⇒ nil ?
- | maINHA ⇒ nil ?
- (* _0/1/2: legale se nessun operando/1 byte/1 word *)
- | maIMM1 b ⇒ [ TByte RS08 b ]
- | maIMM2 w ⇒ [ TByte RS08 (cnH ? w); TByte RS08 (cnL ? w) ]
- | maDIR1 b ⇒ [ TByte RS08 b ]
- (* movimento: legale se 2 operandi byte *)
- | maDIR1_to_DIR1 b1 b2 ⇒ [ TByte RS08 b1 ; TByte RS08 b2 ]
- | maIMM1_to_DIR1 b1 b2 ⇒ [ TByte RS08 b1 ; TByte RS08 b2 ]
- (* cbeq/dbnz: legale se 1/2 operandi byte *)
- | maINHA_and_IMM1 b ⇒ [ TByte RS08 b]
- | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte RS08 b1 ; TByte RS08 b2 ]
- | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte RS08 b1 ; TByte RS08 b2 ]
- (* DIRn: legale se 1 operando byte *)
- | maDIRn _ b ⇒ [ TByte RS08 b]
- (* DIRn_and_IMM1: legale se 2 operandi byte *)
- | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte RS08 b1 ; TByte RS08 b2 ]
- (* TNY: legale se nessun operando *)
- | maTNY _ ⇒ nil ?
- (* SRT: legale se nessun operando *)
- | maSRT _ ⇒ nil ?
- ].
(* *)
(* ********************************************************************** *)
-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))
| 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
projects / helm.git / commitdiff