walther@59866
|
1 |
(* Title: BaseDefinitions/rule-set.sml
|
walther@59850
|
2 |
Author: Walther Neuper
|
walther@59850
|
3 |
(c) due to copyright terms
|
walther@59850
|
4 |
|
walther@59887
|
5 |
In ISAC a Rule_Set serves rewriting. Know_Store holds all rule-sets for ubiquitous access.
|
walther@59850
|
6 |
*)
|
walther@59850
|
7 |
signature RULE_SET =
|
walther@59850
|
8 |
sig
|
walther@59851
|
9 |
datatype T = datatype Rule_Def.rule_set
|
walther@59867
|
10 |
eqtype id
|
walther@59850
|
11 |
|
walther@59867
|
12 |
val id: T -> string
|
walther@59852
|
13 |
val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
|
walther@59857
|
14 |
preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
|
walther@59852
|
15 |
|
walther@59852
|
16 |
val append_rules: string -> T -> Rule_Def.rule list -> T
|
walther@59852
|
17 |
val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
|
walther@59852
|
18 |
val merge: string -> T -> T -> T
|
walther@59852
|
19 |
val get_rules: T -> Rule_Def.rule list
|
walther@59914
|
20 |
(*val rule2rls': Rule.rule -> string*)
|
walther@59914
|
21 |
val id_from_rule: Rule.rule -> string
|
walther@59914
|
22 |
val contains: Rule.rule -> T -> bool
|
walther@59852
|
23 |
|
walther@59852
|
24 |
type for_kestore
|
walther@59852
|
25 |
val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
|
walther@59852
|
26 |
val to_kestore: for_kestore list * for_kestore list -> for_kestore list
|
walther@59852
|
27 |
|
walther@59869
|
28 |
(*/------- this will disappear eventually ----------------------------------------------------\*)
|
walther@59852
|
29 |
val empty: T
|
walther@59850
|
30 |
type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
|
walther@59850
|
31 |
val e_rrlsstate: rrlsstate
|
walther@59851
|
32 |
val e_rrls: T
|
walther@59869
|
33 |
(*\------- this will disappear eventually ----------------------------------------------------/*)
|
walther@59850
|
34 |
|
walther@59850
|
35 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
walther@59850
|
36 |
(*NONE*)
|
walther@59886
|
37 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
walther@59852
|
38 |
val insert_merge: for_kestore -> for_kestore list -> for_kestore list
|
walther@59886
|
39 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
walther@59850
|
40 |
end
|
walther@59852
|
41 |
|
walther@59850
|
42 |
(**)
|
walther@59850
|
43 |
structure Rule_Set(**): RULE_SET(**) =
|
walther@59850
|
44 |
struct
|
walther@59850
|
45 |
(**)
|
walther@59867
|
46 |
datatype T = datatype Rule_Def.rule_set;
|
walther@59867
|
47 |
type id = string;
|
walther@59850
|
48 |
|
walther@59852
|
49 |
(*/------- this will disappear eventually ----------------------------------------------------\*)
|
walther@59852
|
50 |
fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
|
walther@59852
|
51 |
val empty =
|
walther@59852
|
52 |
Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
|
walther@59878
|
53 |
srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.Empty_Prog}
|
walther@59852
|
54 |
(*\------- this will disappear eventually ----------------------------------------------------/*)
|
walther@59850
|
55 |
|
walther@59867
|
56 |
val id = Rule.set_id;
|
walther@59852
|
57 |
fun rep Rule_Def.Empty = rep empty
|
walther@59852
|
58 |
| rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
|
walther@59852
|
59 |
{id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
|
walther@59852
|
60 |
calc = calc, rules = rules, scr = scr}
|
walther@59878
|
61 |
| rep (Rule_Def.Sequence {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
|
walther@59852
|
62 |
{id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
|
walther@59852
|
63 |
calc = calc, rules = rules, scr = scr}
|
walther@59852
|
64 |
| rep (Rule_Def.Rrls _) = rep empty
|
walther@59850
|
65 |
|
walther@59852
|
66 |
fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
|
walther@59852
|
67 |
| append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59852
|
68 |
rules = rs, errpatts = errpatts, scr = sc}) r =
|
walther@59852
|
69 |
Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59852
|
70 |
rules = rs @ r, errpatts = errpatts, scr = sc}
|
walther@59878
|
71 |
| append_rules id (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59852
|
72 |
rules = rs, errpatts = errpatts, scr = sc}) r =
|
walther@59878
|
73 |
Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59852
|
74 |
rules = rs @ r, errpatts = errpatts, scr = sc}
|
walther@59852
|
75 |
| append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
|
walther@59852
|
76 |
|
walther@59852
|
77 |
fun merge_ids rls1 rls2 =
|
walther@59852
|
78 |
let
|
walther@59852
|
79 |
val id1 = (#id o rep) rls1
|
walther@59852
|
80 |
val id2 = (#id o rep) rls2
|
walther@59852
|
81 |
in
|
walther@59852
|
82 |
if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
|
walther@59852
|
83 |
end
|
walther@59852
|
84 |
|
walther@59852
|
85 |
fun merge _ Rule_Def.Empty rls = rls
|
walther@59852
|
86 |
| merge _ rls Rule_Def.Empty = rls
|
walther@59852
|
87 |
| merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
|
walther@59852
|
88 |
| merge _ _ (Rrls x) = Rrls x
|
walther@59852
|
89 |
| merge id
|
walther@59852
|
90 |
(Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
|
walther@59852
|
91 |
rules = rs1, errpatts = eps1, scr = sc1, ...})
|
walther@59852
|
92 |
(Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
|
walther@59852
|
93 |
rules = rs2, errpatts = eps2, ...})
|
walther@59852
|
94 |
=
|
walther@59852
|
95 |
Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,
|
walther@59852
|
96 |
preconds = union (op =) pc1 pc2,
|
walther@59852
|
97 |
erls = merge (merge_ids er1 er2) er1 er2,
|
walther@59852
|
98 |
srls = merge (merge_ids sr1 sr2) sr1 sr2,
|
walther@59853
|
99 |
calc = union Exec_Def.calc_eq ca1 ca2,
|
walther@59867
|
100 |
rules = union Rule.equal rs1 rs2,
|
walther@59852
|
101 |
errpatts = union (op =) eps1 eps2}
|
walther@59852
|
102 |
| merge id
|
walther@59878
|
103 |
(Rule_Def.Sequence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
|
walther@59852
|
104 |
rules = rs1, errpatts = eps1, scr = sc1, ...})
|
walther@59878
|
105 |
(Rule_Def.Sequence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
|
walther@59852
|
106 |
rules = rs2, errpatts = eps2, ...})
|
walther@59852
|
107 |
=
|
walther@59878
|
108 |
Rule_Def.Sequence {id = id, rew_ord = ro1, scr = sc1,
|
walther@59852
|
109 |
preconds = union (op =) pc1 pc2,
|
walther@59852
|
110 |
erls = merge (merge_ids er1 er2) er1 er2,
|
walther@59852
|
111 |
srls = merge (merge_ids sr1 sr2) sr1 sr2,
|
walther@59853
|
112 |
calc = union Exec_Def.calc_eq ca1 ca2,
|
walther@59867
|
113 |
rules = union Rule.equal rs1 rs2,
|
walther@59852
|
114 |
errpatts = union (op =) eps1 eps2}
|
walther@59852
|
115 |
| merge id _ _ = error ("merge: \"" ^ id ^
|
walther@59878
|
116 |
"\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Sequence");
|
walther@59852
|
117 |
|
walther@59850
|
118 |
(* datastructure for KEStore_Elems, intermediate for thehier *)
|
walther@59852
|
119 |
type for_kestore =
|
walther@59867
|
120 |
(id * (* id unique within Isac *)
|
walther@59879
|
121 |
(ThyC.id * (* just for assignment in thehier, not appropriate for parsing etc *)
|
walther@59867
|
122 |
T)) (* ((#id o rep) T) = id by coding discipline *)
|
walther@59852
|
123 |
fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
|
walther@59850
|
124 |
|
walther@59852
|
125 |
fun insert_merge (re as (id, (thyID, r1))) ys =
|
walther@59852
|
126 |
case get_index (fn y => if curry equal re y then SOME y else NONE) ys of
|
walther@59850
|
127 |
NONE => re :: ys
|
walther@59850
|
128 |
| SOME (i, (_, (_, r2))) =>
|
walther@59850
|
129 |
let
|
walther@59852
|
130 |
val r12 = merge id r1 r2
|
walther@59850
|
131 |
in list_update ys i (id, (thyID, r12)) end
|
walther@59852
|
132 |
fun to_kestore (s1, s2) = fold insert_merge s1 s2;
|
walther@59850
|
133 |
|
walther@59852
|
134 |
(* used only for one hack *)
|
walther@59852
|
135 |
fun keep_unique_rules id
|
walther@59852
|
136 |
(Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59852
|
137 |
rules = rs, errpatts = eps, scr = sc}) r =
|
walther@59852
|
138 |
Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59867
|
139 |
rules = gen_rems Rule.equal (rs, r),
|
walther@59852
|
140 |
errpatts = eps,
|
walther@59852
|
141 |
scr = sc}
|
walther@59852
|
142 |
| keep_unique_rules id
|
walther@59878
|
143 |
(Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59852
|
144 |
rules = rs, errpatts = eps, scr = sc}) r =
|
walther@59878
|
145 |
Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
|
walther@59867
|
146 |
rules = gen_rems Rule.equal (rs, r),
|
walther@59852
|
147 |
errpatts = eps,
|
walther@59852
|
148 |
scr = sc}
|
walther@59852
|
149 |
| keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
|
walther@59867
|
150 |
| keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ id rls);
|
walther@59850
|
151 |
|
walther@59851
|
152 |
fun get_rules Rule_Def.Empty = []
|
walther@59851
|
153 |
| get_rules (Rule_Def.Repeat {rules, ...}) = rules
|
walther@59878
|
154 |
| get_rules (Rule_Def.Sequence {rules, ...}) = rules
|
walther@59851
|
155 |
| get_rules (Rule_Def.Rrls _) = [];
|
walther@59850
|
156 |
|
walther@59907
|
157 |
fun id_from_rule (Rule.Rls_ rls) = id rls
|
walther@59907
|
158 |
| id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r);
|
walther@59907
|
159 |
|
walther@59914
|
160 |
(* check if a rule is contained in a rule-set (recursivley down in Rls_);
|
walther@59914
|
161 |
this rule can even be a rule-set itself *)
|
walther@59914
|
162 |
fun contains r rls =
|
walther@59914
|
163 |
let
|
walther@59914
|
164 |
fun (*find (_, Rls_ rls) = finds (get_rules rls)
|
walther@59914
|
165 |
| find r12 = equal r12
|
walther@59914
|
166 |
and*) finds [] = false
|
walther@59914
|
167 |
| finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
|
walther@59914
|
168 |
in
|
walther@59914
|
169 |
finds (get_rules rls)
|
walther@59914
|
170 |
end
|
walther@59914
|
171 |
|
walther@59863
|
172 |
(*/------- this will disappear eventually -----------\*)
|
walther@59863
|
173 |
type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
|
walther@59863
|
174 |
(term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
|
walther@59868
|
175 |
val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;
|
walther@59907
|
176 |
local
|
walther@59863
|
177 |
fun ii (_: term) = e_rrlsstate;
|
walther@59868
|
178 |
fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);
|
walther@59868
|
179 |
fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
|
walther@59863
|
180 |
fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
|
walther@59868
|
181 |
fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
|
walther@59863
|
182 |
in
|
walther@59863
|
183 |
val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
|
walther@59863
|
184 |
next_rule = ne, attach_form = fo};
|
walther@59863
|
185 |
end;
|
walther@59863
|
186 |
val e_rrls =
|
walther@59863
|
187 |
Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
|
walther@59863
|
188 |
calc = [], errpatts = [], scr = e_rfuns}
|
walther@59863
|
189 |
(*\------- this will disappear eventually -----------/*)
|
walther@59863
|
190 |
|
walther@59850
|
191 |
|
walther@59850
|
192 |
(**)end(**)
|