separate struct. UnparseC, shift code to ThmC
1 (* Title: CalcElements/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
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28 structure Rewrite_Ord(**): REWRITE_ORDER(**) =
32 val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
33 type rew_ord_ = Rule_Def.rew_ord_;
34 type subst = (term * term) list;
35 fun dummy_ord (_: subst) (_: term, _: term) = true;
36 val e_rew_ord_ = dummy_ord;
38 type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
39 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
40 val e_rew_ordX = (e_rew_ord', e_rew_ord_)
42 type rew_ord' = Rule_Def.rew_ord'
43 (* rewrite orders, also stored in 'type met' and type 'and rls'
44 The association list is required for 'rewrite.."rew_ord"..' *)
45 val rew_ord' = Unsynchronized.ref
46 ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
47 : (rew_ord' * (* the key for the association list *)
48 (subst (* the bound variables - they get high order*)
49 -> (term * term) (* (t1, t2) to be compared *)
50 -> bool)) (* if t1 <= t2 then true else false *)
51 list); (* association list *)
52 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
53 | assoc' ((keyi, xi) :: pairs, key) =
54 if key = keyi then SOME xi else assoc' (pairs, key);
55 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
56 handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");