matita/matita/contribs/ng_assembly/emulator/translation/translation_base.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/opcodes/pseudo.ma".
  24 include "common/option.ma".
  25 include "emulator/opcodes/HC05_table.ma".
  26 include "emulator/opcodes/HC08_table.ma".
  27 include "emulator/opcodes/HCS08_table.ma".
  28 include "emulator/opcodes/RS08_table.ma".
  29 include "emulator/opcodes/IP2022_table.ma".
  30
  31 (* ***************************** *)
  32 (* TRADUZIONE ESADECIMALE → INFO *)
  33 (* ***************************** *)
  34
  35 (* accesso alla tabella della ALU prescelta *)
  36 ndefinition opcode_table ≝
  37 λm:mcu_type.
  38  match m
  39   return λm:mcu_type.list (aux_table_type m)
  40  with
  41   [ HC05  ⇒ opcode_table_HC05
  42   | HC08  ⇒ opcode_table_HC08
  43   | HCS08 ⇒ opcode_table_HCS08
  44   | RS08  ⇒ opcode_table_RS08
  45   | IP2022 ⇒ opcode_table_IP2022
  46  ].
  47
  48 (* traduzione mcu+esadecimale → info *)
  49 (* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
  50 (* NB: per matchare una word (precode+code) bisogna passare una word *)
  51 (* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
  52 nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16) (param:list (aux_table_type m)) on param ≝
  53  match param with
  54   [ nil ⇒ None ?
  55   | cons hd tl ⇒
  56    match thd4T … hd with
  57     [ Byte b ⇒ match borw with
  58      [ Byte borw' ⇒ match eq_b8 borw' b with
  59       [ true ⇒ Some ? hd
  60       | false ⇒ full_info_of_word16_aux m borw tl ]
  61      | Word _ ⇒ full_info_of_word16_aux m borw tl ]
  62     | Word w ⇒ match borw with
  63      [ Byte _ ⇒ full_info_of_word16_aux m borw tl
  64      | Word borw' ⇒ match eq_w16 borw' w with
  65       [ true ⇒ Some ? hd
  66       | false ⇒ full_info_of_word16_aux m borw tl ]
  67     ]]].
  68
  69 ndefinition full_info_of_word16 ≝
  70 λm:mcu_type.λborw:byte8_or_word16.
  71 full_info_of_word16_aux m borw (opcode_table m).
  72
  73 (* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
  74 ninductive t_byte8 (m:mcu_type) : Type ≝
  75  TByte : byte8 → t_byte8 m.
  76
  77 ndefinition eq_tbyte8 ≝
  78 λm.λtb1,tb2:t_byte8 m.
  79  match tb1 with
  80   [ TByte b1 ⇒ match tb2 with
  81    [ TByte b2 ⇒ eq_b8 b1 b2 ]].