]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
mod change (-x)
[helm.git] / matita / matita / contribs / ng_assembly2 / emulator / opcodes / pseudo.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/Freescale_pseudo.ma".
24 include "emulator/opcodes/Freescale_instr_mode.ma".
25 include "emulator/opcodes/IP2022_pseudo.ma".
26 include "emulator/opcodes/IP2022_instr_mode.ma".
27 include "emulator/opcodes/byte_or_word.ma".
28 include "common/list.ma".
29
30 (* ********************************************** *)
31 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
32 (* ********************************************** *)
33
34 (* enumerazione delle ALU *)
35 ninductive mcu_type: Type ≝
36   HC05   : mcu_type
37 | HC08   : mcu_type
38 | HCS08  : mcu_type
39 | RS08   : mcu_type
40 | IP2022 : mcu_type.
41
42 ndefinition eq_mcutype ≝
43 λm1,m2:mcu_type.
44  match m1 with
45   [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
46   | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
47   | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
48   | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
49   | IP2022 ⇒ match m2 with [ IP2022 ⇒ true | _ ⇒ false ]
50   ].
51
52 ndefinition aux_pseudo_type ≝
53 λmcu:mcu_type.match mcu with
54  [ HC05 ⇒ Freescale_pseudo
55  | HC08 ⇒ Freescale_pseudo
56  | HCS08 ⇒ Freescale_pseudo
57  | RS08 ⇒ Freescale_pseudo
58  | IP2022 ⇒ IP2022_pseudo
59  ].
60
61 ndefinition pseudo_is_comparable: mcu_type → comparable.
62  #mcu; @ (aux_pseudo_type mcu)
63   ##[ nelim mcu;
64       ##[ ##1,2,3,4: napply (zeroc Freescalepseudo_is_comparable)
65       ##| ##5: napply (zeroc IP2022pseudo_is_comparable) ##]
66   ##| nelim mcu;
67       ##[ ##1,2,3,4: napply (forallc Freescalepseudo_is_comparable)
68       ##| ##5:  napply (forallc IP2022pseudo_is_comparable) ##]
69   ##| nelim mcu;
70       ##[ ##1,2,3,4: napply (eqc Freescalepseudo_is_comparable)
71       ##| ##5: napply (eqc IP2022pseudo_is_comparable) ##]
72   ##| nelim mcu;
73       ##[ ##1,2,3,4: napply (eqc_to_eq Freescalepseudo_is_comparable)
74       ##| ##5: napply (eqc_to_eq IP2022pseudo_is_comparable) ##]
75   ##| nelim mcu;
76       ##[ ##1,2,3,4: napply (eq_to_eqc Freescalepseudo_is_comparable)
77       ##| ##5: napply (eq_to_eqc IP2022pseudo_is_comparable) ##]
78   ##| nelim mcu;
79       ##[ ##1,2,3,4: napply (neqc_to_neq Freescalepseudo_is_comparable)
80       ##| ##5: napply (neqc_to_neq IP2022pseudo_is_comparable) ##]
81   ##| nelim mcu;
82       ##[ ##1,2,3,4: napply (neq_to_neqc Freescalepseudo_is_comparable)
83       ##| ##5: napply (neq_to_neqc IP2022pseudo_is_comparable) ##]
84   ##| nelim mcu;
85       ##[ ##1,2,3,4: napply (decidable_c Freescalepseudo_is_comparable)
86       ##| ##5: napply (decidable_c IP2022pseudo_is_comparable) ##]
87   ##| nelim mcu;
88       ##[ ##1,2,3,4: napply (symmetric_eqc Freescalepseudo_is_comparable)
89       ##| ##5: napply (symmetric_eqc IP2022pseudo_is_comparable) ##]
90   ##]
91 nqed.
92
93 unification hint 0 ≔ M:mcu_type ⊢ carr (pseudo_is_comparable M) ≡ aux_pseudo_type M.
94
95 ndefinition aux_im_type ≝
96 λmcu:mcu_type.match mcu with
97  [ HC05 ⇒ Freescale_instr_mode
98  | HC08 ⇒ Freescale_instr_mode
99  | HCS08 ⇒ Freescale_instr_mode
100  | RS08 ⇒ Freescale_instr_mode
101  | IP2022 ⇒ IP2022_instr_mode
102  ].
103
104 ndefinition im_is_comparable: mcu_type → comparable.
105  #mcu; @ (aux_im_type mcu)
106   ##[ nelim mcu;
107       ##[ ##1,2,3,4: napply (zeroc Freescaleim_is_comparable)
108       ##| ##5: napply (zeroc IP2022im_is_comparable) ##]
109   ##| nelim mcu;
110       ##[ ##1,2,3,4: napply (forallc Freescaleim_is_comparable)
111       ##| ##5:  napply (forallc IP2022im_is_comparable) ##]
112   ##| nelim mcu;
113       ##[ ##1,2,3,4: napply (eqc Freescaleim_is_comparable)
114       ##| ##5: napply (eqc IP2022im_is_comparable) ##]
115   ##| nelim mcu;
116       ##[ ##1,2,3,4: napply (eqc_to_eq Freescaleim_is_comparable)
117       ##| ##5: napply (eqc_to_eq IP2022im_is_comparable) ##]
118   ##| nelim mcu;
119       ##[ ##1,2,3,4: napply (eq_to_eqc Freescaleim_is_comparable)
120       ##| ##5: napply (eq_to_eqc IP2022im_is_comparable) ##]
121   ##| nelim mcu;
122       ##[ ##1,2,3,4: napply (neqc_to_neq Freescaleim_is_comparable)
123       ##| ##5: napply (neqc_to_neq IP2022im_is_comparable) ##]
124   ##| nelim mcu;
125       ##[ ##1,2,3,4: napply (neq_to_neqc Freescaleim_is_comparable)
126       ##| ##5: napply (neq_to_neqc IP2022im_is_comparable) ##]
127   ##| nelim mcu;
128       ##[ ##1,2,3,4: napply (decidable_c Freescaleim_is_comparable)
129       ##| ##5: napply (decidable_c IP2022im_is_comparable) ##]
130   ##| nelim mcu;
131       ##[ ##1,2,3,4: napply (symmetric_eqc Freescaleim_is_comparable)
132       ##| ##5: napply (symmetric_eqc IP2022im_is_comparable) ##]
133   ##]
134 nqed.
135
136 unification hint 0 ≔ M:mcu_type ⊢ carr (im_is_comparable M) ≡ aux_im_type M.
137
138 (* ********************************************* *)
139 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
140 (* ********************************************* *)
141
142 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 nat.
143
144 (* su tutta la lista quante volte compare il byte *)
145 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
146  match l with
147   [ nil ⇒ c
148   | cons hd tl ⇒ match thd4T … hd with
149    [ Byte b' ⇒ match eqc ? b b' with
150     [ true ⇒ get_byte_count m b (succc ? c) tl
151     | false ⇒ get_byte_count m b c tl
152     ]
153    | Word _ ⇒ get_byte_count m b c tl
154    ]
155   ].
156
157 (* su tutta la lista quante volte compare la word *)
158 nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
159  match l with
160   [ nil ⇒ c
161   | cons hd tl ⇒ match thd4T … hd with
162    [ Byte _ ⇒ get_word_count m w c tl
163    | Word w' ⇒ match eqc ? w w' with
164     [ true ⇒ get_word_count m w (succc ? c) tl
165     | false ⇒ get_word_count m w c tl
166     ]
167    ]
168   ].
169
170 (* su tutta la lista quante volte compare lo pseudocodice *)
171 nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
172  match l with
173   [ nil ⇒ c
174   | cons hd tl ⇒ match eqc ? o (fst4T … hd) with
175    [ true ⇒ get_pseudo_count m o (succc ? c) tl
176    | false ⇒ get_pseudo_count m o c tl
177    ]
178   ].
179
180 (* su tutta la lista quante volte compare la modalita' *)
181 nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
182  match l with
183   [ nil ⇒ c
184   | cons hd tl ⇒ match eqc ? i (snd4T … hd) with
185    [ true ⇒ get_mode_count m i (succc ? c) tl
186    | false ⇒ get_mode_count m i c tl
187    ]
188   ].
189
190 (* b e' non implementato? *)
191 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
192  match l with
193   [ nil ⇒ false
194   | cons hd tl ⇒ match eqc ? b hd with
195    [ true ⇒ true
196    | false ⇒ test_not_impl_byte b tl
197    ]
198   ].
199
200 (* su tutta la lista quante volte compare la coppia pseudo,instr_mode *)
201 nlet rec get_PsIm_count (m:mcu_type) (o:aux_pseudo_type m) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
202  match l with
203   [ nil ⇒ c
204   | cons hd tl ⇒
205    match (eqc ? o (fst4T … hd)) ⊗
206          (eqc ? i (snd4T … hd)) with
207     [ true ⇒ get_PsIm_count m o i (succc ? c) tl
208     | false ⇒ get_PsIm_count m o i c tl
209     ] 
210   ].
211
212 (* o e' non implementato? *)
213 nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_pseudo_type m) (l:list (aux_pseudo_type m)) on l ≝
214  match l with
215   [ nil ⇒ false
216   | cons hd tl ⇒ match eqc ? o hd with
217    [ true ⇒ true
218    | false ⇒ test_not_impl_pseudo m o tl
219    ]
220   ].
221
222 (* i e' non implementato? *)
223 nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
224  match l with
225   [ nil ⇒ false
226   | cons hd tl ⇒ match eqc ? i hd with
227    [ true ⇒ true
228    | false ⇒ test_not_impl_mode m i tl
229    ]
230   ].