(* Title:  BaseDefinitions/rewrite-order.sml

   Author: Walther Neuper

   (c) due to copyright terms

*)

signature REWRITE_ORDER =

sig

  val e_rew_ord': Rule_Def.rew_ord';

  val dummy_ord: Rule_Def.rew_ord_

  val e_rew_ord: Rule_Def.rew_ord_

  type rew_ord = Rule_Def.rew_ord

  val e_rew_ordX: rew_ord

  val to_string: rew_ord -> string

  type rew_ord' = Rule_Def.rew_ord'

  val equal: rew_ord * rew_ord -> bool

end

(**)

structure Rewrite_Ord(**): REWRITE_ORDER(**) =

struct

(**)

val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';

type rew_ord_ = Rule_Def.rew_ord_;

fun dummy_ord (_: subst) (_: term, _: term) = true;

val e_rew_ord_ = dummy_ord;

type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord

val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)

val e_rew_ordX = (e_rew_ord', e_rew_ord_)

fun to_string (rew_ord', _) = "(" ^ rew_ord' ^ ", _: fn)"

type rew_ord' = Rule_Def.rew_ord'

(* rewrite orders, also stored in 'type met' and type 'and rls'

  The association list is required for 'rewrite.."rew_ord"..' *)

val rew_ord' = Unsynchronized.ref

  ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]

	: (rew_ord' *    (* the key for the association list         *)

	    (subst 	    (* the bound variables - they get high order*)

	     -> (term * term) (* (t1, t2) to be compared                  *)

	     -> bool))        (* if t1 <= t2 then true else false         *)

		list);              (* association list                         *)

fun equal ((id1, _), (id2, _)) = id1 = id2

end