1 (* the problems and methods as stored in hierarchies |
|
2 author Walther Neuper 1998 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"ME/ptyps.sml"; |
|
6 use"ptyps.sml"; |
|
7 *) |
|
8 |
|
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*) |
|
13 |
|
14 |
|
15 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*) |
|
16 |
|
17 fun itm_2item thy (Cor ((d,ts),_)) = |
|
18 Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (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 (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) |
|
23 | itm_2item thy (Sup (d,ts)) = |
|
24 Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts))) |
|
25 | itm_2item _ (Mis (d,pid)) = |
|
26 Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ |
|
27 Syntax.string_of_term (thy2ctxt' "Isac") pid); |
|
28 |
|
29 |
|
30 (* --- 8.3.00 |
|
31 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list) |
|
32 handle _ => error ("get_dsc_in not for "^sel); |
|
33 |
|
34 fun dscs_in dscppc = |
|
35 ((get_dsc_in dscppc "#Given") @ |
|
36 (get_dsc_in dscppc "#Find") @ |
|
37 (get_dsc_in dscppc "#Relate")):term list; |
|
38 |
|
39 --- 26.1.88 |
|
40 fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel))); |
|
41 fun get_dsc pblID = |
|
42 (get_dsc_of pblID "#Given") @ |
|
43 (get_dsc_of pblID "#Find") @ |
|
44 (get_dsc_of pblID "#Relate"); |
|
45 --- *) |
|
46 |
|
47 fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) = |
|
48 {Given=map f gi, Where=map f wh, |
|
49 Find=map f fi, With=map f wi, Relate=map f re}:'b ppc; |
|
50 fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) = |
|
51 {Given=f gi, Where=f wh, |
|
52 Find=f fi, With=f wi, Relate=f re}:'b ppc; |
|
53 |
|
54 (*for ppc of changing type*) |
|
55 fun sel_ppc sel ppc = |
|
56 case sel of |
|
57 "#Given" => #Given (ppc:'a ppc) |
|
58 | "#Where" => #Where (ppc:'a ppc) |
|
59 | "#Find" => #Find (ppc:'a ppc) |
|
60 | "#With" => #With (ppc:'a ppc) |
|
61 | "#Relate" => #Relate (ppc:'a ppc) |
|
62 | _ => raise error ("sel_ppc tried to select by '"^sel^"'"); |
|
63 |
|
64 fun repl_sel_ppc sel |
|
65 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x = |
|
66 case sel of |
|
67 "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) |
|
68 | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re} |
|
69 | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re} |
|
70 | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re} |
|
71 | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x} |
|
72 | _ => raise error ("repl_sel_ppc tried to select by '"^sel^"'"); |
|
73 |
|
74 fun add_sel_ppc thy sel |
|
75 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x = |
|
76 case sel of |
|
77 "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) |
|
78 | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re} |
|
79 | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re} |
|
80 | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]} |
|
81 | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*) |
|
82 | _ => raise error ("add_sel_ppc tried to select by '"^sel^"'"); |
|
83 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh = |
|
84 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc); |
|
85 |
|
86 (*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*) |
|
87 |
|
88 |
|
89 (*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*) |
|
90 |
|
91 |
|
92 |
|
93 (*decompose a problem-type into description and identifier |
|
94 FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *) |
|
95 fun split_dsc thy t = |
|
96 (let val (hd,args) = strip_comb t |
|
97 in if is_dsc hd |
|
98 then (hd, args) |
|
99 else (e_term, [t]) (*??? 9.01 just copied*) |
|
100 end) |
|
101 handle _ => raise error ("split_dsc: called with "^ |
|
102 (Syntax.string_of_term (thy2ctxt' "Isac") t)); |
|
103 (* |
|
104 > val t1 = (term_of o the o (parse thy)) "errorBound err_"; |
|
105 > split_dsc t1; |
|
106 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool")) |
|
107 : term * term |
|
108 > val t3 = (term_of o the o (parse thy)) "valuesFor vs_"; |
|
109 > split_dsc t3; |
|
110 (Const ("Descript.valuesFor","bool List.list => Tools.toreall"), |
|
111 Free ("vs_","bool List.list")) : term * term*) |
|
112 |
|
113 |
|
114 |
|
115 (*. take the first two return-values; for prep_ori .*) |
|
116 (*WN.13.5.03fun split_dts' thy t = |
|
117 let val (d, ts, _) = split_dts thy t |
|
118 in (d, ts) end;*) |
|
119 (*WN.8.12.03 quick for prep_ori'*) |
|
120 fun split_dsc' t = |
|
121 (let val dsc $ var = t |
|
122 in var end) |
|
123 handle _ => raise error ("split_dsc': called with "^term2str t); |
|
124 |
|
125 (*9.3.00*) |
|
126 (* split a term into description and (id | structured variable) |
|
127 for pbt, met.ppc *) |
|
128 fun split_did t = |
|
129 (let val (hd,[arg]) = strip_comb t |
|
130 in (hd,arg) end) |
|
131 handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = " |
|
132 ^(Syntax.string_of_term (thy2ctxt' "Script") t)); |
|
133 |
|
134 |
|
135 |
|
136 (*create output-string for itm_*) |
|
137 fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
|
138 | itm_out thy (Syn c) = c |
|
139 | itm_out thy (Typ c) = c |
|
140 | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
|
141 | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
|
142 | itm_out thy (Mis (d,pid)) = |
|
143 Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ |
|
144 Syntax.string_of_term (thy2ctxt' "Isac") pid; |
|
145 |
|
146 (*22.11.00 unused |
|
147 fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*) |
|
148 |
|
149 |
|
150 (*--3.3. |
|
151 fun itms2dts itms = |
|
152 let |
|
153 fun coll itms' [] = itms' |
|
154 | coll itms' (i::itms) = |
|
155 case i of |
|
156 (Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms |
|
157 | (Syn c) => coll (itms' ) itms |
|
158 | (Typ c) => coll (itms' ) itms |
|
159 | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms |
|
160 | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms |
|
161 | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms |
|
162 in coll [] itms end; |
|
163 *) |
|
164 (*--3.3.00 |
|
165 fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = |
|
166 Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
|
167 | itm2item (_,_,_,_,Syn (c)) = SyntaxE c |
|
168 | itm2item (_,_,_,_,Typ (c)) = TypeE c |
|
169 | itm2item (_,_,_,_,Fal (d,ts)) = |
|
170 False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
|
171 | itm2item (_,_,_,_,Inc (d,ts)) = |
|
172 Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))) |
|
173 | itm2item (_,_,_,_,Sup (d,ts)) = |
|
174 Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts))); |
|
175 *) |
|
176 |
|
177 fun boolterm2item (true, term) = Correct (term2str term) |
|
178 | boolterm2item (false, term) = False (term2str term); |
|
179 |
|
180 (* use"ME/modspec.sml"; |
|
181 *) |
|
182 fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) = |
|
183 let |
|
184 fun coll ppc [] = ppc |
|
185 | coll ppc ((_,_,_,field,itm_)::itms) = |
|
186 coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms; |
|
187 val gfr = coll empty_ppc itms; |
|
188 in add_where gfr (map boolterm2item pre) end; |
|
189 (*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*) |
|
190 |
|
191 (*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*) |
|
192 |
|
193 (* --- 9.3.fun add_field dscs (d,ts) = |
|
194 if d mem (get_dsc_in dscs "#Given") |
|
195 then ("#Given",d,ts:term list) |
|
196 else if d mem (get_dsc_in dscs "#Find") |
|
197 then ("#Find",d,ts) |
|
198 else if d mem (get_dsc_in dscs "#Relate") |
|
199 then ("#Relate",d,ts) |
|
200 else ("#undef",d,ts); |
|
201 (* 28.1.00 raise error ("add_field: '"^ |
|
202 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
|
203 "' not in ppc-description "); *) |
|
204 ------9.3. *) |
|
205 |
|
206 (* 9.3.00 |
|
207 compare d and dsc in pbt and transfer field to pre-ori *) |
|
208 fun add_field thy pbt (d,ts) = |
|
209 let fun eq d pt = (d = (fst o snd) pt); |
|
210 in case filter (eq d) pbt of |
|
211 [(fi,(dsc,_))] => (fi,d,ts) |
|
212 | [] => ("#undef",d,ts) (*may come with met.ppc*) |
|
213 | _ => raise error ("add_field: "^ |
|
214 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
|
215 " more than once in pbt") |
|
216 end; |
|
217 |
|
218 (*. take over field from met.ppc at 'Specify_Method' into ori, |
|
219 i.e. also removes "#undef" fields .*) |
|
220 (* val (mpc, ori) = ((#ppc o get_met) mID, oris); |
|
221 *) |
|
222 fun add_field' thy mpc (ori:ori list) = |
|
223 let fun eq d pt = (d = (fst o snd) pt); |
|
224 fun repl mpc (i,v,_,d,ts) = |
|
225 case filter (eq d) mpc of |
|
226 [(fi,(dsc,_))] => [(i,v,fi,d,ts)] |
|
227 | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*) |
|
228 (*raise error ("add_field': "^ |
|
229 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
|
230 " not in met"*) |
|
231 | _ => raise error ("add_field': "^ |
|
232 (Syntax.string_of_term (thy2ctxt' "Isac") d)^ |
|
233 " more than once in met"); |
|
234 in (flat ((map (repl mpc)) ori)):ori list end; |
|
235 |
|
236 |
|
237 (*.mark an element with the position within a plateau; |
|
238 a plateau with length 1 is marked with 0 .*) |
|
239 fun mark eq [] = raise error "mark []" |
|
240 | mark eq xs = |
|
241 let |
|
242 fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)] |
|
243 | mar xx eq (x::x'::xs) n = |
|
244 if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1) |
|
245 else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1; |
|
246 in mar [] eq xs 1 end; |
|
247 (* |
|
248 > val xs = [1,1,1,2,4,4,5]; |
|
249 > mark (op=) xs; |
|
250 val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)] |
|
251 *) |
|
252 |
|
253 (*.assumes equal descriptions to be in adjacent 'plateaus', |
|
254 items at a certain position within the plateaus form a variant; |
|
255 length = 1 ... marked with 0: covers all variants .*) |
|
256 fun add_variants fdts = |
|
257 let |
|
258 fun eq (a,b) = curry op= (snd3 a) (snd3 b); |
|
259 in mark eq fdts end; |
|
260 |
|
261 (* collect equal elements: the model for coll_variants *) |
|
262 fun coll eq xs = |
|
263 let |
|
264 fun col xs eq x [] = xs @ [x] |
|
265 | col xs eq x (y::ys) = |
|
266 if eq(x,y) then col xs eq x ys |
|
267 else col (xs @ [x]) eq y ys; |
|
268 in col [] eq (hd xs) xs end; |
|
269 (* |
|
270 > val xs = [1,1,1,2,4,4,4]; |
|
271 > coll (op=) xs; |
|
272 val it = [1,2,4] : int list |
|
273 *) |
|
274 |
|
275 fun max [] = raise error "max of []" |
|
276 | max (y::ys) = |
|
277 let fun mx x [] = x |
|
278 | mx x (y::ys) = if x < y then mx y ys else mx x ys; |
|
279 in mx y ys end; |
|
280 fun gen_max _ [] = raise error "gen_max of []" |
|
281 | gen_max ord (y::ys) = |
|
282 let fun mx x [] = x |
|
283 | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys; |
|
284 in mx y ys end; |
|
285 |
|
286 |
|
287 |
|
288 (* assumes *) |
|
289 fun coll_variants (((v,x)::vxs)) = |
|
290 let |
|
291 fun col xs (vs,x) [] = xs @ [(vs,x)] |
|
292 | col xs (vs,x) ((v',x')::vxs') = |
|
293 if x=x' then col xs (vs @ [v'], x') vxs' |
|
294 else col (xs @ [(vs,x)]) ([v'], x') vxs'; |
|
295 in col [] ([v],x) vxs end; |
|
296 (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]; |
|
297 > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs); |
|
298 val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *) |
|
299 |
|
300 |
|
301 fun replace_0 vm [0] = intsto vm |
|
302 | replace_0 vm vs = vs; |
|
303 |
|
304 fun add_id [] = raise error "add_id []" |
|
305 | add_id xs = |
|
306 let fun add n [] = [] |
|
307 | add n (x::xs) = (n,x) :: add (n+1) xs; |
|
308 in add 1 xs end; |
|
309 (* |
|
310 > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)]; |
|
311 > add_id xs; |
|
312 val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))] |
|
313 *) |
|
314 |
|
315 fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e); |
|
316 fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e); |
|
317 fun flat3 (a,(b,c)) = (a,b,c); |
|
318 (* |
|
319 val pI = pI'; |
|
320 !pbts; |
|
321 *) |
|
322 (* in root (only!) fmz may be empty: fill with ..,dsc,[] |
|
323 fun init_ori fmz thy pI = |
|
324 if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*) |
|
325 else |
|
326 let |
|
327 val fds = map (cons2 (fst, fst o snd)) (get_pbt pI); |
|
328 val vfds = map ((pair [1]) o (rpair [])) fds; |
|
329 val ivfds = add_id vfds |
|
330 in (map flattup' ivfds):ori list end; 10.3.00---*) |
|
331 (* val fmz = ctl; val pI=["sqroot-test","univariate","equation"]; |
|
332 val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI'); |
|
333 val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI)); |
|
334 *) |
|
335 fun prep_ori [] _ _ = [] |
|
336 | prep_ori fmz thy pbt = |
|
337 let |
|
338 val ctopts = map (parse thy) fmz |
|
339 val _= (*FIXME.WN060916 improve error report*) |
|
340 if null (filter is_none ctopts) then () |
|
341 else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz) |
|
342 val dts = map ((split_dts thy) o term_of o the) ctopts |
|
343 val ori = map (add_field thy pbt) dts; |
|
344 (* val ori = map (flat3 o (pair "#undef")) dts; *) |
|
345 val ori' = add_variants ori; |
|
346 val maxv = max (map fst ori'); |
|
347 val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv; |
|
348 val ori'' = coll_variants ori'; |
|
349 val ori''' = map (apfst (replace_0 maxv)) ori''; |
|
350 val ori'''' = add_id ori''' |
|
351 in (map flattup ori''''):ori list end; |
|
352 |
|
353 |
|
354 (*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*) |
|
355 |
|
356 (*.the pattern for an item of a problems model or a methods guard.*) |
|
357 type pat = (string * (*field*) |
|
358 (term * (*description*) |
|
359 term)) (*id | struct-var*); |
|
360 fun pat2str ((field, (dsc, id)):pat) = |
|
361 pair2str (field, pair2str (term2str dsc, term2str id)); |
|
362 fun pats2str pats = (strs2str o (map pat2str)) pats; |
|
363 |
|
364 (* data for methods stored in 'methods'-database *) |
|
365 type met = |
|
366 {guh : guh, (*unique within this isac-knowledge *) |
|
367 mathauthors: string list,(*copyright *) |
|
368 init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*) |
|
369 rew_ord' : rew_ord', (*for rules in Detail |
|
370 TODO.WN0509 store fun itself, see 'type pbt'*) |
|
371 erls : rls, (*the eval_rls for cond. in rules FIXME "rls' |
|
372 instead erls in "fun prep_met" *) |
|
373 srls : rls, (*for evaluating list expressions in scr *) |
|
374 prls : rls, (*for evaluating predicates in modelpattern *) |
|
375 crls : rls, (*for check_elementwise, ie. formulae in calc.*) |
|
376 nrls : rls, (*canonical simplifier specific for this met *) |
|
377 calc : calc list, (*040207: <--- calclist' in fun prep_met *) |
|
378 (*branch : TransitiveB set in append_problem at generation ob pblobj |
|
379 FIXXXME.8.03: set branch from met in Apply_Method *) |
|
380 |
|
381 (* compare type pbt:*) |
|
382 ppc: pat list, |
|
383 (*.items in given, find, relate; |
|
384 items (in "#Find") which need not occur in the arg-list of a SubProblem |
|
385 are 'copy-named' with an identifier "*_!_". |
|
386 copy-named items are 'generating' if they are NOT "*___" |
|
387 see ME/calchead.sml 'fun is_copy_named'.*) |
|
388 pre: term list, (*preconditions in where*) |
|
389 (*script*) |
|
390 scr: scr (*prep_met requires either script or string "empty_script"*) |
|
391 }; |
|
392 (* ------- template ------------------------------------------------------ |
|
393 store_met |
|
394 (prep_met *.thy |
|
395 ([(*"EqSystem","normalize"*)], |
|
396 [("#Given" ,[ (*"equalities es_", "solveForVars vs_"*)]), |
|
397 ("#Find" ,[ (*dont forget typing non-reals *)]), |
|
398 ("#Relate",[])(*may be omitted *) ], |
|
399 {calc = [], (*filled autom. in prep_met *) |
|
400 crls = Erls, (*for check_elementwise *) |
|
401 prls = Erls, (*for evaluating preds in guard *) |
|
402 nrls = Erls, (*can.simplifier for all formulae*) |
|
403 rew_ord'="tless_true", (*for rules in Detail *) |
|
404 rls' = Erls, (*erls, the eval_rls for cond. in rules*) |
|
405 srls = Erls}, (*for evaluating list expr in scr*) |
|
406 "empty_script" |
|
407 )); |
|
408 ---------- template ----------------------------------------------------*) |
|
409 val e_met = {guh="met_empty",mathauthors=[],init=e_metID, |
|
410 rew_ord' = "e_rew_ord'": rew_ord', |
|
411 erls = e_rls, srls = e_rls, prls = e_rls, |
|
412 calc = [], crls = e_rls, nrls = e_rls, |
|
413 (*asm_thm = []: thm' list, |
|
414 asm_rls = []: rls' list,*) |
|
415 ppc = []: (string * (term * term)) list, |
|
416 pre = []: term list, |
|
417 scr = EmptyScr: scr}:met; |
|
418 |
|
419 |
|
420 (** problem-types stored in format for usage in specify **) |
|
421 (*25.8.01 ---- |
|
422 val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*) |
|
423 (term * (* description *) |
|
424 term)) (* id | struct-var *) |
|
425 list) |
|
426 ) list);*) |
|
427 |
|
428 (*deprecated due to 'type pat'*) |
|
429 type pbt_ = (string * (* field "#Given",..*) |
|
430 (term * (* description *) |
|
431 term)); (* id | struct-var *) |
|
432 val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_; |
|
433 type pbt = |
|
434 {guh : guh, (*unique within this isac-knowledge*) |
|
435 mathauthors: string list, (*copyright*) |
|
436 init : pblID, (*to start refinement with*) |
|
437 thy : theory, (* which allows to compile that pbt |
|
438 TODO: search generalized for subthy (ref.p.69*) |
|
439 (*^^^ WN050912 NOT used during application of the problem, |
|
440 because applied terms may be from 'subthy' as well as from super; |
|
441 thus we take 'maxthy'; see match_ags !*) |
|
442 cas : term option,(*'CAS-command'*) |
|
443 prls : rls, (* for preds in where_*) |
|
444 where_: term list, (* where - predicates*) |
|
445 ppc : pat list, |
|
446 (*this is the model-pattern; |
|
447 it contains "#Given","#Where","#Find","#Relate"-patterns*) |
|
448 met : metID list}; (* methods solving the pbt*) |
|
449 val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure", |
|
450 cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt; |
|
451 fun pbt2 (str, (t1, t2)) = |
|
452 pair2str (str, pair2str (term2str t1, term2str t2)); |
|
453 fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt; |
|
454 |
|
455 |
|
456 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]); |
|
457 val e_Mets = Ptyp ("e_metID",[e_met],[]); |
|
458 |
|
459 type ptyps = (pbt ptyp) list; |
|
460 val ptyps = ref ([e_Ptyp]:ptyps); |
|
461 |
|
462 type mets = (met ptyp) list; |
|
463 val mets = ref ([e_Mets]:mets); |
|
464 |
|
465 |
|
466 (**+ breadth-first search on hierarchy of problem-types +**) |
|
467 |
|
468 type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*) |
|
469 (* eg. ["equations","univariate","normalize"] while |
|
470 ["normalize","univariate","equations"] is the related pblID |
|
471 WN.24.4.03: also used for metID*) |
|
472 |
|
473 fun get_py thy d _ [] = |
|
474 error ("get_pbt not found: "^(strs2str d)) |
|
475 | get_py thy d [k] ((Ptyp (k',[py],_))::pys) = |
|
476 if k=k' then py |
|
477 else get_py thy d ([k]:pblRD) pys |
|
478 | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') = |
|
479 if k=k' then get_py thy d ks pys |
|
480 else get_py thy d (k::ks) pys'; |
|
481 (*> ptyps:= |
|
482 [Ptyp ("1",[("ptyp 1",([],[]))], |
|
483 [Ptyp ("11",[("ptyp 11",([],[]))], |
|
484 []) |
|
485 ]), |
|
486 Ptyp ("2",[("ptyp 2",([],[]))], |
|
487 [Ptyp ("21",[("ptyp 21",([],[]))], |
|
488 []) |
|
489 ]) |
|
490 ]; |
|
491 > get_py SqRoot.thy ["1"] ["1"] (!ptyps); |
|
492 > get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps); |
|
493 _REVERSE_ .......... !!!!!!!!!!*) |
|
494 |
|
495 (*TODO: search generalized for subthy*) |
|
496 fun get_pbt (pblID:pblID) = |
|
497 let val pblRD = rev pblID; |
|
498 in get_py (theory "Pure") pblID pblRD (!ptyps) end; |
|
499 (* get_pbt thy ["1"]; |
|
500 get_pbt thy ["21","2"]; |
|
501 *) |
|
502 |
|
503 (*TODO: throws exn 'get_pbt not found: ' ... confusing !! |
|
504 take 'ketype' as an argument !!!!!*) |
|
505 fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets); |
|
506 fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier); |
|
507 |
|
508 |
|
509 |
|
510 fun del_eq k ptyps = |
|
511 let fun del k ptyps [] = ptyps |
|
512 | del k ptyps ((Ptyp (k', [p], ps))::pys) = |
|
513 if k=k' then del k ptyps pys |
|
514 else del k (ptyps @ [Ptyp (k', [p], ps)]) pys; |
|
515 in del k [] ptyps end; |
|
516 |
|
517 fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])] |
|
518 |
|
519 | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) = |
|
520 ((*writeln("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*) |
|
521 if k=k' |
|
522 then ((Ptyp (k', [pbt], ps))::pys) |
|
523 else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*) |
|
524 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys)) |
|
525 ) |
|
526 | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) = |
|
527 ((*writeln("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*) |
|
528 if k=k' |
|
529 then ((Ptyp (k', [p], insrt d pbt ks ps))::pys) |
|
530 else |
|
531 if length pys = 0 |
|
532 then error ("insert: not found "^(strs2str (d:pblID))) |
|
533 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys)) |
|
534 ); |
|
535 |
|
536 |
|
537 fun coll_pblguhs pbls = |
|
538 let fun node coll (Ptyp (_,[n],ns)) = |
|
539 [(#guh : pbt -> guh) n] @ (nodes coll ns) |
|
540 and nodes coll [] = coll |
|
541 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns); |
|
542 in nodes [] pbls end; |
|
543 fun coll_metguhs mets = |
|
544 let fun node coll (Ptyp (_,[n],ns)) = |
|
545 [(#guh : met -> guh) n] |
|
546 and nodes coll [] = coll |
|
547 | nodes coll (n::ns) = (node coll n) @ (nodes coll ns); |
|
548 in nodes [] mets end; |
|
549 |
|
550 (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*) |
|
551 fun guh2kestoreID (guh:guh) = |
|
552 case (implode o (take_fromto 1 4) o explode) guh of |
|
553 "pbl_" => |
|
554 let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) = |
|
555 if gu = guh |
|
556 then SOME ((ids@[id]) : kestoreID) |
|
557 else nodes (ids@[id]) gu ns |
|
558 and nodes _ _ [] = NONE |
|
559 | nodes ids gu (n::ns) = |
|
560 case node ids gu n of SOME id => SOME id |
|
561 | NONE => nodes ids gu ns |
|
562 in case nodes [] guh (!ptyps) of |
|
563 SOME id => rev id |
|
564 | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^ |
|
565 "not found in (!ptyps)") |
|
566 end |
|
567 | "met_" => |
|
568 let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) = |
|
569 if gu = guh |
|
570 then SOME ((ids@[id]) : kestoreID) |
|
571 else nodes (ids@[id]) gu ns |
|
572 and nodes _ _ [] = NONE |
|
573 | nodes ids gu (n::ns) = |
|
574 case node ids gu n of SOME id => SOME id |
|
575 | NONE => nodes ids gu ns |
|
576 in case nodes [] guh (!mets) of |
|
577 SOME id => id |
|
578 | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^ |
|
579 "not found in (!mets)") end |
|
580 | _ => error ("guh2kestoreID called with '" ^ guh ^ "'"); |
|
581 (*> guh2kestoreID "pbl_equ_univ_lin"; |
|
582 val it = ["linear", "univariate", "equation"] : string list*) |
|
583 |
|
584 |
|
585 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) = |
|
586 if member op = (coll_pblguhs pbls) guh |
|
587 then error ("check_guh_unique failed with '"^guh^"';\n"^ |
|
588 "use 'sort_pblguhs()' for a list of guhs;\n"^ |
|
589 "consider setting 'check_guhs_unique := false'") |
|
590 else (); |
|
591 (* val (guh, mets) = ("met_test", !mets); |
|
592 *) |
|
593 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) = |
|
594 if member op = (coll_metguhs mets) guh |
|
595 then error ("check_guh_unique failed with '"^guh^"';\n"^ |
|
596 "use 'sort_metguhs()' for a list of guhs;\n"^ |
|
597 "consider setting 'check_guhs_unique := false'") |
|
598 else (); |
|
599 |
|
600 |
|
601 |
|
602 (*.the pblID has the leaf-element as first; better readability achieved;.*) |
|
603 fun store_pbt (pbt as {guh,...}, pblID) = |
|
604 (if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else (); |
|
605 ptyps:= insrt pblID pbt (rev pblID) (!ptyps)); |
|
606 |
|
607 (*.the metID has the root-element as first; compare 'fun store_pbt'.*) |
|
608 (* val (met as {guh,...}, metID) = |
|
609 ((prep_met EqSystem.thy "met_eqsys" [] e_metID |
|
610 (["EqSystem"], |
|
611 [], |
|
612 {rew_ord'="tless_true", rls' = Erls, calc = [], |
|
613 srls = Erls, prls = Erls, crls = Erls, nrls = Erls}, |
|
614 "empty_script" |
|
615 ))); |
|
616 *) |
|
617 fun store_met (met as {guh,...}, metID) = |
|
618 (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else (); |
|
619 mets:= insrt metID met metID (!mets)); |
|
620 |
|
621 |
|
622 (*. prepare problem-types before storing in pbltypes; |
|
623 dont forget to 'check_guh_unique' before ins.*) |
|
624 fun prep_pbt thy guh maa init |
|
625 (pblID, dsc_dats: (string * (string list)) list, |
|
626 ev:rls, ca: string option, metIDs:metID list) = |
|
627 (* val (thy, (pblID, dsc_dats: (string * (string list)) list, |
|
628 ev:rls, ca: string option, metIDs:metID list)) = |
|
629 ((EqSystem.thy, (["system"], |
|
630 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
|
631 ("#Find" ,["solution ss___"](*___ is copy-named*)) |
|
632 ], |
|
633 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
634 SOME "solveSystem es_ vs_", |
|
635 []))); |
|
636 *) |
|
637 let fun eq f (f', _) = f = f'; |
|
638 val gi = filter (eq "#Given") dsc_dats; |
|
639 (*val gi = [("#Given",["equality e_","solveFor v_"])] |
|
640 : (string * string list) list*) |
|
641 val gi = (case gi of |
|
642 [] => [] |
|
643 | ((_,gi')::[]) => |
|
644 ((map (split_did o term_of o the o (parse thy)) gi') |
|
645 handle _ => error |
|
646 ("prep_pbt: syntax error in '#Given' of "^ |
|
647 (strs2str pblID))) |
|
648 | _ => |
|
649 (error ("prep_pbt: more than one '#Given' in "^ |
|
650 (strs2str pblID)))); |
|
651 (*val gi = |
|
652 [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")), |
|
653 (Const ("Descript.solveFor","RealDef.real => Tools.una"), |
|
654 Free ("v_","RealDef.real"))] : (term * term) list *) |
|
655 val gi = map (pair "#Given") gi; |
|
656 (*val gi = |
|
657 [("#Given", |
|
658 (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))), |
|
659 ("#Given", |
|
660 (Const ("Descript.solveFor","RealDef.real => Tools.una"), |
|
661 Free ("v_","RealDef.real")))] : (string * (term * term)) list*) |
|
662 |
|
663 val fi = filter (eq "#Find") dsc_dats; |
|
664 val fi = (case fi of |
|
665 [] => [](*28.8.01: ["tool"] ...// raise error |
|
666 ("prep_pbt: no '#Find' in "^(strs2str pblID))*) |
|
667 (* val ((_,fi')::[]) = fi; |
|
668 *) |
|
669 | ((_,fi')::[]) => |
|
670 ((map (split_did o term_of o the o (parse thy)) fi') |
|
671 handle _ => raise error |
|
672 ("prep_pbt: syntax error in '#Find' of "^ |
|
673 (strs2str pblID))) |
|
674 | _ => |
|
675 (raise error ("prep_pbt: more than one '#Find' in "^ |
|
676 (strs2str pblID)))); |
|
677 val fi = map (pair "#Find") fi; |
|
678 |
|
679 val re = filter (eq "#Relate") dsc_dats; |
|
680 val re = (case re of |
|
681 [] => [] |
|
682 | ((_,re')::[]) => |
|
683 ((map (split_did o term_of o the o (parse thy)) re') |
|
684 handle _ => raise error |
|
685 ("prep_pbt: syntax error in '#Relate' of "^ |
|
686 (strs2str pblID))) |
|
687 | _ => |
|
688 (raise error ("prep_pbt: more than one '#Relate' in "^ |
|
689 (strs2str pblID)))); |
|
690 val re = map (pair "#Relate") re; |
|
691 |
|
692 val wh = filter (eq "#Where") dsc_dats; |
|
693 val wh = (case wh of |
|
694 [] => [] |
|
695 | ((_,wh')::[]) => |
|
696 ((map (term_of o the o (parse thy)) wh') |
|
697 handle _ => raise error |
|
698 ("prep_pbt: syntax error in '#Where' of "^ |
|
699 (strs2str pblID))) |
|
700 | _ => |
|
701 (raise error ("prep_pbt: more than one '#Where' in "^ |
|
702 (strs2str pblID)))); |
|
703 in ({guh=guh,mathauthors=maa,init=init, |
|
704 thy=thy,cas= case ca of NONE => NONE |
|
705 | SOME s => |
|
706 SOME ((term_of o the o (parse thy)) s), |
|
707 prls=ev,where_=wh,ppc= gi @ fi @ re, |
|
708 met=metIDs}, pblID):pbt * pblID end; |
|
709 (* prep_pbt thy (pblID, dsc_dats, metIDs); |
|
710 val it = |
|
711 ({met=[], |
|
712 ppc=[("#Given",(Const (#,#),Free (#,#))), |
|
713 ("#Given",(Const (#,#),Free (#,#))), |
|
714 ("#Find",(Const (#,#),Free (#,#)))], |
|
715 thy={ProtoPure, ..., Atools, RatArith}, |
|
716 where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $ |
|
717 Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *) |
|
718 |
|
719 |
|
720 |
|
721 |
|
722 (*. prepare met for storage analogous to pbt .*) |
|
723 fun prep_met thy guh maa init |
|
724 (metID, ppc: (string * string list) list (*'#Where' -> #pre*), |
|
725 {rew_ord'=ro, rls'=rls, srls=srls, prls=prls, |
|
726 calc = scr_isa_fns(*FIXME.040207: del - auto-done*), |
|
727 crls=cr, nrls=nr}, scr) = |
|
728 let fun eq f (f', _) = f = f'; |
|
729 (*val thy = (assoc_thy o fst) metID*) |
|
730 val gi = filter (eq "#Given") ppc; |
|
731 val gi = (case gi of |
|
732 [] => [] |
|
733 | ((_,gi')::[]) => |
|
734 ((map (split_did o term_of o the o (parse thy)) gi') |
|
735 handle _ => raise error |
|
736 ("prep_pbt: syntax error in '#Given' of "^ |
|
737 (strs2str metID))) |
|
738 | _ => |
|
739 (raise error ("prep_pbt: more than one '#Given' in "^ |
|
740 (strs2str metID)))); |
|
741 val gi = map (pair "#Given") gi; |
|
742 |
|
743 val fi = filter (eq "#Find") ppc; |
|
744 val fi = (case fi of |
|
745 [] => [](*28.8.01: ["tool"] ...// raise error |
|
746 ("prep_pbt: no '#Find' in "^(strs2str metID))*) |
|
747 | ((_,fi')::[]) => |
|
748 ((map (split_did o term_of o the o (parse thy)) fi') |
|
749 handle _ => raise error |
|
750 ("prep_pbt: syntax error in '#Find' of "^ |
|
751 (strs2str metID))) |
|
752 | _ => |
|
753 (raise error ("prep_pbt: more than one '#Find' in "^ |
|
754 (strs2str metID)))); |
|
755 val fi = map (pair "#Find") fi; |
|
756 |
|
757 val re = filter (eq "#Relate") ppc; |
|
758 val re = (case re of |
|
759 [] => [] |
|
760 | ((_,re')::[]) => |
|
761 ((map (split_did o term_of o the o (parse thy)) re') |
|
762 handle _ => raise error |
|
763 ("prep_pbt: syntax error in '#Relate' of "^ |
|
764 (strs2str metID))) |
|
765 | _ => |
|
766 (raise error ("prep_pbt: more than one '#Relate' in "^ |
|
767 (strs2str metID)))); |
|
768 val re = map (pair "#Relate") re; |
|
769 |
|
770 val wh = filter (eq "#Where") ppc; |
|
771 val wh = (case wh of |
|
772 [] => [] |
|
773 | ((_,wh')::[]) => |
|
774 ((map (term_of o the o (parse thy)) wh') |
|
775 handle _ => raise error |
|
776 ("prep_pbt: syntax error in '#Where' of "^ |
|
777 (strs2str metID))) |
|
778 | _ => |
|
779 (raise error ("prep_pbt: more than one '#Where' in "^ |
|
780 (strs2str metID)))); |
|
781 val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr) |
|
782 in ({guh=guh,mathauthors=maa,init=init, |
|
783 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls, |
|
784 calc = if scr = "empty_script" then [] |
|
785 else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o |
|
786 (filter is_calc) o stacpbls) sc, |
|
787 crls=cr, nrls=nr, scr=Script sc}:met, |
|
788 metID:metID) |
|
789 end; |
|
790 |
|
791 |
|
792 (**. get pblIDs of all entries in mat3D .**) |
|
793 |
|
794 |
|
795 fun format_pblID strl = enclose " [" "]" (commas_quote strl); |
|
796 fun format_pblIDl strll = enclose "[\n" "\n]\n" |
|
797 (space_implode ",\n" (map format_pblID strll)); |
|
798 |
|
799 fun scan _ [] = [] (* no base case, for empty doms only *) |
|
800 | scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]] |
|
801 | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl |
|
802 | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps) |
|
803 | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps); |
|
804 |
|
805 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps); |
|
806 (* ptyps:=[]; |
|
807 show_ptyps(); |
|
808 *) |
|
809 fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets); |
|
810 |
|
811 |
|
812 |
|
813 (*vvvvv---------- preparational work 8.01. UNUSED *) |
|
814 (**+ instantiate a problem-type +**) |
|
815 |
|
816 (*+ transform oris +*) |
|
817 |
|
818 fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs; |
|
819 (*> coll_vats [11,22] (hd oris); |
|
820 val it = [22,11,1,2,3] : int list |
|
821 |
|
822 > foldl coll_vats ([],oris); |
|
823 val it = [1,2,3] : int list |
|
824 |
|
825 > val i=1; |
|
826 > filter ((curry (op mem) i) o #2) oris; |
|
827 val it = |
|
828 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]), |
|
829 (2,[1,2,3],"#Find",Const (#,#),[Free #]), |
|
830 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), |
|
831 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), |
|
832 (6,[1],"#undef",Const (#,#),[Free #]), |
|
833 (9,[1,2],"#undef",Const (#,#),[# $ #]), |
|
834 (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *) |
|
835 |
|
836 local infix mem; (*from Isabelle2002*) |
|
837 fun x mem [] = false |
|
838 | x mem (y :: ys) = x = y orelse x mem ys; |
|
839 in |
|
840 fun filter_vat oris i = |
|
841 filter ((curry (op mem) i) o (#2 : ori -> int list)) oris; |
|
842 end; |
|
843 (*> map (filter_vat oris) [1,2,3]; |
|
844 val it = |
|
845 [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]), |
|
846 (2,[1,2,3],"#Find",Const (#,#),[Free #]), |
|
847 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), |
|
848 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), |
|
849 (6,[1],"#undef",Const (#,#),[Free #]), |
|
850 (9,[1,2],"#undef",Const (#,#),[# $ #]), |
|
851 (11,[1,2,3],"#undef",Const (#,#),[# $ #])], |
|
852 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]), |
|
853 (2,[1,2,3],"#Find",Const (#,#),[Free #]), |
|
854 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), |
|
855 (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]), |
|
856 (7,[2],"#undef",Const (#,#),[Free #]), |
|
857 (9,[1,2],"#undef",Const (#,#),[# $ #]), |
|
858 (11,[1,2,3],"#undef",Const (#,#),[# $ #])], |
|
859 [(1,[1,2,3],"#Given",Const (#,#),[# $ #]), |
|
860 (2,[1,2,3],"#Find",Const (#,#),[Free #]), |
|
861 (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]), |
|
862 (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]), |
|
863 (8,[3],"#undef",Const (#,#),[Free #]), |
|
864 (10,[3],"#undef",Const (#,#),[# $ #]), |
|
865 (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*) |
|
866 |
|
867 fun separate_vats oris = |
|
868 let val vats = foldl coll_vats ([] : int list, oris); |
|
869 in map (filter_vat oris) vats end; |
|
870 (*^^^ end preparational work 8.01.*) |
|
871 |
|
872 |
|
873 |
|
874 (**. check a problem (ie. itm list) for matching a problemtype .**) |
|
875 |
|
876 fun eq1 d (_,(d',_)) = (d = d'); |
|
877 fun itm_id ((i,_,_,_,_):itm) = i; |
|
878 fun ori_id ((i,_,_,_,_):ori) = i; |
|
879 fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm); |
|
880 (*see + add_sel_ppc ~~~~~~~*) |
|
881 fun field_eq f ((_,_,f',_,_):ori) = f = f'; |
|
882 |
|
883 (*. check an item (with arbitrary itm_ from previous matchings) |
|
884 for matching a problemtype; returns true only for itms found in pbt .*) |
|
885 fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) = |
|
886 (case find_first (eq1 d) pbt of |
|
887 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs), |
|
888 (id, pbl_ids' thy d vs))):itm) |
|
889 | NONE => (i,vats,false,f,Sup (d,vs))) |
|
890 | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) = |
|
891 (case find_first (eq1 d) pbt of |
|
892 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs), |
|
893 (id, pbl_ids' thy d vs))):itm) |
|
894 | NONE => (i,vats,false,f,Sup (d,vs))) |
|
895 |
|
896 | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm |
|
897 | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm |
|
898 |
|
899 | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) = |
|
900 (case find_first (eq1 d) pbt of |
|
901 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs), |
|
902 (id, pbl_ids' thy d vs))):itm) |
|
903 | NONE => (i,vats,false,f,Sup (d,vs))) |
|
904 (* val (i,vats,b,f,Mis (d,vs)) = i4; |
|
905 *) |
|
906 | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) = |
|
907 (case find_first (eq1 d) pbt of |
|
908 (* val SOME (_,(_,id)) = find_first (eq1 d) pbt; |
|
909 *) |
|
910 SOME (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\ |
|
911 \(id, pbl_ids' d vs))):itm)" |
|
912 | NONE => (i,vats,false,f,Sup (d,[vs]))); |
|
913 |
|
914 (* chk_ thy pbt i |
|
915 *) |
|
916 |
|
917 fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_; |
|
918 fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d'; |
|
919 fun eq0 ((0,_,_,_,_):itm) = true |
|
920 | eq0 _ = false; |
|
921 fun max_i i [] = i |
|
922 | max_i i ((id,_,_,_,_)::is) = |
|
923 if i > id then max_i i is else max_i id is; |
|
924 fun max_id [] = 0 |
|
925 | max_id ((id,_,_,_,_)::is) = max_i id is; |
|
926 fun add_idvat itms _ _ [] = itms |
|
927 | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) = |
|
928 add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *) |
|
929 ],b,f,itm_):itm]) (i+1) mvat its; |
|
930 |
|
931 |
|
932 (*. find elements of pbt not contained in itms; |
|
933 if such one is untouched, return this one, otherwise create new itm .*) |
|
934 fun chk_m (itms:itm list) untouched (p as (f,(d,id))) = |
|
935 case find_first (eq2 p) itms of |
|
936 SOME _ => [] |
|
937 | NONE => (case find_first (eq2 p) untouched of |
|
938 SOME itm => [itm] |
|
939 | NONE => [(0,[],false,f,Mis (d,id)):itm]); |
|
940 (* val itms = itms''; |
|
941 *) |
|
942 fun chk_mis mvat itms untouched pbt = |
|
943 let val mis = (flat o (map (chk_m itms untouched))) pbt; |
|
944 val mid = max_id itms; |
|
945 in add_idvat [] (mid + 1) mvat mis end; |
|
946 |
|
947 (*. check a problem (ie. itm list) for matching a problemtype, |
|
948 takes the max_vt for concluding completeness (could be another!) .*) |
|
949 (* val itms = itms'; val (pbt,pre) = (ppc, pre); |
|
950 val itms = itms; val (pbt,pre) = (ppc, pre); |
|
951 *) |
|
952 fun match_itms thy itms (pbt,pre,prls) = |
|
953 (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat |
|
954 andalso b; |
|
955 val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*) |
|
956 val mvat = max_vt itms'; |
|
957 val itms'' = filter (okv mvat) itms'; |
|
958 val untouched = filter eq0 itms;(*i.e. dsc only (from init)*) |
|
959 val mis = chk_mis mvat itms'' untouched pbt; |
|
960 val pre' = check_preconds' prls pre itms'' mvat |
|
961 val pb = foldl and_ (true, map fst pre') |
|
962 in (length mis = 0 andalso pb, (itms'@ mis, pre')) end); |
|
963 |
|
964 (*. check a problem pbl (ie. itm list) for matching a problemtype pbt, |
|
965 for missing items get data from formalization (ie. ori list); |
|
966 takes the max_vt for concluding completeness (could be another!) .*) |
|
967 (* (0) determine the most frequent variant mv in pbl |
|
968 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => |
|
969 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; |
|
970 (3) newitms = filter (mv mem vat(news)) news |
|
971 (4) pbt @ newitms *) |
|
972 (* val (pbl, pbt, pre) = (met, mtt, pre); |
|
973 val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt); |
|
974 val (pbl, pbt, pre) = (itms, ppc, where_); |
|
975 *) |
|
976 fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris = |
|
977 let |
|
978 (*0*)val mv = max_vt pbl; |
|
979 |
|
980 fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_; |
|
981 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of |
|
982 SOME _ => false | NONE => true; |
|
983 (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt; |
|
984 |
|
985 fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d'; |
|
986 fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) = |
|
987 (i,v,false,f,Mis (d,pid)):itm; |
|
988 (*2*)fun oris2itms oris mis1 = |
|
989 ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; |
|
990 val news = (flat o (map (oris2itms oris))) mis; |
|
991 (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv; |
|
992 val newitms = filter mem_vat news; |
|
993 (*4*)val itms' = pbl @ newitms; |
|
994 val pre' = check_preconds' prls pre itms' mv |
|
995 val pb = foldl and_ (true, map fst pre') |
|
996 in (length mis = 0 andalso pb, (itms', pre')) end; |
|
997 (*handle _ => (false,([],[]))*); |
|
998 |
|
999 |
|
1000 (*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris |
|
1001 allow for faster access to descriptions and terms *) |
|
1002 (**. check a problem (ie. itm list) for matching a problemtype .**) |
|
1003 |
|
1004 (*. check an ori for matching a problemtype by description; |
|
1005 returns true only for itms found in pbt .*) |
|
1006 fun chk1_ thy pbt ((i,vats,f,d,vs):ori) = |
|
1007 case find_first (eq1 d) pbt of |
|
1008 SOME (_,(_,id)) => [(i,vats,true,f, |
|
1009 Cor ((d,vs), (id, pbl_ids' thy d vs))):itm] |
|
1010 | NONE => []; |
|
1011 |
|
1012 (* elem 'p' of pbt contained in itms ? *) |
|
1013 fun chk1_m (itms:itm list) p = |
|
1014 case find_first (eq2 p) itms of |
|
1015 SOME _ => true | NONE => false; |
|
1016 fun chk1_m' (oris: ori list) (p as (f,(d,t))) = |
|
1017 case find_first (eq2' p) oris of |
|
1018 SOME _ => [] |
|
1019 | NONE => [(f, Mis (d, t))]; |
|
1020 fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm; |
|
1021 |
|
1022 fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc); |
|
1023 fun chk1_mis' oris ppc = |
|
1024 map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc); |
|
1025 |
|
1026 |
|
1027 (*. check a problem (ie. ori list) for matching a problemtype, |
|
1028 takes the max_vt for concluding completeness (FIXME could be another!) .*) |
|
1029 (* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py); |
|
1030 *) |
|
1031 fun match_oris thy prls oris (pbt,pre) = |
|
1032 let val itms = (flat o (map (chk1_ thy pbt))) oris; |
|
1033 val mvat = max_vt itms; |
|
1034 val complete = chk1_mis mvat itms pbt; |
|
1035 val pre' = check_preconds' prls pre itms mvat |
|
1036 val pb = foldl and_ (true, map fst pre') |
|
1037 in if complete andalso pb then true else false end; |
|
1038 (*run subp-rooteq.sml 'root-eq + subpbl: solve_linear' |
|
1039 until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"... |
|
1040 > val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_, |
|
1041 Nd(PblObj{origin=(oris,_,_),...},[])]) = pt; |
|
1042 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"], |
|
1043 (#where_ o get_pbt) ["linear","univariate","equation"]); |
|
1044 > match_oris oris (pbt,pre); |
|
1045 val it = true : bool |
|
1046 |
|
1047 |
|
1048 > val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"], |
|
1049 (#where_ o get_pbt)["plain_square","univariate","equation"]); |
|
1050 > match_oris oris (pbt,pre); |
|
1051 val it = false : bool |
|
1052 |
|
1053 |
|
1054 --------------------------------------------------- |
|
1055 run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square' |
|
1056 until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ... |
|
1057 > val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]), |
|
1058 Nd (PblObj {origin=(oris,_,_),...},[])]) = pt; |
|
1059 > val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"], |
|
1060 (#where_ o get_pbt) ["linear","univariate","equation"]); |
|
1061 > match_oris oris (pbt,pre); |
|
1062 val it = false : bool |
|
1063 |
|
1064 |
|
1065 > val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"], |
|
1066 (#where_ o get_pbt) ["plain_square","univariate","equation"]); |
|
1067 > match_oris oris (pbt,pre); |
|
1068 val it = true : bool |
|
1069 *) |
|
1070 (*^^^--- doubled 20.9.01 *) |
|
1071 |
|
1072 |
|
1073 (*. check a problem (ie. ori list) for matching a problemtype, |
|
1074 returns items for output to math-experts .*) |
|
1075 (* val (ppc,pre) = (#ppc py, #where_ py); |
|
1076 *) |
|
1077 fun match_oris' thy oris (ppc,pre,prls) = |
|
1078 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls)); |
|
1079 *) |
|
1080 let val itms = (flat o (map (chk1_ thy ppc))) oris; |
|
1081 val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris; |
|
1082 val mvat = max_vt itms; |
|
1083 val miss = chk1_mis' oris ppc; |
|
1084 val pre' = check_preconds' prls pre itms mvat |
|
1085 val pb = foldl and_ (true, map fst pre') |
|
1086 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; |
|
1087 |
|
1088 (*. for the user .*) |
|
1089 datatype match' = |
|
1090 Matches' of item ppc |
|
1091 | NoMatch' of item ppc; |
|
1092 |
|
1093 (*. match a formalization with a problem type .*) |
|
1094 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) = |
|
1095 let val oris = prep_ori fmz thy ppc; |
|
1096 val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er); |
|
1097 in if bool then Matches' (itms2itemppc thy itms pre') |
|
1098 else NoMatch' (itms2itemppc thy itms pre') end; |
|
1099 (* |
|
1100 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
1101 "solveFor x","errorBound (eps=0)","solutions L"]; |
|
1102 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} = |
|
1103 get_pbt ["univariate","equation"]; |
|
1104 match_pbl fmz pbt; |
|
1105 *) |
|
1106 |
|
1107 |
|
1108 (*. refine a problem; construct pblRD while scanning .*) |
|
1109 (* val (pblRD,ori)=("xxx",oris); |
|
1110 val py = get_pbt ["equation"]; |
|
1111 val py = get_pbt ["univariate","equation"]; |
|
1112 val py = get_pbt ["linear","univariate","equation"]; |
|
1113 val py = get_pbt ["root","univariate","equation"]; |
|
1114 match_oris (#prls py) ori (#ppc py, #where_ py); |
|
1115 |
|
1116 *) |
|
1117 fun refin (pblRD:pblRD) ori |
|
1118 ((Ptyp (pI,[py],[])):pbt ptyp) = |
|
1119 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) |
|
1120 then SOME ((pblRD @ [pI]):pblRD) |
|
1121 else NONE |
|
1122 | refin pblRD ori (Ptyp (pI,[py],pys)) = |
|
1123 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) |
|
1124 then (case refins (pblRD @ [pI]) ori pys of |
|
1125 SOME pblRD' => SOME pblRD' |
|
1126 | NONE => SOME (pblRD @ [pI])) |
|
1127 else NONE |
|
1128 and refins pblRD ori [] = NONE |
|
1129 | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) = |
|
1130 (case refin pblRD ori p of |
|
1131 SOME pblRD' => SOME pblRD' |
|
1132 | NONE => refins pblRD ori pts); |
|
1133 |
|
1134 (*. refine a problem; version providing output for math-experts .*) |
|
1135 fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) = |
|
1136 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) = |
|
1137 (rev ["linear","system"], fmz, [(*match list*)], |
|
1138 ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp)); |
|
1139 *) |
|
1140 let val _ = (writeln o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI]) |
|
1141 val {thy,ppc,where_,prls,...} = py |
|
1142 val oris = prep_ori fmz thy ppc |
|
1143 (*8.3.02: itms!: oris ev. are _not_ complete here*) |
|
1144 val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls) |
|
1145 in if b then pbls @ [Matches (rev (pblRD @ [pI]), |
|
1146 itms2itemppc thy itms pre')] |
|
1147 else pbls @ [NoMatch (rev (pblRD @ [pI]), |
|
1148 itms2itemppc thy itms pre')] |
|
1149 end |
|
1150 (* val pblRD = ["pbla"]; val fmz = fmz1; val pbls = []; |
|
1151 val Ptyp (pI,[py],pys) = hd (!ptyps); |
|
1152 refin' pblRD fmz pbls (Ptyp (pI,[py],pys)); |
|
1153 *) |
|
1154 | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) = |
|
1155 let val _ = (writeln o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI]) |
|
1156 val {thy,ppc,where_,prls,...} = py |
|
1157 val oris = prep_ori fmz thy ppc; |
|
1158 (*8.3.02: itms!: oris ev. are _not_ complete here*) |
|
1159 val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls); |
|
1160 in if b |
|
1161 then let val pbl = Matches (rev (pblRD @ [pI]), |
|
1162 itms2itemppc thy itms pre') |
|
1163 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end |
|
1164 else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]) |
|
1165 end |
|
1166 and refins' pblRD fmz pbls [] = pbls |
|
1167 | refins' pblRD fmz pbls ((p as Ptyp (pI,_,_))::pts) = |
|
1168 let val pbls' = refin' pblRD fmz pbls p |
|
1169 in case last_elem pbls' of |
|
1170 Matches _ => pbls' |
|
1171 | NoMatch _ => refins' pblRD fmz pbls' pts end; |
|
1172 |
|
1173 (*. refine a problem; version for tactic Refine_Problem .*) |
|
1174 fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) = |
|
1175 let (*val _ = writeln("### refin''1: pI="^pI);*) |
|
1176 val {thy,ppc,where_,prls,...} = py |
|
1177 val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls); |
|
1178 in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))] |
|
1179 else pbls @ [NoMatch_] |
|
1180 end |
|
1181 (* val pblRD = (rev o tl) pblID; val pbls = []; |
|
1182 val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps); |
|
1183 *) |
|
1184 | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) = |
|
1185 let (*val _ = writeln("### refin''2: pI="^pI);*) |
|
1186 val {thy,ppc,where_,prls,...} = py |
|
1187 val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls); |
|
1188 in if b |
|
1189 then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre')) |
|
1190 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end |
|
1191 else (pbls @ [NoMatch_]) |
|
1192 end |
|
1193 and refins'' thy pblRD itms pbls [] = pbls |
|
1194 | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) = |
|
1195 let val pbls' = refin'' thy pblRD itms pbls p |
|
1196 in case last_elem pbls' of |
|
1197 Match_ _ => pbls' |
|
1198 | NoMatch_ => refins'' thy pblRD itms pbls' pts end; |
|
1199 |
|
1200 |
|
1201 (*. apply a fun to a ptyps node; copied from get_py .*) |
|
1202 fun app_ptyp f (d:pblID) _ [] = |
|
1203 raise error ("app_ptyp not found: "^(strs2str d)) |
|
1204 | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) = |
|
1205 if k=k' then f p |
|
1206 else app_ptyp f d ([k]:pblRD) pys |
|
1207 | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') = |
|
1208 if k=k' then app_ptyp f d ks pys |
|
1209 else app_ptyp f d (k::ks) pys'; |
|
1210 |
|
1211 (*. for tactic Refine_Tacitly .*) |
|
1212 (*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*) |
|
1213 (* val (thy,pblID) = (assoc_thy dI',pI); |
|
1214 *) |
|
1215 fun refine_ori oris (pblID:pblID) = |
|
1216 let val opt = app_ptyp (refin ((rev o tl) pblID) oris) |
|
1217 pblID (rev pblID) (!ptyps); |
|
1218 in case opt of |
|
1219 SOME pblRD => let val (pblID':pblID) =(rev pblRD) |
|
1220 in if pblID' = pblID then NONE |
|
1221 else SOME pblID' end |
|
1222 | NONE => NONE end; |
|
1223 fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI; |
|
1224 |
|
1225 (*. for tactic Refine_Problem .*); |
|
1226 (* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *) |
|
1227 (* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps); |
|
1228 *) |
|
1229 fun refine_pbl thy (pblID:pblID) itms = |
|
1230 case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms []) |
|
1231 pblID (rev pblID) (!ptyps)) of |
|
1232 NONE => NONE |
|
1233 | SOME (Match_ (rfd as (pI',_))) => |
|
1234 if pblID = pI' then NONE else SOME rfd; |
|
1235 |
|
1236 |
|
1237 (*. for math-experts .*) |
|
1238 (*19.10.02FIXME: needs thy for parsing fmz*) |
|
1239 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID; |
|
1240 val pbls = []; val ptys = !ptyps; |
|
1241 *) |
|
1242 fun refine (fmz:fmz_) (pblID:pblID) = |
|
1243 app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps); |
|
1244 |
|
1245 |
|
1246 (*.make a guh from a reference to an element in the kestore; |
|
1247 EXCEPT theory hierarchy ... compare 'fun keref2xml'.*) |
|
1248 fun pblID2guh (pblID:pblID) = |
|
1249 (((#guh o get_pbt) pblID) |
|
1250 handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'")); |
|
1251 fun metID2guh (metID:metID) = |
|
1252 (((#guh o get_met) metID) |
|
1253 handle _ => raise error ("metID2guh: no 'Met_' for '"^ |
|
1254 strs2str' metID ^ "'")); |
|
1255 fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID |
|
1256 | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID |
|
1257 | kestoreID2guh ketype kestoreID = |
|
1258 raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^ |
|
1259 strs2str' kestoreID ^ "'"); |
|
1260 |
|
1261 fun show_pblguhs () = |
|
1262 (print_depth 999; |
|
1263 (writeln o strs2str o (map linefeed)) (coll_pblguhs (!ptyps)); |
|
1264 print_depth 3); |
|
1265 fun sort_pblguhs () = |
|
1266 (print_depth 999; |
|
1267 (writeln o strs2str o (map linefeed)) |
|
1268 (((sort string_ord) o coll_pblguhs) (!ptyps)); |
|
1269 print_depth 3); |
|
1270 |
|
1271 fun show_metguhs () = |
|
1272 (print_depth 999; |
|
1273 (writeln o strs2str o (map linefeed)) (coll_metguhs (!mets)); |
|
1274 print_depth 3); |
|
1275 fun sort_metguhs () = |
|
1276 (print_depth 999; |
|
1277 (writeln o strs2str o (map linefeed)) |
|
1278 (((sort string_ord) o coll_metguhs) (!mets)); |
|
1279 print_depth 3); |
|