source: driver/extracted/list.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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_723, x_722) ->
28  h_cons x_723 x_722 (list_rect_Type4 h_nil h_cons x_722)
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_733, x_732) ->
35  h_cons x_733 x_732 (list_rect_Type3 h_nil h_cons x_732)
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_738, x_737) ->
42  h_cons x_738 x_737 (list_rect_Type2 h_nil h_cons x_737)
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_743, x_742) ->
49  h_cons x_743 x_742 (list_rect_Type1 h_nil h_cons x_742)
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_748, x_747) ->
56  h_cons x_748 x_747 (list_rect_Type0 h_nil h_cons x_747)
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 compose : ('a1 -> 'a2 -> 'a3) -> 'a1 list -> 'a2 list -> 'a3 list **)
141let compose f l1 l2 =
142  foldr (fun i acc -> append (map (f i) l2) acc) Nil l1
143
144(** val rev_append : 'a1 list -> 'a1 list -> 'a1 list **)
145let rec rev_append l1 l2 =
146  match l1 with
147  | Nil -> l2
148  | Cons (a, tl) -> rev_append tl (Cons (a, l2))
149
150(** val reverse : 'a1 list -> 'a1 list **)
151let reverse l =
152  rev_append l Nil
153
154(** val length : 'a1 list -> Nat.nat **)
155let rec length = function
156| Nil -> Nat.O
157| Cons (a, tl) -> Nat.S (length tl)
158
159(** val split_rev :
160    'a1 list -> 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
161let rec split_rev l acc = function
162| Nat.O -> { Types.fst = acc; Types.snd = l }
163| Nat.S m ->
164  (match l with
165   | Nil -> { Types.fst = acc; Types.snd = Nil }
166   | Cons (a, tl) -> split_rev tl (Cons (a, acc)) m)
167
168(** val split : 'a1 list -> Nat.nat -> ('a1 list, 'a1 list) Types.prod **)
169let split l n =
170  let { Types.fst = l1; Types.snd = l2 } = split_rev l Nil n in
171  { Types.fst = (reverse l1); Types.snd = l2 }
172
173(** val flatten : 'a1 list list -> 'a1 list **)
174let flatten l =
175  foldr append Nil l
176
177(** val nth : Nat.nat -> 'a1 list -> 'a1 -> 'a1 **)
178let rec nth n l d =
179  match n with
180  | Nat.O -> hd l d
181  | Nat.S m -> nth m (tail l) d
182
183(** val nth_opt : Nat.nat -> 'a1 list -> 'a1 Types.option **)
184let rec nth_opt n = function
185| Nil -> Types.None
186| Cons (h, t) ->
187  (match n with
188   | Nat.O -> Types.Some h
189   | Nat.S m -> nth_opt m t)
190
191(** val fold :
192    ('a2 -> 'a2 -> 'a2) -> 'a2 -> ('a1 -> Bool.bool) -> ('a1 -> 'a2) -> 'a1
193    list -> 'a2 **)
194let rec fold op b p f = function
195| Nil -> b
196| Cons (a, l0) ->
197  (match p a with
198   | Bool.True -> op (f a) (fold op b p f l0)
199   | Bool.False -> fold op b p f l0)
200
201type 'a aop =
202  'a -> 'a -> 'a
203  (* singleton inductive, whose constructor was mk_Aop *)
204
205(** val aop_rect_Type4 :
206    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
207let rec aop_rect_Type4 nil h_mk_Aop x_783 =
208  let op = x_783 in h_mk_Aop op __ __ __
209
210(** val aop_rect_Type5 :
211    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
212let rec aop_rect_Type5 nil h_mk_Aop x_785 =
213  let op = x_785 in h_mk_Aop op __ __ __
214
215(** val aop_rect_Type3 :
216    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
217let rec aop_rect_Type3 nil h_mk_Aop x_787 =
218  let op = x_787 in h_mk_Aop op __ __ __
219
220(** val aop_rect_Type2 :
221    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
222let rec aop_rect_Type2 nil h_mk_Aop x_789 =
223  let op = x_789 in h_mk_Aop op __ __ __
224
225(** val aop_rect_Type1 :
226    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
227let rec aop_rect_Type1 nil h_mk_Aop x_791 =
228  let op = x_791 in h_mk_Aop op __ __ __
229
230(** val aop_rect_Type0 :
231    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
232let rec aop_rect_Type0 nil h_mk_Aop x_793 =
233  let op = x_793 in h_mk_Aop op __ __ __
234
235(** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
236let rec op nil xxx =
237  let yyy = xxx in yyy
238
239(** val aop_inv_rect_Type4 :
240    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
241    'a2 **)
242let aop_inv_rect_Type4 x2 hterm h1 =
243  let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
244
245(** val aop_inv_rect_Type3 :
246    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
247    'a2 **)
248let aop_inv_rect_Type3 x2 hterm h1 =
249  let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
250
251(** val aop_inv_rect_Type2 :
252    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
253    'a2 **)
254let aop_inv_rect_Type2 x2 hterm h1 =
255  let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
256
257(** val aop_inv_rect_Type1 :
258    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
259    'a2 **)
260let aop_inv_rect_Type1 x2 hterm h1 =
261  let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
262
263(** val aop_inv_rect_Type0 :
264    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
265    'a2 **)
266let aop_inv_rect_Type0 x2 hterm h1 =
267  let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
268
269(** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
270let aop_discr a2 x y =
271  Logic.eq_rect_Type2 x
272    (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
273
274(** val dpi1__o__op :
275    'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
276let dpi1__o__op x1 x3 =
277  op x1 x3.Types.dpi1
278
279(** val lhd : 'a1 list -> Nat.nat -> 'a1 list **)
280let rec lhd l = function
281| Nat.O -> Nil
282| Nat.S n0 ->
283  (match l with
284   | Nil -> Nil
285   | Cons (a, l0) -> Cons (a, (lhd l0 n0)))
286
287(** val ltl : 'a1 list -> Nat.nat -> 'a1 list **)
288let rec ltl l = function
289| Nat.O -> l
290| Nat.S n0 -> ltl (tail l) n0
291
292(** val find : ('a1 -> 'a2 Types.option) -> 'a1 list -> 'a2 Types.option **)
293let rec find f = function
294| Nil -> Types.None
295| Cons (h, t) ->
296  (match f h with
297   | Types.None -> find f t
298   | Types.Some b -> Types.Some b)
299
300(** val position_of_aux :
301    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat -> Nat.nat Types.option **)
302let rec position_of_aux found l acc =
303  match l with
304  | Nil -> Types.None
305  | Cons (h, t) ->
306    (match found h with
307     | Bool.True -> Types.Some acc
308     | Bool.False -> position_of_aux found t (Nat.S acc))
309
310(** val position_of :
311    ('a1 -> Bool.bool) -> 'a1 list -> Nat.nat Types.option **)
312let position_of found l =
313  position_of_aux found l Nat.O
314
315(** val make_list : 'a1 -> Nat.nat -> 'a1 list **)
316let rec make_list a = function
317| Nat.O -> Nil
318| Nat.S m -> Cons (a, (make_list a m))
319
Note: See TracBrowser for help on using the repository browser.