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 = pos' * cterm' * imodel * pos_ * spec
12 val fetchErrorpatterns : tac -> errpatID list
13 val input_icalhd : ptree -> icalhd -> ptree * ocalhd
14 val inform : calcstate' -> string -> string * calcstate'
15 val find_fillpatterns : ptree * pos' -> errpatID -> (fillpatID * term * thm * subs option) list
16 val is_exactly_equal : ptree * (pos * pos_) -> string -> string * 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 -> (ptree * ocalhd) option
21 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
22 val compare_step : taci list * pos' list * (ptree * pos') -> term -> string * 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 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 pos_ * (*model belongs to Pbl or Met*)
57 spec; (*specification: domID, pblID, metID*)
58 val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec) : icalhd
60 fun is_casinput (hdf : cterm') ((fmz_, spec) : 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, ...} = get_pbt pI
79 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
81 val pits = map flattup2 its
86 case refine_pbl thy pI pits of
87 SOME (pI,_) => (pI, (hd o #met o get_pbt) pI)
88 | NONE => (pI, (hd o #met o get_pbt) pI)
89 val {ppc, pre, prls, ...} = get_met mI
90 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
92 val mits = map flattup2 its
93 val pre = check_preconds thy prls pre mits
94 val ctxt = 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 cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, hdt)
112 val pt = update_spec pt [] spec
113 val pt = update_pbl pt [] pits
114 val pt = update_met pt [] mits
115 val pt = update_ctxt pt [] ctxt
117 SOME (pt, (true, Met, hdt, mits, pre, spec) : 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 is_known ctxt sel oris t of
187 (case 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 = 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 (insert_ppc' itm ppc) pbt ss end
237 fun oris2itms _ _ [] = ([] : itm list)
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 filter_dsc oris itm =
244 filter_out ((curry op= ((d_in o #5) (itm:itm))) o (#4:ori -> term)) oris
246 fun par2fstr ((_, _, _, f, Par s) : itm) = (f, s)
247 | par2fstr itm = error ("par2fstr: called with " ^ itm2str_ (thy2ctxt' "Isac") itm)
248 fun itms2fstr ((_, _, _, f, Cor ((d, ts), _)) : itm) = (f, comp_dts'' (d, ts))
249 | itms2fstr (_, _, _, f, Syn str) = (f, str)
250 | itms2fstr (_, _, _, f, Typ str) = (f, str)
251 | itms2fstr (_, _, _, f, Inc ((d, ts), _)) = (f, comp_dts'' (d,ts))
252 | itms2fstr (_, _, _, f, Sup (d, ts)) = (f, comp_dts'' (d, ts))
253 | itms2fstr (_, _, _, f, Mis (d, t)) = (f, term2str (d $ t))
254 | itms2fstr (itm as (_, _, _, _, Par _)) =
255 error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") 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, Pbl, spec as (dI,pI,mI)):icalhd) =
267 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
268 spec = sspec as (sdI,spI,smI), probl, meth, ...} = get_obj I pt p;
269 in if is_casinput hdf fmz then the (cas_input (str2term hdf))
270 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
271 let val (pos_, pits, mits) =
273 then let val its = map (parsitm (assoc_thy dI)) probl;
274 val (its, trms) = filter_sep is_Par its;
275 val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
276 in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
278 then if pI = snd3 ospec then (Pbl, probl, meth)
280 let val pbt = (#ppc o get_pbt) pI
281 val dI' = #1 (some_spec ospec spec)
282 val oris = if pI = #2 ospec then oris
283 else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
284 in (Pbl, appl_adds dI' oris probl pbt
285 (map itms2fstr probl), meth) end
286 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
287 then let val met = (#ppc o get_met) mI
288 val mits = complete_metitms oris probl meth met
289 in if foldl and_ (true, map #3 mits)
290 then (Pbl, probl, mits) else (Met, probl, mits)
292 else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
293 ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
294 (imodel2fstr imodel), meth);
295 val pt = update_spec pt p spec;
297 then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
298 val pre =check_preconds(assoc_thy"Isac")prls where_ pits
299 in (update_pbl pt p pits,
300 (ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
302 else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
303 val pre = check_preconds (assoc_thy"Isac") prls pre mits
304 in (update_met pt p mits,
305 (ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec):ocalhd)
309 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
310 error "input_icalhd Met not impl.";
313 (***. handle an input formula .***)
315 Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
316 Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
317 wenn Abteilungen nur auf gleichem Level gesucht werden ?
320 Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
322 ------------------------------------------------------------------------------
323 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
324 ------------------------------------------------------------------------------
325 1. "5 * x / (x - 2) - x / (x + 2) = 4"
327 4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
329 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
331 4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
334 ------------------------------------------------------------------------------
335 (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
337 (4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
338 ------------------------------------------------------------------------------
341 ------------------------------------------------------------------------------
342 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
343 ------------------------------------------------------------------------------
344 1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
346 4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
347 Subproblem["normalize", "polynomial", "univariate"..
349 4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
351 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
352 4.4.5. "[x = 0, x = 6 / 5]"
354 5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
356 ------------------------------------------------------------------------------
357 (1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
359 (4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
360 ------------------------------------------------------------------------------
363 ------------------------------------------------------------------------------
364 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
365 ------------------------------------------------------------------------------
366 1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
368 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
369 Subproblem["sq", "root'", "univariate", "equation"]
371 6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
372 Subproblem["normalize", "polynomial", "univariate", "equation"]
374 6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
376 6.6.3.2 "UniversalList"
377 ------------------------------------------------------------------------------
378 (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
380 (6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
381 ------------------------------------------------------------------------------
383 (*sh. comments auf 498*)
387 (*the lists contain eq-al elem-pairs at the beginning;
388 return first list reverted (again) - ie. in order as required subsequently*)
389 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
391 if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is)
392 else (rev (f1::f2::fs), i1::i2::is)
393 else error "dropwhile': did not start with equal elements"
394 | dropwhile' equal (f::fs) [i] =
395 if equal f i then (rev (f::fs), [i])
396 else error "dropwhile': did not start with equal elements"
397 | dropwhile' equal [f] (i::is) =
398 if equal f i then ([f], i::is)
399 else error "dropwhile': did not start with equal elements";
402 val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
403 val r_foder = rev foder; val r_ifoder = rev ifoder;
404 dropwhile' equal r_foder r_ifoder;
405 > vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
407 val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
408 val r_foder = rev foder; val r_ifoder = rev ifoder;
409 dropwhile' equal r_foder r_ifoder;
410 > val it = ([3], [3, 12, 11]) : int list * int list
412 val foder = [5]; val ifoder = [11,12,3,4,5];
413 val r_foder = rev foder; val r_ifoder = rev ifoder;
414 dropwhile' equal r_foder r_ifoder;
415 > val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
417 val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
418 val r_foder = rev foder; val r_ifoder = rev ifoder;
419 dropwhile' equal r_foder r_ifoder;
420 > *** dropwhile': did not start with equal elements*)
422 (*040214: version for concat_deriv*)
423 fun rev_deriv' (t, r, (t', a)) = (t', sym_rule r, (t, a));
425 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
427 Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
428 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
429 | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
430 (Rewrite_Set (Lucin.rule2rls' r),
431 Rewrite_Set' ("Isac", false, rls, t, (t', a)),
432 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
433 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t);
435 (*fo = ifo excluded already in inform*)
436 fun concat_deriv rew_ord erls rules fo ifo =
438 fun derivat ([]:(term * rule * (term * term list)) list) = e_term
439 | derivat dt = (#1 o #3 o last_elem) dt
440 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
441 val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
442 val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
445 ([], []) => if fo = ifo then (true, []) else (false, [])
446 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
447 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
449 if derivat fod = derivat ifod (*common normal form found*)
452 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
453 in (true, fod' @ (map rev_deriv' rifod')) end
457 val ({rew_ord, erls, rules,...}, fo, ifo) =
458 (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
459 (tracing o trtas2str) fod';
461 (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
462 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
463 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
464 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
466 (tracing o trtas2str) (map rev_deriv' rifod');
468 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
469 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
470 (-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
475 (* compare inform with ctree.form at current pos by nrls;
476 if found, embed the derivation generated during comparison
477 if not, let the mat-engine compute the next ctree.form *)
478 (*structure copied from complete_solve
479 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
480 all_modspec etc. has to be inserted at Subproblem'*)
481 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
485 Frm => get_obj g_form pt p
486 | Res => (fst o (get_obj g_result pt)) p
487 | _ => e_term (*on PblObj is fo <> ifo*);
488 val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p))
489 val {rew_ord, erls, rules, ...} = rep_rls nrls
490 val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
495 val tacis' = map (mk_tacis rew_ord erls) der;
496 val (c', ptp) = embed_deriv tacis' ptp;
497 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
499 if pos = ([], Res) (*TODO: we should stop earlier with trying subproblems *)
500 then ("no derivation found", (tacis, c, ptp): calcstate')
503 val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*)
504 val cs' as (tacis, c'', ptp) =
506 ((Subproblem _, _, _)::_) =>
508 val ptp as (pt, (p,_)) = all_modspec ptp (*<------------------*)
509 val mI = get_obj g_metID pt p
511 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
514 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
517 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *)
518 fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls =
520 val (res', _, _, rewritten) =
521 rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res;
526 val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of
528 | SOME (norm_res, _) => norm_res
529 val norm_inf = case rewrite_set_inst_ (Isac()) false subst rls inf of
531 | SOME (norm_inf, _) => norm_inf
532 in if norm_res = norm_inf then SOME errpatID else NONE
537 (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
538 (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
539 fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
541 val (_, subst) = get_bdv_subst prog env
542 fun scan (_, [], _) = NONE
543 | scan (errpatID, errpat :: errpats, _) =
544 case check_err_patt (res, inf) (subst: subst) (errpatID, errpat) rls of
545 NONE => scan (errpatID, errpats, [])
546 | SOME errpatID => SOME errpatID
548 | scans (group :: groups) =
551 | SOME errpatID => SOME errpatID
552 in scans errpats end;
554 (*.handle a user-input formula, which may be a CAS-command, too.
556 create a calchead, and do 1 step
557 TOOODO.WN0602 works only for the root-problem !!!
558 formula, which is no CAS-command:
559 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
560 collect all the tacs applied by the way;
561 if "no derivation found" then check_error_patterns.
562 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*)
563 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
564 case parse (assoc_thy "Isac") istr of
567 val f_in = Thm.term_of f_in
568 val f_succ = get_curr_formula (pt, pos);
571 then ("same-formula", cs) (* ctree not cut with replaceFormula *)
573 case cas_input f_in of
574 SOME (pt, _) => ("ok",([], [], (pt, (p, Met))))
577 val pos_pred = lev_back' pos
578 (* f_pred ---"step pos cs"---> f_succ in appendFormula *)
579 val f_pred = get_curr_formula (pt, pos_pred)
580 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*)
581 (*last step re-calc in compare_step TODO before WN09*)
583 case msg_calcstate' of
584 ("no derivation found", calcstate') =>
586 val pp = par_pblobj pt p
587 val {errpats, nrls, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
588 val ScrState (env, _, _, _, _, _) = get_istate pt pos
590 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
591 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
592 | NONE => msg_calcstate'
594 | _ => msg_calcstate'
597 | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate');
599 (* fill-in patterns an forms.
600 returns thm required by "fun in_fillform *)
601 fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) =
603 val (form', _, _, rewritten) =
604 rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form;
605 in (*the fillpat of the thm must be dedicated to errpatID*)
606 if errpatID = erpaID andalso rewritten
607 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) else NONE end;
609 fun get_fillpats subst form errpatID thm =
611 val thmDeriv = Thm.get_name_hint thm
612 val (part, thyID) = thy_containing_thm thmDeriv
613 val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
614 val Hthm {fillpats, ...} = get_the theID
615 val some = map (get_fillform subst (thm, form) errpatID) fillpats
616 in some |> filter is_some |> map the end;
618 fun find_fillpatterns (pt, pos as (p, _): pos') errpatID =
620 val f_curr = get_curr_formula (pt, pos);
621 val pp = par_pblobj pt p
622 val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
623 val ScrState (env, _, _, _, _, _) = get_istate pt pos
624 val subst = get_bdv_subst prog env
625 val errpatthms = errpats
626 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
627 |> map (#3: errpat -> thm list)
629 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end;
631 (* check if an input formula is exactly equal the rewrite from a rule
632 which is stored at the pos where the input is stored of "ok". *)
633 fun is_exactly_equal (pt, pos as (p, _)) istr =
634 case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of
635 NONE => ("syntax error in '" ^ istr ^ "'", Tac "")
639 val tac = get_obj g_tac pt p';
641 case applicable_in pos pt tac of
642 Notappl msg => (msg, Tac "")
645 val res = case rew of
646 Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
647 | Rewrite' (_, _, _, _, _, _, (res, _)) => res
650 then ("input does not exactly fill the gaps", Tac "")
655 (* fetch errpatIDs from an arbitrary tactic *)
656 fun fetchErrorpatterns tac =
660 Rewrite_Set rlsID => rlsID
661 | Rewrite_Set_Inst (_, rlsID) => rlsID
663 val (part, thyID) = thy_containing_rls "Isac" rlsID;
664 val Hrls {thy_rls = (_, rls), ...} = get_the [part, thyID, "Rulesets", rlsID]
666 Rls {errpatts, ...} => errpatts
667 | Seq {errpatts, ...} => errpatts
668 | Rrls {errpatts, ...} => errpatts