matita/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 (* iteratore sulle word *)
  42 ndefinition forall_w24 ≝
  43  λP.
  44   forall_b8 (λbx.
  45   forall_b8 (λbh.
  46   forall_b8 (λbl.
  47    P (mk_word24 bx bh bl )))).
  48
  49 (* operatore = *)
  50 ndefinition eq_w24 ≝
  51 λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
  52        (eq_b8 (w24h w1) (w24h w2)) ⊗
  53        (eq_b8 (w24l w1) (w24l w2)).
  54
  55 (* operatore < *)
  56 ndefinition lt_w24 ≝
  57 λw1,w2:word24.
  58  (lt_b8 (w24x w1) (w24x w2)) ⊕
  59  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
  60                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (lt_b8 (w24l w1) (w24l w2))))).
  61
  62 (* operatore ≤ *)
  63 ndefinition le_w24 ≝
  64 λw1,w2:word24.
  65  (lt_b8 (w24x w1) (w24x w2)) ⊕
  66  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
  67                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (le_b8 (w24l w1) (w24l w2))))).
  68
  69 (* operatore > *)
  70 ndefinition gt_w24 ≝
  71 λw1,w2:word24.
  72  (gt_b8 (w24x w1) (w24x w2)) ⊕
  73  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
  74                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (gt_b8 (w24l w1) (w24l w2))))).
  75
  76 (* operatore ≥ *)
  77 ndefinition ge_w24 ≝
  78 λw1,w2:word24.
  79  (gt_b8 (w24x w1) (w24x w2)) ⊕
  80  ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
  81                                  ((eq_b8 (w24h w1) (w24h w2)) ⊗ (ge_b8 (w24l w1) (w24l w2))))).
  82
  83 (* operatore and *)
  84 ndefinition and_w24 ≝
  85 λw1,w2:word24.
  86  mk_word24 (and_b8 (w24x w1) (w24x w2))
  87            (and_b8 (w24h w1) (w24h w2))
  88            (and_b8 (w24l w1) (w24l w2)).
  89
  90 (* operatore or *)
  91 ndefinition or_w24 ≝
  92 λw1,w2:word24.
  93  mk_word24 (or_b8 (w24x w1) (w24x w2))
  94            (or_b8 (w24h w1) (w24h w2))
  95            (or_b8 (w24l w1) (w24l w2)).
  96
  97 (* operatore xor *)
  98 ndefinition xor_w24 ≝
  99 λw1,w2:word24.
 100  mk_word24 (xor_b8 (w24x w1) (w24x w2))
 101            (xor_b8 (w24h w1) (w24h w2))
 102            (xor_b8 (w24l w1) (w24l w2)).
 103
 104 (* operatore Most Significant Bit *)
 105 ndefinition getMSB_w24 ≝ λw:word24.getMSB_b8 (w24x w).
 106 ndefinition setMSB_w24 ≝ λw:word24.mk_word24 (setMSB_b8 (w24x w)) (w24h w) (w24l w).
 107 ndefinition clrMSB_w24 ≝ λw:word24.mk_word24 (clrMSB_b8 (w24x w)) (w24h w) (w24l w).
 108
 109 (* operatore Least Significant Bit *)
 110 ndefinition getLSB_w24 ≝ λw:word24.getLSB_b8 (w24l w).
 111 ndefinition setLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (setLSB_b8 (w24l w)).
 112 ndefinition clrLSB_w24 ≝ λw:word24.mk_word24 (w24x w) (w24h w) (clrLSB_b8 (w24l w)).
 113
 114 (* operatore rotazione destra con carry *)
 115 ndefinition rcr_w24 ≝
 116 λc:bool.λw:word24.match rcr_b8 c (w24x w) with
 117  [ pair c' wx' ⇒ match rcr_b8 c' (w24h w) with
 118   [ pair c'' wh' ⇒ match rcr_b8 c'' (w24l w) with
 119    [ pair c''' wl' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
 120
 121 (* operatore shift destro *)
 122 ndefinition shr_w24 ≝ rcr_w24 false.
 123
 124 (* operatore rotazione destra *)
 125 ndefinition ror_w24 ≝
 126 λw.match shr_w24 w with
 127  [ pair c w' ⇒ match c with
 128   [ true ⇒ setMSB_w24 w' | false ⇒ w' ]].
 129
 130 (* operatore rotazione sinistra con carry *)
 131 ndefinition rcl_w24 ≝
 132 λc:bool.λw:word24.match rcl_b8 c (w24l w) with
 133  [ pair c' wl' ⇒ match rcl_b8 c' (w24h w) with
 134   [ pair c'' wh' ⇒ match rcl_b8 c'' (w24x w) with
 135    [ pair c''' wx' ⇒ pair … c''' (mk_word24 wx' wh' wl') ]]].
 136
 137 (* operatore shift sinistro *)
 138 ndefinition shl_w24 ≝ rcl_w24 false.
 139
 140 (* operatore rotazione sinistra *)
 141 ndefinition rol_w24 ≝
 142 λw.match shl_w24 w with
 143  [ pair c w' ⇒ match c with
 144   [ true ⇒ setLSB_w24 w' | false ⇒ w' ]].
 145
 146 (* operatore not/complemento a 1 *)
 147 ndefinition not_w24 ≝
 148 λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
 149
 150 (* operatore somma con data+carry → data+carry *)
 151 ndefinition plus_w24_dc_dc ≝
 152 λc:bool.λw1,w2:word24.
 153  match plus_b8_dc_dc c (w24l w1) (w24l w2) with
 154   [ pair c' l ⇒ match plus_b8_dc_dc c' (w24h w1) (w24h w2) with
 155    [ pair c'' h ⇒ match plus_b8_dc_dc c'' (w24x w1) (w24x w2) with
 156     [ pair c''' x ⇒ pair … c''' 〈x;h;l〉 ]]].
 157
 158 (* operatore somma con data+carry → data *)
 159 ndefinition plus_w24_dc_d ≝ λc,w1,w2.snd … (plus_w24_dc_dc c w1 w2).
 160
 161 (* operatore somma con data+carry → c *)
 162 ndefinition plus_w24_dc_c ≝ λc,w1,w2.fst … (plus_w24_dc_dc c w1 w2).
 163
 164 (* operatore somma con data → data+carry *)
 165 ndefinition plus_w24_d_dc ≝ plus_w24_dc_dc false.
 166
 167 (* operatore somma con data → data *)
 168 ndefinition plus_w24_d_d ≝ λw1,w2.snd … (plus_w24_d_dc w1 w2).
 169
 170 (* operatore somma con data → c *)
 171 ndefinition plus_w24_d_c ≝ λw1,w2.fst … (plus_w24_d_dc w1 w2).
 172
 173 (* operatore predecessore *)
 174 ndefinition pred_w24 ≝
 175 λw:word24.match eq_b8 (w24l w) 〈x0,x0〉 with
 176  [ true ⇒ match eq_b8 (w24h w) 〈x0,x0〉 with
 177   [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
 178   | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
 179  | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
 180
 181 (* operatore successore *)
 182 ndefinition succ_w24 ≝
 183 λw:word24.match eq_b8 (w24l w) 〈xF,xF〉 with
 184  [ true ⇒ match eq_b8 (w24h w) 〈xF,xF〉 with
 185   [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
 186   | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
 187  | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
 188
 189 (* operatore neg/complemento a 2 *)
 190 ndefinition compl_w24 ≝
 191 λw:word24.match getMSB_w24 w with
 192  [ true ⇒ succ_w24 (not_w24 w)
 193  | false ⇒ not_w24 (pred_w24 w) ].
 194
 195 (* operatore abs *)
 196 ndefinition abs_w24 ≝
 197 λw:word24.match getMSB_w24 w with
 198  [ true ⇒ compl_w24 w | false ⇒ w ].
 199
 200 (* operatore x in [inf,sup] o in sup],[inf *)
 201 ndefinition inrange_w24 ≝
 202 λx,inf,sup:word24.
 203  match le_w24 inf sup with
 204   [ true ⇒ and_bool | false ⇒ or_bool ]
 205  (le_w24 inf x) (le_w24 x sup).