helm/software/matita/contribs/ng_assembly2/emulator/memory/memory_trees.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/memory/memory_base.ma".
  24 include "emulator/memory/memory_struct.ma".
  25 include "num/word32.ma".
  26 include "common/list.ma".
  27
  28 (* ************************** *)
  29 (* 8 segmenti da 64Kb → 512Kb *)
  30 (* 4 + 16 bit indirizzo       *)
  31 (* ************************** *)
  32
  33 (* ********************* *)
  34 (* MEMORIA E DESCRITTORE *)
  35 (* ********************* *)
  36
  37 ndefinition aux_20B_filler ≝
  38 λT:Type.λel:T.
  39 let lev4 ≝ mk_Array16T T el el el el el el el el el el el el el el el el in
  40 let lev3 ≝ mk_Array16T ?
  41            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  42            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4 in
  43 let lev2 ≝ mk_Array16T ?
  44            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  45            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3 in
  46 let lev1 ≝ mk_Array16T ?
  47            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  48            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 in
  49 let lev0 ≝ mk_Array8T ?
  50            lev1 lev1 lev1 lev1 lev1 lev1 lev1 lev1
  51            in
  52 lev0.
  53
  54 ndefinition aux_20B_type ≝
  55 λT:Type.Array8T (Array16T (Array16T (Array16T (Array16T T)))).
  56
  57 (* tutta la memoria non installata *)
  58 ndefinition mt_out_of_bound_memory ≝ aux_20B_filler ? MEM_OUT_OF_BOUND.
  59
  60 (* tutta la memoria a 0 *)
  61 ndefinition mt_zero_memory ≝ aux_20B_filler ? 〈x0,x0〉.
  62
  63 (* visita di un albero da 512Kb di elementi: ln16(512Kb)=5 passaggi *)
  64 ndefinition mt_visit ≝
  65 λT:Type.λdata:aux_20B_type T.λsel:oct.λaddr:word16.
  66  getn_array16T (cnL ? (cnL ? addr)) ?
  67   (getn_array16T (cnH ? (cnL ? addr)) ?
  68    (getn_array16T (cnL ? (cnH ? addr)) ?
  69     (getn_array16T (cnH ? (cnH ? addr)) ?
  70      (getn_array8T sel ? data)))).
  71
  72 (* scrittura di un elemento in un albero da 512Kb *)
  73 ndefinition mt_update ≝
  74 λT:Type.λdata:aux_20B_type T.λsel:oct.λaddr:word16.λv:T.
  75  let lev1 ≝ getn_array8T sel ? data in
  76  let lev2 ≝ getn_array16T (cnH ? (cnH ? addr)) ? lev1 in
  77  let lev3 ≝ getn_array16T (cnL ? (cnH ? addr)) ? lev2 in
  78  let lev4 ≝ getn_array16T (cnH ? (cnL ? addr)) ? lev3 in
  79  setn_array8T sel ? data
  80   (setn_array16T (cnH ? (cnH ? addr)) ? lev1
  81    (setn_array16T (cnL ? (cnH ? addr)) ? lev2
  82     (setn_array16T (cnH ? (cnL ? addr)) ? lev3
  83      (setn_array16T (cnL ? (cnL ? addr)) T lev4 v)))).
  84
  85 (* scrittura di un segmento (max 64Kb) degli otto disponibili *)
  86 nlet rec mt_update_ranged (T:Type) (data:aux_20B_type T) (sel:oct) (addr:word16) (w:word16) (rw:rec_word16 w) (v:T) on rw ≝
  87  match rw with
  88   [ w16_O ⇒ data
  89   | w16_S w' rw' ⇒ mt_update_ranged T (mt_update T data sel addr v)
  90                                       sel (succc ? addr) w' rw' v
  91   ].
  92
  93 (* scrivi controllando il tipo di memoria *)
  94 ndefinition mt_mem_update ≝
  95 λmem:aux_20B_type byte8.
  96 λchk:aux_20B_type memory_type.
  97 λsel:oct.λaddr:word16.λv:byte8.
  98  match mt_visit ? chk sel addr with
  99   (* ROM? ok, ma il valore viene perso *)
 100   [ MEM_READ_ONLY ⇒ Some ? mem
 101   (* RAM? ok *)
 102   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem sel addr v)
 103   (* NON INSTALLATA? no *)
 104   | MEM_OUT_OF_BOUND ⇒ None ? ].
 105
 106 (* leggi controllando il tipo di memoria *)
 107 ndefinition mt_mem_read ≝
 108 λmem:aux_20B_type byte8.
 109 λchk:aux_20B_type memory_type.
 110 λsel:oct.λaddr:word16.
 111  match mt_visit ? chk sel addr with
 112   [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem sel addr)
 113   | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem sel addr)
 114   | MEM_OUT_OF_BOUND ⇒ None ? ].
 115
 116 (* ************************** *)
 117 (* CARICAMENTO PROGRAMMA/DATI *)
 118 (* ************************** *)
 119
 120 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
 121 nlet rec mt_load_from_source_at (old_mem:aux_20B_type byte8)
 122                                 (src:list byte8) (sel:oct) (addr:word16) on src ≝
 123  match src with
 124   (* fine di source: carica da old_mem *)
 125   [ nil ⇒ old_mem
 126   | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem sel addr hd)
 127                                         tl sel (succc ? addr)
 128   ].