helm/software/matita/contribs/ng_assembly/emulator/translation/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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/translation/HC05_translation.ma".
  24 include "emulator/translation/HC08_translation.ma".
  25 include "emulator/translation/HCS08_translation.ma".
  26 include "emulator/translation/RS08_translation.ma".
  27
  28 (* ******************************************************* *)
  29 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
  30 (* ******************************************************* *)
  31
  32 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
  33 ndefinition MA_check ≝
  34 λmcu:mcu_type.
  35  match mcu
  36   return λm.(aux_im_type m) → Type
  37  with
  38   [ HC05 ⇒ HC05_MA_check
  39   | HC08 ⇒ HC08_MA_check
  40   | HCS08 ⇒ HCS08_MA_check
  41   | RS08 ⇒ RS08_MA_check
  42   ].
  43
  44 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
  45    MA_check i → list (t_byte8 m) *)
  46 ndefinition args_picker ≝
  47 λmcu:mcu_type.
  48  match mcu
  49   return λm.Πi:(aux_im_type m).MA_check m i → ?
  50  with
  51   [ HC05 ⇒ HC05_args_picker
  52   | HC08 ⇒ HC08_args_picker
  53   | HCS08 ⇒ HCS08_args_picker
  54   | RS08 ⇒ RS08_args_picker
  55   ].
  56
  57 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
  58 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)
  59                                              (param:list (aux_table_type m)) on param ≝
  60  match param with
  61  [ nil ⇒ None ? | cons hd tl ⇒
  62   match (eq_op m o (fst4T … hd)) ⊗ (eq_im m i (snd4T … hd)) with
  63    [ true ⇒ match thd4T … hd with
  64     [ Byte isab ⇒
  65      Some ? ([ (TByte m isab) ]@(args_picker m i p))
  66     | Word isaw ⇒
  67      Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p))
  68     ]
  69    | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
  70
  71 ndefinition bytes_of_pseudo_instr_mode_param ≝
  72 λm:mcu_type.λo:aux_op_type m.λi:aux_im_type m.λp:MA_check m i.
  73 bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
  74
  75 (* ****************************** *)
  76 (* APPROCCIO COMPILAZIONE AL VOLO *)
  77 (* ****************************** *)
  78
  79 (* ausiliario di compile *)
  80 ndefinition defined_option ≝
  81  λT:Type.λo:option T.
  82   match o with
  83    [ None ⇒ False
  84    | Some _ ⇒ True
  85    ].
  86
  87 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
  88 ndefinition compile ≝
  89 λmcu:mcu_type.λi:aux_im_type mcu.λop:aux_op_type mcu.λarg:MA_check mcu i.
  90  match bytes_of_pseudo_instr_mode_param mcu op i arg
  91   return λres:option ?.defined_option ? res → ?
  92  with
  93   [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
  94   | Some x ⇒ λp:defined_option ? (Some ? x).x
  95   ].
  96
  97 (* detipatore del compilato: (t_byte8 m) → byte8 *)
  98 nlet rec source_to_byte8_HC05_aux (p1:list (t_byte8 HC05)) (p2:list byte8) ≝
  99  match p1 with
 100   [ nil ⇒ p2
 101   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC05_aux tl (p2@[b]) ]
 102   ].
 103
 104 nlet rec source_to_byte8_HC08_aux (p1:list (t_byte8 HC08)) (p2:list byte8) ≝
 105  match p1 with
 106   [ nil ⇒ p2
 107   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HC08_aux tl (p2@[b]) ]
 108   ].
 109
 110 nlet rec source_to_byte8_HCS08_aux (p1:list (t_byte8 HCS08)) (p2:list byte8) ≝
 111  match p1 with
 112   [ nil ⇒ p2
 113   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_HCS08_aux tl (p2@[b]) ]
 114   ].
 115
 116 nlet rec source_to_byte8_RS08_aux (p1:list (t_byte8 RS08)) (p2:list byte8) ≝
 117  match p1 with
 118   [ nil ⇒ p2
 119   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_RS08_aux tl (p2@[b]) ]
 120   ].
 121
 122 ndefinition source_to_byte8 ≝
 123 λm:mcu_type.
 124  match m
 125   return λm:mcu_type.list (t_byte8 m) → list byte8
 126  with
 127   [ HC05 ⇒ λl:list (t_byte8 HC05).source_to_byte8_HC05_aux l []
 128   | HC08 ⇒ λl:list (t_byte8 HC08).source_to_byte8_HC08_aux l []
 129   | HCS08 ⇒ λl:list (t_byte8 HCS08).source_to_byte8_HCS08_aux l []
 130   | RS08 ⇒ λl:list (t_byte8 RS08).source_to_byte8_RS08_aux l []
 131   ].