1 (* Title: BaseDefinitions/rewrite-order.sml
3 (c) due to copyright terms
5 TODO: use "Rewrite_Ord" for renaming identifiers.
7 signature REWRITE_ORDER =
10 val e_rew_ord': Rule_Def.rew_ord';
11 val dummy_ord: Rule_Def.rew_ord_
12 val e_rew_ord: Rule_Def.rew_ord_
14 type rew_ord = Rule_Def.rew_ord
15 val e_rew_ordX: rew_ord
17 type rew_ord' = Rule_Def.rew_ord'
18 val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
19 val assoc_rew_ord: string -> subst -> term * term -> bool
23 structure Rewrite_Ord(**): REWRITE_ORDER(**) =
27 val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
28 type rew_ord_ = Rule_Def.rew_ord_;
29 type subst = (term * term) list;
30 fun dummy_ord (_: subst) (_: term, _: term) = true;
31 val e_rew_ord_ = dummy_ord;
33 type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
34 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
35 val e_rew_ordX = (e_rew_ord', e_rew_ord_)
37 type rew_ord' = Rule_Def.rew_ord'
38 (* rewrite orders, also stored in 'type met' and type 'and rls'
39 The association list is required for 'rewrite.."rew_ord"..' *)
40 val rew_ord' = Unsynchronized.ref
41 ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
42 : (rew_ord' * (* the key for the association list *)
43 (subst (* the bound variables - they get high order*)
44 -> (term * term) (* (t1, t2) to be compared *)
45 -> bool)) (* if t1 <= t2 then true else false *)
46 list); (* association list *)
47 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
48 | assoc' ((keyi, xi) :: pairs, key) =
49 if key = keyi then SOME xi else assoc' (pairs, key);
50 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord', ro))
51 handle ERROR _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");