helm/software/matita/contribs/ng_assembly/freescale/translation.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/table_HC05.ma".
  24 include "freescale/table_HC08.ma".
  25 include "freescale/table_HCS08.ma".
  26 include "freescale/table_RS08.ma".
  27 include "freescale/option.ma".
  28
  29 (* ***************************** *)
  30 (* TRADUZIONE ESADECIMALE → INFO *)
  31 (* ***************************** *)
  32
  33 (* accesso alla tabella della ALU prescelta *)
  34 ndefinition opcode_table ≝
  35 λm:mcu_type.
  36  match m
  37   return λm:mcu_type.list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)
  38  with
  39   [ HC05  ⇒ opcode_table_HC05
  40   | HC08  ⇒ opcode_table_HC08
  41   | HCS08 ⇒ opcode_table_HCS08
  42   | RS08  ⇒ opcode_table_RS08
  43  ].
  44
  45 (* traduzione mcu+esadecimale → info *)
  46 (* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
  47 (* NB: per matchare una word (precode+code) bisogna passare una word *)
  48 (* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
  49 nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16)
  50                                 (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
  51  match param with
  52   [ nil ⇒ None ?
  53   | cons hd tl ⇒
  54    match thd4T … hd with
  55     [ Byte b ⇒ match borw with
  56      [ Byte borw' ⇒ match eq_b8 borw' b with
  57       [ true ⇒ Some ? hd
  58       | false ⇒ full_info_of_word16_aux m borw tl ]
  59      | Word _ ⇒ full_info_of_word16_aux m borw tl ]
  60     | Word w ⇒ match borw with
  61      [ Byte _ ⇒ full_info_of_word16_aux m borw tl
  62      | Word borw' ⇒ match eq_w16 borw' w with
  63       [ true ⇒ Some ? hd
  64       | false ⇒ full_info_of_word16_aux m borw tl ]
  65     ]]].
  66
  67 ndefinition full_info_of_word16 ≝
  68 λm:mcu_type.λborw:byte8_or_word16.
  69 full_info_of_word16_aux m borw (opcode_table m).
  70
  71 (* ******************************************************* *)
  72 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
  73 (* ******************************************************* *)
  74
  75 (* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
  76 ninductive t_byte8 (m:mcu_type) : Type ≝
  77  TByte : byte8 → t_byte8 m.
  78
  79 nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  80  #m; #b1; #b2; #H;
  81  nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
  82  nrewrite < H;
  83  nnormalize;
  84  napply refl_eq.
  85 nqed.
  86
  87 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
  88 ninductive MA_check : instr_mode → Type ≝
  89   maINH              : MA_check MODE_INH
  90 | maINHA             : MA_check MODE_INHA
  91 | maINHX             : MA_check MODE_INHX
  92 | maINHH             : MA_check MODE_INHH
  93 | maINHX0ADD         : MA_check MODE_INHX0ADD
  94 | maINHX1ADD         : byte8 → MA_check MODE_INHX1ADD
  95 | maINHX2ADD         : word16 → MA_check MODE_INHX2ADD
  96 | maIMM1             : byte8  → MA_check MODE_IMM1
  97 | maIMM1EXT          : byte8  → MA_check MODE_IMM1EXT
  98 | maIMM2             : word16 → MA_check MODE_IMM2
  99 | maDIR1             : byte8  → MA_check MODE_DIR1
 100 | maDIR2             : word16 → MA_check MODE_DIR2
 101 | maIX0              : MA_check MODE_IX0
 102 | maIX1              : byte8  → MA_check MODE_IX1
 103 | maIX2              : word16 → MA_check MODE_IX2
 104 | maSP1              : byte8  → MA_check MODE_SP1
 105 | maSP2              : word16 → MA_check MODE_SP2
 106 | maDIR1_to_DIR1     : byte8 → byte8 → MA_check MODE_DIR1_to_DIR1
 107 | maIMM1_to_DIR1     : byte8 → byte8 → MA_check MODE_IMM1_to_DIR1
 108 | maIX0p_to_DIR1     : byte8 → MA_check MODE_IX0p_to_DIR1
 109 | maDIR1_to_IX0p     : byte8 → MA_check MODE_DIR1_to_IX0p
 110 | maINHA_and_IMM1    : byte8 → MA_check MODE_INHA_and_IMM1
 111 | maINHX_and_IMM1    : byte8 → MA_check MODE_INHX_and_IMM1
 112 | maIMM1_and_IMM1    : byte8 → byte8 → MA_check MODE_IMM1_and_IMM1
 113 | maDIR1_and_IMM1    : byte8 → byte8 → MA_check MODE_DIR1_and_IMM1
 114 | maIX0_and_IMM1     : byte8 → MA_check MODE_IX0_and_IMM1
 115 | maIX0p_and_IMM1    : byte8 → MA_check MODE_IX0p_and_IMM1
 116 | maIX1_and_IMM1     : byte8 → byte8 → MA_check MODE_IX1_and_IMM1
 117 | maIX1p_and_IMM1    : byte8 → byte8 → MA_check MODE_IX1p_and_IMM1
 118 | maSP1_and_IMM1     : byte8 → byte8 → MA_check MODE_SP1_and_IMM1
 119 | maDIRn             : ∀n.byte8 → MA_check (MODE_DIRn n)
 120 | maDIRn_and_IMM1    : ∀n.byte8 → byte8 → MA_check (MODE_DIRn_and_IMM1 n)
 121 | maTNY              : ∀e.MA_check (MODE_TNY e)
 122 | maSRT              : ∀t.MA_check (MODE_SRT t)
 123 .
 124
 125 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
 126    MA_check i → list (t_byte8 m) *)
 127 ndefinition args_picker ≝
 128 λm:mcu_type.λi:instr_mode.λargs:MA_check i.
 129  match args with
 130   (* inherent: legale se nessun operando *)
 131   [ maINH    ⇒ nil ?
 132   | maINHA   ⇒ nil ?
 133   | maINHX   ⇒ nil ?
 134   | maINHH   ⇒ nil ?
 135   (* inherent address: legale se nessun operando/1 byte/1 word *)
 136   | maINHX0ADD ⇒ nil ?
 137   | maINHX1ADD b ⇒ [ TByte m b ]
 138   | maINHX2ADD w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 139   (* _0/1/2: legale se nessun operando/1 byte/1 word *)
 140   | maIMM1 b ⇒ [ TByte m b ]
 141   | maIMM1EXT b ⇒ [ TByte m b ]
 142   | maIMM2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 143   | maDIR1 b ⇒ [ TByte m b ]
 144   | maDIR2 w ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 145   | maIX0    ⇒ nil ?
 146   | maIX1 b  ⇒ [ TByte m b ]
 147   | maIX2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 148   | maSP1 b  ⇒ [ TByte m b ]
 149   | maSP2 w  ⇒ [ TByte m (w16h w); TByte m (w16l w) ]
 150   (* movimento: legale se 2 operandi byte *)
 151   | maDIR1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
 152   | maIMM1_to_DIR1 b1 b2  ⇒ [ TByte m b1 ; TByte m b2 ]
 153   | maIX0p_to_DIR1 b      ⇒ [ TByte m b]
 154   | maDIR1_to_IX0p b      ⇒ [ TByte m b]
 155   (* cbeq/dbnz: legale se 1/2 operandi byte *)
 156   | maINHA_and_IMM1 b     ⇒ [ TByte m b]
 157   | maINHX_and_IMM1 b     ⇒ [ TByte m b]
 158   | maIMM1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 159   | maDIR1_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 160   | maIX0_and_IMM1  b     ⇒ [ TByte m b]
 161   | maIX0p_and_IMM1 b     ⇒ [ TByte m b]
 162   | maIX1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 163   | maIX1p_and_IMM1 b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 164   | maSP1_and_IMM1  b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 165   (* DIRn: legale se 1 operando byte *)
 166   | maDIRn _ b ⇒ [ TByte m b]
 167   (* DIRn_and_IMM1: legale se 2 operandi byte *)
 168   | maDIRn_and_IMM1 _ b1 b2 ⇒ [ TByte m b1 ; TByte m b2 ]
 169   (* TNY: legale se nessun operando *)
 170   | maTNY _ ⇒ nil ?
 171   (* SRT: legale se nessun operando *)
 172   | maSRT _ ⇒ nil ?
 173   ].
 174
 175 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
 176 nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:any_opcode m) (i:instr_mode) (p:MA_check i)
 177                                              (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
 178  match param with
 179  [ nil ⇒ None ? | cons hd tl ⇒
 180   match (eq_anyop m o (fst4T … hd)) ⊗ (eq_instrmode i (snd4T … hd)) with
 181    [ true ⇒ match thd4T … hd with
 182     [ Byte isab ⇒
 183      Some ? ([ (TByte m isab) ]@(args_picker m i p))
 184     | Word isaw ⇒
 185      Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
 186     ]
 187    | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
 188
 189 ndefinition bytes_of_pseudo_instr_mode_param ≝
 190 λm:mcu_type.λo:any_opcode m.λi:instr_mode.λp:MA_check i.
 191 bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
 192
 193 (* ****************************** *)
 194 (* APPROCCIO COMPILAZIONE AL VOLO *)
 195 (* ****************************** *)
 196
 197 (* ausiliario di compile *)
 198 ndefinition defined_option ≝
 199  λT:Type.λo:option T.
 200   match o with
 201    [ None ⇒ False
 202    | Some _ ⇒ True
 203    ].
 204
 205 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
 206 ndefinition compile ≝
 207 λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i.
 208  match bytes_of_pseudo_instr_mode_param mcu (anyOP mcu op) i arg
 209   return λres:option ?.defined_option ? res → ?
 210  with
 211   [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
 212   | Some x ⇒ λp:defined_option ? (Some ? x).x
 213   ].
 214
 215 (* detipatore del compilato: (t_byte8 m) → byte8 *)
 216 nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
 217  match p1 with
 218   [ nil ⇒ p2
 219   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
 220   ].
 221
 222 nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
 223  match p1 with
 224   [ nil ⇒ p2
 225   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
 226   ].
 227
 228 nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
 229  match p1 with
 230   [ nil ⇒ p2
 231   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
 232   ].
 233
 234 nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
 235  match p1 with
 236   [ nil ⇒ p2
 237   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
 238   ].
 239
 240 ndefinition source_to_byte8 ≝
 241 λm:mcu_type.
 242  match m
 243   return λm:mcu_type.list (t_byte8 m) → list byte8
 244  with
 245   [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
 246   | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
 247   | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
 248   | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []
 249   ].