helm/software/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 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  48 (* posso definire un getter a matrice sull'array *)
  49
  50 ndefinition getn_array16T ≝
  51 λn:exadecim.λT:Type.λp:Array16T T.
  52  match n return λn.(Array16T T) → T with
  53   [ x0 ⇒ a16_1  T | x1 ⇒ a16_2  T | x2 ⇒ a16_3  T | x3 ⇒ a16_4  T
  54   | x4 ⇒ a16_5  T | x5 ⇒ a16_6  T | x6 ⇒ a16_7  T | x7 ⇒ a16_8  T
  55   | x8 ⇒ a16_9  T | x9 ⇒ a16_10 T | xA ⇒ a16_11 T | xB ⇒ a16_12 T
  56   | xC ⇒ a16_13 T | xD ⇒ a16_14 T | xE ⇒ a16_15 T | xF ⇒ a16_16 T
  57   ] p.
  58
  59 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  60 (* posso definire un setter a matrice sull'array *)
  61 ndefinition setn_array16T ≝
  62 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
  63 let e00 ≝ (a16_1 T p) in
  64 let e01 ≝ (a16_2 T p) in
  65 let e02 ≝ (a16_3 T p) in
  66 let e03 ≝ (a16_4 T p) in
  67 let e04 ≝ (a16_5 T p) in
  68 let e05 ≝ (a16_6 T p) in
  69 let e06 ≝ (a16_7 T p) in
  70 let e07 ≝ (a16_8 T p) in
  71 let e08 ≝ (a16_9 T p) in
  72 let e09 ≝ (a16_10 T p) in
  73 let e10 ≝ (a16_11 T p) in
  74 let e11 ≝ (a16_12 T p) in
  75 let e12 ≝ (a16_13 T p) in
  76 let e13 ≝ (a16_14 T p) in
  77 let e14 ≝ (a16_15 T p) in
  78 let e15 ≝ (a16_16 T p) in
  79  match n with
  80   [ x0 ⇒ mk_Array16T T v   e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  81   | x1 ⇒ mk_Array16T T e00 v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  82   | x2 ⇒ mk_Array16T T e00 e01 v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  83   | x3 ⇒ mk_Array16T T e00 e01 e02 v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  84   | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  85   | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  86   | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v   e07 e08 e09 e10 e11 e12 e13 e14 e15
  87   | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v   e08 e09 e10 e11 e12 e13 e14 e15
  88   | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v   e09 e10 e11 e12 e13 e14 e15
  89   | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v   e10 e11 e12 e13 e14 e15
  90   | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v   e11 e12 e13 e14 e15
  91   | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v   e12 e13 e14 e15
  92   | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v   e13 e14 e15
  93   | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v   e14 e15
  94   | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v   e15
  95   | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
  96   ].
  97
  98 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  99 (* posso definire un setter multiplo [m,n] a matrice sull'array *)
 100 (* m ≤ n *)
 101 ndefinition setmn_array16T ≝
 102 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
 103 let e00 ≝ (a16_1 T p) in
 104 let e01 ≝ (a16_2 T p) in
 105 let e02 ≝ (a16_3 T p) in
 106 let e03 ≝ (a16_4 T p) in
 107 let e04 ≝ (a16_5 T p) in
 108 let e05 ≝ (a16_6 T p) in
 109 let e06 ≝ (a16_7 T p) in
 110 let e07 ≝ (a16_8 T p) in
 111 let e08 ≝ (a16_9 T p) in
 112 let e09 ≝ (a16_10 T p) in
 113 let e10 ≝ (a16_11 T p) in
 114 let e11 ≝ (a16_12 T p) in
 115 let e12 ≝ (a16_13 T p) in
 116 let e13 ≝ (a16_14 T p) in
 117 let e14 ≝ (a16_15 T p) in
 118 let e15 ≝ (a16_16 T p) in
 119  match m with
 120   [ x0 ⇒ match n with
 121    [ x0 ⇒ mk_Array16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 122    | x1 ⇒ mk_Array16T T v v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 123    | x2 ⇒ mk_Array16T T v v   v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 124    | x3 ⇒ mk_Array16T T v v   v   v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 125    | x4 ⇒ mk_Array16T T v v   v   v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 126    | x5 ⇒ mk_Array16T T v v   v   v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 127    | x6 ⇒ mk_Array16T T v v   v   v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 128    | x7 ⇒ mk_Array16T T v v   v   v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 129    | x8 ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 130    | x9 ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 131    | xA ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 132    | xB ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 133    | xC ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 134    | xD ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   e14 e15
 135    | xE ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   v   e15
 136    | xF ⇒ mk_Array16T T v v   v   v   v   v   v   v   v   v   v   v   v   v   v   v ]
 137   | x1 ⇒ match n with
 138    [ x0 ⇒ p
 139    | x1 ⇒ mk_Array16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 140    | x2 ⇒ mk_Array16T T e00 v v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 141    | x3 ⇒ mk_Array16T T e00 v v   v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 142    | x4 ⇒ mk_Array16T T e00 v v   v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 143    | x5 ⇒ mk_Array16T T e00 v v   v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 144    | x6 ⇒ mk_Array16T T e00 v v   v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 145    | x7 ⇒ mk_Array16T T e00 v v   v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 146    | x8 ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 147    | x9 ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 148    | xA ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 149    | xB ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 150    | xC ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 151    | xD ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   e14 e15
 152    | xE ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   v   e15
 153    | xF ⇒ mk_Array16T T e00 v v   v   v   v   v   v   v   v   v   v   v   v   v   v ]
 154   | x2 ⇒ match n with
 155    [ x0 ⇒ p | x1 ⇒ p
 156    | x2 ⇒ mk_Array16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 157    | x3 ⇒ mk_Array16T T e00 e01 v v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 158    | x4 ⇒ mk_Array16T T e00 e01 v v   v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 159    | x5 ⇒ mk_Array16T T e00 e01 v v   v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 160    | x6 ⇒ mk_Array16T T e00 e01 v v   v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 161    | x7 ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 162    | x8 ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 163    | x9 ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 164    | xA ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 165    | xB ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   e12 e13 e14 e15
 166    | xC ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   e13 e14 e15
 167    | xD ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   e14 e15
 168    | xE ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   v   e15
 169    | xF ⇒ mk_Array16T T e00 e01 v v   v   v   v   v   v   v   v   v   v   v   v   v ]
 170   | x3 ⇒ match n with
 171    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p
 172    | x3 ⇒ mk_Array16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 173    | x4 ⇒ mk_Array16T T e00 e01 e02 v v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 174    | x5 ⇒ mk_Array16T T e00 e01 e02 v v   v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 175    | x6 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 176    | x7 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 177    | x8 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 178    | x9 ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   e10 e11 e12 e13 e14 e15
 179    | xA ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   e11 e12 e13 e14 e15
 180    | xB ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   e12 e13 e14 e15
 181    | xC ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   e13 e14 e15
 182    | xD ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   e14 e15
 183    | xE ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   v   e15
 184    | xF ⇒ mk_Array16T T e00 e01 e02 v v   v   v   v   v   v   v   v   v   v   v   v ]
 185   | x4 ⇒ match n with
 186    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p
 187    | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 188    | x5 ⇒ mk_Array16T T e00 e01 e02 e03 v v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 189    | x6 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 190    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   e08 e09 e10 e11 e12 e13 e14 e15
 191    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   e09 e10 e11 e12 e13 e14 e15
 192    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   e10 e11 e12 e13 e14 e15
 193    | xA ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   e11 e12 e13 e14 e15
 194    | xB ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   e12 e13 e14 e15
 195    | xC ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   e13 e14 e15
 196    | xD ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   e14 e15
 197    | xE ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   v   e15
 198    | xF ⇒ mk_Array16T T e00 e01 e02 e03 v v   v   v   v   v   v   v   v   v   v   v ]
 199   | x5 ⇒ match n with
 200    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p
 201    | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
 202    | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   e07 e08 e09 e10 e11 e12 e13 e14 e15
 203    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   e08 e09 e10 e11 e12 e13 e14 e15
 204    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   e09 e10 e11 e12 e13 e14 e15
 205    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   e10 e11 e12 e13 e14 e15
 206    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   e11 e12 e13 e14 e15
 207    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   e12 e13 e14 e15
 208    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   e13 e14 e15
 209    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   e14 e15
 210    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   v   e15
 211    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 v v   v   v   v   v   v   v   v   v   v ]
 212   | x6 ⇒ match n with
 213    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p
 214    | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15
 215    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   e08 e09 e10 e11 e12 e13 e14 e15
 216    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   e09 e10 e11 e12 e13 e14 e15
 217    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   e10 e11 e12 e13 e14 e15
 218    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   e11 e12 e13 e14 e15
 219    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   e12 e13 e14 e15
 220    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   e13 e14 e15
 221    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   e14 e15
 222    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   v   e15
 223    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v v   v   v   v   v   v   v   v   v ]
 224   | x7 ⇒ match n with
 225    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p
 226    | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15
 227    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   e09 e10 e11 e12 e13 e14 e15
 228    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   e10 e11 e12 e13 e14 e15
 229    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   e11 e12 e13 e14 e15
 230    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   e12 e13 e14 e15
 231    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   e13 e14 e15
 232    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   e14 e15
 233    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   v   e15
 234    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v v   v   v   v   v   v   v   v ]
 235   | x8 ⇒ match n with
 236    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 237    | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15
 238    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   e10 e11 e12 e13 e14 e15
 239    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   e11 e12 e13 e14 e15
 240    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   e12 e13 e14 e15
 241    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   e13 e14 e15
 242    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   e14 e15
 243    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   v   e15
 244    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v v   v   v   v   v   v   v ]
 245   | x9 ⇒ match n with
 246    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p  | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 247    | x8 ⇒ p
 248    | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15
 249    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   e11 e12 e13 e14 e15
 250    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   e12 e13 e14 e15
 251    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   e13 e14 e15
 252    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   e14 e15
 253    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   v   e15
 254    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v   v   v   v   v   v ]
 255   | xA ⇒ match n with
 256    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 257    | x8 ⇒ p | x9 ⇒ p
 258    | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15
 259    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   e12 e13 e14 e15
 260    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   e13 e14 e15
 261    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   e14 e15
 262    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   v   e15
 263    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v   v   v   v   v ]
 264   | xB ⇒ match n with
 265    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 266    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p
 267    | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15
 268    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   e13 e14 e15
 269    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   e14 e15
 270    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   v   e15
 271    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v   v   v   v ]
 272   | xC ⇒ match n with
 273    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 274    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p
 275    | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15
 276    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   e14 e15
 277    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   v   e15
 278    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v   v   v ]
 279   | xD ⇒ match n with
 280    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 281    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p
 282    | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15
 283    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v   e15
 284    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v   v ]
 285   | xE ⇒ match n with
 286    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 287    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p
 288    | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15
 289    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ]
 290   | xF ⇒ match n with
 291    [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p
 292    | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p
 293    | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ]
 294   ].
 295
 296 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 297 (* posso definire un setter composto [m+1,n-1] a matrice sull'array *)
 298 (* NB: obbiettivo evitare l'overflow *)
 299 ndefinition setmn_array16T_succ_pred ≝
 300 λm,n:exadecim.λT:Type.λp:Array16T T.λv:T.
 301  match lt_ex m xF with
 302   [ true ⇒ match gt_ex n x0 with
 303    [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v
 304    | false ⇒ p
 305    ]
 306   | false ⇒ p
 307   ].
 308
 309 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 310 (* posso definire un setter composto [m+1,F] a matrice sull'array *)
 311 (* NB: obbiettivo evitare l'overflow *)
 312 ndefinition setmn_array16T_succ ≝
 313 λm:exadecim.λT:Type.λp:Array16T T.λv:T.
 314  match lt_ex m xF with
 315   [ true ⇒ setmn_array16T (succ_ex m) xF T p v
 316   | false ⇒ p
 317   ].
 318
 319 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
 320 (* posso definire un setter composto [0,n-1] a matrice sull'array *)
 321 (* NB: obbiettivo evitare l'overflow *)
 322 ndefinition setmn_array16T_pred ≝
 323 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
 324  match gt_ex n x0 with
 325   [ true ⇒ setmn_array16T x0 (pred_ex n) T p v
 326   | false ⇒ p
 327   ].
 328
 329 (* ************************** *)
 330 (* TIPO BYTE COME INSIEME BIT *)
 331 (* ************************** *)
 332
 333 (* definizione di un byte come 8 bit *)
 334 nrecord Array8T (T:Type) : Type ≝
 335 { a8_1  : T ; a8_2  : T ; a8_3  : T ; a8_4  : T
 336 ; a8_5  : T ; a8_6  : T ; a8_7  : T ; a8_8  : T }.
 337
 338 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 339 (* posso definire un getter a matrice sull'array *)
 340 ndefinition getn_array8T ≝
 341 λn:oct.λT:Type.λp:Array8T T.
 342  match n return λn.(Array8T T) → T with
 343   [ o0 ⇒ a8_1  T | o1 ⇒ a8_2  T | o2 ⇒ a8_3  T | o3 ⇒ a8_4  T
 344   | o4 ⇒ a8_5  T | o5 ⇒ a8_6  T | o6 ⇒ a8_7  T | o7 ⇒ a8_8  T
 345   ] p.
 346
 347 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 348 (* posso definire un setter a matrice sull'array *)
 349 ndefinition setn_array8T ≝
 350 λn:oct.λT:Type.λp:Array8T T.λv:T.
 351 let e00 ≝ (a8_1 T p) in
 352 let e01 ≝ (a8_2 T p) in
 353 let e02 ≝ (a8_3 T p) in
 354 let e03 ≝ (a8_4 T p) in
 355 let e04 ≝ (a8_5 T p) in
 356 let e05 ≝ (a8_6 T p) in
 357 let e06 ≝ (a8_7 T p) in
 358 let e07 ≝ (a8_8 T p) in
 359  match n with
 360   [ o0 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 e01 v
 361   | o1 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 v   e00
 362   | o2 ⇒ mk_Array8T T e07 e06 e05 e04 e03 v   e01 e00
 363   | o3 ⇒ mk_Array8T T e07 e06 e05 e04 v   e02 e01 e00
 364   | o4 ⇒ mk_Array8T T e07 e06 e05 v   e03 e02 e01 e00
 365   | o5 ⇒ mk_Array8T T e07 e06 v   e04 e03 e02 e01 e00
 366   | o6 ⇒ mk_Array8T T e07 v   e05 e04 e03 e02 e01 e00
 367   | o7 ⇒ mk_Array8T T v   e06 e05 e04 e03 e02 e01 e00
 368   ].
 369
 370 (* lettura byte *)
 371 ndefinition byte8_of_bits ≝
 372 λp:Array8T bool.
 373    mk_byte8
 374    (or_ex (match a8_8 ? p with [ true ⇒ x8 | false ⇒ x0 ])
 375    (or_ex (match a8_7 ? p with [ true ⇒ x4 | false ⇒ x0 ])
 376    (or_ex (match a8_6 ? p with [ true ⇒ x2 | false ⇒ x0 ])
 377           (match a8_5 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
 378    (or_ex (match a8_4 ? p with [ true ⇒ x8 | false ⇒ x0 ])
 379    (or_ex (match a8_3 ? p with [ true ⇒ x4 | false ⇒ x0 ])
 380    (or_ex (match a8_2 ? p with [ true ⇒ x2 | false ⇒ x0 ])
 381           (match a8_1 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
 382
 383 (* scrittura byte *)
 384 ndefinition bits_of_byte8 ≝
 385 λp:byte8.
 386  match b8h p with
 387   [ x0 ⇒ match b8l p with
 388    [ x0 ⇒ mk_Array8T bool false false false false false false false false
 389    | x1 ⇒ mk_Array8T bool false false false false false false false true
 390    | x2 ⇒ mk_Array8T bool false false false false false false true  false
 391    | x3 ⇒ mk_Array8T bool false false false false false false true  true
 392    | x4 ⇒ mk_Array8T bool false false false false false true  false false
 393    | x5 ⇒ mk_Array8T bool false false false false false true  false true
 394    | x6 ⇒ mk_Array8T bool false false false false false true  true  false
 395    | x7 ⇒ mk_Array8T bool false false false false false true  true  true
 396    | x8 ⇒ mk_Array8T bool false false false false true  false false false
 397    | x9 ⇒ mk_Array8T bool false false false false true  false false true
 398    | xA ⇒ mk_Array8T bool false false false false true  false true  false
 399    | xB ⇒ mk_Array8T bool false false false false true  false true  true
 400    | xC ⇒ mk_Array8T bool false false false false true  true  false false
 401    | xD ⇒ mk_Array8T bool false false false false true  true  false true
 402    | xE ⇒ mk_Array8T bool false false false false true  true  true  false
 403    | xF ⇒ mk_Array8T bool false false false false true  true  true  true ]
 404   | x1 ⇒ match b8l p with
 405    [ x0 ⇒ mk_Array8T bool false false false true  false false false false
 406    | x1 ⇒ mk_Array8T bool false false false true  false false false true
 407    | x2 ⇒ mk_Array8T bool false false false true  false false true  false
 408    | x3 ⇒ mk_Array8T bool false false false true  false false true  true
 409    | x4 ⇒ mk_Array8T bool false false false true  false true  false false
 410    | x5 ⇒ mk_Array8T bool false false false true  false true  false true
 411    | x6 ⇒ mk_Array8T bool false false false true  false true  true  false
 412    | x7 ⇒ mk_Array8T bool false false false true  false true  true  true
 413    | x8 ⇒ mk_Array8T bool false false false true  true  false false false
 414    | x9 ⇒ mk_Array8T bool false false false true  true  false false true
 415    | xA ⇒ mk_Array8T bool false false false true  true  false true  false
 416    | xB ⇒ mk_Array8T bool false false false true  true  false true  true
 417    | xC ⇒ mk_Array8T bool false false false true  true  true  false false
 418    | xD ⇒ mk_Array8T bool false false false true  true  true  false true
 419    | xE ⇒ mk_Array8T bool false false false true  true  true  true  false
 420    | xF ⇒ mk_Array8T bool false false false true  true  true  true  true ]
 421   | x2 ⇒ match b8l p with
 422    [ x0 ⇒ mk_Array8T bool false false true  false false false false false
 423    | x1 ⇒ mk_Array8T bool false false true  false false false false true
 424    | x2 ⇒ mk_Array8T bool false false true  false false false true  false
 425    | x3 ⇒ mk_Array8T bool false false true  false false false true  true
 426    | x4 ⇒ mk_Array8T bool false false true  false false true  false false
 427    | x5 ⇒ mk_Array8T bool false false true  false false true  false true
 428    | x6 ⇒ mk_Array8T bool false false true  false false true  true  false
 429    | x7 ⇒ mk_Array8T bool false false true  false false true  true  true
 430    | x8 ⇒ mk_Array8T bool false false true  false true  false false false
 431    | x9 ⇒ mk_Array8T bool false false true  false true  false false true
 432    | xA ⇒ mk_Array8T bool false false true  false true  false true  false
 433    | xB ⇒ mk_Array8T bool false false true  false true  false true  true
 434    | xC ⇒ mk_Array8T bool false false true  false true  true  false false
 435    | xD ⇒ mk_Array8T bool false false true  false true  true  false true
 436    | xE ⇒ mk_Array8T bool false false true  false true  true  true  false
 437    | xF ⇒ mk_Array8T bool false false true  false true  true  true  true ]
 438   | x3 ⇒ match b8l p with
 439    [ x0 ⇒ mk_Array8T bool false false true  true  false false false false
 440    | x1 ⇒ mk_Array8T bool false false true  true  false false false true
 441    | x2 ⇒ mk_Array8T bool false false true  true  false false true  false
 442    | x3 ⇒ mk_Array8T bool false false true  true  false false true  true
 443    | x4 ⇒ mk_Array8T bool false false true  true  false true  false false
 444    | x5 ⇒ mk_Array8T bool false false true  true  false true  false true
 445    | x6 ⇒ mk_Array8T bool false false true  true  false true  true  false
 446    | x7 ⇒ mk_Array8T bool false false true  true  false true  true  true
 447    | x8 ⇒ mk_Array8T bool false false true  true  true  false false false
 448    | x9 ⇒ mk_Array8T bool false false true  true  true  false false true
 449    | xA ⇒ mk_Array8T bool false false true  true  true  false true  false
 450    | xB ⇒ mk_Array8T bool false false true  true  true  false true  true
 451    | xC ⇒ mk_Array8T bool false false true  true  true  true  false false
 452    | xD ⇒ mk_Array8T bool false false true  true  true  true  false true
 453    | xE ⇒ mk_Array8T bool false false true  true  true  true  true  false
 454    | xF ⇒ mk_Array8T bool false false true  true  true  true  true  true ]
 455   | x4 ⇒ match b8l p with
 456    [ x0 ⇒ mk_Array8T bool false true  false false false false false false
 457    | x1 ⇒ mk_Array8T bool false true  false false false false false true
 458    | x2 ⇒ mk_Array8T bool false true  false false false false true  false
 459    | x3 ⇒ mk_Array8T bool false true  false false false false true  true
 460    | x4 ⇒ mk_Array8T bool false true  false false false true  false false
 461    | x5 ⇒ mk_Array8T bool false true  false false false true  false true
 462    | x6 ⇒ mk_Array8T bool false true  false false false true  true  false
 463    | x7 ⇒ mk_Array8T bool false true  false false false true  true  true
 464    | x8 ⇒ mk_Array8T bool false true  false false true  false false false
 465    | x9 ⇒ mk_Array8T bool false true  false false true  false false true
 466    | xA ⇒ mk_Array8T bool false true  false false true  false true  false
 467    | xB ⇒ mk_Array8T bool false true  false false true  false true  true
 468    | xC ⇒ mk_Array8T bool false true  false false true  true  false false
 469    | xD ⇒ mk_Array8T bool false true  false false true  true  false true
 470    | xE ⇒ mk_Array8T bool false true  false false true  true  true  false
 471    | xF ⇒ mk_Array8T bool false true  false false true  true  true  true ]
 472   | x5 ⇒ match b8l p with
 473    [ x0 ⇒ mk_Array8T bool false true  false true  false false false false
 474    | x1 ⇒ mk_Array8T bool false true  false true  false false false true
 475    | x2 ⇒ mk_Array8T bool false true  false true  false false true  false
 476    | x3 ⇒ mk_Array8T bool false true  false true  false false true  true
 477    | x4 ⇒ mk_Array8T bool false true  false true  false true  false false
 478    | x5 ⇒ mk_Array8T bool false true  false true  false true  false true
 479    | x6 ⇒ mk_Array8T bool false true  false true  false true  true  false
 480    | x7 ⇒ mk_Array8T bool false true  false true  false true  true  true
 481    | x8 ⇒ mk_Array8T bool false true  false true  true  false false false
 482    | x9 ⇒ mk_Array8T bool false true  false true  true  false false true
 483    | xA ⇒ mk_Array8T bool false true  false true  true  false true  false
 484    | xB ⇒ mk_Array8T bool false true  false true  true  false true  true
 485    | xC ⇒ mk_Array8T bool false true  false true  true  true  false false
 486    | xD ⇒ mk_Array8T bool false true  false true  true  true  false true
 487    | xE ⇒ mk_Array8T bool false true  false true  true  true  true  false
 488    | xF ⇒ mk_Array8T bool false true  false true  true  true  true  true ]
 489   | x6 ⇒ match b8l p with
 490    [ x0 ⇒ mk_Array8T bool false true  true  false false false false false
 491    | x1 ⇒ mk_Array8T bool false true  true  false false false false true
 492    | x2 ⇒ mk_Array8T bool false true  true  false false false true  false
 493    | x3 ⇒ mk_Array8T bool false true  true  false false false true  true
 494    | x4 ⇒ mk_Array8T bool false true  true  false false true  false false
 495    | x5 ⇒ mk_Array8T bool false true  true  false false true  false true
 496    | x6 ⇒ mk_Array8T bool false true  true  false false true  true  false
 497    | x7 ⇒ mk_Array8T bool false true  true  false false true  true  true
 498    | x8 ⇒ mk_Array8T bool false true  true  false true  false false false
 499    | x9 ⇒ mk_Array8T bool false true  true  false true  false false true
 500    | xA ⇒ mk_Array8T bool false true  true  false true  false true  false
 501    | xB ⇒ mk_Array8T bool false true  true  false true  false true  true
 502    | xC ⇒ mk_Array8T bool false true  true  false true  true  false false
 503    | xD ⇒ mk_Array8T bool false true  true  false true  true  false true
 504    | xE ⇒ mk_Array8T bool false true  true  false true  true  true  false
 505    | xF ⇒ mk_Array8T bool false true  true  false true  true  true  true ]
 506   | x7 ⇒ match b8l p with
 507    [ x0 ⇒ mk_Array8T bool false true  true  true  false false false false
 508    | x1 ⇒ mk_Array8T bool false true  true  true  false false false true
 509    | x2 ⇒ mk_Array8T bool false true  true  true  false false true  false
 510    | x3 ⇒ mk_Array8T bool false true  true  true  false false true  true
 511    | x4 ⇒ mk_Array8T bool false true  true  true  false true  false false
 512    | x5 ⇒ mk_Array8T bool false true  true  true  false true  false true
 513    | x6 ⇒ mk_Array8T bool false true  true  true  false true  true  false
 514    | x7 ⇒ mk_Array8T bool false true  true  true  false true  true  true
 515    | x8 ⇒ mk_Array8T bool false true  true  true  true  false false false
 516    | x9 ⇒ mk_Array8T bool false true  true  true  true  false false true
 517    | xA ⇒ mk_Array8T bool false true  true  true  true  false true  false
 518    | xB ⇒ mk_Array8T bool false true  true  true  true  false true  true
 519    | xC ⇒ mk_Array8T bool false true  true  true  true  true  false false
 520    | xD ⇒ mk_Array8T bool false true  true  true  true  true  false true
 521    | xE ⇒ mk_Array8T bool false true  true  true  true  true  true  false
 522    | xF ⇒ mk_Array8T bool false true  true  true  true  true  true  true ]
 523   | x8 ⇒ match b8l p with
 524    [ x0 ⇒ mk_Array8T bool true  false false false false false false false
 525    | x1 ⇒ mk_Array8T bool true  false false false false false false true
 526    | x2 ⇒ mk_Array8T bool true  false false false false false true  false
 527    | x3 ⇒ mk_Array8T bool true  false false false false false true  true
 528    | x4 ⇒ mk_Array8T bool true  false false false false true  false false
 529    | x5 ⇒ mk_Array8T bool true  false false false false true  false true
 530    | x6 ⇒ mk_Array8T bool true  false false false false true  true  false
 531    | x7 ⇒ mk_Array8T bool true  false false false false true  true  true
 532    | x8 ⇒ mk_Array8T bool true  false false false true  false false false
 533    | x9 ⇒ mk_Array8T bool true  false false false true  false false true
 534    | xA ⇒ mk_Array8T bool true  false false false true  false true  false
 535    | xB ⇒ mk_Array8T bool true  false false false true  false true  true
 536    | xC ⇒ mk_Array8T bool true  false false false true  true  false false
 537    | xD ⇒ mk_Array8T bool true  false false false true  true  false true
 538    | xE ⇒ mk_Array8T bool true  false false false true  true  true  false
 539    | xF ⇒ mk_Array8T bool true  false false false true  true  true  true ]
 540   | x9 ⇒ match b8l p with
 541    [ x0 ⇒ mk_Array8T bool true  false false true  false false false false
 542    | x1 ⇒ mk_Array8T bool true  false false true  false false false true
 543    | x2 ⇒ mk_Array8T bool true  false false true  false false true  false
 544    | x3 ⇒ mk_Array8T bool true  false false true  false false true  true
 545    | x4 ⇒ mk_Array8T bool true  false false true  false true  false false
 546    | x5 ⇒ mk_Array8T bool true  false false true  false true  false true
 547    | x6 ⇒ mk_Array8T bool true  false false true  false true  true  false
 548    | x7 ⇒ mk_Array8T bool true  false false true  false true  true  true
 549    | x8 ⇒ mk_Array8T bool true  false false true  true  false false false
 550    | x9 ⇒ mk_Array8T bool true  false false true  true  false false true
 551    | xA ⇒ mk_Array8T bool true  false false true  true  false true  false
 552    | xB ⇒ mk_Array8T bool true  false false true  true  false true  true
 553    | xC ⇒ mk_Array8T bool true  false false true  true  true  false false
 554    | xD ⇒ mk_Array8T bool true  false false true  true  true  false true
 555    | xE ⇒ mk_Array8T bool true  false false true  true  true  true  false
 556    | xF ⇒ mk_Array8T bool true  false false true  true  true  true  true ]
 557   | xA ⇒ match b8l p with
 558    [ x0 ⇒ mk_Array8T bool true  false true  false false false false false
 559    | x1 ⇒ mk_Array8T bool true  false true  false false false false true
 560    | x2 ⇒ mk_Array8T bool true  false true  false false false true  false
 561    | x3 ⇒ mk_Array8T bool true  false true  false false false true  true
 562    | x4 ⇒ mk_Array8T bool true  false true  false false true  false false
 563    | x5 ⇒ mk_Array8T bool true  false true  false false true  false true
 564    | x6 ⇒ mk_Array8T bool true  false true  false false true  true  false
 565    | x7 ⇒ mk_Array8T bool true  false true  false false true  true  true
 566    | x8 ⇒ mk_Array8T bool true  false true  false true  false false false
 567    | x9 ⇒ mk_Array8T bool true  false true  false true  false false true
 568    | xA ⇒ mk_Array8T bool true  false true  false true  false true  false
 569    | xB ⇒ mk_Array8T bool true  false true  false true  false true  true
 570    | xC ⇒ mk_Array8T bool true  false true  false true  true  false false
 571    | xD ⇒ mk_Array8T bool true  false true  false true  true  false true
 572    | xE ⇒ mk_Array8T bool true  false true  false true  true  true  false
 573    | xF ⇒ mk_Array8T bool true  false true  false true  true  true  true ]
 574   | xB ⇒ match b8l p with
 575    [ x0 ⇒ mk_Array8T bool true  false true  true  false false false false
 576    | x1 ⇒ mk_Array8T bool true  false true  true  false false false true
 577    | x2 ⇒ mk_Array8T bool true  false true  true  false false true  false
 578    | x3 ⇒ mk_Array8T bool true  false true  true  false false true  true
 579    | x4 ⇒ mk_Array8T bool true  false true  true  false true  false false
 580    | x5 ⇒ mk_Array8T bool true  false true  true  false true  false true
 581    | x6 ⇒ mk_Array8T bool true  false true  true  false true  true  false
 582    | x7 ⇒ mk_Array8T bool true  false true  true  false true  true  true
 583    | x8 ⇒ mk_Array8T bool true  false true  true  true  false false false
 584    | x9 ⇒ mk_Array8T bool true  false true  true  true  false false true
 585    | xA ⇒ mk_Array8T bool true  false true  true  true  false true  false
 586    | xB ⇒ mk_Array8T bool true  false true  true  true  false true  true
 587    | xC ⇒ mk_Array8T bool true  false true  true  true  true  false false
 588    | xD ⇒ mk_Array8T bool true  false true  true  true  true  false true
 589    | xE ⇒ mk_Array8T bool true  false true  true  true  true  true  false
 590    | xF ⇒ mk_Array8T bool true  false true  true  true  true  true  true ]
 591   | xC ⇒ match b8l p with
 592    [ x0 ⇒ mk_Array8T bool true  true  false false false false false false
 593    | x1 ⇒ mk_Array8T bool true  true  false false false false false true
 594    | x2 ⇒ mk_Array8T bool true  true  false false false false true  false
 595    | x3 ⇒ mk_Array8T bool true  true  false false false false true  true
 596    | x4 ⇒ mk_Array8T bool true  true  false false false true  false false
 597    | x5 ⇒ mk_Array8T bool true  true  false false false true  false true
 598    | x6 ⇒ mk_Array8T bool true  true  false false false true  true  false
 599    | x7 ⇒ mk_Array8T bool true  true  false false false true  true  true
 600    | x8 ⇒ mk_Array8T bool true  true  false false true  false false false
 601    | x9 ⇒ mk_Array8T bool true  true  false false true  false false true
 602    | xA ⇒ mk_Array8T bool true  true  false false true  false true  false
 603    | xB ⇒ mk_Array8T bool true  true  false false true  false true  true
 604    | xC ⇒ mk_Array8T bool true  true  false false true  true  false false
 605    | xD ⇒ mk_Array8T bool true  true  false false true  true  false true
 606    | xE ⇒ mk_Array8T bool true  true  false false true  true  true  false
 607    | xF ⇒ mk_Array8T bool true  true  false false true  true  true  true ]
 608   | xD ⇒ match b8l p with
 609    [ x0 ⇒ mk_Array8T bool true  true  false true  false false false false
 610    | x1 ⇒ mk_Array8T bool true  true  false true  false false false true
 611    | x2 ⇒ mk_Array8T bool true  true  false true  false false true  false
 612    | x3 ⇒ mk_Array8T bool true  true  false true  false false true  true
 613    | x4 ⇒ mk_Array8T bool true  true  false true  false true  false false
 614    | x5 ⇒ mk_Array8T bool true  true  false true  false true  false true
 615    | x6 ⇒ mk_Array8T bool true  true  false true  false true  true  false
 616    | x7 ⇒ mk_Array8T bool true  true  false true  false true  true  true
 617    | x8 ⇒ mk_Array8T bool true  true  false true  true  false false false
 618    | x9 ⇒ mk_Array8T bool true  true  false true  true  false false true
 619    | xA ⇒ mk_Array8T bool true  true  false true  true  false true  false
 620    | xB ⇒ mk_Array8T bool true  true  false true  true  false true  true
 621    | xC ⇒ mk_Array8T bool true  true  false true  true  true  false false
 622    | xD ⇒ mk_Array8T bool true  true  false true  true  true  false true
 623    | xE ⇒ mk_Array8T bool true  true  false true  true  true  true  false
 624    | xF ⇒ mk_Array8T bool true  true  false true  true  true  true  true ]
 625   | xE ⇒ match b8l p with
 626    [ x0 ⇒ mk_Array8T bool true  true  true  false false false false false
 627    | x1 ⇒ mk_Array8T bool true  true  true  false false false false true
 628    | x2 ⇒ mk_Array8T bool true  true  true  false false false true  false
 629    | x3 ⇒ mk_Array8T bool true  true  true  false false false true  true
 630    | x4 ⇒ mk_Array8T bool true  true  true  false false true  false false
 631    | x5 ⇒ mk_Array8T bool true  true  true  false false true  false true
 632    | x6 ⇒ mk_Array8T bool true  true  true  false false true  true  false
 633    | x7 ⇒ mk_Array8T bool true  true  true  false false true  true  true
 634    | x8 ⇒ mk_Array8T bool true  true  true  false true  false false false
 635    | x9 ⇒ mk_Array8T bool true  true  true  false true  false false true
 636    | xA ⇒ mk_Array8T bool true  true  true  false true  false true  false
 637    | xB ⇒ mk_Array8T bool true  true  true  false true  false true  true
 638    | xC ⇒ mk_Array8T bool true  true  true  false true  true  false false
 639    | xD ⇒ mk_Array8T bool true  true  true  false true  true  false true
 640    | xE ⇒ mk_Array8T bool true  true  true  false true  true  true  false
 641    | xF ⇒ mk_Array8T bool true  true  true  false true  true  true  true ]
 642   | xF ⇒ match b8l p with
 643    [ x0 ⇒ mk_Array8T bool true  true  true  true  false false false false
 644    | x1 ⇒ mk_Array8T bool true  true  true  true  false false false true
 645    | x2 ⇒ mk_Array8T bool true  true  true  true  false false true  false
 646    | x3 ⇒ mk_Array8T bool true  true  true  true  false false true  true
 647    | x4 ⇒ mk_Array8T bool true  true  true  true  false true  false false
 648    | x5 ⇒ mk_Array8T bool true  true  true  true  false true  false true
 649    | x6 ⇒ mk_Array8T bool true  true  true  true  false true  true  false
 650    | x7 ⇒ mk_Array8T bool true  true  true  true  false true  true  true
 651    | x8 ⇒ mk_Array8T bool true  true  true  true  true  false false false
 652    | x9 ⇒ mk_Array8T bool true  true  true  true  true  false false true
 653    | xA ⇒ mk_Array8T bool true  true  true  true  true  false true  false
 654    | xB ⇒ mk_Array8T bool true  true  true  true  true  false true  true
 655    | xC ⇒ mk_Array8T bool true  true  true  true  true  true  false false
 656    | xD ⇒ mk_Array8T bool true  true  true  true  true  true  false true
 657    | xE ⇒ mk_Array8T bool true  true  true  true  true  true  true  false
 658    | xF ⇒ mk_Array8T bool true  true  true  true  true  true  true  true ]
 659   ].