source: extracted/set_adt.ml @ 2730

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

Exported again.

File size: 2.8 KB
Line 
1type 'x set (* AXIOM TO BE REALIZED *)
2
3(** val set_empty : 'a1 set0 **)
4let set_empty =
5  failwith "AXIOM TO BE REALIZED"
6
7(** val set_size : 'a1 set0 -> Nat.nat **)
8let set_size =
9  failwith "AXIOM TO BE REALIZED"
10
11(** val set_to_list : 'a1 set0 -> 'a1 List.list **)
12let set_to_list =
13  failwith "AXIOM TO BE REALIZED"
14
15(** val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0 **)
16let set_insert =
17  failwith "AXIOM TO BE REALIZED"
18
19(** val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0 **)
20let set_remove =
21  failwith "AXIOM TO BE REALIZED"
22
23(** val set_member :
24    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
25let set_member =
26  failwith "AXIOM TO BE REALIZED"
27
28(** val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
29let set_forall =
30  failwith "AXIOM TO BE REALIZED"
31
32(** val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
33let set_exists =
34  failwith "AXIOM TO BE REALIZED"
35
36(** val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 **)
37let set_filter =
38  failwith "AXIOM TO BE REALIZED"
39
40(** val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0 **)
41let set_map =
42  failwith "AXIOM TO BE REALIZED"
43
44(** val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2 **)
45let set_fold =
46  failwith "AXIOM TO BE REALIZED"
47
48(** val set_equal :
49    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
50let set_equal =
51  failwith "AXIOM TO BE REALIZED"
52
53(** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
54let set_diff =
55  failwith "AXIOM TO BE REALIZED"
56
57(** val set_is_empty : 'a1 set0 -> Bool.bool **)
58let set_is_empty set1 =
59  Util.eq_nat (set_size set1) Nat.O
60
61(** val set_singleton : 'a1 -> 'a1 set0 **)
62let set_singleton elt =
63  set_insert elt set_empty
64
65(** val set_from_list : 'a1 List.list -> 'a1 set0 **)
66let set_from_list the_list =
67  List.foldr set_insert set_empty the_list
68
69(** val set_split :
70    ('a1 -> Bool.bool) -> 'a1 set0 -> ('a1 set0, 'a1 set0) Types.prod **)
71let set_split pred0 the_set =
72  let left = set_filter pred0 the_set in
73  let npred = fun x -> Bool.notb (pred0 x) in
74  let right = set_filter npred the_set in
75  { Types.fst = left; Types.snd = right }
76
77(** val set_subset :
78    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
79let set_subset eq left right =
80  set_forall (fun elt -> set_member eq elt right) left
81
82(** val set_subseteq :
83    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
84let set_subseteq eq left right =
85  Bool.andb (set_equal eq left right) (set_subset eq left right)
86
87(** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
88let set_union left right =
89  set_fold set_insert left right
90
91(** val set_intersection :
92    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
93let set_intersection eq left right =
94  set_filter (fun elt -> set_member eq elt right) left
95
Note: See TracBrowser for help on using the repository browser.