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: use"ME/inform.sml"; neuper@37906: use"inform.sml"; neuper@37906: *) neuper@37906: neuper@37906: signature INFORM = neuper@37906: sig neuper@37906: neuper@37906: type castab neuper@37906: type icalhd neuper@37906: neuper@37906: (* type iitem *) neuper@37906: datatype neuper@37906: iitem = neuper@37906: Find of cterm' list neuper@37906: | Given of cterm' list neuper@37906: | Relate of cterm' list neuper@37906: type imodel neuper@37906: val imodel2fstr : iitem list -> (string * cterm') list neuper@37906: neuper@37906: neuper@37931: val Isac : 'a -> theory neuper@37906: val appl_add' : neuper@37906: theory' -> neuper@37906: SpecifyTools.ori list -> neuper@37906: SpecifyTools.itm list -> neuper@37906: ('a * (Term.term * Term.term)) list -> neuper@37906: string * cterm' -> SpecifyTools.itm neuper@37906: (* val appl_adds : neuper@37906: theory' -> neuper@37906: SpecifyTools.ori list -> neuper@37906: SpecifyTools.itm list -> neuper@37906: (string * (Term.term * Term.term)) list -> neuper@37906: (string * string) list -> SpecifyTools.itm list *) neuper@37906: (* val cas_input : string -> ptree * ocalhd *) neuper@37906: (* val cas_input_ : neuper@37906: spec -> neuper@37906: (Term.term * Term.term list) list -> neuper@37906: pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list * neuper@37906: (bool * Term.term) list *) neuper@38007: val castab : castab Unsynchronized.ref neuper@37906: val compare_step : neuper@37906: calcstate' -> Term.term -> string * calcstate' neuper@37906: (* val concat_deriv : neuper@37906: 'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool) neuper@37906: -> neuper@37906: rls -> neuper@37906: rule list -> neuper@37906: Term.term -> neuper@37906: Term.term -> neuper@37906: bool * (Term.term * rule * (Term.term * Term.term list)) list *) neuper@37906: val dropwhile' : (* systest/auto-inform.sml *) neuper@37906: ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list neuper@37906: (* val dtss2itm_ : neuper@37906: pbt_ list -> neuper@37906: Term.term * Term.term list -> neuper@37906: int list * bool * string * SpecifyTools.itm_ *) neuper@37906: (* val e_icalhd : icalhd *) neuper@37906: val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool neuper@37906: val equal : ''a -> ''a -> bool neuper@37906: (* val filter_dsc : neuper@37906: SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *) neuper@37906: (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *) neuper@37906: (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *) neuper@37906: (* val fstr2itm_ : neuper@37931: theory -> neuper@37906: (''a * (Term.term * Term.term)) list -> neuper@37906: ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *) neuper@37906: val inform : neuper@37906: calcstate' -> cterm' -> string * calcstate' neuper@37906: val input_icalhd : ptree -> icalhd -> ptree * ocalhd neuper@37906: (* val is_Par : SpecifyTools.itm -> bool *) neuper@37906: (* val is_casinput : cterm' -> fmz -> bool *) neuper@37906: (* val is_e_ts : Term.term list -> bool *) neuper@37906: (* val itms2fstr : SpecifyTools.itm -> string * string *) neuper@37906: (* val mk_tacis : neuper@37906: rew_ord' * 'a -> neuper@37906: rls -> neuper@37906: Term.term * rule * (Term.term * Term.term list) -> neuper@37906: tac * tac_ * (pos' * istate) *) neuper@37906: val oris2itms : neuper@37906: 'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list neuper@37906: (* val par2fstr : SpecifyTools.itm -> string * cterm' *) neuper@37931: (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *) neuper@37906: val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c) neuper@37906: (* val unknown_expl : neuper@37906: theory' -> neuper@37906: (string * (Term.term * Term.term)) list -> neuper@37906: (string * string) list -> SpecifyTools.itm list *) neuper@37906: end neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (***. handle an input calc-head .***) neuper@37906: neuper@37906: (*------------------------------------------------------------------(**) neuper@37906: structure inform :INFORM = neuper@37906: struct neuper@37906: (**)------------------------------------------------------------------*) neuper@37906: neuper@37906: datatype iitem = neuper@37906: Given of cterm' list neuper@37906: (*Where is never input*) neuper@37906: | Find of cterm' list neuper@37906: | Relate of cterm' list; neuper@37906: neuper@37906: type imodel = iitem list; neuper@37906: neuper@37906: (*calc-head as input*) neuper@37906: type icalhd = neuper@37906: pos' * (*the position of the calc-head in the calc-tree neuper@37906: pos' as (p,p_) where p_ is neglected due to pos_ below*) neuper@37906: cterm' * (*the headline*) neuper@37906: imodel * (*the model (without Find) of the calc-head*) neuper@37906: pos_ * (*model belongs to Pbl or Met*) neuper@37906: spec; (*specification: domID, pblID, metID*) neuper@37906: val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec): icalhd; neuper@37906: neuper@37906: fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) = neuper@37906: hdf <> "" andalso fmz_ = [] andalso spec = e_spec; neuper@37906: neuper@37906: (*.handle an input as into an algebra system.*) neuper@37906: fun dtss2itm_ ppc (d, ts) = neuper@37906: let val (f, (d, id)) = the (find_first ((curry op= d) o neuper@37906: (#1: (term * term) -> term) o neuper@37906: (#2: pbt_ -> (term * term))) ppc) neuper@37906: in ([1], true, f, Cor ((d, ts), (id, ts))) end; neuper@37906: neuper@37906: fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.association list with cas-commands, for generating a complete calc-head.*) neuper@37906: type castab = neuper@37906: (term * (*cas-command, eg. 'solve'*) neuper@37906: (spec * (*theory, problem, method*) neuper@37906: neuper@37906: (*the function generating a kind of formalization*) neuper@37906: (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*) neuper@37906: (term * (*description of an element*) neuper@37906: term list) (*value of the element (always put into a list)*) neuper@37906: list))) (*of elements in the formalization*) neuper@37906: list; (*of cas-entries in the association list*) neuper@37906: neuper@38006: val castab = Unsynchronized.ref ([]: castab); neuper@37906: neuper@37906: neuper@41995: fun cas_input_ ((dI,pI,mI): spec) dtss = (*WN110515 reconsider thy..ctxt*) neuper@41995: let neuper@41995: val thy = assoc_thy dI neuper@41995: val {ppc, ...} = get_pbt pI neuper@41995: val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) neuper@41995: val its = 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 neuper@41995: case refine_pbl thy pI pits of neuper@37926: SOME (pI,_) => (pI, (hd o #met o get_pbt) pI) neuper@37926: | NONE => (pI, (hd o #met o get_pbt) pI) neuper@41995: val {ppc, pre, prls, ...} = get_met mI neuper@41995: val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) neuper@41995: val its = add_id its_ neuper@41995: val mits = map flattup2 its neuper@41995: val pre = check_preconds thy prls pre mits neuper@41995: val ctxt = e_ctxt (*WN110515 cas_input_ DOESNT WORK*) neuper@41995: in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end; neuper@37906: neuper@37906: neuper@41995: (* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *) neuper@37906: fun cas_input hdt = neuper@41995: let val (h,argl) = strip_comb hdt neuper@41995: in neuper@41995: case assoc (!castab, h) of neuper@41995: NONE => NONE neuper@41995: | 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,_) = neuper@41995: cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, hdt) neuper@41995: val pt = update_spec pt [] spec neuper@41995: val pt = update_pbl pt [] pits neuper@41995: val pt = update_met pt [] mits neuper@41995: val pt = update_ctxt pt [] ctxt neuper@41995: in SOME (pt, (true, Met, hdt, mits, pre, spec) : ocalhd) end neuper@41995: end; neuper@37906: neuper@40836: (*lazy evaluation for (Thy_Info.get_theory "Isac")*) neuper@38050: fun Isac _ = assoc_thy "Isac"; neuper@37906: neuper@37906: (*re-parse itms with a new thy and prepare for checking with ori list*) neuper@37906: fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) = neuper@37906: (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl; neuper@37906: *) bonzai@41949: (let val t = comp_dts (d,ts); neuper@38053: val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@37906: in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) neuper@37906: | parsitm dI (itm as (i,v,b,f, Syn str)) = neuper@37906: (let val t = (term_of o the o (parse dI)) str neuper@37906: in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) neuper@37906: | parsitm dI (itm as (i,v,b,f, Typ str)) = neuper@37906: (let val t = (term_of o the o (parse dI)) str neuper@37906: in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) neuper@37906: | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) = bonzai@41949: (let val t = comp_dts (d,ts); neuper@38053: val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@37906: in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) neuper@37906: | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) = bonzai@41949: (let val t = comp_dts (d,ts); neuper@38053: val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@37906: in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) neuper@37906: | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) = neuper@37906: (let val t = d $ t'; neuper@38053: val s = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt dI)) t; neuper@37906: (*this ^ should raise the exn on unability of re-parsing dts*) neuper@37906: in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) neuper@37906: | parsitm dI (itm as (i,v,_,f, Par _)) = neuper@38031: error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^ neuper@37906: "): 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 = neuper@37906: let fun filt ab [] = ab neuper@37906: | filt (a,b) (x :: xs) = if pred x neuper@37906: then filt (a,b@[x]) xs neuper@37906: else filt (a@[x],b) xs neuper@37906: in filt ([],[]) xs end; neuper@37906: fun is_Par ((_,_,_,_,Par _):itm) = 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: neuper@37906: (*WN.9.11.03 copied from fun appl_add (in modspec.sml)*) neuper@37906: (* val (sel,ct) = selct; neuper@37906: val (dI, oris, ppc, pbt, (sel, ct))= neuper@37906: (#1 (some_spec ospec spec), oris, []:itm list, neuper@37906: ((#ppc o get_pbt) (#2 (some_spec ospec spec))), neuper@37906: hd (imodel2fstr imodel)); neuper@37906: *) neuper@37906: fun appl_add' dI oris ppc pbt (sel, ct) = neuper@37906: let bonzai@41951: val ctxt = assoc_thy dI |> thy2ctxt; bonzai@41952: in case parseNEW ctxt ct of neuper@37926: NONE => (0,[],false,sel, Syn ct):itm bonzai@41952: | SOME t => (case is_known ctxt sel oris t of bonzai@41951: ("", ori', all) => bonzai@41951: (case is_notyet_input ctxt ppc all ori' pbt of bonzai@41949: ("",itm) => itm bonzai@41949: | (msg,_) => error ("appl_add': " ^ msg)) bonzai@41949: | (_, (i, v, _, d, ts), _) => if is_e_ts ts then bonzai@41949: (i, v, false, sel, Inc ((d, ts), (e_term, []))) else bonzai@41949: (i, v, false, sel, Sup (d, ts))) neuper@37906: end; neuper@37906: neuper@37906: (*.generate preliminary itm_ from a strin (with field "#Given" etc.).*) neuper@37906: (* val (f, str) = hd selcts; neuper@37906: *) neuper@37906: fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d'; neuper@37906: fun fstr2itm_ thy pbt (f, str) = neuper@37906: let val topt = parse thy str neuper@37906: in case topt of neuper@37926: NONE => ([], false, f, Syn str) neuper@37926: | SOME ct => neuper@37926: (* val SOME ct = parse thy str; neuper@37906: *) bonzai@41949: let val (d,ts) = (split_dts o term_of) ct neuper@37906: val popt = find_first (eq7 (f,d)) pbt neuper@37906: in case popt of neuper@37926: NONE => ([1](*??*), true(*??*), f, Sup (d,ts)) neuper@37926: | SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts))) neuper@37906: end neuper@37906: end; neuper@37906: 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 neuper@37906: val thy = assoc_thy dI neuper@37906: val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) neuper@37906: val its = add_id its_ neuper@37906: in (map flattup2 its): itm list end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation neuper@37906: appl_add': generate 1 item neuper@37906: appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..) neuper@37906: appl_add' . is_notyet_input: compare with items in model already input neuper@37906: insert_ppc': insert this 1 item*) neuper@37906: (* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)], neuper@37906: ((#ppc o get_pbt) (#2 (some_spec ospec spec))), neuper@37906: (imodel2fstr imodel)); neuper@37906: *) neuper@37906: fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts neuper@37906: (*already present itms in model are being overwritten*) neuper@37906: | appl_adds dI oris ppc pbt [] = ppc neuper@37906: | appl_adds dI oris ppc pbt (selct::ss) = neuper@37906: (* val selct = (sel, string_of_cterm ct); neuper@37906: *) neuper@37906: let val itm = appl_add' dI oris ppc pbt selct; neuper@37906: in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end; neuper@37906: (* val (dI, oris, ppc, pbt, selct::ss) = neuper@37906: (dI, pors, probl, ppc, map itms2fstr probl); neuper@37906: ...vvv neuper@37906: *) neuper@37906: (* val (dI, oris, ppc, pbt, (selct::ss))= neuper@37906: (#1 (some_spec ospec spec), oris, []:itm list, neuper@37906: ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); neuper@37906: val iii = appl_adds dI oris ppc pbt (selct::ss); neuper@38015: tracing(itms2str_ thy iii); neuper@37906: neuper@37906: val itm = appl_add' dI oris ppc pbt selct; neuper@37906: val ppc = insert_ppc' itm ppc; neuper@37906: neuper@37906: val _::selct::ss = (selct::ss); neuper@37906: val itm = appl_add' dI oris ppc pbt selct; neuper@37906: val ppc = insert_ppc' itm ppc; neuper@37906: neuper@37906: val _::selct::ss = (selct::ss); neuper@37906: val itm = appl_add' dI oris ppc pbt selct; neuper@37906: val ppc = insert_ppc' itm ppc; neuper@38015: tracing(itms2str_ thy ppc); neuper@37906: neuper@37906: val _::selct::ss = (selct::ss); neuper@37906: val itm = appl_add' dI oris ppc pbt selct; neuper@37906: val ppc = insert_ppc' itm ppc; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: fun oris2itms _ _ ([]:ori list) = ([]:itm list) neuper@37906: | oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) = neuper@37930: if member op = vat v neuper@37906: then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os) neuper@37906: else oris2itms pbt vat os; neuper@37906: neuper@37906: fun filter_dsc oris itm = neuper@37906: filter_out ((curry op= ((d_in o #5) (itm:itm))) o neuper@37906: (#4:ori -> term)) oris; neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun par2fstr ((_,_,_,f, Par s):itm) = (f, s) neuper@38031: | par2fstr itm = error ("par2fstr: called with " ^ neuper@37939: itm2str_ (thy2ctxt' "Isac") itm); neuper@37906: fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts)) neuper@37906: | itms2fstr (_,_,_,f, Syn str) = (f, str) neuper@37906: | itms2fstr (_,_,_,f, Typ str) = (f, str) neuper@37906: | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts)) neuper@37906: | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts)) neuper@37906: | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t)) neuper@37906: | itms2fstr (itm as (_,_,_,f, Par _)) = neuper@38031: error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ neuper@37906: "): 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 *) neuper@37906: fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) = neuper@37906: let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), neuper@41988: spec = sspec as (sdI,spI,smI), probl, meth, ...} = get_obj I pt p; neuper@37906: in if is_casinput hdf fmz then the (cas_input (str2term hdf)) neuper@37906: else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) neuper@41976: let val (pos_, pits, mits) = neuper@41976: if dI <> sdI neuper@41976: then let val its = map (parsitm (assoc_thy dI)) probl; neuper@41976: val (its, trms) = filter_sep is_Par its; neuper@41976: val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec)); neuper@41976: in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end neuper@41976: else if pI <> spI neuper@41976: then if pI = snd3 ospec then (Pbl, probl, meth) neuper@41976: else neuper@41976: let val pbt = (#ppc o get_pbt) pI neuper@41976: val dI' = #1 (some_spec ospec spec) neuper@41976: val oris = if pI = #2 ospec then oris neuper@41976: else prep_ori fmz_(assoc_thy"Isac") pbt |> #1; neuper@41976: in (Pbl, appl_adds dI' oris probl pbt neuper@41976: (map itms2fstr probl), meth) end neuper@41976: else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) neuper@41976: then let val met = (#ppc o get_met) mI neuper@41976: val mits = complete_metitms oris probl meth met neuper@41976: in if foldl and_ (true, map #3 mits) neuper@41976: then (Pbl, probl, mits) else (Met, probl, mits) neuper@41976: end neuper@41976: else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)] neuper@41976: ((#ppc o get_pbt) (#2 (some_spec ospec spec))) neuper@41976: (imodel2fstr imodel), meth); neuper@41976: val pt = update_spec pt p spec; neuper@41976: in if pos_ = Pbl neuper@41976: then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec)) neuper@41976: val pre =check_preconds(assoc_thy"Isac")prls where_ pits neuper@41976: in (update_pbl pt p pits, neuper@41976: (ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd) neuper@41976: end neuper@41976: else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec)) neuper@41976: val pre = check_preconds (assoc_thy"Isac") prls pre mits neuper@41976: in (update_met pt p mits, neuper@41976: (ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec):ocalhd) neuper@41976: end neuper@41976: end neuper@41976: end neuper@37906: | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) = neuper@38031: error "input_icalhd Met not impl."; neuper@37906: neuper@37906: neuper@37906: (***. handle an input formula .***) neuper@37906: (* neuper@37906: Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler: neuper@37906: Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden, neuper@37906: wenn Abteilungen nur auf gleichem Level gesucht werden ? neuper@37906: WN.040216 neuper@37906: neuper@37906: Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml neuper@37906: neuper@37906: ------------------------------------------------------------------------------ neuper@37906: "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)"; neuper@37906: ------------------------------------------------------------------------------ neuper@37906: 1. "5 * x / (x - 2) - x / (x + 2) = 4" neuper@37906: ... neuper@37906: 4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly".. neuper@37906: ... neuper@37906: 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate".. neuper@37906: ... neuper@37906: 4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions" neuper@37906: ... neuper@37906: "[x = -4 / 3]" neuper@37906: ------------------------------------------------------------------------------ neuper@37906: (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n] neuper@37906: neuper@37906: (4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n] neuper@37906: ------------------------------------------------------------------------------ neuper@37906: neuper@37906: neuper@37906: ------------------------------------------------------------------------------ neuper@37906: "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)"; neuper@37906: ------------------------------------------------------------------------------ neuper@37906: 1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x" neuper@37906: ... neuper@37906: 4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))" neuper@37906: Subproblem["normalize", "polynomial", "univariate".. neuper@37906: ... neuper@37906: 4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. neuper@37906: ... neuper@37906: 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" neuper@37906: 4.4.5. "[x = 0, x = 6 / 5]" neuper@37906: ... neuper@37906: 5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" neuper@37906: "[x = 6 / 5]" neuper@37906: ------------------------------------------------------------------------------ neuper@37906: (1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x] neuper@37906: neuper@37906: (4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.] neuper@37906: ------------------------------------------------------------------------------ neuper@37906: neuper@37906: neuper@37906: ------------------------------------------------------------------------------ neuper@37906: "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))"; neuper@37906: ------------------------------------------------------------------------------ neuper@37906: 1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)" neuper@37906: ... neuper@37906: 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x" neuper@37986: Subproblem["sq", "root'", "univariate", "equation"] neuper@37906: ... neuper@37906: 6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2" neuper@37906: Subproblem["normalize", "polynomial", "univariate", "equation"] neuper@37906: ... neuper@37906: 6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"] neuper@37906: ... Or_to_List neuper@37906: 6.6.3.2 "UniversalList" neuper@37906: ------------------------------------------------------------------------------ neuper@37906: (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n] neuper@37906: neuper@37906: (6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n] neuper@37906: ------------------------------------------------------------------------------ neuper@37906: *) neuper@37906: (*sh. comments auf 498*) neuper@37906: neuper@37906: fun equal a b = a=b; 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) = neuper@37906: if equal f1 i1 then neuper@37906: if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is) neuper@37906: 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] = neuper@37906: if equal f i then (rev (f::fs), [i]) neuper@38031: else error "dropwhile': did not start with equal elements" neuper@37906: | dropwhile' equal [f] (i::is) = neuper@37906: if equal f i then ([f], i::is) neuper@38031: else error "dropwhile': did not start with equal elements"; neuper@37906: (* neuper@37906: fun equal a b = a=b; neuper@37906: val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5]; neuper@37906: val r_foder = rev foder; val r_ifoder = rev ifoder; neuper@37906: dropwhile' equal r_foder r_ifoder; neuper@37906: > vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list neuper@37906: neuper@37906: val foder = [3,4,5]; val ifoder = [11,12,3,4,5]; neuper@37906: val r_foder = rev foder; val r_ifoder = rev ifoder; neuper@37906: dropwhile' equal r_foder r_ifoder; neuper@37906: > val it = ([3], [3, 12, 11]) : int list * int list neuper@37906: neuper@37906: val foder = [5]; val ifoder = [11,12,3,4,5]; neuper@37906: val r_foder = rev foder; val r_ifoder = rev ifoder; neuper@37906: dropwhile' equal r_foder r_ifoder; neuper@37906: > val it = ([5], [5, 4, 3, 12, 11]) : int list * int list neuper@37906: neuper@37906: val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5]; neuper@37906: val r_foder = rev foder; val r_ifoder = rev ifoder; neuper@37906: dropwhile' equal r_foder r_ifoder; neuper@37906: > *** dropwhile': did not start with equal elements*) neuper@37906: neuper@37906: (*040214: version for concat_deriv*) neuper@37906: fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a)); neuper@37906: neuper@37906: fun mk_tacis ro erls (t, r as Thm _, (t', a)) = neuper@41995: (Rewrite (rule2thm' r), neuper@41995: Rewrite' ("Isac", fst ro, erls, false, rule2thm' r, t, (t', a)), neuper@41995: (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt))) neuper@37906: | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) = neuper@41995: (Rewrite_Set (rule2rls' r), neuper@41995: Rewrite_Set' ("Isac", false, rls, t, (t', a)), neuper@41995: (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt))); neuper@37906: neuper@37906: (*fo = ifo excluded already in inform*) neuper@37906: fun concat_deriv rew_ord erls rules fo ifo = neuper@37906: let fun derivat ([]:(term * rule * (term * term list)) list) = e_term neuper@37906: | derivat dt = (#1 o #3 o last_elem) dt neuper@37906: fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2 neuper@37926: val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo neuper@37926: val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo neuper@37906: in case (fod, ifod) of neuper@37906: ([], []) => if fo = ifo then (true, []) neuper@37906: else (false, []) neuper@37906: | (fod, []) => if derivat fod = ifo neuper@37906: then (true, fod) (*ifo is normal form*) neuper@37906: else (false, []) neuper@37906: | ([], ifod) => if fo = derivat ifod neuper@37906: then (true, ((map rev_deriv') o rev) ifod) neuper@37906: else (false, []) neuper@37906: | (fod, ifod) => neuper@37906: if derivat fod = derivat ifod (*common normal form found*) neuper@37906: then let val (fod', rifod') = neuper@37906: dropwhile' equal (rev fod) (rev ifod) neuper@37906: in (true, fod' @ (map rev_deriv' rifod')) end neuper@37906: else (false, []) neuper@37906: end; neuper@37906: (* neuper@37906: val ({rew_ord, erls, rules,...}, fo, ifo) = neuper@37906: (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0"); neuper@38015: (tracing o trtas2str) fod'; neuper@37906: > [" neuper@37906: (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))"," neuper@37906: (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))"," neuper@37906: (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))"," neuper@37906: (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] neuper@37906: val it = () : unit neuper@38015: (tracing o trtas2str) (map rev_deriv' rifod'); neuper@37906: > [" neuper@37906: (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))"," neuper@37906: (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))"," neuper@37906: (-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"] neuper@37906: val it = () : unit neuper@37906: *) neuper@37906: neuper@37906: neuper@41995: (* compare inform with ctree.form at current pos by nrls; neuper@37906: if found, embed the derivation generated during comparison neuper@41995: if not, let the mat-engine compute the next ctree.form *) neuper@37906: (*structure copied from complete_solve neuper@37906: CAUTION: tacis in returned calcstate' do NOT construct resulting ptp -- neuper@37906: all_modspec etc. has to be inserted at Subproblem'*) neuper@37906: fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo = neuper@41995: let neuper@41995: val fo = neuper@41995: case p_ of neuper@41995: Frm => get_obj g_form pt p neuper@41995: | Res => (fst o (get_obj g_result pt)) p neuper@41995: | _ => e_term (*on PblObj is fo <> ifo*); neuper@41995: val {nrls, ...} = get_met (get_obj g_metID pt (par_pblobj pt p)) neuper@41995: val {rew_ord, erls, rules, ...} = rep_rls nrls neuper@42423: val (found, der) = concat_deriv rew_ord erls rules fo ifo; (*<---------------*) neuper@41995: in neuper@41995: if found neuper@41995: then neuper@41995: let neuper@41995: val tacis' = map (mk_tacis rew_ord erls) der; neuper@41995: val (c', ptp) = embed_deriv tacis' ptp; neuper@41995: in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end neuper@41995: else neuper@41995: if pos = ([], Res) neuper@41995: then ("no derivation found", (tacis, c, ptp): calcstate') neuper@41995: else neuper@41995: let neuper@42423: val cs' as (tacis, c', ptp) = nxt_solve_ ptp; (*<---------------------*) neuper@41995: val cs' as (tacis, c'', ptp) = neuper@41995: case tacis of neuper@41995: ((Subproblem _, _, _)::_) => neuper@41995: let neuper@41995: val ptp as (pt, (p,_)) = all_modspec ptp neuper@41995: val mI = get_obj g_metID pt p neuper@42423: in neuper@42423: nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp neuper@41995: end neuper@41995: | _ => cs'; neuper@41995: in compare_step (tacis, c @ c' @ c'', ptp) ifo end neuper@41995: end; neuper@37906: neuper@42428: (* check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls *) neuper@42426: fun check_err_patt (res, inf) (subst: subst) (errpatID: errpatID, pat) rls = neuper@42423: let neuper@42423: val (res', _, _, rewritten) = neuper@42426: rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) res; neuper@42423: in neuper@42423: if rewritten neuper@42423: then neuper@42423: let neuper@42426: val norm_res = case rewrite_set_inst_ (Isac()) false subst rls res' of neuper@42423: NONE => res' neuper@42423: | SOME (norm_res, _) => norm_res neuper@42426: val norm_inf = case 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 neuper@42433: val (_, subst) = get_bdv_subst prog env neuper@42428: fun scan (_, [], _) = NONE neuper@42428: | scan (errpatID, errpat :: errpats, _) = neuper@42428: case check_err_patt (res, inf) (subst: 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@37906: (*.handle a user-input formula, which may be a CAS-command, too. neuper@37906: CAS-command: neuper@37906: create a calchead, and do 1 step neuper@37906: TOOODO.WN0602 works only for the root-problem !!! neuper@37906: formula, which is no CAS-command: neuper@37906: compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos; neuper@42423: collect all the tacs applied by the way; neuper@42426: if "no derivation found" then check_error_patterns. neuper@42427: ALTERNATIVE: check_error_patterns _within_ compare_step seems too expensive.*) neuper@37906: fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr = neuper@42423: case parse (assoc_thy "Isac") istr of neuper@42427: SOME f_in => neuper@42423: let neuper@42427: val f_in = term_of f_in neuper@42431: val f_succ = get_curr_formula (pt, pos); neuper@42423: in neuper@42427: if f_succ = f_in neuper@42423: then ("same-formula", cs) (* ctree not cut with replaceFormula *) neuper@42423: else neuper@42427: case cas_input f_in of neuper@42423: SOME (pt, _) => ("ok",([], [], (pt, (p, Met)))) neuper@42423: | NONE => neuper@42428: let neuper@42428: val pos_pred = lev_back' pos neuper@42428: (* f_pred ---"step pos cs"---> f_succ in appendFormula *) neuper@42431: val f_pred = get_curr_formula (pt, pos_pred) neuper@42430: val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in (*<<=====*) neuper@42426: (*last step re-calc in compare_step TODO before WN09*) neuper@42423: in neuper@42423: case msg_calcstate' of neuper@42426: ("no derivation found", calcstate') => neuper@42426: let neuper@42426: val pp = par_pblobj pt p neuper@42427: val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp) neuper@42427: val ScrState (env, _, _, _, _, _) = get_istate pt pos neuper@42426: in neuper@42428: case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of neuper@42426: SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate') neuper@42426: | NONE => msg_calcstate' neuper@42426: end neuper@42423: | _ => msg_calcstate' neuper@42423: end neuper@42423: end neuper@42426: | NONE => ("syntax error in '" ^ istr ^ "'", e_calcstate'); neuper@37906: neuper@42433: (* fill-in patterns an forms. neuper@42433: returns thm required by "fun in_fillform *) neuper@42433: fun get_fillform (subs_opt, subst) (thm, form) errpatID ((fillpatID, pat, erpaID): fillpat) = neuper@42430: let neuper@42430: val (form', _, _, rewritten) = neuper@42430: rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (Trueprop $ pat) form; neuper@42430: in (*the fillpat of the thm must be dedicated to errpatID*) neuper@42430: if errpatID = erpaID andalso rewritten neuper@42433: then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) else NONE end; neuper@42430: neuper@42430: fun get_fillpats subst form errpatID thm = neuper@42430: let neuper@42430: val thmDeriv = Thm.get_name_hint thm neuper@42430: val (part, thyID) = thy_containing_thm thmDeriv neuper@42430: val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv] neuper@42430: val Hthm {fillpats, ...} = get_the theID neuper@42433: val some = map (get_fillform subst (thm, form) errpatID) fillpats neuper@42430: in some |> filter is_some |> map the end; neuper@42430: neuper@42430: fun find_fillpatterns (pt, pos as (p, _): pos') errpatID = neuper@42430: let neuper@42431: val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*) neuper@42430: val pp = par_pblobj pt p neuper@42430: val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp) neuper@42430: val ScrState (env, _, _, _, _, _) = get_istate pt pos neuper@42430: val subst = get_bdv_subst prog env neuper@42430: val errpatthms = errpats neuper@42430: |> filter ((curry op = errpatID) o (#1: errpat -> errpatID)) neuper@42430: |> map (#3: errpat -> thm list) neuper@42430: |> flat neuper@42430: in map (get_fillpats subst f_curr errpatID) errpatthms |> flat end; neuper@37906: neuper@37906: (*------------------------------------------------------------------(**) neuper@37906: end neuper@37906: open inform; neuper@37906: (**)------------------------------------------------------------------*)