equal
deleted
inserted
replaced
8 sig |
8 sig |
9 val trace: bool Unsynchronized.ref |
9 val trace: bool Unsynchronized.ref |
10 val trace_msg: (unit -> string) -> unit |
10 val trace_msg: (unit -> string) -> unit |
11 |
11 |
12 val last2: 'a list -> 'a * 'a |
12 val last2: 'a list -> 'a * 'a |
|
13 val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list) |
13 val split_last2: 'a list -> 'a list * 'a * 'a |
14 val split_last2: 'a list -> 'a list * 'a * 'a |
14 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
15 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
15 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
16 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
16 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
17 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
17 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
18 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
65 fun remove_dups eq [] = [] |
66 fun remove_dups eq [] = [] |
66 | remove_dups eq (x :: xs) = |
67 | remove_dups eq (x :: xs) = |
67 if member eq xs x |
68 if member eq xs x |
68 then remove_dups eq xs |
69 then remove_dups eq xs |
69 else x :: remove_dups eq xs |
70 else x :: remove_dups eq xs |
|
71 |
|
72 fun split_triples xs = |
|
73 fold (fn (a, b, c) => fn (axs, bxs, cxs) => (a :: axs, b :: bxs, c :: cxs)) xs ([], [], []) |
70 |
74 |
71 fun last2 [] = raise Empty |
75 fun last2 [] = raise Empty |
72 | last2 [_] = raise Empty |
76 | last2 [_] = raise Empty |
73 | last2 [x, y] = (x, y) |
77 | last2 [x, y] = (x, y) |
74 | last2 (_ :: xs) = last2 xs |
78 | last2 (_ :: xs) = last2 xs |