1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: DoubleType.v 10964 2008-05-22 11:08:13Z letouzey $ i*)
13
Set Implicit Arguments.
15
Require Import ZArith.
16
Open Local Scope Z_scope.
18
Definition base digits := Zpower 2 (Zpos digits).
28
Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c :=
31
| C1 x => sign*B + interp x
40
(** From a type [znz] representing a cyclic structure Z/nZ,
41
we produce a representation of Z/2nZ by pairs of elements of [znz]
42
(plus a special case for zero). High half of the new number comes
48
| WW : znz -> znz -> zn2z.
50
Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) :=
53
| WW xh xl => w_to_Z xh * wB + w_to_Z xl
58
Implicit Arguments W0 [znz].
60
(** From a cyclic representation [w], we iterate the [zn2z] construct
61
[n] times, gaining the type of binary trees of depth at most [n],
62
whose leafs are either W0 (if depth < n) or elements of w
66
Fixpoint word (w:Type) (n:nat) : Type :=
69
| S n => zn2z (word w n)