blob: 60fa09584fb148395c3c8c82e8c99353aec7464f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Set Implicit Arguments.
Require Import ZArith.
Open Local Scope Z_scope.
Section Carry.
Variable A : Set.
Inductive carry : Set :=
| C0 : A -> carry
| C1 : A -> carry.
End Carry.
Section Zn2Z.
Variable znz : Set.
Inductive zn2z : Set :=
| W0 : zn2z
| WW : znz -> znz -> zn2z.
Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) :=
match x with
| W0 => 0
| WW xh xl => w_to_Z xh * wB + w_to_Z xl
end.
Definition base digits := Zpower 2 (Zpos digits).
Definition interp_carry sign B (interp:znz -> Z) c :=
match c with
| C0 x => interp x
| C1 x => sign*B + interp x
end.
End Zn2Z.
Implicit Arguments W0 [znz].
Fixpoint word_tr (w:Set) (n:nat) {struct n} : Set :=
match n with
| O => w
| S n => word_tr (zn2z w) n
end.
Fixpoint word (w:Set) (n:nat) {struct n} : Set :=
match n with
| O => w
| S n => zn2z (word w n)
end.
|
