neuper@37906: (* the problems and methods as stored in hierarchies neuper@37906: author Walther Neuper 1998 neuper@37906: (c) due to copyright terms neuper@37906: neuper@37906: use"ME/ptyps.sml"; neuper@37906: use"ptyps.sml"; neuper@37906: *) neuper@37906: neuper@37906: (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*) neuper@37928: val dsc_unknown = (term_of o the o (parseold @{theory Script})) neuper@37906: "unknown::'a => unknow"; neuper@37906: (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*) neuper@37906: neuper@37906: neuper@37906: (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) neuper@37906: neuper@37928: fun itm_2item thy (Cor ((d,ts),_)) = neuper@37929: Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) neuper@37928: | itm_2item _ (Syn c) = SyntaxE c neuper@37928: | itm_2item _ (Typ c) = TypeE c neuper@37928: | itm_2item thy (Inc ((d,ts),_)) = neuper@37929: Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) neuper@37928: | itm_2item thy (Sup (d,ts)) = neuper@37929: Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) neuper@37928: | itm_2item _ (Mis (d,pid)) = neuper@37929: Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ neuper@37929: Syntax.string_of_term (thy2ctxt' "Isac") pid); neuper@37906: neuper@37906: neuper@37906: (* --- 8.3.00 neuper@37906: fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list) neuper@37906: handle _ => error ("get_dsc_in not for "^sel); neuper@37906: neuper@37906: fun dscs_in dscppc = neuper@37906: ((get_dsc_in dscppc "#Given") @ neuper@37906: (get_dsc_in dscppc "#Find") @ neuper@37906: (get_dsc_in dscppc "#Relate")):term list; neuper@37906: neuper@37906: --- 26.1.88 neuper@37906: fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel))); neuper@37906: fun get_dsc pblID = neuper@37906: (get_dsc_of pblID "#Given") @ neuper@37906: (get_dsc_of pblID "#Find") @ neuper@37906: (get_dsc_of pblID "#Relate"); neuper@37906: --- *) neuper@37906: neuper@37906: fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) = neuper@37906: {Given=map f gi, Where=map f wh, neuper@37906: Find=map f fi, With=map f wi, Relate=map f re}:'b ppc; neuper@37906: fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) = neuper@37906: {Given=f gi, Where=f wh, neuper@37906: Find=f fi, With=f wi, Relate=f re}:'b ppc; neuper@37906: neuper@37906: (*for ppc of changing type*) neuper@37906: fun sel_ppc sel ppc = neuper@37906: case sel of neuper@37906: "#Given" => #Given (ppc:'a ppc) neuper@37906: | "#Where" => #Where (ppc:'a ppc) neuper@37906: | "#Find" => #Find (ppc:'a ppc) neuper@37906: | "#With" => #With (ppc:'a ppc) neuper@37906: | "#Relate" => #Relate (ppc:'a ppc) neuper@38031: | _ => error ("sel_ppc tried to select by '"^sel^"'"); neuper@37906: neuper@37906: fun repl_sel_ppc sel neuper@37906: ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x = neuper@37906: case sel of neuper@37906: "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) neuper@37906: | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re} neuper@37906: | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re} neuper@37906: | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re} neuper@37906: | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x} neuper@38031: | _ => error ("repl_sel_ppc tried to select by '"^sel^"'"); neuper@37906: neuper@37906: fun add_sel_ppc thy sel neuper@37906: ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x = neuper@37906: case sel of neuper@37906: "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) neuper@37906: | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re} neuper@37906: | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re} neuper@37906: | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]} neuper@37906: | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*) neuper@38031: | _ => error ("add_sel_ppc tried to select by '"^sel^"'"); neuper@37906: fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh = neuper@37906: ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc); neuper@37906: neuper@37906: (*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*) neuper@37906: neuper@37906: neuper@37906: (*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*decompose a problem-type into description and identifier neuper@37906: FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *) neuper@37906: fun split_dsc thy t = neuper@37906: (let val (hd,args) = strip_comb t neuper@37906: in if is_dsc hd neuper@37906: then (hd, args) neuper@37906: else (e_term, [t]) (*??? 9.01 just copied*) neuper@37906: end) neuper@38031: handle _ => error ("split_dsc: called with "^ neuper@37929: (Syntax.string_of_term (thy2ctxt' "Isac") t)); neuper@37906: (* neuper@37906: > val t1 = (term_of o the o (parse thy)) "errorBound err_"; neuper@37906: > split_dsc t1; neuper@37906: (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool")) neuper@37906: : term * term neuper@37906: > val t3 = (term_of o the o (parse thy)) "valuesFor vs_"; neuper@37906: > split_dsc t3; neuper@37906: (Const ("Descript.valuesFor","bool List.list => Tools.toreall"), neuper@37906: Free ("vs_","bool List.list")) : term * term*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*. take the first two return-values; for prep_ori .*) neuper@37906: (*WN.13.5.03fun split_dts' thy t = neuper@37906: let val (d, ts, _) = split_dts thy t neuper@37906: in (d, ts) end;*) neuper@37906: (*WN.8.12.03 quick for prep_ori'*) neuper@37906: fun split_dsc' t = neuper@37906: (let val dsc $ var = t neuper@37906: in var end) neuper@38031: handle _ => error ("split_dsc': called with "^term2str t); neuper@37906: neuper@37906: (*9.3.00*) neuper@37906: (* split a term into description and (id | structured variable) neuper@37906: for pbt, met.ppc *) neuper@37906: fun split_did t = neuper@37906: (let val (hd,[arg]) = strip_comb t neuper@37906: in (hd,arg) end) neuper@38031: handle _ => error ("split_did: doesn't match (hd,[arg]) for t = " neuper@37928: ^(Syntax.string_of_term (thy2ctxt' "Script") t)); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*create output-string for itm_*) neuper@37929: fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) neuper@37906: | itm_out thy (Syn c) = c neuper@37906: | itm_out thy (Typ c) = c neuper@37929: | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) neuper@37929: | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) neuper@37906: | itm_out thy (Mis (d,pid)) = neuper@37929: Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ neuper@37929: Syntax.string_of_term (thy2ctxt' "Isac") pid; neuper@37906: neuper@37906: (*22.11.00 unused neuper@37906: fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) neuper@37906: neuper@37906: neuper@37906: (*--3.3. neuper@37906: fun itms2dts itms = neuper@37906: let neuper@37906: fun coll itms' [] = itms' neuper@37906: | coll itms' (i::itms) = neuper@37906: case i of neuper@37906: (Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms neuper@37906: | (Syn c) => coll (itms' ) itms neuper@37906: | (Typ c) => coll (itms' ) itms neuper@37906: | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms neuper@37906: | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms neuper@37906: | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms neuper@37906: in coll [] itms end; neuper@37906: *) neuper@37906: (*--3.3.00 neuper@37906: fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = neuper@37929: Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) neuper@37906: | itm2item (_,_,_,_,Syn (c)) = SyntaxE c neuper@37906: | itm2item (_,_,_,_,Typ (c)) = TypeE c neuper@37906: | itm2item (_,_,_,_,Fal (d,ts)) = neuper@37929: False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) neuper@37906: | itm2item (_,_,_,_,Inc (d,ts)) = neuper@37929: Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) neuper@37906: | itm2item (_,_,_,_,Sup (d,ts)) = neuper@37929: Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))); neuper@37906: *) neuper@37906: neuper@37906: fun boolterm2item (true, term) = Correct (term2str term) neuper@37906: | boolterm2item (false, term) = False (term2str term); neuper@37906: neuper@37906: (* use"ME/modspec.sml"; neuper@37906: *) neuper@37906: fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) = neuper@37906: let neuper@37906: fun coll ppc [] = ppc neuper@37906: | coll ppc ((_,_,_,field,itm_)::itms) = neuper@37906: coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms; neuper@37906: val gfr = coll empty_ppc itms; neuper@37906: in add_where gfr (map boolterm2item pre) end; neuper@37906: (*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*) neuper@37906: neuper@37906: (*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*) neuper@37906: neuper@37906: (* --- 9.3.fun add_field dscs (d,ts) = neuper@37906: if d mem (get_dsc_in dscs "#Given") neuper@37906: then ("#Given",d,ts:term list) neuper@37906: else if d mem (get_dsc_in dscs "#Find") neuper@37906: then ("#Find",d,ts) neuper@37906: else if d mem (get_dsc_in dscs "#Relate") neuper@37906: then ("#Relate",d,ts) neuper@37906: else ("#undef",d,ts); neuper@38031: (* 28.1.00 error ("add_field: '"^ neuper@37929: (Syntax.string_of_term (thy2ctxt' "Isac") d)^ neuper@37906: "' not in ppc-description "); *) neuper@37906: ------9.3. *) neuper@37906: neuper@37906: (* 9.3.00 neuper@37906: compare d and dsc in pbt and transfer field to pre-ori *) neuper@37906: fun add_field thy pbt (d,ts) = neuper@37906: let fun eq d pt = (d = (fst o snd) pt); neuper@37906: in case filter (eq d) pbt of neuper@37906: [(fi,(dsc,_))] => (fi,d,ts) neuper@37906: | [] => ("#undef",d,ts) (*may come with met.ppc*) neuper@38031: | _ => error ("add_field: "^ neuper@37929: (Syntax.string_of_term (thy2ctxt' "Isac") d)^ neuper@37906: " more than once in pbt") neuper@37906: end; neuper@37906: neuper@37906: (*. take over field from met.ppc at 'Specify_Method' into ori, neuper@37906: i.e. also removes "#undef" fields .*) neuper@37906: (* val (mpc, ori) = ((#ppc o get_met) mID, oris); neuper@37906: *) neuper@37906: fun add_field' thy mpc (ori:ori list) = neuper@37906: let fun eq d pt = (d = (fst o snd) pt); neuper@37906: fun repl mpc (i,v,_,d,ts) = neuper@37906: case filter (eq d) mpc of neuper@37906: [(fi,(dsc,_))] => [(i,v,fi,d,ts)] neuper@37906: | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) neuper@38031: (*error ("add_field': "^ neuper@37929: (Syntax.string_of_term (thy2ctxt' "Isac") d)^ neuper@37906: " not in met"*) neuper@38031: | _ => error ("add_field': "^ neuper@37929: (Syntax.string_of_term (thy2ctxt' "Isac") d)^ neuper@37906: " more than once in met"); neuper@37906: in (flat ((map (repl mpc)) ori)):ori list end; neuper@37906: neuper@37906: neuper@37906: (*.mark an element with the position within a plateau; neuper@37906: a plateau with length 1 is marked with 0 .*) neuper@38031: fun mark eq [] = error "mark []" neuper@37906: | mark eq xs = neuper@37906: let neuper@37906: fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)] neuper@37906: | mar xx eq (x::x'::xs) n = neuper@37906: if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1) neuper@37906: else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1; neuper@37906: in mar [] eq xs 1 end; neuper@37906: (* neuper@37906: > val xs = [1,1,1,2,4,4,5]; neuper@37906: > mark (op=) xs; neuper@37906: val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)] neuper@37906: *) neuper@37906: neuper@37906: (*.assumes equal descriptions to be in adjacent 'plateaus', neuper@37906: items at a certain position within the plateaus form a variant; neuper@37906: length = 1 ... marked with 0: covers all variants .*) neuper@37906: fun add_variants fdts = neuper@37906: let neuper@37906: fun eq (a,b) = curry op= (snd3 a) (snd3 b); neuper@37906: in mark eq fdts end; neuper@37906: neuper@37906: (* collect equal elements: the model for coll_variants *) neuper@37906: fun coll eq xs = neuper@37906: let neuper@37906: fun col xs eq x [] = xs @ [x] neuper@37906: | col xs eq x (y::ys) = neuper@37906: if eq(x,y) then col xs eq x ys neuper@37906: else col (xs @ [x]) eq y ys; neuper@37906: in col [] eq (hd xs) xs end; neuper@37906: (* neuper@37906: > val xs = [1,1,1,2,4,4,4]; neuper@37906: > coll (op=) xs; neuper@37906: val it = [1,2,4] : int list neuper@37906: *) neuper@37906: neuper@38031: fun max [] = error "max of []" neuper@37906: | max (y::ys) = neuper@37906: let fun mx x [] = x neuper@37906: | mx x (y::ys) = if x < y then mx y ys else mx x ys; neuper@37906: in mx y ys end; neuper@38031: fun gen_max _ [] = error "gen_max of []" neuper@37906: | gen_max ord (y::ys) = neuper@37906: let fun mx x [] = x neuper@37906: | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys; neuper@37906: in mx y ys end; neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* assumes *) neuper@37906: fun coll_variants (((v,x)::vxs)) = neuper@37906: let neuper@37906: fun col xs (vs,x) [] = xs @ [(vs,x)] neuper@37906: | col xs (vs,x) ((v',x')::vxs') = neuper@37906: if x=x' then col xs (vs @ [v'], x') vxs' neuper@37906: else col (xs @ [(vs,x)]) ([v'], x') vxs'; neuper@37906: in col [] ([v],x) vxs end; neuper@37906: (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]; neuper@37906: > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs); neuper@37906: val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *) neuper@37906: neuper@37906: neuper@37906: fun replace_0 vm [0] = intsto vm neuper@37906: | replace_0 vm vs = vs; neuper@37906: neuper@38031: fun add_id [] = error "add_id []" neuper@37906: | add_id xs = neuper@37906: let fun add n [] = [] neuper@37906: | add n (x::xs) = (n,x) :: add (n+1) xs; neuper@37906: in add 1 xs end; neuper@37906: (* neuper@37906: > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)]; neuper@37906: > add_id xs; neuper@37906: val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))] neuper@37906: *) neuper@37906: neuper@37906: fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e); neuper@37906: fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e); neuper@37906: fun flat3 (a,(b,c)) = (a,b,c); neuper@37906: (* neuper@37906: val pI = pI'; neuper@37906: !pbts; neuper@37906: *) neuper@37906: (* in root (only!) fmz may be empty: fill with ..,dsc,[] neuper@37906: fun init_ori fmz thy pI = neuper@37906: if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*) neuper@37906: else neuper@37906: let neuper@37906: val fds = map (cons2 (fst, fst o snd)) (get_pbt pI); neuper@37906: val vfds = map ((pair [1]) o (rpair [])) fds; neuper@37906: val ivfds = add_id vfds neuper@37906: in (map flattup' ivfds):ori list end; 10.3.00---*) neuper@37906: (* val fmz = ctl; val pI=["sqroot-test","univariate","equation"]; neuper@37906: val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI'); neuper@37906: val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI)); neuper@37906: *) neuper@37906: fun prep_ori [] _ _ = [] neuper@37906: | prep_ori fmz thy pbt = neuper@37906: let neuper@37906: val ctopts = map (parse thy) fmz neuper@37906: val _= (*FIXME.WN060916 improve error report*) neuper@37906: if null (filter is_none ctopts) then () neuper@38031: else error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz) neuper@37906: val dts = map ((split_dts thy) o term_of o the) ctopts neuper@37906: val ori = map (add_field thy pbt) dts; neuper@37906: (* val ori = map (flat3 o (pair "#undef")) dts; *) neuper@37906: val ori' = add_variants ori; neuper@37906: val maxv = max (map fst ori'); neuper@37906: val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv; neuper@37906: val ori'' = coll_variants ori'; neuper@37906: val ori''' = map (apfst (replace_0 maxv)) ori''; neuper@37906: val ori'''' = add_id ori''' neuper@37906: in (map flattup ori''''):ori list end; neuper@37906: neuper@37906: neuper@37906: (*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*) neuper@37906: neuper@37906: (*.the pattern for an item of a problems model or a methods guard.*) neuper@37906: type pat = (string * (*field*) neuper@37906: (term * (*description*) neuper@38009: term)) (*id | arbitrary term*); neuper@37906: fun pat2str ((field, (dsc, id)):pat) = neuper@37906: pair2str (field, pair2str (term2str dsc, term2str id)); neuper@37906: fun pats2str pats = (strs2str o (map pat2str)) pats; neuper@37906: neuper@37906: (* data for methods stored in 'methods'-database *) neuper@37906: type met = neuper@37906: {guh : guh, (*unique within this isac-knowledge *) neuper@37906: mathauthors: string list,(*copyright *) neuper@37906: init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*) neuper@37906: rew_ord' : rew_ord', (*for rules in Detail neuper@37906: TODO.WN0509 store fun itself, see 'type pbt'*) neuper@37906: erls : rls, (*the eval_rls for cond. in rules FIXME "rls' neuper@37906: instead erls in "fun prep_met" *) neuper@37906: srls : rls, (*for evaluating list expressions in scr *) neuper@37906: prls : rls, (*for evaluating predicates in modelpattern *) neuper@37906: crls : rls, (*for check_elementwise, ie. formulae in calc.*) neuper@37906: nrls : rls, (*canonical simplifier specific for this met *) neuper@37906: calc : calc list, (*040207: <--- calclist' in fun prep_met *) neuper@37906: (*branch : TransitiveB set in append_problem at generation ob pblobj neuper@38009: FIXXXME.0308: set branch from met in Apply_Method ? *) neuper@37906: neuper@37906: (* compare type pbt:*) neuper@37906: ppc: pat list, neuper@37906: (*.items in given, find, relate; neuper@37906: items (in "#Find") which need not occur in the arg-list of a SubProblem neuper@37906: are 'copy-named' with an identifier "*_!_". neuper@37906: copy-named items are 'generating' if they are NOT "*___" neuper@37906: see ME/calchead.sml 'fun is_copy_named'.*) neuper@38009: pre: term list, (*preconditions in where*) neuper@37906: (*script*) neuper@37906: scr: scr (*prep_met requires either script or string "empty_script"*) neuper@37906: }; neuper@37906: (* ------- template ------------------------------------------------------ neuper@37906: store_met neuper@37906: (prep_met *.thy neuper@37906: ([(*"EqSystem","normalize"*)], neuper@37906: [("#Given" ,[ (*"equalities es_", "solveForVars vs_"*)]), neuper@37906: ("#Find" ,[ (*dont forget typing non-reals *)]), neuper@37906: ("#Relate",[])(*may be omitted *) ], neuper@37906: {calc = [], (*filled autom. in prep_met *) neuper@37906: crls = Erls, (*for check_elementwise *) neuper@37906: prls = Erls, (*for evaluating preds in guard *) neuper@37906: nrls = Erls, (*can.simplifier for all formulae*) neuper@37906: rew_ord'="tless_true", (*for rules in Detail *) neuper@37906: rls' = Erls, (*erls, the eval_rls for cond. in rules*) neuper@37906: srls = Erls}, (*for evaluating list expr in scr*) neuper@37906: "empty_script" neuper@37906: )); neuper@37906: ---------- template ----------------------------------------------------*) neuper@37906: val e_met = {guh="met_empty",mathauthors=[],init=e_metID, neuper@37906: rew_ord' = "e_rew_ord'": rew_ord', neuper@37906: erls = e_rls, srls = e_rls, prls = e_rls, neuper@37906: calc = [], crls = e_rls, nrls = e_rls, neuper@37906: (*asm_thm = []: thm' list, neuper@37906: asm_rls = []: rls' list,*) neuper@37906: ppc = []: (string * (term * term)) list, neuper@37906: pre = []: term list, neuper@37906: scr = EmptyScr: scr}:met; neuper@37906: neuper@37906: neuper@37906: (** problem-types stored in format for usage in specify **) neuper@37906: (*25.8.01 ---- neuper@38006: val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*) neuper@37906: (term * (* description *) neuper@37906: term)) (* id | struct-var *) neuper@37906: list) neuper@37906: ) list);*) neuper@37906: neuper@38011: type pbt_ = (string * (* field "#Given",..*)(*deprecated due to 'type pat'*) neuper@37906: (term * (* description *) neuper@37906: term)); (* id | struct-var *) neuper@37906: val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_; neuper@37906: type pbt = neuper@37906: {guh : guh, (*unique within this isac-knowledge*) neuper@37906: mathauthors: string list, (*copyright*) neuper@37906: init : pblID, (*to start refinement with*) neuper@37906: thy : theory, (* which allows to compile that pbt neuper@37906: TODO: search generalized for subthy (ref.p.69*) neuper@37906: (*^^^ WN050912 NOT used during application of the problem, neuper@37906: because applied terms may be from 'subthy' as well as from super; neuper@37906: thus we take 'maxthy'; see match_ags !*) neuper@37906: cas : term option,(*'CAS-command'*) neuper@37906: prls : rls, (* for preds in where_*) neuper@37906: where_: term list, (* where - predicates*) neuper@37906: ppc : pat list, neuper@37906: (*this is the model-pattern; neuper@38011: it contains "#Given","#Where","#Find","#Relate"-patterns neuper@38011: for constraints on identifiers see "fun cpy_nam"*) neuper@37906: met : metID list}; (* methods solving the pbt*) neuper@37928: val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure", neuper@37926: cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt; neuper@37906: fun pbt2 (str, (t1, t2)) = neuper@37906: pair2str (str, pair2str (term2str t1, term2str t2)); neuper@37906: fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt; neuper@37906: neuper@37906: neuper@37906: val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]); neuper@37906: val e_Mets = Ptyp ("e_metID",[e_met],[]); neuper@37906: neuper@37906: type ptyps = (pbt ptyp) list; neuper@38006: val ptyps = Unsynchronized.ref ([e_Ptyp]:ptyps); neuper@37906: neuper@37906: type mets = (met ptyp) list; neuper@38006: val mets = Unsynchronized.ref ([e_Mets]:mets); neuper@37906: neuper@37906: neuper@37906: (**+ breadth-first search on hierarchy of problem-types +**) neuper@37906: neuper@37906: type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*) neuper@37906: (* eg. ["equations","univariate","normalize"] while neuper@37906: ["normalize","univariate","equations"] is the related pblID neuper@37906: WN.24.4.03: also used for metID*) neuper@37906: neuper@37906: fun get_py thy d _ [] = neuper@37906: error ("get_pbt not found: "^(strs2str d)) neuper@37906: | get_py thy d [k] ((Ptyp (k',[py],_))::pys) = neuper@37906: if k=k' then py neuper@37906: else get_py thy d ([k]:pblRD) pys neuper@37906: | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') = neuper@37906: if k=k' then get_py thy d ks pys neuper@37906: else get_py thy d (k::ks) pys'; neuper@37906: (*> ptyps:= neuper@37906: [Ptyp ("1",[("ptyp 1",([],[]))], neuper@37906: [Ptyp ("11",[("ptyp 11",([],[]))], neuper@37906: []) neuper@37906: ]), neuper@37906: Ptyp ("2",[("ptyp 2",([],[]))], neuper@37906: [Ptyp ("21",[("ptyp 21",([],[]))], neuper@37906: []) neuper@37906: ]) neuper@37906: ]; neuper@37906: > get_py SqRoot.thy ["1"] ["1"] (!ptyps); neuper@37906: > get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps); neuper@37906: _REVERSE_ .......... !!!!!!!!!!*) neuper@37906: neuper@37906: (*TODO: search generalized for subthy*) neuper@37906: fun get_pbt (pblID:pblID) = neuper@37906: let val pblRD = rev pblID; neuper@37928: in get_py (theory "Pure") pblID pblRD (!ptyps) end; neuper@37906: (* get_pbt thy ["1"]; neuper@37906: get_pbt thy ["21","2"]; neuper@37906: *) neuper@37906: neuper@37906: (*TODO: throws exn 'get_pbt not found: ' ... confusing !! neuper@37906: take 'ketype' as an argument !!!!!*) neuper@37928: fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets); neuper@37928: fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier); neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun del_eq k ptyps = neuper@37906: let fun del k ptyps [] = ptyps neuper@37906: | del k ptyps ((Ptyp (k', [p], ps))::pys) = neuper@37906: if k=k' then del k ptyps pys neuper@37906: else del k (ptyps @ [Ptyp (k', [p], ps)]) pys; neuper@37906: in del k [] ptyps end; neuper@37906: neuper@37906: fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])] neuper@37906: neuper@37906: | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) = neuper@38015: ((*tracing("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*) neuper@37906: if k=k' neuper@37906: then ((Ptyp (k', [pbt], ps))::pys) neuper@37906: else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*) neuper@37906: ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys)) neuper@37906: ) neuper@37906: | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) = neuper@38015: ((*tracing("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*) neuper@37906: if k=k' neuper@37906: then ((Ptyp (k', [p], insrt d pbt ks ps))::pys) neuper@37906: else neuper@37906: if length pys = 0 neuper@37906: then error ("insert: not found "^(strs2str (d:pblID))) neuper@37906: else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys)) neuper@37906: ); neuper@37906: neuper@37906: neuper@37906: fun coll_pblguhs pbls = neuper@37906: let fun node coll (Ptyp (_,[n],ns)) = neuper@37906: [(#guh : pbt -> guh) n] @ (nodes coll ns) neuper@37906: and nodes coll [] = coll neuper@37906: | nodes coll (n::ns) = (node coll n) @ (nodes coll ns); neuper@37906: in nodes [] pbls end; neuper@37906: fun coll_metguhs mets = neuper@37906: let fun node coll (Ptyp (_,[n],ns)) = neuper@37906: [(#guh : met -> guh) n] neuper@37906: and nodes coll [] = coll neuper@37906: | nodes coll (n::ns) = (node coll n) @ (nodes coll ns); neuper@37906: in nodes [] mets end; neuper@37906: neuper@37906: (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*) neuper@37906: fun guh2kestoreID (guh:guh) = neuper@37906: case (implode o (take_fromto 1 4) o explode) guh of neuper@37906: "pbl_" => neuper@37906: let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) = neuper@37906: if gu = guh neuper@37926: then SOME ((ids@[id]) : kestoreID) neuper@37906: else nodes (ids@[id]) gu ns neuper@37926: and nodes _ _ [] = NONE neuper@37906: | nodes ids gu (n::ns) = neuper@37926: case node ids gu n of SOME id => SOME id neuper@37926: | NONE => nodes ids gu ns neuper@37906: in case nodes [] guh (!ptyps) of neuper@37926: SOME id => rev id neuper@37926: | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^ neuper@37906: "not found in (!ptyps)") neuper@37906: end neuper@37906: | "met_" => neuper@37906: let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) = neuper@37906: if gu = guh neuper@37926: then SOME ((ids@[id]) : kestoreID) neuper@37906: else nodes (ids@[id]) gu ns neuper@37926: and nodes _ _ [] = NONE neuper@37906: | nodes ids gu (n::ns) = neuper@37926: case node ids gu n of SOME id => SOME id neuper@37926: | NONE => nodes ids gu ns neuper@37906: in case nodes [] guh (!mets) of neuper@37926: SOME id => id neuper@37926: | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^ neuper@37906: "not found in (!mets)") end neuper@37906: | _ => error ("guh2kestoreID called with '" ^ guh ^ "'"); neuper@37906: (*> guh2kestoreID "pbl_equ_univ_lin"; neuper@37906: val it = ["linear", "univariate", "equation"] : string list*) neuper@37906: neuper@37906: neuper@37906: fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) = neuper@37928: if member op = (coll_pblguhs pbls) guh neuper@37906: then error ("check_guh_unique failed with '"^guh^"';\n"^ neuper@37906: "use 'sort_pblguhs()' for a list of guhs;\n"^ neuper@37906: "consider setting 'check_guhs_unique := false'") neuper@37906: else (); neuper@37906: (* val (guh, mets) = ("met_test", !mets); neuper@37906: *) neuper@37906: fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = neuper@37928: if member op = (coll_metguhs mets) guh neuper@37906: then error ("check_guh_unique failed with '"^guh^"';\n"^ neuper@37906: "use 'sort_metguhs()' for a list of guhs;\n"^ neuper@37906: "consider setting 'check_guhs_unique := false'") neuper@37906: else (); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.the pblID has the leaf-element as first; better readability achieved;.*) neuper@37906: fun store_pbt (pbt as {guh,...}, pblID) = neuper@37906: (if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else (); neuper@37906: ptyps:= insrt pblID pbt (rev pblID) (!ptyps)); neuper@37906: neuper@37906: (*.the metID has the root-element as first; compare 'fun store_pbt'.*) neuper@37906: (* val (met as {guh,...}, metID) = neuper@37906: ((prep_met EqSystem.thy "met_eqsys" [] e_metID neuper@37906: (["EqSystem"], neuper@37906: [], neuper@37906: {rew_ord'="tless_true", rls' = Erls, calc = [], neuper@37906: srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, neuper@37906: "empty_script" neuper@37906: ))); neuper@37906: *) neuper@37906: fun store_met (met as {guh,...}, metID) = neuper@37906: (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else (); neuper@37906: mets:= insrt metID met metID (!mets)); neuper@37906: neuper@37906: neuper@37906: (*. prepare problem-types before storing in pbltypes; neuper@37906: dont forget to 'check_guh_unique' before ins.*) neuper@37906: fun prep_pbt thy guh maa init neuper@37906: (pblID, dsc_dats: (string * (string list)) list, neuper@37906: ev:rls, ca: string option, metIDs:metID list) = neuper@37906: (* val (thy, (pblID, dsc_dats: (string * (string list)) list, neuper@37906: ev:rls, ca: string option, metIDs:metID list)) = neuper@37906: ((EqSystem.thy, (["system"], neuper@37906: [("#Given" ,["equalities es_", "solveForVars vs_"]), neuper@37906: ("#Find" ,["solution ss___"](*___ is copy-named*)) neuper@37906: ], neuper@37906: append_rls "e_rls" e_rls [(*for preds in where_*)], neuper@37926: SOME "solveSystem es_ vs_", neuper@37906: []))); neuper@37906: *) neuper@37906: let fun eq f (f', _) = f = f'; neuper@37906: val gi = filter (eq "#Given") dsc_dats; neuper@37906: (*val gi = [("#Given",["equality e_","solveFor v_"])] neuper@37906: : (string * string list) list*) neuper@37906: val gi = (case gi of neuper@37906: [] => [] neuper@37906: | ((_,gi')::[]) => neuper@37906: ((map (split_did o term_of o the o (parse thy)) gi') neuper@37906: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Given' of "^ neuper@37906: (strs2str pblID))) neuper@37906: | _ => neuper@37906: (error ("prep_pbt: more than one '#Given' in "^ neuper@37906: (strs2str pblID)))); neuper@37906: (*val gi = neuper@37906: [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")), neuper@37906: (Const ("Descript.solveFor","RealDef.real => Tools.una"), neuper@37906: Free ("v_","RealDef.real"))] : (term * term) list *) neuper@37906: val gi = map (pair "#Given") gi; neuper@37906: (*val gi = neuper@37906: [("#Given", neuper@37906: (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))), neuper@37906: ("#Given", neuper@37906: (Const ("Descript.solveFor","RealDef.real => Tools.una"), neuper@37906: Free ("v_","RealDef.real")))] : (string * (term * term)) list*) neuper@37906: neuper@37906: val fi = filter (eq "#Find") dsc_dats; neuper@37906: val fi = (case fi of neuper@38031: [] => [](*28.8.01: ["tool"] ...// error neuper@37906: ("prep_pbt: no '#Find' in "^(strs2str pblID))*) neuper@37906: (* val ((_,fi')::[]) = fi; neuper@37906: *) neuper@37906: | ((_,fi')::[]) => neuper@37906: ((map (split_did o term_of o the o (parse thy)) fi') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Find' of "^ neuper@37906: (strs2str pblID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Find' in "^ neuper@37906: (strs2str pblID)))); neuper@37906: val fi = map (pair "#Find") fi; neuper@37906: neuper@37906: val re = filter (eq "#Relate") dsc_dats; neuper@37906: val re = (case re of neuper@37906: [] => [] neuper@37906: | ((_,re')::[]) => neuper@37906: ((map (split_did o term_of o the o (parse thy)) re') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Relate' of "^ neuper@37906: (strs2str pblID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Relate' in "^ neuper@37906: (strs2str pblID)))); neuper@37906: val re = map (pair "#Relate") re; neuper@37906: neuper@37906: val wh = filter (eq "#Where") dsc_dats; neuper@37906: val wh = (case wh of neuper@37906: [] => [] neuper@37906: | ((_,wh')::[]) => neuper@37977: ((map (parse_patt thy) wh') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Where' of "^ neuper@37906: (strs2str pblID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Where' in "^ neuper@37906: (strs2str pblID)))); neuper@37906: in ({guh=guh,mathauthors=maa,init=init, neuper@37926: thy=thy,cas= case ca of NONE => NONE neuper@37926: | SOME s => neuper@37926: SOME ((term_of o the o (parse thy)) s), neuper@37906: prls=ev,where_=wh,ppc= gi @ fi @ re, neuper@37906: met=metIDs}, pblID):pbt * pblID end; neuper@37906: (* prep_pbt thy (pblID, dsc_dats, metIDs); neuper@37906: val it = neuper@37906: ({met=[], neuper@37906: ppc=[("#Given",(Const (#,#),Free (#,#))), neuper@37906: ("#Given",(Const (#,#),Free (#,#))), neuper@37906: ("#Find",(Const (#,#),Free (#,#)))], neuper@37906: thy={ProtoPure, ..., Atools, RatArith}, neuper@37906: where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $ neuper@37906: Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*. prepare met for storage analogous to pbt .*) neuper@37906: fun prep_met thy guh maa init neuper@37906: (metID, ppc: (string * string list) list (*'#Where' -> #pre*), neuper@37906: {rew_ord'=ro, rls'=rls, srls=srls, prls=prls, neuper@37906: calc = scr_isa_fns(*FIXME.040207: del - auto-done*), neuper@37906: crls=cr, nrls=nr}, scr) = neuper@37906: let fun eq f (f', _) = f = f'; neuper@37906: (*val thy = (assoc_thy o fst) metID*) neuper@37906: val gi = filter (eq "#Given") ppc; neuper@37906: val gi = (case gi of neuper@37906: [] => [] neuper@37906: | ((_,gi')::[]) => neuper@37906: ((map (split_did o term_of o the o (parse thy)) gi') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Given' of "^ neuper@37906: (strs2str metID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Given' in "^ neuper@37906: (strs2str metID)))); neuper@37906: val gi = map (pair "#Given") gi; neuper@37906: neuper@37906: val fi = filter (eq "#Find") ppc; neuper@37906: val fi = (case fi of neuper@38031: [] => [](*28.8.01: ["tool"] ...// error neuper@37906: ("prep_pbt: no '#Find' in "^(strs2str metID))*) neuper@37906: | ((_,fi')::[]) => neuper@37906: ((map (split_did o term_of o the o (parse thy)) fi') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Find' of "^ neuper@37906: (strs2str metID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Find' in "^ neuper@37906: (strs2str metID)))); neuper@37906: val fi = map (pair "#Find") fi; neuper@37906: neuper@37906: val re = filter (eq "#Relate") ppc; neuper@37906: val re = (case re of neuper@37906: [] => [] neuper@37906: | ((_,re')::[]) => neuper@37906: ((map (split_did o term_of o the o (parse thy)) re') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Relate' of "^ neuper@37906: (strs2str metID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Relate' in "^ neuper@37906: (strs2str metID)))); neuper@37906: val re = map (pair "#Relate") re; neuper@37906: neuper@37906: val wh = filter (eq "#Where") ppc; neuper@37906: val wh = (case wh of neuper@37906: [] => [] neuper@37906: | ((_,wh')::[]) => neuper@37977: ((map (parse_patt thy) wh') neuper@38031: handle _ => error neuper@37906: ("prep_pbt: syntax error in '#Where' of "^ neuper@37906: (strs2str metID))) neuper@37906: | _ => neuper@38031: (error ("prep_pbt: more than one '#Where' in "^ neuper@37906: (strs2str metID)))); neuper@37906: val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr) neuper@37906: in ({guh=guh,mathauthors=maa,init=init, neuper@37906: ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls, neuper@37906: calc = if scr = "empty_script" then [] neuper@37906: else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o neuper@37906: (filter is_calc) o stacpbls) sc, neuper@37906: crls=cr, nrls=nr, scr=Script sc}:met, neuper@37906: metID:metID) neuper@37906: end; neuper@37906: neuper@37906: neuper@37906: (**. get pblIDs of all entries in mat3D .**) neuper@37906: neuper@37906: neuper@37906: fun format_pblID strl = enclose " [" "]" (commas_quote strl); neuper@37906: fun format_pblIDl strll = enclose "[\n" "\n]\n" neuper@37906: (space_implode ",\n" (map format_pblID strll)); neuper@37906: neuper@37906: fun scan _ [] = [] (* no base case, for empty doms only *) neuper@37906: | scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]] neuper@37906: | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl neuper@37906: | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps) neuper@37906: | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps); neuper@37906: neuper@38015: fun show_ptyps () = (tracing o format_pblIDl o (scan [])) (!ptyps); neuper@37906: (* ptyps:=[]; neuper@37906: show_ptyps(); neuper@37906: *) neuper@38015: fun show_mets () = (tracing o format_pblIDl o (scan [])) (!mets); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*vvvvv---------- preparational work 8.01. UNUSED *) neuper@37906: (**+ instantiate a problem-type +**) neuper@37906: neuper@37906: (*+ transform oris +*) neuper@37906: neuper@37928: fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs; neuper@37906: (*> coll_vats [11,22] (hd oris); neuper@37906: val it = [22,11,1,2,3] : int list neuper@37906: neuper@37906: > foldl coll_vats ([],oris); neuper@37906: val it = [1,2,3] : int list neuper@37906: neuper@37906: > val i=1; neuper@37906: > filter ((curry (op mem) i) o #2) oris; neuper@37906: val it = neuper@37906: [(1,[1,2,3],"#Given",Const (#,#),[# $ #]), neuper@37906: (2,[1,2,3],"#Find",Const (#,#),[Free #]), neuper@37906: (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), neuper@37906: (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), neuper@37906: (6,[1],"#undef",Const (#,#),[Free #]), neuper@37906: (9,[1,2],"#undef",Const (#,#),[# $ #]), neuper@37906: (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *) neuper@37906: neuper@37936: local infix mem; (*from Isabelle2002*) neuper@37928: fun x mem [] = false neuper@37928: | x mem (y :: ys) = x = y orelse x mem ys; neuper@37928: in neuper@37928: fun filter_vat oris i = neuper@37928: filter ((curry (op mem) i) o (#2 : ori -> int list)) oris; neuper@37928: end; neuper@37906: (*> map (filter_vat oris) [1,2,3]; neuper@37906: val it = neuper@37906: [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]), neuper@37906: (2,[1,2,3],"#Find",Const (#,#),[Free #]), neuper@37906: (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), neuper@37906: (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), neuper@37906: (6,[1],"#undef",Const (#,#),[Free #]), neuper@37906: (9,[1,2],"#undef",Const (#,#),[# $ #]), neuper@37906: (11,[1,2,3],"#undef",Const (#,#),[# $ #])], neuper@37906: [(1,[1,2,3],"#Given",Const (#,#),[# $ #]), neuper@37906: (2,[1,2,3],"#Find",Const (#,#),[Free #]), neuper@37906: (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), neuper@37906: (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), neuper@37906: (7,[2],"#undef",Const (#,#),[Free #]), neuper@37906: (9,[1,2],"#undef",Const (#,#),[# $ #]), neuper@37906: (11,[1,2,3],"#undef",Const (#,#),[# $ #])], neuper@37906: [(1,[1,2,3],"#Given",Const (#,#),[# $ #]), neuper@37906: (2,[1,2,3],"#Find",Const (#,#),[Free #]), neuper@37906: (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), neuper@37906: (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]), neuper@37906: (8,[3],"#undef",Const (#,#),[Free #]), neuper@37906: (10,[3],"#undef",Const (#,#),[# $ #]), neuper@37906: (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*) neuper@37906: neuper@37906: fun separate_vats oris = neuper@37928: let val vats = foldl coll_vats ([] : int list, oris); neuper@37906: in map (filter_vat oris) vats end; neuper@37906: (*^^^ end preparational work 8.01.*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (**. check a problem (ie. itm list) for matching a problemtype .**) neuper@37906: neuper@37906: fun eq1 d (_,(d',_)) = (d = d'); neuper@37906: fun itm_id ((i,_,_,_,_):itm) = i; neuper@37906: fun ori_id ((i,_,_,_,_):ori) = i; neuper@37906: fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm); neuper@37906: (*see + add_sel_ppc ~~~~~~~*) neuper@37906: fun field_eq f ((_,_,f',_,_):ori) = f = f'; neuper@37906: neuper@37906: (*. check an item (with arbitrary itm_ from previous matchings) neuper@37906: for matching a problemtype; returns true only for itms found in pbt .*) neuper@37906: fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) = neuper@37906: (case find_first (eq1 d) pbt of neuper@37926: SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs), neuper@37906: (id, pbl_ids' thy d vs))):itm) neuper@37926: | NONE => (i,vats,false,f,Sup (d,vs))) neuper@37906: | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) = neuper@37906: (case find_first (eq1 d) pbt of neuper@37926: SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs), neuper@37906: (id, pbl_ids' thy d vs))):itm) neuper@37926: | NONE => (i,vats,false,f,Sup (d,vs))) neuper@37906: neuper@37906: | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm neuper@37906: | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm neuper@37906: neuper@37906: | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) = neuper@37906: (case find_first (eq1 d) pbt of neuper@37926: SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs), neuper@37906: (id, pbl_ids' thy d vs))):itm) neuper@37926: | NONE => (i,vats,false,f,Sup (d,vs))) neuper@37906: (* val (i,vats,b,f,Mis (d,vs)) = i4; neuper@37906: *) neuper@37906: | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) = neuper@37906: (case find_first (eq1 d) pbt of neuper@37926: (* val SOME (_,(_,id)) = find_first (eq1 d) pbt; neuper@37906: *) neuper@38031: SOME (_,(_,id)) => error "chk_: ((i,vats,b,f,Cor ((d,vs),\ neuper@37906: \(id, pbl_ids' d vs))):itm)" neuper@37926: | NONE => (i,vats,false,f,Sup (d,[vs]))); neuper@37906: neuper@37906: (* chk_ thy pbt i neuper@37906: *) neuper@37906: neuper@37906: fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_; neuper@37906: fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d'; neuper@37906: fun eq0 ((0,_,_,_,_):itm) = true neuper@37906: | eq0 _ = false; neuper@37906: fun max_i i [] = i neuper@37906: | max_i i ((id,_,_,_,_)::is) = neuper@37906: if i > id then max_i i is else max_i id is; neuper@37906: fun max_id [] = 0 neuper@37906: | max_id ((id,_,_,_,_)::is) = max_i id is; neuper@37906: fun add_idvat itms _ _ [] = itms neuper@37906: | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) = neuper@37906: add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *) neuper@37906: ],b,f,itm_):itm]) (i+1) mvat its; neuper@37906: neuper@37906: neuper@37906: (*. find elements of pbt not contained in itms; neuper@37906: if such one is untouched, return this one, otherwise create new itm .*) neuper@37906: fun chk_m (itms:itm list) untouched (p as (f,(d,id))) = neuper@37906: case find_first (eq2 p) itms of neuper@37926: SOME _ => [] neuper@37926: | NONE => (case find_first (eq2 p) untouched of neuper@37926: SOME itm => [itm] neuper@37926: | NONE => [(0,[],false,f,Mis (d,id)):itm]); neuper@37906: (* val itms = itms''; neuper@37906: *) neuper@37906: fun chk_mis mvat itms untouched pbt = neuper@37906: let val mis = (flat o (map (chk_m itms untouched))) pbt; neuper@37906: val mid = max_id itms; neuper@37906: in add_idvat [] (mid + 1) mvat mis end; neuper@37906: neuper@37906: (*. check a problem (ie. itm list) for matching a problemtype, neuper@37906: takes the max_vt for concluding completeness (could be another!) .*) neuper@37906: (* val itms = itms'; val (pbt,pre) = (ppc, pre); neuper@37906: val itms = itms; val (pbt,pre) = (ppc, pre); neuper@37906: *) neuper@37906: fun match_itms thy itms (pbt,pre,prls) = neuper@37928: (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat neuper@37928: andalso b; neuper@37906: val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*) neuper@37906: val mvat = max_vt itms'; neuper@37906: val itms'' = filter (okv mvat) itms'; neuper@37906: val untouched = filter eq0 itms;(*i.e. dsc only (from init)*) neuper@37906: val mis = chk_mis mvat itms'' untouched pbt; neuper@37906: val pre' = check_preconds' prls pre itms'' mvat neuper@37906: val pb = foldl and_ (true, map fst pre') neuper@37906: in (length mis = 0 andalso pb, (itms'@ mis, pre')) end); neuper@37906: neuper@37906: (*. check a problem pbl (ie. itm list) for matching a problemtype pbt, neuper@37906: for missing items get data from formalization (ie. ori list); neuper@37906: takes the max_vt for concluding completeness (could be another!) .*) neuper@37906: (* (0) determine the most frequent variant mv in pbl neuper@37906: ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => neuper@37906: (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; neuper@37906: (3) newitms = filter (mv mem vat(news)) news neuper@37906: (4) pbt @ newitms *) neuper@37906: (* val (pbl, pbt, pre) = (met, mtt, pre); neuper@37906: val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt); neuper@37906: val (pbl, pbt, pre) = (itms, ppc, where_); neuper@37906: *) neuper@37906: fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris = neuper@37906: let neuper@37906: (*0*)val mv = max_vt pbl; neuper@37906: neuper@37906: fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_; neuper@37906: fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of neuper@37926: SOME _ => false | NONE => true; neuper@37906: (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt; neuper@37906: neuper@37906: fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d'; neuper@37906: fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) = neuper@37906: (i,v,false,f,Mis (d,pid)):itm; neuper@37906: (*2*)fun oris2itms oris mis1 = neuper@37906: ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; neuper@37906: val news = (flat o (map (oris2itms oris))) mis; neuper@37928: (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv; neuper@37906: val newitms = filter mem_vat news; neuper@37906: (*4*)val itms' = pbl @ newitms; neuper@37906: val pre' = check_preconds' prls pre itms' mv neuper@37906: val pb = foldl and_ (true, map fst pre') neuper@37906: in (length mis = 0 andalso pb, (itms', pre')) end; neuper@37906: (*handle _ => (false,([],[]))*); neuper@37906: neuper@37906: neuper@37906: (*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris neuper@37906: allow for faster access to descriptions and terms *) neuper@37906: (**. check a problem (ie. itm list) for matching a problemtype .**) neuper@37906: neuper@37906: (*. check an ori for matching a problemtype by description; neuper@37906: returns true only for itms found in pbt .*) neuper@37906: fun chk1_ thy pbt ((i,vats,f,d,vs):ori) = neuper@37906: case find_first (eq1 d) pbt of neuper@37926: SOME (_,(_,id)) => [(i,vats,true,f, neuper@37906: Cor ((d,vs), (id, pbl_ids' thy d vs))):itm] neuper@37926: | NONE => []; neuper@37906: neuper@37906: (* elem 'p' of pbt contained in itms ? *) neuper@37906: fun chk1_m (itms:itm list) p = neuper@37906: case find_first (eq2 p) itms of neuper@37926: SOME _ => true | NONE => false; neuper@37906: fun chk1_m' (oris: ori list) (p as (f,(d,t))) = neuper@37906: case find_first (eq2' p) oris of neuper@37926: SOME _ => [] neuper@37926: | NONE => [(f, Mis (d, t))]; neuper@37906: fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm; neuper@37906: neuper@37906: fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc); neuper@37906: fun chk1_mis' oris ppc = neuper@37906: map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc); neuper@37906: neuper@37906: neuper@37906: (*. check a problem (ie. ori list) for matching a problemtype, neuper@37906: takes the max_vt for concluding completeness (FIXME could be another!) .*) neuper@37906: (* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py); neuper@37906: *) neuper@37906: fun match_oris thy prls oris (pbt,pre) = neuper@37906: let val itms = (flat o (map (chk1_ thy pbt))) oris; neuper@37906: val mvat = max_vt itms; neuper@37906: val complete = chk1_mis mvat itms pbt; neuper@37906: val pre' = check_preconds' prls pre itms mvat neuper@37906: val pb = foldl and_ (true, map fst pre') neuper@37906: in if complete andalso pb then true else false end; neuper@37906: (*run subp-rooteq.sml 'root-eq + subpbl: solve_linear' neuper@37906: until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"... neuper@37906: > val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_, neuper@37906: Nd(PblObj{origin=(oris,_,_),...},[])]) = pt; neuper@37906: > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"], neuper@37906: (#where_ o get_pbt) ["linear","univariate","equation"]); neuper@37906: > match_oris oris (pbt,pre); neuper@37906: val it = true : bool neuper@37906: neuper@37906: neuper@37906: > val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"], neuper@37906: (#where_ o get_pbt)["plain_square","univariate","equation"]); neuper@37906: > match_oris oris (pbt,pre); neuper@37906: val it = false : bool neuper@37906: neuper@37906: neuper@37906: --------------------------------------------------- neuper@37906: run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square' neuper@37906: until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ... neuper@37906: > val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]), neuper@37906: Nd (PblObj {origin=(oris,_,_),...},[])]) = pt; neuper@37906: > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"], neuper@37906: (#where_ o get_pbt) ["linear","univariate","equation"]); neuper@37906: > match_oris oris (pbt,pre); neuper@37906: val it = false : bool neuper@37906: neuper@37906: neuper@37906: > val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"], neuper@37906: (#where_ o get_pbt) ["plain_square","univariate","equation"]); neuper@37906: > match_oris oris (pbt,pre); neuper@37906: val it = true : bool neuper@37906: *) neuper@37906: (*^^^--- doubled 20.9.01 *) neuper@37906: neuper@37906: neuper@37906: (*. check a problem (ie. ori list) for matching a problemtype, neuper@37906: returns items for output to math-experts .*) neuper@37906: (* val (ppc,pre) = (#ppc py, #where_ py); neuper@37906: *) neuper@37906: fun match_oris' thy oris (ppc,pre,prls) = neuper@37906: (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls)); neuper@37906: *) neuper@37906: let val itms = (flat o (map (chk1_ thy ppc))) oris; neuper@37906: val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris; neuper@37906: val mvat = max_vt itms; neuper@37906: val miss = chk1_mis' oris ppc; neuper@37906: val pre' = check_preconds' prls pre itms mvat neuper@37906: val pb = foldl and_ (true, map fst pre') neuper@37906: in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; neuper@37906: neuper@37906: (*. for the user .*) neuper@37906: datatype match' = neuper@37906: Matches' of item ppc neuper@37906: | NoMatch' of item ppc; neuper@37906: neuper@37906: (*. match a formalization with a problem type .*) neuper@37906: fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) = neuper@37906: let val oris = prep_ori fmz thy ppc; neuper@37906: val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er); neuper@37906: in if bool then Matches' (itms2itemppc thy itms pre') neuper@37906: else NoMatch' (itms2itemppc thy itms pre') end; neuper@37906: (* neuper@37906: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", neuper@37906: "solveFor x","errorBound (eps=0)","solutions L"]; neuper@37906: val pbt as {thy = thy, where_ = pre, ppc = ppc,...} = neuper@37906: get_pbt ["univariate","equation"]; neuper@37906: match_pbl fmz pbt; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*. refine a problem; construct pblRD while scanning .*) neuper@37906: (* val (pblRD,ori)=("xxx",oris); neuper@37906: val py = get_pbt ["equation"]; neuper@37906: val py = get_pbt ["univariate","equation"]; neuper@37906: val py = get_pbt ["linear","univariate","equation"]; neuper@37986: val py = get_pbt ["root'","univariate","equation"]; neuper@37906: match_oris (#prls py) ori (#ppc py, #where_ py); neuper@37906: neuper@37906: *) neuper@37906: fun refin (pblRD:pblRD) ori neuper@37906: ((Ptyp (pI,[py],[])):pbt ptyp) = neuper@37906: if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) neuper@37926: then SOME ((pblRD @ [pI]):pblRD) neuper@37926: else NONE neuper@37906: | refin pblRD ori (Ptyp (pI,[py],pys)) = neuper@37906: if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) neuper@37906: then (case refins (pblRD @ [pI]) ori pys of neuper@37926: SOME pblRD' => SOME pblRD' neuper@37926: | NONE => SOME (pblRD @ [pI])) neuper@37926: else NONE neuper@37926: and refins pblRD ori [] = NONE neuper@37906: | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) = neuper@37906: (case refin pblRD ori p of neuper@37926: SOME pblRD' => SOME pblRD' neuper@37926: | NONE => refins pblRD ori pts); neuper@37906: neuper@37906: (*. refine a problem; version providing output for math-experts .*) neuper@37906: fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) = neuper@37906: (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) = neuper@37906: (rev ["linear","system"], fmz, [(*match list*)], neuper@37906: ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp)); neuper@37906: *) neuper@38015: let val _ = (tracing o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI]) neuper@37906: val {thy,ppc,where_,prls,...} = py neuper@37906: val oris = prep_ori fmz thy ppc neuper@37906: (*8.3.02: itms!: oris ev. are _not_ complete here*) neuper@37906: val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls) neuper@37906: in if b then pbls @ [Matches (rev (pblRD @ [pI]), neuper@37906: itms2itemppc thy itms pre')] neuper@37906: else pbls @ [NoMatch (rev (pblRD @ [pI]), neuper@37906: itms2itemppc thy itms pre')] neuper@37906: end neuper@37906: (* val pblRD = ["pbla"]; val fmz = fmz1; val pbls = []; neuper@37906: val Ptyp (pI,[py],pys) = hd (!ptyps); neuper@37906: refin' pblRD fmz pbls (Ptyp (pI,[py],pys)); neuper@37906: *) neuper@37906: | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) = neuper@38015: let val _ = (tracing o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI]) neuper@37906: val {thy,ppc,where_,prls,...} = py neuper@37906: val oris = prep_ori fmz thy ppc; neuper@37906: (*8.3.02: itms!: oris ev. are _not_ complete here*) neuper@37906: val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls); neuper@37906: in if b neuper@37906: then let val pbl = Matches (rev (pblRD @ [pI]), neuper@37906: itms2itemppc thy itms pre') neuper@37906: in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end neuper@37906: else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]) neuper@37906: end neuper@37906: and refins' pblRD fmz pbls [] = pbls neuper@37906: | refins' pblRD fmz pbls ((p as Ptyp (pI,_,_))::pts) = neuper@37906: let val pbls' = refin' pblRD fmz pbls p neuper@37906: in case last_elem pbls' of neuper@37906: Matches _ => pbls' neuper@37906: | NoMatch _ => refins' pblRD fmz pbls' pts end; neuper@37906: neuper@37906: (*. refine a problem; version for tactic Refine_Problem .*) neuper@37906: fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) = neuper@38015: let (*val _ = tracing("### refin''1: pI="^pI);*) neuper@37906: val {thy,ppc,where_,prls,...} = py neuper@37906: val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls); neuper@37906: in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))] neuper@37906: else pbls @ [NoMatch_] neuper@37906: end neuper@37906: (* val pblRD = (rev o tl) pblID; val pbls = []; neuper@37906: val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps); neuper@37906: *) neuper@37906: | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) = neuper@38015: let (*val _ = tracing("### refin''2: pI="^pI);*) neuper@37906: val {thy,ppc,where_,prls,...} = py neuper@37906: val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls); neuper@37906: in if b neuper@37906: then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre')) neuper@37906: in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end neuper@37906: else (pbls @ [NoMatch_]) neuper@37906: end neuper@37906: and refins'' thy pblRD itms pbls [] = pbls neuper@37906: | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) = neuper@37906: let val pbls' = refin'' thy pblRD itms pbls p neuper@37906: in case last_elem pbls' of neuper@37906: Match_ _ => pbls' neuper@37906: | NoMatch_ => refins'' thy pblRD itms pbls' pts end; neuper@37906: neuper@37906: neuper@37906: (*. apply a fun to a ptyps node; copied from get_py .*) neuper@37906: fun app_ptyp f (d:pblID) _ [] = neuper@38031: error ("app_ptyp not found: "^(strs2str d)) neuper@37906: | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) = neuper@37906: if k=k' then f p neuper@37906: else app_ptyp f d ([k]:pblRD) pys neuper@37906: | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') = neuper@37906: if k=k' then app_ptyp f d ks pys neuper@37906: else app_ptyp f d (k::ks) pys'; neuper@37906: neuper@37906: (*. for tactic Refine_Tacitly .*) neuper@37906: (*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*) neuper@37906: (* val (thy,pblID) = (assoc_thy dI',pI); neuper@37906: *) neuper@37906: fun refine_ori oris (pblID:pblID) = neuper@37906: let val opt = app_ptyp (refin ((rev o tl) pblID) oris) neuper@37906: pblID (rev pblID) (!ptyps); neuper@37906: in case opt of neuper@37926: SOME pblRD => let val (pblID':pblID) =(rev pblRD) neuper@37926: in if pblID' = pblID then NONE neuper@37926: else SOME pblID' end neuper@37926: | NONE => NONE end; neuper@37906: fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI; neuper@37906: neuper@37906: (*. for tactic Refine_Problem .*); neuper@37906: (* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *) neuper@37906: (* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps); neuper@37906: *) neuper@37906: fun refine_pbl thy (pblID:pblID) itms = neuper@37906: case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms []) neuper@37906: pblID (rev pblID) (!ptyps)) of neuper@37926: NONE => NONE neuper@37926: | SOME (Match_ (rfd as (pI',_))) => neuper@37926: if pblID = pI' then NONE else SOME rfd; neuper@37906: neuper@37906: neuper@37906: (*. for math-experts .*) neuper@37906: (*19.10.02FIXME: needs thy for parsing fmz*) neuper@37906: (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID; neuper@37906: val pbls = []; val ptys = !ptyps; neuper@37906: *) neuper@37906: fun refine (fmz:fmz_) (pblID:pblID) = neuper@37906: app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps); neuper@37906: neuper@37906: neuper@37906: (*.make a guh from a reference to an element in the kestore; neuper@37906: EXCEPT theory hierarchy ... compare 'fun keref2xml'.*) neuper@37906: fun pblID2guh (pblID:pblID) = neuper@37906: (((#guh o get_pbt) pblID) neuper@38031: handle _ => error ("pblID2guh: not for '"^strs2str' pblID ^ "'")); neuper@37906: fun metID2guh (metID:metID) = neuper@37906: (((#guh o get_met) metID) neuper@38031: handle _ => error ("metID2guh: no 'Met_' for '"^ neuper@37906: strs2str' metID ^ "'")); neuper@37906: fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID neuper@37906: | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID neuper@37906: | kestoreID2guh ketype kestoreID = neuper@38031: error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^ neuper@37906: strs2str' kestoreID ^ "'"); neuper@37906: neuper@37906: fun show_pblguhs () = neuper@37906: (print_depth 999; neuper@38015: (tracing o strs2str o (map linefeed)) (coll_pblguhs (!ptyps)); neuper@37906: print_depth 3); neuper@37906: fun sort_pblguhs () = neuper@37906: (print_depth 999; neuper@38015: (tracing o strs2str o (map linefeed)) neuper@37906: (((sort string_ord) o coll_pblguhs) (!ptyps)); neuper@37906: print_depth 3); neuper@37906: neuper@37906: fun show_metguhs () = neuper@37906: (print_depth 999; neuper@38015: (tracing o strs2str o (map linefeed)) (coll_metguhs (!mets)); neuper@37906: print_depth 3); neuper@37906: fun sort_metguhs () = neuper@37906: (print_depth 999; neuper@38015: (tracing o strs2str o (map linefeed)) neuper@37906: (((sort string_ord) o coll_metguhs) (!mets)); neuper@37906: print_depth 3);