Changeset 2738 for extracted/untrusted/set_adt.ml
 Timestamp:
 Feb 27, 2013, 2:03:12 PM (7 years ago)
 Location:
 extracted/untrusted
 Files:

 1 added
 1 copied
Legend:
 Unmodified
 Added
 Removed

extracted/untrusted/set_adt.ml
r2735 r2738 1 (* Copied from OCaml's set.ml *) 1 type 'x set = 'x Pset.set 2 2 3 type 'a set = Empty  Node of 'a set * 'a * 'a set * int 4 5 let height = function 6 Empty > 0 7  Node(_, _, _, h) > h 8 9 let create l v r = 10 let hl = match l with Empty > 0  Node(_,_,_,h) > h in 11 let hr = match r with Empty > 0  Node(_,_,_,h) > h in 12 Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1)) 13 14 let bal l v r = 15 let hl = match l with Empty > 0  Node(_,_,_,h) > h in 16 let hr = match r with Empty > 0  Node(_,_,_,h) > h in 17 if hl > hr + 2 then begin 18 match l with 19 Empty > invalid_arg "Set.bal" 20  Node(ll, lv, lr, _) > 21 if height ll >= height lr then 22 create ll lv (create lr v r) 23 else begin 24 match lr with 25 Empty > invalid_arg "Set.bal" 26  Node(lrl, lrv, lrr, _)> 27 create (create ll lv lrl) lrv (create lrr v r) 28 end 29 end else if hr > hl + 2 then begin 30 match r with 31 Empty > invalid_arg "Set.bal" 32  Node(rl, rv, rr, _) > 33 if height rr >= height rl then 34 create (create l v rl) rv rr 35 else begin 36 match rl with 37 Empty > invalid_arg "Set.bal" 38  Node(rll, rlv, rlr, _) > 39 create (create l v rll) rlv (create rlr rv rr) 40 end 41 end else 42 Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1)) 43 44 let rec add x = function 45 Empty > Node(Empty, x, Empty, 1) 46  Node(l, v, r, _) as t > 47 let c = compare x v in 48 if c = 0 then t else 49 if c < 0 then bal (add x l) v r else bal l v (add x r) 50 51 let rec min_elt = function 52 Empty > raise Not_found 53  Node(Empty, v, r, _) > v 54  Node(l, v, r, _) > min_elt l 55 56 let rec remove_min_elt = function 57 Empty > invalid_arg "Set.remove_min_elt" 58  Node(Empty, v, r, _) > r 59  Node(l, v, r, _) > bal (remove_min_elt l) v r 60 61 let merge t1 t2 = 62 match (t1, t2) with 63 (Empty, t) > t 64  (t, Empty) > t 65  (_, _) > bal t1 (min_elt t2) (remove_min_elt t2) 66 67 let rec join l v r = 68 match (l, r) with 69 (Empty, _) > add v r 70  (_, Empty) > add v l 71  (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) > 72 if lh > rh + 2 then bal ll lv (join lr v r) else 73 if rh > lh + 2 then bal (join l v rl) rv rr else 74 create l v r 75 76 let rec split x = function 77 Empty > 78 (Empty, false, Empty) 79  Node(l, v, r, _) > 80 let c = compare x v in 81 if c = 0 then (l, true, r) 82 else if c < 0 then 83 let (ll, pres, rl) = split x l in (ll, pres, join rl v r) 84 else 85 let (lr, pres, rr) = split x r in (join l v lr, pres, rr) 86 87 let rec union s1 s2 = 88 match (s1, s2) with 89 (Empty, t2) > t2 90  (t1, Empty) > t1 91  (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) > 92 if h1 >= h2 then 93 if h2 = 1 then add v2 s1 else begin 94 let (l2, _, r2) = split v1 s2 in 95 join (union l1 l2) v1 (union r1 r2) 96 end 97 else 98 if h1 = 1 then add v1 s2 else begin 99 let (l1, _, r1) = split v2 s1 in 100 join (union l1 l2) v2 (union r1 r2) 101 end 102 103 let concat t1 t2 = 104 match (t1, t2) with 105 (Empty, t) > t 106  (t, Empty) > t 107  (_, _) > join t1 (min_elt t2) (remove_min_elt t2) 108 109 let rec mem x = function 110 Empty > false 111  Node(l, v, r, _) > 112 let c = compare x v in 113 c = 0  mem x (if c < 0 then l else r) 114 115 let rec for_all p = function 116 Empty > true 117  Node(l, v, r, _) > p v && for_all p l && for_all p r 118 119 let rec exists p = function 120 Empty > false 121  Node(l, v, r, _) > p v  exists p l  exists p r 122 123 let rec subset s1 s2 = 124 match (s1, s2) with 125 Empty, _ > 126 true 127  _, Empty > 128 false 129  Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) > 130 let c = compare v1 v2 in 131 if c = 0 then 132 subset l1 l2 && subset r1 r2 133 else if c < 0 then 134 subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 135 else 136 subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2 137 138 let rec diff s1 s2 = 139 match (s1, s2) with 140 (Empty, t2) > Empty 141  (t1, Empty) > t1 142  (Node(l1, v1, r1, _), t2) > 143 match split v1 t2 with 144 (l2, false, r2) > 145 join (diff l1 l2) v1 (diff r1 r2) 146  (l2, true, r2) > 147 concat (diff l1 l2) (diff r1 r2) 148 149 type 'a enumeration = End  More of 'a * 'a set * 'a enumeration 150 151 let rec cons_enum s e = 152 match s with 153 Empty > e 154  Node(l, v, r, _) > cons_enum l (More(v, r, e)) 155 156 let rec compare_aux e1 e2 = 157 match (e1, e2) with 158 (End, End) > 0 159  (End, _) > 1 160  (_, End) > 1 161  (More(v1, r1, e1), More(v2, r2, e2)) > 162 let c = compare v1 v2 in 163 if c <> 0 164 then c 165 else compare_aux (cons_enum r1 e1) (cons_enum r2 e2) 166 167 let compare s1 s2 = 168 compare_aux (cons_enum s1 End) (cons_enum s2 End) 169 170 let equal s1 s2 = 171 compare s1 s2 = 0 172 173 let matitabool_of_bool b = if b then Bool.True else Bool.False 3 let matitabool_of_bool b = if b then Bool.True else Bool.False 174 4 175 5 (** val set_empty : 'a1 set0 **) 176 let set_empty = Empty6 let set_empty = Pset.empty 177 7 178 8 (** val set_member : 179 9 ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set0 > Bool.bool **) 180 let set_member _ x s = matitabool_of_bool ( mem x s)10 let set_member _ x s = matitabool_of_bool (Pset.mem x s) 181 11 182 12 (** val set_equal : 183 13 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **) 184 let set_equal _ s1 s2 = matitabool_of_bool ( equal s1 s2)14 let set_equal _ s1 s2 = matitabool_of_bool (Pset.equal s1 s2) 185 15 186 16 (** val set_diff : 'a1 set0 > 'a1 set0 > 'a1 set0 **) 187 let set_diff = diff17 let set_diff = Pset.diff 188 18 189 19 (** val set_singleton : 'a1 > 'a1 set0 **) 190 let set_singleton elt = 191 add elt set_empty 20 let set_singleton = Pset.singleton 192 21 193 22 (** val set_from_list : 'a1 List.list > 'a1 set0 **) 194 23 let set_from_list the_list = 195 List.foldr add set_empty the_list24 List.foldr Pset.add set_empty the_list 196 25 197 26 (** val set_subset : 198 27 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **) 199 let set_subset _ s1 s2 = matitabool_of_bool ( subset s1 s2)28 let set_subset _ s1 s2 = matitabool_of_bool (Pset.subset s1 s2) 200 29 201 30 (** val set_union : 'a1 set0 > 'a1 set0 > 'a1 set0 **) 202 let set_union = union31 let set_union = Pset.union
Note: See TracChangeset
for help on using the changeset viewer.