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 cterm' list | Given of cterm' list | Relate of cterm' list
10 type imodel = iitem list
11 type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec
12 val fetchErrorpatterns : Ctree.tac -> errpatID list
13 val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd
14 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
15 val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
16 val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac
18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
19 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
20 val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option
21 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
22 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate'
23 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
24 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
25 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
26 val check_error_patterns :
28 term * (term * term) list -> (errpatID * term list * 'a list) list * rls -> errpatID option
30 'a * (term * term) list -> 'b * term -> errpatID -> fillpat -> (fillpatID * term * 'b * 'a) option
32 'a * (term * term) list -> term -> errpatID -> thm -> (fillpatID * term * thm * 'a) list
33 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
37 structure Inform(**): INPUT_FORMULAS(**) =
41 (*** handle an input calc-head ***)
45 (*Where is never input*)
47 | Relate of cterm' list
49 type imodel = iitem list
51 (*calc-head as input*)
53 Ctree.pos' * (*the position of the calc-head in the calc-tree*)
54 cterm' * (*the headline*)
55 imodel * (*the model (without Find) of the calc-head*)
56 Ctree.pos_ * (*model belongs to Pbl or Met*)
57 spec; (*specification: domID, pblID, metID*)
58 val e_icalhd = (Ctree.e_pos', "", [Given [""]], Ctree.Pbl, e_spec) : icalhd
60 fun is_casinput (hdf : cterm') ((fmz_, spec) : Ctree.fmz) =
61 hdf <> "" andalso fmz_ = [] andalso spec = e_spec
63 (*.handle an input as into an algebra system.*)
64 fun dtss2itm_ ppc (d, ts) =
66 val (f, (d, id)) = the (find_first ((curry op= d) o
67 (#1: (term * term) -> term) o
68 (#2: pbt_ -> (term * term))) ppc)
70 ([1], true, f, Cor ((d, ts), (id, ts)))
73 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
75 fun cas_input_ ((dI, pI, mI): spec) dtss = (*WN110515 reconsider thy..ctxt*)
77 val thy = assoc_thy dI
78 val {ppc, ...} = Specify.get_pbt pI
79 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
80 val its = Specify.add_id its_
81 val pits = map flattup2 its
86 case Specify.refine_pbl thy pI pits of
87 SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI)
88 | NONE => (pI, (hd o #met o Specify.get_pbt) pI)
89 val {ppc, pre, prls, ...} = Specify.get_met mI
90 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
91 val its = Specify.add_id its_
92 val mits = map flattup2 its
93 val pre = check_preconds thy prls pre mits
94 val ctxt = Ctree.e_ctxt (*WN110515 cas_input_ DOESNT WORK*)
95 in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
98 (* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *)
101 val (h, argl) = strip_comb hdt
103 case assoc_cas (assoc_thy "Isac") h of
105 | SOME (spec as (dI,_,_), argl2dtss) =>
107 val dtss = argl2dtss argl
108 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
109 val spec = (dI, pI, mI)
111 Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
112 val pt = Ctree.update_spec pt [] spec
113 val pt = Ctree.update_pbl pt [] pits
114 val pt = Ctree.update_met pt [] mits
115 val pt = Ctree.update_ctxt pt [] ctxt
117 SOME (pt, (true, Ctree.Met, hdt, mits, pre, spec) : Ctree.ocalhd)
121 (*lazy evaluation for (Thy_Info.get_theory "Isac")*)
122 fun Isac _ = assoc_thy "Isac";
124 (* re-parse itms with a new thy and prepare for checking with ori list *)
125 fun parsitm dI (itm as (i, v, _, f, Cor ((d, ts), _)) : itm) =
126 (let val t = comp_dts (d, ts)
127 val _ = (term_to_string''' dI t)
128 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
130 handle _ => ((i, v, false, f, Syn (term2str t)) : itm))
131 | parsitm dI (i, v, b, f, Syn str) =
132 (let val _ = (Thm.term_of o the o (parse dI)) str
133 in (i, v, b ,f, Par str) end
134 handle _ => (i, v, b, f, Syn str))
135 | parsitm dI (i, v, b, f, Typ str) =
136 (let val _ = (Thm.term_of o the o (parse dI)) str
137 in (i, v, b, f, Par str) end
138 handle _ => (i, v, b, f, Syn str))
139 | parsitm dI (itm as (i, v, _, f, Inc ((d, ts), _))) =
140 (let val t = comp_dts (d,ts);
141 val _ = term_to_string''' dI t;
142 (*this ^ should raise the exn on unability of re-parsing dts*)
144 handle _ => (i, v, false, f, Syn (term2str t)))
145 | parsitm dI (itm as (i, v, _, f, Sup (d, ts))) =
146 (let val t = comp_dts (d,ts);
147 val _ = term_to_string''' dI t;
148 (*this ^ should raise the exn on unability of re-parsing dts*)
150 handle _ => (i, v, false, f, Syn (term2str t)))
151 | parsitm dI (itm as (i, v, _, f, Mis (d, t'))) =
153 val _ = term_to_string''' dI t;
154 (*this ^ should raise the exn on unability of re-parsing dts*)
156 handle _ => (i, v, false, f, Syn (term2str t)))
157 | parsitm dI (itm as (_, _, _, _, Par _)) =
158 error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm ^ "): Par should be internal");
160 (*separate a list to a pair of elements that do NOT satisfy the predicate,
161 and of elements that satisfy the predicate, i.e. (false, true)*)
162 fun filter_sep pred xs =
165 | filt (a, b) (x :: xs) =
167 then filt (a, b @ [x]) xs
168 else filt (a @ [x], b) xs
169 in filt ([], []) xs end;
170 fun is_Par ((_, _, _, _,Par _) : itm) = true
173 fun is_e_ts [] = true
174 | is_e_ts [Const ("List.list.Nil", _)] = true
177 (* WN.9.11.03 copied from fun appl_add *)
178 fun appl_add' dI oris ppc pbt (sel, ct) =
180 val ctxt = assoc_thy dI |> thy2ctxt;
182 case parseNEW ctxt ct of
183 NONE => (0,[],false,sel, Syn ct):itm
185 (case Chead.is_known ctxt sel oris t of
187 (case Chead.is_notyet_input ctxt ppc all ori' pbt of
189 | (msg,_) => error ("appl_add': " ^ msg))
190 | (_, (i, v, _, d, ts), _) =>
192 then (i, v, false, sel, Inc ((d, ts), (e_term, [])))
193 else (i, v, false, sel, Sup (d, ts)))
196 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
197 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
198 fun fstr2itm_ thy pbt (f, str) =
200 val topt = parse thy str
203 NONE => ([], false, f, Syn str)
206 val (d, ts) = (split_dts o Thm.term_of) ct
207 val popt = find_first (eq7 (f, d)) pbt
210 NONE => ([1](*??*), true(*??*), f, Sup (d, ts))
211 | SOME (f, (d, id)) => ([1], true, f, Cor ((d, ts), (id, ts)))
215 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
216 fun unknown_expl dI pbt selcts =
218 val thy = assoc_thy dI
219 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
220 val its = Specify.add_id its_
222 (map flattup2 its): itm list
225 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
226 appl_add': generate 1 item
227 appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
228 appl_add' . is_notyet_input: compare with items in model already input
229 insert_ppc': insert this 1 item*)
230 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
231 (*already present itms in model are being overwritten*)
232 | appl_adds _ _ ppc _ [] = ppc
233 | appl_adds dI oris ppc pbt (selct :: ss) =
234 let val itm = appl_add' dI oris ppc pbt selct;
235 in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end
237 fun oris2itms _ _ [] = ([] : itm list) (* WN161130: similar in ptyps ?!? *)
238 | oris2itms pbt vat ((i, v, f, d, ts) :: (os: ori list)) =
240 then (i, v, true, f, Cor ((d, ts), (e_term, []))) :: (oris2itms pbt vat os)
241 else oris2itms pbt vat os
243 fun par2fstr ((_, _, _, f, Par s) : itm) = (f, s)
244 | par2fstr itm = error ("par2fstr: called with " ^ itm2str_ (thy2ctxt' "Isac") itm)
245 fun itms2fstr ((_, _, _, f, Cor ((d, ts), _)) : itm) = (f, comp_dts'' (d, ts))
246 | itms2fstr (_, _, _, f, Syn str) = (f, str)
247 | itms2fstr (_, _, _, f, Typ str) = (f, str)
248 | itms2fstr (_, _, _, f, Inc ((d, ts), _)) = (f, comp_dts'' (d,ts))
249 | itms2fstr (_, _, _, f, Sup (d, ts)) = (f, comp_dts'' (d, ts))
250 | itms2fstr (_, _, _, f, Mis (d, t)) = (f, term2str (d $ t))
251 | itms2fstr (itm as (_, _, _, _, Par _)) =
252 error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ "): Par should be internal");
254 fun imodel2fstr iitems =
257 | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
258 | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
259 | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
260 in xxx [] iitems end;
262 (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
263 fun input_icalhd pt (((p, _), hdf, imodel, Pbl, spec as (dI, pI, mI)) : icalhd) =
265 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
266 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
267 spec = sspec as (sdI, spI, smI), probl, meth, ...}
268 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
269 | _ => error "input_icalhd: uncovered case of get_obj I pt p"
270 in if is_casinput hdf fmz then the (cas_input (str2term hdf))
271 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
272 let val (pos_, pits, mits) =
274 then let val its = map (parsitm (assoc_thy dI)) probl;
275 val (its, trms) = filter_sep is_Par its;
276 val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec))
277 in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
280 then if pI = snd3 ospec then (Pbl, probl, meth)
282 let val pbt = (#ppc o Specify.get_pbt) pI
283 val dI' = #1 (Chead.some_spec ospec spec)
284 val oris = if pI = #2 ospec then oris
285 else Specify.prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
286 in (Pbl, appl_adds dI' oris probl pbt
287 (map itms2fstr probl), meth) end
288 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
289 then let val met = (#ppc o Specify.get_met) mI
290 val mits = Chead.complete_metitms oris probl meth met
291 in if foldl and_ (true, map #3 mits)
292 then (Pbl, probl, mits) else (Ctree.Met, probl, mits)
294 else (Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)]
295 ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec)))
296 (imodel2fstr imodel), meth)
297 val pt = Ctree.update_spec pt p spec;
299 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
300 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
301 in (Ctree.update_pbl pt p pits,
302 (Chead.ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
304 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
305 val pre = check_preconds (assoc_thy"Isac") prls pre mits
306 in (Ctree.update_met pt p mits,
307 (Chead.ocalhd_complete mits pre spec, Ctree.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
311 | input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl."
314 (***. handle an input formula .***)
316 fun equal a b = a = b
318 (*the lists contain eq-al elem-pairs at the beginning;
319 return first list reverted (again) - ie. in order as required subsequently*)
320 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
323 if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
324 else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
325 else error "dropwhile': did not start with equal elements"
326 | dropwhile' equal (f::fs) [i] =
328 then (rev (f::fs), [i])
329 else error "dropwhile': did not start with equal elements"
330 | dropwhile' equal [f] (i::is) =
333 else error "dropwhile': did not start with equal elements"
334 | dropwhile' _ _ _ = error "dropwhile': uncovered case"
336 (* 040214: version for concat_deriv *)
337 fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a));
339 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
340 (Ctree.Rewrite (id, thm),
341 Ctree.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
342 (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Ctree.Uistate, Ctree.e_ctxt)))
343 | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
344 (Ctree.Rewrite_Set (Lucin.rule2rls' r),
345 Ctree.Rewrite_Set' ("Isac", false, rls, t, (t', a)),
346 (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Ctree.Uistate, Ctree.e_ctxt)))
347 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t)
349 (* fo = ifo excluded already in inform *)
350 fun concat_deriv rew_ord erls rules fo ifo =
352 fun derivat ([]:(term * rule * (term * term list)) list) = e_term
353 | derivat dt = (#1 o #3 o last_elem) dt
354 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
355 val fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
356 val ifod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
359 ([], []) => if fo = ifo then (true, []) else (false, [])
360 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
361 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
363 if derivat fod = derivat ifod (*common normal form found*)
366 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
367 in (true, fod' @ (map rev_deriv' rifod')) end
371 (* compare inform with ctree.form at current pos by nrls;
372 if found, embed the derivation generated during comparison
373 if not, let the mat-engine compute the next ctree.form *)
374 (* structure copied from complete_solve
375 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
376 all_modspec etc. has to be inserted at Subproblem'*)
377 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =
381 Frm => Ctree.get_obj Ctree.g_form pt p
382 | Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
383 | _ => e_term (*on PblObj is fo <> ifo*);
384 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
385 val {rew_ord, erls, rules, ...} = rep_rls nrls
386 val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
391 val tacis' = map (mk_tacis rew_ord erls) der;
392 val (c', ptp) = Generate.embed_deriv tacis' ptp;
393 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
395 if pos = ([], Ctree.Res) (*TODO: we should stop earlier with trying subproblems *)
396 then ("no derivation found", (tacis, c, ptp): Chead.calcstate')
399 val cs' as (tacis, c', ptp) = Solve.nxt_solve_ ptp; (*<---------------------*)
400 val (tacis, c'', ptp) = case tacis of
401 ((Ctree.Subproblem _, _, _)::_) =>
403 val ptp as (pt, (p,_)) = Chead.all_modspec ptp (*<--------------------*)
404 val mI = Ctree.get_obj Ctree.g_metID pt p
406 Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp
409 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
412 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
413 fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
415 val (res', _, _, rewritten) =
416 rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
421 val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
423 | SOME (norm_res, _) => norm_res
424 val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
426 | SOME (norm_inf, _) => norm_inf
427 in if norm_res = norm_inf then SOME errpatID else NONE
432 (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
433 (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
434 fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
436 val (_, subst) = Rtools.get_bdv_subst prog env
437 fun scan (_, [], _) = NONE
438 | scan (errpatID, errpat :: errpats, _) =
439 case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
440 NONE => scan (errpatID, errpats, [])
441 | SOME errpatID => SOME errpatID
443 | scans (group :: groups) =
446 | SOME errpatID => SOME errpatID
447 in scans errpats end;
449 (*.handle a user-input formula, which may be a CAS-command, too.
451 create a calchead, and do 1 step
452 TOOODO.WN0602 works only for the root-problem !!!
453 formula, which is no CAS-command:
454 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
455 collect all the tacs applied by the way;
456 if "no derivation found" then check_error_patterns.
457 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
458 fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
459 case parse (assoc_thy "Isac") istr of
462 val f_in = Thm.term_of f_in
463 val f_succ = Ctree.get_curr_formula (pt, pos);
466 then ("same-formula", cs) (* ctree not cut with replaceFormula *)
468 case cas_input f_in of
469 SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
472 val pos_pred = Ctree.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
473 val f_pred = Ctree.get_curr_formula (pt, pos_pred)
474 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
475 (*last step re-calc in compare_step TODO before WN09*)
477 case msg_calcstate' of
478 ("no derivation found", calcstate') =>
480 val pp = Ctree.par_pblobj pt p
481 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
482 {errpats, nrls, scr = Prog prog, ...} => (errpats, nrls, prog)
483 | _ => error "inform: uncovered case of get_met"
484 val env = case Ctree.get_istate pt pos of
485 Ctree.ScrState (env, _, _, _, _, _) => env
486 | _ => error "inform: uncovered case of get_istate"
488 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
489 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
490 | NONE => msg_calcstate'
492 | _ => msg_calcstate'
495 | NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate')
497 (* fill-in patterns an forms.
498 returns thm required by "fun in_fillform *)
499 fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) =
501 val (form', _, _, rewritten) =
502 rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
503 in (*the fillpat of the thm must be dedicated to errpatID*)
504 if errpatID = erpaID andalso rewritten
505 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
509 fun get_fillpats subst form errpatID thm =
511 val thmDeriv = Thm.get_name_hint thm
512 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
513 val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
514 val fillpats = case Specify.get_the theID of
515 Hthm {fillpats, ...} => fillpats
516 | _ => error "get_fillpats: uncovered case of get_the"
517 val some = map (get_fillform subst (thm, form) errpatID) fillpats
518 in some |> filter is_some |> map the end
520 fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID =
522 val f_curr = Ctree.get_curr_formula (pt, pos);
523 val pp = Ctree.par_pblobj pt p
524 val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
525 {errpats, scr = Prog prog, ...} => (errpats, prog)
526 | _ => error "find_fillpatterns: uncovered case of get_met"
527 val env = case Ctree.get_istate pt pos of
528 Ctree.ScrState (env, _, _, _, _, _) => env
529 | _ => error "inform: uncovered case of get_istate"
530 val subst = Rtools.get_bdv_subst prog env
531 val errpatthms = errpats
532 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
533 |> map (#3: errpat -> thm list)
535 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end
537 (* check if an input formula is exactly equal the rewrite from a rule
538 which is stored at the pos where the input is stored of "ok". *)
539 fun is_exactly_equal (pt, pos as (p, _)) istr =
540 case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
541 NONE => ("syntax error in '" ^ istr ^ "'", Ctree.Tac "")
544 val p' = Ctree.lev_on p;
545 val tac = Ctree.get_obj Ctree.g_tac pt p';
547 case Applicable.applicable_in pos pt tac of
548 Chead.Notappl msg => (msg, Ctree.Tac "")
551 val res = case rew of
552 Ctree.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
553 | Ctree.Rewrite' (_, _, _, _, _, _, (res, _)) => res
554 | t => error ("is_exactly_equal: uncovered case for " ^ Ctree.tac_2str t)
557 then ("input does not exactly fill the gaps", Ctree.Tac "")
562 (* fetch errpatIDs from an arbitrary tactic *)
563 fun fetchErrorpatterns tac =
567 Ctree.Rewrite_Set rlsID => rlsID
568 | Ctree.Rewrite_Set_Inst (_, rlsID) => rlsID
570 val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
571 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
572 Hrls {thy_rls = (_, rls), ...} => rls
573 | _ => error "fetchErrorpatterns: uncovered case of get_the"
575 Rls {errpatts, ...} => errpatts
576 | Seq {errpatts, ...} => errpatts
577 | Rrls {errpatts, ...} => errpatts