walther@59866
|
1 |
(* Title: BaseDefinitions/rewrite-order.sml
|
walther@59857
|
2 |
Author: Walther Neuper
|
walther@59857
|
3 |
(c) due to copyright terms
|
walther@59857
|
4 |
|
walther@59857
|
5 |
TODO: use "Rewrite_Ord" for renaming identifiers.
|
walther@59857
|
6 |
*)
|
walther@59857
|
7 |
signature REWRITE_ORDER =
|
walther@59857
|
8 |
sig
|
walther@59857
|
9 |
type subst
|
walther@59857
|
10 |
val e_rew_ord': Rule_Def.rew_ord';
|
walther@59857
|
11 |
val dummy_ord: Rule_Def.rew_ord_
|
walther@59857
|
12 |
val e_rew_ord: Rule_Def.rew_ord_
|
walther@59857
|
13 |
|
walther@59857
|
14 |
type rew_ord = Rule_Def.rew_ord
|
walther@59857
|
15 |
val e_rew_ordX: rew_ord
|
walther@59857
|
16 |
|
walther@59857
|
17 |
type rew_ord' = Rule_Def.rew_ord'
|
walther@59857
|
18 |
val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
|
walther@59857
|
19 |
val assoc_rew_ord: string -> subst -> term * term -> bool
|
walther@59861
|
20 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59861
|
21 |
(*NONE*)
|
walther@59861
|
22 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59861
|
23 |
(*NONE*)
|
walther@59861
|
24 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59857
|
25 |
end
|
walther@59857
|
26 |
|
walther@59857
|
27 |
(**)
|
walther@59857
|
28 |
structure Rewrite_Ord(**): REWRITE_ORDER(**) =
|
walther@59857
|
29 |
struct
|
walther@59857
|
30 |
(**)
|
walther@59857
|
31 |
|
walther@59857
|
32 |
val e_rew_ord' = "e_rew_ord" : Rule_Def.rew_ord';
|
walther@59857
|
33 |
type rew_ord_ = Rule_Def.rew_ord_;
|
walther@59857
|
34 |
type subst = (term * term) list;
|
walther@59857
|
35 |
fun dummy_ord (_: subst) (_: term, _: term) = true;
|
walther@59857
|
36 |
val e_rew_ord_ = dummy_ord;
|
walther@59857
|
37 |
|
walther@59857
|
38 |
type rew_ord = (*rew_ord' * rew_ord_;*) Rule_Def.rew_ord
|
walther@59857
|
39 |
val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
|
walther@59857
|
40 |
val e_rew_ordX = (e_rew_ord', e_rew_ord_)
|
walther@59857
|
41 |
|
walther@59857
|
42 |
type rew_ord' = Rule_Def.rew_ord'
|
walther@59857
|
43 |
(* rewrite orders, also stored in 'type met' and type 'and rls'
|
walther@59857
|
44 |
The association list is required for 'rewrite.."rew_ord"..' *)
|
walther@59857
|
45 |
val rew_ord' = Unsynchronized.ref
|
walther@59857
|
46 |
([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
|
walther@59857
|
47 |
: (rew_ord' * (* the key for the association list *)
|
walther@59857
|
48 |
(subst (* the bound variables - they get high order*)
|
walther@59857
|
49 |
-> (term * term) (* (t1, t2) to be compared *)
|
walther@59857
|
50 |
-> bool)) (* if t1 <= t2 then true else false *)
|
walther@59857
|
51 |
list); (* association list *)
|
walther@59857
|
52 |
fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
|
walther@59857
|
53 |
| assoc' ((keyi, xi) :: pairs, key) =
|
walther@59857
|
54 |
if key = keyi then SOME xi else assoc' (pairs, key);
|
walther@59857
|
55 |
fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
|
walther@59857
|
56 |
handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
|
walther@59857
|
57 |
|
walther@59857
|
58 |
end |