Stuff moved from old Matita.

[helm.git] / matita / matita / contribs / ng_assembly2 / emulator / translation / Freescale_translation.ma

diff --git a/matita/matita/contribs/ng_assembly2/emulator/translation/Freescale_translation.ma b/matita/matita/contribs/ng_assembly2/emulator/translation/Freescale_translation.ma
new file mode 100755 (executable)
index 0000000..98d1823
--- /dev/null
+++ b/matita/matita/contribs/ng_assembly2/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 ?
+  ].