matitaB/matita/contribs/ng_assembly/emulator/memory/memory_struct.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 "num/oct.ma".
  24 include "num/byte8.ma".
  25
  26 (* **************************** *)
  27 (* TIPI PER I MODULI DI MEMORIA *)
  28 (* **************************** *)
  29
  30 (* tipi di memoria:RAM/ROM/non installata *)
  31 ninductive memory_type : Type ≝
  32   MEM_READ_ONLY: memory_type
  33 | MEM_READ_WRITE: memory_type
  34 | MEM_OUT_OF_BOUND: memory_type.
  35
  36 (* **************** *)
  37 (* TIPO ARRAY DA 16 *)
  38 (* **************** *)
  39
  40 (* definizione di un array omogeneo di dimensione 16 *)
  41 nrecord Array16T (T:Type) : Type ≝
  42 { a16_1  : T ; a16_2  : T ; a16_3  : T ; a16_4  : T
  43 ; a16_5  : T ; a16_6  : T ; a16_7  : T ; a16_8  : T
  44 ; a16_9  : T ; a16_10 : T ; a16_11 : T ; a16_12 : T
  45 ; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }.
  46
  47 (* operatore uguaglianza *)
  48 ndefinition eq_ar16 ≝
  49 λT.λf:T → T → bool.λa1,a2:Array16T T.
  50  (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗
  51  (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗
  52  (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗
  53  (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗
  54  (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗
  55  (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗
  56  (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗
  57  (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)).
  58
  59 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  60 (* posso definire un getter a matrice sull'array *)
  61
  62 ndefinition getn_array16T ≝
  63 λn:exadecim.λT:Type.λp:Array16T T.
  64  match n return λn.(Array16T T) → T with
  65   [ x0 ⇒ a16_1  T | x1 ⇒ a16_2  T | x2 ⇒ a16_3  T | x3 ⇒ a16_4  T
  66   | x4 ⇒ a16_5  T | x5 ⇒ a16_6  T | x6 ⇒ a16_7  T | x7 ⇒ a16_8  T
  67   | x8 ⇒ a16_9  T | x9 ⇒ a16_10 T | xA ⇒ a16_11 T | xB ⇒ a16_12 T
  68   | xC ⇒ a16_13 T | xD ⇒ a16_14 T | xE ⇒ a16_15 T | xF ⇒ a16_16 T
  69   ] p.
  70
  71 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  72 (* posso definire un setter a matrice sull'array *)
  73 ndefinition setn_array16T ≝
  74 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
  75 let e00 ≝ (a16_1 T p) in
  76 let e01 ≝ (a16_2 T p) in
  77 let e02 ≝ (a16_3 T p) in
  78 let e03 ≝ (a16_4 T p) in
  79 let e04 ≝ (a16_5 T p) in
  80 let e05 ≝ (a16_6 T p) in
  81 let e06 ≝ (a16_7 T p) in
  82 let e07 ≝ (a16_8 T p) in
  83 let e08 ≝ (a16_9 T p) in
  84 let e09 ≝ (a16_10 T p) in
  85 let e10 ≝ (a16_11 T p) in
  86 let e11 ≝ (a16_12 T p) in
  87 let e12 ≝ (a16_13 T p) in
  88 let e13 ≝ (a16_14 T p) in
  89 let e14 ≝ (a16_15 T p) in
  90 let e15 ≝ (a16_16 T p) in
  91  match n with
  92   [ x0 ⇒ mk_Array16T T v   e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  93   | x1 ⇒ mk_Array16T T e00 v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  94   | x2 ⇒ mk_Array16T T e00 e01 v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  95   | x3 ⇒ mk_Array16T T e00 e01 e02 v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  96   | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  97   | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  98   | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v   e07 e08 e09 e10 e11 e12 e13 e14 e15
  99   | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v   e08 e09 e10 e11 e12 e13 e14 e15
 100   | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v   e09 e10 e11 e12 e13 e14 e15
 101   | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v   e10 e11 e12 e13 e14 e15
 102   | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v   e11 e12 e13 e14 e15
 103   | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v   e12 e13 e14 e15
 104   | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v   e13 e14 e15
 105   | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v   e14 e15
 106   | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v   e15
 107   | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
 108   ].
 109
 110 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 111 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
 112 (* m ≤ n *)
 113 ndefinition setmn_array16T ≝
 114 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
 115 let e00 ≝ (a16_1 T p) in
 116 let e01 ≝ (a16_2 T p) in
 117 let e02 ≝ (a16_3 T p) in
 118 let e03 ≝ (a16_4 T p) in
 119 let e04 ≝ (a16_5 T p) in
 120 let e05 ≝ (a16_6 T p) in
 121 let e06 ≝ (a16_7 T p) in
 122 let e07 ≝ (a16_8 T p) in
 123 let e08 ≝ (a16_9 T p) in
 124 let e09 ≝ (a16_10 T p) in
 125 let e10 ≝ (a16_11 T p) in
 126 let e11 ≝ (a16_12 T p) in
 127 let e12 ≝ (a16_13 T p) in
 128 let e13 ≝ (a16_14 T p) in
 129 let e14 ≝ (a16_15 T p) in
 130 let e15 ≝ (a16_16 T p) in
 131  match m with
 132   [ x0 ⇒ match n with
 133    [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 134    | x1 ⇒ mk_Array16T T v v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 135    | x2 ⇒ mk_Array16T T v v   v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 136    | x3 ⇒ mk_Array16T T v v   v   v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 137    | x4 ⇒ mk_Array16T T v v   v   v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 138    | x5 ⇒ mk_Array16T T v v   v   v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 139    | x6 ⇒ mk_Array16T T v v   v   v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 140    | x7 ⇒ mk_Array16T T v v   v   v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 141    | x8 ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 142    | x9 ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 143    | xA ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 144    | xB ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 145    | xC ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 146    | xD ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   e14 e15
 147    | xE ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   v   e15
 148    | xF ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   v   v ]
 149   | x1 ⇒ match n with
 150    [ x0 ⇒ p
 151    | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 152    | x2 ⇒ mk_Array16T T e00 v v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 153    | x3 ⇒ mk_Array16T T e00 v v   v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 154    | x4 ⇒ mk_Array16T T e00 v v   v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 155    | x5 ⇒ mk_Array16T T e00 v v   v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 156    | x6 ⇒ mk_Array16T T e00 v v   v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 157    | x7 ⇒ mk_Array16T T e00 v v   v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 158    | x8 ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 159    | x9 ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 160    | xA ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 161    | xB ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 162    | xC ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 163    | xD ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   e14 e15
 164    | xE ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   v   e15
 165    | xF ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   v   v ]
 166   | x2 ⇒ match n with
 167    [ x0 ⇒ p | x1 ⇒ p
 168    | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 169    | x3 ⇒ mk_Array16T T e00 e01 v v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 170    | x4 ⇒ mk_Array16T T e00 e01 v v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 171    | x5 ⇒ mk_Array16T T e00 e01 v v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 172    | x6 ⇒ mk_Array16T T e00 e01 v v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 173    | x7 ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 174    | x8 ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 175    | x9 ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 176    | xA ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 177    | xB ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 178    | xC ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 179    | xD ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   e14 e15
 180    | xE ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   v   e15
 181    | xF ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   v   v ]
 182   | x3 ⇒ match n with
 183    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p
 184    | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 185    | x4 ⇒ mk_Array16T T e00 e01 e02 v v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 186    | x5 ⇒ mk_Array16T T e00 e01 e02 v v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 187    | x6 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 188    | x7 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 189    | x8 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 190    | x9 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 191    | xA ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 192    | xB ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   e12 e13 e14 e15
 193    | xC ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   e13 e14 e15
 194    | xD ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   e14 e15
 195    | xE ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   v   e15
 196    | xF ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   v   v ]
 197   | x4 ⇒ match n with
 198    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p
 199    | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 200    | x5 ⇒ mk_Array16T T e00 e01 e02 e03 v v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 201    | x6 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 202    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 203    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 204    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   e10 e11 e12 e13 e14 e15
 205    | xA ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   e11 e12 e13 e14 e15
 206    | xB ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   e12 e13 e14 e15
 207    | xC ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   e13 e14 e15
 208    | xD ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   e14 e15
 209    | xE ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   v   e15
 210    | xF ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   v   v ]
 211   | x5 ⇒ match n with
 212    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p
 213    | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 214    | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 215    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   e08 e09 e10 e11 e12 e13 e14 e15
 216    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   e09 e10 e11 e12 e13 e14 e15
 217    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   e10 e11 e12 e13 e14 e15
 218    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   e11 e12 e13 e14 e15
 219    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   e12 e13 e14 e15
 220    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   e13 e14 e15
 221    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   e14 e15
 222    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   v   e15
 223    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   v   v ]
 224   | x6 ⇒ match n with
 225    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p
 226    | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
 227    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   e08 e09 e10 e11 e12 e13 e14 e15
 228    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   e09 e10 e11 e12 e13 e14 e15
 229    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   e10 e11 e12 e13 e14 e15
 230    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   e11 e12 e13 e14 e15
 231    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   e12 e13 e14 e15
 232    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   e13 e14 e15
 233    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   e14 e15
 234    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   v   e15
 235    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   v   v ]
 236   | x7 ⇒ match n with
 237    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p
 238    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
 239    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   e09 e10 e11 e12 e13 e14 e15
 240    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   e10 e11 e12 e13 e14 e15
 241    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   e11 e12 e13 e14 e15
 242    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   e12 e13 e14 e15
 243    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   e13 e14 e15
 244    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   e14 e15
 245    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   v   e15
 246    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   v   v ]
 247   | x8 ⇒ match n with
 248    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 249    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
 250    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   e10 e11 e12 e13 e14 e15
 251    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   e11 e12 e13 e14 e15
 252    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   e12 e13 e14 e15
 253    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   e13 e14 e15
 254    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   e14 e15
 255    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   v   e15
 256    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   v   v ]
 257   | x9 ⇒ match n with
 258    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p  | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 259    | x8 ⇒ p
 260    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
 261    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   e11 e12 e13 e14 e15
 262    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   e12 e13 e14 e15
 263    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   e13 e14 e15
 264    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   e14 e15
 265    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   v   e15
 266    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   v   v ]
 267   | xA ⇒ match n with
 268    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 269    | x8 ⇒ p | x9 ⇒ p
 270    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
 271    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   e12 e13 e14 e15
 272    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   e13 e14 e15
 273    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   e14 e15
 274    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   v   e15
 275    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   v   v ]
 276   | xB ⇒ match n with
 277    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 278    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p
 279    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
 280    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   e13 e14 e15
 281    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   e14 e15
 282    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   v   e15
 283    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   v   v ]
 284   | xC ⇒ match n with
 285    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 286    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p
 287    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
 288    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   e14 e15
 289    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   v   e15
 290    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   v   v ]
 291   | xD ⇒ match n with
 292    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 293    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p
 294    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
 295    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v   e15
 296    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v   v ]
 297   | xE ⇒ match n with
 298    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 299    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p
 300    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
 301    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ]
 302   | xF ⇒ match n with
 303    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 304    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p
 305    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ]
 306   ].
 307
 308 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 309 (* posso definire un setter composto [m+1,n-1] a matrice sull'array *)
 310 (* NB: obbiettivo evitare l'overflow *)
 311 ndefinition setmn_array16T_succ_pred ≝
 312 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
 313  match lt_ex m xF with
 314   [ true ⇒ match gt_ex n x0 with
 315    [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v
 316    | false ⇒ p
 317    ]
 318   | false ⇒ p
 319   ].
 320
 321 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 322 (* posso definire un setter composto [m+1,F] a matrice sull'array *)
 323 (* NB: obbiettivo evitare l'overflow *)
 324 ndefinition setmn_array16T_succ ≝
 325 λm:exadecim.λT:Type.λp:Array16T T.λv:T.
 326  match lt_ex m xF with
 327   [ true ⇒ setmn_array16T (succ_ex m) xF T p v
 328   | false ⇒ p
 329   ].
 330
 331 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 332 (* posso definire un setter composto [0,n-1] a matrice sull'array *)
 333 (* NB: obbiettivo evitare l'overflow *)
 334 ndefinition setmn_array16T_pred ≝
 335 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
 336  match gt_ex n x0 with
 337   [ true ⇒ setmn_array16T x0 (pred_ex n) T p v
 338   | false ⇒ p
 339   ].
 340
 341 (* ************************** *)
 342 (* TIPO BYTE COME INSIEME BIT *)
 343 (* ************************** *)
 344
 345 (* definizione di un byte come 8 bit *)
 346 nrecord Array8T (T:Type) : Type ≝
 347 { a8_1  : T ; a8_2  : T ; a8_3  : T ; a8_4  : T
 348 ; a8_5  : T ; a8_6  : T ; a8_7  : T ; a8_8  : T }.
 349
 350 (* operatore uguaglianza *)
 351 ndefinition eq_ar8 ≝
 352 λT.λf:T → T → bool.λa1,a2:Array8T T.
 353  (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗
 354  (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗
 355  (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗
 356  (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)).
 357
 358 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 359 (* posso definire un getter a matrice sull'array *)
 360 ndefinition getn_array8T ≝
 361 λn:oct.λT:Type.λp:Array8T T.
 362  match n return λn.(Array8T T) → T with
 363   [ o0 ⇒ a8_1  T | o1 ⇒ a8_2  T | o2 ⇒ a8_3  T | o3 ⇒ a8_4  T
 364   | o4 ⇒ a8_5  T | o5 ⇒ a8_6  T | o6 ⇒ a8_7  T | o7 ⇒ a8_8  T
 365   ] p.
 366
 367 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 368 (* posso definire un setter a matrice sull'array *)
 369 ndefinition setn_array8T ≝
 370 λn:oct.λT:Type.λp:Array8T T.λv:T.
 371 let e00 ≝ (a8_1 T p) in
 372 let e01 ≝ (a8_2 T p) in
 373 let e02 ≝ (a8_3 T p) in
 374 let e03 ≝ (a8_4 T p) in
 375 let e04 ≝ (a8_5 T p) in
 376 let e05 ≝ (a8_6 T p) in
 377 let e06 ≝ (a8_7 T p) in
 378 let e07 ≝ (a8_8 T p) in
 379  match n with
 380   [ o0 ⇒ mk_Array8T T v   e01 e02 e03 e04 e05 e06 e07
 381   | o1 ⇒ mk_Array8T T e00 v   e02 e03 e04 e05 e06 e07
 382   | o2 ⇒ mk_Array8T T e00 e01 v   e03 e04 e05 e06 e07
 383   | o3 ⇒ mk_Array8T T e00 e01 e02 v   e04 e05 e06 e07
 384   | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v   e05 e06 e07
 385   | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v   e06 e07
 386   | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v   e07
 387   | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v
 388   ].
 389
 390 (* lettura byte *)
 391 ndefinition byte8_of_bits ≝
 392 λp:Array8T bool.
 393    mk_byte8
 394    (or_ex (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ])
 395    (or_ex (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ])
 396    (or_ex (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ])
 397           (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
 398    (or_ex (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ])
 399    (or_ex (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ])
 400    (or_ex (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ])
 401           (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
 402
 403 (* scrittura byte *)
 404 ndefinition bits_of_exadecim ≝
 405 λe:exadecim.match e with
 406  [ x0 ⇒ quadruple … false false false false
 407  | x1 ⇒ quadruple … false false false true
 408  | x2 ⇒ quadruple … false false true  false
 409  | x3 ⇒ quadruple … false false true  true
 410  | x4 ⇒ quadruple … false true  false false
 411  | x5 ⇒ quadruple … false true  false true
 412  | x6 ⇒ quadruple … false true  true  false
 413  | x7 ⇒ quadruple … false true  true  true
 414  | x8 ⇒ quadruple … true  false false false
 415  | x9 ⇒ quadruple … true  false false true
 416  | xA ⇒ quadruple … true  false true  false
 417  | xB ⇒ quadruple … true  false true  true
 418  | xC ⇒ quadruple … true  true  false false
 419  | xD ⇒ quadruple … true  true  false true
 420  | xE ⇒ quadruple … true  true  true  false
 421  | xF ⇒ quadruple … true  true  true  true
 422  ].
 423
 424 ndefinition bits_of_byte8 ≝
 425 λb:byte8.
 426  mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
 427               (snd4T … (bits_of_exadecim (cnH ? b)))
 428               (thd4T … (bits_of_exadecim (cnH ? b)))
 429               (fth4T … (bits_of_exadecim (cnH ? b)))
 430               (fst4T … (bits_of_exadecim (cnL ? b)))
 431               (snd4T … (bits_of_exadecim (cnL ? b)))
 432               (thd4T … (bits_of_exadecim (cnL ? b)))
 433               (fth4T … (bits_of_exadecim (cnL ? b))).