matitaB/matita/contribs/ng_assembly2/emulator/memory/memory_struct_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 "num/byte8.ma".
  24
  25 (* **************** *)
  26 (* TIPO ARRAY DA 16 *)
  27 (* **************** *)
  28
  29 (* definizione di un array omogeneo di dimensione 16 *)
  30 nrecord Array16T (T:Type) : Type ≝
  31 { a16_1  : T ; a16_2  : T ; a16_3  : T ; a16_4  : T
  32 ; a16_5  : T ; a16_6  : T ; a16_7  : T ; a16_8  : T
  33 ; a16_9  : T ; a16_10 : T ; a16_11 : T ; a16_12 : T
  34 ; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }.
  35
  36 (* operatore uguaglianza *)
  37 ndefinition eq_ar16 ≝
  38 λT.λf:T → T → bool.λa1,a2:Array16T T.
  39  (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗
  40  (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗
  41  (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗
  42  (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗
  43  (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗
  44  (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗
  45  (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗
  46  (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)).
  47
  48 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  49 (* posso definire un getter a matrice sull'array *)
  50
  51 ndefinition getn_array16T ≝
  52 λn:exadecim.λT:Type.λp:Array16T T.
  53  match n return λn.(Array16T T) → T with
  54   [ x0 ⇒ a16_1  T | x1 ⇒ a16_2  T | x2 ⇒ a16_3  T | x3 ⇒ a16_4  T
  55   | x4 ⇒ a16_5  T | x5 ⇒ a16_6  T | x6 ⇒ a16_7  T | x7 ⇒ a16_8  T
  56   | x8 ⇒ a16_9  T | x9 ⇒ a16_10 T | xA ⇒ a16_11 T | xB ⇒ a16_12 T
  57   | xC ⇒ a16_13 T | xD ⇒ a16_14 T | xE ⇒ a16_15 T | xF ⇒ a16_16 T
  58   ] p.
  59
  60 (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
  61 (* posso definire un setter a matrice sull'array *)
  62 ndefinition setn_array16T ≝
  63 λn:exadecim.λT:Type.λp:Array16T T.λv:T.
  64 let e00 ≝ (a16_1 T p) in
  65 let e01 ≝ (a16_2 T p) in
  66 let e02 ≝ (a16_3 T p) in
  67 let e03 ≝ (a16_4 T p) in
  68 let e04 ≝ (a16_5 T p) in
  69 let e05 ≝ (a16_6 T p) in
  70 let e06 ≝ (a16_7 T p) in
  71 let e07 ≝ (a16_8 T p) in
  72 let e08 ≝ (a16_9 T p) in
  73 let e09 ≝ (a16_10 T p) in
  74 let e10 ≝ (a16_11 T p) in
  75 let e11 ≝ (a16_12 T p) in
  76 let e12 ≝ (a16_13 T p) in
  77 let e13 ≝ (a16_14 T p) in
  78 let e14 ≝ (a16_15 T p) in
  79 let e15 ≝ (a16_16 T p) in
  80  match n with
  81   [ x0 ⇒ mk_Array16T T v   e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  82   | x1 ⇒ mk_Array16T T e00 v   e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  83   | x2 ⇒ mk_Array16T T e00 e01 v   e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  84   | x3 ⇒ mk_Array16T T e00 e01 e02 v   e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  85   | x4 ⇒ mk_Array16T T e00 e01 e02 e03 v   e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  86   | x5 ⇒ mk_Array16T T e00 e01 e02 e03 e04 v   e06 e07 e08 e09 e10 e11 e12 e13 e14 e15
  87   | x6 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 v   e07 e08 e09 e10 e11 e12 e13 e14 e15
  88   | x7 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 v   e08 e09 e10 e11 e12 e13 e14 e15
  89   | x8 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 v   e09 e10 e11 e12 e13 e14 e15
  90   | x9 ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v   e10 e11 e12 e13 e14 e15
  91   | xA ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v   e11 e12 e13 e14 e15
  92   | xB ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v   e12 e13 e14 e15
  93   | xC ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v   e13 e14 e15
  94   | xD ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v   e14 e15
  95   | xE ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v   e15
  96   | xF ⇒ mk_Array16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v
  97   ].
  98
  99 (* ************************** *)
 100 (* TIPO BYTE COME INSIEME BIT *)
 101 (* ************************** *)
 102
 103 (* definizione di un byte come 8 bit *)
 104 nrecord Array8T (T:Type) : Type ≝
 105 { a8_1  : T ; a8_2  : T ; a8_3  : T ; a8_4  : T
 106 ; a8_5  : T ; a8_6  : T ; a8_7  : T ; a8_8  : T }.
 107
 108 (* operatore uguaglianza *)
 109 ndefinition eq_ar8 ≝
 110 λT.λf:T → T → bool.λa1,a2:Array8T T.
 111  (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗
 112  (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗
 113  (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗
 114  (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)).
 115
 116 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 117 (* posso definire un getter a matrice sull'array *)
 118 ndefinition getn_array8T ≝
 119 λn:oct.λT:Type.λp:Array8T T.
 120  match n return λn.(Array8T T) → T with
 121   [ o0 ⇒ a8_1  T | o1 ⇒ a8_2  T | o2 ⇒ a8_3  T | o3 ⇒ a8_4  T
 122   | o4 ⇒ a8_5  T | o5 ⇒ a8_6  T | o6 ⇒ a8_7  T | o7 ⇒ a8_8  T
 123   ] p.
 124
 125 (* abbiamo gia' gli ottali come tipo induttivo quindi: *)
 126 (* posso definire un setter a matrice sull'array *)
 127 ndefinition setn_array8T ≝
 128 λn:oct.λT:Type.λp:Array8T T.λv:T.
 129 let e00 ≝ (a8_1 T p) in
 130 let e01 ≝ (a8_2 T p) in
 131 let e02 ≝ (a8_3 T p) in
 132 let e03 ≝ (a8_4 T p) in
 133 let e04 ≝ (a8_5 T p) in
 134 let e05 ≝ (a8_6 T p) in
 135 let e06 ≝ (a8_7 T p) in
 136 let e07 ≝ (a8_8 T p) in
 137  match n with
 138   [ o0 ⇒ mk_Array8T T v   e01 e02 e03 e04 e05 e06 e07
 139   | o1 ⇒ mk_Array8T T e00 v   e02 e03 e04 e05 e06 e07
 140   | o2 ⇒ mk_Array8T T e00 e01 v   e03 e04 e05 e06 e07
 141   | o3 ⇒ mk_Array8T T e00 e01 e02 v   e04 e05 e06 e07
 142   | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v   e05 e06 e07
 143   | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v   e06 e07
 144   | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v   e07
 145   | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v
 146   ].
 147
 148 (* lettura byte *)
 149 ndefinition byte8_of_bits ≝
 150 λp:Array8T bool.
 151    mk_byte8
 152    (orc ? (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ])
 153    (orc ? (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ])
 154    (orc ? (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ])
 155           (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
 156    (orc ? (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ])
 157    (orc ? (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ])
 158    (orc ? (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ])
 159           (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
 160
 161 (* scrittura byte *)
 162 ndefinition bits_of_exadecim ≝
 163 λe:exadecim.match e with
 164  [ x0 ⇒ quadruple … false false false false
 165  | x1 ⇒ quadruple … false false false true
 166  | x2 ⇒ quadruple … false false true  false
 167  | x3 ⇒ quadruple … false false true  true
 168  | x4 ⇒ quadruple … false true  false false
 169  | x5 ⇒ quadruple … false true  false true
 170  | x6 ⇒ quadruple … false true  true  false
 171  | x7 ⇒ quadruple … false true  true  true
 172  | x8 ⇒ quadruple … true  false false false
 173  | x9 ⇒ quadruple … true  false false true
 174  | xA ⇒ quadruple … true  false true  false
 175  | xB ⇒ quadruple … true  false true  true
 176  | xC ⇒ quadruple … true  true  false false
 177  | xD ⇒ quadruple … true  true  false true
 178  | xE ⇒ quadruple … true  true  true  false
 179  | xF ⇒ quadruple … true  true  true  true
 180  ].
 181
 182 ndefinition bits_of_byte8 ≝
 183 λb:byte8.
 184  mk_Array8T ? (fst4T … (bits_of_exadecim (cnH ? b)))
 185               (snd4T … (bits_of_exadecim (cnH ? b)))
 186               (thd4T … (bits_of_exadecim (cnH ? b)))
 187               (fth4T … (bits_of_exadecim (cnH ? b)))
 188               (fst4T … (bits_of_exadecim (cnL ? b)))
 189               (snd4T … (bits_of_exadecim (cnL ? b)))
 190               (thd4T … (bits_of_exadecim (cnL ? b)))
 191               (fth4T … (bits_of_exadecim (cnL ? b))).