source: extracted/division.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 7.2 KB
Line 
1open Preamble
2
3open Types
4
5open Bool
6
7open Relations
8
9open Nat
10
11open Hints_declaration
12
13open Core_notation
14
15open Pts
16
17open Logic
18
19open Positive
20
21open Z
22
23type natp =
24| Pzero
25| Ppos of Positive.pos
26
27(** val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
28let rec natp_rect_Type4 h_pzero h_ppos = function
29| Pzero -> h_pzero
30| Ppos x_4849 -> h_ppos x_4849
31
32(** val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
33let rec natp_rect_Type5 h_pzero h_ppos = function
34| Pzero -> h_pzero
35| Ppos x_4853 -> h_ppos x_4853
36
37(** val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
38let rec natp_rect_Type3 h_pzero h_ppos = function
39| Pzero -> h_pzero
40| Ppos x_4857 -> h_ppos x_4857
41
42(** val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
43let rec natp_rect_Type2 h_pzero h_ppos = function
44| Pzero -> h_pzero
45| Ppos x_4861 -> h_ppos x_4861
46
47(** val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
48let rec natp_rect_Type1 h_pzero h_ppos = function
49| Pzero -> h_pzero
50| Ppos x_4865 -> h_ppos x_4865
51
52(** val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
53let rec natp_rect_Type0 h_pzero h_ppos = function
54| Pzero -> h_pzero
55| Ppos x_4869 -> h_ppos x_4869
56
57(** val natp_inv_rect_Type4 :
58    natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
59let 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 **)
64let 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 **)
69let 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 **)
74let 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 **)
79let 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 -> __ **)
83let 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 **)
90let natp0 = function
91| Pzero -> Pzero
92| Ppos m -> Ppos (Positive.P0 m)
93
94(** val natp1 : natp -> natp **)
95let 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 **)
100let 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 **)
139let div m n =
140  (divide m n).Types.fst
141
142(** val mod0 : Positive.pos -> Positive.pos -> natp **)
143let mod0 m n =
144  (divide m n).Types.snd
145
146(** val natp_plus : natp -> natp -> natp **)
147let 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.plus0 n' m'))
154
155(** val natp_times : natp -> natp -> natp **)
156let 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.times0 n' m'))
163
164(** val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum **)
165let 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 **)
178let 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 **)
197let natp_to_Z = function
198| Pzero -> Z.OZ
199| Ppos p -> Z.Pos p
200
201(** val natp_to_negZ : natp -> Z.z **)
202let natp_to_negZ = function
203| Pzero -> Z.OZ
204| Ppos p -> Z.Neg p
205
206(** val divZ : Z.z -> Z.z -> Z.z **)
207let 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 **)
230let 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
Note: See TracBrowser for help on using the repository browser.