helm/software/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/opcode.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
  30 (* ***************************** *)
  31 (* TRADUZIONE ESADECIMALE → INFO *)
  32 (* ***************************** *)
  33
  34 (* accesso alla tabella della ALU prescelta *)
  35 ndefinition opcode_table ≝
  36 λm:mcu_type.
  37  match m
  38   return λm:mcu_type.list (aux_table_type m)
  39  with
  40   [ HC05  ⇒ opcode_table_HC05
  41   | HC08  ⇒ opcode_table_HC08
  42   | HCS08 ⇒ opcode_table_HCS08
  43   | RS08  ⇒ opcode_table_RS08
  44  ].
  45
  46 (* traduzione mcu+esadecimale → info *)
  47 (* NB: la ricerca per byte non matcha con una word con lo stesso byte superiore uguale *)
  48 (* NB: per matchare una word (precode+code) bisogna passare una word *)
  49 (* NB: il risultato e' sempre un'opzione, NON esiste un dummy opcode tipo UNKNOWN/ILLEGAL *)
  50 nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16) (param:list (aux_table_type m)) 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 (* introduzione di un tipo byte8 dipendente dall'mcu_type (phantom type) *)
  72 ninductive t_byte8 (m:mcu_type) : Type ≝
  73  TByte : byte8 → t_byte8 m.
  74
  75 ndefinition eq_tbyte8 ≝
  76 λm.λtb1,tb2:t_byte8 m.
  77  match tb1 with
  78   [ TByte b1 ⇒ match tb2 with
  79    [ TByte b2 ⇒ eq_b8 b1 b2 ]].