1 (* Handle user-input during the specify- and the solve-phase.
4 (c) due to copyright terms
7 signature INPUT_FORMULAS =
9 datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list
10 type imodel = iitem list
11 type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec
12 val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
13 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
14 val find_fillpatterns : Ctree.state -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
15 val is_exactly_equal : Ctree.state -> string -> string * Tactic.input
16 (*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
17 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
18 Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
19 val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))
20 val check_error_patterns :
22 term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule.rls -> Rule.errpatID option
23 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
27 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
29 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
30 val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option
32 'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
34 'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list
35 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
37 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
39 val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list ->
40 ('c * ''b * bool * 'd * Model.itm_) list
43 structure Inform(**): INPUT_FORMULAS(**) =
46 (*** handle an input calc-head ***)
49 Given of Rule.cterm' list
50 (*Where is never input*)
51 | Find of Rule.cterm' list
52 | Relate of Rule.cterm' list
54 type imodel = iitem list
56 (*calc-head as input*)
58 Ctree.pos' * (*the position of the calc-head in the calc-tree*)
59 Rule.cterm' * (*the headline*)
60 imodel * (*the model (without Find) of the calc-head*)
61 Ctree.pos_ * (*model belongs to Pbl or Met*)
62 Celem.spec; (*specification: domID, pblID, metID*)
63 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
65 fun is_casinput (hdf : Rule.cterm') ((fmz_, spec) : Selem.fmz) =
66 hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
68 (*.handle an input as into an algebra system.*)
69 fun dtss2itm_ ppc (d, ts) =
71 val (f, (d, id)) = the (find_first ((curry op= d) o
72 (#1: (term * term) -> term) o
73 (#2: Celem.pbt_ -> (term * term))) ppc)
75 ([1], true, f, Model.Cor ((d, ts), (id, ts)))
78 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
80 fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*)
82 val thy = Celem.assoc_thy dI
83 val {ppc, ...} = Specify.get_pbt pI
84 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
85 val its = Specify.add_id its_
86 val pits = map flattup2 its
91 case Specify.refine_pbl thy pI pits of
92 SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
93 | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
94 val {ppc, pre, prls, ...} = Specify.get_met mI
95 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
96 val its = Specify.add_id its_
97 val mits = map flattup2 its
98 val pre = Stool.check_preconds thy prls pre mits
99 val ctxt = ContextC.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
100 in (pI, pits, mI, mits, pre, ctxt) end;
103 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
106 val (h, argl) = strip_comb hdt
108 case assoc_cas (Celem.assoc_thy "Isac_Knowledge") h of
110 | SOME (spec as (dI,_,_), argl2dtss) =>
112 val dtss = argl2dtss argl
113 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
114 val spec = (dI, pI, mI)
116 Ctree.cappend_problem Ctree.e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, hdt)
117 val pt = Ctree.update_spec pt [] spec
118 val pt = Ctree.update_pbl pt [] pits
119 val pt = Ctree.update_met pt [] mits
120 val pt = Ctree.update_ctxt pt [] ctxt
122 SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
126 (*lazy evaluation for (Thy_Info_get_theory "Isac_Knowledge")*)
127 fun Isac _ = Celem.assoc_thy "Isac_Knowledge";
129 (* re-parse itms with a new thy and prepare for checking with ori list *)
130 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
131 (let val t = Model.comp_dts (d, ts)
132 val _ = (Rule.term_to_string''' dI t)
133 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
135 handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
136 | parsitm dI (i, v, b, f, Model.Syn str) =
137 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
138 in (i, v, b ,f, Model.Par str) end
139 handle _ => (i, v, b, f, Model.Syn str))
140 | parsitm dI (i, v, b, f, Model.Typ str) =
141 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
142 in (i, v, b, f, Model.Par str) end
143 handle _ => (i, v, b, f, Model.Syn str))
144 | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) =
145 (let val t = Model.comp_dts (d,ts);
146 val _ = Rule.term_to_string''' dI t;
147 (*this ^ should raise the exn on unability of re-parsing dts*)
149 handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
150 | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) =
151 (let val t = Model.comp_dts (d,ts);
152 val _ = Rule.term_to_string''' dI t;
153 (*this ^ should raise the exn on unability of re-parsing dts*)
155 handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
156 | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) =
158 val _ = Rule.term_to_string''' dI t;
159 (*this ^ should raise the exn on unability of re-parsing dts*)
161 handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
162 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
163 error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt dI) itm ^ "): Par should be internal");
165 (*separate a list to a pair of elements that do NOT satisfy the predicate,
166 and of elements that satisfy the predicate, i.e. (false, true)*)
167 fun filter_sep pred xs =
170 | filt (a, b) (x :: xs) =
172 then filt (a, b @ [x]) xs
173 else filt (a @ [x], b) xs
174 in filt ([], []) xs end;
175 fun is_Par (_, _, _, _, Model.Par _) = true
178 fun is_e_ts [] = true
179 | is_e_ts [Const ("List.list.Nil", _)] = true
182 (* WN.9.11.03 copied from fun appl_add *)
183 fun appl_add' dI oris ppc pbt (sel, ct) =
185 val ctxt = Celem.assoc_thy dI |> Rule.thy2ctxt;
187 case TermC.parseNEW ctxt ct of
188 NONE => (0, [], false, sel, Model.Syn ct)
190 (case Chead.is_known ctxt sel oris t of
192 (case Chead.is_notyet_input ctxt ppc all ori' pbt of
194 | (msg,_) => error ("appl_add': " ^ msg))
195 | (_, (i, v, _, d, ts), _) =>
197 then (i, v, false, sel, Model.Inc ((d, ts), (Rule.e_term, [])))
198 else (i, v, false, sel, Model.Sup (d, ts)))
201 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
202 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
203 fun fstr2itm_ thy pbt (f, str) =
205 val topt = TermC.parse thy str
208 NONE => ([], false, f, Model.Syn str)
211 val (d, ts) = (Model.split_dts o Thm.term_of) ct
212 val popt = find_first (eq7 (f, d)) pbt
215 NONE => ([1](*??*), true(*??*), f, Model.Sup (d, ts))
216 | SOME (f, (d, id)) => ([1], true, f, Model.Cor ((d, ts), (id, ts)))
220 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
221 fun unknown_expl dI pbt selcts =
223 val thy = Celem.assoc_thy dI
224 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
225 val its = Specify.add_id its_
226 in map flattup2 its end
228 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
229 appl_add': generate 1 item
230 appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
231 appl_add' . is_notyet_input: compare with items in model already input
232 insert_ppc': insert this 1 item*)
233 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
234 (*already present itms in model are being overwritten*)
235 | appl_adds _ _ ppc _ [] = ppc
236 | appl_adds dI oris ppc pbt (selct :: ss) =
237 let val itm = appl_add' dI oris ppc pbt selct;
238 in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
240 fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *)
241 | oris2itms pbt vat ((i, v, f, d, ts) :: os) =
243 then (i, v, true, f, Model.Cor ((d, ts), (Rule.e_term, []))) :: (oris2itms pbt vat os)
244 else oris2itms pbt vat os
246 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
247 | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm)
248 fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
249 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
250 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
251 | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts))
252 | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
253 | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Rule.term2str (d $ t))
254 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
255 error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
257 fun imodel2fstr iitems =
260 | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
261 | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
262 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
263 in xxx [] iitems end;
265 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
266 fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
268 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
269 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
270 spec = sspec as (sdI, spI, smI), probl, meth, ...}
271 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
272 | _ => error "input_icalhd: uncovered case of get_obj I pt p"
273 in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf))
274 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
275 let val (pos_, pits, mits) =
277 then let val its = map (parsitm (Celem.assoc_thy dI)) probl;
278 val (its, trms) = filter_sep is_Par its;
279 val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
280 in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
283 then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
285 let val pbt = (#ppc o Specify.get_pbt) pI
286 val dI' = #1 (Chead.some_spec ospec spec)
287 val oris = if pI = #2 ospec then oris
288 else Specify.prep_ori fmz_(Celem.assoc_thy"Isac_Knowledge") pbt |> #1;
289 in (Pos.Pbl, appl_adds dI' oris probl pbt
290 (map itms2fstr probl), meth) end
291 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
292 then let val met = (#ppc o Specify.get_met) mI
293 val mits = Chead.complete_metitms oris probl meth met
294 in if foldl and_ (true, map #3 mits)
295 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
297 else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
298 ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
299 (imodel2fstr imodel), meth)
300 val pt = Ctree.update_spec pt p spec;
302 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
303 val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls where_ pits
304 in (Ctree.update_pbl pt p pits,
305 (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
307 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
308 val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls pre mits
309 in (Ctree.update_met pt p mits,
310 (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
314 | input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl."
317 (***. handle an input formula .***)
319 (*the lists contain eq-al elem-pairs at the beginning;
320 return first list reverted (again) - ie. in order as required subsequently*)
321 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
324 if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
325 else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
326 else error "dropwhile': did not start with equal elements"
327 | dropwhile' equal (f::fs) [i] =
329 then (rev (f::fs), [i])
330 else error "dropwhile': did not start with equal elements"
331 | dropwhile' equal [f] (i::is) =
334 else error "dropwhile': did not start with equal elements"
335 | dropwhile' _ _ _ = error "dropwhile': uncovered case"
337 (* 040214: version for concat_deriv *)
338 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
340 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
341 (Tactic.Rewrite (id, thm),
342 Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
343 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
344 | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
345 (Tactic.Rewrite_Set (Lucin.rule2rls' r),
346 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
347 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
348 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)
350 (* fo = ifo excluded already in inform *)
351 fun concat_deriv rew_ord erls rules fo ifo =
353 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = Rule.e_term
354 | derivat dt = (#1 o #3 o last_elem) dt
355 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
356 val fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
357 val ifod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
360 ([], []) => if fo = ifo then (true, []) else (false, [])
361 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
362 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
364 if derivat fod = derivat ifod (*common normal form found*)
367 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
368 in (true, fod' @ (map rev_deriv' rifod')) end
372 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
373 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
375 val (res', _, _, rewritten) =
376 Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res;
381 val norm_res = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls res' of
383 | SOME (norm_res, _) => norm_res
384 val norm_inf = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls inf of
386 | SOME (norm_inf, _) => norm_inf
387 in if norm_res = norm_inf then SOME errpatID else NONE
392 (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
393 (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
394 fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
396 val (_, subst) = Rtools.get_bdv_subst prog env
397 fun scan (_, [], _) = NONE
398 | scan (errpatID, errpat :: errpats, _) =
399 case check_err_patt (res, inf) subst (errpatID, errpat) rls of
400 NONE => scan (errpatID, errpats, [])
401 | SOME errpatID => SOME errpatID
403 | scans (group :: groups) =
406 | SOME errpatID => SOME errpatID
407 in scans errpats end;
409 (* fill-in patterns an forms.
410 returns thm required by "fun in_fillform *)
411 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
413 val (form', _, _, rewritten) =
414 Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form;
415 in (*the fillpat of the thm must be dedicated to errpatID*)
416 if errpatID = erpaID andalso rewritten
417 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
421 fun get_fillpats subst form errpatID thm =
423 val thmDeriv = Thm.get_name_hint thm
424 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
425 val theID = [part, thyID, "Theorems", Celem.thmID_of_derivation_name thmDeriv]
426 val fillpats = case Specify.get_the theID of
427 Celem.Hthm {fillpats, ...} => fillpats
428 | _ => error "get_fillpats: uncovered case of get_the"
429 val some = map (get_fillform subst (thm, form) errpatID) fillpats
430 in some |> filter is_some |> map the end
432 fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =
434 val f_curr = Ctree.get_curr_formula (pt, pos);
435 val pp = Ctree.par_pblobj pt p
436 val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
437 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
438 | _ => error "find_fillpatterns: uncovered case of get_met"
439 val {env, ...} = Ctree.get_istate pt pos |> Istate.the_pstate
440 val subst = Rtools.get_bdv_subst prog env
441 val errpatthms = errpats
442 |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID))
443 |> map (#3: Rule.errpat -> thm list)
445 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
447 (* check if an input formula is exactly equal the rewrite from a rule
448 which is stored at the pos where the input is stored of "ok". *)
449 fun is_exactly_equal (pt, pos as (p, _)) istr =
450 case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of
451 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
454 val p' = Ctree.lev_on p;
455 val tac = Ctree.get_obj Ctree.g_tac pt p';
457 case Applicable.applicable_in pos pt tac of
458 Chead.Notappl msg => (msg, Tactic.Tac "")
461 val res = case rew of
462 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
463 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
464 | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.tac_2str t)
467 then ("input does not exactly fill the gaps", Tactic.Tac "")
472 (* fetch errpatIDs from an arbitrary tactic *)
473 fun fetchErrorpatterns tac =
477 Tactic.Rewrite_Set rlsID => rlsID
478 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
480 val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
481 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
482 Celem.Hrls {thy_rls = (_, rls), ...} => rls
483 | _ => error "fetchErrorpatterns: uncovered case of get_the"
485 Rule.Rls {errpatts, ...} => errpatts
486 | Rule.Seq {errpatts, ...} => errpatts
487 | Rule.Rrls {errpatts, ...} => errpatts