mindless-coding/sets.mli at master · jonleivent/mindless-coding · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146


type __ = Obj.t

type nat =
| O
| S of nat

type comparison =
| Eq
| Lt
| Gt

type compareSpecT =
| CompEqT
| CompLtT
| CompGtT

val id : 'a1 -> 'a1

type 'a sig0 =
  'a
  (* singleton inductive, whose constructor was exist *)

type 'a eqDec = 'a -> 'a -> bool

type 'a ordered = { eq_dec : 'a eqDec; compare : ('a -> 'a -> comparison);
                    compare_spec : ('a -> 'a -> compareSpecT) }

val compare_spec : 'a1 ordered -> 'a1 -> 'a1 -> compareSpecT

type ('a, 'tree) breakResult =
| BreakLeaf
| BreakNode of 'tree * 'a * 'tree

type ('a, 'tree) insertResult =
| InsertFound
| Inserted of 'tree

type ('a, 'tree) delminResult =
| DelminLeaf
| DelminNode of 'a * 'tree

type ('a, 'tree) delmaxResult =
| DelmaxLeaf
| DelmaxNode of 'a * 'tree

type ('a, 'tree) deleteResult =
| DelNotFound
| Deleted of 'tree

type 'a tree = { leaf : __; break : (__ -> __ -> ('a, __) breakResult);
                 insert : ('a -> __ -> __ -> ('a, __) insertResult);
                 join : (__ -> __ -> 'a -> __ -> __ -> __ -> __);
                 delmin : (__ -> __ -> ('a, __) delminResult);
                 delmax : (__ -> __ -> ('a, __) delmaxResult);
                 delete : ('a -> __ -> __ -> ('a, __) deleteResult) }

type 'a tree0 = __

val leaf : 'a1 ordered -> 'a1 tree -> 'a1 tree0

val break :
  'a1 ordered -> 'a1 tree -> 'a1 tree0 -> ('a1, 'a1 tree0) breakResult

val join :
  'a1 ordered -> 'a1 tree -> 'a1 tree0 -> 'a1 -> 'a1 tree0 -> 'a1 tree0

val delmin :
  'a1 ordered -> 'a1 tree -> 'a1 tree0 -> ('a1, 'a1 tree0) delminResult

val enat_xrect : (__ -> (__ -> __ -> 'a1) -> 'a1) -> 'a1

type a (* AXIOM TO BE REALIZED *)

val ordA : a ordered

val treeA : a tree

type findResult =
| Found
| NotFound

val find : a -> a tree0 -> findResult

type splitResult =
| Split of bool * a tree0 * a tree0

val split : a -> a tree0 -> splitResult

type unionResult =
  a tree0
  (* singleton inductive, whose constructor was UnionResult *)

val union : a tree0 -> a tree0 -> unionResult

val delete_free_delmin : a tree0 -> (a, a tree0) delminResult

val merge : a tree0 -> a tree0 -> a tree0

type intersectResult =
  a tree0
  (* singleton inductive, whose constructor was IntersectResult *)

val intersection : a tree0 -> a tree0 -> intersectResult

type setdiffResult =
  a tree0
  (* singleton inductive, whose constructor was SetDiffResult *)

val setdifference : a tree0 -> a tree0 -> setdiffResult

type filterResult =
  a tree0
  (* singleton inductive, whose constructor was Filtered *)

val filter : (a -> bool) -> a tree0 -> filterResult

type partitionResult =
| Partitioned of a tree0 * a tree0

val partition : (a -> bool) -> a tree0 -> partitionResult

type subsetResult =
| IsSubset of bool
| NotSubset of a

val subset : a tree0 -> a tree0 -> subsetResult

val equiv : a tree0 -> a tree0 -> bool

type 't ecomprehension = 't

type 'b foldLeftResult = 'b ecomprehension

val fold_left : ('a1 -> a -> 'a1) -> a tree0 -> 'a1 -> 'a1 foldLeftResult

type 'b foldRightResult = 'b ecomprehension

val fold_right : (a -> 'a1 -> 'a1) -> 'a1 -> a tree0 -> 'a1 foldRightResult

val cardinality : a tree0 -> nat ecomprehension

val map : (a -> 'a1) -> a tree0 -> 'a1 list ecomprehension

val flatten : a tree0 -> a list ecomprehension