matita/matita/contribs/ng_assembly2/emulator/memory/memory_bits.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_trees.ma".
  24
  25 (* ********************* *)
  26 (* MEMORIA E DESCRITTORE *)
  27 (* ********************* *)
  28
  29 (* tutta la memoria non installata *)
  30 ndefinition mb_out_of_bound_memory ≝
  31  aux_20B_filler ?
  32   (mk_Array8T ? MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND
  33                 MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND MEM_OUT_OF_BOUND).
  34
  35 (* tutta la memoria a 0 *)
  36 ndefinition mb_zero_memory ≝
  37  aux_20B_filler ? (mk_Array8T ? false false false false false false false false).
  38
  39 (* scrivi bit controllando il tipo di memoria *)
  40 ndefinition mb_mem_update_bit ≝
  41 λmem:aux_20B_type (Array8T bool).
  42 λchk:aux_20B_type (Array8T memory_type).
  43 λsel:oct.λaddr:word16.λsub:oct.λv:bool.
  44  match getn_array8T sub ? (mt_visit ? chk sel addr) with
  45   (* ROM? ok, ma il valore viene perso *)
  46   [ MEM_READ_ONLY ⇒ Some ? mem
  47   (* RAM? ok *)
  48   | MEM_READ_WRITE ⇒ Some ? (mt_update ? mem sel addr (setn_array8T sub ? (mt_visit ? mem sel addr) v))
  49   (* NON INSTALLATA? no *)
  50   | MEM_OUT_OF_BOUND ⇒ None ? ].
  51
  52 ndefinition mb_mem_update ≝
  53 λmem:aux_20B_type (Array8T bool).
  54 λchk:aux_20B_type (Array8T memory_type).
  55 λsel:oct.λaddr:word16.λv:byte8.
  56 let old_value ≝ mt_visit (Array8T bool) mem sel addr in
  57 let new_value ≝ bits_of_byte8 v in
  58 let memtypes ≝ mt_visit (Array8T memory_type) chk sel addr in
  59 let newbit0 ≝ match getn_array8T o0 memory_type memtypes with
  60  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool old_value)
  61  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool new_value)
  62  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  63 let newbit1 ≝ match getn_array8T o1 memory_type memtypes with
  64  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool old_value)
  65  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool new_value)
  66  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  67 let newbit2 ≝ match getn_array8T o2 memory_type memtypes with
  68  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool old_value)
  69  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool new_value)
  70  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  71 let newbit3 ≝ match getn_array8T o3 memory_type memtypes with
  72  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool old_value)
  73  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool new_value)
  74  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  75 let newbit4 ≝ match getn_array8T o4 memory_type memtypes with
  76  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool old_value)
  77  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool new_value)
  78  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  79 let newbit5 ≝ match getn_array8T o5 memory_type memtypes with
  80  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool old_value)
  81  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool new_value)
  82  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  83 let newbit6 ≝ match getn_array8T o6 memory_type memtypes with
  84  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool old_value)
  85  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool new_value)
  86  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  87 let newbit7 ≝ match getn_array8T o7 memory_type memtypes with
  88  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool old_value)
  89  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool new_value)
  90  | MEM_OUT_OF_BOUND ⇒ None bool ] in
  91        opt_map … newbit0
  92  (λnb0.opt_map … newbit1
  93  (λnb1.opt_map … newbit2
  94  (λnb2.opt_map … newbit3
  95  (λnb3.opt_map … newbit4
  96  (λnb4.opt_map … newbit5
  97  (λnb5.opt_map … newbit6
  98  (λnb6.opt_map … newbit7
  99  (λnb7.Some ? (mt_update ? mem sel addr (mk_Array8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 100
 101 (* scrivi tipo di bit *)
 102 ndefinition mb_chk_update_bit ≝
 103 λchk:aux_20B_type (Array8T memory_type).
 104 λsel:oct.λaddr:word16.λsub:oct.λv:memory_type.
 105  mt_update ? chk sel addr (setn_array8T sub ? (mt_visit ? chk sel addr) v).
 106
 107 (* leggi bit controllando il tipo di memoria *)
 108 ndefinition mb_mem_read_bit ≝
 109 λmem:aux_20B_type (Array8T bool).
 110 λchk:aux_20B_type (Array8T memory_type).
 111 λsel:oct.λaddr:word16.λsub:oct.
 112  match getn_array8T sub ? (mt_visit ? chk sel addr) with
 113   (* ROM? ok, ma il valore viene perso *)
 114   [ MEM_READ_ONLY ⇒ Some ? (getn_array8T sub ? (mt_visit ? mem sel addr))
 115   (* RAM? ok *)
 116   | MEM_READ_WRITE ⇒ Some ? (getn_array8T sub ? (mt_visit ? mem sel addr))
 117   (* NON INSTALLATA? no *)
 118   | MEM_OUT_OF_BOUND ⇒ None ? ].
 119
 120 (* leggi controllando il tipo di memoria *)
 121 (* NB: devono esistere tutti i bit *)
 122 ndefinition mb_mem_read ≝
 123 λmem:aux_20B_type (Array8T bool).
 124 λchk:aux_20B_type (Array8T memory_type).
 125 λsel:oct.λaddr:word16.
 126 let value ≝ mt_visit (Array8T bool) mem sel addr in
 127 let memtypes ≝ mt_visit (Array8T memory_type) chk sel addr in
 128 let newbit0 ≝ match getn_array8T o0 memory_type memtypes with
 129  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o0 bool value)
 130  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o0 bool value)
 131  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 132 let newbit1 ≝ match getn_array8T o1 memory_type memtypes with
 133  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o1 bool value)
 134  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o1 bool value)
 135  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 136 let newbit2 ≝ match getn_array8T o2 memory_type memtypes with
 137  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o2 bool value)
 138  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o2 bool value)
 139  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 140 let newbit3 ≝ match getn_array8T o3 memory_type memtypes with
 141  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o3 bool value)
 142  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o3 bool value)
 143  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 144 let newbit4 ≝ match getn_array8T o4 memory_type memtypes with
 145  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o4 bool value)
 146  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o4 bool value)
 147  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 148 let newbit5 ≝ match getn_array8T o5 memory_type memtypes with
 149  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o5 bool value)
 150  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o5 bool value)
 151  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 152 let newbit6 ≝ match getn_array8T o6 memory_type memtypes with
 153  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o6 bool value)
 154  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o6 bool value)
 155  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 156 let newbit7 ≝ match getn_array8T o7 memory_type memtypes with
 157  [ MEM_READ_ONLY ⇒ Some bool (getn_array8T o7 bool value)
 158  | MEM_READ_WRITE ⇒ Some bool (getn_array8T o7 bool value)
 159  | MEM_OUT_OF_BOUND ⇒ None bool ] in
 160        opt_map … newbit0
 161  (λnb0.opt_map … newbit1
 162  (λnb1.opt_map … newbit2
 163  (λnb2.opt_map … newbit3
 164  (λnb3.opt_map … newbit4
 165  (λnb4.opt_map … newbit5
 166  (λnb5.opt_map … newbit6
 167  (λnb6.opt_map … newbit7
 168  (λnb7.Some ? (byte8_of_bits (mk_Array8T bool nb7 nb6 nb5 nb4 nb3 nb2 nb1 nb0)))))))))).
 169
 170 (* ************************** *)
 171 (* CARICAMENTO PROGRAMMA/DATI *)
 172 (* ************************** *)
 173
 174 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 175 nlet rec mb_load_from_source_at (old_mem:aux_20B_type (Array8T bool))
 176                                 (src:list byte8) (sel:oct) (addr:word16) on src ≝
 177  match src with
 178   (* fine di source: carica da old_mem *)
 179   [ nil ⇒ old_mem
 180   | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem sel addr (bits_of_byte8 hd))
 181                                         tl sel (succc ? addr)
 182   ].