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