Changeset 2733 for extracted/set_adt.ml
 Timestamp:
 Feb 25, 2013, 11:04:57 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/set_adt.ml
r2731 r2733 1 (* Copied from OCaml's set.ml *) 2 1 3 type 'a set = Empty  Node of 'a set * 'a * 'a set * int 2 4 … … 47 49 if c < 0 then bal (add x l) v r else bal l v (add x r) 48 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 174 49 175 (** val set_empty : 'a1 set0 **) 50 176 let set_empty = Empty 51 177 52 (** val set_size : 'a1 set0 > Nat.nat **)53 let set_size _ =54 failwith "AXIOM TO BE REALIZED"55 56 (** val set_to_list : 'a1 set0 > 'a1 List.list **)57 let set_to_list _ =58 failwith "AXIOM TO BE REALIZED"59 60 (** val set_insert : 'a1 > 'a1 set0 > 'a1 set0 **)61 let set_insert = add62 63 (** val set_remove : 'a1 > 'a1 set0 > 'a1 set0 **)64 let set_remove _ =65 failwith "AXIOM TO BE REALIZED"66 67 178 (** val set_member : 68 179 ('a1 > 'a1 > Bool.bool) > 'a1 > 'a1 set0 > Bool.bool **) 69 let set_member _ = 70 failwith "AXIOM TO BE REALIZED" 71 72 (** val set_forall : ('a1 > Bool.bool) > 'a1 set0 > Bool.bool **) 73 let set_forall _ = 74 failwith "AXIOM TO BE REALIZED" 75 76 (** val set_exists : ('a1 > Bool.bool) > 'a1 set0 > Bool.bool **) 77 let set_exists _ = 78 failwith "AXIOM TO BE REALIZED" 79 80 (** val set_filter : ('a1 > Bool.bool) > 'a1 set0 > 'a1 set0 **) 81 let set_filter _ = 82 failwith "AXIOM TO BE REALIZED" 83 84 (** val set_map : ('a1 > 'a2) > 'a1 set0 > 'a2 set0 **) 85 let set_map _ = 86 failwith "AXIOM TO BE REALIZED" 87 88 (** val set_fold : ('a1 > 'a2 > 'a2) > 'a1 set0 > 'a2 > 'a2 **) 89 let set_fold _ = 90 failwith "AXIOM TO BE REALIZED" 180 let set_member _ x s = matitabool_of_bool (mem x s) 91 181 92 182 (** val set_equal : 93 183 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **) 94 let set_equal _ = 95 failwith "AXIOM TO BE REALIZED" 184 let set_equal _ s1 s2 = matitabool_of_bool (equal s1 s2) 96 185 97 186 (** val set_diff : 'a1 set0 > 'a1 set0 > 'a1 set0 **) 98 let set_diff _ = 99 failwith "AXIOM TO BE REALIZED" 100 101 (** val set_is_empty : 'a1 set0 > Bool.bool **) 102 let set_is_empty set1 = 103 Util.eq_nat (set_size set1) Nat.O 187 let set_diff = diff 104 188 105 189 (** val set_singleton : 'a1 > 'a1 set0 **) 106 190 let set_singleton elt = 107 set_insertelt set_empty191 add elt set_empty 108 192 109 193 (** val set_from_list : 'a1 List.list > 'a1 set0 **) 110 194 let 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 **) 115 let 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 } 195 List.foldr add set_empty the_list 120 196 121 197 (** val set_subset : 122 198 ('a1 > 'a1 > Bool.bool) > 'a1 set0 > 'a1 set0 > Bool.bool **) 123 let 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 **) 128 let set_subseteq eq left right = 129 Bool.andb (set_equal eq left right) (set_subset eq left right) 199 let set_subset _ s1 s2 = matitabool_of_bool (subset s1 s2) 130 200 131 201 (** val set_union : 'a1 set0 > 'a1 set0 > 'a1 set0 **) 132 let 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 **) 137 let set_intersection eq left right = 138 set_filter (fun elt > set_member eq elt right) left 202 let set_union = union
Note: See TracChangeset
for help on using the changeset viewer.