2 Author: Walther Neuper |
2 Author: Walther Neuper |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 signature REWRITE_ORDER = |
5 signature REWRITE_ORDER = |
6 sig |
6 sig |
7 val e_rew_ord': Rule_Def.rew_ord'; |
7 type id = Rule_Def.rew_ord_id |
8 val dummy_ord: Rule_Def.rew_ord_ |
8 val id_empty: id |
9 val e_rew_ord: Rule_Def.rew_ord_ |
|
10 |
9 |
11 type rew_ord = Rule_Def.rew_ord |
10 type function = Rule_Def.rew_ord_function |
12 val e_rew_ordX: rew_ord |
11 val function_empty: function |
13 val to_string: rew_ord -> string |
|
14 |
12 |
15 type rew_ord' = Rule_Def.rew_ord' |
13 type T = Rule_Def.rew_ord_T |
16 val equal: rew_ord * rew_ord -> bool |
14 val empty: T |
|
15 |
|
16 val to_string: T -> string |
|
17 val equal: T * T -> bool |
17 end |
18 end |
18 |
19 |
19 (**) |
20 (**) |
20 structure Rewrite_Ord(**): REWRITE_ORDER(**) = |
21 structure Rewrite_Ord(**): REWRITE_ORDER(**) = |
21 struct |
22 struct |
22 (**) |
23 (**) |
23 |
24 |
24 val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord'; |
25 type id = Rule_Def.rew_ord_id |
25 type rew_ord_ = Rule_Def.rew_ord_; |
26 val id_empty = "Rewrite_Ord.id_empty"; |
26 fun dummy_ord (_: subst) (_: term, _: term) = true; |
|
27 val e_rew_ord_ = dummy_ord; |
|
28 |
27 |
29 type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord |
28 type function = Rule_Def.rew_ord_function; |
30 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*) |
29 fun function_empty (_: LibraryC.subst) (_: term, _: term) = true; |
31 val e_rew_ordX = (e_rew_ord', e_rew_ord_) |
30 |
|
31 type T = Rule_Def.rew_ord_T |
|
32 val empty = (id_empty, function_empty) |
|
33 |
32 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)" |
34 fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)" |
33 |
|
34 type rew_ord' = Rule_Def.rew_ord' |
|
35 fun equal ((id1, _), (id2, _)) = id1 = id2 |
35 fun equal ((id1, _), (id2, _)) = id1 = id2 |
36 |
36 |
37 end |
37 end |