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/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".
30 (* ********************************************** *)
31 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
32 (* ********************************************** *)
34 (* enumerazione delle ALU *)
35 ninductive mcu_type: Type ≝
42 ndefinition eq_mcutype ≝
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 ]
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
61 ndefinition aux_im_type ≝
62 λmcu:mcu_type.match mcu with
63 [ HC05 ⇒ Freescale_instr_mode
64 | HC08 ⇒ Freescale_instr_mode
65 | HCS08 ⇒ Freescale_instr_mode
66 | RS08 ⇒ Freescale_instr_mode
67 | IP2022 ⇒ IP2022_instr_mode
70 (* ********************************************* *)
71 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
72 (* ********************************************* *)
74 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
78 ndefinition pseudo_is_comparable: mcu_type → comparable.
80 @ (aux_pseudo_type mcu)
81 ##[ napply (match mcu return λmcu. aux_pseudo_type mcu with
82 [ HC05 ⇒ zeroc Freescalepseudo_is_comparable
83 | HC08 ⇒ zeroc Freescalepseudo_is_comparable
84 | HCS08 ⇒ zeroc Freescalepseudo_is_comparable
85 | RS08 ⇒ zeroc Freescalepseudo_is_comparable
86 | IP2022 ⇒ zeroc IP2022pseudo_is_comparable
88 | napply (match mcu return λmcu. (aux_pseudo_type mcu → bool) → bool with
89 [ HC05 ⇒ forallc Freescalepseudo_is_comparable
90 | HC08 ⇒ forallc Freescalepseudo_is_comparable
91 | HCS08 ⇒ forallc Freescalepseudo_is_comparable
92 | RS08 ⇒ forallc Freescalepseudo_is_comparable
93 | IP2022 ⇒ forallc IP2022pseudo_is_comparable
95 | napply (match mcu return λmcu. aux_pseudo_type mcu → aux_pseudo_type mcu → bool with
96 [ HC05 ⇒ eqc Freescalepseudo_is_comparable
97 | HC08 ⇒ eqc Freescalepseudo_is_comparable
98 | HCS08 ⇒ eqc Freescalepseudo_is_comparable
99 | RS08 ⇒ eqc Freescalepseudo_is_comparable
100 | IP2022 ⇒ eqc IP2022pseudo_is_comparable
102 |##*: ncases daemon ]
106 (* come suggerire di unificare?
107 carr (pseudo_is_comparable M) = aux_pseudo_type M *)
109 unification hint 0 ≔ MCU:mcu_type ⊢
110 carr (pseudo_is_comparable MCU) ≡ aux_pseudo_type MCU.
112 (* su tutta la lista quante volte compare lo pseudocodice *)
113 nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
116 | cons hd tl ⇒ match eqc ? o (fst4T … hd) with
117 [ true ⇒ get_pseudo_count m o (succc ? c) tl
118 | false ⇒ get_pseudo_count m o c tl