source: extracted/util.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 19.5 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 exponential : Nat.nat -> Nat.nat -> Nat.nat **)
557let rec exponential m = function
558| Nat.O -> Nat.S Nat.O
559| Nat.S o -> Nat.times m (exponential m o)
560
561(** val less_than_or_equal_b_elim :
562    Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
563let less_than_or_equal_b_elim m n h1 h2 =
564  (match Nat.leb m n with
565   | Bool.True -> (fun _ _ -> h1 __)
566   | Bool.False -> (fun _ _ -> h2 __)) __ __
567
568open Div_and_mod
569
570type even_p = __
571
572type odd_p = __
573
574(** val if_then_else_safe :
575    Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
576let if_then_else_safe b f g0 =
577  (match b with
578   | Bool.True -> f
579   | Bool.False -> g0) __
580
581(** val prod_jmdiscr :
582    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
583let prod_jmdiscr x y =
584  Logic.eq_rect_Type2 x
585    (let { Types.fst = a0; Types.snd = a10 } = x in
586    Obj.magic (fun _ dH -> dH __ __)) y
587
588(** val eq_rect_Type1_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
589let eq_rect_Type1_r0 a h x =
590  (fun _ auto -> auto) __ h
591
592(** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
593let some_Some_elim x y h =
594  h __
595
596(** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
597let pose a auto =
598  auto a __
599
600(** val eq_sum :
601    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
602    Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
603let eq_sum leq req left right =
604  match left with
605  | Types.Inl l ->
606    (match right with
607     | Types.Inl l' -> leq l l'
608     | Types.Inr x -> Bool.False)
609  | Types.Inr r ->
610    (match right with
611     | Types.Inl x -> Bool.False
612     | Types.Inr r' -> req r r')
613
614(** val eq_prod :
615    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
616    Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
617let eq_prod leq req left right =
618  let { Types.fst = l; Types.snd = r } = left in
619  let { Types.fst = l'; Types.snd = r' } = right in
620  Bool.andb (leq l l') (req r r')
621
Note: See TracBrowser for help on using the repository browser.