helm/software/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   ].