source: extracted/set_adt.ml @ 2731

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

Minimal set of axioms implemented to make the driver run.

File size: 4.3 KB
Line 
1    type 'a set = Empty | Node of 'a set * 'a * 'a set * int
2
3    let height = function
4        Empty -> 0
5      | Node(_, _, _, h) -> h
6
7    let create l v r =
8      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
9      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
10      Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
11
12    let bal l v r =
13      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
14      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
15      if hl > hr + 2 then begin
16        match l with
17          Empty -> invalid_arg "Set.bal"
18        | Node(ll, lv, lr, _) ->
19            if height ll >= height lr then
20              create ll lv (create lr v r)
21            else begin
22              match lr with
23                Empty -> invalid_arg "Set.bal"
24              | Node(lrl, lrv, lrr, _)->
25                  create (create ll lv lrl) lrv (create lrr v r)
26            end
27      end else if hr > hl + 2 then begin
28        match r with
29          Empty -> invalid_arg "Set.bal"
30        | Node(rl, rv, rr, _) ->
31            if height rr >= height rl then
32              create (create l v rl) rv rr
33            else begin
34              match rl with
35                Empty -> invalid_arg "Set.bal"
36              | Node(rll, rlv, rlr, _) ->
37                  create (create l v rll) rlv (create rlr rv rr)
38            end
39      end else
40        Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1))
41
42    let rec add x = function
43       Empty -> Node(Empty, x, Empty, 1)
44     | Node(l, v, r, _) as t ->
45         let c = compare x v in
46         if c = 0 then t else
47         if c < 0 then bal (add x l) v r else bal l v (add x r)
48
49(** val set_empty : 'a1 set0 **)
50let set_empty = Empty
51
52(** val set_size : 'a1 set0 -> Nat.nat **)
53let set_size _ =
54  failwith "AXIOM TO BE REALIZED"
55
56(** val set_to_list : 'a1 set0 -> 'a1 List.list **)
57let set_to_list _ =
58  failwith "AXIOM TO BE REALIZED"
59
60(** val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0 **)
61let set_insert = add
62
63(** val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0 **)
64let set_remove _ =
65  failwith "AXIOM TO BE REALIZED"
66
67(** val set_member :
68    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
69let set_member _ =
70  failwith "AXIOM TO BE REALIZED"
71
72(** val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
73let set_forall _ =
74  failwith "AXIOM TO BE REALIZED"
75
76(** val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool **)
77let set_exists _ =
78  failwith "AXIOM TO BE REALIZED"
79
80(** val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 **)
81let set_filter _ =
82  failwith "AXIOM TO BE REALIZED"
83
84(** val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0 **)
85let set_map _ =
86  failwith "AXIOM TO BE REALIZED"
87
88(** val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2 **)
89let set_fold _ =
90  failwith "AXIOM TO BE REALIZED"
91
92(** val set_equal :
93    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
94let set_equal _ =
95  failwith "AXIOM TO BE REALIZED"
96
97(** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
98let set_diff _ =
99  failwith "AXIOM TO BE REALIZED"
100
101(** val set_is_empty : 'a1 set0 -> Bool.bool **)
102let set_is_empty set1 =
103  Util.eq_nat (set_size set1) Nat.O
104
105(** val set_singleton : 'a1 -> 'a1 set0 **)
106let set_singleton elt =
107  set_insert elt set_empty
108
109(** val set_from_list : 'a1 List.list -> 'a1 set0 **)
110let set_from_list the_list =
111  List.foldr set_insert set_empty the_list
112
113(** val set_split :
114    ('a1 -> Bool.bool) -> 'a1 set0 -> ('a1 set0, 'a1 set0) Types.prod **)
115let set_split pred0 the_set =
116  let left = set_filter pred0 the_set in
117  let npred = fun x -> Bool.notb (pred0 x) in
118  let right = set_filter npred the_set in
119  { Types.fst = left; Types.snd = right }
120
121(** val set_subset :
122    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
123let set_subset eq left right =
124  set_forall (fun elt -> set_member eq elt right) left
125
126(** val set_subseteq :
127    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
128let set_subseteq eq left right =
129  Bool.andb (set_equal eq left right) (set_subset eq left right)
130
131(** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
132let set_union left right =
133  set_fold set_insert left right
134
135(** val set_intersection :
136    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
137let set_intersection eq left right =
138  set_filter (fun elt -> set_member eq elt right) left
Note: See TracBrowser for help on using the repository browser.