131 val _ = (term_to_string''' dI t) |
131 val _ = (term_to_string''' dI t) |
132 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) |
132 (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) |
133 in itm end |
133 in itm end |
134 handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*)))) |
134 handle _ => (i, v, false, f, Model.Syn (term2str e_term (*t ..(t) has not been declared*)))) |
135 | parsitm dI (i, v, b, f, Model.Syn str) = |
135 | parsitm dI (i, v, b, f, Model.Syn str) = |
136 (let val _ = (Thm.term_of o the o (parse dI)) str |
136 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str |
137 in (i, v, b ,f, Model.Par str) end |
137 in (i, v, b ,f, Model.Par str) end |
138 handle _ => (i, v, b, f, Model.Syn str)) |
138 handle _ => (i, v, b, f, Model.Syn str)) |
139 | parsitm dI (i, v, b, f, Model.Typ str) = |
139 | parsitm dI (i, v, b, f, Model.Typ str) = |
140 (let val _ = (Thm.term_of o the o (parse dI)) str |
140 (let val _ = (Thm.term_of o the o (TermC.parse dI)) str |
141 in (i, v, b, f, Model.Par str) end |
141 in (i, v, b, f, Model.Par str) end |
142 handle _ => (i, v, b, f, Model.Syn str)) |
142 handle _ => (i, v, b, f, Model.Syn str)) |
143 | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) = |
143 | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) = |
144 (let val t = Model.comp_dts (d,ts); |
144 (let val t = Model.comp_dts (d,ts); |
145 val _ = term_to_string''' dI t; |
145 val _ = term_to_string''' dI t; |
181 (* WN.9.11.03 copied from fun appl_add *) |
181 (* WN.9.11.03 copied from fun appl_add *) |
182 fun appl_add' dI oris ppc pbt (sel, ct) = |
182 fun appl_add' dI oris ppc pbt (sel, ct) = |
183 let |
183 let |
184 val ctxt = assoc_thy dI |> thy2ctxt; |
184 val ctxt = assoc_thy dI |> thy2ctxt; |
185 in |
185 in |
186 case parseNEW ctxt ct of |
186 case TermC.parseNEW ctxt ct of |
187 NONE => (0, [], false, sel, Model.Syn ct) |
187 NONE => (0, [], false, sel, Model.Syn ct) |
188 | SOME t => |
188 | SOME t => |
189 (case Chead.is_known ctxt sel oris t of |
189 (case Chead.is_known ctxt sel oris t of |
190 ("", ori', all) => |
190 ("", ori', all) => |
191 (case Chead.is_notyet_input ctxt ppc all ori' pbt of |
191 (case Chead.is_notyet_input ctxt ppc all ori' pbt of |
199 |
199 |
200 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *) |
200 (* generate preliminary itm_ from a strin (with field "#Given" etc.) *) |
201 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d'; |
201 fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d'; |
202 fun fstr2itm_ thy pbt (f, str) = |
202 fun fstr2itm_ thy pbt (f, str) = |
203 let |
203 let |
204 val topt = parse thy str |
204 val topt = TermC.parse thy str |
205 in |
205 in |
206 case topt of |
206 case topt of |
207 NONE => ([], false, f, Model.Syn str) |
207 NONE => ([], false, f, Model.Syn str) |
208 | SOME ct => |
208 | SOME ct => |
209 let |
209 let |
267 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of |
267 val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of |
268 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), |
268 Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), |
269 spec = sspec as (sdI, spI, smI), probl, meth, ...} |
269 spec = sspec as (sdI, spI, smI), probl, meth, ...} |
270 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) |
270 => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) |
271 | _ => error "input_icalhd: uncovered case of get_obj I pt p" |
271 | _ => error "input_icalhd: uncovered case of get_obj I pt p" |
272 in if is_casinput hdf fmz then the (cas_input (str2term hdf)) |
272 in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf)) |
273 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) |
273 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) |
274 let val (pos_, pits, mits) = |
274 let val (pos_, pits, mits) = |
275 if dI <> sdI |
275 if dI <> sdI |
276 then let val its = map (parsitm (assoc_thy dI)) probl; |
276 then let val its = map (parsitm (assoc_thy dI)) probl; |
277 val (its, trms) = filter_sep is_Par its; |
277 val (its, trms) = filter_sep is_Par its; |
411 |
411 |
412 (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *) |
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 = |
413 fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls = |
414 let |
414 let |
415 val (res', _, _, rewritten) = |
415 val (res', _, _, rewritten) = |
416 Rewrite.rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res; |
416 Rewrite.rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (TermC.Trueprop $ pat) res; |
417 in |
417 in |
418 if rewritten |
418 if rewritten |
419 then |
419 then |
420 let |
420 let |
421 val norm_res = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls res' of |
421 val norm_res = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls res' of |
454 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos; |
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; |
455 collect all the tacs applied by the way; |
456 if "no derivation found" then check_error_patterns. |
456 if "no derivation found" then check_error_patterns. |
457 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*) |
457 ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*) |
458 fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr = |
458 fun inform (cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr = |
459 case parse (assoc_thy "Isac") istr of |
459 case TermC.parse (assoc_thy "Isac") istr of |
460 SOME f_in => |
460 SOME f_in => |
461 let |
461 let |
462 val f_in = Thm.term_of f_in |
462 val f_in = Thm.term_of f_in |
463 val f_succ = Ctree.get_curr_formula (pt, pos); |
463 val f_succ = Ctree.get_curr_formula (pt, pos); |
464 in |
464 in |
497 (* fill-in patterns an forms. |
497 (* fill-in patterns an forms. |
498 returns thm required by "fun in_fillform *) |
498 returns thm required by "fun in_fillform *) |
499 fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) = |
499 fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) = |
500 let |
500 let |
501 val (form', _, _, rewritten) = |
501 val (form', _, _, rewritten) = |
502 Rewrite.rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form; |
502 Rewrite.rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (TermC.Trueprop $ pat) form; |
503 in (*the fillpat of the thm must be dedicated to errpatID*) |
503 in (*the fillpat of the thm must be dedicated to errpatID*) |
504 if errpatID = erpaID andalso rewritten |
504 if errpatID = erpaID andalso rewritten |
505 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
505 then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) |
506 else NONE |
506 else NONE |
507 end |
507 end |
535 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end |
535 in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end |
536 |
536 |
537 (* check if an input formula is exactly equal the rewrite from a rule |
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". *) |
538 which is stored at the pos where the input is stored of "ok". *) |
539 fun is_exactly_equal (pt, pos as (p, _)) istr = |
539 fun is_exactly_equal (pt, pos as (p, _)) istr = |
540 case parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of |
540 case TermC.parseNEW (assoc_thy "Isac" |> thy2ctxt) istr of |
541 NONE => ("syntax error in '" ^ istr ^ "'", Tac.Tac "") |
541 NONE => ("syntax error in '" ^ istr ^ "'", Tac.Tac "") |
542 | SOME ifo => |
542 | SOME ifo => |
543 let |
543 let |
544 val p' = Ctree.lev_on p; |
544 val p' = Ctree.lev_on p; |
545 val tac = Ctree.get_obj Ctree.g_tac pt p'; |
545 val tac = Ctree.get_obj Ctree.g_tac pt p'; |