neuper@37906: (* Handle user-input during the specify- and the solve-phase. neuper@37906: author: Walther Neuper neuper@37906: 0603 neuper@37906: (c) due to copyright terms neuper@37906: *) neuper@37906: wneuper@59262: signature INPUT_FORMULAS = wneuper@59262: sig wneuper@59416: datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list wneuper@59262: type imodel = iitem list wneuper@59416: type icalhd = Ctree.pos' * Rule.cterm' * imodel * Ctree.pos_ * Celem.spec wneuper@59571: val fetchErrorpatterns : Tactic.input -> Rule.errpatID list wneuper@59279: val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd wneuper@59416: val find_fillpatterns : Ctree.state -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list wneuper@59571: val is_exactly_equal : Ctree.state -> string -> string * Tactic.input wneuper@59555: (*cp here from "! aktivate for Test_Isac" below due to LucinNEW*) wneuper@59555: val concat_deriv : 'a * ((term * term) list -> term * term -> bool) -> wneuper@59555: Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list wneuper@59572: 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)) wneuper@59556: val check_error_patterns : wneuper@59556: term * term -> wneuper@59556: term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule.rls -> Rule.errpatID option wneuper@59556: val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option wneuper@59555: wneuper@59310: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) wneuper@59310: (* NONE *) walther@59702: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59262: val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list wneuper@59416: val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c) wneuper@59416: val check_err_patt : term * term -> Rule.subst -> Rule.errpatID * term -> Rule.rls -> Rule.errpatID option wneuper@59262: val get_fillform : wneuper@59416: 'a * (term * term) list -> 'b * term -> Rule.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option wneuper@59262: val get_fillpats : wneuper@59416: 'a * (term * term) list -> term -> Rule.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list walther@59702: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59310: wneuper@59310: (*----- unused code, kept as hints to design ideas ---------------------------------------------*) wneuper@59313: val e_icalhd : icalhd wneuper@59313: val oris2itms : 'a -> ''b list -> ('c * ''b * 'd * term * term list) list -> wneuper@59316: ('c * ''b * bool * 'd * Model.itm_) list wneuper@59262: end neuper@37906: wneuper@59557: structure Inform(**): INPUT_FORMULAS(**) = wneuper@59262: struct neuper@37906: wneuper@59262: (*** handle an input calc-head ***) neuper@37906: neuper@37906: datatype iitem = wneuper@59416: Given of Rule.cterm' list neuper@37906: (*Where is never input*) wneuper@59416: | Find of Rule.cterm' list wneuper@59416: | Relate of Rule.cterm' list neuper@37906: wneuper@59262: type imodel = iitem list neuper@37906: neuper@37906: (*calc-head as input*) neuper@37906: type icalhd = wneuper@59276: Ctree.pos' * (*the position of the calc-head in the calc-tree*) wneuper@59416: Rule.cterm' * (*the headline*) wneuper@59405: imodel * (*the model (without Find) of the calc-head*) wneuper@59276: Ctree.pos_ * (*model belongs to Pbl or Met*) wneuper@59405: Celem.spec; (*specification: domID, pblID, metID*) walther@59694: val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec) neuper@37906: wneuper@59416: fun is_casinput (hdf : Rule.cterm') ((fmz_, spec) : Selem.fmz) = wneuper@59405: hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec neuper@37906: neuper@37906: (*.handle an input as into an algebra system.*) neuper@37906: fun dtss2itm_ ppc (d, ts) = wneuper@59264: let wneuper@59264: val (f, (d, id)) = the (find_first ((curry op= d) o wneuper@59264: (#1: (term * term) -> term) o wneuper@59405: (#2: Celem.pbt_ -> (term * term))) ppc) wneuper@59264: in wneuper@59316: ([1], true, f, Model.Cor ((d, ts), (id, ts))) wneuper@59264: end neuper@37906: wneuper@59262: fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e) neuper@37906: wneuper@59405: fun cas_input_ ((dI, pI, mI): Celem.spec) dtss = (*WN110515 reconsider thy..ctxt*) neuper@41995: let wneuper@59405: val thy = Celem.assoc_thy dI wneuper@59269: val {ppc, ...} = Specify.get_pbt pI neuper@41995: val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) wneuper@59269: val its = Specify.add_id its_ neuper@41995: val pits = map flattup2 its neuper@41995: val (pI, mI) = neuper@41995: if mI <> ["no_met"] neuper@41995: then (pI, mI) neuper@41995: else wneuper@59269: case Specify.refine_pbl thy pI pits of wneuper@59269: SOME (pI,_) => (pI, (hd o #met o Specify.get_pbt) pI) wneuper@59269: | NONE => (pI, (hd o #met o Specify.get_pbt) pI) wneuper@59269: val {ppc, pre, prls, ...} = Specify.get_met mI neuper@41995: val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) wneuper@59269: val its = Specify.add_id its_ neuper@41995: val mits = map flattup2 its wneuper@59308: val pre = Stool.check_preconds thy prls pre mits walther@59722: val ctxt = Proof_Context.init_global thy wneuper@59308: in (pI, pits, mI, mits, pre, ctxt) end; neuper@37906: neuper@37906: wneuper@59279: (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *) neuper@37906: fun cas_input hdt = wneuper@59262: let wneuper@59262: val (h, argl) = strip_comb hdt neuper@41995: in wneuper@59592: case assoc_cas (Celem.assoc_thy "Isac_Knowledge") h of wneuper@59262: NONE => NONE wneuper@59262: | SOME (spec as (dI,_,_), argl2dtss) => neuper@41995: let neuper@41995: val dtss = argl2dtss argl neuper@41995: val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss neuper@41995: val spec = (dI, pI, mI) neuper@41995: val (pt,_) = wneuper@59581: Ctree.cappend_problem Ctree.e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], Celem.e_spec) ([], Celem.e_spec, hdt) wneuper@59276: val pt = Ctree.update_spec pt [] spec wneuper@59276: val pt = Ctree.update_pbl pt [] pits wneuper@59276: val pt = Ctree.update_met pt [] mits wneuper@59276: val pt = Ctree.update_ctxt pt [] ctxt wneuper@59262: in walther@59694: SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Ctree.ocalhd) wneuper@59262: end wneuper@59262: end neuper@37906: wneuper@59592: (*lazy evaluation for (Thy_Info_get_theory "Isac_Knowledge")*) wneuper@59592: fun Isac _ = Celem.assoc_thy "Isac_Knowledge"; neuper@37906: wneuper@59262: (* re-parse itms with a new thy and prepare for checking with ori list *) wneuper@59316: fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) = wneuper@59316: (let val t = Model.comp_dts (d, ts) wneuper@59416: val _ = (Rule.term_to_string''' dI t) wneuper@59262: (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *) neuper@52070: in itm end wneuper@59416: handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*)))) wneuper@59316: | parsitm dI (i, v, b, f, Model.Syn str) = wneuper@59389: (let val _ = (Thm.term_of o the o (TermC.parse dI)) str wneuper@59316: in (i, v, b ,f, Model.Par str) end wneuper@59316: handle _ => (i, v, b, f, Model.Syn str)) wneuper@59316: | parsitm dI (i, v, b, f, Model.Typ str) = wneuper@59389: (let val _ = (Thm.term_of o the o (TermC.parse dI)) str wneuper@59316: in (i, v, b, f, Model.Par str) end wneuper@59316: handle _ => (i, v, b, f, Model.Syn str)) wneuper@59316: | parsitm dI (itm as (i, v, _, f, Model.Inc ((d, ts), _))) = wneuper@59316: (let val t = Model.comp_dts (d,ts); wneuper@59416: val _ = Rule.term_to_string''' dI t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@52070: in itm end wneuper@59416: handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*)))) wneuper@59316: | parsitm dI (itm as (i, v, _, f, Model.Sup (d, ts))) = wneuper@59316: (let val t = Model.comp_dts (d,ts); wneuper@59416: val _ = Rule.term_to_string''' dI t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@52070: in itm end wneuper@59416: handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*)))) wneuper@59316: | parsitm dI (itm as (i, v, _, f, Model.Mis (d, t'))) = neuper@37906: (let val t = d $ t'; wneuper@59416: val _ = Rule.term_to_string''' dI t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@52070: in itm end wneuper@59416: handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*)))) wneuper@59316: | parsitm dI (itm as (_, _, _, _, Model.Par _)) = wneuper@59416: error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt dI) itm ^ "): Par should be internal"); neuper@37906: neuper@37906: (*separate a list to a pair of elements that do NOT satisfy the predicate, neuper@37906: and of elements that satisfy the predicate, i.e. (false, true)*) neuper@37906: fun filter_sep pred xs = wneuper@59262: let wneuper@59262: fun filt ab [] = ab wneuper@59262: | filt (a, b) (x :: xs) = wneuper@59262: if pred x wneuper@59262: then filt (a, b @ [x]) xs wneuper@59262: else filt (a @ [x], b) xs wneuper@59262: in filt ([], []) xs end; wneuper@59316: fun is_Par (_, _, _, _, Model.Par _) = true neuper@37906: | is_Par _ = false; neuper@37906: neuper@37906: fun is_e_ts [] = true neuper@37906: | is_e_ts [Const ("List.list.Nil", _)] = true neuper@37906: | is_e_ts _ = false; neuper@37906: wneuper@59262: (* WN.9.11.03 copied from fun appl_add *) neuper@37906: fun appl_add' dI oris ppc pbt (sel, ct) = wneuper@59262: let wneuper@59416: val ctxt = Celem.assoc_thy dI |> Rule.thy2ctxt; wneuper@59262: in wneuper@59389: case TermC.parseNEW ctxt ct of wneuper@59316: NONE => (0, [], false, sel, Model.Syn ct) wneuper@59262: | SOME t => wneuper@59265: (case Chead.is_known ctxt sel oris t of wneuper@59262: ("", ori', all) => wneuper@59265: (case Chead.is_notyet_input ctxt ppc all ori' pbt of wneuper@59262: ("",itm) => itm wneuper@59262: | (msg,_) => error ("appl_add': " ^ msg)) wneuper@59262: | (_, (i, v, _, d, ts), _) => wneuper@59262: if is_e_ts ts wneuper@59416: then (i, v, false, sel, Model.Inc ((d, ts), (Rule.e_term, []))) wneuper@59316: else (i, v, false, sel, Model.Sup (d, ts))) wneuper@59262: end neuper@37906: wneuper@59262: (* generate preliminary itm_ from a strin (with field "#Given" etc.) *) wneuper@59262: fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d'; neuper@37906: fun fstr2itm_ thy pbt (f, str) = wneuper@59262: let wneuper@59389: val topt = TermC.parse thy str wneuper@59262: in wneuper@59262: case topt of wneuper@59316: NONE => ([], false, f, Model.Syn str) wneuper@59262: | SOME ct => wneuper@59262: let wneuper@59316: val (d, ts) = (Model.split_dts o Thm.term_of) ct wneuper@59262: val popt = find_first (eq7 (f, d)) pbt wneuper@59262: in wneuper@59262: case popt of wneuper@59316: NONE => ([1](*??*), true(*??*), f, Model.Sup (d, ts)) wneuper@59316: | SOME (f, (d, id)) => ([1], true, f, Model.Cor ((d, ts), (id, ts))) wneuper@59262: end wneuper@59262: end neuper@37906: neuper@37906: (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) neuper@37906: fun unknown_expl dI pbt selcts = neuper@37906: let wneuper@59405: val thy = Celem.assoc_thy dI neuper@37906: val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) wneuper@59269: val its = Specify.add_id its_ wneuper@59308: in map flattup2 its end neuper@37906: wneuper@59262: (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation wneuper@59262: appl_add': generate 1 item wneuper@59262: appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..) wneuper@59262: appl_add' . is_notyet_input: compare with items in model already input wneuper@59262: insert_ppc': insert this 1 item*) wneuper@59262: fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts wneuper@59262: (*already present itms in model are being overwritten*) wneuper@59262: | appl_adds _ _ ppc _ [] = ppc wneuper@59262: | appl_adds dI oris ppc pbt (selct :: ss) = wneuper@59262: let val itm = appl_add' dI oris ppc pbt selct; wneuper@59265: in appl_adds dI oris (Chead.insert_ppc' itm ppc) pbt ss end neuper@37906: wneuper@59308: fun oris2itms _ _ [] = [] (* WN161130: similar in ptyps ?!? *) wneuper@59308: | oris2itms pbt vat ((i, v, f, d, ts) :: os) = neuper@37930: if member op = vat v wneuper@59416: then (i, v, true, f, Model.Cor ((d, ts), (Rule.e_term, []))) :: (oris2itms pbt vat os) wneuper@59262: else oris2itms pbt vat os neuper@37906: wneuper@59316: fun par2fstr (_, _, _, f, Model.Par s) = (f, s) wneuper@59592: | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm) wneuper@59316: fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts)) wneuper@59316: | itms2fstr (_, _, _, f, Model.Syn str) = (f, str) wneuper@59316: | itms2fstr (_, _, _, f, Model.Typ str) = (f, str) wneuper@59316: | itms2fstr (_, _, _, f, Model.Inc ((d, ts), _)) = (f, Model.comp_dts'' (d,ts)) wneuper@59316: | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts)) wneuper@59416: | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Rule.term2str (d $ t)) wneuper@59316: | itms2fstr (itm as (_, _, _, _, Model.Par _)) = wneuper@59592: error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal"); neuper@37906: neuper@37906: fun imodel2fstr iitems = neuper@41976: let neuper@41976: fun xxx is [] = is neuper@41976: | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis neuper@41976: | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis neuper@41976: | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis neuper@41976: in xxx [] iitems end; neuper@37906: neuper@41976: (* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *) walther@59694: fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) = wneuper@59264: let wneuper@59276: val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), wneuper@59264: spec = sspec as (sdI, spI, smI), probl, meth, ...} wneuper@59264: => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) wneuper@59264: | _ => error "input_icalhd: uncovered case of get_obj I pt p" wneuper@59389: in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf)) neuper@37906: else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) neuper@41976: let val (pos_, pits, mits) = neuper@41976: if dI <> sdI wneuper@59405: then let val its = map (parsitm (Celem.assoc_thy dI)) probl; neuper@41976: val (its, trms) = filter_sep is_Par its; wneuper@59269: val pbt = (#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec sspec)) walther@59694: in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end wneuper@59264: else wneuper@59264: if pI <> spI walther@59694: then if pI = snd3 ospec then (Pos.Pbl, probl, meth) wneuper@59264: else wneuper@59269: let val pbt = (#ppc o Specify.get_pbt) pI wneuper@59265: val dI' = #1 (Chead.some_spec ospec spec) wneuper@59264: val oris = if pI = #2 ospec then oris wneuper@59592: else Specify.prep_ori fmz_(Celem.assoc_thy"Isac_Knowledge") pbt |> #1; walther@59694: in (Pos.Pbl, appl_adds dI' oris probl pbt wneuper@59264: (map itms2fstr probl), meth) end wneuper@59264: else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) wneuper@59269: then let val met = (#ppc o Specify.get_met) mI wneuper@59265: val mits = Chead.complete_metitms oris probl meth met wneuper@59264: in if foldl and_ (true, map #3 mits) walther@59694: then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) wneuper@59264: end walther@59694: else (Pos.Pbl, appl_adds (#1 (Chead.some_spec ospec spec)) oris [(*!!!*)] wneuper@59269: ((#ppc o Specify.get_pbt) (#2 (Chead.some_spec ospec spec))) wneuper@59264: (imodel2fstr imodel), meth) wneuper@59276: val pt = Ctree.update_spec pt p spec; walther@59694: in if pos_ = Pos.Pbl wneuper@59269: then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec)) wneuper@59592: val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls where_ pits wneuper@59276: in (Ctree.update_pbl pt p pits, walther@59694: (Chead.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Ctree.ocalhd) neuper@41976: end wneuper@59269: else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec)) wneuper@59592: val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls pre mits wneuper@59276: in (Ctree.update_met pt p mits, walther@59694: (Chead.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Ctree.ocalhd) neuper@41976: end neuper@41976: end neuper@41976: end wneuper@59264: | input_icalhd _ (_, _, _, _(*Met*), _) = error "input_icalhd Met not impl." neuper@37906: neuper@37906: neuper@37906: (***. handle an input formula .***) neuper@37906: neuper@37906: (*the lists contain eq-al elem-pairs at the beginning; neuper@37906: return first list reverted (again) - ie. in order as required subsequently*) neuper@37906: fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = wneuper@59264: if equal f1 i1 wneuper@59264: then wneuper@59264: if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is) wneuper@59264: else (rev (f1 :: f2 :: fs), i1 :: i2 :: is) neuper@38031: else error "dropwhile': did not start with equal elements" neuper@37906: | dropwhile' equal (f::fs) [i] = wneuper@59264: if equal f i wneuper@59264: then (rev (f::fs), [i]) neuper@38031: else error "dropwhile': did not start with equal elements" neuper@37906: | dropwhile' equal [f] (i::is) = wneuper@59264: if equal f i wneuper@59264: then ([f], i::is) wneuper@59264: else error "dropwhile': did not start with equal elements" wneuper@59264: | dropwhile' _ _ _ = error "dropwhile': uncovered case" neuper@37906: wneuper@59264: (* 040214: version for concat_deriv *) wneuper@59263: fun rev_deriv' (t, r, (t', a)) = (t', Rtools.sym_rule r, (t, a)); neuper@37906: wneuper@59416: fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) = wneuper@59571: (Tactic.Rewrite (id, thm), wneuper@59592: Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)), walther@59694: (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt))) wneuper@59416: | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) = wneuper@59571: (Tactic.Rewrite_Set (Lucin.rule2rls' r), wneuper@59592: Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)), walther@59694: (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt))) wneuper@59416: | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t) neuper@37906: wneuper@59264: (* fo = ifo excluded already in inform *) neuper@37906: fun concat_deriv rew_ord erls rules fo ifo = neuper@55487: let wneuper@59416: fun derivat ([]:(term * Rule.rule * (term * term list)) list) = Rule.e_term neuper@55487: | derivat dt = (#1 o #3 o last_elem) dt neuper@55487: fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2 wneuper@59263: val fod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE fo wneuper@59263: val ifod = Rtools.make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo neuper@55487: in neuper@55487: case (fod, ifod) of neuper@55487: ([], []) => if fo = ifo then (true, []) else (false, []) neuper@55487: | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) neuper@55487: | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) neuper@55487: | (fod, ifod) => neuper@55487: if derivat fod = derivat ifod (*common normal form found*) neuper@55487: then neuper@55487: let neuper@55487: val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod) neuper@55487: in (true, fod' @ (map rev_deriv' rifod')) end neuper@55487: else (false, []) wneuper@59264: end neuper@37906: neuper@42428: (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *) wneuper@59405: fun check_err_patt (res, inf) subst (errpatID, pat) rls = neuper@42423: let neuper@42423: val (res', _, _, rewritten) = wneuper@59416: Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res; neuper@42423: in neuper@42423: if rewritten neuper@42423: then neuper@42423: let wneuper@59380: val norm_res = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls res' of neuper@42423: NONE => res' neuper@42423: | SOME (norm_res, _) => norm_res wneuper@59380: val norm_inf = case Rewrite.rewrite_set_inst_ (Isac()) false subst rls inf of neuper@42423: NONE => inf neuper@42423: | SOME (norm_inf, _) => norm_inf neuper@42423: in if norm_res = norm_inf then SOME errpatID else NONE neuper@42423: end neuper@42423: else NONE neuper@42423: end; neuper@42423: neuper@42428: (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls; neuper@42428: (prog, env) for retrieval of casual substitution for bdv in the pattern. *) neuper@42428: fun check_error_patterns (res, inf) (prog, env) (errpats, rls) = neuper@42428: let wneuper@59263: val (_, subst) = Rtools.get_bdv_subst prog env neuper@42428: fun scan (_, [], _) = NONE neuper@42428: | scan (errpatID, errpat :: errpats, _) = wneuper@59405: case check_err_patt (res, inf) subst (errpatID, errpat) rls of neuper@42428: NONE => scan (errpatID, errpats, []) neuper@42428: | SOME errpatID => SOME errpatID neuper@42428: fun scans [] = NONE neuper@42428: | scans (group :: groups) = neuper@42428: case scan group of neuper@42428: NONE => scans groups neuper@42428: | SOME errpatID => SOME errpatID neuper@42428: in scans errpats end; neuper@42428: neuper@42433: (* fill-in patterns an forms. neuper@42433: returns thm required by "fun in_fillform *) wneuper@59405: fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) = neuper@42430: let neuper@42430: val (form', _, _, rewritten) = wneuper@59416: Rewrite.rew_sub (Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form; neuper@42430: in (*the fillpat of the thm must be dedicated to errpatID*) neuper@42430: if errpatID = erpaID andalso rewritten wneuper@59264: then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) wneuper@59264: else NONE wneuper@59264: end neuper@42430: neuper@42430: fun get_fillpats subst form errpatID thm = wneuper@59264: let wneuper@59264: val thmDeriv = Thm.get_name_hint thm wneuper@59264: val (part, thyID) = Rtools.thy_containing_thm thmDeriv wneuper@59405: val theID = [part, thyID, "Theorems", Celem.thmID_of_derivation_name thmDeriv] wneuper@59269: val fillpats = case Specify.get_the theID of wneuper@59405: Celem.Hthm {fillpats, ...} => fillpats wneuper@59264: | _ => error "get_fillpats: uncovered case of get_the" wneuper@59264: val some = map (get_fillform subst (thm, form) errpatID) fillpats wneuper@59264: in some |> filter is_some |> map the end neuper@42430: wneuper@59276: fun find_fillpatterns (pt, pos as (p, _): Ctree.pos') errpatID = neuper@42430: let wneuper@59276: val f_curr = Ctree.get_curr_formula (pt, pos); wneuper@59276: val pp = Ctree.par_pblobj pt p wneuper@59276: val (errpats, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of wneuper@59416: {errpats, scr = Rule.Prog prog, ...} => (errpats, prog) wneuper@59264: | _ => error "find_fillpatterns: uncovered case of get_met" walther@59685: val {env, ...} = Ctree.get_istate pt pos |> Istate.the_pstate wneuper@59263: val subst = Rtools.get_bdv_subst prog env neuper@42430: val errpatthms = errpats wneuper@59416: |> filter ((curry op = errpatID) o (#1: Rule.errpat -> Rule.errpatID)) wneuper@59416: |> map (#3: Rule.errpat -> thm list) neuper@42430: |> flat wneuper@59264: in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end neuper@37906: neuper@42437: (* check if an input formula is exactly equal the rewrite from a rule neuper@42437: which is stored at the pos where the input is stored of "ok". *) neuper@42437: fun is_exactly_equal (pt, pos as (p, _)) istr = wneuper@59592: case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of wneuper@59571: NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "") neuper@42437: | SOME ifo => neuper@42437: let walther@59757: val p' = Pos.lev_on p; wneuper@59276: val tac = Ctree.get_obj Ctree.g_tac pt p'; neuper@42437: in wneuper@59272: case Applicable.applicable_in pos pt tac of walther@59735: Applicable.Notappl msg => (msg, Tactic.Tac "") walther@59735: | Applicable.Appl rew => neuper@42437: let neuper@42437: val res = case rew of wneuper@59571: Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res wneuper@59571: |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res walther@59728: | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t) neuper@42437: in neuper@42437: if not (ifo = res) wneuper@59571: then ("input does not exactly fill the gaps", Tactic.Tac "") neuper@42437: else ("ok", tac) neuper@42437: end neuper@42437: end neuper@42437: neuper@42458: (* fetch errpatIDs from an arbitrary tactic *) neuper@42458: fun fetchErrorpatterns tac = neuper@42458: let neuper@42458: val rlsID = neuper@42458: case tac of wneuper@59571: Tactic.Rewrite_Set rlsID => rlsID wneuper@59571: |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID neuper@55415: | _ => "e_rls" wneuper@59592: val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID; wneuper@59269: val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of wneuper@59405: Celem.Hrls {thy_rls = (_, rls), ...} => rls wneuper@59264: | _ => error "fetchErrorpatterns: uncovered case of get_the" neuper@42458: in case rls of wneuper@59416: Rule.Rls {errpatts, ...} => errpatts wneuper@59416: | Rule.Seq {errpatts, ...} => errpatts wneuper@59416: | Rule.Rrls {errpatts, ...} => errpatts wneuper@59416: | Rule.Erls => [] neuper@42458: end wneuper@59264: wneuper@59262: (**) neuper@37906: end wneuper@59262: (**)