source: extracted/lists.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 2.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 Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29(** val all0 : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
30let rec all0 p = function
31| List.Nil -> Bool.True
32| List.Cons (h, t) -> Bool.andb (p h) (all0 p t)
33
34type ('x, 'x0) all2 = __
35
36(** val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
37let rec map_All f l =
38  (match l with
39   | List.Nil -> (fun _ -> List.Nil)
40   | List.Cons (hd0, tl) -> (fun _ -> List.Cons ((f hd0 __), (map_All f tl))))
41    __
42
43open Setoids
44
45open Monad
46
47open Option
48
49(** val append0 : 'a1 List.list List.aop **)
50let append0 =
51  List.append
52
53(** val list0 : Monad.monadProps **)
54let list0 =
55  Monad.makeMonadProps (fun _ x -> List.Cons (x, List.Nil)) (fun _ _ l f ->
56    List.foldr (fun x -> List.append (f x)) List.Nil l)
57
58(** val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
59let rec count f = function
60| List.Nil -> Nat.O
61| List.Cons (x, l') ->
62  Nat.plus
63    (match f x with
64     | Bool.True -> Nat.S Nat.O
65     | Bool.False -> Nat.O) (count f l')
66
67(** val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
68let position_of_safe test l =
69  Option.opt_safe (List.position_of test l)
70
71(** val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat **)
72let index_of test l =
73  position_of_safe test l
74
75(** val ordered_insert :
76    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list **)
77let rec ordered_insert lt a = function
78| List.Nil -> List.Cons (a, List.Nil)
79| List.Cons (h, t) ->
80  (match lt a h with
81   | Bool.True -> List.Cons (a, (List.Cons (h, t)))
82   | Bool.False -> List.Cons (h, (ordered_insert lt a t)))
83
84(** val insert_sort :
85    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
86let rec insert_sort lt = function
87| List.Nil -> List.Nil
88| List.Cons (h, t) -> ordered_insert lt h (insert_sort lt t)
89
90(** val range_strong_internal :
91    Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list **)
92let rec range_strong_internal index how_many end0 =
93  (match how_many with
94   | Nat.O -> (fun _ -> List.Nil)
95   | Nat.S k ->
96     (fun _ -> List.Cons (index,
97       (range_strong_internal (Nat.S index) k end0)))) __
98
99(** val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list **)
100let range_strong end0 =
101  range_strong_internal Nat.O end0 end0
102
Note: See TracBrowser for help on using the repository browser.