matita/matita/contribs/ng_assembly2/emulator/memory/memory_func.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 "num/word16.ma".
  25 include "common/list.ma".
  26
  27 (* ************************** *)
  28 (* 8 segmenti da 64Kb → 512Kb *)
  29 (* ************************** *)
  30
  31 (* ********************* *)
  32 (* MEMORIA E DESCRITTORE *)
  33 (* ********************* *)
  34
  35 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
  36 ndefinition mf_check_update_ranged ≝
  37 λf:oct → word16 → memory_type.λsel:oct.λaddr:word16.λrange:word16.λv.
  38  λx,y.
  39  match (eqc ? sel x)⊗(inrangec ? y addr (plusc_d_d ? addr range)) with
  40   [ true ⇒ v
  41   | false ⇒ f x y ].
  42
  43 (* tutta la memoria non installata *)
  44 ndefinition mf_out_of_bound_memory ≝ λ_:oct.λ_:word16.MEM_OUT_OF_BOUND.
  45
  46 (* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
  47 ndefinition mf_mem_update ≝
  48 λf:oct → word16 → byte8.λc:oct → word16 → memory_type.λsel:oct.λa:word16.λv:byte8.
  49  match c sel a with
  50   (* ROM? ok, ma il valore viene perso *)
  51   [ MEM_READ_ONLY ⇒ Some ? f
  52   (* RAM? ok *)
  53   | MEM_READ_WRITE ⇒ Some ? (λx,y.match (eqc ? sel x)⊗(eqc ? a y) with [ true ⇒ v | false ⇒ f x y ])
  54   (* NON INSTALLATA? no *)
  55   | MEM_OUT_OF_BOUND ⇒ None ? ].
  56
  57 (* tutta la memoria a 0 *)
  58 ndefinition mf_zero_memory ≝ λ_:oct.λ_:word16.〈x0,x0〉.
  59
  60 (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
  61 ndefinition mf_mem_read ≝
  62 λf:oct → word16 → byte8.λc:oct → word16 → memory_type.λsel:oct.λa:word16.
  63  match c sel a with
  64   [ MEM_READ_ONLY ⇒ Some ? (f sel a)
  65   | MEM_READ_WRITE ⇒ Some ? (f sel a)
  66   | MEM_OUT_OF_BOUND ⇒ None ? ].
  67
  68 (* ************************** *)
  69 (* CARICAMENTO PROGRAMMA/DATI *)
  70 (* ************************** *)
  71
  72 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
  73 nlet rec mf_load_from_source_at (old_mem:oct → word16 → byte8) (src:list byte8) (sel:oct) (addr:word16) on src ≝
  74  match src with
  75   (* fine di source: carica da old_mem *)
  76   [ nil ⇒ old_mem
  77   | cons hd tl ⇒ λx,y.match (eqc ? sel x)⊗(eqc ? addr y) with
  78    (* la locazione corrisponde al punto corrente di source *)
  79    [ true ⇒ hd
  80    (* la locazione e' piu' avanti? ricorsione *)
  81    | false ⇒ (mf_load_from_source_at old_mem tl sel (succc ? addr)) x y
  82    ]
  83   ].