author | wneuper <Walther.Neuper@jku.at> |
Wed, 03 Aug 2022 18:06:02 +0200 | |
changeset 60507 | b125dcf14489 |
parent 60506 | 145e45cd7a0f |
child 60509 | 2e0b7ca391dc |
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@59857 | 7 |
val e_rew_ord': Rule_Def.rew_ord'; |
walther@59857 | 8 |
val dummy_ord: Rule_Def.rew_ord_ |
walther@59857 | 9 |
val e_rew_ord: Rule_Def.rew_ord_ |
walther@59857 | 10 |
|
walther@59857 | 11 |
type rew_ord = Rule_Def.rew_ord |
walther@59857 | 12 |
val e_rew_ordX: rew_ord |
Walther@60436 | 13 |
val to_string: rew_ord -> string |
walther@59857 | 14 |
|
walther@59857 | 15 |
type rew_ord' = Rule_Def.rew_ord' |
Walther@60506 | 16 |
val equal: rew_ord * rew_ord -> bool |
walther@59857 | 17 |
end |
walther@59857 | 18 |
|
walther@59857 | 19 |
(**) |
walther@59857 | 20 |
structure Rewrite_Ord(**): REWRITE_ORDER(**) = |
walther@59857 | 21 |
struct |
walther@59857 | 22 |
(**) |
walther@59857 | 23 |
|
walther@59857 | 24 |
val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord'; |
walther@59857 | 25 |
type rew_ord_ = Rule_Def.rew_ord_; |
walther@59857 | 26 |
fun dummy_ord (_: subst) (_: term, _: term) = true; |
walther@59857 | 27 |
val e_rew_ord_ = dummy_ord; |
walther@59857 | 28 |
|
walther@59857 | 29 |
type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord |
walther@59857 | 30 |
val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*) |
walther@59857 | 31 |
val e_rew_ordX = (e_rew_ord', e_rew_ord_) |
Walther@60436 | 32 |
fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)" |
walther@59857 | 33 |
|
walther@59857 | 34 |
type rew_ord' = Rule_Def.rew_ord' |
Walther@60506 | 35 |
fun equal ((id1, _), (id2, _)) = id1 = id2 |
Walther@60506 | 36 |
|
Walther@60506 | 37 |
end |