walther@59866: (* Title:  BaseDefinitions/rewrite-order.sml
walther@59857:    Author: Walther Neuper
walther@59857:    (c) due to copyright terms
walther@59857: *)
walther@59857: signature REWRITE_ORDER =
walther@59857: sig
Walther@60509:   type id = Rule_Def.rew_ord_id
Walther@60509:   val id_empty: id
walther@59857: 
Walther@60509:   type function = Rule_Def.rew_ord_function
Walther@60509:   val function_empty: function
walther@59857: 
Walther@60509:   type T = Rule_Def.rew_ord_T
Walther@60509:   val empty: T
Walther@60509: 
Walther@60509:   val to_string: T -> string
Walther@60509:   val equal: T * T -> bool
walther@59857: end
walther@59857: 
walther@59857: (**)
walther@59857: structure Rewrite_Ord(**): REWRITE_ORDER(**) =
walther@59857: struct
walther@59857: (**)
walther@59857: 
Walther@60509: type id = Rule_Def.rew_ord_id
Walther@60509: val id_empty = "Rewrite_Ord.id_empty";
walther@59857: 
Walther@60509: type function = Rule_Def.rew_ord_function;
Walther@60509: fun function_empty (_: LibraryC.subst) (_: term, _: term) = true;
Walther@60509: 
Walther@60509: type T = Rule_Def.rew_ord_T
Walther@60509: val empty = (id_empty, function_empty)
Walther@60509: 
Walther@60436: fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"
Walther@60506: fun equal ((id1, _), (id2, _)) = id1 = id2
Walther@60506: 
Walther@60506: end