From Corelib Require Export BinNums PosDef.

Module N.

Definition succ_double x :=
  match x with
  | N0 => Npos 1
  | Npos p => Npos p~1
  end.

Definition double n :=
  match n with
  | N0 => N0
  | Npos p => Npos p~0
  end.

Definition succ_pos (n : N) : positive :=
 match n with
   | N0 => xH
   | Npos p => Pos.succ p
 end.

Definition sub n m :=
match n, m with
| N0, _ => N0
| n, N0 => n
| Npos n', Npos m' =>
  match Pos.sub_mask n' m' with
  | Pos.IsPos p => Npos p
  | _ => N0
  end
end.

Definition compare n m :=
  match n, m with
  | N0, N0 => Eq
  | N0, Npos m' => Lt
  | Npos n', N0 => Gt
  | Npos n', Npos m' => Pos.compare n' m'
  end.

Definition leb x y :=
 match compare x y with Gt => false | _ => true end.

Fixpoint pos_div_eucl (a:positive)(b:N) : N * N :=
  match a with
    | xH =>
       match b with Npos 1 => (Npos 1, N0) | _ => (N0, Npos 1) end
    | xO a' =>
       let (q, r) := pos_div_eucl a' b in
       let r' := double r in
       if leb b r' then (succ_double q, sub r' b)
        else (double q, r')
    | xI a' =>
       let (q, r) := pos_div_eucl a' b in
       let r' := succ_double r in
       if leb b r' then (succ_double q, sub r' b)
        else (double q, r')
  end.

Definition lor n m :=
 match n, m with
   | N0, _ => m
   | _, N0 => n
   | Npos p, Npos q => Npos (Pos.lor p q)
 end.

Definition land n m :=
 match n, m with
  | N0, _ => N0
  | _, N0 => N0
  | Npos p, Npos q => Pos.land p q
 end.

Definition ldiff n m :=
 match n, m with
  | N0, _ => N0
  | _, N0 => n
  | Npos p, Npos q => Pos.ldiff p q
 end.

Definition lxor n m :=
  match n, m with
    | N0, _ => m
    | _, N0 => n
    | Npos p, Npos q => Pos.lxor p q
  end.

End N.