helm/software/matita/contribs/ng_assembly2/emulator/read_write/fetch_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/translation/translation.ma".
  24
  25 (* errori possibili nel fetch OPCODE / ILLEGAL ADDRESS *)
  26 ninductive error_type : Type ≝
  27   ILL_OP: error_type
  28 | ILL_FETCH_AD: error_type
  29 .
  30
  31 (* - errore: interessa solo l'errore
  32    - ok: interessa info, nuovo pc *)
  33 ninductive fetch_result (A:Type) : Type ≝
  34   FetchERR : error_type → fetch_result A
  35 | FetchOK  : A → word16 → fetch_result A.
  36
  37 ndefinition fetch_byte_aux ≝
  38 λm:mcu_type.λcur_pc:word16.λbh:byte8.
  39  match full_info_of_word16 m (Byte bh) with
  40   [ None ⇒ FetchERR ? ILL_FETCH_AD
  41   | Some info ⇒ FetchOK ? info cur_pc
  42   ].
  43
  44 ndefinition fetch_word_aux ≝
  45 λm:mcu_type.λcur_pc:word16.λw:word16.
  46  match full_info_of_word16 m (Word w) with
  47   [ None ⇒ FetchERR ? ILL_FETCH_AD
  48   | Some info ⇒ FetchOK ? info cur_pc
  49   ].