equal
deleted
inserted
replaced
4 Basic functions for nominal. |
4 Basic functions for nominal. |
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
|
9 val trace: bool Unsynchronized.ref |
|
10 val trace_msg: (unit -> string) -> unit |
|
11 |
9 val last2: 'a list -> 'a * 'a |
12 val last2: 'a list -> 'a * 'a |
10 val split_last2: 'a list -> 'a list * 'a * 'a |
13 val split_last2: 'a list -> 'a list * 'a * 'a |
11 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
14 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
12 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
15 val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list |
13 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
16 val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list |
138 end |
141 end |
139 |
142 |
140 |
143 |
141 structure Nominal_Library: NOMINAL_LIBRARY = |
144 structure Nominal_Library: NOMINAL_LIBRARY = |
142 struct |
145 struct |
|
146 |
|
147 val trace = Unsynchronized.ref false |
|
148 fun trace_msg msg = if ! trace then tracing (msg ()) else () |
|
149 |
143 |
150 |
144 (* orders an AList according to keys - every key needs to be there *) |
151 (* orders an AList according to keys - every key needs to be there *) |
145 fun order eq keys list = |
152 fun order eq keys list = |
146 map (the o AList.lookup eq list) keys |
153 map (the o AList.lookup eq list) keys |
147 |
154 |