helm/software/matita/contribs/ng_assembly/freescale/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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/memory_struct.ma".
  24 include "num/word16.ma".
  25 include "common/option.ma".
  26 include "common/list.ma".
  27
  28 (* ********************* *)
  29 (* MEMORIA E DESCRITTORE *)
  30 (* ********************* *)
  31
  32 (* tutta la memoria non installata *)
  33 ndefinition mt_out_of_bound_memory ≝
  34 let lev4 ≝ array_16T ?
  35            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  36            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  37            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  38            MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  39            in
  40 let lev3 ≝ array_16T ?
  41            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  42            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  43            in
  44 let lev2 ≝ array_16T ?
  45            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  46            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  47            in
  48 let lev1 ≝ array_16T ?
  49            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  50            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  51            in
  52 lev1.
  53
  54 (* tutta la memoria a 0 *)
  55 ndefinition mt_zero_memory ≝
  56 let lev4 ≝ array_16T ?
  57            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  58            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  59            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  60            (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0) (mk_byte8 x0 x0)
  61            in
  62 let lev3 ≝ array_16T ?
  63            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  64            lev4 lev4 lev4 lev4 lev4 lev4 lev4 lev4
  65            in
  66 let lev2 ≝ array_16T ?
  67            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  68            lev3 lev3 lev3 lev3 lev3 lev3 lev3 lev3
  69            in
  70 let lev1 ≝ array_16T ?
  71            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  72            lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2
  73            in
  74 lev1.
  75
  76 (* visita di un albero da 64KB di elementi: ln16(65536)=4 passaggi *)
  77 ndefinition mt_visit ≝
  78 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.
  79  match addr with
  80   [ mk_word16 wh wl ⇒
  81  getn_array16T (b8l wl) ?
  82   (getn_array16T (b8h wl) ?
  83    (getn_array16T (b8l wh) ?
  84     (getn_array16T (b8h wh) ? data))) ].
  85
  86 (* scrittura di un elemento in un albero da 64KB *)
  87 ndefinition mt_update ≝
  88 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λaddr:word16.λv:T.
  89  match addr with
  90   [ mk_word16 wh wl ⇒
  91  let lev2 ≝ getn_array16T (b8h wh) ? data in
  92  let lev3 ≝ getn_array16T (b8l wh) ? lev2 in
  93  let lev4 ≝ getn_array16T (b8h wl) ? lev3 in
  94  setn_array16T (b8h wh) ? data
  95   (setn_array16T (b8l wh) ? lev2
  96    (setn_array16T (b8h wl) ? lev3
  97     (setn_array16T (b8l wl) T lev4 v))) ].
  98
  99 (* scrittura di un range in un albero da 64KB *)
 100 ndefinition mt_update_ranged ≝
 101 λT:Type.λdata:Array16T (Array16T (Array16T (Array16T T))).λi,s:word16.λv:T.
 102  (* ok i≤s *)
 103  match le_w16 i s with
 104   [ true ⇒
 105  match i with
 106   [ mk_word16 ih il ⇒
 107  match s with
 108   [ mk_word16 sh sl ⇒
 109  let aux_4 ≝ Array16T T in
 110  let aux_3 ≝ Array16T (Array16T T) in
 111  let aux_2 ≝ Array16T (Array16T (Array16T T)) in
 112
 113  let ilev2 ≝ getn_array16T (b8h ih) aux_2 data in
 114  let ilev3 ≝ getn_array16T (b8l ih) aux_3 ilev2 in
 115  let ilev4 ≝ getn_array16T (b8h il) aux_4 ilev3 in
 116
 117  let slev2 ≝ getn_array16T (b8h sh) aux_2 data in
 118  let slev3 ≝ getn_array16T (b8l sh) aux_3 slev2 in
 119  let slev4 ≝ getn_array16T (b8h sl) aux_4 slev3 in
 120
 121  let vlev4 ≝ array_16T T v v v v v v v v v v v v v v v v in
 122  let vlev3 ≝ array_16T aux_4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4
 123                              vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 vlev4 in
 124  let vlev2 ≝ array_16T aux_3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3
 125                              vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 vlev3 in
 126
 127  match eq_ex (b8h ih) (b8h sh) with
 128   [ true ⇒ match eq_ex (b8l ih) (b8l sh) with
 129    [ true ⇒ match eq_ex (b8h il) (b8h sl) with
 130     (* caso 0x...(X) a 0x...(Y) *)
 131     [ true ⇒ setn_array16T (b8h ih) aux_2 data
 132               (setn_array16T (b8l ih) aux_3 ilev2
 133                (setn_array16T (b8h il) aux_4 ilev3
 134                 (* cambio a partire da livello 4 *)
 135                 (setmn_array16T (b8l il) (b8l sl) T ilev4 v))) (* ...X,...Y *)
 136     (* caso 0x..(X1)(X2) a 0x..(Y1)(Y2) *)
 137     | false ⇒ setn_array16T (b8h ih) aux_2 data
 138                (setn_array16T (b8l ih) aux_3 ilev2
 139                 (* cambio a partire da livello 3 *)
 140                 (setn_array16T (b8h sl) aux_4 (* ..(Y1)0,..(Y1)(Y2) *)
 141                  (setmn_array16T_succ_pred (b8h il) (b8h sl) aux_4 (* ..(X1+1).,..(Y1-1). *)
 142                   (setn_array16T (b8h il) aux_4 ilev3
 143                    (setmn_array16T (b8l il) xF T ilev4 v)) (* ..(X1)(X2),..(X1)F *)
 144                   vlev4)
 145                  (setmn_array16T x0 (b8l sl) T slev4 v))) ]
 146    (* caso 0x.(X1)(X2)(X3) a 0x..(Y1)(Y2)(Y3) *)
 147    | false ⇒ setn_array16T (b8h ih) aux_2 data
 148               (* cambio a partire da livello 2 *)
 149               (setn_array16T (b8l sh) aux_3
 150                (setmn_array16T_succ_pred (b8l ih) (b8l sh) aux_3 (* .(X1+1)..,.(Y1-1).. *)
 151                 (setn_array16T (b8l ih) aux_3 ilev2
 152                  (setmn_array16T_succ (b8h il) aux_4 (* .(X1)(X2+1).,.(X1)F. *)
 153                   (setn_array16T (b8h il) aux_4 ilev3
 154                    (setmn_array16T (b8l il) xF T ilev4 v)) (* .(X1)(X2)(X3),.(X1)(X2)F *)
 155                   vlev4))
 156                 vlev3)
 157                (setmn_array16T_pred (b8h sl) aux_4 (* .(Y1)0.,.(Y1)(Y2-1). *)
 158                 (setn_array16T (b8h sl) aux_4 slev3
 159                  (setmn_array16T x0 (b8l sl) T slev4 v)) (* .(Y1)(Y2)0,.(Y1)(Y2)(Y3) *)
 160                 vlev4))
 161    ]
 162   (* caso 0x(X1)(X2)(X3)(X4) a 0x(Y1)(Y2)(Y3)(Y4) *)
 163   | false ⇒ setn_array16T (b8h sh) aux_2
 164              (setmn_array16T_succ_pred (b8h ih) (b8h sh) aux_2 (* (X+1)...,(Y-1)... *)
 165               (setn_array16T (b8h ih) aux_2 data
 166                (setmn_array16T_succ (b8l ih) aux_3 (* (X1)(X2+1)..,(X1)F.. *)
 167                 (setn_array16T (b8l ih) aux_3 ilev2
 168                  (setmn_array16T_succ (b8h il) aux_4 (* (X1)(X2)(X3+1).,(X1)(X2)F. *)
 169                   (setn_array16T (b8h il) aux_4 ilev3
 170                    (setmn_array16T (b8l il) xF T ilev4 v)) (* (X1)(X2)(X3)(X4),(X1)(X2)(X3)F *)
 171                   vlev4))
 172                 vlev3))
 173                vlev2)
 174              (setmn_array16T_pred (b8l sh) aux_3 (* (Y1)0..,(Y1)(Y2-1).. *)
 175               (setn_array16T (b8l sh) aux_3 slev2
 176                (setmn_array16T_pred (b8h sl) aux_4 (* (Y1)(Y2)0.,(Y1)(Y2)(Y3-1). *)
 177                 (setn_array16T (b8h sl) aux_4 slev3
 178                  (setmn_array16T x0 (b8l sl) T slev4 v)) (* (Y1)(Y2)(Y3)0,(Y1)(Y2)(Y3)(Y4) *)
 179                 vlev4))
 180               vlev3) ]]]
 181  (* no i>s *)
 182  | false ⇒ data
 183  ].
 184
 185 ndefinition mt_chk_get ≝
 186 λchk:Array16T (Array16T (Array16T (Array16T memory_type))).λaddr:word16.
 187  match mt_visit ? chk addr with
 188  [ 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
 189  | 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
 190  | 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
 191  ].
 192
 193 (* scrivi controllando il tipo di memoria *)
 194 ndefinition mt_mem_update ≝
 195 λmem:Array16T (Array16T (Array16T (Array16T byte8))).
 196 λchk:Array8T memory_type.
 197 λaddr:word16.λv:byte8.
 198  match getn_array8T o0 ? chk with
 199   (* ROM? ok, ma il valore viene perso *)
 200   [ MEM_READ_ONLY ⇒ Some ? mem
 201   (* RAM? ok *)
 202   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem addr v)
 203   (* NON INSTALLATA? no *)
 204   | MEM_OUT_OF_BOUND ⇒ None ? ].
 205
 206 (* leggi controllando il tipo di memoria *)
 207 ndefinition mt_mem_read ≝
 208 λmem:Array16T (Array16T (Array16T (Array16T byte8))).
 209 λchk:Array16T (Array16T (Array16T (Array16T memory_type))).
 210 λaddr:word16.
 211  match  mt_visit ? chk addr with
 212   [ MEM_READ_ONLY ⇒ Some ? (mt_visit ? mem addr)
 213   | MEM_READ_WRITE ⇒ Some ? (mt_visit ? mem addr)
 214   | MEM_OUT_OF_BOUND ⇒ None ? ].
 215
 216 (* ************************** *)
 217 (* CARICAMENTO PROGRAMMA/DATI *)
 218 (* ************************** *)
 219
 220 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
 221 nlet rec mt_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T byte8))))
 222                                 (src:list byte8) (addr:word16) on src ≝
 223  match src with
 224   (* fine di source: carica da old_mem *)
 225   [ nil ⇒ old_mem
 226   | cons hd tl ⇒ mt_load_from_source_at (mt_update ? old_mem addr hd) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
 227   ].