helm/software/matita/contribs/ng_assembly/num/word24.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 (* BYTE+WORD *)
  27 (* ********* *)
  28
  29 nrecord word24 : Type ≝
  30  {
  31  w24x: byte8;
  32  w24h: byte8;
  33  w24l: byte8
  34  }.
  35
  36 (* \langle \rangle *)
  37 notation "〈x;y;z〉" non associative with precedence 80
  38  for @{ 'mk_word24 $x $y $z }.
  39 interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
  40
  41 (* operatore = *)
  42 ndefinition eq_w24 ≝
  43 λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
  44        (eq_b8 (w24h w1) (w24h w2)) ⊗
  45        (eq_b8 (w24l w1) (w24l w2)).
  46
  47 (* operatore < *)
  48 ndefinition lt_w24 ≝
  49 λw1,w2:word24.
  50  (lt_b8 (w24x w1) (w24x w2)) ⊕
  51  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
  52                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (lt_b8 (w24l w1) (w24l w2))))).
  53
  54 (* operatore ≤ *)
  55 ndefinition le_w24 ≝
  56 λw1,w2:word24.
  57  (lt_b8 (w24x w1) (w24x w2)) ⊕
  58  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
  59                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (le_b8 (w24l w1) (w24l w2))))).
  60
  61 (* operatore > *)
  62 ndefinition gt_w24 ≝
  63 λw1,w2:word24.
  64  (gt_b8 (w24x w1) (w24x w2)) ⊕
  65  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
  66                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (gt_b8 (w24l w1) (w24l w2))))).
  67
  68 (* operatore ≥ *)
  69 ndefinition ge_w24 ≝
  70 λw1,w2:word24.
  71  (gt_b8 (w24x w1) (w24x w2)) ⊕
  72  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
  73                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (ge_b8 (w24l w1) (w24l w2))))).
  74
  75 (* operatore and *)
  76 ndefinition and_w24 ≝
  77 λw1,w2:word24.
  78  mk_word24 (and_b8 (w24x w1) (w24x w2))
  79            (and_b8 (w24h w1) (w24h w2))
  80            (and_b8 (w24l w1) (w24l w2)).
  81
  82 (* operatore or *)
  83 ndefinition or_w24 ≝
  84 λw1,w2:word24.
  85  mk_word24 (or_b8 (w24x w1) (w24x w2))
  86            (or_b8 (w24h w1) (w24h w2))
  87            (or_b8 (w24l w1) (w24l w2)).
  88
  89 (* operatore xor *)
  90 ndefinition xor_w24 ≝
  91 λw1,w2:word24.
  92  mk_word24 (xor_b8 (w24x w1) (w24x w2))
  93            (xor_b8 (w24h w1) (w24h w2))
  94            (xor_b8 (w24l w1) (w24l w2)).
  95
  96 (* operatore rotazione destra con carry *)
  97 ndefinition rcr_w24 ≝
  98 λw:word24.λc:bool.match rcr_b8 (w24x w) c with
  99  [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
 100   [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
 101    [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
 102
 103 (* operatore shift destro *)
 104 ndefinition shr_w24 ≝
 105 λw:word24.match shr_b8 (w24x w) with
 106  [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
 107   [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
 108    [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
 109
 110 (* operatore rotazione destra *)
 111 ndefinition ror_w24 ≝
 112 λw:word24.match shr_b8 (w24x w) with
 113  [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
 114   [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
 115    [ pair wl' c''' ⇒ match c''' with
 116     [ true ⇒ mk_word24 (or_b8 (mk_byte8 x8 x0) wx') wh' wl'
 117     | false ⇒ mk_word24 wx' wh' wl' ]]]].
 118
 119 (* operatore rotazione destra n-volte *)
 120 nlet rec ror_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
 121  match rt with
 122   [ bi_O ⇒ w
 123   | bi_S t' n' ⇒ ror_w24_n (ror_w24 w) t' n' ].
 124
 125 (* operatore rotazione sinistra con carry *)
 126 ndefinition rcl_w24 ≝
 127 λw:word24.λc:bool.match rcl_b8 (w24l w) c with
 128  [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
 129   [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
 130    [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
 131
 132 (* operatore shift sinistro *)
 133 ndefinition shl_w24 ≝
 134 λw:word24.match shl_b8 (w24l w) with
 135  [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
 136   [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
 137    [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
 138
 139 (* operatore rotazione sinistra *)
 140 ndefinition rol_w24 ≝
 141 λw:word24.match shl_b8 (w24l w) with
 142  [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
 143   [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
 144    [ pair wx' c''' ⇒ match c''' with
 145     [ true ⇒ mk_word24 wx' wh' (or_b8 (mk_byte8 x0 x1) wl')
 146     | false ⇒ mk_word24 wx' wh' wl' ]]]].
 147
 148 (* operatore rotazione sinistra n-volte *)
 149 nlet rec rol_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
 150  match rt with
 151   [ bi_O ⇒ w
 152   | bi_S t' n' ⇒ rol_w24_n (rol_w24 w) t' n' ].
 153
 154 (* operatore not/complemento a 1 *)
 155 ndefinition not_w24 ≝
 156 λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
 157
 158 (* operatore somma con data+carry → data+carry *)
 159 ndefinition plus_w24_dc_dc ≝
 160 λw1,w2:word24.λc:bool.
 161  match plus_b8_dc_dc (w24l w1) (w24l w2) c with
 162   [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
 163    [ pair h c'' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c'' with
 164     [ pair x c''' ⇒ pair … 〈x;h;l〉 c''' ]]].
 165
 166 (* operatore somma con data+carry → data *)
 167 ndefinition plus_w24_dc_d ≝
 168 λw1,w2:word24.λc:bool.
 169  match plus_b8_dc_dc (w24l w1) (w24l w2) c with
 170   [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
 171    [ pair h c'' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c'';h;l〉 ]].
 172
 173 (* operatore somma con data+carry → c *)
 174 ndefinition plus_w24_dc_c ≝
 175 λw1,w2:word24.λc:bool.
 176  plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_dc_c (w24l w1) (w24l w2) c)).
 177
 178 (* operatore somma con data → data+carry *)
 179 ndefinition plus_w24_d_dc ≝
 180 λw1,w2:word24.
 181  match plus_b8_d_dc (w24l w1) (w24l w2) with
 182   [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
 183    [ pair h c' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c' with
 184     [ pair x c'' ⇒ pair … 〈x;h;l〉 c'' ]]].
 185
 186 (* operatore somma con data → data *)
 187 ndefinition plus_w24_d_d ≝
 188 λw1,w2:word24.
 189  match plus_b8_d_dc (w24l w1) (w24l w2) with
 190   [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
 191    [ pair h c' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c';h;l〉 ]].
 192
 193 (* operatore somma con data → c *)
 194 ndefinition plus_w24_d_c ≝
 195 λw1,w2:word24.
 196  plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_d_c (w24l w1) (w24l w2))).
 197
 198 (* operatore Most Significant Bit *)
 199 ndefinition MSB_w24 ≝ λw:word24.eq_ex x8 (and_ex x8 (b8h (w24x w))).
 200
 201 (* operatore predecessore *)
 202 ndefinition pred_w24 ≝
 203 λw:word24.match eq_b8 (w24l w) (mk_byte8 x0 x0) with
 204  [ true ⇒ match eq_b8 (w24h w) (mk_byte8 x0 x0) with
 205   [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
 206   | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
 207  | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
 208
 209 (* operatore successore *)
 210 ndefinition succ_w24 ≝
 211 λw:word24.match eq_b8 (w24l w) (mk_byte8 xF xF) with
 212  [ true ⇒ match eq_b8 (w24h w) (mk_byte8 xF xF) with
 213   [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
 214   | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
 215  | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
 216
 217 (* operatore neg/complemento a 2 *)
 218 ndefinition compl_w24 ≝
 219 λw:word24.match MSB_w24 w with
 220  [ true ⇒ succ_w24 (not_w24 w)
 221  | false ⇒ not_w24 (pred_w24 w) ].
 222
 223 (* operatore x in [inf,sup] o in sup],[inf *)
 224 ndefinition inrange_w24 ≝
 225 λx,inf,sup:word24.
 226  match le_w24 inf sup with
 227   [ true ⇒ and_bool | false ⇒ or_bool ]
 228  (le_w24 inf x) (le_w24 x sup).
 229
 230 (* iteratore sulle word *)
 231 ndefinition forall_w24 ≝
 232  λP.
 233   forall_b8 (λbx.
 234   forall_b8 (λbh.
 235   forall_b8 (λbl.
 236    P (mk_word24 bx bh bl )))).