helm/software/matita/library/freescale/memory_abs.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 set "baseuri" "cic:/matita/freescale/memory_abs/".
  28
  29 (*include "/media/VIRTUOSO/freescale/memory_func.ma".*)
  30 include "freescale/memory_func.ma".
  31 (*include "/media/VIRTUOSO/freescale/memory_trees.ma".*)
  32 include "freescale/memory_trees.ma".
  33 (*include "/media/VIRTUOSO/freescale/memory_bits.ma".*)
  34 include "freescale/memory_bits.ma".
  35
  36 (* ********************************************* *)
  37 (* ASTRAZIONE DALL'IMPLEMENTAZIONE DELLA MEMORIA *)
  38 (* ********************************************* *)
  39
  40 (* tipi di implementazione della memoria *)
  41 inductive memory_impl : Type ≝
  42   MEM_FUNC: memory_impl
  43 | MEM_TREE: memory_impl
  44 | MEM_BITS: memory_impl.
  45
  46 (* ausiliario per il tipo della memoria *)
  47 definition aux_mem_type ≝
  48 λt:memory_impl.match t with
  49  [ MEM_FUNC ⇒ word16 → byte8
  50  | MEM_TREE ⇒ Prod16T (Prod16T (Prod16T (Prod16T byte8)))
  51  | MEM_BITS ⇒ Prod16T (Prod16T (Prod16T (Prod16T (Prod8T bool))))
  52  ].
  53
  54 (* ausiliario per il tipo del checker *)
  55 definition aux_chk_type ≝
  56 λt:memory_impl.match t with
  57  [ MEM_FUNC ⇒ word16 → memory_type
  58  | MEM_TREE ⇒ Prod16T (Prod16T (Prod16T (Prod16T memory_type)))
  59  | MEM_BITS ⇒ Prod16T (Prod16T (Prod16T (Prod16T (Prod8T memory_type))))
  60  ].
  61
  62 (* unificazione di out_of_bound_memory *)
  63 definition out_of_bound_memory ≝
  64 λt:memory_impl.
  65  match t
  66   return λt.aux_chk_type t
  67  with
  68   [ MEM_FUNC ⇒ mf_out_of_bound_memory
  69   | MEM_TREE ⇒ mt_out_of_bound_memory
  70   | MEM_BITS ⇒ mb_out_of_bound_memory
  71   ].
  72
  73 (* unificazione di zero_memory *)
  74 definition zero_memory ≝
  75 λt:memory_impl.
  76  match t
  77   return λt.aux_mem_type t
  78  with
  79   [ MEM_FUNC ⇒ mf_zero_memory
  80   | MEM_TREE ⇒ mt_zero_memory
  81   | MEM_BITS ⇒ mb_zero_memory
  82   ].
  83
  84 (* unificazione della lettura senza chk: mem_read_abs mem addr *)
  85 definition mem_read_abs ≝
  86 λt:memory_impl.
  87  match t
  88   return λt.aux_mem_type t → word16 → byte8
  89  with
  90   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
  91                λaddr:word16.
  92                m addr
  93   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
  94                λaddr:word16.
  95                mt_visit byte8 m addr
  96   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
  97                λaddr:word16.
  98                byte8_of_bits (mt_visit (Prod8T bool) m addr)
  99   ].
 100
 101 (* unificazione della lettura con chk: mem_read mem chk addr *)
 102 definition mem_read ≝
 103 λt:memory_impl.
 104  match t
 105   return λt.aux_mem_type t → aux_chk_type t → word16 → option byte8
 106  with
 107   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 108                λc:aux_chk_type MEM_FUNC.
 109                λaddr:word16.
 110                mf_mem_read m c addr
 111   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 112                λc:aux_chk_type MEM_TREE.
 113                λaddr:word16.
 114                mt_mem_read m c addr
 115   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 116                λc:aux_chk_type MEM_BITS.
 117                λaddr:word16.
 118                mb_mem_read m c addr
 119   ].
 120
 121 (* unificazione della lettura di bit con chk: mem_read mem chk addr sub *)
 122 definition mem_read_bit ≝
 123 λt:memory_impl.
 124  match t
 125   return λt.aux_mem_type t → aux_chk_type t → word16 → oct → option bool
 126  with
 127   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 128                λc:aux_chk_type MEM_FUNC.
 129                λaddr:word16.
 130                λo:oct.
 131                opt_map ?? (mf_mem_read m c addr)
 132                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 133   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 134                λc:aux_chk_type MEM_TREE.
 135                λaddr:word16.
 136                λo:oct.
 137                opt_map ?? (mt_mem_read m c addr)
 138                 (λb.Some ? (getn_array8T o bool (bits_of_byte8 b)))
 139   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 140                λc:aux_chk_type MEM_BITS.
 141                λaddr:word16.
 142                λo:oct.
 143                mb_mem_read_bit m c addr o
 144   ].
 145
 146 (* unificazione della scrittura con chk: mem_update mem chk addr val *)
 147 definition mem_update ≝
 148 λt:memory_impl.
 149  match t
 150   return λt.aux_mem_type t → aux_chk_type t → word16 → byte8 → option (aux_mem_type t)
 151  with
 152   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 153                λc:aux_chk_type MEM_FUNC.
 154                λaddr:word16.
 155                λv:byte8.
 156                mf_mem_update m c addr v
 157   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 158                λc:aux_chk_type MEM_TREE.
 159                λaddr:word16.
 160                λv:byte8.
 161                mt_mem_update m c addr v
 162   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 163                λc:aux_chk_type MEM_BITS.
 164                λaddr:word16.
 165                λv:byte8.
 166                mb_mem_update m c addr v
 167   ].
 168
 169 (* unificazione della scrittura di bit con chk: mem_update mem chk addr sub val *)
 170 definition mem_update_bit ≝
 171 λt:memory_impl.
 172  match t
 173   return λt.aux_mem_type t → aux_chk_type t → word16 → oct → bool → option (aux_mem_type t)
 174  with
 175   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 176                λc:aux_chk_type MEM_FUNC.
 177                λaddr:word16.
 178                λo:oct.
 179                λv:bool.
 180                opt_map ?? (mf_mem_read m c addr)
 181                 (λb.mf_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
 182   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 183                λc:aux_chk_type MEM_TREE.
 184                λaddr:word16.
 185                λo:oct.
 186                λv:bool.
 187                opt_map ?? (mt_mem_read m c addr)
 188                 (λb.mt_mem_update m c addr (byte8_of_bits (setn_array8T o bool (bits_of_byte8 b) v)))
 189   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 190                λc:aux_chk_type MEM_BITS.
 191                λaddr:word16.
 192                λo:oct.
 193                λv:bool.
 194                mb_mem_update_bit m c addr o v
 195   ].
 196
 197 (* unificazione del caricamento: load_from_source_at old_mem source addr *)
 198 definition load_from_source_at ≝
 199 λt:memory_impl.
 200  match t
 201   return λt.aux_mem_type t → list byte8 → word16 → aux_mem_type t
 202  with
 203   [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
 204                λl:list byte8.
 205                λaddr:word16.
 206                mf_load_from_source_at m l addr
 207   | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
 208                λl:list byte8.
 209                λaddr:word16.
 210                mt_load_from_source_at m l addr
 211   | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
 212                λl:list byte8.
 213                λaddr:word16.
 214                mb_load_from_source_at m l addr
 215   ].
 216
 217 (* unificazione dell'impostazione della memoria: chk_update_ranged chk inf sup v *)
 218 definition check_update_ranged ≝
 219 λt:memory_impl.
 220  match t
 221   return λt.aux_chk_type t → word16 → word16 → memory_type → aux_chk_type t
 222  with
 223   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 224                λinf,sup:word16.
 225                λv:memory_type.
 226                mf_check_update_ranged c inf sup v
 227   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 228                λinf,sup:word16.
 229                λv:memory_type.
 230                mt_update_ranged memory_type c inf sup v
 231   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 232                λinf,sup:word16.
 233                λv:memory_type.
 234                mt_update_ranged (Prod8T memory_type) c inf sup (array_8T memory_type v v v v v v v v)
 235   ].
 236
 237 (* unificazione dell'impostazione dei bit: chk_update_bit chk addr sub v *)
 238 (* NB: dove non esiste la granularita' del bit, lascio inalterato *)
 239 definition check_update_bit ≝
 240 λt:memory_impl.
 241  match t
 242   return λt.aux_chk_type t → word16 → oct → memory_type → aux_chk_type t
 243  with
 244   [ MEM_FUNC ⇒ λc:aux_chk_type MEM_FUNC.
 245                λaddr:word16.
 246                λo:oct.
 247                λv:memory_type.
 248                c
 249   | MEM_TREE ⇒ λc:aux_chk_type MEM_TREE.
 250                λaddr:word16.
 251                λo:oct.
 252                λv:memory_type.
 253                c
 254   | MEM_BITS ⇒ λc:aux_chk_type MEM_BITS.
 255                λaddr:word16.
 256                λo:oct.
 257                λv:memory_type.
 258                mb_chk_update_bit c addr o v
 259   ].