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