extracted/division.ml

   1 open Preamble
   2
   3 open Types
   4
   5 open Bool
   6
   7 open Relations
   8
   9 open Nat
  10
  11 open Hints_declaration
  12
  13 open Core_notation
  14
  15 open Pts
  16
  17 open Logic
  18
  19 open Positive
  20
  21 open Z
  22
  23 type natp =
  24 | Pzero
  25 | Ppos of Positive.pos
  26
  27 (** val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
  28 let rec natp_rect_Type4 h_pzero h_ppos = function
  29 | Pzero -> h_pzero
  30 | Ppos x_4901 -> h_ppos x_4901
  31
  32 (** val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
  33 let rec natp_rect_Type5 h_pzero h_ppos = function
  34 | Pzero -> h_pzero
  35 | Ppos x_4905 -> h_ppos x_4905
  36
  37 (** val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
  38 let rec natp_rect_Type3 h_pzero h_ppos = function
  39 | Pzero -> h_pzero
  40 | Ppos x_4909 -> h_ppos x_4909
  41
  42 (** val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
  43 let rec natp_rect_Type2 h_pzero h_ppos = function
  44 | Pzero -> h_pzero
  45 | Ppos x_4913 -> h_ppos x_4913
  46
  47 (** val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
  48 let rec natp_rect_Type1 h_pzero h_ppos = function
  49 | Pzero -> h_pzero
  50 | Ppos x_4917 -> h_ppos x_4917
  51
  52 (** val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
  53 let rec natp_rect_Type0 h_pzero h_ppos = function
  54 | Pzero -> h_pzero
  55 | Ppos x_4921 -> h_ppos x_4921
  56
  57 (** val natp_inv_rect_Type4 :
  58     natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
  59 let natp_inv_rect_Type4 hterm h1 h2 =
  60   let hcut = natp_rect_Type4 h1 h2 hterm in hcut __
  61
  62 (** val natp_inv_rect_Type3 :
  63     natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
  64 let natp_inv_rect_Type3 hterm h1 h2 =
  65   let hcut = natp_rect_Type3 h1 h2 hterm in hcut __
  66
  67 (** val natp_inv_rect_Type2 :
  68     natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
  69 let natp_inv_rect_Type2 hterm h1 h2 =
  70   let hcut = natp_rect_Type2 h1 h2 hterm in hcut __
  71
  72 (** val natp_inv_rect_Type1 :
  73     natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
  74 let natp_inv_rect_Type1 hterm h1 h2 =
  75   let hcut = natp_rect_Type1 h1 h2 hterm in hcut __
  76
  77 (** val natp_inv_rect_Type0 :
  78     natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
  79 let natp_inv_rect_Type0 hterm h1 h2 =
  80   let hcut = natp_rect_Type0 h1 h2 hterm in hcut __
  81
  82 (** val natp_discr : natp -> natp -> __ **)
  83 let natp_discr x y =
  84   Logic.eq_rect_Type2 x
  85     (match x with
  86      | Pzero -> Obj.magic (fun _ dH -> dH)
  87      | Ppos a0 -> Obj.magic (fun _ dH -> dH __)) y
  88
  89 (** val natp0 : natp -> natp **)
  90 let natp0 = function
  91 | Pzero -> Pzero
  92 | Ppos m -> Ppos (Positive.P0 m)
  93
  94 (** val natp1 : natp -> natp **)
  95 let natp1 = function
  96 | Pzero -> Ppos Positive.One
  97 | Ppos m -> Ppos (Positive.P1 m)
  98
  99 (** val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod **)
 100 let rec divide m n =
 101   match m with
 102   | Positive.One ->
 103     (match n with
 104      | Positive.One -> { Types.fst = (Ppos Positive.One); Types.snd = Pzero }
 105      | Positive.P1 x ->
 106        { Types.fst = Pzero; Types.snd = (Ppos Positive.One) }
 107      | Positive.P0 x ->
 108        { Types.fst = Pzero; Types.snd = (Ppos Positive.One) })
 109   | Positive.P1 m' ->
 110     let { Types.fst = q; Types.snd = r } = divide m' n in
 111     (match r with
 112      | Pzero ->
 113        (match n with
 114         | Positive.One -> { Types.fst = (natp1 q); Types.snd = Pzero }
 115         | Positive.P1 x ->
 116           { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) }
 117         | Positive.P0 x ->
 118           { Types.fst = (natp0 q); Types.snd = (Ppos Positive.One) })
 119      | Ppos r' ->
 120        (match Positive.partial_minus (Positive.P1 r') n with
 121         | Positive.MinusNeg ->
 122           { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P1 r')) }
 123         | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero }
 124         | Positive.MinusPos r'' ->
 125           { Types.fst = (natp1 q); Types.snd = (Ppos r'') }))
 126   | Positive.P0 m' ->
 127     let { Types.fst = q; Types.snd = r } = divide m' n in
 128     (match r with
 129      | Pzero -> { Types.fst = (natp0 q); Types.snd = Pzero }
 130      | Ppos r' ->
 131        (match Positive.partial_minus (Positive.P0 r') n with
 132         | Positive.MinusNeg ->
 133           { Types.fst = (natp0 q); Types.snd = (Ppos (Positive.P0 r')) }
 134         | Positive.MinusZero -> { Types.fst = (natp1 q); Types.snd = Pzero }
 135         | Positive.MinusPos r'' ->
 136           { Types.fst = (natp1 q); Types.snd = (Ppos r'') }))
 137
 138 (** val div : Positive.pos -> Positive.pos -> natp **)
 139 let div m n =
 140   (divide m n).Types.fst
 141
 142 (** val mod0 : Positive.pos -> Positive.pos -> natp **)
 143 let mod0 m n =
 144   (divide m n).Types.snd
 145
 146 (** val natp_plus : natp -> natp -> natp **)
 147 let rec natp_plus n m =
 148   match n with
 149   | Pzero -> m
 150   | Ppos n' ->
 151     (match m with
 152      | Pzero -> n
 153      | Ppos m' -> Ppos (Positive.plus n' m'))
 154
 155 (** val natp_times : natp -> natp -> natp **)
 156 let rec natp_times n m =
 157   match n with
 158   | Pzero -> Pzero
 159   | Ppos n' ->
 160     (match m with
 161      | Pzero -> Pzero
 162      | Ppos m' -> Ppos (Positive.times n' m'))
 163
 164 (** val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum **)
 165 let dec_divides m n =
 166   Types.prod_rect_Type0 (fun dv md ->
 167     match md with
 168     | Pzero ->
 169       (match dv with
 170        | Pzero -> (fun _ -> Obj.magic natp_discr (Ppos n) Pzero __ __)
 171        | Ppos dv' -> (fun _ -> Types.Inl __))
 172     | Ppos x ->
 173       (match dv with
 174        | Pzero -> (fun md' _ -> Types.Inr __)
 175        | Ppos md' -> (fun dv' _ -> Types.Inr __)) x) (divide n m) __
 176
 177 (** val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum **)
 178 let dec_dividesZ p q =
 179   match p with
 180   | Z.OZ ->
 181     (match q with
 182      | Z.OZ -> Types.Inr __
 183      | Z.Pos m -> Types.Inr __
 184      | Z.Neg m -> Types.Inr __)
 185   | Z.Pos n ->
 186     (match q with
 187      | Z.OZ -> Types.Inl __
 188      | Z.Pos auto -> dec_divides n auto
 189      | Z.Neg auto -> dec_divides n auto)
 190   | Z.Neg n ->
 191     (match q with
 192      | Z.OZ -> Types.Inl __
 193      | Z.Pos auto -> dec_divides n auto
 194      | Z.Neg auto -> dec_divides n auto)
 195
 196 (** val natp_to_Z : natp -> Z.z **)
 197 let natp_to_Z = function
 198 | Pzero -> Z.OZ
 199 | Ppos p -> Z.Pos p
 200
 201 (** val natp_to_negZ : natp -> Z.z **)
 202 let natp_to_negZ = function
 203 | Pzero -> Z.OZ
 204 | Ppos p -> Z.Neg p
 205
 206 (** val divZ : Z.z -> Z.z -> Z.z **)
 207 let divZ x y =
 208   match x with
 209   | Z.OZ -> Z.OZ
 210   | Z.Pos n ->
 211     (match y with
 212      | Z.OZ -> Z.OZ
 213      | Z.Pos m -> natp_to_Z (divide n m).Types.fst
 214      | Z.Neg m ->
 215        let { Types.fst = q; Types.snd = r } = divide n m in
 216        (match r with
 217         | Pzero -> natp_to_negZ q
 218         | Ppos x0 -> Z.zpred (natp_to_negZ q)))
 219   | Z.Neg n ->
 220     (match y with
 221      | Z.OZ -> Z.OZ
 222      | Z.Pos m ->
 223        let { Types.fst = q; Types.snd = r } = divide n m in
 224        (match r with
 225         | Pzero -> natp_to_negZ q
 226         | Ppos x0 -> Z.zpred (natp_to_negZ q))
 227      | Z.Neg m -> natp_to_Z (divide n m).Types.fst)
 228
 229 (** val modZ : Z.z -> Z.z -> Z.z **)
 230 let modZ x y =
 231   match x with
 232   | Z.OZ -> Z.OZ
 233   | Z.Pos n ->
 234     (match y with
 235      | Z.OZ -> Z.OZ
 236      | Z.Pos m -> natp_to_Z (divide n m).Types.snd
 237      | Z.Neg m ->
 238        let { Types.fst = q; Types.snd = r } = divide n m in
 239        (match r with
 240         | Pzero -> Z.OZ
 241         | Ppos x0 -> Z.zplus y (natp_to_Z r)))
 242   | Z.Neg n ->
 243     (match y with
 244      | Z.OZ -> Z.OZ
 245      | Z.Pos m ->
 246        let { Types.fst = q; Types.snd = r } = divide n m in
 247        (match r with
 248         | Pzero -> Z.OZ
 249         | Ppos x0 -> Z.zminus y (natp_to_Z r))
 250      | Z.Neg m -> natp_to_Z (divide n m).Types.snd)
 251