equal
deleted
inserted
replaced
2 Author: Christian Urban |
2 Author: Christian Urban |
3 |
3 |
4 Basic functions for nominal. |
4 Basic functions for nominal. |
5 *) |
5 *) |
6 |
6 |
|
7 infix 1 ||>>> |>>> |
|
8 |
7 signature NOMINAL_BASIC = |
9 signature NOMINAL_BASIC = |
8 sig |
10 sig |
9 val trace: bool Unsynchronized.ref |
11 val trace: bool Unsynchronized.ref |
10 val trace_msg: (unit -> string) -> unit |
12 val trace_msg: (unit -> string) -> unit |
|
13 |
|
14 val |>>> : 'a * ('a -> 'b * 'c) -> 'b list * 'c |
|
15 val ||>>> : ('a list * 'b) * ('b -> 'a * 'b) -> 'a list * 'b |
11 |
16 |
12 val last2: 'a list -> 'a * 'a |
17 val last2: 'a list -> 'a * 'a |
13 val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list) |
18 val split_triples: ('a * 'b * 'c) list -> ('a list * 'b list * 'c list) |
14 val split_last2: 'a list -> 'a list * 'a * 'a |
19 val split_last2: 'a list -> 'a list * 'a * 'a |
15 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
20 val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list |
50 structure Nominal_Basic: NOMINAL_BASIC = |
55 structure Nominal_Basic: NOMINAL_BASIC = |
51 struct |
56 struct |
52 |
57 |
53 val trace = Unsynchronized.ref false |
58 val trace = Unsynchronized.ref false |
54 fun trace_msg msg = if ! trace then tracing (msg ()) else () |
59 fun trace_msg msg = if ! trace then tracing (msg ()) else () |
|
60 |
|
61 |
|
62 infix 1 ||>>> |>>> |
|
63 |
|
64 fun (x |>>> f) = |
|
65 let |
|
66 val (x', y') = f x |
|
67 in |
|
68 ([x'], y') |
|
69 end |
|
70 |
|
71 fun (([], y) ||>>> f) = ([], y) |
|
72 | ((xs, y) ||>>> f) = |
|
73 let |
|
74 val (x', y') = f y |
|
75 in |
|
76 (xs @ [x'], y') |
|
77 end |
55 |
78 |
56 |
79 |
57 (* orders an AList according to keys - every key needs to be there *) |
80 (* orders an AList according to keys - every key needs to be there *) |
58 fun order eq keys list = |
81 fun order eq keys list = |
59 map (the o AList.lookup eq list) keys |
82 map (the o AList.lookup eq list) keys |