helm/software/matita/contribs/ng_assembly2/num/word32.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/word16.ma".
  24
  25 (* ***** *)
  26 (* DWORD *)
  27 (* ***** *)
  28
  29 ndefinition word32 ≝ comp_num word16.
  30 ndefinition mk_word32 ≝ λw1,w2.mk_comp_num word16 w1 w2.
  31
  32 (* \langle \rangle *)
  33 notation "〈x.y〉" non associative with precedence 80
  34  for @{ mk_comp_num word16 $x $y }.
  35
  36 ndefinition word32_is_comparable ≝ cn_is_comparable word16_is_comparable.
  37 ndefinition word32_is_comparable_ext ≝ cn_is_comparable_ext word16_is_comparable_ext.
  38 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ comp_num (comp_num (comp_num exadecim)).
  39 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ comp_num (comp_num byte8).
  40 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ comp_num word16.
  41 unification hint 0 ≔ ⊢ carr (comp_base word32_is_comparable_ext) ≡ word32.
  42 unification hint 0 ≔ ⊢ carr word32_is_comparable ≡ comp_num (comp_num (comp_num exadecim)).
  43 unification hint 0 ≔ ⊢ carr word32_is_comparable ≡ comp_num (comp_num byte8).
  44 unification hint 0 ≔ ⊢ carr word32_is_comparable ≡ comp_num word16.
  45 unification hint 0 ≔ ⊢ carr word32_is_comparable ≡ word32.
  46
  47 (* operatore estensione unsigned *)
  48 ndefinition extu_w32 ≝ λw2.〈zeroc ?.w2〉.
  49 ndefinition extu2_w32 ≝ λb2.〈zeroc ?.〈zeroc ?:b2〉〉.
  50 ndefinition extu3_w32 ≝ λe2.〈zeroc ?.〈zeroc ?:〈zeroc ?,e2〉〉〉.
  51
  52 (* operatore estensione signed *)
  53 ndefinition exts_w32 ≝
  54 λw2.〈(match getMSBc ? w2 with
  55       [ true ⇒ predc ? (zeroc ?) | false ⇒ zeroc ? ]).w2〉.
  56 ndefinition exts2_w32 ≝
  57 λb2.(match getMSBc ? b2 with
  58       [ true ⇒ 〈predc ? (zeroc ?).〈predc ? (zeroc ?):b2〉〉
  59       | false ⇒ 〈zeroc ?.〈zeroc ?:b2〉〉 ]).
  60 ndefinition exts3_w32 ≝
  61 λe2.(match getMSBc ? e2 with
  62       [ true ⇒ 〈predc ? (zeroc ?).〈predc ? (zeroc ?):〈predc ? (zeroc ?),e2〉〉〉
  63       | false ⇒ 〈zeroc ?.〈zeroc ?:〈zeroc ?,e2〉〉〉 ]).
  64
  65 (* operatore moltiplicazione senza segno *)
  66 (* 〈a1,a2〉 * 〈b1,b2〉 = (a1*b1) x0 x0 + x0 (a1*b2) x0 + x0 (a2*b1) x0 + x0 x0 (a2*b2) *)
  67 ndefinition mulu_w16_aux ≝
  68 λw:word32.nat_it ? (rolc ?) w nat8.
  69
  70 ndefinition mulu_w16 ≝
  71 λw1,w2:word16.
  72  plusc_d_d ? 〈(mulu_b8 (cnH ? w1) (cnH ? w2)).zeroc ?〉
  73  (plusc_d_d ? (mulu_w16_aux (extu_w32 (mulu_b8 (cnH ? w1) (cnL ? w2))))
  74   (plusc_d_d ? (mulu_w16_aux (extu_w32 (mulu_b8 (cnL ? w1) (cnH ? w2))))
  75                 (extu_w32 (mulu_b8 (cnL ? w1) (cnL ? w2))))).
  76
  77 (* operatore moltiplicazione con segno *)
  78 (* x * y = sgn(x) * sgn(y) * |x| * |y| *)
  79 ndefinition muls_w16 ≝
  80 λw1,w2:word16.
  81 (* ++/-- → +, +-/-+ → - *)
  82  match (getMSBc ? w1) ⊙ (getMSBc ? w2) with
  83   (* +- -+ → - *)
  84   [ true ⇒ complc ?
  85   (* ++/-- → + *)
  86   | false ⇒ λx.x ] (mulu_w16 (absc ? w1) (absc ? w2)).