+++ /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 *)
-(* ********************* *)
-
-(* tutta la memoria non installata *)
-ndefinition mt_out_of_bound_memory ≝
-let lev4 ≝ array_16T ?
- 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
- 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
- in
-let lev3 ≝ array_16T ?
- lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
- lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
- in
-let lev2 ≝ array_16T ?
- lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
- lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
- in
-let lev1 ≝ array_16T ?
- lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
- lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
- in
-lev1.
-
-(* tutta la memoria a 0 *)
-ndefinition mt_zero_memory ≝
-let lev4 ≝ array_16T ?
- (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
- (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
- (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
- (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
- in
-let lev3 ≝ array_16T ?
- lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
- lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
- in
-let lev2 ≝ array_16T ?
- lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
- lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
- in
-let lev1 ≝ array_16T ?
- lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
- lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
- in
-lev1.
-
-(* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *)
-ndefinition mt_visit ≝
-λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.
- match addr with
- [ mk_word16 wh wl ⇒
- getn_array16T (b8l wl) ?
- (getn_array16T (b8h wl) ?
- (getn_array16T (b8l wh) ?
- (getn_array16T (b8h wh) ? data))) ].
-
-(* scrittura di un elemento in un albero da 64KB *)
-ndefinition mt_update ≝
-λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.λv:T.
- match addr with
- [ mk_word16 wh wl ⇒
- let lev2 ≝ getn_array16T (b8h wh) ? data in
- let lev3 ≝ getn_array16T (b8l wh) ? lev2 in
- let lev4 ≝ getn_array16T (b8h wl) ? lev3 in
- setn_array16T (b8h wh) ? data
- (setn_array16T (b8l wh) ? lev2
- (setn_array16T (b8h wl) ? lev3
- (setn_array16T (b8l wl) T lev4 v))) ].
-
-(* scrittura di un range in un albero da 64KB *)
-ndefinition mt_update_ranged ≝
-λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λi,s:word16.λv:T.
- (* ok i≤s *)
- match le_w16 i s with
- [ true ⇒
- match i with
- [ mk_word16 ih il ⇒
- match s with
- [ mk_word16 sh sl ⇒
- let aux_4 ≝ Array16T T in
- let aux_3 ≝ Array16T (Array16T T) in
- let aux_2 ≝ Array16T (Array16T (Array16T T)) in
-
- let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in
- let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in
- let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in
-
- let slev2 ≝ getn_array16T (b8h sh) aux_2 data in
- let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in
- let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in
-
- let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in
- let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4
- vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in
- let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3
- vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in
-
- match eq_ex (b8h ih) (b8h sh) with
- [ true ⇒ match eq_ex (b8l ih) (b8l sh) with
- [ true ⇒ match eq_ex (b8h il) (b8h sl) with
- (* caso 0x...(X) a 0x...(Y) *)
- [ true ⇒ setn_array16T (b8h ih) aux_2 data
- (setn_array16T (b8l ih) aux_3 ilev2
- (setn_array16T (b8h il) aux_4 ilev3
- (* cambio a partire da livello 4 *)
- (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *)
- (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *)
- | false ⇒ setn_array16T (b8h ih) aux_2 data
- (setn_array16T (b8l ih) aux_3 ilev2
- (* cambio a partire da livello 3 *)
- (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *)
- (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *)
- (setn_array16T (b8h il) aux_4 ilev3
- (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *)
- vlev4)
- (setmn_array16T x0 (b8l sl) T slev4 v))) ]
- (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *)
- | false ⇒ setn_array16T (b8h ih) aux_2 data
- (* cambio a partire da livello 2 *)
- (setn_array16T (b8l sh) aux_3
- (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *)
- (setn_array16T (b8l ih) aux_3 ilev2
- (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *)
- (setn_array16T (b8h il) aux_4 ilev3
- (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *)
- vlev4))
- vlev3)
- (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *)
- (setn_array16T (b8h sl) aux_4 slev3
- (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *)
- vlev4))
- ]
- (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *)
- | false ⇒ setn_array16T (b8h sh) aux_2
- (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *)
- (setn_array16T (b8h ih) aux_2 data
- (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *)
- (setn_array16T (b8l ih) aux_3 ilev2
- (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *)
- (setn_array16T (b8h il) aux_4 ilev3
- (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *)
- vlev4))
- vlev3))
- vlev2)
- (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *)
- (setn_array16T (b8l sh) aux_3 slev2
- (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *)
- (setn_array16T (b8h sl) aux_4 slev3
- (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *)
- vlev4))
- vlev3) ]]]
- (* no i>s *)
- | false ⇒ data
- ].
-
-ndefinition mt_chk_get ≝
-λchk:Array16T (Array16T (Array16T (Array16T memory_type))).λaddr:word16.
- match mt_visit ? chk addr 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
- ].
-
-(* scrivi controllando il tipo di memoria *)
-ndefinition mt_mem_update ≝
-λmem:Array16T (Array16T (Array16T (Array16T byte8))).
-λchk:Array8T memory_type.
-λaddr:word16.λv:byte8.
- match getn_array8T o0 ? chk with
- (* ROM? ok, ma il valore viene perso *)
- [ MEM_READ_ONLY ⇒ Some ? mem
- (* RAM? ok *)
- | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
- (* NON INSTALLATA? no *)
- | MEM_OUT_OF_BOUND ⇒ None ? ].
-
-(* leggi controllando il tipo di memoria *)
-ndefinition mt_mem_read ≝
-λmem:Array16T (Array16T (Array16T (Array16T byte8))).
-λchk:Array16T (Array16T (Array16T (Array16T memory_type))).
-λaddr:word16.
- match mt_visit ? chk addr with
- [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
- | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
- | MEM_OUT_OF_BOUND ⇒ None ? ].
-
-(* ************************** *)
-(* CARICAMENTO PROGRAMMA/DATI *)
-(* ************************** *)
-
-(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
-nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8))))
- (src:list byte8) (addr:word16) on src ≝
- match src with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
- ].
projects / helm.git / blobdiff