freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / memory_func.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
new file mode 100755 (executable)
index 0000000..be27f55
--- /dev/null
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_func.ma
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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:                                                         *)
+(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*                                                                        *)
+(* Questo materiale fa parte della tesi:                                  *)
+(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
+(*                                                                        *)
+(*                    data ultima modifica 15/11/2007                     *)
+(* ********************************************************************** *)
+
+include "freescale/memory_struct.ma".
+include "freescale/word16.ma".
+include "freescale/option.ma".
+include "freescale/theory.ma".
+
+(* ********************* *)
+(* MEMORIA E DESCRITTORE *)
+(* ********************* *)
+
+(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
+ndefinition mf_check_update_ranged ≝
+λf:word16 → memory_type.λi.λs.λv.
+ λx.match in_range x i s with
+  [ true ⇒ v
+  | false ⇒ f x ].
+
+(* tutta la memoria non installata *)
+ndefinition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND.
+
+ndefinition mf_chk_get ≝
+λc:word16 → memory_type.λa:word16.
+ match c a with
+  [ MEM_READ_ONLY ⇒ array_8T ? MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY MEM_READ_ONLY
+  | MEM_READ_WRITE ⇒ array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE
+  | MEM_OUT_OF_BOUND ⇒ array_8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
+  ].
+
+(* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
+ndefinition mf_mem_update ≝
+λf:word16 → byte8.λc:Array8T memory_type.λa:word16.λv:byte8.
+ match getn_array8T o0 ? c with
+  (* ROM? ok, ma il valore viene perso *)
+  [ MEM_READ_ONLY ⇒ Some ? f
+  (* RAM? ok *)
+  | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w16 x a with [ true ⇒ v | false ⇒ f x ])
+  (* NON INSTALLATA? no *)
+  | MEM_OUT_OF_BOUND ⇒ None ? ].  
+
+(* tutta la memoria a 0 *)
+ndefinition mf_zero_memory ≝ λ_:word16.〈x0,x0〉.
+
+(* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
+ndefinition mf_mem_read ≝
+λf:word16 → byte8.λc:word16 → memory_type.λa.
+ match c a with
+  [ MEM_READ_ONLY ⇒ Some ? (f a)
+  | MEM_READ_WRITE ⇒ Some ? (f a)
+  | MEM_OUT_OF_BOUND ⇒ None ? ].
+
+(* ************************** *)
+(* CARICAMENTO PROGRAMMA/DATI *)
+(* ************************** *)
+
+(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
+nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
+match source with
+ (* fine di source: carica da old_mem *)
+ [ nil ⇒ old_mem
+ | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
+  (* e' prima di source: carica da old_mem *)
+  [ true ⇒ old_mem x
+  | false ⇒ match eq_w16 x addr with
+   (* la locazione corrisponde al punto corrente di source *)
+   [ true ⇒ hd
+   (* la locazione e' piu' avanti: ricorsione *)
+   | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)) x
+   ]
+  ]
+ ].