walther@59857: (* Title:  CalcElements/rewrite-order.sml
walther@59857:    Author: Walther Neuper
walther@59857:    (c) due to copyright terms
walther@59857: 
walther@59857: TODO: use "Rewrite_Ord" for renaming identifiers.
walther@59857: *)
walther@59857: signature REWRITE_ORDER =
walther@59857: sig
walther@59857:   type subst
walther@59857:   val e_rew_ord': Rule_Def.rew_ord';
walther@59857:   val dummy_ord: Rule_Def.rew_ord_
walther@59857:   val e_rew_ord: Rule_Def.rew_ord_
walther@59857: 
walther@59857:   type rew_ord = Rule_Def.rew_ord
walther@59857:   val e_rew_ordX: rew_ord
walther@59857: 
walther@59857:   type rew_ord' = Rule_Def.rew_ord'
walther@59857:   val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
walther@59857:   val assoc_rew_ord: string -> subst -> term * term -> bool
walther@59857: end
walther@59857: 
walther@59857: (**)
walther@59857: structure Rewrite_Ord(**): REWRITE_ORDER(**) =
walther@59857: struct
walther@59857: (**)
walther@59857: 
walther@59857: val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
walther@59857: type rew_ord_ = Rule_Def.rew_ord_;
walther@59857: type subst = (term * term) list;
walther@59857: fun dummy_ord (_: subst) (_: term, _: term) = true;
walther@59857: val e_rew_ord_ = dummy_ord;
walther@59857: 
walther@59857: type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
walther@59857: val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
walther@59857: val e_rew_ordX = (e_rew_ord', e_rew_ord_)
walther@59857: 
walther@59857: type rew_ord' = Rule_Def.rew_ord'
walther@59857: (* rewrite orders, also stored in 'type met' and type 'and rls'
walther@59857:   The association list is required for 'rewrite.."rew_ord"..' *)
walther@59857: val rew_ord' = Unsynchronized.ref
walther@59857:   ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
walther@59857: 	: (rew_ord' *    (* the key for the association list         *)
walther@59857: 	    (subst 	    (* the bound variables - they get high order*)
walther@59857: 	     -> (term * term) (* (t1, t2) to be compared                  *)
walther@59857: 	     -> bool))        (* if t1 <= t2 then true else false         *)
walther@59857: 		list);              (* association list                         *)
walther@59857: fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
walther@59857:   | assoc' ((keyi, xi) :: pairs, key) =
walther@59857:     if key = keyi then SOME xi else assoc' (pairs, key);
walther@59857: fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
walther@59857:   handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
walther@59857: 
walther@59857: end