From d6a9ed2a08fcc4e3e26a40cde8cab88c2c69cb3a Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Sat, 30 Jan 2010 09:45:32 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 17 +-- .../ng_assembly/emulator/status/status.ma | 4 +- .../emulator/status/status_lemmas.ma | 14 +-- .../translation/Freescale_translation.ma | 115 ++++++++++++++++++ .../emulator/translation/HC05_translation.ma | 75 ------------ .../emulator/translation/HC08_translation.ma | 109 ----------------- .../emulator/translation/HCS08_translation.ma | 109 ----------------- .../translation/IP2022_translation.ma | 2 +- .../emulator/translation/RS08_translation.ma | 74 ----------- .../emulator/translation/translation.ma | 29 ++--- 10 files changed, 142 insertions(+), 406 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/translation/Freescale_translation.ma delete mode 100755 helm/software/matita/contribs/ng_assembly/emulator/translation/HC05_translation.ma delete mode 100755 helm/software/matita/contribs/ng_assembly/emulator/translation/HC08_translation.ma delete mode 100755 helm/software/matita/contribs/ng_assembly/emulator/translation/HCS08_translation.ma delete mode 100755 helm/software/matita/contribs/ng_assembly/emulator/translation/RS08_translation.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index ef408e293..dfbc41974 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,5 +1,4 @@ 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 @@ -25,19 +24,16 @@ emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/Freescale_instr_m 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 @@ -50,7 +46,6 @@ compiler/ast_type.ma common/list_utility.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 @@ -61,17 +56,15 @@ emulator/model/HC08_model.ma emulator/status/status.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 @@ -93,11 +86,9 @@ emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_ 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 diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma index 0456997fc..927da3d25 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma @@ -34,7 +34,7 @@ include "emulator/opcodes/pseudo.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 ≝ @@ -93,7 +93,7 @@ nlet rec forall_memory_ranged (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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma index 48d10ecf6..2320efa7d 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_lemmas.ma @@ -39,7 +39,7 @@ nlemma symmetric_eqclk : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = eq_clk m clk2 cl ##[ ##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. @@ -50,7 +50,7 @@ nlemma eqclk_to_eq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = true → clk1 = clk2 ##[ ##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. @@ -61,7 +61,7 @@ nlemma eq_to_eqclk : ∀m.∀clk1,clk2.(clk1 = clk2) → (eq_clk m clk1 clk2 = t ##[ ##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. @@ -72,7 +72,7 @@ nlemma neqclk_to_neq : ∀m.∀clk1,clk2.eq_clk m clk1 clk2 = false → clk1 ≠ ##[ ##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. @@ -83,12 +83,12 @@ nlemma neq_to_neqclk : ∀m.∀clk1,clk2.(clk1 ≠ clk2) → (eq_clk m clk1 clk2 ##[ ##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. @@ -99,7 +99,7 @@ nlemma decidable_clk : ∀m.∀clk1,clk2:option (aux_clk_type m).decidable (clk1 ##[ ##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. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/Freescale_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/Freescale_translation.ma new file mode 100755 index 000000000..98d182310 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/Freescale_translation.ma @@ -0,0 +1,115 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ? + ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/HC05_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/HC05_translation.ma deleted file mode 100755 index dcc04ac25..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/HC05_translation.ma +++ /dev/null @@ -1,75 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 ] - ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/HC08_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/HC08_translation.ma deleted file mode 100755 index 16142d426..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/HC08_translation.ma +++ /dev/null @@ -1,109 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 ] - ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/HCS08_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/HCS08_translation.ma deleted file mode 100755 index cef092004..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/HCS08_translation.ma +++ /dev/null @@ -1,109 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 ] - ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma index c3d8efcc6..a207c7c93 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/IP2022_translation.ma @@ -43,7 +43,7 @@ ninductive IP2022_MA_check : IP2022_instr_mode → Type ≝ (* 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 ? diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/RS08_translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/RS08_translation.ma deleted file mode 100755 index b6aa83e8b..000000000 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/RS08_translation.ma +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 ? - ]. 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 c507eac17..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,19 +47,19 @@ 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)) @@ -72,7 +69,7 @@ nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:aux_op_type m) (i: | 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 -- 2.39.2