1 (* rules guiding stepwise execution of methods in the LUCAS_INTERPRETER.
2 Author: Walther Neuper 2018 (code gathered from other Isac source)
3 (c) copyright due to lincense terms
9 type eval_fn = string -> term -> theory -> (string * term) option
10 val e_evalfn: 'a -> term -> theory -> (string * term) option
11 type cal = calID * eval_fn
13 type calc = prog_calcID * cal
15 val calc_eq: calc_elem * calc_elem -> bool
17 eqtype cterm' (* shift up in sequence of defs *)
18 type subst = (term * term) list (* shift up in sequence of defs *)
21 val e_rew_ord': rew_ord'
23 val dummy_ord: rew_ord_
24 val e_rew_ord_: rew_ord_
25 type rew_ord = rew_ord' * rew_ord_
26 val e_rew_ord: rew_ord_
27 val e_rew_ordX: rew_ord
28 val rew_ord': (rew_ord' * (subst -> term * term -> bool)) list Unsynchronized.ref
29 val assoc_rew_ord: string -> subst -> term * term -> bool
32 type errpat = errpatID * term list * thm list
36 | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
37 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
38 | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
39 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
40 | Rrls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,
41 prepat: (term list * term) list, rew_ord: rew_ord, scr: scr}
42 and rule = Cal1 of string * eval_fn | Calc of string * eval_fn | Erule
43 | Rls_ of rls | Thm of string * thm
48 {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,
49 init_state: term -> term * term * rule list list * (rule * (term * term list)) list,
50 locate_rule: rule list list -> term -> rule -> (rule * (term * term list)) list,
51 next_rule: rule list list -> term -> rule option, normal_form: term ->
52 (term * term list) option}
53 val rule2str: rule -> string
54 val rule2str': rule -> string
56 val get_rules: rls -> rule list
57 val id_rule: rule -> string
58 val eq_rule: rule * rule -> bool
60 val scr2str: scr -> string
64 val rls2str: rls -> string
65 val id_rls: rls -> string
66 val rep_rls: rls -> {calc: calc list, erls: rls, errpats: errpatID list, id: string,
67 preconds: term list, rew_ord: rew_ord, rules: rule list, scr: scr, srls: rls}
68 val append_rls: string -> rls -> rule list -> rls
69 val merge_rls: string -> rls -> rls -> rls
70 val remove_rls: string -> rls -> rule list -> rls
72 type rrlsstate = term * term * rule list list * (rule * (term * term list)) list
73 val e_rrlsstate: rrlsstate
75 val thy2ctxt: theory -> Proof.context (* shift up in sequence of defs *)
76 val thy2ctxt': string -> Proof.context (* shift up in sequence of defs *)
77 val Thy_Info_get_theory: string -> theory (* shift up in sequence of defs *)
79 eqtype thyID (* shift up in sequence of defs *)
80 eqtype domID (* shift up in sequence of defs *)
81 val e_domID: domID (* shift up in sequence of defs *)
82 eqtype theory' (* shift up in sequence of defs *)
83 val theory'2thyID: theory' -> theory' (* shift up in sequence of defs *)
84 val theory2theory': theory -> theory' (* shift up in sequence of defs *)
85 val theory2thyID: theory -> thyID (* shift up in sequence of defs *)
86 val thyID2theory': thyID -> thyID (* shift up in sequence of defs *)
87 val string_of_thy: theory -> theory' (* shift up in sequence of defs *)
88 val theory2domID: theory -> theory' (* shift up in sequence of defs *)
90 val Isac: 'a -> theory (* shift up in sequence of defs *)
92 val string_of_thmI: thm -> string (* shift up to Unparse *)
93 val e_term: term (* shift up to Unparse *)
94 val e_type: typ (* shift up to Unparse *)
95 val type2str: typ -> string
96 val term_to_string': Proof.context -> term -> string (* shift up to Unparse *)
97 val term2str: term -> string (* shift up to Unparse *)
98 val termopt2str: term option -> string (* shift up to Unparse *)
99 val theory2str: theory -> theory' (* shift up to Unparse *)
100 val terms2str: term list -> string (* shift up to Unparse *)
101 val terms2strs: term list -> string list
102 val term_to_string'': thyID -> term -> string (* shift up to Unparse *)
103 val term_to_string''': theory -> term -> string (* shift up to Unparse *)
104 val t2str: theory -> term -> string
105 val ts2str: theory -> term list -> string (* shift up to Unparse *)
106 val string_of_typ: typ -> string (* shift up to Unparse *)
107 val string_of_typ_thy: thyID -> typ -> string (* shift up to Unparse *)
109 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
110 val terms2str': term list -> string (* shift up to Unparse *)
111 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
112 val string_of_thm': theory -> thm -> string (* shift up to Unparse *)
113 val string_of_thm: thm -> string (* shift up to Unparse *)
114 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
116 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
121 structure Rule(**): RULE(**) =
126 (* eval function calling sml code during rewriting.
127 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
128 see "fun rule2stac": instead of
129 Calc: calID * eval_fn -> rule
131 Calc: prog_calcID * (calID * eval_fn)) -> rule*)
132 type eval_fn = (string -> term -> theory -> (string * term) option);
133 fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
135 (* op in isa-term "Const(op,_)" *)
136 type cal = calID * eval_fn;
137 type prog_calcID = string;
138 type calc = (prog_calcID * cal);
140 type calc_elem = (* fun calculate_ fetches the evaluation-function via this list *)
141 prog_calcID * (* a simple identifier used in programs *)
142 (calID * (* a long identifier used in Const *)
143 eval_fn) (* an ML function *)
144 fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
146 then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
149 type cterm' = string;
150 type subst = (term * term) list;
152 (*TODO.WN060610 make use of "type rew_ord" total*)
153 type rew_ord' = string;
154 val e_rew_ord' = "e_rew_ord" : rew_ord';
156 type rew_ord_ = subst -> Term.term * Term.term -> bool;
157 fun dummy_ord (_: subst) (_: term, _: term) = true;
158 val e_rew_ord_ = dummy_ord;
159 type rew_ord = rew_ord' * rew_ord_;
160 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
161 val e_rew_ordX = (e_rew_ord', e_rew_ord_);
163 (* rewrite orders, also stored in 'type met' and type 'and rls'
164 The association list is required for 'rewrite.."rew_ord"..' *)
165 val rew_ord' = Unsynchronized.ref
166 ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
167 : (rew_ord' * (* the key for the association list *)
168 (subst (* the bound variables - they get high order*)
169 -> (term * term) (* (t1, t2) to be compared *)
170 -> bool)) (* if t1 <= t2 then true else false *)
171 list); (* association list *)
172 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
173 | assoc' ((keyi, xi) :: pairs, key) =
174 if key = keyi then SOME xi else assoc' (pairs, key);
175 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
176 handle _ => error ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
179 (* error patterns and fill patterns *)
180 type errpatID = string
182 errpatID (* one identifier for a list of patterns
183 DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
184 * term list (* error patterns *)
185 * thm list (* thms related to error patterns; note that respective lhs
186 do not match (which reflects student's error).
187 fillpatterns are stored with these thms. *)
190 Erule (*.the empty rule .*)
191 | Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm *)
192 | Calc of string * (*.sml-code manipulating a (sub)term .*)
194 | Cal1 of string * (*.sml-code applied only to whole term
195 or left/right-hand-side of eqality .*)
197 | Rls_ of rls (*.ie. rule sets may be nested.*)
200 | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
201 where 'exp' does not contain a tactic. *)
202 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
203 {init_state : (* initialise for reverse rewriting by the Interpreter *)
204 term -> (* for this the rrlsstate is initialised: *)
205 term * (* the current formula: goes locate_input_tactic -> determine_next_tactic via istate *)
206 term * (* the final formula *)
207 rule list (* of reverse rewrite set (#1#) *)
208 list * (* may be serveral, eg. in norm_rational *)
209 ( rule * (* Thm (+ Thm generated from Calc) resulting in ... *)
210 (term * (* ... rewrite with ... *)
211 term list)) (* ... assumptions *)
212 list, (* derivation from given term to normalform
213 in reverse order with sym_thm;
214 (#1#) could be extracted from here #1 *)
215 normal_form: (* the function which drives the Rrls ##############################*)
216 term -> (term * term list) option,
217 locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
218 then return the list of rules (+ the terms they are rewriting to)
219 which need to be applied before R should be applied.
220 precondition: the rule is applicable to the argument-term. *)
221 rule list list -> (* the reverse rule list *)
222 term -> (* ... to which the rule shall be applied *)
223 rule -> (* ... to be applied to term *)
224 ( rule * (* value: a rule rewriting to ... *)
225 (term * (* ... the resulting term ... *)
226 term list)) (* ... with the assumptions ( //#0) *)
227 list, (* there may be several such rules; the list is empty,
228 if the rule has nothing to do with e.g. cancelation *)
229 next_rule: (* for a given term return the next rules to be done for cancelling *)
230 rule list list->(* the reverse rule list *)
231 term -> (* the term for which ... *)
232 rule option, (* ... this rule is appropriate for cancellation;
233 there may be no such rule (if the term is eg.canceled already*)
234 attach_form: (* checks an input term TI, if it may belong to e.g. a current
235 cancellation, by trying to derive it from the given term TG.
238 term -> (* TG, the last one agreed upon by user + math-eng *)
239 term -> (* TI, the next one input by the user *)
240 ( rule * (* the rule to be applied in order to reach TI *)
241 (term * (* ... obtained by applying the rule ... *)
242 term list)) (* ... and the respective assumptions *)
243 list} (* there may be several such rules; the list is empty, if the
244 users term does not belong to e.g. a cancellation of the term
247 Erls (*for init e_rls*)
249 | Rls of (*a confluent and terminating ruleset, in general *)
250 {id : string, (*for trace_rewrite:=true *)
251 preconds : term list, (*unused WN020820 *)
252 (*WN060616 for efficiency...
253 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
254 rew_ord : rew_ord, (*for rules*)
255 erls : rls, (*for the conditions in rules *)
256 srls : rls, (*for evaluation of list_fns in script *)
257 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
259 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *)
260 scr : scr} (*Prog term: generating intermed.steps *)
261 | Seq of (*a sequence of rules to be tried only once *)
262 {id : string, (*for trace_rewrite:=true *)
263 preconds : term list, (*unused 20.8.02 *)
264 (*WN060616 for efficiency...
265 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
266 rew_ord : rew_ord, (*for rules *)
267 erls : rls, (*for the conditions in rules *)
268 srls : rls, (*for evaluation of list_fns in script *)
269 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
271 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
272 scr : scr} (*Prog term (how to restrict type ???)*)
274 (*Rrls call SML-code and simulate an rls
275 difference: there is always _ONE_ redex rewritten in 1 call,
276 thus wrap Rrls by: Rls (Rls_ ...)*)
277 | Rrls of (* SML-functions within rewriting; step-wise execution provided;
279 difference: there is always _ONE_ redex rewritten in 1 call,
280 thus wrap Rrls by: Rls (Rls_ ...) *)
281 {id : string, (* for trace_rewrite := true *)
282 prepat : (term list *(* preconds, eval with subst from pattern;
283 if [@{term True}], match decides alone *)
284 term ) (* pattern matched with current (sub)term *)
285 list, (* meta-conjunction is or *)
286 rew_ord : rew_ord, (* for rules *)
287 erls : rls, (* for the conditions in rules and preconds *)
288 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
289 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
290 scr : scr}; (* Rfuns {...} (how to restrict type ???) *)
292 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Erls"*)
293 | id_rls (Rls {id, ...}) = id
294 | id_rls (Seq {id, ...}) = id
295 | id_rls (Rrls {id, ...}) = id;
296 val rls2str = id_rls;
297 fun id_rule (Thm (id, _)) = id
298 | id_rule (Calc (id, _)) = id
299 | id_rule (Cal1 (id, _)) = id
300 | id_rule (Rls_ rls) = id_rls rls
301 | id_rule Erule = "Erule";
302 fun eq_rule (Thm (thm1, _), Thm (thm2, _)) = thm1 = thm2
303 | eq_rule (Calc (id1, _), Calc (id2, _)) = id1 = id2
304 | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
307 (* Since Isabelle2017 sessions in theory identifiers are enforced.
308 However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
309 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
310 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
311 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
312 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
314 fun term_to_string' ctxt t =
316 val ctxt' = Config.put show_markup false ctxt
317 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
318 fun term_to_string'' thyID t =
320 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
321 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
322 fun term_to_string''' thy t =
324 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
325 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
327 fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
328 fun t2str thy t = term_to_string' (thy2ctxt thy) t;
329 fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
330 fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
331 val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
332 val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *)
333 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
334 | termopt2str NONE = "NONE";
337 there are two kinds of theorems ...
338 (1) known by isabelle
339 (2) not known, eg. calc_thm, instantiated rls
340 the latter have a thmid "#..."
341 and thus outside isa we ALWAYS transport both (thmID, string_of_thmI)
342 and have a special assoc_thm / assoc_rls in this interface *)
343 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
344 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
345 type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
346 val e_domID = "e_domID" : domID;
348 fun string_of_thy thy = Context.theory_name thy: theory';
349 val theory2domID = string_of_thy;
350 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
351 val theory2theory' = string_of_thy;
352 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
354 fun thyID2theory' (thyID:thyID) = thyID;
355 fun theory'2thyID (theory':theory') = theory';
357 fun type_to_string'' (thyID : thyID) t =
359 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
360 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
361 fun type2str typ = type_to_string'' "Isac" typ; (*TODO legacy*)
362 val string_of_typ = type2str; (*legacy*)
363 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
365 (*check for [.] as caused by "fun assoc_thm'"*)
366 fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (Thm.prop_of thm)
367 fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
368 fun string_of_thmI thm =
370 val str = (de_quote o string_of_thm) thm
371 val (a, b) = split_nlast (5, Symbol.explode str)
374 [" ", " ","[", ".", "]"] => implode a
378 fun get_rules Erls = []
379 | get_rules (Rls {rules, ...}) = rules
380 | get_rules (Seq {rules, ...}) = rules
381 | get_rules (Rrls _) = [];
382 fun rule2str Erule = "Erule"
383 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
384 | rule2str (Calc (str, _)) = "Calc (\""^str^"\",fn)"
385 | rule2str (Cal1 (str, _)) = "Cal1 (\""^str^"\",fn)"
386 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
387 fun rule2str' Erule = "Erule"
388 | rule2str' (Thm (str, _)) = "Thm (\""^str^"\",\"\")"
389 | rule2str' (Calc (str, _)) = "Calc (\""^str^"\",fn)"
390 | rule2str' (Cal1 (str, _)) = "Cal1 (\""^str^"\",fn)"
391 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
392 fun scr2str EmptyScr = "EmptyScr"
393 | scr2str (Prog s) = "Prog " ^ term2str s
394 | scr2str (Rfuns _) = "Rfuns";
396 val e_type = Type ("empty",[]);
397 val e_term = Const ("empty", e_type);
398 val e_rule = Thm ("refl", @{thm refl});
399 val e_term = Const ("empty", Type("'a", []));
400 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
401 (term * term * rule list list * (rule * (term * term list)) list);
402 val e_rrlsstate = (e_term,e_term, [[e_rule]], [(e_rule, (e_term, []))]) : rrlsstate;
406 fun ii (_: term) = e_rrlsstate;
407 fun no (_: term) = SOME (e_term, [e_term]);
408 fun lo (_: rule list list) (_: term) (_: rule) = [(e_rule, (e_term, [e_term]))];
409 fun ne (_: rule list list) (_: term) = SOME e_rule;
410 fun fo (_: rule list list) (_: term) (_: term) = [(e_rule, (e_term, [e_term]))];
412 val e_rfuns = Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
413 next_rule = ne, attach_form = fo};
416 Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
417 srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls;
419 Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
420 calc = [], errpatts = [], scr = e_rfuns}:rls;
422 fun rep_rls Erls = rep_rls e_rls
423 | rep_rls (Rls {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
424 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
425 calc = calc, rules = rules, scr = scr}
426 | rep_rls (Seq {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
427 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
428 calc = calc, rules = rules, scr = scr}
429 | rep_rls (Rrls _) = rep_rls e_rls
431 fun append_rls id Erls _ = raise ERROR ("append_rls: with \"" ^ id ^ "\" not for Erls")
432 | append_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
433 rules = rs, errpatts = errpatts, scr = sc}) r =
434 Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
435 rules = rs @ r, errpatts = errpatts, scr = sc}
436 | append_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
437 rules = rs, errpatts = errpatts, scr = sc}) r =
438 Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
439 rules = rs @ r, errpatts = errpatts, scr = sc}
440 | append_rls id (Rrls _) _ = raise ERROR ("append_rls: not for reverse-rewrite-rule-set " ^ id);
442 fun merge_ids rls1 rls2 =
444 val id1 = (#id o rep_rls) rls1
445 val id2 = (#id o rep_rls) rls2
447 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
449 fun merge_rls _ Erls rls = rls
450 | merge_rls _ rls Erls = rls
451 | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
452 | merge_rls _ _ (Rrls x) = Rrls x
454 (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
455 rules = rs1, errpatts = eps1, scr = sc1, ...})
456 (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
457 rules = rs2, errpatts = eps2, ...})
459 Rls {id = id, rew_ord = ro1, scr = sc1,
460 preconds = union (op =) pc1 pc2,
461 erls = merge_rls (merge_ids er1 er2) er1 er2,
462 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
463 calc = union calc_eq ca1 ca2,
464 rules = union eq_rule rs1 rs2,
465 errpatts = union (op =) eps1 eps2}
467 (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
468 rules = rs1, errpatts = eps1, scr = sc1, ...})
469 (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
470 rules = rs2, errpatts = eps2, ...})
472 Seq {id = id, rew_ord = ro1, scr = sc1,
473 preconds = union (op =) pc1 pc2,
474 erls = merge_rls (merge_ids er1 er2) er1 er2,
475 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
476 calc = union calc_eq ca1 ca2,
477 rules = union eq_rule rs1 rs2,
478 errpatts = union (op =) eps1 eps2}
479 | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^
480 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");
482 (* used only for one hack TODO remove *)
483 fun remove_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
484 rules = rs, errpatts = eps, scr = sc}) r =
485 Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
486 rules = gen_rems eq_rule (rs, r),
489 | remove_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
490 rules = rs, errpatts = eps, scr = sc}) r =
491 Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
492 rules = gen_rems eq_rule (rs, r),
495 | remove_rls id (Rrls _) _ = raise ERROR ("remove_rls: not for reverse-rewrite-rule-set "^id)
496 | remove_rls _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);