Ignore:
Timestamp:
Feb 27, 2013, 2:03:12 PM (7 years ago)
Author:
sacerdot
Message:

Porting the graph colouring stuff from the untrusted prototype to the extracted
code.

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 *)
     1type 'x set = 'x Pset.set
    22
    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
     3let matitabool_of_bool b = if b then Bool.True else Bool.False
    1744
    1755(** val set_empty : 'a1 set0 **)
    176 let set_empty = Empty
     6let set_empty = Pset.empty
    1777
    1788(** val set_member :
    1799    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
    180 let set_member _ x s = matitabool_of_bool (mem x s)
     10let set_member _ x s = matitabool_of_bool (Pset.mem x s)
    18111
    18212(** val set_equal :
    18313    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    184 let set_equal _ s1 s2 = matitabool_of_bool (equal s1 s2)
     14let set_equal _ s1 s2 = matitabool_of_bool (Pset.equal s1 s2)
    18515
    18616(** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    187 let set_diff = diff
     17let set_diff = Pset.diff
    18818
    18919(** val set_singleton : 'a1 -> 'a1 set0 **)
    190 let set_singleton elt =
    191   add elt set_empty
     20let set_singleton = Pset.singleton
    19221
    19322(** val set_from_list : 'a1 List.list -> 'a1 set0 **)
    19423let set_from_list the_list =
    195   List.foldr add set_empty the_list
     24  List.foldr Pset.add set_empty the_list
    19625
    19726(** val set_subset :
    19827    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    199 let set_subset _ s1 s2 = matitabool_of_bool (subset s1 s2)
     28let set_subset _ s1 s2 = matitabool_of_bool (Pset.subset s1 s2)
    20029
    20130(** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    202 let set_union = union
     31let set_union = Pset.union
Note: See TracChangeset for help on using the changeset viewer.