Library Coq.Numbers.Cyclic.Abstract.DoubleType


Set Implicit Arguments.

Require Import BinInt.
Local Open Scope Z_scope.

Definition base digits := Z.pow 2 (Zpos digits).


Definition interp_carry {A} (sign:Z)(B:Z)(interp:A -> Z) c :=
  match c with
  | C0 x => interp x
  | C1 x => sign*B + interp x
  end.

From a type znz representing a cyclic structure Z/nZ, we produce a representation of Z/2nZ by pairs of elements of znz (plus a special case for zero). High half of the new number comes first.

Definition zn2z_to_Z znz (wB:Z) (w_to_Z:znz->Z) (x:zn2z znz) :=
  match x with
  | W0 => 0
  | WW xh xl => w_to_Z xh * wB + w_to_Z xl
  end.


From a cyclic representation w, we iterate the zn2z construct n times, gaining the type of binary trees of depth at most n, whose leafs are either W0 (if depth < n) or elements of w (if depth = n).

Fixpoint word (w:Type) (n:nat) : Type :=
 match n with
 | O => w
 | S n => zn2z (word w n)
 end.