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.
76 ndefinition pseudo_is_comparable ≝
77 λmcu:mcu_type.match mcu with
78 [ HC05 ⇒ Freescalepseudo_is_comparable
79 | HC08 ⇒ Freescalepseudo_is_comparable
80 | HCS08 ⇒ Freescalepseudo_is_comparable
81 | RS08 ⇒ Freescalepseudo_is_comparable
82 | IP2022 ⇒ IP2022pseudo_is_comparable
85 (* come suggerire di unificare?
86 carr (pseudo_is_comparable M) = aux_pseudo_type M *)
88 (* su tutta la lista quante volte compare lo pseudocodice *)
89 nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
92 | cons hd tl ⇒ match eqc ? o (fst4T … hd) with
93 [ true ⇒ get_pseudo_count m o (succc ? c) tl
94 | false ⇒ get_pseudo_count m o c tl