1 (* the problems and methods as stored in hierarchies
2 author Walther Neuper 1998
3 (c) due to copyright terms
9 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
10 val dsc_unknown = (term_of o the o (parseold Script.thy))
11 "unknown::'a => unknow";
12 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
20 fun itm_2item thy (Cor ((d,ts),_))= Correct(string_of_cterm (comp_dts thy(d,ts)))
21 | itm_2item thy (Syn c) = SyntaxE c
22 | itm_2item thy (Typ c) = TypeE c
23 | itm_2item thy (Inc ((d,ts),_))= Incompl(string_of_cterm (comp_dts thy(d,ts)))
24 | itm_2item thy (Sup (d,ts)) = Superfl(string_of_cterm (comp_dts thy(d,ts)))
25 | itm_2item thy (Mis (d,pid)) =
26 Missing (Sign.string_of_term (sign_of thy) d ^" "^
27 Sign.string_of_term (sign_of thy) pid);
34 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list)
35 handle _ => error ("get_dsc_in not for "^sel);
38 ((get_dsc_in dscppc "#Given") @
39 (get_dsc_in dscppc "#Find") @
40 (get_dsc_in dscppc "#Relate")):term list;
43 fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel)));
45 (get_dsc_of pblID "#Given") @
46 (get_dsc_of pblID "#Find") @
47 (get_dsc_of pblID "#Relate");
50 fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
51 {Given=map f gi, Where=map f wh,
52 Find=map f fi, With=map f wi, Relate=map f re}:'b ppc;
53 fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
54 {Given=f gi, Where=f wh,
55 Find=f fi, With=f wi, Relate=f re}:'b ppc;
57 (*for ppc of changing type*)
60 "#Given" => #Given (ppc:'a ppc)
61 | "#Where" => #Where (ppc:'a ppc)
62 | "#Find" => #Find (ppc:'a ppc)
63 | "#With" => #With (ppc:'a ppc)
64 | "#Relate" => #Relate (ppc:'a ppc)
65 | _ => raise error ("sel_ppc tried to select by '"^sel^"'");
68 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
70 "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
71 | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
72 | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
73 | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
74 | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
75 | _ => raise error ("repl_sel_ppc tried to select by '"^sel^"'");
77 fun add_sel_ppc thy sel
78 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
80 "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
81 | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}
82 | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
83 | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
84 | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
85 | _ => raise error ("add_sel_ppc tried to select by '"^sel^"'");
86 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
87 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
89 (*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*)
92 (*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*)
96 (*decompose a problem-type into description and identifier
97 FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
99 (let val (hd,args) = strip_comb t
102 else (e_term, [t]) (*??? 9.01 just copied*)
104 handle _ => raise error ("split_dsc: called with "^
105 (Sign.string_of_term (sign_of thy) t));
107 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
109 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
111 > val t3 = (term_of o the o (parse thy)) "valuesFor vs_";
113 (Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
114 Free ("vs_","bool List.list")) : term * term*)
118 (*. take the first two return-values; for prep_ori .*)
119 (*WN.13.5.03fun split_dts' thy t =
120 let val (d, ts, _) = split_dts thy t
122 (*WN.8.12.03 quick for prep_ori'*)
124 (let val dsc $ var = t
126 handle _ => raise error ("split_dsc': called with "^term2str t);
129 (* split a term into description and (id | structured variable)
132 (let val (hd,[arg]) = strip_comb t
134 handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
135 ^(Sign.string_of_term (sign_of Script.thy) t));
139 (*create output-string for itm_*)
140 fun itm_out thy (Cor ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
141 | itm_out thy (Syn c) = c
142 | itm_out thy (Typ c) = c
143 | itm_out thy (Inc ((d,ts),_)) = (string_of_cterm (comp_dts thy(d,ts)))
144 | itm_out thy (Sup (d,ts)) = (string_of_cterm (comp_dts thy(d,ts)))
145 | itm_out thy (Mis (d,pid)) =
146 Sign.string_of_term (sign_of thy) d ^" "^
147 Sign.string_of_term (sign_of thy) pid;
150 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
156 fun coll itms' [] = itms'
157 | coll itms' (i::itms) =
159 (Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms
160 | (Syn c) => coll (itms' ) itms
161 | (Typ c) => coll (itms' ) itms
162 | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms
163 | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms
164 | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms
168 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
169 Correct (string_of_cterm (comp_dts thy(d,ts)))
170 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
171 | itm2item (_,_,_,_,Typ (c)) = TypeE c
172 | itm2item (_,_,_,_,Fal (d,ts)) =
173 False (string_of_cterm (comp_dts thy(d,ts)))
174 | itm2item (_,_,_,_,Inc (d,ts)) =
175 Incompl (string_of_cterm (comp_dts thy(d,ts)))
176 | itm2item (_,_,_,_,Sup (d,ts)) =
177 Superfl (string_of_cterm (comp_dts thy(d,ts)));
180 fun boolterm2item (true, term) = Correct (term2str term)
181 | boolterm2item (false, term) = False (term2str term);
183 (* use"ME/modspec.sml";
185 fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) =
187 fun coll ppc [] = ppc
188 | coll ppc ((_,_,_,field,itm_)::itms) =
189 coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
190 val gfr = coll empty_ppc itms;
191 in add_where gfr (map boolterm2item pre) end;
192 (*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*)
194 (*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*)
196 (* --- 9.3.fun add_field dscs (d,ts) =
197 if d mem (get_dsc_in dscs "#Given")
198 then ("#Given",d,ts:term list)
199 else if d mem (get_dsc_in dscs "#Find")
201 else if d mem (get_dsc_in dscs "#Relate")
202 then ("#Relate",d,ts)
203 else ("#undef",d,ts);
204 (* 28.1.00 raise error ("add_field: '"^
205 (Sign.string_of_term (sign_of thy) d)^
206 "' not in ppc-description "); *)
210 compare d and dsc in pbt and transfer field to pre-ori *)
211 fun add_field thy pbt (d,ts) =
212 let fun eq d pt = (d = (fst o snd) pt);
213 in case filter (eq d) pbt of
214 [(fi,(dsc,_))] => (fi,d,ts)
215 | [] => ("#undef",d,ts) (*may come with met.ppc*)
216 | _ => raise error ("add_field: "^
217 (Sign.string_of_term (sign_of thy) d)^
218 " more than once in pbt")
221 (*. take over field from met.ppc at 'Specify_Method' into ori,
222 i.e. also removes "#undef" fields .*)
223 (* val (mpc, ori) = ((#ppc o get_met) mID, oris);
225 fun add_field' thy mpc (ori:ori list) =
226 let fun eq d pt = (d = (fst o snd) pt);
227 fun repl mpc (i,v,_,d,ts) =
228 case filter (eq d) mpc of
229 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
230 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
231 (*raise error ("add_field': "^
232 (Sign.string_of_term (sign_of thy) d)^
234 | _ => raise error ("add_field': "^
235 (Sign.string_of_term (sign_of thy) d)^
236 " more than once in met");
237 in (flat ((map (repl mpc)) ori)):ori list end;
240 (*.mark an element with the position within a plateau;
241 a plateau with length 1 is marked with 0 .*)
242 fun mark eq [] = raise error "mark []"
245 fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
246 | mar xx eq (x::x'::xs) n =
247 if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)
248 else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1;
249 in mar [] eq xs 1 end;
251 > val xs = [1,1,1,2,4,4,5];
253 val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
256 (*.assumes equal descriptions to be in adjacent 'plateaus',
257 items at a certain position within the plateaus form a variant;
258 length = 1 ... marked with 0: covers all variants .*)
259 fun add_variants fdts =
261 fun eq (a,b) = curry op= (snd3 a) (snd3 b);
264 (* collect equal elements: the model for coll_variants *)
267 fun col xs eq x [] = xs @ [x]
268 | col xs eq x (y::ys) =
269 if eq(x,y) then col xs eq x ys
270 else col (xs @ [x]) eq y ys;
271 in col [] eq (hd xs) xs end;
273 > val xs = [1,1,1,2,4,4,4];
275 val it = [1,2,4] : int list
278 fun max [] = raise error "max of []"
281 | mx x (y::ys) = if x < y then mx y ys else mx x ys;
283 fun gen_max _ [] = raise error "gen_max of []"
284 | gen_max ord (y::ys) =
286 | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
292 fun coll_variants (((v,x)::vxs)) =
294 fun col xs (vs,x) [] = xs @ [(vs,x)]
295 | col xs (vs,x) ((v',x')::vxs') =
296 if x=x' then col xs (vs @ [v'], x') vxs'
297 else col (xs @ [(vs,x)]) ([v'], x') vxs';
298 in col [] ([v],x) vxs end;
299 (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
300 > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);
301 val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *)
304 fun replace_0 vm [0] = intsto vm
305 | replace_0 vm vs = vs;
307 fun add_id [] = raise error "add_id []"
309 let fun add n [] = []
310 | add n (x::xs) = (n,x) :: add (n+1) xs;
313 > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
315 val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]
318 fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e);
319 fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e);
320 fun flat3 (a,(b,c)) = (a,b,c);
325 (* in root (only!) fmz may be empty: fill with ..,dsc,[]
326 fun init_ori fmz thy pI =
327 if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*)
330 val fds = map (cons2 (fst, fst o snd)) (get_pbt pI);
331 val vfds = map ((pair [1]) o (rpair [])) fds;
332 val ivfds = add_id vfds
333 in (map flattup' ivfds):ori list end; 10.3.00---*)
334 (* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];
335 val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
336 val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
338 fun prep_ori [] _ _ = []
339 | prep_ori fmz thy pbt =
341 val ctopts = map (parse thy) fmz
342 val _= (*FIXME.WN060916 improve error report*)
343 if null (filter is_none ctopts) then ()
344 else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
345 val dts = map ((split_dts thy) o term_of o the) ctopts
346 val ori = map (add_field thy pbt) dts;
347 (* val ori = map (flat3 o (pair "#undef")) dts; *)
348 val ori' = add_variants ori;
349 val maxv = max (map fst ori');
350 val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv;
351 val ori'' = coll_variants ori';
352 val ori''' = map (apfst (replace_0 maxv)) ori'';
353 val ori'''' = add_id ori'''
354 in (map flattup ori''''):ori list end;
357 (*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
359 (*.the pattern for an item of a problems model or a methods guard.*)
360 type pat = (string * (*field*)
361 (term * (*description*)
362 term)) (*id | struct-var*);
363 fun pat2str ((field, (dsc, id)):pat) =
364 pair2str (field, pair2str (term2str dsc, term2str id));
365 fun pats2str pats = (strs2str o (map pat2str)) pats;
367 (* data for methods stored in 'methods'-database *)
369 {guh : guh, (*unique within this isac-knowledge *)
370 mathauthors: string list,(*copyright *)
371 init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
372 rew_ord' : rew_ord', (*for rules in Detail
373 TODO.WN0509 store fun itself, see 'type pbt'*)
374 erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
375 instead erls in "fun prep_met" *)
376 srls : rls, (*for evaluating list expressions in scr *)
377 prls : rls, (*for evaluating predicates in modelpattern *)
378 crls : rls, (*for check_elementwise, ie. formulae in calc.*)
379 nrls : rls, (*canonical simplifier specific for this met *)
380 calc : calc list, (*040207: <--- calclist' in fun prep_met *)
381 (*branch : TransitiveB set in append_problem at generation ob pblobj
382 FIXXXME.8.03: set branch from met in Apply_Method *)
384 (* compare type pbt:*)
386 (*.items in given, find, relate;
387 items (in "#Find") which need not occur in the arg-list of a SubProblem
388 are 'copy-named' with an identifier "*_!_".
389 copy-named items are 'generating' if they are NOT "*___"
390 see ME/calchead.sml 'fun is_copy_named'.*)
391 pre: term list, (*preconditions in where*)
393 scr: scr (*prep_met requires either script or string "empty_script"*)
395 (* ------- template ------------------------------------------------------
398 ([(*"EqSystem","normalize"*)],
399 [("#Given" ,[ (*"equalities es_", "solveForVars vs_"*)]),
400 ("#Find" ,[ (*dont forget typing non-reals *)]),
401 ("#Relate",[])(*may be omitted *) ],
402 {calc = [], (*filled autom. in prep_met *)
403 crls = Erls, (*for check_elementwise *)
404 prls = Erls, (*for evaluating preds in guard *)
405 nrls = Erls, (*can.simplifier for all formulae*)
406 rew_ord'="tless_true", (*for rules in Detail *)
407 rls' = Erls, (*erls, the eval_rls for cond. in rules*)
408 srls = Erls}, (*for evaluating list expr in scr*)
411 ---------- template ----------------------------------------------------*)
412 val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
413 rew_ord' = "e_rew_ord'": rew_ord',
414 erls = e_rls, srls = e_rls, prls = e_rls,
415 calc = [], crls = e_rls, nrls = e_rls,
416 (*asm_thm = []: thm' list,
417 asm_rls = []: rls' list,*)
418 ppc = []: (string * (term * term)) list,
420 scr = EmptyScr: scr}:met;
423 (** problem-types stored in format for usage in specify **)
425 val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
426 (term * (* description *)
427 term)) (* id | struct-var *)
431 (*deprecated due to 'type pat'*)
432 type pbt_ = (string * (* field "#Given",..*)
433 (term * (* description *)
434 term)); (* id | struct-var *)
435 val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_;
437 {guh : guh, (*unique within this isac-knowledge*)
438 mathauthors: string list, (*copyright*)
439 init : pblID, (*to start refinement with*)
440 thy : theory, (* which allows to compile that pbt
441 TODO: search generalized for subthy (ref.p.69*)
442 (*^^^ WN050912 NOT used during application of the problem,
443 because applied terms may be from 'subthy' as well as from super;
444 thus we take 'maxthy'; see match_ags !*)
445 cas : term option,(*'CAS-command'*)
446 prls : rls, (* for preds in where_*)
447 where_: term list, (* where - predicates*)
449 (*this is the model-pattern;
450 it contains "#Given","#Where","#Find","#Relate"-patterns*)
451 met : metID list}; (* methods solving the pbt*)
452 val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=ProtoPure.thy,
453 cas=None,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
454 fun pbt2 (str, (t1, t2)) =
455 pair2str (str, pair2str (term2str t1, term2str t2));
456 fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;
459 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]);
460 val e_Mets = Ptyp ("e_metID",[e_met],[]);
462 type ptyps = (pbt ptyp) list;
463 val ptyps = ref ([e_Ptyp]:ptyps);
465 type mets = (met ptyp) list;
466 val mets = ref ([e_Mets]:mets);
469 (**+ breadth-first search on hierarchy of problem-types +**)
471 type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)
472 (* eg. ["equations","univariate","normalize"] while
473 ["normalize","univariate","equations"] is the related pblID
474 WN.24.4.03: also used for metID*)
476 fun get_py thy d _ [] =
477 error ("get_pbt not found: "^(strs2str d))
478 | get_py thy d [k] ((Ptyp (k',[py],_))::pys) =
480 else get_py thy d ([k]:pblRD) pys
481 | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') =
482 if k=k' then get_py thy d ks pys
483 else get_py thy d (k::ks) pys';
485 [Ptyp ("1",[("ptyp 1",([],[]))],
486 [Ptyp ("11",[("ptyp 11",([],[]))],
489 Ptyp ("2",[("ptyp 2",([],[]))],
490 [Ptyp ("21",[("ptyp 21",([],[]))],
494 > get_py SqRoot.thy ["1"] ["1"] (!ptyps);
495 > get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);
496 _REVERSE_ .......... !!!!!!!!!!*)
498 (*TODO: search generalized for subthy*)
499 fun get_pbt (pblID:pblID) =
500 let val pblRD = rev pblID;
501 in get_py ProtoPure.thy pblID pblRD (!ptyps) end;
502 (* get_pbt thy ["1"];
503 get_pbt thy ["21","2"];
506 (*TODO: throws exn 'get_pbt not found: ' ... confusing !!
507 take 'ketype' as an argument !!!!!*)
508 fun get_met (metID:metID) = get_py ProtoPure.thy metID metID (!mets);
509 fun get_the (theID:theID) = get_py ProtoPure.thy theID theID (!thehier);
514 let fun del k ptyps [] = ptyps
515 | del k ptyps ((Ptyp (k', [p], ps))::pys) =
516 if k=k' then del k ptyps pys
517 else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
518 in del k [] ptyps end;
520 fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])]
522 | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
523 ((*writeln("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
525 then ((Ptyp (k', [pbt], ps))::pys)
526 else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
527 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
529 | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
530 ((*writeln("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
532 then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
535 then error ("insert: not found "^(strs2str (d:pblID)))
536 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
540 fun coll_pblguhs pbls =
541 let fun node coll (Ptyp (_,[n],ns)) =
542 [(#guh : pbt -> guh) n] @ (nodes coll ns)
543 and nodes coll [] = coll
544 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
545 in nodes [] pbls end;
546 fun coll_metguhs mets =
547 let fun node coll (Ptyp (_,[n],ns)) =
548 [(#guh : met -> guh) n]
549 and nodes coll [] = coll
550 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
551 in nodes [] mets end;
553 (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
554 fun guh2kestoreID (guh:guh) =
555 case (implode o (take_fromto 1 4) o explode) guh of
557 let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
559 then Some ((ids@[id]) : kestoreID)
560 else nodes (ids@[id]) gu ns
561 and nodes _ _ [] = None
562 | nodes ids gu (n::ns) =
563 case node ids gu n of Some id => Some id
564 | None => nodes ids gu ns
565 in case nodes [] guh (!ptyps) of
567 | None => error ("guh2kestoreID: '" ^ guh ^ "' " ^
568 "not found in (!ptyps)")
571 let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =
573 then Some ((ids@[id]) : kestoreID)
574 else nodes (ids@[id]) gu ns
575 and nodes _ _ [] = None
576 | nodes ids gu (n::ns) =
577 case node ids gu n of Some id => Some id
578 | None => nodes ids gu ns
579 in case nodes [] guh (!mets) of
581 | None => error ("guh2kestoreID: '" ^ guh ^ "' " ^
582 "not found in (!mets)") end
583 | _ => error ("guh2kestoreID called with '" ^ guh ^ "'");
584 (*> guh2kestoreID "pbl_equ_univ_lin";
585 val it = ["linear", "univariate", "equation"] : string list*)
588 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
589 if guh mem (coll_pblguhs pbls)
590 then error ("check_guh_unique failed with '"^guh^"';\n"^
591 "use 'sort_pblguhs()' for a list of guhs;\n"^
592 "consider setting 'check_guhs_unique := false'")
594 (* val (guh, mets) = ("met_test", !mets);
596 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
597 if guh mem (coll_metguhs mets)
598 then error ("check_guh_unique failed with '"^guh^"';\n"^
599 "use 'sort_metguhs()' for a list of guhs;\n"^
600 "consider setting 'check_guhs_unique := false'")
605 (*.the pblID has the leaf-element as first; better readability achieved;.*)
606 fun store_pbt (pbt as {guh,...}, pblID) =
607 (if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else ();
608 ptyps:= insrt pblID pbt (rev pblID) (!ptyps));
610 (*.the metID has the root-element as first; compare 'fun store_pbt'.*)
611 (* val (met as {guh,...}, metID) =
612 ((prep_met EqSystem.thy "met_eqsys" [] e_metID
615 {rew_ord'="tless_true", rls' = Erls, calc = [],
616 srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
620 fun store_met (met as {guh,...}, metID) =
621 (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
622 mets:= insrt metID met metID (!mets));
625 (*. prepare problem-types before storing in pbltypes;
626 dont forget to 'check_guh_unique' before ins.*)
627 fun prep_pbt thy guh maa init
628 (pblID, dsc_dats: (string * (string list)) list,
629 ev:rls, ca: string option, metIDs:metID list) =
630 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
631 ev:rls, ca: string option, metIDs:metID list)) =
632 ((EqSystem.thy, (["system"],
633 [("#Given" ,["equalities es_", "solveForVars vs_"]),
634 ("#Find" ,["solution ss___"](*___ is copy-named*))
636 append_rls "e_rls" e_rls [(*for preds in where_*)],
637 Some "solveSystem es_ vs_",
640 let fun eq f (f', _) = f = f';
641 val gi = filter (eq "#Given") dsc_dats;
642 (*val gi = [("#Given",["equality e_","solveFor v_"])]
643 : (string * string list) list*)
647 ((map (split_did o term_of o the o (parse thy)) gi')
649 ("prep_pbt: syntax error in '#Given' of "^
652 (error ("prep_pbt: more than one '#Given' in "^
655 [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")),
656 (Const ("Descript.solveFor","RealDef.real => Tools.una"),
657 Free ("v_","RealDef.real"))] : (term * term) list *)
658 val gi = map (pair "#Given") gi;
661 (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))),
663 (Const ("Descript.solveFor","RealDef.real => Tools.una"),
664 Free ("v_","RealDef.real")))] : (string * (term * term)) list*)
666 val fi = filter (eq "#Find") dsc_dats;
668 [] => [](*28.8.01: ["tool"] ...// raise error
669 ("prep_pbt: no '#Find' in "^(strs2str pblID))*)
670 (* val ((_,fi')::[]) = fi;
673 ((map (split_did o term_of o the o (parse thy)) fi')
674 handle _ => raise error
675 ("prep_pbt: syntax error in '#Find' of "^
678 (raise error ("prep_pbt: more than one '#Find' in "^
680 val fi = map (pair "#Find") fi;
682 val re = filter (eq "#Relate") dsc_dats;
686 ((map (split_did o term_of o the o (parse thy)) re')
687 handle _ => raise error
688 ("prep_pbt: syntax error in '#Relate' of "^
691 (raise error ("prep_pbt: more than one '#Relate' in "^
693 val re = map (pair "#Relate") re;
695 val wh = filter (eq "#Where") dsc_dats;
699 ((map (term_of o the o (parse thy)) wh')
700 handle _ => raise error
701 ("prep_pbt: syntax error in '#Where' of "^
704 (raise error ("prep_pbt: more than one '#Where' in "^
706 in ({guh=guh,mathauthors=maa,init=init,
707 thy=thy,cas= case ca of None => None
709 Some ((term_of o the o (parse thy)) s),
710 prls=ev,where_=wh,ppc= gi @ fi @ re,
711 met=metIDs}, pblID):pbt * pblID end;
712 (* prep_pbt thy (pblID, dsc_dats, metIDs);
715 ppc=[("#Given",(Const (#,#),Free (#,#))),
716 ("#Given",(Const (#,#),Free (#,#))),
717 ("#Find",(Const (#,#),Free (#,#)))],
718 thy={ProtoPure, ..., Atools, RatArith},
719 where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $
720 Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *)
725 (*. prepare met for storage analogous to pbt .*)
726 fun prep_met thy guh maa init
727 (metID, ppc: (string * string list) list (*'#Where' -> #pre*),
728 {rew_ord'=ro, rls'=rls, srls=srls, prls=prls,
729 calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
730 crls=cr, nrls=nr}, scr) =
731 let fun eq f (f', _) = f = f';
732 (*val thy = (assoc_thy o fst) metID*)
733 val gi = filter (eq "#Given") ppc;
737 ((map (split_did o term_of o the o (parse thy)) gi')
738 handle _ => raise error
739 ("prep_pbt: syntax error in '#Given' of "^
742 (raise error ("prep_pbt: more than one '#Given' in "^
744 val gi = map (pair "#Given") gi;
746 val fi = filter (eq "#Find") ppc;
748 [] => [](*28.8.01: ["tool"] ...// raise error
749 ("prep_pbt: no '#Find' in "^(strs2str metID))*)
751 ((map (split_did o term_of o the o (parse thy)) fi')
752 handle _ => raise error
753 ("prep_pbt: syntax error in '#Find' of "^
756 (raise error ("prep_pbt: more than one '#Find' in "^
758 val fi = map (pair "#Find") fi;
760 val re = filter (eq "#Relate") ppc;
764 ((map (split_did o term_of o the o (parse thy)) re')
765 handle _ => raise error
766 ("prep_pbt: syntax error in '#Relate' of "^
769 (raise error ("prep_pbt: more than one '#Relate' in "^
771 val re = map (pair "#Relate") re;
773 val wh = filter (eq "#Where") ppc;
777 ((map (term_of o the o (parse thy)) wh')
778 handle _ => raise error
779 ("prep_pbt: syntax error in '#Where' of "^
782 (raise error ("prep_pbt: more than one '#Where' in "^
784 val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
785 in ({guh=guh,mathauthors=maa,init=init,
786 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
787 calc = if scr = "empty_script" then []
788 else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
789 (filter is_calc) o stacpbls) sc,
790 crls=cr, nrls=nr, scr=Script sc}:met,
795 (**. get pblIDs of all entries in mat3D .**)
798 fun format_pblID strl = enclose " [" "]" (commas_quote strl);
799 fun format_pblIDl strll = enclose "[\n" "\n]\n"
800 (space_implode ",\n" (map format_pblID strll));
802 fun scan _ [] = [] (* no base case, for empty doms only *)
803 | scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]]
804 | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl
805 | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
806 | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
808 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);
812 fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);
816 (*vvvvv---------- preparational work 8.01. UNUSED *)
817 (**+ instantiate a problem-type +**)
819 (*+ transform oris +*)
821 fun coll_vats (vats, ((_,vs,_,_,_):ori)) = vats union vs;
822 (*> coll_vats [11,22] (hd oris);
823 val it = [22,11,1,2,3] : int list
825 > foldl coll_vats ([],oris);
826 val it = [1,2,3] : int list
829 > filter ((curry (op mem) i) o #2) oris;
831 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
832 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
833 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
834 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
835 (6,[1],"#undef",Const (#,#),[Free #]),
836 (9,[1,2],"#undef",Const (#,#),[# $ #]),
837 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
839 fun filter_vat oris i = filter ((curry (op mem) i)o(#2:ori -> int list))oris;
840 (*> map (filter_vat oris) [1,2,3];
842 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
843 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
844 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
845 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
846 (6,[1],"#undef",Const (#,#),[Free #]),
847 (9,[1,2],"#undef",Const (#,#),[# $ #]),
848 (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
849 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
850 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
851 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
852 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
853 (7,[2],"#undef",Const (#,#),[Free #]),
854 (9,[1,2],"#undef",Const (#,#),[# $ #]),
855 (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
856 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
857 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
858 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
859 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
860 (8,[3],"#undef",Const (#,#),[Free #]),
861 (10,[3],"#undef",Const (#,#),[# $ #]),
862 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
865 fun separate_vats oris =
866 let val vats = foldl coll_vats ([],oris);
867 in map (filter_vat oris) vats end;
868 (*^^^ end preparational work 8.01.*)
872 (**. check a problem (ie. itm list) for matching a problemtype .**)
874 fun eq1 d (_,(d',_)) = (d = d');
875 fun itm_id ((i,_,_,_,_):itm) = i;
876 fun ori_id ((i,_,_,_,_):ori) = i;
877 fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm);
878 (*see + add_sel_ppc ~~~~~~~*)
879 fun field_eq f ((_,_,f',_,_):ori) = f = f';
881 (*. check an item (with arbitrary itm_ from previous matchings)
882 for matching a problemtype; returns true only for itms found in pbt .*)
883 fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
884 (case find_first (eq1 d) pbt of
885 Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
886 (id, pbl_ids' thy d vs))):itm)
887 | None => (i,vats,false,f,Sup (d,vs)))
888 | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
889 (case find_first (eq1 d) pbt of
890 Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
891 (id, pbl_ids' thy d vs))):itm)
892 | None => (i,vats,false,f,Sup (d,vs)))
894 | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
895 | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm
897 | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
898 (case find_first (eq1 d) pbt of
899 Some (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
900 (id, pbl_ids' thy d vs))):itm)
901 | None => (i,vats,false,f,Sup (d,vs)))
902 (* val (i,vats,b,f,Mis (d,vs)) = i4;
904 | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
905 (case find_first (eq1 d) pbt of
906 (* val Some (_,(_,id)) = find_first (eq1 d) pbt;
908 Some (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
909 \(id, pbl_ids' d vs))):itm)"
910 | None => (i,vats,false,f,Sup (d,[vs])));
915 fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;
916 fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
917 fun eq0 ((0,_,_,_,_):itm) = true
920 | max_i i ((id,_,_,_,_)::is) =
921 if i > id then max_i i is else max_i id is;
923 | max_id ((id,_,_,_,_)::is) = max_i id is;
924 fun add_idvat itms _ _ [] = itms
925 | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) =
926 add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *)
927 ],b,f,itm_):itm]) (i+1) mvat its;
930 (*. find elements of pbt not contained in itms;
931 if such one is untouched, return this one, otherwise create new itm .*)
932 fun chk_m (itms:itm list) untouched (p as (f,(d,id))) =
933 case find_first (eq2 p) itms of
935 | None => (case find_first (eq2 p) untouched of
937 | None => [(0,[],false,f,Mis (d,id)):itm]);
938 (* val itms = itms'';
940 fun chk_mis mvat itms untouched pbt =
941 let val mis = (flat o (map (chk_m itms untouched))) pbt;
942 val mid = max_id itms;
943 in add_idvat [] (mid + 1) mvat mis end;
945 (*. check a problem (ie. itm list) for matching a problemtype,
946 takes the max_vt for concluding completeness (could be another!) .*)
947 (* val itms = itms'; val (pbt,pre) = (ppc, pre);
948 val itms = itms; val (pbt,pre) = (ppc, pre);
950 fun match_itms thy itms (pbt,pre,prls) =
951 (let fun okv mvat (_,vats,b,_,_) = mvat mem vats andalso b;
952 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
953 val mvat = max_vt itms';
954 val itms'' = filter (okv mvat) itms';
955 val untouched = filter eq0 itms;(*i.e. dsc only (from init)*)
956 val mis = chk_mis mvat itms'' untouched pbt;
957 val pre' = check_preconds' prls pre itms'' mvat
958 val pb = foldl and_ (true, map fst pre')
959 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end);
961 (*. check a problem pbl (ie. itm list) for matching a problemtype pbt,
962 for missing items get data from formalization (ie. ori list);
963 takes the max_vt for concluding completeness (could be another!) .*)
964 (* (0) determine the most frequent variant mv in pbl
965 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
966 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
967 (3) newitms = filter (mv mem vat(news)) news
969 (* val (pbl, pbt, pre) = (met, mtt, pre);
970 val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt);
971 val (pbl, pbt, pre) = (itms, ppc, where_);
973 fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris =
975 (*0*)val mv = max_vt pbl;
977 fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
978 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
979 Some _ => false | None => true;
980 (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;
982 fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
983 fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) =
984 (i,v,false,f,Mis (d,pid)):itm;
985 (*2*)fun oris2itms oris mis1 =
986 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
987 val news = (flat o (map (oris2itms oris))) mis;
988 (*3*)fun mem_vat (_,vats,b,_,_) = mv mem vats;
989 val newitms = filter mem_vat news;
990 (*4*)val itms' = pbl @ newitms;
991 val pre' = check_preconds' prls pre itms' mv
992 val pb = foldl and_ (true, map fst pre')
993 in (length mis = 0 andalso pb, (itms', pre')) end;
994 (*handle _ => (false,([],[]))*);
997 (*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris
998 allow for faster access to descriptions and terms *)
999 (**. check a problem (ie. itm list) for matching a problemtype .**)
1001 (*. check an ori for matching a problemtype by description;
1002 returns true only for itms found in pbt .*)
1003 fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
1004 case find_first (eq1 d) pbt of
1005 Some (_,(_,id)) => [(i,vats,true,f,
1006 Cor ((d,vs), (id, pbl_ids' thy d vs))):itm]
1009 (* elem 'p' of pbt contained in itms ? *)
1010 fun chk1_m (itms:itm list) p =
1011 case find_first (eq2 p) itms of
1012 Some _ => true | None => false;
1013 fun chk1_m' (oris: ori list) (p as (f,(d,t))) =
1014 case find_first (eq2' p) oris of
1016 | None => [(f, Mis (d, t))];
1017 fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;
1019 fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
1020 fun chk1_mis' oris ppc =
1021 map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
1024 (*. check a problem (ie. ori list) for matching a problemtype,
1025 takes the max_vt for concluding completeness (FIXME could be another!) .*)
1026 (* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py);
1028 fun match_oris thy prls oris (pbt,pre) =
1029 let val itms = (flat o (map (chk1_ thy pbt))) oris;
1030 val mvat = max_vt itms;
1031 val complete = chk1_mis mvat itms pbt;
1032 val pre' = check_preconds' prls pre itms mvat
1033 val pb = foldl and_ (true, map fst pre')
1034 in if complete andalso pb then true else false end;
1035 (*run subp-rooteq.sml 'root-eq + subpbl: solve_linear'
1036 until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"...
1037 > val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_,
1038 Nd(PblObj{origin=(oris,_,_),...},[])]) = pt;
1039 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1040 (#where_ o get_pbt) ["linear","univariate","equation"]);
1041 > match_oris oris (pbt,pre);
1042 val it = true : bool
1045 > val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"],
1046 (#where_ o get_pbt)["plain_square","univariate","equation"]);
1047 > match_oris oris (pbt,pre);
1048 val it = false : bool
1051 ---------------------------------------------------
1052 run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square'
1053 until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ...
1054 > val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]),
1055 Nd (PblObj {origin=(oris,_,_),...},[])]) = pt;
1056 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1057 (#where_ o get_pbt) ["linear","univariate","equation"]);
1058 > match_oris oris (pbt,pre);
1059 val it = false : bool
1062 > val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"],
1063 (#where_ o get_pbt) ["plain_square","univariate","equation"]);
1064 > match_oris oris (pbt,pre);
1065 val it = true : bool
1067 (*^^^--- doubled 20.9.01 *)
1070 (*. check a problem (ie. ori list) for matching a problemtype,
1071 returns items for output to math-experts .*)
1072 (* val (ppc,pre) = (#ppc py, #where_ py);
1074 fun match_oris' thy oris (ppc,pre,prls) =
1075 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));
1077 let val itms = (flat o (map (chk1_ thy ppc))) oris;
1078 val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris;
1079 val mvat = max_vt itms;
1080 val miss = chk1_mis' oris ppc;
1081 val pre' = check_preconds' prls pre itms mvat
1082 val pb = foldl and_ (true, map fst pre')
1083 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
1085 (*. for the user .*)
1087 Matches' of item ppc
1088 | NoMatch' of item ppc;
1090 (*. match a formalization with a problem type .*)
1091 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
1092 let val oris = prep_ori fmz thy ppc;
1093 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
1094 in if bool then Matches' (itms2itemppc thy itms pre')
1095 else NoMatch' (itms2itemppc thy itms pre') end;
1097 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1098 "solveFor x","errorBound (eps=0)","solutions L"];
1099 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
1100 get_pbt ["univariate","equation"];
1105 (*. refine a problem; construct pblRD while scanning .*)
1106 (* val (pblRD,ori)=("xxx",oris);
1107 val py = get_pbt ["equation"];
1108 val py = get_pbt ["univariate","equation"];
1109 val py = get_pbt ["linear","univariate","equation"];
1110 val py = get_pbt ["root","univariate","equation"];
1111 match_oris (#prls py) ori (#ppc py, #where_ py);
1114 fun refin (pblRD:pblRD) ori
1115 ((Ptyp (pI,[py],[])):pbt ptyp) =
1116 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
1117 then Some ((pblRD @ [pI]):pblRD)
1119 | refin pblRD ori (Ptyp (pI,[py],pys)) =
1120 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
1121 then (case refins (pblRD @ [pI]) ori pys of
1122 Some pblRD' => Some pblRD'
1123 | None => Some (pblRD @ [pI]))
1125 and refins pblRD ori [] = None
1126 | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =
1127 (case refin pblRD ori p of
1128 Some pblRD' => Some pblRD'
1129 | None => refins pblRD ori pts);
1131 (*. refine a problem; version providing output for math-experts .*)
1132 fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
1133 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
1134 (rev ["linear","system"], fmz, [(*match list*)],
1135 ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
1137 let val _ = (writeln o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
1138 val {thy,ppc,where_,prls,...} = py
1139 val oris = prep_ori fmz thy ppc
1140 (*8.3.02: itms!: oris ev. are _not_ complete here*)
1141 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
1142 in if b then pbls @ [Matches (rev (pblRD @ [pI]),
1143 itms2itemppc thy itms pre')]
1144 else pbls @ [NoMatch (rev (pblRD @ [pI]),
1145 itms2itemppc thy itms pre')]
1147 (* val pblRD = ["pbla"]; val fmz = fmz1; val pbls = [];
1148 val Ptyp (pI,[py],pys) = hd (!ptyps);
1149 refin' pblRD fmz pbls (Ptyp (pI,[py],pys));
1151 | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) =
1152 let val _ = (writeln o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
1153 val {thy,ppc,where_,prls,...} = py
1154 val oris = prep_ori fmz thy ppc;
1155 (*8.3.02: itms!: oris ev. are _not_ complete here*)
1156 val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
1158 then let val pbl = Matches (rev (pblRD @ [pI]),
1159 itms2itemppc thy itms pre')
1160 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
1161 else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
1163 and refins' pblRD fmz pbls [] = pbls
1164 | refins' pblRD fmz pbls ((p as Ptyp (pI,_,_))::pts) =
1165 let val pbls' = refin' pblRD fmz pbls p
1166 in case last_elem pbls' of
1168 | NoMatch _ => refins' pblRD fmz pbls' pts end;
1170 (*. refine a problem; version for tactic Refine_Problem .*)
1171 fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
1172 let (*val _ = writeln("### refin''1: pI="^pI);*)
1173 val {thy,ppc,where_,prls,...} = py
1174 val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
1175 in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
1176 else pbls @ [NoMatch_]
1178 (* val pblRD = (rev o tl) pblID; val pbls = [];
1179 val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);
1181 | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =
1182 let (*val _ = writeln("### refin''2: pI="^pI);*)
1183 val {thy,ppc,where_,prls,...} = py
1184 val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
1186 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
1187 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
1188 else (pbls @ [NoMatch_])
1190 and refins'' thy pblRD itms pbls [] = pbls
1191 | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) =
1192 let val pbls' = refin'' thy pblRD itms pbls p
1193 in case last_elem pbls' of
1195 | NoMatch_ => refins'' thy pblRD itms pbls' pts end;
1198 (*. apply a fun to a ptyps node; copied from get_py .*)
1199 fun app_ptyp f (d:pblID) _ [] =
1200 raise error ("app_ptyp not found: "^(strs2str d))
1201 | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =
1203 else app_ptyp f d ([k]:pblRD) pys
1204 | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') =
1205 if k=k' then app_ptyp f d ks pys
1206 else app_ptyp f d (k::ks) pys';
1208 (*. for tactic Refine_Tacitly .*)
1209 (*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*)
1210 (* val (thy,pblID) = (assoc_thy dI',pI);
1212 fun refine_ori oris (pblID:pblID) =
1213 let val opt = app_ptyp (refin ((rev o tl) pblID) oris)
1214 pblID (rev pblID) (!ptyps);
1216 Some pblRD => let val (pblID':pblID) =(rev pblRD)
1217 in if pblID' = pblID then None
1218 else Some pblID' end
1220 fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
1222 (*. for tactic Refine_Problem .*);
1223 (* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
1224 (* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);
1226 fun refine_pbl thy (pblID:pblID) itms =
1227 case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms [])
1228 pblID (rev pblID) (!ptyps)) of
1230 | Some (Match_ (rfd as (pI',_))) =>
1231 if pblID = pI' then None else Some rfd;
1234 (*. for math-experts .*)
1235 (*19.10.02FIXME: needs thy for parsing fmz*)
1236 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
1237 val pbls = []; val ptys = !ptyps;
1239 fun refine (fmz:fmz_) (pblID:pblID) =
1240 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps);
1243 (*.make a guh from a reference to an element in the kestore;
1244 EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
1245 fun pblID2guh (pblID:pblID) =
1246 (((#guh o get_pbt) pblID)
1247 handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
1248 fun metID2guh (metID:metID) =
1249 (((#guh o get_met) metID)
1250 handle _ => raise error ("metID2guh: no 'Met_' for '"^
1251 strs2str' metID ^ "'"));
1252 fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
1253 | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
1254 | kestoreID2guh ketype kestoreID =
1255 raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
1256 strs2str' kestoreID ^ "'");
1258 fun show_pblguhs () =
1260 (writeln o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));
1262 fun sort_pblguhs () =
1264 (writeln o strs2str o (map linefeed))
1265 (((sort string_ord) o coll_pblguhs) (!ptyps));
1268 fun show_metguhs () =
1270 (writeln o strs2str o (map linefeed)) (coll_metguhs (!mets));
1272 fun sort_metguhs () =
1274 (writeln o strs2str o (map linefeed))
1275 (((sort string_ord) o coll_metguhs) (!mets));