Changeset 2738


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
Files:
21 added
2 edited
2 copied
6 moved

Legend:

Unmodified
Added
Removed
  • extracted/build

    r2731 r2738  
    22
    33# Uses a GNU sed extension
    4 ls *.ml | sed -e 's/\(.\)\(.*\)\.ml/\U\1\E\2/' > extracted.mlpack
    5 ocamlbuild -cflag -g extracted.cmo
     4for i in `ls *.ml untrusted/*.ml`; do basename $i | sed -e 's/\(.\)\(.*\)\.ml/\U\1\E\2/'; done > extracted.mlpack
     5ocamlbuild -Is untrusted -cflag -g extracted.cmo
  • extracted/compiler.ml

    r2736 r2738  
    274274
    275275(** val colour_graph : Interference.coloured_graph_computer **)
    276 let colour_graph _ =
    277   failwith "AXIOM TO BE REALIZED"
     276let colour_graph = Compute_colouring.colour_graph
    278277
    279278(** val back_end :
  • extracted/untrusted/Fix.ml

    r2736 r2738  
    1212(**************************************************************************)
    1313
    14 module MyList = struct
    15 let rec rev_append l1 l2 =
    16   match l1 with
    17     [] -> l2
    18   | a :: l -> rev_append l (a :: l2)
    19 
    20 let rev l = rev_append l []
    21 
    22 let find_all p =
    23   let rec find accu = function
    24   | [] -> rev accu
    25   | x :: l -> if p x then find (x :: accu) l else find accu l in
    26   find []
    27 
    28 let filter = find_all
    29 
    30 let rec map f = function
    31     [] -> []
    32   | a::l -> let r = f a in r :: map f l
    33 
    34 let rec iter f = function
    35     [] -> ()
    36   | a::l -> f a; iter f l
    37 end
    38 
    3914(* -------------------------------------------------------------------------- *)
    4015
     
    203178
    204179  let predecessors (node : 'data node) : 'data node list =
    205     let predecessors = MyList.filter (fun edge -> not edge.destroyed) node.incoming in
     180    let predecessors = OcamlList.filter (fun edge -> not edge.destroyed) node.incoming in
    206181    node.incoming <- predecessors;
    207     MyList.map (follow node) predecessors
     182    OcamlList.map (follow node) predecessors
    208183
    209184  (* [link src dst] creates a new edge from [src] to [dst], together
     
    237212
    238213  let clear_successors (node : 'data node) : unit =
    239     MyList.iter (fun edge ->
     214    OcamlList.iter (fun edge ->
    240215      assert (not edge.destroyed);
    241216      edge.destroyed <- true;
     
    362337
    363338let signal subject =
    364   MyList.iter (fun observer ->
     339  OcamlList.iter (fun observer ->
    365340    Graph.clear_successors observer;
    366341    Workset.insert observer
  • extracted/untrusted/pset.ml

    r2735 r2738  
    22
    33    type 'a set = Empty | Node of 'a set * 'a * 'a set * int
     4
     5    let empty = Empty
     6
     7    let is_empty = function Empty -> true | Node _ -> false
    48
    59    let height = function
     
    4953         if c < 0 then bal (add x l) v r else bal l v (add x r)
    5054
     55    let singleton elt = add elt Empty
     56
    5157    let rec min_elt = function
    5258        Empty -> raise Not_found
     
    6470      | (t, Empty) -> t
    6571      | (_, _) -> bal t1 (min_elt t2) (remove_min_elt t2)
     72
     73    let rec remove x = function
     74        Empty -> Empty
     75      | Node(l, v, r, _) ->
     76          let c = compare x v in
     77          if c = 0 then merge l r else
     78          if c < 0 then bal (remove x l) v r else bal l v (remove x r)
     79
     80    let rec fold f s accu =
     81      match s with
     82        Empty -> accu
     83      | Node(l, v, r, _) -> fold f r (f v (fold f l accu))
     84
     85    let rec iter f = function
     86        Empty -> ()
     87      | Node(l, v, r, _) -> iter f l; f v; iter f r
     88
     89    let rec cardinal = function
     90        Empty -> 0
     91      | Node(l, v, r, _) -> cardinal l + 1 + cardinal r
    6692
    6793    let rec join l v r =
     
    170196    let equal s1 s2 =
    171197      compare s1 s2 = 0
    172 
    173     let matitabool_of_bool b = if b then Bool.True else Bool.False
    174 
    175 (** val set_empty : 'a1 set0 **)
    176 let set_empty = Empty
    177 
    178 (** val set_member :
    179     ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
    180 let set_member _ x s = matitabool_of_bool (mem x s)
    181 
    182 (** val set_equal :
    183     ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    184 let set_equal _ s1 s2 = matitabool_of_bool (equal s1 s2)
    185 
    186 (** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    187 let set_diff = diff
    188 
    189 (** val set_singleton : 'a1 -> 'a1 set0 **)
    190 let set_singleton elt =
    191   add elt set_empty
    192 
    193 (** val set_from_list : 'a1 List.list -> 'a1 set0 **)
    194 let set_from_list the_list =
    195   List.foldr add set_empty the_list
    196 
    197 (** val set_subset :
    198     ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
    199 let set_subset _ s1 s2 = matitabool_of_bool (subset s1 s2)
    200 
    201 (** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
    202 let set_union = union
  • extracted/untrusted/pset.mli

    r2735 r2738  
    11type 'x set
    22
    3 val set_empty : 'a1 set
     3val empty : 'a1 set
    44
    5 val set_member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set -> Bool.bool
     5val is_empty: 'a1 set -> bool
    66
    7 val set_equal :
    8   ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool
     7val mem : 'a1 -> 'a1 set -> bool
    98
    10 val set_diff : 'a1 set -> 'a1 set -> 'a1 set
     9val add : 'a1 -> 'a1 set -> 'a1 set
    1110
    12 val set_singleton : 'a1 -> 'a1 set
     11val remove: 'a1 -> 'a1 set -> 'a1 set
    1312
    14 val set_from_list : 'a1 List.list -> 'a1 set
     13val cardinal: 'a1 set -> int
    1514
    16 val set_subset :
    17   ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool
     15val fold: ('a1 -> 'a -> 'a) -> 'a1 set -> 'a -> 'a
    1816
    19 val set_union : 'a1 set -> 'a1 set -> 'a1 set
     17val iter: ('a1 -> unit) -> 'a1 set -> unit
     18
     19val equal : 'a1 set -> 'a1 set -> bool
     20
     21val diff : 'a1 set -> 'a1 set -> 'a1 set
     22
     23val singleton : 'a1 -> 'a1 set
     24
     25val subset : 'a1 set -> 'a1 set -> bool
     26
     27val union : 'a1 set -> 'a1 set -> 'a1 set
  • 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.