]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/emulator/translation/translation_base.ma
some improvements and new lemmas for
[helm.git] / 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 ]].