1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/exadecim.ma".
29 nrecord comp_num (T:Type) : Type ≝
35 ndefinition forall_cn ≝
36 λT.λf:(T → bool) → bool.λP.
39 P (mk_comp_num T h l))).
45 (feq (cnH ? cn1) (cnH ? cn2)) ⊗ (feq (cnL ? cn1) (cnL ? cn2)).
50 (feq (cnH ? cn)) ⊗ (feq (cnL ? cn)).
54 λT.λfeq:T → T → bool.λfltgt:T → T → bool.
56 (fltgt (cnH ? cn1) (cnH ? cn2)) ⊕
57 ((feq (cnH ? cn1) (cnH ? cn2)) ⊗ (fltgt (cnL ? cn1) (cnL ? cn2))).
61 λT.λfeq:T → T → bool.λfltgt:T → T → bool.λflege:T → T → bool.
63 (fltgt (cnH ? cn1) (cnH ? cn2)) ⊕
64 ((feq (cnH ? cn1) (cnH ? cn2)) ⊗ (flege (cnL ? cn1) (cnL ? cn2))).
66 (* operatore cn1 op cn2 *)
70 mk_comp_num ? (fop (cnH ? cn1) (cnH ? cn2)) (fop (cnL ? cn1) (cnL ? cn2)).
75 mk_comp_num ? (fop (cnH ? cn)) (fop (cnL ? cn)).
77 (* operatore su parte high *)
78 ndefinition getOPH_cn ≝
83 ndefinition setOPH_cn ≝
86 mk_comp_num ? (f (cnH ? cn)) (cnL ? cn).
88 (* operatore su parte low *)
89 ndefinition getOPL_cn ≝
94 ndefinition setOPL_cn ≝
97 mk_comp_num ? (cnH ? cn) (f (cnL ? cn)).
99 (* operatore pred/succ *)
100 ndefinition predsucc_cn ≝
101 λT.λfz:T → bool.λfps:T → T.
103 match fz (cnL ? cn) with
104 [ true ⇒ mk_comp_num ? (fps (cnH ? cn)) (fps (cnL ? cn))
105 | false ⇒ mk_comp_num ? (cnH ? cn) (fps (cnL ? cn)) ].
107 (* operatore con carry applicato DX → SX *)
108 ndefinition opcr2_cn ≝
109 λT.λfopcr:bool → T → T → (ProdT bool T).
110 λc:bool.λcn1,cn2:comp_num T.
111 match fopcr c (cnH ? cn1) (cnH ? cn2) with
112 [ pair c' cnh' ⇒ match fopcr c' (cnL ? cn1) (cnL ? cn2) with
113 [ pair c'' cnl' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].
115 ndefinition opcr_cn ≝
116 λT.λfopcr:bool → T → (ProdT bool T).
117 λc:bool.λcn:comp_num T.
118 match fopcr c (cnH ? cn) with
119 [ pair c' cnh' ⇒ match fopcr c' (cnL ? cn) with
120 [ pair c'' cnl' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].
122 (* operatore con carry applicato SX → DX *)
123 ndefinition opcl2_cn ≝
124 λT.λfopcl:bool → T → T → (ProdT bool T).
125 λc:bool.λcn1,cn2:comp_num T.
126 match fopcl c (cnL ? cn1) (cnL ? cn2) with
127 [ pair c' cnl' ⇒ match fopcl c' (cnH ? cn1) (cnH ? cn2) with
128 [ pair c'' cnh' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].
130 ndefinition opcl_cn ≝
131 λT.λfopcl:bool → T → (ProdT bool T).
132 λc:bool.λcn:comp_num T.
133 match fopcl c (cnL ? cn) with
134 [ pair c' cnl' ⇒ match fopcl c' (cnH ? cn) with
135 [ pair c'' cnh' ⇒ pair … c'' (mk_comp_num ? cnh' cnl') ]].