]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma
freescale porting
[helm.git] / 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 include "emulator/translation/IP2022_translation.ma".
28
29 (* ******************************************************* *)
30 (* TRADUZIONE MCU+OPCODE+MODALITA'+ARGOMENTI → ESADECIMALE *)
31 (* ******************************************************* *)
32
33 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
34 ndefinition MA_check ≝
35 λmcu:mcu_type.
36  match mcu
37   return λm.(aux_im_type m) → Type
38  with
39   [ HC05 ⇒ HC05_MA_check
40   | HC08 ⇒ HC08_MA_check
41   | HCS08 ⇒ HCS08_MA_check
42   | RS08 ⇒ RS08_MA_check
43   | IP2022 ⇒ IP2022_MA_check
44   ].
45
46 (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param:
47    MA_check i → list (t_byte8 m) *)
48 ndefinition args_picker ≝
49 λmcu:mcu_type.
50  match mcu
51   return λm.Πi:(aux_im_type m).MA_check m i → ?
52  with
53   [ HC05 ⇒ HC05_args_picker
54   | HC08 ⇒ HC08_args_picker
55   | HCS08 ⇒ HCS08_args_picker
56   | RS08 ⇒ RS08_args_picker
57   | IP2022 ⇒ IP2022_args_picker
58   ].
59
60 (* trasformatore finale: mcu+opcode+instr_mode+args → list (t_byte8 m) *)
61 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)
62                                              (param:list (aux_table_type m)) on param ≝
63  match param with
64  [ nil ⇒ None ? | cons hd tl ⇒
65   match (eq_op m o (fst4T … hd)) ⊗ (eq_im m i (snd4T … hd)) with
66    [ true ⇒ match thd4T … hd with 
67     [ Byte isab ⇒ 
68      Some ? ([ (TByte m isab) ]@(args_picker m i p))
69     | Word isaw ⇒
70      Some ? ([ (TByte m (cnH ? isaw)) ; (TByte m (cnL ? isaw)) ]@(args_picker m i p))
71     ]
72    | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].
73
74 ndefinition bytes_of_pseudo_instr_mode_param ≝
75 λm:mcu_type.λo:aux_op_type m.λi:aux_im_type m.λp:MA_check m i.
76 bytes_of_pseudo_instr_mode_param_aux m o i p (opcode_table m).
77
78 (* ****************************** *)
79 (* APPROCCIO COMPILAZIONE AL VOLO *)
80 (* ****************************** *)
81
82 (* ausiliario di compile *)
83 ndefinition defined_option ≝
84  λT:Type.λo:option T.
85   match o with
86    [ None ⇒ False
87    | Some _ ⇒ True
88    ].
89
90 (* compila solo se l'intera istruzione+modalita'+argomenti ha riscontro nelle tabelle *)
91 ndefinition compile ≝
92 λmcu:mcu_type.λi:aux_im_type mcu.λop:aux_op_type mcu.λarg:MA_check mcu i.
93  match bytes_of_pseudo_instr_mode_param mcu op i arg
94   return λres:option ?.defined_option ? res → ?
95  with
96   [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p
97   | Some x ⇒ λp:defined_option ? (Some ? x).x
98   ].
99
100 (* detipatore del compilato: (t_byte8 m) → byte8 *)
101 nlet rec source_to_byte8_aux (m:mcu_type) (p2:list byte8) (p1:list (t_byte8 m))  on p1 ≝
102  match p1 with
103   [ nil ⇒ p2
104   | cons hd tl ⇒ match hd with [ TByte b ⇒ source_to_byte8_aux m (p2@[b]) tl ]
105   ].
106
107 ndefinition source_to_byte8 ≝ λm:mcu_type.source_to_byte8_aux m [].