helm/software/matita/contribs/ng_assembly/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 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
  68  ].
  69
  70 ndefinition eq_pseudo ≝
  71 λmcu:mcu_type.
  72  match mcu
  73   return λm.aux_pseudo_type m → aux_pseudo_type m → bool
  74  with
  75   [ HC05 ⇒ eq_Freescale_pseudo
  76   | HC08 ⇒ eq_Freescale_pseudo
  77   | HCS08 ⇒ eq_Freescale_pseudo
  78   | RS08 ⇒ eq_Freescale_pseudo
  79   | IP2022 ⇒ eq_IP2022_pseudo
  80   ].
  81
  82 ndefinition eq_im ≝
  83 λmcu:mcu_type.
  84  match mcu
  85   return λm.aux_im_type m → aux_im_type m → bool
  86  with
  87   [ HC05 ⇒ eq_Freescale_im
  88   | HC08 ⇒ eq_Freescale_im
  89   | HCS08 ⇒ eq_Freescale_im
  90   | RS08 ⇒ eq_Freescale_im
  91   | IP2022 ⇒ eq_IP2022_im
  92   ].
  93
  94 ndefinition forall_pseudo ≝
  95 λmcu:mcu_type.
  96  match mcu
  97   return λm.(aux_pseudo_type m → bool) → bool
  98  with
  99   [ HC05 ⇒ forall_Freescale_pseudo
 100   | HC08 ⇒ forall_Freescale_pseudo
 101   | HCS08 ⇒ forall_Freescale_pseudo
 102   | RS08 ⇒ forall_Freescale_pseudo
 103   | IP2022 ⇒ forall_IP2022_pseudo
 104   ].
 105
 106 ndefinition forall_im ≝
 107 λmcu:mcu_type.
 108  match mcu
 109   return λm.(aux_im_type m → bool) → bool
 110  with
 111   [ HC05 ⇒ forall_Freescale_im
 112   | HC08 ⇒ forall_Freescale_im
 113   | HCS08 ⇒ forall_Freescale_im
 114   | RS08 ⇒ forall_Freescale_im
 115   | IP2022 ⇒ forall_IP2022_im
 116   ].
 117
 118 (* ********************************************* *)
 119 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
 120 (* ********************************************* *)
 121
 122 ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
 123
 124 (* su tutta la lista quante volte compare il byte *)
 125 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝
 126  match l with
 127   [ nil ⇒ c
 128   | cons hd tl ⇒ match thd4T … hd with
 129    [ Byte b' ⇒ match eq_b8 b b' with
 130     [ true ⇒ get_byte_count m b (succ_w16 c) tl
 131     | false ⇒ get_byte_count m b c tl
 132     ]
 133    | Word _ ⇒ get_byte_count m b c tl
 134    ]
 135   ].
 136
 137 (* su tutta la lista quante volte compare la word *)
 138 nlet rec get_word_count (m:mcu_type) (w:word16) (c:word16) (l:list (aux_table_type m)) on l ≝
 139  match l with
 140   [ nil ⇒ c
 141   | cons hd tl ⇒ match thd4T … hd with
 142    [ Byte _ ⇒ get_word_count m w c tl
 143    | Word w' ⇒ match eq_w16 w w' with
 144     [ true ⇒ get_word_count m w (succ_w16 c) tl
 145     | false ⇒ get_word_count m w c tl
 146     ]
 147    ]
 148   ].
 149
 150 (* su tutta la lista quante volte compare lo pseudocodice *)
 151 nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
 152  match l with
 153   [ nil ⇒ c
 154   | cons hd tl ⇒ match eq_pseudo m o (fst4T … hd) with
 155    [ true ⇒ get_pseudo_count m o (succ_w16 c) tl
 156    | false ⇒ get_pseudo_count m o c tl
 157    ]
 158   ].
 159
 160 (* su tutta la lista quante volte compare la modalita' *)
 161 nlet rec get_mode_count (m:mcu_type) (i:aux_im_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
 162  match l with
 163   [ nil ⇒ c
 164   | cons hd tl ⇒ match eq_im m i (snd4T … hd) with
 165    [ true ⇒ get_mode_count m i (succ_w16 c) tl
 166    | false ⇒ get_mode_count m i c tl
 167    ]
 168   ].
 169
 170 (* b e' non implementato? *)
 171 nlet rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
 172  match l with
 173   [ nil ⇒ false
 174   | cons hd tl ⇒ match eq_b8 b hd with
 175    [ true ⇒ true
 176    | false ⇒ test_not_impl_byte b tl
 177    ]
 178   ].
 179
 180 (* su tutta la lista quante volte compare la coppia pseudo,instr_mode *)
 181 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 ≝
 182  match l with
 183   [ nil ⇒ c
 184   | cons hd tl ⇒
 185    match (eq_pseudo m o (fst4T … hd)) ⊗
 186          (eq_im m i (snd4T … hd)) with
 187     [ true ⇒ get_PsIm_count m o i (succ_w16 c) tl
 188     | false ⇒ get_PsIm_count m o i c tl
 189     ]
 190   ].
 191
 192 (* o e' non implementato? *)
 193 nlet rec test_not_impl_pseudo (m:mcu_type) (o:aux_pseudo_type m) (l:list (aux_pseudo_type m)) on l ≝
 194  match l with
 195   [ nil ⇒ false
 196   | cons hd tl ⇒ match eq_pseudo m o hd with
 197    [ true ⇒ true
 198    | false ⇒ test_not_impl_pseudo m o tl
 199    ]
 200   ].
 201
 202 (* i e' non implementato? *)
 203 nlet rec test_not_impl_mode (m:mcu_type) (i:aux_im_type m) (l:list (aux_im_type m)) on l ≝
 204  match l with
 205   [ nil ⇒ false
 206   | cons hd tl ⇒ match eq_im m i hd with
 207    [ true ⇒ true
 208    | false ⇒ test_not_impl_mode m i tl
 209    ]
 210   ].