source: extracted/list.ml @ 2649

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

...

File size: 9.1 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 option_cons : 'a1 Types.option -> 'a1 list -> 'a1 list **)
118let option_cons c l =
119  match c with
120  | Types.None -> l
121  | Types.Some c0 -> Cons (c0, l)
122
123(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
124let rec map f = function
125| Nil -> Nil
126| Cons (x, tl) -> Cons ((f x), (map f tl))
127
128(** val foldr : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
129let rec foldr f b = function
130| Nil -> b
131| Cons (a, l0) -> f a (foldr f b l0)
132
133(** val filter : ('a1 -> Bool.bool) -> 'a1 list -> 'a1 list **)
134let filter p =
135  foldr (fun x l0 ->
136    match p x with
137    | Bool.True -> Cons (x, l0)
138    | Bool.False -> l0) Nil
139
140(** val compose0 :
141    ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **)
142let compose0 f l1 l2 =
143  foldr (fun i acc -> append (map (f i) l2) acc) Nil l1
144
145(** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **)
146let rec rev_append l1 l2 =
147  match l1 with
148  | Nil -> l2
149  | Cons (a, tl) -> rev_append tl (Cons (a, l2))
150
151(** val reverse : 'a1 list -> 'a1 list **)
152let reverse l =
153  rev_append l Nil
154
155(** val length : 'a1 list -> Nat.nat **)
156let rec length = function
157| Nil -> Nat.O
158| Cons (a, tl) -> Nat.S (length tl)
159
160type mem = __
161
162(** val split_rev :
163    'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
164let rec split_rev l acc = function
165| Nat.O -> { Types.fst = acc; Types.snd = l }
166| Nat.S m ->
167  (match l with
168   | Nil -> { Types.fst = acc; Types.snd = Nil }
169   | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m)
170
171(** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
172let split l n =
173  let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in
174  { Types.fst = (reverse l1); Types.snd = l2 }
175
176(** val flatten : 'a1 list list -> 'a1 list **)
177let flatten l =
178  foldr append Nil l
179
180(** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **)
181let rec nth n l d =
182  match n with
183  | Nat.O -> hd l d
184  | Nat.S m -> nth m (tail l) d
185
186(** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **)
187let rec nth_opt n = function
188| Nil -> Types.None
189| Cons (h, t) ->
190  (match n with
191   | Nat.O -> Types.Some h
192   | Nat.S m -> nth_opt m t)
193
194type all = __
195
196type allr = __
197
198type exists = __
199
200(** val fold :
201    ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
202    list -> 'a2 **)
203let rec fold op b p f = function
204| Nil -> b
205| Cons (a, l0) ->
206  (match p a with
207   | Bool.True -> op (f a) (fold op b p f l0)
208   | Bool.False -> fold op b p f l0)
209
210type 'a aop =
211  'a -> 'a -> 'a
212  (* singleton inductive, whose constructor was mk_Aop *)
213
214(** val aop_rect_Type4 :
215    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
216let rec aop_rect_Type4 nil h_mk_Aop x_861 =
217  let op = x_861 in h_mk_Aop op __ __ __
218
219(** val aop_rect_Type5 :
220    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
221let rec aop_rect_Type5 nil h_mk_Aop x_863 =
222  let op = x_863 in h_mk_Aop op __ __ __
223
224(** val aop_rect_Type3 :
225    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
226let rec aop_rect_Type3 nil h_mk_Aop x_865 =
227  let op = x_865 in h_mk_Aop op __ __ __
228
229(** val aop_rect_Type2 :
230    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
231let rec aop_rect_Type2 nil h_mk_Aop x_867 =
232  let op = x_867 in h_mk_Aop op __ __ __
233
234(** val aop_rect_Type1 :
235    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
236let rec aop_rect_Type1 nil h_mk_Aop x_869 =
237  let op = x_869 in h_mk_Aop op __ __ __
238
239(** val aop_rect_Type0 :
240    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
241let rec aop_rect_Type0 nil h_mk_Aop x_871 =
242  let op = x_871 in h_mk_Aop op __ __ __
243
244(** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
245let rec op nil xxx =
246  let yyy = xxx in yyy
247
248(** val aop_inv_rect_Type4 :
249    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
250    'a2 **)
251let aop_inv_rect_Type4 x2 hterm h1 =
252  let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
253
254(** val aop_inv_rect_Type3 :
255    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
256    'a2 **)
257let aop_inv_rect_Type3 x2 hterm h1 =
258  let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
259
260(** val aop_inv_rect_Type2 :
261    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
262    'a2 **)
263let aop_inv_rect_Type2 x2 hterm h1 =
264  let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
265
266(** val aop_inv_rect_Type1 :
267    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
268    'a2 **)
269let aop_inv_rect_Type1 x2 hterm h1 =
270  let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
271
272(** val aop_inv_rect_Type0 :
273    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
274    'a2 **)
275let aop_inv_rect_Type0 x2 hterm h1 =
276  let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
277
278(** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
279let aop_discr a2 x y =
280  Logic.eq_rect_Type2 x
281    (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
282
283(** val dpi1__o__op :
284    'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
285let dpi1__o__op x1 x3 =
286  op x1 x3.Types.dpi1
287
288(** val lhd : 'a1 list -> Nat.nat -> 'a1 list **)
289let rec lhd l = function
290| Nat.O -> Nil
291| Nat.S n0 ->
292  (match l with
293   | Nil -> Nil
294   | Cons (a, l0) -> Cons (a, (lhd l0 n0)))
295
296(** val ltl : 'a1 list -> Nat.nat -> 'a1 list **)
297let rec ltl l = function
298| Nat.O -> l
299| Nat.S n0 -> ltl (tail l) n0
300
301(** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **)
302let rec find f = function
303| Nil -> Types.None
304| Cons (h, t) ->
305  (match f h with
306   | Types.None -> find f t
307   | Types.Some b -> Types.Some b)
308
309(** val position_of_aux :
310    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **)
311let rec position_of_aux found l acc =
312  match l with
313  | Nil -> Types.None
314  | Cons (h, t) ->
315    (match found h with
316     | Bool.True -> Types.Some acc
317     | Bool.False -> position_of_aux found t (Nat.S acc))
318
319(** val position_of :
320    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **)
321let position_of found l =
322  position_of_aux found l Nat.O
323
324(** val make_list : 'a1 -> Nat.nat -> 'a1 list **)
325let rec make_list a = function
326| Nat.O -> Nil
327| Nat.S m -> Cons (a, (make_list a m))
328
Note: See TracBrowser for help on using the repository browser.