helm/software/matita/contribs/ng_assembly2/emulator/read_write/load_write_base.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/read_write/read_write.ma".
  24
  25 (* mattoni base *)
  26 (* - incrementano l'indirizzo normalmente *)
  27 (* - incrementano PC attraverso il filtro *)
  28 (* - letture filtrate, quindi da segmento 0 *)
  29
  30 (* lettura byte da addr *)
  31 ndefinition loadb_from ≝
  32 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  33 λaddr:word16.λcur_pc:word16.λfetched:exadecim.
  34  opt_map … (memory_filter_read … s addr)
  35   (λb.Some ? (triple … s b (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
  36
  37 (* lettura bit da addr *)
  38 ndefinition loadbit_from ≝
  39 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  40 λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:exadecim.
  41  opt_map … (memory_filter_read_bit … s addr sub)
  42   (λb.Some ? (triple … s b (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
  43
  44 (* lettura word da addr *)
  45 ndefinition loadw_from ≝
  46 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  47 λaddr:word16.λcur_pc:word16.λfetched:exadecim.
  48  opt_map … (memory_filter_read … s addr)
  49   (λbh.opt_map … (memory_filter_read … s (succc ? addr))
  50    (λbl.Some ? (triple … s 〈bh:bl〉 (plusc_d_d ? cur_pc (extu2_w16 fetched))))).
  51
  52 (* scrittura byte su addr *)
  53 ndefinition writeb_to ≝
  54 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  55 λaddr:word16.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwriteb:byte8.
  56  opt_map … (memory_filter_write … s addr flag writeb)
  57   (λtmps.Some ? (pair … tmps (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
  58
  59 (* scrittura bit su addr *)
  60 ndefinition writebit_to ≝
  61 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  62 λaddr:word16.λsub:oct.λcur_pc:word16.λfetched:exadecim.λwriteb:bool.
  63  opt_map … (memory_filter_write_bit … s addr sub writeb)
  64   (λtmps.Some ? (pair … tmps (plusc_d_d ? cur_pc (extu2_w16 fetched)))).
  65
  66 (* scrittura word su addr *)
  67 ndefinition writew_to ≝
  68 λm:mcu_type.λt:memory_impl.λs:any_status m t.
  69 λaddr:word16.λflag:aux_mod_type.λcur_pc:word16.λfetched:exadecim.λwritew:word16.
  70  opt_map … (memory_filter_write … s addr auxMode_ok (cnH ? writew))
  71   (λtmps1.opt_map … (memory_filter_write … tmps1 (succc ? addr) auxMode_ok (cnL ? writew))
  72     (λtmps2.Some ? (pair … tmps2 (plusc_d_d ? cur_pc (extu2_w16 fetched))))).
  73
  74 (* ausiliari per definire i tipi e la lettura/scrittura *)
  75
  76 (* ausiliaria per definire il tipo di aux_load *)
  77 ndefinition aux_load_typing ≝
  78 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  79  any_status m t → word16 → word16 → exadecim →
  80  option (Prod3T (any_status m t) match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] word16).
  81
  82 (* per non dover ramificare i vari load in byte/word *)
  83 ndefinition aux_load ≝
  84 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_load_typing m t with
  85  [ true ⇒ loadb_from m t | false ⇒ loadw_from m t ].
  86
  87 (* ausiliaria per definire il tipo di aux_write *)
  88 ndefinition aux_write_typing ≝
  89 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  90  any_status m t → word16 → aux_mod_type → word16 → exadecim →
  91  match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
  92  option (ProdT (any_status m t) word16).
  93
  94 (* per non dover ramificare i vari load in byte/word *)
  95 ndefinition aux_write ≝
  96 λm:mcu_type.λt:memory_impl.λbyteflag:bool.match byteflag return aux_write_typing m t with
  97  [ true ⇒ writeb_to m t | false ⇒ writew_to m t ].
  98
  99 ndefinition mem_read_s ≝
 100 λm,t.λs:any_status m t.mem_read t (mem_desc … s) (chk_desc … s).
 101
 102 ndefinition mem_read_bit_s ≝
 103 λm,t.λs:any_status m t.mem_read_bit t (mem_desc … s) (chk_desc … s).
 104
 105 ndefinition mem_write_s ≝
 106 λm,t.λs:any_status m t.λseg,a,val.
 107  opt_map … (mem_update t (mem_desc … s) (chk_desc … s) seg a val)
 108   (λmem'.Some ? (set_mem_desc … s mem')).
 109
 110 ndefinition mem_write_bit_s ≝
 111 λm,t.λs:any_status m t.λseg,a,sub,val.
 112  opt_map … (mem_update_bit t (mem_desc … s) (chk_desc … s) seg a sub val)
 113   (λmem'.Some ? (set_mem_desc … s mem')).