source: driver/extracted/positive.ml @ 3106

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

The compiler now computes also the stack cost model.

File size: 12.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Bool
12
13open Relations
14
15open Nat
16
17type compare =
18| LT
19| EQ
20| GT
21
22(** val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
23let rec compare_rect_Type4 h_LT h_EQ h_GT = function
24| LT -> h_LT
25| EQ -> h_EQ
26| GT -> h_GT
27
28(** val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
29let rec compare_rect_Type5 h_LT h_EQ h_GT = function
30| LT -> h_LT
31| EQ -> h_EQ
32| GT -> h_GT
33
34(** val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
35let rec compare_rect_Type3 h_LT h_EQ h_GT = function
36| LT -> h_LT
37| EQ -> h_EQ
38| GT -> h_GT
39
40(** val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
41let rec compare_rect_Type2 h_LT h_EQ h_GT = function
42| LT -> h_LT
43| EQ -> h_EQ
44| GT -> h_GT
45
46(** val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
47let rec compare_rect_Type1 h_LT h_EQ h_GT = function
48| LT -> h_LT
49| EQ -> h_EQ
50| GT -> h_GT
51
52(** val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
53let rec compare_rect_Type0 h_LT h_EQ h_GT = function
54| LT -> h_LT
55| EQ -> h_EQ
56| GT -> h_GT
57
58(** val compare_inv_rect_Type4 :
59    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
60let compare_inv_rect_Type4 hterm h1 h2 h3 =
61  let hcut = compare_rect_Type4 h1 h2 h3 hterm in hcut __
62
63(** val compare_inv_rect_Type3 :
64    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
65let compare_inv_rect_Type3 hterm h1 h2 h3 =
66  let hcut = compare_rect_Type3 h1 h2 h3 hterm in hcut __
67
68(** val compare_inv_rect_Type2 :
69    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
70let compare_inv_rect_Type2 hterm h1 h2 h3 =
71  let hcut = compare_rect_Type2 h1 h2 h3 hterm in hcut __
72
73(** val compare_inv_rect_Type1 :
74    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
75let compare_inv_rect_Type1 hterm h1 h2 h3 =
76  let hcut = compare_rect_Type1 h1 h2 h3 hterm in hcut __
77
78(** val compare_inv_rect_Type0 :
79    compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
80let compare_inv_rect_Type0 hterm h1 h2 h3 =
81  let hcut = compare_rect_Type0 h1 h2 h3 hterm in hcut __
82
83(** val compare_discr : compare -> compare -> __ **)
84let compare_discr x y =
85  Logic.eq_rect_Type2 x
86    (match x with
87     | LT -> Obj.magic (fun _ dH -> dH)
88     | EQ -> Obj.magic (fun _ dH -> dH)
89     | GT -> Obj.magic (fun _ dH -> dH)) y
90
91(** val compare_invert : compare -> compare **)
92let compare_invert = function
93| LT -> GT
94| EQ -> EQ
95| GT -> LT
96
97type pos =
98| One
99| P1 of pos
100| P0 of pos
101
102(** val pos_rect_Type4 :
103    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
104let rec pos_rect_Type4 h_one h_p1 h_p0 = function
105| One -> h_one
106| P1 x_1606 -> h_p1 x_1606 (pos_rect_Type4 h_one h_p1 h_p0 x_1606)
107| P0 x_1607 -> h_p0 x_1607 (pos_rect_Type4 h_one h_p1 h_p0 x_1607)
108
109(** val pos_rect_Type3 :
110    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
111let rec pos_rect_Type3 h_one h_p1 h_p0 = function
112| One -> h_one
113| P1 x_1618 -> h_p1 x_1618 (pos_rect_Type3 h_one h_p1 h_p0 x_1618)
114| P0 x_1619 -> h_p0 x_1619 (pos_rect_Type3 h_one h_p1 h_p0 x_1619)
115
116(** val pos_rect_Type2 :
117    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
118let rec pos_rect_Type2 h_one h_p1 h_p0 = function
119| One -> h_one
120| P1 x_1624 -> h_p1 x_1624 (pos_rect_Type2 h_one h_p1 h_p0 x_1624)
121| P0 x_1625 -> h_p0 x_1625 (pos_rect_Type2 h_one h_p1 h_p0 x_1625)
122
123(** val pos_rect_Type1 :
124    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
125let rec pos_rect_Type1 h_one h_p1 h_p0 = function
126| One -> h_one
127| P1 x_1630 -> h_p1 x_1630 (pos_rect_Type1 h_one h_p1 h_p0 x_1630)
128| P0 x_1631 -> h_p0 x_1631 (pos_rect_Type1 h_one h_p1 h_p0 x_1631)
129
130(** val pos_rect_Type0 :
131    'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
132let rec pos_rect_Type0 h_one h_p1 h_p0 = function
133| One -> h_one
134| P1 x_1636 -> h_p1 x_1636 (pos_rect_Type0 h_one h_p1 h_p0 x_1636)
135| P0 x_1637 -> h_p0 x_1637 (pos_rect_Type0 h_one h_p1 h_p0 x_1637)
136
137(** val pos_inv_rect_Type4 :
138    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
139    'a1) -> __ -> 'a1) -> 'a1 **)
140let pos_inv_rect_Type4 hterm h1 h2 h3 =
141  let hcut = pos_rect_Type4 h1 h2 h3 hterm in hcut __
142
143(** val pos_inv_rect_Type3 :
144    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
145    'a1) -> __ -> 'a1) -> 'a1 **)
146let pos_inv_rect_Type3 hterm h1 h2 h3 =
147  let hcut = pos_rect_Type3 h1 h2 h3 hterm in hcut __
148
149(** val pos_inv_rect_Type2 :
150    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
151    'a1) -> __ -> 'a1) -> 'a1 **)
152let pos_inv_rect_Type2 hterm h1 h2 h3 =
153  let hcut = pos_rect_Type2 h1 h2 h3 hterm in hcut __
154
155(** val pos_inv_rect_Type1 :
156    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
157    'a1) -> __ -> 'a1) -> 'a1 **)
158let pos_inv_rect_Type1 hterm h1 h2 h3 =
159  let hcut = pos_rect_Type1 h1 h2 h3 hterm in hcut __
160
161(** val pos_inv_rect_Type0 :
162    pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
163    'a1) -> __ -> 'a1) -> 'a1 **)
164let pos_inv_rect_Type0 hterm h1 h2 h3 =
165  let hcut = pos_rect_Type0 h1 h2 h3 hterm in hcut __
166
167(** val pos_discr : pos -> pos -> __ **)
168let pos_discr x y =
169  Logic.eq_rect_Type2 x
170    (match x with
171     | One -> Obj.magic (fun _ dH -> dH)
172     | P1 a0 -> Obj.magic (fun _ dH -> dH __)
173     | P0 a0 -> Obj.magic (fun _ dH -> dH __)) y
174
175(** val pred : pos -> pos **)
176let rec pred = function
177| One -> One
178| P1 ps -> P0 ps
179| P0 ps ->
180  (match ps with
181   | One -> One
182   | P1 x -> P1 (pred ps)
183   | P0 x -> P1 (pred ps))
184
185(** val succ : pos -> pos **)
186let rec succ = function
187| One -> P0 One
188| P1 ps -> P0 (succ ps)
189| P0 ps -> P1 ps
190
191(** val nat_of_pos : pos -> Nat.nat **)
192let rec nat_of_pos = function
193| One -> Nat.S Nat.O
194| P1 ps -> Nat.S (Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps))
195| P0 ps -> Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps)
196
197(** val succ_pos_of_nat : Nat.nat -> pos **)
198let rec succ_pos_of_nat = function
199| Nat.O -> One
200| Nat.S n' -> succ (succ_pos_of_nat n')
201
202(** val plus : pos -> pos -> pos **)
203let rec plus n m =
204  match n with
205  | One -> succ m
206  | P1 n' ->
207    (match m with
208     | One -> succ n
209     | P1 m' -> P0 (succ (plus n' m'))
210     | P0 m' -> P1 (plus n' m'))
211  | P0 n' ->
212    (match m with
213     | One -> P1 n'
214     | P1 m' -> P1 (plus n' m')
215     | P0 m' -> P0 (plus n' m'))
216
217(** val times : pos -> pos -> pos **)
218let rec times n m =
219  match n with
220  | One -> m
221  | P1 n' -> plus m (P0 (times n' m))
222  | P0 n' -> P0 (times n' m)
223
224type minusresult =
225| MinusNeg
226| MinusZero
227| MinusPos of pos
228
229(** val minusresult_rect_Type4 :
230    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
231let rec minusresult_rect_Type4 h_MinusNeg h_MinusZero h_MinusPos = function
232| MinusNeg -> h_MinusNeg
233| MinusZero -> h_MinusZero
234| MinusPos x_1813 -> h_MinusPos x_1813
235
236(** val minusresult_rect_Type5 :
237    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
238let rec minusresult_rect_Type5 h_MinusNeg h_MinusZero h_MinusPos = function
239| MinusNeg -> h_MinusNeg
240| MinusZero -> h_MinusZero
241| MinusPos x_1818 -> h_MinusPos x_1818
242
243(** val minusresult_rect_Type3 :
244    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
245let rec minusresult_rect_Type3 h_MinusNeg h_MinusZero h_MinusPos = function
246| MinusNeg -> h_MinusNeg
247| MinusZero -> h_MinusZero
248| MinusPos x_1823 -> h_MinusPos x_1823
249
250(** val minusresult_rect_Type2 :
251    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
252let rec minusresult_rect_Type2 h_MinusNeg h_MinusZero h_MinusPos = function
253| MinusNeg -> h_MinusNeg
254| MinusZero -> h_MinusZero
255| MinusPos x_1828 -> h_MinusPos x_1828
256
257(** val minusresult_rect_Type1 :
258    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
259let rec minusresult_rect_Type1 h_MinusNeg h_MinusZero h_MinusPos = function
260| MinusNeg -> h_MinusNeg
261| MinusZero -> h_MinusZero
262| MinusPos x_1833 -> h_MinusPos x_1833
263
264(** val minusresult_rect_Type0 :
265    'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
266let rec minusresult_rect_Type0 h_MinusNeg h_MinusZero h_MinusPos = function
267| MinusNeg -> h_MinusNeg
268| MinusZero -> h_MinusZero
269| MinusPos x_1838 -> h_MinusPos x_1838
270
271(** val minusresult_inv_rect_Type4 :
272    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
273let minusresult_inv_rect_Type4 hterm h1 h2 h3 =
274  let hcut = minusresult_rect_Type4 h1 h2 h3 hterm in hcut __
275
276(** val minusresult_inv_rect_Type3 :
277    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
278let minusresult_inv_rect_Type3 hterm h1 h2 h3 =
279  let hcut = minusresult_rect_Type3 h1 h2 h3 hterm in hcut __
280
281(** val minusresult_inv_rect_Type2 :
282    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
283let minusresult_inv_rect_Type2 hterm h1 h2 h3 =
284  let hcut = minusresult_rect_Type2 h1 h2 h3 hterm in hcut __
285
286(** val minusresult_inv_rect_Type1 :
287    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
288let minusresult_inv_rect_Type1 hterm h1 h2 h3 =
289  let hcut = minusresult_rect_Type1 h1 h2 h3 hterm in hcut __
290
291(** val minusresult_inv_rect_Type0 :
292    minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
293let minusresult_inv_rect_Type0 hterm h1 h2 h3 =
294  let hcut = minusresult_rect_Type0 h1 h2 h3 hterm in hcut __
295
296(** val minusresult_discr : minusresult -> minusresult -> __ **)
297let minusresult_discr x y =
298  Logic.eq_rect_Type2 x
299    (match x with
300     | MinusNeg -> Obj.magic (fun _ dH -> dH)
301     | MinusZero -> Obj.magic (fun _ dH -> dH)
302     | MinusPos a0 -> Obj.magic (fun _ dH -> dH __)) y
303
304(** val partial_minus : pos -> pos -> minusresult **)
305let rec partial_minus n m =
306  match n with
307  | One ->
308    (match m with
309     | One -> MinusZero
310     | P1 x -> MinusNeg
311     | P0 x -> MinusNeg)
312  | P1 n' ->
313    (match m with
314     | One -> MinusPos (P0 n')
315     | P1 m' ->
316       (match partial_minus n' m' with
317        | MinusNeg -> MinusNeg
318        | MinusZero -> MinusZero
319        | MinusPos p -> MinusPos (P0 p))
320     | P0 m' ->
321       (match partial_minus n' m' with
322        | MinusNeg -> MinusNeg
323        | MinusZero -> MinusPos One
324        | MinusPos p -> MinusPos (P1 p)))
325  | P0 n' ->
326    (match m with
327     | One -> MinusPos (pred n)
328     | P1 m' ->
329       (match partial_minus n' m' with
330        | MinusNeg -> MinusNeg
331        | MinusZero -> MinusNeg
332        | MinusPos p -> MinusPos (pred (P0 p)))
333     | P0 m' ->
334       (match partial_minus n' m' with
335        | MinusNeg -> MinusNeg
336        | MinusZero -> MinusZero
337        | MinusPos p -> MinusPos (P0 p)))
338
339(** val minus : pos -> pos -> pos **)
340let minus n m =
341  match partial_minus n m with
342  | MinusNeg -> One
343  | MinusZero -> One
344  | MinusPos p -> p
345
346(** val eqb : pos -> pos -> Bool.bool **)
347let rec eqb n m =
348  match n with
349  | One ->
350    (match m with
351     | One -> Bool.True
352     | P1 x -> Bool.False
353     | P0 x -> Bool.False)
354  | P1 p ->
355    (match m with
356     | One -> Bool.False
357     | P1 q -> eqb p q
358     | P0 x -> Bool.False)
359  | P0 p ->
360    (match m with
361     | One -> Bool.False
362     | P1 x -> Bool.False
363     | P0 q -> eqb p q)
364
365(** val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
366let eqb_elim n m x x0 =
367  pos_rect_Type1 (fun m0 ->
368    match m0 with
369    | One -> (fun _ auto auto' -> auto __)
370    | P1 m' -> (fun _ t f -> f __)
371    | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
372    match m0 with
373    | One -> (fun _ t f -> f __)
374    | P1 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))
375    | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
376    match m0 with
377    | One -> (fun _ t f -> f __)
378    | P1 m' -> (fun _ t f -> f __)
379    | P0 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))) n m
380    __ x x0
381
382(** val leb : pos -> pos -> Bool.bool **)
383let rec leb n m =
384  match partial_minus n m with
385  | MinusNeg -> Bool.True
386  | MinusZero -> Bool.True
387  | MinusPos x -> Bool.False
388
389(** val pos_compare : pos -> pos -> compare **)
390let pos_compare n m =
391  match partial_minus n m with
392  | MinusNeg -> LT
393  | MinusZero -> EQ
394  | MinusPos x -> GT
395
396(** val two_power_nat : Nat.nat -> pos **)
397let rec two_power_nat = function
398| Nat.O -> One
399| Nat.S n' -> P0 (two_power_nat n')
400
401(** val two_power_pos : pos -> pos **)
402let two_power_pos p =
403  two_power_nat (nat_of_pos p)
404
405(** val max : pos -> pos -> pos **)
406let max n m =
407  match leb n m with
408  | Bool.True -> m
409  | Bool.False -> n
410
Note: See TracBrowser for help on using the repository browser.