source: extracted/division.ml @ 3043

open Preamble

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

type natp =
| Pzero
| Ppos of Positive.pos

(** val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
let rec natp_rect_Type4 h_pzero h_ppos = function
| Pzero -> h_pzero
| Ppos x_4901 -> h_ppos x_4901

(** val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
let rec natp_rect_Type5 h_pzero h_ppos = function
| Pzero -> h_pzero
| Ppos x_4905 -> h_ppos x_4905

(** val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
let rec natp_rect_Type3 h_pzero h_ppos = function
| Pzero -> h_pzero
| Ppos x_4909 -> h_ppos x_4909

(** val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
let rec natp_rect_Type2 h_pzero h_ppos = function
| Pzero -> h_pzero
| Ppos x_4913 -> h_ppos x_4913

(** val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
let rec natp_rect_Type1 h_pzero h_ppos = function
| Pzero -> h_pzero
| Ppos x_4917 -> h_ppos x_4917

(** val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
let rec natp_rect_Type0 h_pzero h_ppos = function
| Pzero -> h_pzero
| Ppos x_4921 -> h_ppos x_4921

(** val natp_inv_rect_Type4 :
    natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let natp_inv_rect_Type4 hterm h1 h2 =
  let hcut = natp_rect_Type4 h1 h2 hterm in hcut __

(** val natp_inv_rect_Type3 :
    natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let natp_inv_rect_Type3 hterm h1 h2 =
  let hcut = natp_rect_Type3 h1 h2 hterm in hcut __

(** val natp_inv_rect_Type2 :
    natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let natp_inv_rect_Type2 hterm h1 h2 =
  let hcut = natp_rect_Type2 h1 h2 hterm in hcut __

(** val natp_inv_rect_Type1 :
    natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let natp_inv_rect_Type1 hterm h1 h2 =
  let hcut = natp_rect_Type1 h1 h2 hterm in hcut __

(** val natp_inv_rect_Type0 :
    natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
let natp_inv_rect_Type0 hterm h1 h2 =
  let hcut = natp_rect_Type0 h1 h2 hterm in hcut __

(** val natp_discr : natp -> natp -> __ **)
let natp_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Pzero -> Obj.magic (fun _ dH -> dH)
     | Ppos a0 -> Obj.magic (fun _ dH -> dH __)) y

(** val natp0 : natp -> natp **)
let natp0 = function
| Pzero -> Pzero
| Ppos m -> Ppos (Positive.P0 m)

(** val natp1 : natp -> natp **)
let natp1 = function
| Pzero -> Ppos Positive.One
| Ppos m -> Ppos (Positive.P1 m)

(** val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod **)
let rec divide m n =
  match m with
  | Positive.One ->
    (match n with
     | Positive.One -> { Types.fst = (Ppos Positive.One); Types.snd = Pzero }
     | Positive.P1 x ->
       { Types.fst = Pzero; Types.snd = (Ppos Positive.One) }
     | Positive.P0 x ->
       { Types.fst = Pzero; Types.snd = (Ppos Positive.One) })
  | Positive.P1 m' ->
    let { Types.fst = q; Types.snd = r } = divide m' n in
    (match r with
     | Pzero ->
       (match n with
        | Positive.One -> { Types.fst = (natp1 q); Types.snd = Pzero }
        | Positive.P1 x ->
          { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) }
        | Positive.P0 x ->
          { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) })
     | Ppos r' ->
       (match Positive.partial_minus (Positive.P1 r') n with
        | Positive.MinusNeg ->
          { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P1 r')) }
        | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero }
        | Positive.MinusPos r'' ->
          { Types.fst = (natp1 q); Types.snd = (Ppos r'') }))
  | Positive.P0 m' ->
    let { Types.fst = q; Types.snd = r } = divide m' n in
    (match r with
     | Pzero -> { Types.fst = (natp0 q); Types.snd = Pzero }
     | Ppos r' ->
       (match Positive.partial_minus (Positive.P0 r') n with
        | Positive.MinusNeg ->
          { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P0 r')) }
        | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero }
        | Positive.MinusPos r'' ->
          { Types.fst = (natp1 q); Types.snd = (Ppos r'') }))

(** val div : Positive.pos -> Positive.pos -> natp **)
let div m n =
  (divide m n).Types.fst

(** val mod0 : Positive.pos -> Positive.pos -> natp **)
let mod0 m n =
  (divide m n).Types.snd

(** val natp_plus : natp -> natp -> natp **)
let rec natp_plus n m =
  match n with
  | Pzero -> m
  | Ppos n' ->
    (match m with
     | Pzero -> n
     | Ppos m' -> Ppos (Positive.plus n' m'))

(** val natp_times : natp -> natp -> natp **)
let rec natp_times n m =
  match n with
  | Pzero -> Pzero
  | Ppos n' ->
    (match m with
     | Pzero -> Pzero
     | Ppos m' -> Ppos (Positive.times n' m'))

(** val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum **)
let dec_divides m n =
  Types.prod_rect_Type0 (fun dv md ->
    match md with
    | Pzero ->
      (match dv with
       | Pzero -> (fun _ -> Obj.magic natp_discr (Ppos n) Pzero __ __)
       | Ppos dv' -> (fun _ -> Types.Inl __))
    | Ppos x ->
      (match dv with
       | Pzero -> (fun md' _ -> Types.Inr __)
       | Ppos md' -> (fun dv' _ -> Types.Inr __)) x) (divide n m) __

(** val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum **)
let dec_dividesZ p q =
  match p with
  | Z.OZ ->
    (match q with
     | Z.OZ -> Types.Inr __
     | Z.Pos m -> Types.Inr __
     | Z.Neg m -> Types.Inr __)
  | Z.Pos n ->
    (match q with
     | Z.OZ -> Types.Inl __
     | Z.Pos auto -> dec_divides n auto
     | Z.Neg auto -> dec_divides n auto)
  | Z.Neg n ->
    (match q with
     | Z.OZ -> Types.Inl __
     | Z.Pos auto -> dec_divides n auto
     | Z.Neg auto -> dec_divides n auto)

(** val natp_to_Z : natp -> Z.z **)
let natp_to_Z = function
| Pzero -> Z.OZ
| Ppos p -> Z.Pos p

(** val natp_to_negZ : natp -> Z.z **)
let natp_to_negZ = function
| Pzero -> Z.OZ
| Ppos p -> Z.Neg p

(** val divZ : Z.z -> Z.z -> Z.z **)
let divZ x y =
  match x with
  | Z.OZ -> Z.OZ
  | Z.Pos n ->
    (match y with
     | Z.OZ -> Z.OZ
     | Z.Pos m -> natp_to_Z (divide n m).Types.fst
     | Z.Neg m ->
       let { Types.fst = q; Types.snd = r } = divide n m in
       (match r with
        | Pzero -> natp_to_negZ q
        | Ppos x0 -> Z.zpred (natp_to_negZ q)))
  | Z.Neg n ->
    (match y with
     | Z.OZ -> Z.OZ
     | Z.Pos m ->
       let { Types.fst = q; Types.snd = r } = divide n m in
       (match r with
        | Pzero -> natp_to_negZ q
        | Ppos x0 -> Z.zpred (natp_to_negZ q))
     | Z.Neg m -> natp_to_Z (divide n m).Types.fst)

(** val modZ : Z.z -> Z.z -> Z.z **)
let modZ x y =
  match x with
  | Z.OZ -> Z.OZ
  | Z.Pos n ->
    (match y with
     | Z.OZ -> Z.OZ
     | Z.Pos m -> natp_to_Z (divide n m).Types.snd
     | Z.Neg m ->
       let { Types.fst = q; Types.snd = r } = divide n m in
       (match r with
        | Pzero -> Z.OZ
        | Ppos x0 -> Z.zplus y (natp_to_Z r)))
  | Z.Neg n ->
    (match y with
     | Z.OZ -> Z.OZ
     | Z.Pos m ->
       let { Types.fst = q; Types.snd = r } = divide n m in
       (match r with
        | Pzero -> Z.OZ
        | Ppos x0 -> Z.zminus y (natp_to_Z r))
     | Z.Neg m -> natp_to_Z (divide n m).Types.snd)