| author | wneuper <Walther.Neuper@jku.at> |
| Thu, 04 Aug 2022 12:48:37 +0200 | |
| changeset 60509 | 2e0b7ca391dc |
| parent 60507 | b125dcf14489 |
| child 60586 | 007ef64dbb08 |
| permissions | -rw-r--r-- |
| walther@59866 | 1 |
(* Title: BaseDefinitions/rewrite-order.sml |
| walther@59857 | 2 |
Author: Walther Neuper |
| walther@59857 | 3 |
(c) due to copyright terms |
| walther@59857 | 4 |
*) |
| walther@59857 | 5 |
signature REWRITE_ORDER = |
| walther@59857 | 6 |
sig |
| Walther@60509 | 7 |
type id = Rule_Def.rew_ord_id |
| Walther@60509 | 8 |
val id_empty: id |
| walther@59857 | 9 |
|
| Walther@60509 | 10 |
type function = Rule_Def.rew_ord_function |
| Walther@60509 | 11 |
val function_empty: function |
| walther@59857 | 12 |
|
| Walther@60509 | 13 |
type T = Rule_Def.rew_ord_T |
| Walther@60509 | 14 |
val empty: T |
| Walther@60509 | 15 |
|
| Walther@60509 | 16 |
val to_string: T -> string |
| Walther@60509 | 17 |
val equal: T * T -> bool |
| walther@59857 | 18 |
end |
| walther@59857 | 19 |
|
| walther@59857 | 20 |
(**) |
| walther@59857 | 21 |
structure Rewrite_Ord(**): REWRITE_ORDER(**) = |
| walther@59857 | 22 |
struct |
| walther@59857 | 23 |
(**) |
| walther@59857 | 24 |
|
| Walther@60509 | 25 |
type id = Rule_Def.rew_ord_id |
| Walther@60509 | 26 |
val id_empty = "Rewrite_Ord.id_empty"; |
| walther@59857 | 27 |
|
| Walther@60509 | 28 |
type function = Rule_Def.rew_ord_function; |
| Walther@60509 | 29 |
fun function_empty (_: LibraryC.subst) (_: term, _: term) = true; |
| Walther@60509 | 30 |
|
| Walther@60509 | 31 |
type T = Rule_Def.rew_ord_T |
| Walther@60509 | 32 |
val empty = (id_empty, function_empty) |
| Walther@60509 | 33 |
|
| Walther@60436 | 34 |
fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
|
| Walther@60506 | 35 |
fun equal ((id1, _), (id2, _)) = id1 = id2 |
| Walther@60506 | 36 |
|
| Walther@60506 | 37 |
end |