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: program, 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: program, 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: program}
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: program -> 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: program, 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 val thm2str: thm -> string
112 val thms2str : thm list -> string
113 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
114 val string_of_thm': theory -> thm -> string (* shift up to Unparse *)
115 val string_of_thm: thm -> string (* shift up to Unparse *)
116 val errpats2str : errpat list -> string
117 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
119 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
124 structure Rule(**): RULE(**) =
129 (* eval function calling sml code during rewriting.
130 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,
131 see "fun rule2stac": instead of
132 Calc: calID * eval_fn -> rule
134 Calc: prog_calcID * (calID * eval_fn)) -> rule*)
135 type eval_fn = (string -> term -> theory -> (string * term) option);
136 fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
138 (* op in isa-term "Const(op,_)" *)
139 type cal = calID * eval_fn;
140 type prog_calcID = string;
141 type calc = (prog_calcID * cal);
143 type calc_elem = (* fun calculate_ fetches the evaluation-function via this list *)
144 prog_calcID * (* a simple identifier used in programs *)
145 (calID * (* a long identifier used in Const *)
146 eval_fn) (* an ML function *)
147 fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
149 then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
152 type cterm' = string;
153 type subst = (term * term) list;
155 (*TODO.WN060610 make use of "type rew_ord" total*)
156 type rew_ord' = string;
157 val e_rew_ord' = "e_rew_ord" : rew_ord';
159 type rew_ord_ = subst -> Term.term * Term.term -> bool;
160 fun dummy_ord (_: subst) (_: term, _: term) = true;
161 val e_rew_ord_ = dummy_ord;
162 type rew_ord = rew_ord' * rew_ord_;
163 val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)
164 val e_rew_ordX = (e_rew_ord', e_rew_ord_);
166 (* rewrite orders, also stored in 'type met' and type 'and rls'
167 The association list is required for 'rewrite.."rew_ord"..' *)
168 val rew_ord' = Unsynchronized.ref
169 ([("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]
170 : (rew_ord' * (* the key for the association list *)
171 (subst (* the bound variables - they get high order*)
172 -> (term * term) (* (t1, t2) to be compared *)
173 -> bool)) (* if t1 <= t2 then true else false *)
174 list); (* association list *)
175 fun assoc' ([], key) = raise ERROR ("ME_Isa: \"" ^ key ^ "\" not known")
176 | assoc' ((keyi, xi) :: pairs, key) =
177 if key = keyi then SOME xi else assoc' (pairs, key);
178 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
179 handle _ => error ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
181 (* Since Isabelle2017 sessions in theory identifiers are enforced.
182 However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
183 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
184 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
185 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
186 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)
188 fun term_to_string' ctxt t =
190 val ctxt' = Config.put show_markup false ctxt
191 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
192 fun term_to_string'' thyID t =
194 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
195 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
196 fun term_to_string''' thy t =
198 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
199 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
201 fun term2str t = term_to_string' (thy2ctxt' "Isac_Knowledge") t;
202 fun t2str thy t = term_to_string' (thy2ctxt thy) t;
203 fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
204 fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
205 val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
206 val terms2str' = strs2str' o terms2strs; (* terms2str' [t1,t2] = "[1 + 2,abc]"; *)
207 fun termopt2str (SOME t) = "(SOME " ^ term2str t ^ ")"
208 | termopt2str NONE = "NONE";
212 val t = Thm.prop_of thm
213 val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
214 val ctxt' = Config.put show_markup false ctxt
215 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
216 fun thms2str thms = (strs2str o (map thm2str)) thms
218 (* error patterns and fill patterns *)
219 type errpatID = string
221 errpatID (* one identifier for a list of patterns
222 DESIGN ?TODO: errpatID list for hierarchy of errpats ? *)
223 * term list (* error patterns *)
224 * thm list (* thms related to error patterns; note that respective lhs
225 do not match (which reflects student's error).
226 fillpatterns are stored with these thms. *)
227 fun errpat2str (id, tms, thms) =
228 "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms
229 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
232 Erule (*.the empty rule .*)
233 | Thm of (string * Basic_Thm.thm) (* see TODO CLEANUP Thm *)
234 | Calc of string * (*.sml-code manipulating a (sub)term .*)
236 | Cal1 of string * (*.sml-code applied only to whole term
237 or left/right-hand-side of eqality .*)
239 | Rls_ of rls (*.ie. rule sets may be nested.*)
242 | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
243 where 'exp' does not contain a tactic. *)
244 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
245 {init_state : (* initialise for reverse rewriting by the Interpreter *)
246 term -> (* for this the rrlsstate is initialised: *)
247 term * (* the current formula: goes locate_input_tactic -> determine_next_tactic via istate *)
248 term * (* the final formula *)
249 rule list (* of reverse rewrite set (#1#) *)
250 list * (* may be serveral, eg. in norm_rational *)
251 ( rule * (* Thm (+ Thm generated from Calc) resulting in ... *)
252 (term * (* ... rewrite with ... *)
253 term list)) (* ... assumptions *)
254 list, (* derivation from given term to normalform
255 in reverse order with sym_thm;
256 (#1#) could be extracted from here #1 *)
257 normal_form: (* the function which drives the Rrls ##############################*)
258 term -> (term * term list) option,
259 locate_rule: (* checks a rule R for being a cancel-rule, and if it is,
260 then return the list of rules (+ the terms they are rewriting to)
261 which need to be applied before R should be applied.
262 precondition: the rule is applicable to the argument-term. *)
263 rule list list -> (* the reverse rule list *)
264 term -> (* ... to which the rule shall be applied *)
265 rule -> (* ... to be applied to term *)
266 ( rule * (* value: a rule rewriting to ... *)
267 (term * (* ... the resulting term ... *)
268 term list)) (* ... with the assumptions ( //#0) *)
269 list, (* there may be several such rules; the list is empty,
270 if the rule has nothing to do with e.g. cancelation *)
271 next_rule: (* for a given term return the next rules to be done for cancelling *)
272 rule list list->(* the reverse rule list *)
273 term -> (* the term for which ... *)
274 rule option, (* ... this rule is appropriate for cancellation;
275 there may be no such rule (if the term is eg.canceled already*)
276 attach_form: (* checks an input term TI, if it may belong to e.g. a current
277 cancellation, by trying to derive it from the given term TG.
280 term -> (* TG, the last one agreed upon by user + math-eng *)
281 term -> (* TI, the next one input by the user *)
282 ( rule * (* the rule to be applied in order to reach TI *)
283 (term * (* ... obtained by applying the rule ... *)
284 term list)) (* ... and the respective assumptions *)
285 list} (* there may be several such rules; the list is empty, if the
286 users term does not belong to e.g. a cancellation of the term
289 Erls (*for init e_rls*)
291 | Rls of (*a confluent and terminating ruleset, in general *)
292 {id : string, (*for trace_rewrite:=true *)
293 preconds : term list, (*unused WN020820 *)
294 (*WN060616 for efficiency...
295 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
296 rew_ord : rew_ord, (*for rules*)
297 erls : rls, (*for the conditions in rules *)
298 srls : rls, (*for evaluation of list_fns in script *)
299 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
301 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy *)
302 scr : program} (*Prog term: generating intermed.steps *)
303 | Seq of (*a sequence of rules to be tried only once *)
304 {id : string, (*for trace_rewrite:=true *)
305 preconds : term list, (*unused 20.8.02 *)
306 (*WN060616 for efficiency...
307 bdvs : false, (*set in prep_rls' for get_bdvs *)*)
308 rew_ord : rew_ord, (*for rules *)
309 erls : rls, (*for the conditions in rules *)
310 srls : rls, (*for evaluation of list_fns in script *)
311 calc : calc list, (*for Calculate in scr, set by prep_rls' *)
313 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
314 scr : program} (*Prog term (how to restrict type ???)*)
316 (*Rrls call SML-code and simulate an rls
317 difference: there is always _ONE_ redex rewritten in 1 call,
318 thus wrap Rrls by: Rls (Rls_ ...)*)
319 | Rrls of (* SML-functions within rewriting; step-wise execution provided;
321 difference: there is always _ONE_ redex rewritten in 1 call,
322 thus wrap Rrls by: Rls (Rls_ ...) *)
323 {id : string, (* for trace_rewrite := true *)
324 prepat : (term list *(* preconds, eval with subst from pattern;
325 if [@{term True}], match decides alone *)
326 term ) (* pattern matched with current (sub)term *)
327 list, (* meta-conjunction is or *)
328 rew_ord : rew_ord, (* for rules *)
329 erls : rls, (* for the conditions in rules and preconds *)
330 calc : calc list, (* for Calculate in scr, set automatic.in prep_rls' *)
331 errpatts : errpatID list,(*dialog-authoring in Build_Thydata.thy*)
332 scr : program}; (* Rfuns {...} (how to restrict type ???) *)
334 fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs! TODO "Erls"*)
335 | id_rls (Rls {id, ...}) = id
336 | id_rls (Seq {id, ...}) = id
337 | id_rls (Rrls {id, ...}) = id;
338 val rls2str = id_rls;
339 fun id_rule (Thm (id, _)) = id
340 | id_rule (Calc (id, _)) = id
341 | id_rule (Cal1 (id, _)) = id
342 | id_rule (Rls_ rls) = id_rls rls
343 | id_rule Erule = "Erule";
344 fun eq_rule (Thm (thm1, _), Thm (thm2, _)) = thm1 = thm2
345 | eq_rule (Calc (id1, _), Calc (id2, _)) = id1 = id2
346 | eq_rule (Rls_ rls1, Rls_ rls2) = id_rls rls1 = id_rls rls2
350 there are two kinds of theorems ...
351 (1) known by isabelle
352 (2) not known, eg. calc_thm, instantiated rls
353 the latter have a thmid "#..."
354 and thus outside isa we ALWAYS transport both (thmID, string_of_thmI)
355 and have a special assoc_thm / assoc_rls in this interface *)
356 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
357 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
358 type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
359 val e_domID = "e_domID" : domID;
361 fun string_of_thy thy = Context.theory_name thy: theory';
362 val theory2domID = string_of_thy;
363 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
364 val theory2theory' = string_of_thy;
365 val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
367 fun thyID2theory' (thyID:thyID) = thyID;
368 fun theory'2thyID (theory':theory') = theory';
370 fun type_to_string'' (thyID : thyID) t =
372 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
373 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
374 fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
375 val string_of_typ = type2str; (*legacy*)
376 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
378 (*check for [.] as caused by "fun assoc_thm'"*)
379 fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
380 fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
381 fun string_of_thmI thm =
383 val str = (de_quote o string_of_thm) thm
384 val (a, b) = split_nlast (5, Symbol.explode str)
387 [" ", " ","[", ".", "]"] => implode a
391 fun get_rules Erls = []
392 | get_rules (Rls {rules, ...}) = rules
393 | get_rules (Seq {rules, ...}) = rules
394 | get_rules (Rrls _) = [];
395 fun rule2str Erule = "Erule"
396 | rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thmI thm)^")"
397 | rule2str (Calc (str, _)) = "Calc (\""^str^"\",fn)"
398 | rule2str (Cal1 (str, _)) = "Cal1 (\""^str^"\",fn)"
399 | rule2str (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
400 fun rule2str' Erule = "Erule"
401 | rule2str' (Thm (str, _)) = "Thm (\""^str^"\",\"\")"
402 | rule2str' (Calc (str, _)) = "Calc (\""^str^"\",fn)"
403 | rule2str' (Cal1 (str, _)) = "Cal1 (\""^str^"\",fn)"
404 | rule2str' (Rls_ rls) = "Rls_ (\""^id_rls rls^"\")";
405 fun scr2str EmptyScr = "EmptyScr"
406 | scr2str (Prog s) = "Prog " ^ term2str s
407 | scr2str (Rfuns _) = "Rfuns";
409 val e_type = Type ("empty",[]);
410 val e_term = Const ("empty", e_type);
411 val e_rule = Thm ("refl", @{thm refl});
412 val e_term = Const ("empty", Type("'a", []));
413 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
414 (term * term * rule list list * (rule * (term * term list)) list);
415 val e_rrlsstate = (e_term,e_term, [[e_rule]], [(e_rule, (e_term, []))]) : rrlsstate;
419 fun ii (_: term) = e_rrlsstate;
420 fun no (_: term) = SOME (e_term, [e_term]);
421 fun lo (_: rule list list) (_: term) (_: rule) = [(e_rule, (e_term, [e_term]))];
422 fun ne (_: rule list list) (_: term) = SOME e_rule;
423 fun fo (_: rule list list) (_: term) (_: term) = [(e_rule, (e_term, [e_term]))];
425 val e_rfuns = Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
426 next_rule = ne, attach_form = fo};
429 Rls {id = "e_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
430 srls = Erls, calc = [], rules = [], errpatts = [], scr = EmptyScr}: rls;
432 Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Erls,
433 calc = [], errpatts = [], scr = e_rfuns}:rls;
435 fun rep_rls Erls = rep_rls e_rls
436 | rep_rls (Rls {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
437 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
438 calc = calc, rules = rules, scr = scr}
439 | rep_rls (Seq {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
440 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
441 calc = calc, rules = rules, scr = scr}
442 | rep_rls (Rrls _) = rep_rls e_rls
444 fun append_rls id Erls _ = raise ERROR ("append_rls: with \"" ^ id ^ "\" not for Erls")
445 | append_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
446 rules = rs, errpatts = errpatts, scr = sc}) r =
447 Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
448 rules = rs @ r, errpatts = errpatts, scr = sc}
449 | append_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
450 rules = rs, errpatts = errpatts, scr = sc}) r =
451 Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
452 rules = rs @ r, errpatts = errpatts, scr = sc}
453 | append_rls id (Rrls _) _ = raise ERROR ("append_rls: not for reverse-rewrite-rule-set " ^ id);
455 fun merge_ids rls1 rls2 =
457 val id1 = (#id o rep_rls) rls1
458 val id2 = (#id o rep_rls) rls2
460 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
462 fun merge_rls _ Erls rls = rls
463 | merge_rls _ rls Erls = rls
464 | merge_rls _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
465 | merge_rls _ _ (Rrls x) = Rrls x
467 (Rls {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
468 rules = rs1, errpatts = eps1, scr = sc1, ...})
469 (Rls {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
470 rules = rs2, errpatts = eps2, ...})
472 Rls {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}
480 (Seq {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
481 rules = rs1, errpatts = eps1, scr = sc1, ...})
482 (Seq {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
483 rules = rs2, errpatts = eps2, ...})
485 Seq {id = id, rew_ord = ro1, scr = sc1,
486 preconds = union (op =) pc1 pc2,
487 erls = merge_rls (merge_ids er1 er2) er1 er2,
488 srls = merge_rls (merge_ids sr1 sr2) sr1 sr2,
489 calc = union calc_eq ca1 ca2,
490 rules = union eq_rule rs1 rs2,
491 errpatts = union (op =) eps1 eps2}
492 | merge_rls id _ _ = error ("merge_rls: \"" ^ id ^
493 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Seq");
495 (* used only for one hack TODO remove *)
496 fun remove_rls id (Rls {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
497 rules = rs, errpatts = eps, scr = sc}) r =
498 Rls {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
499 rules = gen_rems eq_rule (rs, r),
502 | remove_rls id (Seq {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
503 rules = rs, errpatts = eps, scr = sc}) r =
504 Seq {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
505 rules = gen_rems eq_rule (rs, r),
508 | remove_rls id (Rrls _) _ = raise ERROR ("remove_rls: not for reverse-rewrite-rule-set "^id)
509 | remove_rls _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);