source: extracted/list.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 9.0 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19type 'a list =
20| Nil
21| Cons of 'a * 'a list
22
23(** val list_rect_Type4 :
24    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
25let rec list_rect_Type4 h_nil h_cons = function
26| Nil -> h_nil
27| Cons (x_801, x_800) ->
28  h_cons x_801 x_800 (list_rect_Type4 h_nil h_cons x_800)
29
30(** val list_rect_Type3 :
31    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
32let rec list_rect_Type3 h_nil h_cons = function
33| Nil -> h_nil
34| Cons (x_811, x_810) ->
35  h_cons x_811 x_810 (list_rect_Type3 h_nil h_cons x_810)
36
37(** val list_rect_Type2 :
38    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
39let rec list_rect_Type2 h_nil h_cons = function
40| Nil -> h_nil
41| Cons (x_816, x_815) ->
42  h_cons x_816 x_815 (list_rect_Type2 h_nil h_cons x_815)
43
44(** val list_rect_Type1 :
45    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
46let rec list_rect_Type1 h_nil h_cons = function
47| Nil -> h_nil
48| Cons (x_821, x_820) ->
49  h_cons x_821 x_820 (list_rect_Type1 h_nil h_cons x_820)
50
51(** val list_rect_Type0 :
52    'a2 -> ('a1 -> 'a1 list -> 'a2 -> 'a2) -> 'a1 list -> 'a2 **)
53let rec list_rect_Type0 h_nil h_cons = function
54| Nil -> h_nil
55| Cons (x_826, x_825) ->
56  h_cons x_826 x_825 (list_rect_Type0 h_nil h_cons x_825)
57
58(** val list_inv_rect_Type4 :
59    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
60    -> 'a2 **)
61let list_inv_rect_Type4 hterm h1 h2 =
62  let hcut = list_rect_Type4 h1 h2 hterm in hcut __
63
64(** val list_inv_rect_Type3 :
65    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
66    -> 'a2 **)
67let list_inv_rect_Type3 hterm h1 h2 =
68  let hcut = list_rect_Type3 h1 h2 hterm in hcut __
69
70(** val list_inv_rect_Type2 :
71    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
72    -> 'a2 **)
73let list_inv_rect_Type2 hterm h1 h2 =
74  let hcut = list_rect_Type2 h1 h2 hterm in hcut __
75
76(** val list_inv_rect_Type1 :
77    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
78    -> 'a2 **)
79let list_inv_rect_Type1 hterm h1 h2 =
80  let hcut = list_rect_Type1 h1 h2 hterm in hcut __
81
82(** val list_inv_rect_Type0 :
83    'a1 list -> (__ -> 'a2) -> ('a1 -> 'a1 list -> (__ -> 'a2) -> __ -> 'a2)
84    -> 'a2 **)
85let list_inv_rect_Type0 hterm h1 h2 =
86  let hcut = list_rect_Type0 h1 h2 hterm in hcut __
87
88(** val list_discr : 'a1 list -> 'a1 list -> __ **)
89let list_discr x y =
90  Logic.eq_rect_Type2 x
91    (match x with
92     | Nil -> Obj.magic (fun _ dH -> dH)
93     | Cons (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
94
95(** val append : 'a1 list -> 'a1 list -> 'a1 list **)
96let rec append l1 l2 =
97  match l1 with
98  | Nil -> l2
99  | Cons (hd, tl) -> Cons (hd, (append tl l2))
100
101(** val hd : 'a1 list -> 'a1 -> 'a1 **)
102let hd l d =
103  match l with
104  | Nil -> d
105  | Cons (a, x) -> a
106
107(** val tail : 'a1 list -> 'a1 list **)
108let tail = function
109| Nil -> Nil
110| Cons (hd0, tl) -> tl
111
112(** val option_hd : 'a1 list -> 'a1 Types.option **)
113let option_hd = function
114| Nil -> Types.None
115| Cons (a, x) -> Types.Some a
116
117(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
118let rec map f = function
119| Nil -> Nil
120| Cons (x, tl) -> Cons ((f x), (map f tl))
121
122(** val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
123let rec foldr f b = function
124| Nil -> b
125| Cons (a, l0) -> f a (foldr f b l0)
126
127(** val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list **)
128let filter p =
129  foldr (fun x l0 ->
130    match p x with
131    | Bool.True -> Cons (x, l0)
132    | Bool.False -> l0) Nil
133
134(** val compose0 :
135    ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **)
136let compose0 f l1 l2 =
137  foldr (fun i acc -> append (map (f i) l2) acc) Nil l1
138
139(** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **)
140let rec rev_append l1 l2 =
141  match l1 with
142  | Nil -> l2
143  | Cons (a, tl) -> rev_append tl (Cons (a, l2))
144
145(** val reverse : 'a1 list -> 'a1 list **)
146let reverse l =
147  rev_append l Nil
148
149(** val length : 'a1 list -> Nat.nat **)
150let rec length = function
151| Nil -> Nat.O
152| Cons (a, tl) -> Nat.S (length tl)
153
154type mem = __
155
156(** val split_rev :
157    'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
158let rec split_rev l acc = function
159| Nat.O -> { Types.fst = acc; Types.snd = l }
160| Nat.S m ->
161  (match l with
162   | Nil -> { Types.fst = acc; Types.snd = Nil }
163   | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m)
164
165(** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
166let split l n =
167  let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in
168  { Types.fst = (reverse l1); Types.snd = l2 }
169
170(** val flatten : 'a1 list list -> 'a1 list **)
171let flatten l =
172  foldr append Nil l
173
174(** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **)
175let rec nth n l d =
176  match n with
177  | Nat.O -> hd l d
178  | Nat.S m -> nth m (tail l) d
179
180(** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **)
181let rec nth_opt n = function
182| Nil -> Types.None
183| Cons (h, t) ->
184  (match n with
185   | Nat.O -> Types.Some h
186   | Nat.S m -> nth_opt m t)
187
188type all = __
189
190type allr = __
191
192type exists = __
193
194(** val fold :
195    ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
196    list -> 'a2 **)
197let rec fold op b p f = function
198| Nil -> b
199| Cons (a, l0) ->
200  (match p a with
201   | Bool.True -> op (f a) (fold op b p f l0)
202   | Bool.False -> fold op b p f l0)
203
204type 'a aop =
205  'a -> 'a -> 'a
206  (* singleton inductive, whose constructor was mk_Aop *)
207
208(** val aop_rect_Type4 :
209    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
210let rec aop_rect_Type4 nil h_mk_Aop x_861 =
211  let op = x_861 in h_mk_Aop op __ __ __
212
213(** val aop_rect_Type5 :
214    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
215let rec aop_rect_Type5 nil h_mk_Aop x_863 =
216  let op = x_863 in h_mk_Aop op __ __ __
217
218(** val aop_rect_Type3 :
219    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
220let rec aop_rect_Type3 nil h_mk_Aop x_865 =
221  let op = x_865 in h_mk_Aop op __ __ __
222
223(** val aop_rect_Type2 :
224    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
225let rec aop_rect_Type2 nil h_mk_Aop x_867 =
226  let op = x_867 in h_mk_Aop op __ __ __
227
228(** val aop_rect_Type1 :
229    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
230let rec aop_rect_Type1 nil h_mk_Aop x_869 =
231  let op = x_869 in h_mk_Aop op __ __ __
232
233(** val aop_rect_Type0 :
234    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
235let rec aop_rect_Type0 nil h_mk_Aop x_871 =
236  let op = x_871 in h_mk_Aop op __ __ __
237
238(** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
239let rec op nil xxx =
240  let yyy = xxx in yyy
241
242(** val aop_inv_rect_Type4 :
243    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
244    'a2 **)
245let aop_inv_rect_Type4 x2 hterm h1 =
246  let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
247
248(** val aop_inv_rect_Type3 :
249    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
250    'a2 **)
251let aop_inv_rect_Type3 x2 hterm h1 =
252  let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
253
254(** val aop_inv_rect_Type2 :
255    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
256    'a2 **)
257let aop_inv_rect_Type2 x2 hterm h1 =
258  let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
259
260(** val aop_inv_rect_Type1 :
261    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
262    'a2 **)
263let aop_inv_rect_Type1 x2 hterm h1 =
264  let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
265
266(** val aop_inv_rect_Type0 :
267    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
268    'a2 **)
269let aop_inv_rect_Type0 x2 hterm h1 =
270  let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
271
272(** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
273let aop_discr a2 x y =
274  Logic.eq_rect_Type2 x
275    (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
276
277(** val dpi1__o__op :
278    'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
279let dpi1__o__op x1 x3 =
280  op x1 x3.Types.dpi1
281
282(** val lhd : 'a1 list -> Nat.nat -> 'a1 list **)
283let rec lhd l = function
284| Nat.O -> Nil
285| Nat.S n0 ->
286  (match l with
287   | Nil -> Nil
288   | Cons (a, l0) -> Cons (a, (lhd l0 n0)))
289
290(** val ltl : 'a1 list -> Nat.nat -> 'a1 list **)
291let rec ltl l = function
292| Nat.O -> l
293| Nat.S n0 -> ltl (tail l) n0
294
295(** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **)
296let rec find f = function
297| Nil -> Types.None
298| Cons (h, t) ->
299  (match f h with
300   | Types.None -> find f t
301   | Types.Some b -> Types.Some b)
302
303(** val position_of_aux :
304    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **)
305let rec position_of_aux found l acc =
306  match l with
307  | Nil -> Types.None
308  | Cons (h, t) ->
309    (match found h with
310     | Bool.True -> Types.Some acc
311     | Bool.False -> position_of_aux found t (Nat.S acc))
312
313(** val position_of :
314    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **)
315let position_of found l =
316  position_of_aux found l Nat.O
317
318(** val make_list : 'a1 -> Nat.nat -> 'a1 list **)
319let rec make_list a = function
320| Nat.O -> Nil
321| Nat.S m -> Cons (a, (make_list a m))
322
Note: See TracBrowser for help on using the repository browser.