helm/software/matita/contribs/ng_assembly/freescale/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 (*   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 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
  33 ndefinition mf_check_update_ranged ≝
  34 λf:word16 → memory_type.λinf.λsup.λv.
  35  λx.match inrange_w16 x inf sup with
  36   [ true ⇒ v
  37   | false ⇒ f x ].
  38
  39 (* tutta la memoria non installata *)
  40 ndefinition mf_out_of_bound_memory ≝ λ_:word16.MEM_OUT_OF_BOUND.
  41
  42 ndefinition mf_chk_get ≝
  43 λc:word16 → memory_type.λa:word16.
  44  match c a with
  45   [ 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
  46   | 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
  47   | 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
  48   ].
  49
  50 (* (mf_mem_update mem checked addr val) = scrivi controllando il tipo di memoria *)
  51 ndefinition mf_mem_update ≝
  52 λf:word16 → byte8.λc:Array8T memory_type.λa:word16.λv:byte8.
  53  match getn_array8T o0 ? c with
  54   (* ROM? ok, ma il valore viene perso *)
  55   [ MEM_READ_ONLY ⇒ Some ? f
  56   (* RAM? ok *)
  57   | MEM_READ_WRITE ⇒ Some ? (λx.match eq_w16 x a with [ true ⇒ v | false ⇒ f x ])
  58   (* NON INSTALLATA? no *)
  59   | MEM_OUT_OF_BOUND ⇒ None ? ].
  60
  61 (* tutta la memoria a 0 *)
  62 ndefinition mf_zero_memory ≝ λ_:word16.〈x0,x0〉.
  63
  64 (* (mf_mem_read mem check addr) = leggi controllando il tipo di memoria *)
  65 ndefinition mf_mem_read ≝
  66 λf:word16 → byte8.λc:word16 → memory_type.λa.
  67  match c a with
  68   [ MEM_READ_ONLY ⇒ Some ? (f a)
  69   | MEM_READ_WRITE ⇒ Some ? (f a)
  70   | MEM_OUT_OF_BOUND ⇒ None ? ].
  71
  72 (* ************************** *)
  73 (* CARICAMENTO PROGRAMMA/DATI *)
  74 (* ************************** *)
  75
  76 (* carica a paratire da addr, overflow se si supera 0xFFFF... *)
  77 nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (src:list byte8) (addr:word16) on src ≝
  78  match src with
  79   (* fine di source: carica da old_mem *)
  80   [ nil ⇒ old_mem
  81   | cons hd tl ⇒ λx:word16.match eq_w16 addr x with
  82    (* la locazione corrisponde al punto corrente di source *)
  83    [ true ⇒ hd
  84    (* la locazione e' piu' avanti? ricorsione *)
  85    | false ⇒ (mf_load_from_source_at old_mem tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)) x
  86    ]
  87   ].