1 (* the problems and methods as stored in hierarchies
2 author Walther Neuper 1998, Mathias Lehnfeld
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 @{theory Script}))
11 "unknown::'a => unknow";
12 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
17 fun itm_2item thy (Cor ((d,ts),_)) =
18 Correct (term2str (comp_dts (d,ts)))
19 | itm_2item _ (Syn c) = SyntaxE c
20 | itm_2item _ (Typ c) = TypeE c
21 | itm_2item thy (Inc ((d,ts),_)) =
22 Incompl (term2str (comp_dts (d,ts)))
23 | itm_2item thy (Sup (d,ts)) =
24 Superfl (term2str (comp_dts (d,ts)))
25 | itm_2item _ (Mis (d,pid)) =
26 Missing (term2str d ^ " " ^ term2str pid);
30 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list)
31 handle _ => error ("get_dsc_in not for "^sel);
34 ((get_dsc_in dscppc "#Given") @
35 (get_dsc_in dscppc "#Find") @
36 (get_dsc_in dscppc "#Relate")):term list;
39 fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel)));
41 (get_dsc_of pblID "#Given") @
42 (get_dsc_of pblID "#Find") @
43 (get_dsc_of pblID "#Relate");
46 fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
47 {Given=map f gi, Where=map f wh,
48 Find=map f fi, With=map f wi, Relate=map f re}:'b ppc;
49 fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
50 {Given=f gi, Where=f wh,
51 Find=f fi, With=f wi, Relate=f re}:'b ppc;
53 (*for ppc of changing type*)
56 "#Given" => #Given (ppc:'a ppc)
57 | "#Where" => #Where (ppc:'a ppc)
58 | "#Find" => #Find (ppc:'a ppc)
59 | "#With" => #With (ppc:'a ppc)
60 | "#Relate" => #Relate (ppc:'a ppc)
61 | _ => error ("sel_ppc tried to select by '"^sel^"'");
64 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
66 "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
67 | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
68 | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
69 | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
70 | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
71 | _ => error ("repl_sel_ppc tried to select by '"^sel^"'");
73 fun add_sel_ppc thy sel
74 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
76 "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
77 | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}
78 | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
79 | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
80 | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
81 | _ => error ("add_sel_ppc tried to select by '"^sel^"'");
82 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
83 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
85 (*decompose a problem-type into description and identifier
86 FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
88 (let val (hd,args) = strip_comb t
91 else (e_term, [t]) (*??? 9.01 just copied*)
93 handle _ => error ("split_dsc: called with " ^ term2str t);
95 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
97 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
99 > val t3 = (term_of o the o (parse thy)) "valuesFor vs_";
101 (Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
102 Free ("vs_","bool List.list")) : term * term*)
106 (*. take the first two return-values; for prep_ori .*)
107 (*WN.13.5.03fun split_dts' thy t =
108 let val (d, ts, _) = split_dts thy t
110 (*WN.8.12.03 quick for prep_ori'*)
112 (let val dsc $ var = t
114 handle _ => error ("split_dsc': called with "^term2str t);
117 (* split a term into description and (id | structured variable)
120 (let val (hd,[arg]) = strip_comb t
123 error ("split_did: doesn't match (hd,[arg]) for t = " ^term2str t);
127 (*create output-string for itm_*)
128 fun itm_out thy (Cor ((d,ts),_)) = term2str (comp_dts (d,ts))
129 | itm_out thy (Syn c) = c
130 | itm_out thy (Typ c) = c
131 | itm_out thy (Inc ((d,ts),_)) = term2str (comp_dts (d,ts))
132 | itm_out thy (Sup (d,ts)) = term2str (comp_dts (d,ts))
133 | itm_out thy (Mis (d,pid)) = term2str d ^ " " ^ term2str pid;
135 fun boolterm2item (true, term) = Correct (term2str term)
136 | boolterm2item (false, term) = False (term2str term);
138 (* use"ME/modspec.sml";
140 fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) =
142 fun coll ppc [] = ppc
143 | coll ppc ((_,_,_,field,itm_)::itms) =
144 coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
145 val gfr = coll empty_ppc itms;
146 in add_where gfr (map boolterm2item pre) end;
149 compare d and dsc in pbt and transfer field to pre-ori *)
150 fun add_field thy pbt (d,ts) =
151 let fun eq d pt = (d = (fst o snd) pt);
152 in case filter (eq d) pbt of
153 [(fi,(dsc,_))] => (fi,d,ts)
154 | [] => ("#undef",d,ts) (*may come with met.ppc*)
155 | _ => error ("add_field: " ^ term2str d ^ " more than once in pbt")
158 (*. take over field from met.ppc at 'Specify_Method' into ori,
159 i.e. also removes "#undef" fields .*)
160 (* val (mpc, ori) = ((#ppc o get_met) mID, oris);
162 fun add_field' thy mpc (ori:ori list) =
163 let fun eq d pt = (d = (fst o snd) pt);
164 fun repl mpc (i,v,_,d,ts) =
165 case filter (eq d) mpc of
166 [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
167 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
168 | _ => error ("add_field': " ^ term2str d ^ " more than once in met");
169 in (flat ((map (repl mpc)) ori)):ori list end;
172 (*.mark an element with the position within a plateau;
173 a plateau with length 1 is marked with 0 .*)
174 fun mark eq [] = error "mark []"
177 fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
178 | mar xx eq (x::x'::xs) n =
179 if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)
180 else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1;
181 in mar [] eq xs 1 end;
183 > val xs = [1,1,1,2,4,4,5];
185 val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
188 (*.assumes equal descriptions to be in adjacent 'plateaus',
189 items at a certain position within the plateaus form a variant;
190 length = 1 ... marked with 0: covers all variants .*)
191 fun add_variants fdts =
193 fun eq (a,b) = curry op= (snd3 a) (snd3 b);
196 (* collect equal elements: the model for coll_variants *)
199 fun col xs eq x [] = xs @ [x]
200 | col xs eq x (y::ys) =
201 if eq(x,y) then col xs eq x ys
202 else col (xs @ [x]) eq y ys;
203 in col [] eq (hd xs) xs end;
205 > val xs = [1,1,1,2,4,4,4];
207 val it = [1,2,4] : int list
210 fun max [] = error "max of []"
213 | mx x (y::ys) = if x < y then mx y ys else mx x ys;
215 fun gen_max _ [] = error "gen_max of []"
216 | gen_max ord (y::ys) =
218 | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
224 fun coll_variants (((v,x)::vxs)) =
226 fun col xs (vs,x) [] = xs @ [(vs,x)]
227 | col xs (vs,x) ((v',x')::vxs') =
228 if x=x' then col xs (vs @ [v'], x') vxs'
229 else col (xs @ [(vs,x)]) ([v'], x') vxs';
230 in col [] ([v],x) vxs end;
231 (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
232 > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);
233 val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *)
236 fun replace_0 vm [0] = intsto vm
237 | replace_0 vm vs = vs;
239 fun add_id [] = error "add_id []"
241 let fun add n [] = []
242 | add n (x::xs) = (n,x) :: add (n+1) xs;
245 > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
247 val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]
250 fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e);
251 fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e);
252 fun flat3 (a,(b,c)) = (a,b,c);
257 (* in root (only!) fmz may be empty: fill with ..,dsc,[]
258 fun init_ori fmz thy pI =
259 if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*)
262 val fds = map (cons2 (fst, fst o snd)) (get_pbt pI);
263 val vfds = map ((pair [1]) o (rpair [])) fds;
264 val ivfds = add_id vfds
265 in (map flattup' ivfds):ori list end; 10.3.00---*)
266 (* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];
267 val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
268 val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
271 fun prep_ori [] _ _ = ([], e_ctxt)
272 | prep_ori fmz thy pbt =
274 val ctxt = Proof_Context.init_global thy |> fold declare_constraints fmz;
275 val ori = map (add_field thy pbt o split_dts o the o parseNEW ctxt) fmz
277 val maxv = map fst ori |> max;
278 val maxv = if maxv = 0 then 1 else maxv;
279 val oris = coll_variants ori
280 |> map (replace_0 maxv |> apfst)
286 val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat
287 val e_fillpat = ("e_fillpatID", parse_patt @{theory} "?a = _", "e_errpatID")
290 (**+ breadth-first search on hierarchy of problem-types +**)
292 type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)
293 (* eg. ["equations","univariate","normalize"] while
294 ["normalize","univariate","equations"] is the related pblID
295 WN.24.4.03: also used for metID*)
297 fun app_py p f (d:pblID) (k:pblRD) = let
299 error ("app_py: not found: " ^ (strs2str d));
300 fun app_py' _ [] = py_err ()
301 | app_py' [] _ = py_err ()
302 | app_py' [k0] ((p' as Ptyp (k', _, _ ))::ps) =
303 if k0 = k' then f p' else app_py' [k0] ps
304 | app_py' (k' as (k0::ks)) (Ptyp (k'', _, ps)::ps') =
305 if k0 = k'' then app_py' ks ps else app_py' k' ps';
309 fun extract_py (Ptyp (_, [py], _)) = py
310 | extract_py _ = error ("extract_py: Ptyp has wrong format.");
311 in app_py p extract_py end;
314 [Ptyp ("1",[("ptyp 1",([],[]))],
315 [Ptyp ("11",[("ptyp 11",([],[]))],
318 Ptyp ("2",[("ptyp 2",([],[]))],
319 [Ptyp ("21",[("ptyp 21",([],[]))],
323 > get_py SqRoot.thy ["1"] ["1"] (!ptyps);
324 > get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);
325 _REVERSE_ .......... !!!!!!!!!!*)
327 (*. apply a fun to a ptyps node .*)
328 fun app_ptyp x = app_py (get_ptyps ()) x;
330 (*TODO: search generalized for subthy*)
331 fun get_pbt (pblID:pblID) = get_py (get_ptyps ()) pblID (rev pblID)
332 (* get_pbt thy ["1"];
333 get_pbt thy ["21","2"];
336 (*TODO: throws exn 'get_pbt not found: ' ... confusing !!
337 take 'ketype' as an argument !!!!!*)
338 fun get_met (metID:metID) = get_py (get_mets ()) metID metID;
339 fun get_the (theID:theID) = get_py (!thehier) theID theID;
344 let fun del k ptyps [] = ptyps
345 | del k ptyps ((Ptyp (k', [p], ps))::pys) =
346 if k=k' then del k ptyps pys
347 else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
348 in del k [] ptyps end;
351 fun coll_metguhs mets =
352 let fun node coll (Ptyp (_,[n],ns)) =
353 [(#guh : met -> guh) n]
354 and nodes coll [] = coll
355 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
356 in nodes [] mets end;
358 (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
359 fun guh2kestoreID (guh:guh) =
360 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
362 let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
364 then SOME ((ids@[id]) : kestoreID)
365 else nodes (ids@[id]) gu ns
366 and nodes _ _ [] = NONE
367 | nodes ids gu (n::ns) =
368 case node ids gu n of SOME id => SOME id
369 | NONE => nodes ids gu ns
370 in case nodes [] guh (get_ptyps ()) of
372 | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
373 "not found in ptyps")
376 let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =
378 then SOME ((ids@[id]) : kestoreID)
379 else nodes (ids@[id]) gu ns
380 and nodes _ _ [] = NONE
381 | nodes ids gu (n::ns) =
382 case node ids gu n of SOME id => SOME id
383 | NONE => nodes ids gu ns
384 in case nodes [] guh (get_mets ()) of
386 | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
387 "not found in (!mets)") end
388 | _ => error ("guh2kestoreID called with '" ^ guh ^ "'");
389 (*> guh2kestoreID "pbl_equ_univ_lin";
390 val it = ["linear", "univariate", "equation"] : string list*)
393 (* val (guh, mets) = ("met_test", !mets);
395 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
396 if member op = (coll_metguhs mets) guh
397 then error ("check_guh_unique failed with '"^guh^"';\n"^
398 "use 'sort_metguhs()' for a list of guhs;\n"^
399 "consider setting 'check_guhs_unique := false'")
404 (*.the metID has the root-element as first.*)
405 fun store_met (met as {guh,...}, metID) =
406 (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
407 mets:= insrt metID met metID (!mets));
410 (*. prepare problem-types before storing in pbltypes;
411 dont forget to 'check_guh_unique' before ins.*)
412 fun prep_pbt thy guh maa init
413 (pblID, dsc_dats: (string * (string list)) list,
414 ev:rls, ca: string option, metIDs:metID list) =
415 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
416 ev:rls, ca: string option, metIDs:metID list)) =
417 ((EqSystem.thy, (["system"],
418 [("#Given" ,["equalities es_", "solveForVars vs_"]),
419 ("#Find" ,["solution ss___"](*___ is copy-named*))
421 append_rls "e_rls" e_rls [(*for preds in where_*)],
422 SOME "solveSystem es_ vs_",
425 let fun eq f (f', _) = f = f';
426 val gi = filter (eq "#Given") dsc_dats;
427 (*val gi = [("#Given",["equality e_","solveFor v_"])]
428 : (string * string list) list*)
432 ((map (split_did o term_of o the o (parse thy)) gi')
434 ("prep_pbt: syntax error in '#Given' of "^
437 (error ("prep_pbt: more than one '#Given' in "^
440 [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")),
441 (Const ("Descript.solveFor","RealDef.real => Tools.una"),
442 Free ("v_","RealDef.real"))] : (term * term) list *)
443 val gi = map (pair "#Given") gi;
446 (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))),
448 (Const ("Descript.solveFor","RealDef.real => Tools.una"),
449 Free ("v_","RealDef.real")))] : (string * (term * term)) list*)
451 val fi = filter (eq "#Find") dsc_dats;
453 [] => [](*28.8.01: ["tool"] ...// error
454 ("prep_pbt: no '#Find' in "^(strs2str pblID))*)
455 (* val ((_,fi')::[]) = fi;
458 ((map (split_did o term_of o the o (parse thy)) fi')
460 ("prep_pbt: syntax error in '#Find' of "^
463 (error ("prep_pbt: more than one '#Find' in "^
465 val fi = map (pair "#Find") fi;
467 val re = filter (eq "#Relate") dsc_dats;
471 ((map (split_did o term_of o the o (parse thy)) re')
473 ("prep_pbt: syntax error in '#Relate' of "^
476 (error ("prep_pbt: more than one '#Relate' in "^
478 val re = map (pair "#Relate") re;
480 val wh = filter (eq "#Where") dsc_dats;
484 ((map (parse_patt thy) wh')
486 ("prep_pbt: syntax error in '#Where' of "^
489 (error ("prep_pbt: more than one '#Where' in "^
491 in ({guh=guh,mathauthors=maa,init=init,
492 thy=thy,cas= case ca of NONE => NONE
494 SOME ((term_of o the o (parse thy)) s),
495 prls=ev,where_=wh,ppc= gi @ fi @ re,
496 met=metIDs}, pblID):pbt * pblID end;
497 (* prep_pbt thy (pblID, dsc_dats, metIDs);
500 ppc=[("#Given",(Const (#,#),Free (#,#))),
501 ("#Given",(Const (#,#),Free (#,#))),
502 ("#Find",(Const (#,#),Free (#,#)))],
503 thy={ProtoPure, ..., Atools, RatArith},
504 where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $
505 Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *)
510 (*. prepare met for storage analogous to pbt .*)
511 fun prep_met thy guh maa init
512 (metID, ppc: (string * string list) list (*'#Where' -> #pre*),
513 {rew_ord'=ro, rls'=rls, srls=srls, prls=prls,
514 calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
515 crls=cr, errpats = ep, nrls= nr}, scr) =
516 let fun eq f (f', _) = f = f';
517 (*val thy = (assoc_thy o fst) metID*)
518 val gi = filter (eq "#Given") ppc;
520 [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])
522 ((map (split_did o term_of o the o (parse thy)) gi')
524 ("prep_pbt: syntax error in '#Given' of "^
527 (error ("prep_pbt: more than one '#Given' in "^
529 val gi = map (pair "#Given") gi;
531 val fi = filter (eq "#Find") ppc;
533 [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])
535 ((map (split_did o term_of o the o (parse thy)) fi')
537 ("prep_pbt: syntax error in '#Find' of "^
540 (error ("prep_pbt: more than one '#Find' in "^
542 val fi = map (pair "#Find") fi;
544 val re = filter (eq "#Relate") ppc;
546 [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])
548 ((map (split_did o term_of o the o (parse thy)) re')
550 ("prep_pbt: syntax error in '#Relate' of "^
553 (error ("prep_pbt: more than one '#Relate' in "^
555 val re = map (pair "#Relate") re;
557 val wh = filter (eq "#Where") ppc;
559 [] => (writeln ("prep_met: in " ^ guh ^ " #Where is empty ?!?"); [])
561 ((map (parse_patt thy) wh')
563 ("prep_pbt: syntax error in '#Where' of "^
566 (error ("prep_pbt: more than one '#Where' in "^
568 val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
569 in ({guh=guh,mathauthors=maa,init=init,
570 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
571 calc = if scr = "empty_script" then []
572 else ((assoc_calc' thy |> map) o (map op_of_calc) o
573 (filter is_calc) o stacpbls) sc,
574 crls=cr, errpats = ep, nrls= nr, scr = Prog sc}:met,
579 (**. get pblIDs of all entries in mat3D .**)
582 fun format_pblID strl = enclose " [" "]" (commas_quote strl);
583 fun format_pblIDl strll = enclose "[\n" "\n]\n"
584 (space_implode ",\n" (map format_pblID strll));
586 fun scan _ [] = [] (* no base case, for empty doms only *)
587 | scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]]
588 | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl
589 | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
590 | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
592 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ());
596 fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ());
600 (*vvvvv---------- preparational work 8.01. UNUSED *)
601 (**+ instantiate a problem-type +**)
603 (*+ transform oris +*)
605 fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs;
606 (*> coll_vats [11,22] (hd oris);
607 val it = [22,11,1,2,3] : int list
609 > foldl coll_vats ([],oris);
610 val it = [1,2,3] : int list
613 > filter ((curry (op mem) i) o #2) oris;
615 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
616 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
617 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
618 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
619 (6,[1],"#undef",Const (#,#),[Free #]),
620 (9,[1,2],"#undef",Const (#,#),[# $ #]),
621 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
623 local infix mem; (*from Isabelle2002*)
625 | x mem (y :: ys) = x = y orelse x mem ys;
627 fun filter_vat oris i =
628 filter ((curry (op mem) i) o (#2 : ori -> int list)) oris;
630 (*> map (filter_vat oris) [1,2,3];
632 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
633 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
634 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
635 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
636 (6,[1],"#undef",Const (#,#),[Free #]),
637 (9,[1,2],"#undef",Const (#,#),[# $ #]),
638 (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
639 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
640 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
641 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
642 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
643 (7,[2],"#undef",Const (#,#),[Free #]),
644 (9,[1,2],"#undef",Const (#,#),[# $ #]),
645 (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
646 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
647 (2,[1,2,3],"#Find",Const (#,#),[Free #]),
648 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
649 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
650 (8,[3],"#undef",Const (#,#),[Free #]),
651 (10,[3],"#undef",Const (#,#),[# $ #]),
652 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
654 fun separate_vats oris =
655 let val vats = foldl coll_vats ([] : int list, oris);
656 in map (filter_vat oris) vats end;
657 (*^^^ end preparational work 8.01.*)
661 (**. check a problem (ie. itm list) for matching a problemtype .**)
663 fun eq1 d (_,(d',_)) = (d = d');
664 fun itm_id ((i,_,_,_,_):itm) = i;
665 fun ori_id ((i,_,_,_,_):ori) = i;
666 fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm);
667 (*see + add_sel_ppc ~~~~~~~*)
668 fun field_eq f ((_,_,f',_,_):ori) = f = f';
670 (*. check an item (with arbitrary itm_ from previous matchings)
671 for matching a problemtype; returns true only for itms found in pbt .*)
672 fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
673 (case find_first (eq1 d) pbt of
674 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
675 (id, pbl_ids' d vs))):itm)
676 | NONE => (i,vats,false,f,Sup (d,vs)))
677 | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
678 (case find_first (eq1 d) pbt of
679 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
680 (id, pbl_ids' d vs))):itm)
681 | NONE => (i,vats,false,f,Sup (d,vs)))
683 | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
684 | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm
686 | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
687 (case find_first (eq1 d) pbt of
688 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
689 (id, pbl_ids' d vs))):itm)
690 | NONE => (i,vats,false,f,Sup (d,vs)))
691 (* val (i,vats,b,f,Mis (d,vs)) = i4;
693 | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
694 (case find_first (eq1 d) pbt of
695 (* val SOME (_,(_,id)) = find_first (eq1 d) pbt;
697 SOME (_,(_,id)) => error "chk_: ((i,vats,b,f,Cor ((d,vs),\
698 \(id, pbl_ids' d vs))):itm)"
699 | NONE => (i,vats,false,f,Sup (d,[vs])));
704 fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;
705 fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
706 fun eq0 ((0,_,_,_,_):itm) = true
709 | max_i i ((id,_,_,_,_)::is) =
710 if i > id then max_i i is else max_i id is;
712 | max_id ((id,_,_,_,_)::is) = max_i id is;
713 fun add_idvat itms _ _ [] = itms
714 | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) =
715 add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *)
716 ],b,f,itm_):itm]) (i+1) mvat its;
719 (*. find elements of pbt not contained in itms;
720 if such one is untouched, return this one, otherwise create new itm .*)
721 fun chk_m (itms:itm list) untouched (p as (f,(d,id))) =
722 case find_first (eq2 p) itms of
724 | NONE => (case find_first (eq2 p) untouched of
726 | NONE => [(0,[],false,f,Mis (d,id)):itm]);
727 (* val itms = itms'';
729 fun chk_mis mvat itms untouched pbt =
730 let val mis = (flat o (map (chk_m itms untouched))) pbt;
731 val mid = max_id itms;
732 in add_idvat [] (mid + 1) mvat mis end;
734 (*. check a problem (ie. itm list) for matching a problemtype,
735 takes the max_vt for concluding completeness (could be another!) .*)
736 (* val itms = itms'; val (pbt,pre) = (ppc, pre);
737 val itms = itms; val (pbt,pre) = (ppc, pre);
739 fun match_itms thy itms (pbt,pre,prls) =
740 (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat
742 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
743 val mvat = max_vt itms';
744 val itms'' = filter (okv mvat) itms';
745 val untouched = filter eq0 itms;(*i.e. dsc only (from init)*)
746 val mis = chk_mis mvat itms'' untouched pbt;
747 val pre' = check_preconds' prls pre itms'' mvat
748 val pb = foldl and_ (true, map fst pre')
749 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end);
751 (*. check a problem pbl (ie. itm list) for matching a problemtype pbt,
752 for missing items get data from formalization (ie. ori list);
753 takes the max_vt for concluding completeness (could be another!) .*)
754 (* (0) determine the most frequent variant mv in pbl
755 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
756 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
757 (3) newitms = filter (mv mem vat(news)) news
759 (* val (pbl, pbt, pre) = (met, mtt, pre);
760 val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt);
761 val (pbl, pbt, pre) = (itms, ppc, where_);
763 fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris =
765 (*0*)val mv = max_vt pbl;
767 fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
768 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
769 SOME _ => false | NONE => true;
770 (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;
772 fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
773 fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) =
774 (i,v,false,f,Mis (d,pid)):itm;
775 (*2*)fun oris2itms oris mis1 =
776 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
777 val news = (flat o (map (oris2itms oris))) mis;
778 (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv;
779 val newitms = filter mem_vat news;
780 (*4*)val itms' = pbl @ newitms;
781 val pre' = check_preconds' prls pre itms' mv
782 val pb = foldl and_ (true, map fst pre')
783 in (length mis = 0 andalso pb, (itms', pre')) end;
784 (*handle _ => (false,([],[]))*);
787 (*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris
788 allow for faster access to descriptions and terms *)
789 (**. check a problem (ie. itm list) for matching a problemtype .**)
791 (*. check an ori for matching a problemtype by description;
792 returns true only for itms found in pbt .*)
793 fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
794 case find_first (eq1 d) pbt of
795 SOME (_,(_,id)) => [(i,vats,true,f,
796 Cor ((d,vs), (id, pbl_ids' d vs))):itm]
799 (* elem 'p' of pbt contained in itms ? *)
800 fun chk1_m (itms:itm list) p =
801 case find_first (eq2 p) itms of
802 SOME _ => true | NONE => false;
803 fun chk1_m' (oris: ori list) (p as (f,(d,t))) =
804 case find_first (eq2' p) oris of
806 | NONE => [(f, Mis (d, t))];
807 fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;
809 fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
810 fun chk1_mis' oris ppc =
811 map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
814 (*. check a problem (ie. ori list) for matching a problemtype,
815 takes the max_vt for concluding completeness (FIXME could be another!) .*)
816 (* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py);
818 fun match_oris thy prls oris (pbt,pre) =
819 let val itms = (flat o (map (chk1_ thy pbt))) oris;
820 val mvat = max_vt itms;
821 val complete = chk1_mis mvat itms pbt;
822 val pre' = check_preconds' prls pre itms mvat
823 val pb = foldl and_ (true, map fst pre')
824 in if complete andalso pb then true else false end;
826 (*. check a problem (ie. ori list) for matching a problemtype,
827 returns items for output to math-experts .*)
828 fun match_oris' thy oris (ppc,pre,prls) =
829 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));
831 let val itms = (flat o (map (chk1_ thy ppc))) oris;
832 val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris;
833 val mvat = max_vt itms;
834 val miss = chk1_mis' oris ppc;
835 val pre' = check_preconds' prls pre itms mvat
836 val pb = foldl and_ (true, map fst pre')
837 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
842 | NoMatch' of item ppc;
844 (* match a formalization with a problem type *)
845 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
846 let val oris = prep_ori fmz thy ppc |> #1;
847 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
848 in if bool then Matches' (itms2itemppc thy itms pre')
849 else NoMatch' (itms2itemppc thy itms pre') end;
851 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
852 "solveFor x","errorBound (eps=0)","solutions L"];
853 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
854 get_pbt ["univariate","equation"];
859 (*. refine a problem; construct pblRD while scanning .*)
860 (* val (pblRD,ori)=("xxx",oris);
861 val py = get_pbt ["equation"];
862 val py = get_pbt ["univariate","equation"];
863 val py = get_pbt ["linear","univariate","equation"];
864 val py = get_pbt ["root'","univariate","equation"];
865 match_oris (#prls py) ori (#ppc py, #where_ py);
868 fun refin (pblRD:pblRD) ori
869 ((Ptyp (pI,[py],[])):pbt ptyp) =
870 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
871 then SOME ((pblRD @ [pI]):pblRD)
873 | refin pblRD ori (Ptyp (pI,[py],pys)) =
874 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
875 then (case refins (pblRD @ [pI]) ori pys of
876 SOME pblRD' => SOME pblRD'
877 | NONE => SOME (pblRD @ [pI]))
879 and refins pblRD ori [] = NONE
880 | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =
881 (case refin pblRD ori p of
882 SOME pblRD' => SOME pblRD'
883 | NONE => refins pblRD ori pts);
885 (*. refine a problem; version providing output for math-experts .*)
886 fun refin' (pblRD: pblRD) fmz pbls ((Ptyp (pI, [py], [])):pbt ptyp) =
888 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
889 val {thy, ppc, where_, prls, ...} = py
890 val oris = prep_ori fmz thy ppc |> #1;
891 (*8.3.02: itms!: oris ev. are _not_ complete here*)
892 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
894 then pbls @ [Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
895 else pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
898 | refin' pblRD fmz pbls (Ptyp (pI, [py], pys)) =
900 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
901 val {thy, ppc, where_, prls, ...} = py
902 val oris = prep_ori fmz thy ppc |> #1;
903 (*8.3.02: itms!: oris ev. are _not_ complete here*)
904 val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
906 then let val pbl = Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')
907 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
908 else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
911 and refins' pblRD fmz pbls [] = pbls
912 | refins' pblRD fmz pbls ((p as Ptyp (pI, _, _))::pts) =
913 let val pbls' = refin' pblRD fmz pbls p
914 in case last_elem pbls' of
916 | NoMatch _ => refins' pblRD fmz pbls' pts
919 (*. refine a problem; version for tactic Refine_Problem .*)
920 fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
921 let (*val _ = tracing("### refin''1: pI="^pI);*)
922 val {thy,ppc,where_,prls,...} = py
923 val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
924 in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
925 else pbls @ [NoMatch_]
927 (* val pblRD = (rev o tl) pblID; val pbls = [];
928 val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);
930 | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =
931 let (*val _ = tracing("### refin''2: pI="^pI);*)
932 val {thy,ppc,where_,prls,...} = py
933 val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
935 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
936 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
937 else (pbls @ [NoMatch_])
939 and refins'' thy pblRD itms pbls [] = pbls
940 | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) =
941 let val pbls' = refin'' thy pblRD itms pbls p
942 in case last_elem pbls' of
944 | NoMatch_ => refins'' thy pblRD itms pbls' pts end;
946 (*. for tactic Refine_Tacitly .*)
947 (*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*)
948 (* val (thy,pblID) = (assoc_thy dI',pI);
950 fun refine_ori oris (pblID:pblID) =
951 let val opt = app_ptyp (refin ((rev o tl) pblID) oris)
954 SOME pblRD => let val (pblID':pblID) =(rev pblRD)
955 in if pblID' = pblID then NONE
958 fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
960 (*. for tactic Refine_Problem .*);
961 (* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
962 (* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);
964 fun refine_pbl thy (pblID:pblID) itms =
965 case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms [])
966 pblID (rev pblID)) of
968 | SOME (Match_ (rfd as (pI',_))) =>
969 if pblID = pI' then NONE else SOME rfd;
972 (*. for math-experts .*)
973 (*FIXME.WN021019: needs thy for parsing fmz*)
974 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
975 val pbls = []; val ptys = !ptyps;
977 fun refine (fmz:fmz_) (pblID:pblID) =
978 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID);
981 (*.make a guh from a reference to an element in the kestore;
982 EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
983 fun pblID2guh (pblID:pblID) =
984 (((#guh o get_pbt) pblID)
985 handle _ => error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
986 fun metID2guh (metID:metID) =
987 (((#guh o get_met) metID)
988 handle _ => error ("metID2guh: no 'Met_' for '"^
989 strs2str' metID ^ "'"));
990 fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
991 | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
992 | kestoreID2guh ketype kestoreID =
993 error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
994 strs2str' kestoreID ^ "'");
996 fun show_pblguhs () =
998 (tracing o strs2str o (map linefeed)) (coll_pblguhs (get_ptyps ()));
1000 fun sort_pblguhs () =
1002 (tracing o strs2str o (map linefeed))
1003 (((sort string_ord) o coll_pblguhs) (get_ptyps ()));
1006 fun show_metguhs () =
1008 (tracing o strs2str o (map linefeed)) (coll_metguhs (get_mets ()));
1010 fun sort_metguhs () =
1012 (tracing o strs2str o (map linefeed))
1013 (((sort string_ord) o coll_metguhs) (get_mets ()));