source: extracted/util.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 19.4 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Jmeq
22
23open Russell
24
25type dAEMONXXX =
26| K1DAEMONXXX
27| K2DAEMONXXX
28
29(** val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
30let rec dAEMONXXX_rect_Type4 h_K1DAEMONXXX h_K2DAEMONXXX = function
31| K1DAEMONXXX -> h_K1DAEMONXXX
32| K2DAEMONXXX -> h_K2DAEMONXXX
33
34(** val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
35let rec dAEMONXXX_rect_Type5 h_K1DAEMONXXX h_K2DAEMONXXX = function
36| K1DAEMONXXX -> h_K1DAEMONXXX
37| K2DAEMONXXX -> h_K2DAEMONXXX
38
39(** val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
40let rec dAEMONXXX_rect_Type3 h_K1DAEMONXXX h_K2DAEMONXXX = function
41| K1DAEMONXXX -> h_K1DAEMONXXX
42| K2DAEMONXXX -> h_K2DAEMONXXX
43
44(** val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
45let rec dAEMONXXX_rect_Type2 h_K1DAEMONXXX h_K2DAEMONXXX = function
46| K1DAEMONXXX -> h_K1DAEMONXXX
47| K2DAEMONXXX -> h_K2DAEMONXXX
48
49(** val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
50let rec dAEMONXXX_rect_Type1 h_K1DAEMONXXX h_K2DAEMONXXX = function
51| K1DAEMONXXX -> h_K1DAEMONXXX
52| K2DAEMONXXX -> h_K2DAEMONXXX
53
54(** val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
55let rec dAEMONXXX_rect_Type0 h_K1DAEMONXXX h_K2DAEMONXXX = function
56| K1DAEMONXXX -> h_K1DAEMONXXX
57| K2DAEMONXXX -> h_K2DAEMONXXX
58
59(** val dAEMONXXX_inv_rect_Type4 :
60    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
61let dAEMONXXX_inv_rect_Type4 hterm h1 h2 =
62  let hcut = dAEMONXXX_rect_Type4 h1 h2 hterm in hcut __
63
64(** val dAEMONXXX_inv_rect_Type3 :
65    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
66let dAEMONXXX_inv_rect_Type3 hterm h1 h2 =
67  let hcut = dAEMONXXX_rect_Type3 h1 h2 hterm in hcut __
68
69(** val dAEMONXXX_inv_rect_Type2 :
70    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
71let dAEMONXXX_inv_rect_Type2 hterm h1 h2 =
72  let hcut = dAEMONXXX_rect_Type2 h1 h2 hterm in hcut __
73
74(** val dAEMONXXX_inv_rect_Type1 :
75    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
76let dAEMONXXX_inv_rect_Type1 hterm h1 h2 =
77  let hcut = dAEMONXXX_rect_Type1 h1 h2 hterm in hcut __
78
79(** val dAEMONXXX_inv_rect_Type0 :
80    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
81let dAEMONXXX_inv_rect_Type0 hterm h1 h2 =
82  let hcut = dAEMONXXX_rect_Type0 h1 h2 hterm in hcut __
83
84(** val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __ **)
85let dAEMONXXX_discr x y =
86  Logic.eq_rect_Type2 x
87    (match x with
88     | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
89     | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
90
91(** val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __ **)
92let dAEMONXXX_jmdiscr x y =
93  Logic.eq_rect_Type2 x
94    (match x with
95     | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
96     | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
97
98(** val ltb : Nat.nat -> Nat.nat -> Bool.bool **)
99let ltb m n =
100  Nat.leb (Nat.S m) n
101
102(** val geb : Nat.nat -> Nat.nat -> Bool.bool **)
103let geb m n =
104  Nat.leb n m
105
106(** val gtb : Nat.nat -> Nat.nat -> Bool.bool **)
107let gtb m n =
108  ltb n m
109
110(** val eq_nat : Nat.nat -> Nat.nat -> Bool.bool **)
111let rec eq_nat n m =
112  match n with
113  | Nat.O ->
114    (match m with
115     | Nat.O -> Bool.True
116     | Nat.S x -> Bool.False)
117  | Nat.S n' ->
118    (match m with
119     | Nat.O -> Bool.False
120     | Nat.S m' -> eq_nat n' m')
121
122(** val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
123let rec forall f = function
124| List.Nil -> Bool.True
125| List.Cons (hd0, tl) -> Bool.andb (f hd0) (forall f tl)
126
127(** val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
128let rec prefix k = function
129| List.Nil -> List.Nil
130| List.Cons (hd0, tl) ->
131  (match k with
132   | Nat.O -> List.Nil
133   | Nat.S k' -> List.Cons (hd0, (prefix k' tl)))
134
135(** val fold_left2 :
136    ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list ->
137    'a1 **)
138let rec fold_left2 f accu left right =
139  (match left with
140   | List.Nil ->
141     (fun _ ->
142       (match right with
143        | List.Nil -> (fun _ -> accu)
144        | List.Cons (hd0, tl) ->
145          (fun _ ->
146            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
147   | List.Cons (hd0, tl) ->
148     (fun _ ->
149       (match right with
150        | List.Nil ->
151          (fun _ ->
152            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
153        | List.Cons (hd', tl') ->
154          (fun _ -> fold_left2 f (f accu hd0 hd') tl tl')) __)) __
155
156(** val remove_n_first_internal :
157    Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
158let rec remove_n_first_internal i l n =
159  match l with
160  | List.Nil -> List.Nil
161  | List.Cons (hd0, tl) ->
162    (match eq_nat i n with
163     | Bool.True -> l
164     | Bool.False -> remove_n_first_internal (Nat.S i) tl n)
165
166(** val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
167let remove_n_first n l =
168  remove_n_first_internal Nat.O l n
169
170(** val foldi_from_until_internal :
171    Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
172    List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list **)
173let rec foldi_from_until_internal i res rem m f =
174  match rem with
175  | List.Nil -> res
176  | List.Cons (e0, tl) ->
177    (match geb i m with
178     | Bool.True -> res
179     | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e0) tl m f)
180
181(** val foldi_from_until :
182    Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list)
183    -> 'a1 List.list -> 'a1 List.list -> 'a1 List.list **)
184let foldi_from_until n m f a l =
185  foldi_from_until_internal Nat.O a (remove_n_first n l) m f
186
187(** val foldi_from :
188    Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
189    List.list -> 'a1 List.list -> 'a1 List.list **)
190let foldi_from n f a l =
191  foldi_from_until n (List.length l) f a l
192
193(** val foldi_until :
194    Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
195    List.list -> 'a1 List.list -> 'a1 List.list **)
196let foldi_until m f a l =
197  foldi_from_until Nat.O m f a l
198
199(** val foldi :
200    (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list ->
201    'a1 List.list -> 'a1 List.list **)
202let foldi f a l =
203  foldi_from_until Nat.O (List.length l) f a l
204
205(** val hd_safe : 'a1 List.list -> 'a1 **)
206let hd_safe l =
207  (match l with
208   | List.Nil -> (fun _ -> assert false (* absurd case *))
209   | List.Cons (hd0, tl) -> (fun _ -> hd0)) __
210
211(** val tail_safe : 'a1 List.list -> 'a1 List.list **)
212let tail_safe l =
213  (match l with
214   | List.Nil -> (fun _ -> assert false (* absurd case *))
215   | List.Cons (hd0, tl) -> (fun _ -> tl)) __
216
217(** val safe_split :
218    'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod **)
219let rec safe_split l index =
220  (match index with
221   | Nat.O -> (fun _ -> { Types.fst = List.Nil; Types.snd = l })
222   | Nat.S index' ->
223     (fun _ ->
224       (match l with
225        | List.Nil -> (fun _ -> assert false (* absurd case *))
226        | List.Cons (hd0, tl) ->
227          (fun _ ->
228            let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
229            { Types.fst = (List.Cons (hd0, l1)); Types.snd = l2 })) __)) __
230
231(** val nth_safe : Nat.nat -> 'a1 List.list -> 'a1 **)
232let rec nth_safe index the_list =
233  (match index with
234   | Nat.O ->
235     (match the_list with
236      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
237      | List.Cons (hd0, tl) -> (fun _ -> hd0))
238   | Nat.S index' ->
239     (match the_list with
240      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
241      | List.Cons (hd0, tl) -> (fun _ -> nth_safe index' tl))) __
242
243(** val last_safe : 'a1 List.list -> 'a1 **)
244let last_safe the_list =
245  nth_safe (Nat.minus (List.length the_list) (Nat.S Nat.O)) the_list
246
247(** val reduce :
248    'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
249    Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod **)
250let rec reduce left right =
251  match left with
252  | List.Nil ->
253    { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil }; Types.snd =
254      { Types.fst = List.Nil; Types.snd = right } }
255  | List.Cons (hd0, tl) ->
256    (match right with
257     | List.Nil ->
258       { Types.fst = { Types.fst = List.Nil; Types.snd = left }; Types.snd =
259         { Types.fst = List.Nil; Types.snd = List.Nil } }
260     | List.Cons (hd', tl') ->
261       let { Types.fst = cleft; Types.snd = cright } = reduce tl tl' in
262       let { Types.fst = commonl; Types.snd = restl } = cleft in
263       let { Types.fst = commonr; Types.snd = restr } = cright in
264       { Types.fst = { Types.fst = (List.Cons (hd0, commonl)); Types.snd =
265       restl }; Types.snd = { Types.fst = (List.Cons (hd', commonr));
266       Types.snd = restr } })
267
268(** val reduce_strong :
269    'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
270    Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
271    Types.sig0 **)
272let rec reduce_strong left right =
273  (match left with
274   | List.Nil ->
275     (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil };
276       Types.snd = { Types.fst = List.Nil; Types.snd = right } })
277   | List.Cons (hd0, tl) ->
278     (fun _ ->
279       (match right with
280        | List.Nil ->
281          (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = left };
282            Types.snd = { Types.fst = List.Nil; Types.snd = List.Nil } })
283        | List.Cons (hd', tl') ->
284          (fun _ ->
285            (let { Types.fst = cleft; Types.snd = cright } =
286               Types.pi1 (reduce_strong tl tl')
287             in
288            (fun _ ->
289            (let { Types.fst = commonl; Types.snd = restl } = cleft in
290            (fun _ ->
291            (let { Types.fst = commonr; Types.snd = restr } = cright in
292            (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd0, commonl));
293            Types.snd = restl }; Types.snd = { Types.fst = (List.Cons (hd',
294            commonr)); Types.snd = restr } })) __)) __)) __)) __)) __
295
296(** val map2_opt :
297    ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
298    Types.option **)
299let rec map2_opt f left right =
300  match left with
301  | List.Nil ->
302    (match right with
303     | List.Nil -> Types.Some List.Nil
304     | List.Cons (x, x0) -> Types.None)
305  | List.Cons (hd0, tl) ->
306    (match right with
307     | List.Nil -> Types.None
308     | List.Cons (hd', tl') ->
309       (match map2_opt f tl tl' with
310        | Types.None -> Types.None
311        | Types.Some tail0 -> Types.Some (List.Cons ((f hd0 hd'), tail0))))
312
313(** val map2 :
314    ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list **)
315let rec map2 f left right =
316  (match left with
317   | List.Nil ->
318     (match right with
319      | List.Nil -> (fun _ -> List.Nil)
320      | List.Cons (x, x0) ->
321        (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length x0)) __))
322   | List.Cons (hd0, tl) ->
323     (match right with
324      | List.Nil ->
325        (fun _ -> Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
326      | List.Cons (hd', tl') ->
327        (fun _ -> List.Cons ((f hd0 hd'), (map2 f tl tl'))))) __
328
329(** val map3 :
330    ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
331    List.list -> 'a4 List.list **)
332let rec map3 f left centre right =
333  (match left with
334   | List.Nil ->
335     (fun _ ->
336       (match centre with
337        | List.Nil ->
338          (fun _ ->
339            (match right with
340             | List.Nil -> (fun _ -> List.Nil)
341             | List.Cons (hd0, tl) ->
342               (fun _ ->
343                 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
344              __)
345        | List.Cons (hd0, tl) ->
346          (fun _ ->
347            Logic.eq_rect_Type0 (List.length centre)
348              (Logic.eq_rect_Type0 (List.length List.Nil) (fun _ ->
349                Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
350                (List.length centre)) (List.length right) __)) __)
351   | List.Cons (hd0, tl) ->
352     (fun _ ->
353       (match centre with
354        | List.Nil ->
355          (fun _ ->
356            Logic.eq_rect_Type0 (List.length centre)
357              (Logic.eq_rect_Type0 (List.length (List.Cons (hd0, tl)))
358                (fun _ ->
359                Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)
360                (List.length centre)) (List.length right) __)
361        | List.Cons (hd', tl') ->
362          (fun _ ->
363            (match right with
364             | List.Nil ->
365               (fun _ _ ->
366                 Obj.magic Nat.nat_discr (Nat.S (List.length tl')) Nat.O __)
367             | List.Cons (hd'', tl'') ->
368               (fun _ _ -> List.Cons ((f hd0 hd' hd''),
369                 (map3 f tl tl' tl'')))) __ __)) __)) __
370
371(** val eq_rect_Type0_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
372let eq_rect_Type0_r0 a h x =
373  (fun _ auto -> auto) __ h
374
375(** val safe_nth : Nat.nat -> 'a1 List.list -> 'a1 **)
376let rec safe_nth n l =
377  (match n with
378   | Nat.O ->
379     (match l with
380      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
381      | List.Cons (hd0, tl) -> (fun _ -> hd0))
382   | Nat.S n' ->
383     (match l with
384      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
385      | List.Cons (hd0, tl) -> (fun _ -> safe_nth n' tl))) __
386
387(** val nub_by_internal :
388    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
389let rec nub_by_internal f l = function
390| Nat.O ->
391  (match l with
392   | List.Nil -> List.Nil
393   | List.Cons (hd0, tl) -> l)
394| Nat.S n0 ->
395  (match l with
396   | List.Nil -> List.Nil
397   | List.Cons (hd0, tl) ->
398     List.Cons (hd0,
399       (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd0)) tl) n0)))
400
401(** val nub_by :
402    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
403let nub_by f l =
404  nub_by_internal f l (List.length l)
405
406(** val member :
407    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool **)
408let rec member eq a = function
409| List.Nil -> Bool.False
410| List.Cons (hd0, tl) -> Bool.orb (eq a hd0) (member eq a tl)
411
412(** val take : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
413let rec take n l =
414  match n with
415  | Nat.O -> List.Nil
416  | Nat.S n0 ->
417    (match l with
418     | List.Nil -> List.Nil
419     | List.Cons (hd0, tl) -> List.Cons (hd0, (take n0 tl)))
420
421(** val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
422let rec drop n l =
423  match n with
424  | Nat.O -> l
425  | Nat.S n0 ->
426    (match l with
427     | List.Nil -> List.Nil
428     | List.Cons (hd0, tl) -> drop n0 tl)
429
430(** val list_split :
431    Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod **)
432let list_split n l =
433  { Types.fst = (take n l); Types.snd = (drop n l) }
434
435(** val mapi_internal :
436    Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
437let rec mapi_internal n f = function
438| List.Nil -> List.Nil
439| List.Cons (hd0, tl) ->
440  List.Cons ((f n hd0), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))
441
442(** val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
443let mapi f l =
444  mapi_internal Nat.O f l
445
446(** val zip_pottier :
447    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
448let rec zip_pottier left right =
449  match left with
450  | List.Nil -> List.Nil
451  | List.Cons (hd0, tl) ->
452    (match right with
453     | List.Nil -> List.Nil
454     | List.Cons (hd', tl') ->
455       List.Cons ({ Types.fst = hd0; Types.snd = hd' }, (zip_pottier tl tl')))
456
457(** val zip_safe :
458    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
459let rec zip_safe left right =
460  (match left with
461   | List.Nil ->
462     (fun _ ->
463       (match right with
464        | List.Nil -> (fun _ -> List.Nil)
465        | List.Cons (hd0, tl) ->
466          (fun _ ->
467            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
468   | List.Cons (hd0, tl) ->
469     (fun _ ->
470       (match right with
471        | List.Nil ->
472          (fun _ ->
473            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
474        | List.Cons (hd', tl') ->
475          (fun _ -> List.Cons ({ Types.fst = hd0; Types.snd = hd' },
476            (zip_safe tl tl')))) __)) __
477
478(** val zip :
479    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
480    Types.option **)
481let rec zip l r =
482  match l with
483  | List.Nil -> Types.Some List.Nil
484  | List.Cons (hd0, tl) ->
485    (match r with
486     | List.Nil -> Types.None
487     | List.Cons (hd', tl') ->
488       (match zip tl tl' with
489        | Types.None -> Types.None
490        | Types.Some tail0 ->
491          Types.Some (List.Cons ({ Types.fst = hd0; Types.snd = hd' },
492            tail0))))
493
494(** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
495let rec foldl f a = function
496| List.Nil -> a
497| List.Cons (hd0, tl) -> foldl f (f a hd0) tl
498
499(** val rev : 'a1 List.list -> 'a1 List.list **)
500let rev l =
501  List.reverse l
502
503(** val fold_left_i_aux :
504    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1 **)
505let rec fold_left_i_aux f x i = function
506| List.Nil -> x
507| List.Cons (hd0, tl) -> fold_left_i_aux f (f i x hd0) (Nat.S i) tl
508
509(** val fold_left_i :
510    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
511let fold_left_i f x =
512  fold_left_i_aux f x Nat.O
513
514(** val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
515let function_apply f a =
516  f a
517
518(** val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1 **)
519let rec iterate f a = function
520| Nat.O -> a
521| Nat.S o -> f (iterate f a o)
522
523(** val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
524let rec division_aux m n p =
525  match ltb n (Nat.S p) with
526  | Bool.True -> Nat.O
527  | Bool.False ->
528    (match m with
529     | Nat.O -> Nat.O
530     | Nat.S q -> Nat.S (division_aux q (Nat.minus n (Nat.S p)) p))
531
532(** val division : Nat.nat -> Nat.nat -> Nat.nat **)
533let division m = function
534| Nat.O -> Nat.S m
535| Nat.S o -> division_aux m m o
536
537(** val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
538let rec modulus_aux m n p =
539  match Nat.leb n p with
540  | Bool.True -> n
541  | Bool.False ->
542    (match m with
543     | Nat.O -> n
544     | Nat.S o -> modulus_aux o (Nat.minus n (Nat.S p)) p)
545
546(** val modulus : Nat.nat -> Nat.nat -> Nat.nat **)
547let modulus m = function
548| Nat.O -> m
549| Nat.S o -> modulus_aux m m o
550
551(** val divide_with_remainder :
552    Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod **)
553let divide_with_remainder m n =
554  { Types.fst = (division m n); Types.snd = (modulus m n) }
555
556(** val less_than_or_equal_b_elim :
557    Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
558let less_than_or_equal_b_elim m n h1 h2 =
559  (match Nat.leb m n with
560   | Bool.True -> (fun _ _ -> h1 __)
561   | Bool.False -> (fun _ _ -> h2 __)) __ __
562
563open Div_and_mod
564
565(** val if_then_else_safe :
566    Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
567let if_then_else_safe b f g0 =
568  (match b with
569   | Bool.True -> f
570   | Bool.False -> g0) __
571
572(** val prod_jmdiscr :
573    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
574let prod_jmdiscr x y =
575  Logic.eq_rect_Type2 x
576    (let { Types.fst = a0; Types.snd = a10 } = x in
577    Obj.magic (fun _ dH -> dH __ __)) y
578
579(** val eq_rect_Type1_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
580let eq_rect_Type1_r0 a h x =
581  (fun _ auto -> auto) __ h
582
583(** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
584let some_Some_elim x y h =
585  h __
586
587(** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
588let pose a auto =
589  auto a __
590
591(** val eq_sum :
592    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
593    Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
594let eq_sum leq req left right =
595  match left with
596  | Types.Inl l ->
597    (match right with
598     | Types.Inl l' -> leq l l'
599     | Types.Inr x -> Bool.False)
600  | Types.Inr r ->
601    (match right with
602     | Types.Inl x -> Bool.False
603     | Types.Inr r' -> req r r')
604
605(** val eq_prod :
606    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
607    Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
608let eq_prod leq req left right =
609  let { Types.fst = l; Types.snd = r } = left in
610  let { Types.fst = l'; Types.snd = r' } = right in
611  Bool.andb (leq l l') (req r r')
612
Note: See TracBrowser for help on using the repository browser.