X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fmodel%2Fmodel.ma;fp=matitaB%2Fmatita%2Fcontribs%2Fng_assembly2%2Femulator%2Fmodel%2Fmodel.ma;h=e730ced1707e7fb0d3c92e3dc9a5f01bd2d810d5;hb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;hp=0000000000000000000000000000000000000000;hpb=f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2;p=helm.git

diff --git a/matitaB/matita/contribs/ng_assembly2/emulator/model/model.ma b/matitaB/matita/contribs/ng_assembly2/emulator/model/model.ma
new file mode 100755
index 000000000..e730ced17
--- /dev/null
+++ b/matitaB/matita/contribs/ng_assembly2/emulator/model/model.ma
@@ -0,0 +1,89 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(*                          Progetto FreeScale                            *)
+(*                                                                        *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Sviluppo: 2008-2010                                                  *)
+(*                                                                        *)
+(* ********************************************************************** *)
+
+include "emulator/model/HC05_model.ma".
+include "emulator/model/HC08_model.ma".
+include "emulator/model/HCS08_model.ma".
+include "emulator/model/RS08_model.ma".
+include "emulator/model/IP2022_model.ma".
+
+(* *********************************** *)
+(* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
+(* *********************************** *)
+
+(* raggruppamento dei modelli *)
+ndefinition aux_model_type ≝
+λm:mcu_type.match m with
+ [ HC05   ⇒ HC05_model
+ | HC08   ⇒ HC08_model
+ | HCS08  ⇒ HCS08_model
+ | RS08   ⇒ RS08_model
+ | IP2022 ⇒ IP2022_model
+ ].
+
+(* ∀modello.descrizione della memoria installata *)
+ndefinition memory_type_of_model ≝
+λm:mcu_type.
+ match m
+  return λm.aux_model_type m → ?
+ with
+ [ HC05   ⇒ memory_type_of_FamilyHC05
+ | HC08   ⇒ memory_type_of_FamilyHC08
+ | HCS08  ⇒ memory_type_of_FamilyHCS08
+ | RS08   ⇒ memory_type_of_FamilyRS08
+ | IP2022 ⇒ memory_type_of_FamilyIP2022
+ ].
+
+(* dato un modello costruisce un descrittore a partire dalla lista precedente *)
+nlet rec build_memory_type_of_model_aux t param (result:aux_chk_type t) on param ≝
+ match param with
+  [ nil ⇒ result
+  | cons hd tl ⇒ 
+   build_memory_type_of_model_aux t tl
+    (check_update_ranged t result (fst4T … hd) (snd4T … hd)
+                                  (thd4T … hd) (fth4T … hd)) ].
+
+ndefinition build_memory_type_of_model ≝
+λm:mcu_type.λmcu:aux_model_type m.λt:memory_impl.
+ build_memory_type_of_model_aux t (memory_type_of_model m mcu) (out_of_bound_memory t).
+
+ndefinition start_of_model ≝
+λm:mcu_type.
+ match m
+  return λm.aux_model_type m → ?
+ with
+ [ HC05   ⇒ start_of_model_HC05
+ | HC08   ⇒ start_of_model_HC08
+ | HCS08  ⇒ start_of_model_HCS08
+ | RS08   ⇒ start_of_model_RS08
+ | IP2022 ⇒ start_of_model_IP2022
+ ].
+
+ndefinition reset_of_model ≝
+λm:mcu_type.
+ match m return λm.Πt.(any_status m t) → ? with
+  [ HC05   ⇒ reset_of_model_HC05
+  | HC08   ⇒ reset_of_model_HC08
+  | HCS08  ⇒ reset_of_model_HCS08
+  | RS08   ⇒ reset_of_model_RS08
+  | IP2022 ⇒ reset_of_model_IP2022
+  ].