+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "freescale/memory_struct.ma".
-include "num/word16.ma".
-include "common/option.ma".
-include "common/list.ma".
-
-(* ********************* *)
-(* MEMORIA E DESCRITTORE *)
-(* ********************* *)
-
-(* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
-ndefinition mf_check_update_ranged ≝
-λf:word16 → memory_type.λinf.λsup.λv.
- λx.match inrange_w16 x inf sup 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, overflow se si supera 0xFFFF... *)
-nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (src:list byte8) (addr:word16) on src ≝
- match src with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ λx:word16.match eq_w16 addr x 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
- ]
- ].