1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
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".
30 (* ***************************** *)
31 (* TRADUZIONE ESADECIMALE → INFO *)
32 (* ***************************** *)
34 (* accesso alla tabella della ALU prescelta *)
35 ndefinition opcode_table ≝
38 return λm:mcu_type.list (aux_table_type m)
40 [ HC05 ⇒ opcode_table_HC05
41 | HC08 ⇒ opcode_table_HC08
42 | HCS08 ⇒ opcode_table_HCS08
43 | RS08 ⇒ opcode_table_RS08
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 ≝
55 [ Byte b ⇒ match borw with
56 [ Byte borw' ⇒ match eq_b8 borw' b with
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
64 | false ⇒ full_info_of_word16_aux m borw tl ]
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).
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.
75 ndefinition eq_tbyte8 ≝
76 λm.λtb1,tb2:t_byte8 m.
78 [ TByte b1 ⇒ match tb2 with
79 [ TByte b2 ⇒ eq_b8 b1 b2 ]].