source: driver/extracted/division.ml @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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_4901 -> h_ppos x_4901
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_4905 -> h_ppos x_4905
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_4909 -> h_ppos x_4909
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_4913 -> h_ppos x_4913
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_4917 -> h_ppos x_4917
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_4921 -> h_ppos x_4921
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.plus 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.times 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.