open BinNums
open BinPos
open Datatypes

module Z =
 struct
  (** val double : coq_Z -> coq_Z **)

  let double = function
  | Z0 -> Z0
  | Zpos p -> Zpos (Coq_xO p)
  | Zneg p -> Zneg (Coq_xO p)

  (** val succ_double : coq_Z -> coq_Z **)

  let succ_double = function
  | Z0 -> Zpos Coq_xH
  | Zpos p -> Zpos (Coq_xI p)
  | Zneg p -> Zneg (Pos.pred_double p)

  (** val pred_double : coq_Z -> coq_Z **)

  let pred_double = function
  | Z0 -> Zneg Coq_xH
  | Zpos p -> Zpos (Pos.pred_double p)
  | Zneg p -> Zneg (Coq_xI p)

  (** val pos_sub : positive -> positive -> coq_Z **)

  let rec pos_sub x y =
    match x with
    | Coq_xI p ->
      (match y with
       | Coq_xI q -> double (pos_sub p q)
       | Coq_xO q -> succ_double (pos_sub p q)
       | Coq_xH -> Zpos (Coq_xO p))
    | Coq_xO p ->
      (match y with
       | Coq_xI q -> pred_double (pos_sub p q)
       | Coq_xO q -> double (pos_sub p q)
       | Coq_xH -> Zpos (Pos.pred_double p))
    | Coq_xH ->
      (match y with
       | Coq_xI q -> Zneg (Coq_xO q)
       | Coq_xO q -> Zneg (Pos.pred_double q)
       | Coq_xH -> Z0)

  (** val add : coq_Z -> coq_Z -> coq_Z **)

  let add x y =
    match x with
    | Z0 -> y
    | Zpos x' ->
      (match y with
       | Z0 -> x
       | Zpos y' -> Zpos (Pos.add x' y')
       | Zneg y' -> pos_sub x' y')
    | Zneg x' ->
      (match y with
       | Z0 -> x
       | Zpos y' -> pos_sub y' x'
       | Zneg y' -> Zneg (Pos.add x' y'))

  (** val opp : coq_Z -> coq_Z **)

  let opp = function
  | Z0 -> Z0
  | Zpos x0 -> Zneg x0
  | Zneg x0 -> Zpos x0

  (** val sub : coq_Z -> coq_Z -> coq_Z **)

  let sub m n =
    add m (opp n)

  (** val mul : coq_Z -> coq_Z -> coq_Z **)

  let mul x y =
    match x with
    | Z0 -> Z0
    | Zpos x' ->
      (match y with
       | Z0 -> Z0
       | Zpos y' -> Zpos (Pos.mul x' y')
       | Zneg y' -> Zneg (Pos.mul x' y'))
    | Zneg x' ->
      (match y with
       | Z0 -> Z0
       | Zpos y' -> Zneg (Pos.mul x' y')
       | Zneg y' -> Zpos (Pos.mul x' y'))

  (** val compare : coq_Z -> coq_Z -> comparison **)

  let compare x y =
    match x with
    | Z0 -> (match y with
             | Z0 -> Eq
             | Zpos _ -> Lt
             | Zneg _ -> Gt)
    | Zpos x' -> (match y with
                  | Zpos y' -> Pos.compare x' y'
                  | _ -> Gt)
    | Zneg x' ->
      (match y with
       | Zneg y' -> coq_CompOpp (Pos.compare x' y')
       | _ -> Lt)

  (** val sgn : coq_Z -> coq_Z **)

  let sgn = function
  | Z0 -> Z0
  | Zpos _ -> Zpos Coq_xH
  | Zneg _ -> Zneg Coq_xH

  (** val leb : coq_Z -> coq_Z -> bool **)

  let leb x y =
    match compare x y with
    | Gt -> false
    | _ -> true

  (** val ltb : coq_Z -> coq_Z -> bool **)

  let ltb x y =
    match compare x y with
    | Lt -> true
    | _ -> false

  (** val eqb : coq_Z -> coq_Z -> bool **)

  let rec eqb x y =
    match x with
    | Z0 -> (match y with
             | Z0 -> true
             | _ -> false)
    | Zpos p -> (match y with
                 | Zpos q -> Pos.eqb p q
                 | _ -> false)
    | Zneg p -> (match y with
                 | Zneg q -> Pos.eqb p q
                 | _ -> false)

  (** val max : coq_Z -> coq_Z -> coq_Z **)

  let max n m =
    match compare n m with
    | Lt -> m
    | _ -> n

  (** val min : coq_Z -> coq_Z -> coq_Z **)

  let min n m =
    match compare n m with
    | Gt -> m
    | _ -> n

  (** val abs : coq_Z -> coq_Z **)

  let abs = function
  | Zneg p -> Zpos p
  | x -> x

  (** val to_pos : coq_Z -> positive **)

  let to_pos = function
  | Zpos p -> p
  | _ -> Coq_xH

  (** val pos_div_eucl : positive -> coq_Z -> coq_Z*coq_Z **)

  let rec pos_div_eucl a b =
    match a with
    | Coq_xI a' ->
      let q,r = pos_div_eucl a' b in
      let r' = add (mul (Zpos (Coq_xO Coq_xH)) r) (Zpos Coq_xH) in
      if ltb r' b
      then (mul (Zpos (Coq_xO Coq_xH)) q),r'
      else (add (mul (Zpos (Coq_xO Coq_xH)) q) (Zpos Coq_xH)),(sub r' b)
    | Coq_xO a' ->
      let q,r = pos_div_eucl a' b in
      let r' = mul (Zpos (Coq_xO Coq_xH)) r in
      if ltb r' b
      then (mul (Zpos (Coq_xO Coq_xH)) q),r'
      else (add (mul (Zpos (Coq_xO Coq_xH)) q) (Zpos Coq_xH)),(sub r' b)
    | Coq_xH ->
      if leb (Zpos (Coq_xO Coq_xH)) b
      then Z0,(Zpos Coq_xH)
      else (Zpos Coq_xH),Z0

  (** val div_eucl : coq_Z -> coq_Z -> coq_Z*coq_Z **)

  let div_eucl a b =
    match a with
    | Z0 -> Z0,Z0
    | Zpos a' ->
      (match b with
       | Z0 -> Z0,Z0
       | Zpos _ -> pos_div_eucl a' b
       | Zneg b' ->
         let q,r = pos_div_eucl a' (Zpos b') in
         (match r with
          | Z0 -> (opp q),Z0
          | _ -> (opp (add q (Zpos Coq_xH))),(add b r)))
    | Zneg a' ->
      (match b with
       | Z0 -> Z0,Z0
       | Zpos _ ->
         let q,r = pos_div_eucl a' b in
         (match r with
          | Z0 -> (opp q),Z0
          | _ -> (opp (add q (Zpos Coq_xH))),(sub b r))
       | Zneg b' -> let q,r = pos_div_eucl a' (Zpos b') in q,(opp r))

  (** val div : coq_Z -> coq_Z -> coq_Z **)

  let div a b =
    let q,_ = div_eucl a b in q

  (** val ggcd : coq_Z -> coq_Z -> coq_Z*(coq_Z*coq_Z) **)

  let ggcd a b =
    match a with
    | Z0 -> (abs b),(Z0,(sgn b))
    | Zpos a0 ->
      (match b with
       | Z0 -> (abs a),((sgn a),Z0)
       | Zpos b0 ->
         let g,p = Pos.ggcd a0 b0 in
         let aa,bb = p in (Zpos g),((Zpos aa),(Zpos bb))
       | Zneg b0 ->
         let g,p = Pos.ggcd a0 b0 in
         let aa,bb = p in (Zpos g),((Zpos aa),(Zneg bb)))
    | Zneg a0 ->
      (match b with
       | Z0 -> (abs a),((sgn a),Z0)
       | Zpos b0 ->
         let g,p = Pos.ggcd a0 b0 in
         let aa,bb = p in (Zpos g),((Zneg aa),(Zpos bb))
       | Zneg b0 ->
         let g,p = Pos.ggcd a0 b0 in
         let aa,bb = p in (Zpos g),((Zneg aa),(Zneg bb)))

  (** val eq_dec : coq_Z -> coq_Z -> bool **)

  let eq_dec x y =
    match x with
    | Z0 -> (match y with
             | Z0 -> true
             | _ -> false)
    | Zpos x0 ->
      (match y with
       | Zpos p0 ->
         let rec f p x1 =
           match p with
           | Coq_xI p1 -> (match x1 with
                           | Coq_xI p2 -> f p1 p2
                           | _ -> false)
           | Coq_xO p1 -> (match x1 with
                           | Coq_xO p2 -> f p1 p2
                           | _ -> false)
           | Coq_xH -> (match x1 with
                        | Coq_xH -> true
                        | _ -> false)
         in f x0 p0
       | _ -> false)
    | Zneg x0 ->
      (match y with
       | Zneg p0 ->
         let rec f p x1 =
           match p with
           | Coq_xI p1 -> (match x1 with
                           | Coq_xI p2 -> f p1 p2
                           | _ -> false)
           | Coq_xO p1 -> (match x1 with
                           | Coq_xO p2 -> f p1 p2
                           | _ -> false)
           | Coq_xH -> (match x1 with
                        | Coq_xH -> true
                        | _ -> false)
         in f x0 p0
       | _ -> false)
 end
