matita/matita/contribs/ng_assembly/emulator/model/model.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/model/HC05_model.ma".
  24 include "emulator/model/HC08_model.ma".
  25 include "emulator/model/HCS08_model.ma".
  26 include "emulator/model/RS08_model.ma".
  27 include "emulator/model/IP2022_model.ma".
  28
  29 (* *********************************** *)
  30 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
  31 (* *********************************** *)
  32
  33 (* raggruppamento dei modelli *)
  34 ndefinition aux_model_type ≝
  35 λm:mcu_type.match m with
  36  [ HC05   ⇒ HC05_model
  37  | HC08   ⇒ HC08_model
  38  | HCS08  ⇒ HCS08_model
  39  | RS08   ⇒ RS08_model
  40  | IP2022 ⇒ IP2022_model
  41  ].
  42
  43 (* ∀modello.descrizione della memoria installata *)
  44 ndefinition memory_type_of_model ≝
  45 λm:mcu_type.
  46  match m
  47   return λm.aux_model_type m → ?
  48  with
  49  [ HC05   ⇒ memory_type_of_FamilyHC05
  50  | HC08   ⇒ memory_type_of_FamilyHC08
  51  | HCS08  ⇒ memory_type_of_FamilyHCS08
  52  | RS08   ⇒ memory_type_of_FamilyRS08
  53  | IP2022 ⇒ memory_type_of_FamilyIP2022
  54  ].
  55
  56 (* dato un modello costruisce un descrittore a partire dalla lista precedente *)
  57 nlet rec build_memory_type_of_model_aux t param (result:aux_chk_type t) on param ≝
  58  match param with
  59   [ nil ⇒ result
  60   | cons hd tl ⇒
  61    build_memory_type_of_model_aux t tl
  62     (check_update_ranged t result (fst3T ??? hd) (snd3T ??? hd) (thd3T ??? hd)) ].
  63
  64 ndefinition build_memory_type_of_model ≝
  65 λm:mcu_type.λmcu:aux_model_type m.λt:memory_impl.
  66  build_memory_type_of_model_aux t (memory_type_of_model m mcu) (out_of_bound_memory t).
  67
  68 ndefinition start_of_model ≝
  69 λm:mcu_type.
  70  match m
  71   return λm.aux_model_type m → ?
  72  with
  73  [ HC05   ⇒ start_of_model_HC05
  74  | HC08   ⇒ start_of_model_HC08
  75  | HCS08  ⇒ start_of_model_HCS08
  76  | RS08   ⇒ start_of_model_RS08
  77  | IP2022 ⇒ start_of_model_IP2022
  78  ].
  79
  80 ndefinition reset_of_model ≝
  81 λm:mcu_type.
  82  match m return λm.Πt.(any_status m t) → ? with
  83   [ HC05   ⇒ reset_of_model_HC05
  84   | HC08   ⇒ reset_of_model_HC08
  85   | HCS08  ⇒ reset_of_model_HCS08
  86   | RS08   ⇒ reset_of_model_RS08
  87   | IP2022 ⇒ reset_of_model_IP2022
  88   ].