X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fmemory%2Fmemory_trees.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fmemory%2Fmemory_trees.ma;h=b2f2a0d35de5e36ae5b2e9236cfe89997f725445;hb=a6501e81dc2cae2025841cefd502c220e01cd5d8;hp=0000000000000000000000000000000000000000;hpb=5683cf231fa2ac8abade3b70aea1af995cc04379;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma b/helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma new file mode 100755 index 000000000..b2f2a0d35 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/memory/memory_trees.ma @@ -0,0 +1,148 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "memory/memory_struct.ma". +include "num/word32.ma". +include "common/option.ma". +include "common/list.ma". + +(* ********************* *) +(* MEMORIA E DESCRITTORE *) +(* ********************* *) + +ndefinition aux_32B_filler ≝ +λT:Type.λel:T. +let lev8 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in +let lev7 ≝ mk_Array16T ? + lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8 + lev8 lev8 lev8 lev8 lev8 lev8 lev8 lev8 + in +let lev6 ≝ mk_Array16T ? + lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7 + lev7 lev7 lev7 lev7 lev7 lev7 lev7 lev7 + in +let lev5 ≝ mk_Array16T ? + lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6 + lev6 lev6 lev6 lev6 lev6 lev6 lev6 lev6 + in +let lev4 ≝ mk_Array16T ? + lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5 + lev5 lev5 lev5 lev5 lev5 lev5 lev5 lev5 + in +let lev3 ≝ mk_Array16T ? + lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 + lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 + in +let lev2 ≝ mk_Array16T ? + lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 + lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 + in +let lev1 ≝ mk_Array16T ? + lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 + lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 + in +lev1. + +ndefinition aux_32B_type ≝ +λT:Type.Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T (Array16T T))))))). + +(* tutta la memoria non installata *) +ndefinition mt_out_of_bound_memory ≝ aux_32B_filler ? MEM_OUT_OF_BOUND. + +(* tutta la memoria a 0 *) +ndefinition mt_zero_memory ≝ aux_32B_filler ? 〈x0,x0〉. + +(* visita di un albero da 4GB di elementi: ln16(4GB)=8 passaggi *) +ndefinition mt_visit ≝ +λT:Type.λdata:aux_32B_type T.λaddr:word32. + getn_array16T (b8l (w16l (w32l addr))) ? + (getn_array16T (b8h (w16l (w32l addr))) ? + (getn_array16T (b8l (w16h (w32l addr))) ? + (getn_array16T (b8h (w16h (w32l addr))) ? + (getn_array16T (b8l (w16l (w32h addr))) ? + (getn_array16T (b8h (w16l (w32h addr))) ? + (getn_array16T (b8l (w16h (w32h addr))) ? + (getn_array16T (b8h (w16h (w32h addr))) ? data))))))). + +(* scrittura di un elemento in un albero da 4GB *) +ndefinition mt_update ≝ +λT:Type.λdata:aux_32B_type T.λaddr:word32.λv:T. + let lev2 ≝ getn_array16T (b8h (w16h (w32h addr))) ? data in + let lev3 ≝ getn_array16T (b8l (w16h (w32h addr))) ? lev2 in + let lev4 ≝ getn_array16T (b8h (w16l (w32h addr))) ? lev3 in + let lev5 ≝ getn_array16T (b8l (w16l (w32h addr))) ? lev4 in + let lev6 ≝ getn_array16T (b8h (w16h (w32l addr))) ? lev5 in + let lev7 ≝ getn_array16T (b8l (w16h (w32l addr))) ? lev6 in + let lev8 ≝ getn_array16T (b8h (w16l (w32l addr))) ? lev7 in + + setn_array16T (b8h (w16h (w32h addr))) ? data + (setn_array16T (b8l (w16h (w32h addr))) ? lev2 + (setn_array16T (b8h (w16l (w32h addr))) ? lev3 + (setn_array16T (b8l (w16l (w32h addr))) ? lev4 + (setn_array16T (b8h (w16h (w32l addr))) ? lev5 + (setn_array16T (b8l (w16h (w32l addr))) ? lev6 + (setn_array16T (b8h (w16l (w32l addr))) ? lev7 + (setn_array16T (b8l (w16l (w32l addr))) T lev8 v))))))). + +(* scrittura di un range (max 64KB) in un albero da 4GB *) +nlet rec mt_update_ranged (T:Type) (data:aux_32B_type T) (addr:word32) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝ + match rw with + [ w16_O ⇒ data + | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data addr v) + (succ_w32 addr) w' rw' v + ]. + +(* scrivi controllando il tipo di memoria *) +ndefinition mt_mem_update ≝ +λmem:aux_32B_type byte8. +λchk:aux_32B_type memory_type. +λaddr:word32.λv:byte8. + match mt_visit ? chk addr 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:aux_32B_type byte8. +λchk:aux_32B_type memory_type. +λaddr:word32. + 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:aux_32B_type byte8) + (src:list byte8) (addr:word32) 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 (succ_w32 addr) + ].