1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,1279 @@
1.4 +(* the problems and methods as stored in hierarchies
1.5 + author Walther Neuper 1998
1.6 + (c) due to copyright terms
1.7 +
1.8 +use"ME/ptyps.sml";
1.9 +use"ptyps.sml";
1.10 +*)
1.11 +
1.12 +(*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)
1.13 +val dsc_unknown = (term_of o the o (parseold @{theory Script}))
1.14 + "unknown::'a => unknow";
1.15 +(*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)
1.16 +
1.17 +
1.18 +(*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)
1.19 +
1.20 +fun itm_2item thy (Cor ((d,ts),_)) =
1.21 + Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
1.22 + | itm_2item _ (Syn c) = SyntaxE c
1.23 + | itm_2item _ (Typ c) = TypeE c
1.24 + | itm_2item thy (Inc ((d,ts),_)) =
1.25 + Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
1.26 + | itm_2item thy (Sup (d,ts)) =
1.27 + Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))
1.28 + | itm_2item _ (Mis (d,pid)) =
1.29 + Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
1.30 + Syntax.string_of_term (thy2ctxt' "Isac") pid);
1.31 +
1.32 +
1.33 +(* --- 8.3.00
1.34 +fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list)
1.35 + handle _ => error ("get_dsc_in not for "^sel);
1.36 +
1.37 +fun dscs_in dscppc =
1.38 + ((get_dsc_in dscppc "#Given") @
1.39 + (get_dsc_in dscppc "#Find") @
1.40 + (get_dsc_in dscppc "#Relate")):term list;
1.41 +
1.42 + --- 26.1.88
1.43 +fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel)));
1.44 +fun get_dsc pblID =
1.45 + (get_dsc_of pblID "#Given") @
1.46 + (get_dsc_of pblID "#Find") @
1.47 + (get_dsc_of pblID "#Relate");
1.48 + --- *)
1.49 +
1.50 +fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
1.51 + {Given=map f gi, Where=map f wh,
1.52 + Find=map f fi, With=map f wi, Relate=map f re}:'b ppc;
1.53 +fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) =
1.54 + {Given=f gi, Where=f wh,
1.55 + Find=f fi, With=f wi, Relate=f re}:'b ppc;
1.56 +
1.57 +(*for ppc of changing type*)
1.58 +fun sel_ppc sel ppc =
1.59 + case sel of
1.60 + "#Given" => #Given (ppc:'a ppc)
1.61 + | "#Where" => #Where (ppc:'a ppc)
1.62 + | "#Find" => #Find (ppc:'a ppc)
1.63 + | "#With" => #With (ppc:'a ppc)
1.64 + | "#Relate" => #Relate (ppc:'a ppc)
1.65 + | _ => raise error ("sel_ppc tried to select by '"^sel^"'");
1.66 +
1.67 +fun repl_sel_ppc sel
1.68 + ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
1.69 + case sel of
1.70 + "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
1.71 + | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}
1.72 + | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}
1.73 + | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}
1.74 + | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}
1.75 + | _ => raise error ("repl_sel_ppc tried to select by '"^sel^"'");
1.76 +
1.77 +fun add_sel_ppc thy sel
1.78 + ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =
1.79 + case sel of
1.80 + "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)
1.81 + | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}
1.82 + | "#Find" => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}
1.83 + | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}
1.84 + | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)
1.85 + | _ => raise error ("add_sel_ppc tried to select by '"^sel^"'");
1.86 +fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
1.87 + ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
1.88 +
1.89 +(*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*)
1.90 +
1.91 +
1.92 +(*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*)
1.93 +
1.94 +
1.95 +
1.96 +(*decompose a problem-type into description and identifier
1.97 + FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
1.98 +fun split_dsc thy t =
1.99 + (let val (hd,args) = strip_comb t
1.100 + in if is_dsc hd
1.101 + then (hd, args)
1.102 + else (e_term, [t]) (*??? 9.01 just copied*)
1.103 + end)
1.104 + handle _ => raise error ("split_dsc: called with "^
1.105 + (Syntax.string_of_term (thy2ctxt' "Isac") t));
1.106 +(*
1.107 +> val t1 = (term_of o the o (parse thy)) "errorBound err_";
1.108 +> split_dsc t1;
1.109 +(Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))
1.110 + : term * term
1.111 +> val t3 = (term_of o the o (parse thy)) "valuesFor vs_";
1.112 +> split_dsc t3;
1.113 +(Const ("Descript.valuesFor","bool List.list => Tools.toreall"),
1.114 + Free ("vs_","bool List.list")) : term * term*)
1.115 +
1.116 +
1.117 +
1.118 +(*. take the first two return-values; for prep_ori .*)
1.119 +(*WN.13.5.03fun split_dts' thy t =
1.120 + let val (d, ts, _) = split_dts thy t
1.121 + in (d, ts) end;*)
1.122 +(*WN.8.12.03 quick for prep_ori'*)
1.123 +fun split_dsc' t =
1.124 + (let val dsc $ var = t
1.125 + in var end)
1.126 + handle _ => raise error ("split_dsc': called with "^term2str t);
1.127 +
1.128 +(*9.3.00*)
1.129 +(* split a term into description and (id | structured variable)
1.130 + for pbt, met.ppc *)
1.131 +fun split_did t =
1.132 + (let val (hd,[arg]) = strip_comb t
1.133 + in (hd,arg) end)
1.134 + handle _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "
1.135 + ^(Syntax.string_of_term (thy2ctxt' "Script") t));
1.136 +
1.137 +
1.138 +
1.139 +(*create output-string for itm_*)
1.140 +fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.141 + | itm_out thy (Syn c) = c
1.142 + | itm_out thy (Typ c) = c
1.143 + | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.144 + | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.145 + | itm_out thy (Mis (d,pid)) =
1.146 + Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^
1.147 + Syntax.string_of_term (thy2ctxt' "Isac") pid;
1.148 +
1.149 +(*22.11.00 unused
1.150 +fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)
1.151 +
1.152 +
1.153 +(*--3.3.
1.154 +fun itms2dts itms =
1.155 + let
1.156 + fun coll itms' [] = itms'
1.157 + | coll itms' (i::itms) =
1.158 + case i of
1.159 + (Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.160 + | (Syn c) => coll (itms' ) itms
1.161 + | (Typ c) => coll (itms' ) itms
1.162 + | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.163 + | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.164 + | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms
1.165 + in coll [] itms end;
1.166 +*)
1.167 +(*--3.3.00
1.168 +fun itm2item ((_,_,_,_,Cor (d,ts)):itm) =
1.169 + Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.170 + | itm2item (_,_,_,_,Syn (c)) = SyntaxE c
1.171 + | itm2item (_,_,_,_,Typ (c)) = TypeE c
1.172 + | itm2item (_,_,_,_,Fal (d,ts)) =
1.173 + False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.174 + | itm2item (_,_,_,_,Inc (d,ts)) =
1.175 + Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))
1.176 + | itm2item (_,_,_,_,Sup (d,ts)) =
1.177 + Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));
1.178 +*)
1.179 +
1.180 +fun boolterm2item (true, term) = Correct (term2str term)
1.181 + | boolterm2item (false, term) = False (term2str term);
1.182 +
1.183 +(* use"ME/modspec.sml";
1.184 + *)
1.185 +fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) =
1.186 + let
1.187 + fun coll ppc [] = ppc
1.188 + | coll ppc ((_,_,_,field,itm_)::itms) =
1.189 + coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;
1.190 + val gfr = coll empty_ppc itms;
1.191 + in add_where gfr (map boolterm2item pre) end;
1.192 +(*-----------------------------------------^^^-(3) aus modspec.sml 23.3.02*)
1.193 +
1.194 +(*-----------------------------------------vvv-(4) aus modspec.sml 23.3.02*)
1.195 +
1.196 +(* --- 9.3.fun add_field dscs (d,ts) =
1.197 + if d mem (get_dsc_in dscs "#Given")
1.198 + then ("#Given",d,ts:term list)
1.199 + else if d mem (get_dsc_in dscs "#Find")
1.200 + then ("#Find",d,ts)
1.201 + else if d mem (get_dsc_in dscs "#Relate")
1.202 + then ("#Relate",d,ts)
1.203 + else ("#undef",d,ts);
1.204 +(* 28.1.00 raise error ("add_field: '"^
1.205 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.206 + "' not in ppc-description "); *)
1.207 + ------9.3. *)
1.208 +
1.209 +(* 9.3.00
1.210 + compare d and dsc in pbt and transfer field to pre-ori *)
1.211 +fun add_field thy pbt (d,ts) =
1.212 + let fun eq d pt = (d = (fst o snd) pt);
1.213 + in case filter (eq d) pbt of
1.214 + [(fi,(dsc,_))] => (fi,d,ts)
1.215 + | [] => ("#undef",d,ts) (*may come with met.ppc*)
1.216 + | _ => raise error ("add_field: "^
1.217 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.218 + " more than once in pbt")
1.219 + end;
1.220 +
1.221 +(*. take over field from met.ppc at 'Specify_Method' into ori,
1.222 + i.e. also removes "#undef" fields .*)
1.223 +(* val (mpc, ori) = ((#ppc o get_met) mID, oris);
1.224 + *)
1.225 +fun add_field' thy mpc (ori:ori list) =
1.226 + let fun eq d pt = (d = (fst o snd) pt);
1.227 + fun repl mpc (i,v,_,d,ts) =
1.228 + case filter (eq d) mpc of
1.229 + [(fi,(dsc,_))] => [(i,v,fi,d,ts)]
1.230 + | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)
1.231 + (*raise error ("add_field': "^
1.232 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.233 + " not in met"*)
1.234 + | _ => raise error ("add_field': "^
1.235 + (Syntax.string_of_term (thy2ctxt' "Isac") d)^
1.236 + " more than once in met");
1.237 + in (flat ((map (repl mpc)) ori)):ori list end;
1.238 +
1.239 +
1.240 +(*.mark an element with the position within a plateau;
1.241 + a plateau with length 1 is marked with 0 .*)
1.242 +fun mark eq [] = raise error "mark []"
1.243 + | mark eq xs =
1.244 + let
1.245 + fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]
1.246 + | mar xx eq (x::x'::xs) n =
1.247 + if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)
1.248 + else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1;
1.249 + in mar [] eq xs 1 end;
1.250 +(*
1.251 +> val xs = [1,1,1,2,4,4,5];
1.252 +> mark (op=) xs;
1.253 +val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]
1.254 +*)
1.255 +
1.256 +(*.assumes equal descriptions to be in adjacent 'plateaus',
1.257 + items at a certain position within the plateaus form a variant;
1.258 + length = 1 ... marked with 0: covers all variants .*)
1.259 +fun add_variants fdts =
1.260 + let
1.261 + fun eq (a,b) = curry op= (snd3 a) (snd3 b);
1.262 + in mark eq fdts end;
1.263 +
1.264 +(* collect equal elements: the model for coll_variants *)
1.265 +fun coll eq xs =
1.266 + let
1.267 + fun col xs eq x [] = xs @ [x]
1.268 + | col xs eq x (y::ys) =
1.269 + if eq(x,y) then col xs eq x ys
1.270 + else col (xs @ [x]) eq y ys;
1.271 + in col [] eq (hd xs) xs end;
1.272 +(*
1.273 +> val xs = [1,1,1,2,4,4,4];
1.274 +> coll (op=) xs;
1.275 +val it = [1,2,4] : int list
1.276 +*)
1.277 +
1.278 +fun max [] = raise error "max of []"
1.279 + | max (y::ys) =
1.280 + let fun mx x [] = x
1.281 + | mx x (y::ys) = if x < y then mx y ys else mx x ys;
1.282 +in mx y ys end;
1.283 +fun gen_max _ [] = raise error "gen_max of []"
1.284 + | gen_max ord (y::ys) =
1.285 + let fun mx x [] = x
1.286 + | mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;
1.287 +in mx y ys end;
1.288 +
1.289 +
1.290 +
1.291 +(* assumes *)
1.292 +fun coll_variants (((v,x)::vxs)) =
1.293 + let
1.294 + fun col xs (vs,x) [] = xs @ [(vs,x)]
1.295 + | col xs (vs,x) ((v',x')::vxs') =
1.296 + if x=x' then col xs (vs @ [v'], x') vxs'
1.297 + else col (xs @ [(vs,x)]) ([v'], x') vxs';
1.298 + in col [] ([v],x) vxs end;
1.299 +(* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];
1.300 +> col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);
1.301 +val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)] *)
1.302 +
1.303 +
1.304 +fun replace_0 vm [0] = intsto vm
1.305 + | replace_0 vm vs = vs;
1.306 +
1.307 +fun add_id [] = raise error "add_id []"
1.308 + | add_id xs =
1.309 + let fun add n [] = []
1.310 + | add n (x::xs) = (n,x) :: add (n+1) xs;
1.311 +in add 1 xs end;
1.312 +(*
1.313 +> val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];
1.314 +> add_id xs;
1.315 +val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]
1.316 + *)
1.317 +
1.318 +fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e);
1.319 +fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e);
1.320 +fun flat3 (a,(b,c)) = (a,b,c);
1.321 +(*
1.322 + val pI = pI';
1.323 + !pbts;
1.324 +*)
1.325 +(* in root (only!) fmz may be empty: fill with ..,dsc,[]
1.326 +fun init_ori fmz thy pI =
1.327 + if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*)
1.328 + else
1.329 + let
1.330 + val fds = map (cons2 (fst, fst o snd)) (get_pbt pI);
1.331 + val vfds = map ((pair [1]) o (rpair [])) fds;
1.332 + val ivfds = add_id vfds
1.333 + in (map flattup' ivfds):ori list end; 10.3.00---*)
1.334 +(* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];
1.335 + val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');
1.336 + val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));
1.337 + *)
1.338 +fun prep_ori [] _ _ = []
1.339 + | prep_ori fmz thy pbt =
1.340 + let
1.341 + val ctopts = map (parse thy) fmz
1.342 + val _= (*FIXME.WN060916 improve error report*)
1.343 + if null (filter is_none ctopts) then ()
1.344 + else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)
1.345 + val dts = map ((split_dts thy) o term_of o the) ctopts
1.346 + val ori = map (add_field thy pbt) dts;
1.347 +(* val ori = map (flat3 o (pair "#undef")) dts; *)
1.348 + val ori' = add_variants ori;
1.349 + val maxv = max (map fst ori');
1.350 + val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv;
1.351 + val ori'' = coll_variants ori';
1.352 + val ori''' = map (apfst (replace_0 maxv)) ori'';
1.353 + val ori'''' = add_id ori'''
1.354 + in (map flattup ori''''):ori list end;
1.355 +
1.356 +
1.357 +(*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
1.358 +
1.359 +(*.the pattern for an item of a problems model or a methods guard.*)
1.360 +type pat = (string * (*field*)
1.361 + (term * (*description*)
1.362 + term)) (*id | struct-var*);
1.363 +fun pat2str ((field, (dsc, id)):pat) =
1.364 + pair2str (field, pair2str (term2str dsc, term2str id));
1.365 +fun pats2str pats = (strs2str o (map pat2str)) pats;
1.366 +
1.367 +(* data for methods stored in 'methods'-database *)
1.368 +type met =
1.369 + {guh : guh, (*unique within this isac-knowledge *)
1.370 + mathauthors: string list,(*copyright *)
1.371 + init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
1.372 + rew_ord' : rew_ord', (*for rules in Detail
1.373 + TODO.WN0509 store fun itself, see 'type pbt'*)
1.374 + erls : rls, (*the eval_rls for cond. in rules FIXME "rls'
1.375 + instead erls in "fun prep_met" *)
1.376 + srls : rls, (*for evaluating list expressions in scr *)
1.377 + prls : rls, (*for evaluating predicates in modelpattern *)
1.378 + crls : rls, (*for check_elementwise, ie. formulae in calc.*)
1.379 + nrls : rls, (*canonical simplifier specific for this met *)
1.380 + calc : calc list, (*040207: <--- calclist' in fun prep_met *)
1.381 + (*branch : TransitiveB set in append_problem at generation ob pblobj
1.382 + FIXXXME.8.03: set branch from met in Apply_Method *)
1.383 +
1.384 + (* compare type pbt:*)
1.385 + ppc: pat list,
1.386 + (*.items in given, find, relate;
1.387 + items (in "#Find") which need not occur in the arg-list of a SubProblem
1.388 + are 'copy-named' with an identifier "*_!_".
1.389 + copy-named items are 'generating' if they are NOT "*___"
1.390 + see ME/calchead.sml 'fun is_copy_named'.*)
1.391 + pre: term list, (*preconditions in where*)
1.392 + (*script*)
1.393 + scr: scr (*prep_met requires either script or string "empty_script"*)
1.394 + };
1.395 +(* ------- template ------------------------------------------------------
1.396 +store_met
1.397 + (prep_met *.thy
1.398 + ([(*"EqSystem","normalize"*)],
1.399 + [("#Given" ,[ (*"equalities es_", "solveForVars vs_"*)]),
1.400 + ("#Find" ,[ (*dont forget typing non-reals *)]),
1.401 + ("#Relate",[])(*may be omitted *) ],
1.402 + {calc = [], (*filled autom. in prep_met *)
1.403 + crls = Erls, (*for check_elementwise *)
1.404 + prls = Erls, (*for evaluating preds in guard *)
1.405 + nrls = Erls, (*can.simplifier for all formulae*)
1.406 + rew_ord'="tless_true", (*for rules in Detail *)
1.407 + rls' = Erls, (*erls, the eval_rls for cond. in rules*)
1.408 + srls = Erls}, (*for evaluating list expr in scr*)
1.409 + "empty_script"
1.410 + ));
1.411 +---------- template ----------------------------------------------------*)
1.412 +val e_met = {guh="met_empty",mathauthors=[],init=e_metID,
1.413 + rew_ord' = "e_rew_ord'": rew_ord',
1.414 + erls = e_rls, srls = e_rls, prls = e_rls,
1.415 + calc = [], crls = e_rls, nrls = e_rls,
1.416 + (*asm_thm = []: thm' list,
1.417 + asm_rls = []: rls' list,*)
1.418 + ppc = []: (string * (term * term)) list,
1.419 + pre = []: term list,
1.420 + scr = EmptyScr: scr}:met;
1.421 +
1.422 +
1.423 +(** problem-types stored in format for usage in specify **)
1.424 +(*25.8.01 ----
1.425 +val pbltypes = ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
1.426 + (term * (* description *)
1.427 + term)) (* id | struct-var *)
1.428 + list)
1.429 + ) list);*)
1.430 +
1.431 +(*deprecated due to 'type pat'*)
1.432 +type pbt_ = (string * (* field "#Given",..*)
1.433 + (term * (* description *)
1.434 + term)); (* id | struct-var *)
1.435 +val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_;
1.436 +type pbt =
1.437 + {guh : guh, (*unique within this isac-knowledge*)
1.438 + mathauthors: string list, (*copyright*)
1.439 + init : pblID, (*to start refinement with*)
1.440 + thy : theory, (* which allows to compile that pbt
1.441 + TODO: search generalized for subthy (ref.p.69*)
1.442 + (*^^^ WN050912 NOT used during application of the problem,
1.443 + because applied terms may be from 'subthy' as well as from super;
1.444 + thus we take 'maxthy'; see match_ags !*)
1.445 + cas : term option,(*'CAS-command'*)
1.446 + prls : rls, (* for preds in where_*)
1.447 + where_: term list, (* where - predicates*)
1.448 + ppc : pat list,
1.449 + (*this is the model-pattern;
1.450 + it contains "#Given","#Where","#Find","#Relate"-patterns*)
1.451 + met : metID list}; (* methods solving the pbt*)
1.452 +val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=theory "Pure",
1.453 + cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;
1.454 +fun pbt2 (str, (t1, t2)) =
1.455 + pair2str (str, pair2str (term2str t1, term2str t2));
1.456 +fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;
1.457 +
1.458 +
1.459 +val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]);
1.460 +val e_Mets = Ptyp ("e_metID",[e_met],[]);
1.461 +
1.462 +type ptyps = (pbt ptyp) list;
1.463 +val ptyps = ref ([e_Ptyp]:ptyps);
1.464 +
1.465 +type mets = (met ptyp) list;
1.466 +val mets = ref ([e_Mets]:mets);
1.467 +
1.468 +
1.469 +(**+ breadth-first search on hierarchy of problem-types +**)
1.470 +
1.471 +type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)
1.472 + (* eg. ["equations","univariate","normalize"] while
1.473 + ["normalize","univariate","equations"] is the related pblID
1.474 + WN.24.4.03: also used for metID*)
1.475 +
1.476 +fun get_py thy d _ [] =
1.477 + error ("get_pbt not found: "^(strs2str d))
1.478 + | get_py thy d [k] ((Ptyp (k',[py],_))::pys) =
1.479 + if k=k' then py
1.480 + else get_py thy d ([k]:pblRD) pys
1.481 + | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') =
1.482 + if k=k' then get_py thy d ks pys
1.483 + else get_py thy d (k::ks) pys';
1.484 +(*> ptyps:=
1.485 +[Ptyp ("1",[("ptyp 1",([],[]))],
1.486 + [Ptyp ("11",[("ptyp 11",([],[]))],
1.487 + [])
1.488 + ]),
1.489 + Ptyp ("2",[("ptyp 2",([],[]))],
1.490 + [Ptyp ("21",[("ptyp 21",([],[]))],
1.491 + [])
1.492 + ])
1.493 + ];
1.494 +> get_py SqRoot.thy ["1"] ["1"] (!ptyps);
1.495 +> get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);
1.496 + _REVERSE_ .......... !!!!!!!!!!*)
1.497 +
1.498 +(*TODO: search generalized for subthy*)
1.499 +fun get_pbt (pblID:pblID) =
1.500 + let val pblRD = rev pblID;
1.501 + in get_py (theory "Pure") pblID pblRD (!ptyps) end;
1.502 +(* get_pbt thy ["1"];
1.503 + get_pbt thy ["21","2"];
1.504 + *)
1.505 +
1.506 +(*TODO: throws exn 'get_pbt not found: ' ... confusing !!
1.507 + take 'ketype' as an argument !!!!!*)
1.508 +fun get_met (metID:metID) = get_py (theory "Pure") metID metID (!mets);
1.509 +fun get_the (theID:theID) = get_py (theory "Pure") theID theID (!thehier);
1.510 +
1.511 +
1.512 +
1.513 +fun del_eq k ptyps =
1.514 +let fun del k ptyps [] = ptyps
1.515 + | del k ptyps ((Ptyp (k', [p], ps))::pys) =
1.516 + if k=k' then del k ptyps pys
1.517 + else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;
1.518 +in del k [] ptyps end;
1.519 +
1.520 +fun insrt d pbt [k] [] = [Ptyp (k, [pbt],[])]
1.521 +
1.522 + | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =
1.523 +((*writeln("### insert 1: ks = "^(strs2str [k])^" k'= "^k');*)
1.524 + if k=k'
1.525 + then ((Ptyp (k', [pbt], ps))::pys)
1.526 + else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)
1.527 + ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))
1.528 +)
1.529 + | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =
1.530 +((*writeln("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
1.531 + if k=k'
1.532 + then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)
1.533 + else
1.534 + if length pys = 0
1.535 + then error ("insert: not found "^(strs2str (d:pblID)))
1.536 + else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))
1.537 +);
1.538 +
1.539 +
1.540 +fun coll_pblguhs pbls =
1.541 + let fun node coll (Ptyp (_,[n],ns)) =
1.542 + [(#guh : pbt -> guh) n] @ (nodes coll ns)
1.543 + and nodes coll [] = coll
1.544 + | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.545 + in nodes [] pbls end;
1.546 +fun coll_metguhs mets =
1.547 + let fun node coll (Ptyp (_,[n],ns)) =
1.548 + [(#guh : met -> guh) n]
1.549 + and nodes coll [] = coll
1.550 + | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);
1.551 + in nodes [] mets end;
1.552 +
1.553 +(*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)
1.554 +fun guh2kestoreID (guh:guh) =
1.555 + case (implode o (take_fromto 1 4) o explode) guh of
1.556 + "pbl_" =>
1.557 + let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =
1.558 + if gu = guh
1.559 + then SOME ((ids@[id]) : kestoreID)
1.560 + else nodes (ids@[id]) gu ns
1.561 + and nodes _ _ [] = NONE
1.562 + | nodes ids gu (n::ns) =
1.563 + case node ids gu n of SOME id => SOME id
1.564 + | NONE => nodes ids gu ns
1.565 + in case nodes [] guh (!ptyps) of
1.566 + SOME id => rev id
1.567 + | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
1.568 + "not found in (!ptyps)")
1.569 + end
1.570 + | "met_" =>
1.571 + let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =
1.572 + if gu = guh
1.573 + then SOME ((ids@[id]) : kestoreID)
1.574 + else nodes (ids@[id]) gu ns
1.575 + and nodes _ _ [] = NONE
1.576 + | nodes ids gu (n::ns) =
1.577 + case node ids gu n of SOME id => SOME id
1.578 + | NONE => nodes ids gu ns
1.579 + in case nodes [] guh (!mets) of
1.580 + SOME id => id
1.581 + | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^
1.582 + "not found in (!mets)") end
1.583 + | _ => error ("guh2kestoreID called with '" ^ guh ^ "'");
1.584 +(*> guh2kestoreID "pbl_equ_univ_lin";
1.585 +val it = ["linear", "univariate", "equation"] : string list*)
1.586 +
1.587 +
1.588 +fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =
1.589 + if member op = (coll_pblguhs pbls) guh
1.590 + then error ("check_guh_unique failed with '"^guh^"';\n"^
1.591 + "use 'sort_pblguhs()' for a list of guhs;\n"^
1.592 + "consider setting 'check_guhs_unique := false'")
1.593 + else ();
1.594 +(* val (guh, mets) = ("met_test", !mets);
1.595 + *)
1.596 +fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
1.597 + if member op = (coll_metguhs mets) guh
1.598 + then error ("check_guh_unique failed with '"^guh^"';\n"^
1.599 + "use 'sort_metguhs()' for a list of guhs;\n"^
1.600 + "consider setting 'check_guhs_unique := false'")
1.601 + else ();
1.602 +
1.603 +
1.604 +
1.605 +(*.the pblID has the leaf-element as first; better readability achieved;.*)
1.606 +fun store_pbt (pbt as {guh,...}, pblID) =
1.607 + (if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else ();
1.608 + ptyps:= insrt pblID pbt (rev pblID) (!ptyps));
1.609 +
1.610 +(*.the metID has the root-element as first; compare 'fun store_pbt'.*)
1.611 +(* val (met as {guh,...}, metID) =
1.612 + ((prep_met EqSystem.thy "met_eqsys" [] e_metID
1.613 + (["EqSystem"],
1.614 + [],
1.615 + {rew_ord'="tless_true", rls' = Erls, calc = [],
1.616 + srls = Erls, prls = Erls, crls = Erls, nrls = Erls},
1.617 + "empty_script"
1.618 + )));
1.619 + *)
1.620 +fun store_met (met as {guh,...}, metID) =
1.621 + (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();
1.622 + mets:= insrt metID met metID (!mets));
1.623 +
1.624 +
1.625 +(*. prepare problem-types before storing in pbltypes;
1.626 + dont forget to 'check_guh_unique' before ins.*)
1.627 +fun prep_pbt thy guh maa init
1.628 + (pblID, dsc_dats: (string * (string list)) list,
1.629 + ev:rls, ca: string option, metIDs:metID list) =
1.630 +(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
1.631 + ev:rls, ca: string option, metIDs:metID list)) =
1.632 + ((EqSystem.thy, (["system"],
1.633 + [("#Given" ,["equalities es_", "solveForVars vs_"]),
1.634 + ("#Find" ,["solution ss___"](*___ is copy-named*))
1.635 + ],
1.636 + append_rls "e_rls" e_rls [(*for preds in where_*)],
1.637 + SOME "solveSystem es_ vs_",
1.638 + [])));
1.639 + *)
1.640 + let fun eq f (f', _) = f = f';
1.641 + val gi = filter (eq "#Given") dsc_dats;
1.642 +(*val gi = [("#Given",["equality e_","solveFor v_"])]
1.643 + : (string * string list) list*)
1.644 + val gi = (case gi of
1.645 + [] => []
1.646 + | ((_,gi')::[]) =>
1.647 + ((map (split_did o term_of o the o (parse thy)) gi')
1.648 + handle _ => error
1.649 + ("prep_pbt: syntax error in '#Given' of "^
1.650 + (strs2str pblID)))
1.651 + | _ =>
1.652 + (error ("prep_pbt: more than one '#Given' in "^
1.653 + (strs2str pblID))));
1.654 +(*val gi =
1.655 + [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")),
1.656 + (Const ("Descript.solveFor","RealDef.real => Tools.una"),
1.657 + Free ("v_","RealDef.real"))] : (term * term) list *)
1.658 + val gi = map (pair "#Given") gi;
1.659 +(*val gi =
1.660 + [("#Given",
1.661 + (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))),
1.662 + ("#Given",
1.663 + (Const ("Descript.solveFor","RealDef.real => Tools.una"),
1.664 + Free ("v_","RealDef.real")))] : (string * (term * term)) list*)
1.665 +
1.666 + val fi = filter (eq "#Find") dsc_dats;
1.667 + val fi = (case fi of
1.668 + [] => [](*28.8.01: ["tool"] ...// raise error
1.669 + ("prep_pbt: no '#Find' in "^(strs2str pblID))*)
1.670 +(* val ((_,fi')::[]) = fi;
1.671 + *)
1.672 + | ((_,fi')::[]) =>
1.673 + ((map (split_did o term_of o the o (parse thy)) fi')
1.674 + handle _ => raise error
1.675 + ("prep_pbt: syntax error in '#Find' of "^
1.676 + (strs2str pblID)))
1.677 + | _ =>
1.678 + (raise error ("prep_pbt: more than one '#Find' in "^
1.679 + (strs2str pblID))));
1.680 + val fi = map (pair "#Find") fi;
1.681 +
1.682 + val re = filter (eq "#Relate") dsc_dats;
1.683 + val re = (case re of
1.684 + [] => []
1.685 + | ((_,re')::[]) =>
1.686 + ((map (split_did o term_of o the o (parse thy)) re')
1.687 + handle _ => raise error
1.688 + ("prep_pbt: syntax error in '#Relate' of "^
1.689 + (strs2str pblID)))
1.690 + | _ =>
1.691 + (raise error ("prep_pbt: more than one '#Relate' in "^
1.692 + (strs2str pblID))));
1.693 + val re = map (pair "#Relate") re;
1.694 +
1.695 + val wh = filter (eq "#Where") dsc_dats;
1.696 + val wh = (case wh of
1.697 + [] => []
1.698 + | ((_,wh')::[]) =>
1.699 + ((map (term_of o the o (parse thy)) wh')
1.700 + handle _ => raise error
1.701 + ("prep_pbt: syntax error in '#Where' of "^
1.702 + (strs2str pblID)))
1.703 + | _ =>
1.704 + (raise error ("prep_pbt: more than one '#Where' in "^
1.705 + (strs2str pblID))));
1.706 + in ({guh=guh,mathauthors=maa,init=init,
1.707 + thy=thy,cas= case ca of NONE => NONE
1.708 + | SOME s =>
1.709 + SOME ((term_of o the o (parse thy)) s),
1.710 + prls=ev,where_=wh,ppc= gi @ fi @ re,
1.711 + met=metIDs}, pblID):pbt * pblID end;
1.712 +(* prep_pbt thy (pblID, dsc_dats, metIDs);
1.713 + val it =
1.714 + ({met=[],
1.715 + ppc=[("#Given",(Const (#,#),Free (#,#))),
1.716 + ("#Given",(Const (#,#),Free (#,#))),
1.717 + ("#Find",(Const (#,#),Free (#,#)))],
1.718 + thy={ProtoPure, ..., Atools, RatArith},
1.719 + where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $
1.720 + Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID *)
1.721 +
1.722 +
1.723 +
1.724 +
1.725 +(*. prepare met for storage analogous to pbt .*)
1.726 +fun prep_met thy guh maa init
1.727 + (metID, ppc: (string * string list) list (*'#Where' -> #pre*),
1.728 + {rew_ord'=ro, rls'=rls, srls=srls, prls=prls,
1.729 + calc = scr_isa_fns(*FIXME.040207: del - auto-done*),
1.730 + crls=cr, nrls=nr}, scr) =
1.731 + let fun eq f (f', _) = f = f';
1.732 + (*val thy = (assoc_thy o fst) metID*)
1.733 + val gi = filter (eq "#Given") ppc;
1.734 + val gi = (case gi of
1.735 + [] => []
1.736 + | ((_,gi')::[]) =>
1.737 + ((map (split_did o term_of o the o (parse thy)) gi')
1.738 + handle _ => raise error
1.739 + ("prep_pbt: syntax error in '#Given' of "^
1.740 + (strs2str metID)))
1.741 + | _ =>
1.742 + (raise error ("prep_pbt: more than one '#Given' in "^
1.743 + (strs2str metID))));
1.744 + val gi = map (pair "#Given") gi;
1.745 +
1.746 + val fi = filter (eq "#Find") ppc;
1.747 + val fi = (case fi of
1.748 + [] => [](*28.8.01: ["tool"] ...// raise error
1.749 + ("prep_pbt: no '#Find' in "^(strs2str metID))*)
1.750 + | ((_,fi')::[]) =>
1.751 + ((map (split_did o term_of o the o (parse thy)) fi')
1.752 + handle _ => raise error
1.753 + ("prep_pbt: syntax error in '#Find' of "^
1.754 + (strs2str metID)))
1.755 + | _ =>
1.756 + (raise error ("prep_pbt: more than one '#Find' in "^
1.757 + (strs2str metID))));
1.758 + val fi = map (pair "#Find") fi;
1.759 +
1.760 + val re = filter (eq "#Relate") ppc;
1.761 + val re = (case re of
1.762 + [] => []
1.763 + | ((_,re')::[]) =>
1.764 + ((map (split_did o term_of o the o (parse thy)) re')
1.765 + handle _ => raise error
1.766 + ("prep_pbt: syntax error in '#Relate' of "^
1.767 + (strs2str metID)))
1.768 + | _ =>
1.769 + (raise error ("prep_pbt: more than one '#Relate' in "^
1.770 + (strs2str metID))));
1.771 + val re = map (pair "#Relate") re;
1.772 +
1.773 + val wh = filter (eq "#Where") ppc;
1.774 + val wh = (case wh of
1.775 + [] => []
1.776 + | ((_,wh')::[]) =>
1.777 + ((map (term_of o the o (parse thy)) wh')
1.778 + handle _ => raise error
1.779 + ("prep_pbt: syntax error in '#Where' of "^
1.780 + (strs2str metID)))
1.781 + | _ =>
1.782 + (raise error ("prep_pbt: more than one '#Where' in "^
1.783 + (strs2str metID))));
1.784 + val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)
1.785 + in ({guh=guh,mathauthors=maa,init=init,
1.786 + ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,
1.787 + calc = if scr = "empty_script" then []
1.788 + else ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o
1.789 + (filter is_calc) o stacpbls) sc,
1.790 + crls=cr, nrls=nr, scr=Script sc}:met,
1.791 + metID:metID)
1.792 + end;
1.793 +
1.794 +
1.795 +(**. get pblIDs of all entries in mat3D .**)
1.796 +
1.797 +
1.798 +fun format_pblID strl = enclose " [" "]" (commas_quote strl);
1.799 +fun format_pblIDl strll = enclose "[\n" "\n]\n"
1.800 + (space_implode ",\n" (map format_pblID strll));
1.801 +
1.802 +fun scan _ [] = [] (* no base case, for empty doms only *)
1.803 + | scan id ((Ptyp ((i,_,[])))::[]) = [id@[i]]
1.804 + | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl
1.805 + | scan id ((Ptyp ((i,_,[])))::ps) = [id@[i]] @(scan id ps)
1.806 + | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);
1.807 +
1.808 +fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);
1.809 +(* ptyps:=[];
1.810 + show_ptyps();
1.811 + *)
1.812 +fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);
1.813 +
1.814 +
1.815 +
1.816 +(*vvvvv---------- preparational work 8.01. UNUSED *)
1.817 +(**+ instantiate a problem-type +**)
1.818 +
1.819 +(*+ transform oris +*)
1.820 +
1.821 +fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs;
1.822 +(*> coll_vats [11,22] (hd oris);
1.823 +val it = [22,11,1,2,3] : int list
1.824 +
1.825 +> foldl coll_vats ([],oris);
1.826 +val it = [1,2,3] : int list
1.827 +
1.828 +> val i=1;
1.829 +> filter ((curry (op mem) i) o #2) oris;
1.830 +val it =
1.831 + [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.832 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.833 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.834 + (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
1.835 + (6,[1],"#undef",Const (#,#),[Free #]),
1.836 + (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.837 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)
1.838 +
1.839 +local infix mem; (*from Isabelle2002*)
1.840 +fun x mem [] = false
1.841 + | x mem (y :: ys) = x = y orelse x mem ys;
1.842 +in
1.843 +fun filter_vat oris i =
1.844 + filter ((curry (op mem) i) o (#2 : ori -> int list)) oris;
1.845 +end;
1.846 +(*> map (filter_vat oris) [1,2,3];
1.847 +val it =
1.848 + [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.849 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.850 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.851 + (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
1.852 + (6,[1],"#undef",Const (#,#),[Free #]),
1.853 + (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.854 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
1.855 + [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.856 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.857 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.858 + (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),
1.859 + (7,[2],"#undef",Const (#,#),[Free #]),
1.860 + (9,[1,2],"#undef",Const (#,#),[# $ #]),
1.861 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])],
1.862 + [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),
1.863 + (2,[1,2,3],"#Find",Const (#,#),[Free #]),
1.864 + (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),
1.865 + (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),
1.866 + (8,[3],"#undef",Const (#,#),[Free #]),
1.867 + (10,[3],"#undef",Const (#,#),[# $ #]),
1.868 + (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)
1.869 +
1.870 +fun separate_vats oris =
1.871 + let val vats = foldl coll_vats ([] : int list, oris);
1.872 + in map (filter_vat oris) vats end;
1.873 +(*^^^ end preparational work 8.01.*)
1.874 +
1.875 +
1.876 +
1.877 +(**. check a problem (ie. itm list) for matching a problemtype .**)
1.878 +
1.879 +fun eq1 d (_,(d',_)) = (d = d');
1.880 +fun itm_id ((i,_,_,_,_):itm) = i;
1.881 +fun ori_id ((i,_,_,_,_):ori) = i;
1.882 +fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm);
1.883 +(*see + add_sel_ppc ~~~~~~~*)
1.884 +fun field_eq f ((_,_,f',_,_):ori) = f = f';
1.885 +
1.886 +(*. check an item (with arbitrary itm_ from previous matchings)
1.887 + for matching a problemtype; returns true only for itms found in pbt .*)
1.888 +fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =
1.889 + (case find_first (eq1 d) pbt of
1.890 + SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
1.891 + (id, pbl_ids' thy d vs))):itm)
1.892 + | NONE => (i,vats,false,f,Sup (d,vs)))
1.893 + | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =
1.894 + (case find_first (eq1 d) pbt of
1.895 + SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
1.896 + (id, pbl_ids' thy d vs))):itm)
1.897 + | NONE => (i,vats,false,f,Sup (d,vs)))
1.898 +
1.899 + | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm
1.900 + | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm
1.901 +
1.902 + | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =
1.903 + (case find_first (eq1 d) pbt of
1.904 + SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),
1.905 + (id, pbl_ids' thy d vs))):itm)
1.906 + | NONE => (i,vats,false,f,Sup (d,vs)))
1.907 +(* val (i,vats,b,f,Mis (d,vs)) = i4;
1.908 + *)
1.909 + | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =
1.910 + (case find_first (eq1 d) pbt of
1.911 +(* val SOME (_,(_,id)) = find_first (eq1 d) pbt;
1.912 + *)
1.913 + SOME (_,(_,id)) => raise error "chk_: ((i,vats,b,f,Cor ((d,vs),\
1.914 + \(id, pbl_ids' d vs))):itm)"
1.915 + | NONE => (i,vats,false,f,Sup (d,[vs])));
1.916 +
1.917 +(* chk_ thy pbt i
1.918 + *)
1.919 +
1.920 +fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1.921 +fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
1.922 +fun eq0 ((0,_,_,_,_):itm) = true
1.923 + | eq0 _ = false;
1.924 +fun max_i i [] = i
1.925 + | max_i i ((id,_,_,_,_)::is) =
1.926 + if i > id then max_i i is else max_i id is;
1.927 +fun max_id [] = 0
1.928 + | max_id ((id,_,_,_,_)::is) = max_i id is;
1.929 +fun add_idvat itms _ _ [] = itms
1.930 + | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) =
1.931 + add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *)
1.932 + ],b,f,itm_):itm]) (i+1) mvat its;
1.933 +
1.934 +
1.935 +(*. find elements of pbt not contained in itms;
1.936 + if such one is untouched, return this one, otherwise create new itm .*)
1.937 +fun chk_m (itms:itm list) untouched (p as (f,(d,id))) =
1.938 + case find_first (eq2 p) itms of
1.939 + SOME _ => []
1.940 + | NONE => (case find_first (eq2 p) untouched of
1.941 + SOME itm => [itm]
1.942 + | NONE => [(0,[],false,f,Mis (d,id)):itm]);
1.943 +(* val itms = itms'';
1.944 + *)
1.945 +fun chk_mis mvat itms untouched pbt =
1.946 + let val mis = (flat o (map (chk_m itms untouched))) pbt;
1.947 + val mid = max_id itms;
1.948 + in add_idvat [] (mid + 1) mvat mis end;
1.949 +
1.950 +(*. check a problem (ie. itm list) for matching a problemtype,
1.951 + takes the max_vt for concluding completeness (could be another!) .*)
1.952 +(* val itms = itms'; val (pbt,pre) = (ppc, pre);
1.953 + val itms = itms; val (pbt,pre) = (ppc, pre);
1.954 + *)
1.955 +fun match_itms thy itms (pbt,pre,prls) =
1.956 + (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat
1.957 + andalso b;
1.958 + val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)
1.959 + val mvat = max_vt itms';
1.960 + val itms'' = filter (okv mvat) itms';
1.961 + val untouched = filter eq0 itms;(*i.e. dsc only (from init)*)
1.962 + val mis = chk_mis mvat itms'' untouched pbt;
1.963 + val pre' = check_preconds' prls pre itms'' mvat
1.964 + val pb = foldl and_ (true, map fst pre')
1.965 + in (length mis = 0 andalso pb, (itms'@ mis, pre')) end);
1.966 +
1.967 +(*. check a problem pbl (ie. itm list) for matching a problemtype pbt,
1.968 + for missing items get data from formalization (ie. ori list);
1.969 + takes the max_vt for concluding completeness (could be another!) .*)
1.970 +(* (0) determine the most frequent variant mv in pbl
1.971 + ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
1.972 + (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
1.973 + (3) newitms = filter (mv mem vat(news)) news
1.974 + (4) pbt @ newitms *)
1.975 +(* val (pbl, pbt, pre) = (met, mtt, pre);
1.976 + val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt);
1.977 + val (pbl, pbt, pre) = (itms, ppc, where_);
1.978 + *)
1.979 +fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris =
1.980 + let
1.981 + (*0*)val mv = max_vt pbl;
1.982 +
1.983 + fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;
1.984 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
1.985 + SOME _ => false | NONE => true;
1.986 + (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;
1.987 +
1.988 + fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';
1.989 + fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) =
1.990 + (i,v,false,f,Mis (d,pid)):itm;
1.991 + (*2*)fun oris2itms oris mis1 =
1.992 + ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
1.993 + val news = (flat o (map (oris2itms oris))) mis;
1.994 + (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv;
1.995 + val newitms = filter mem_vat news;
1.996 + (*4*)val itms' = pbl @ newitms;
1.997 + val pre' = check_preconds' prls pre itms' mv
1.998 + val pb = foldl and_ (true, map fst pre')
1.999 + in (length mis = 0 andalso pb, (itms', pre')) end;
1.1000 + (*handle _ => (false,([],[]))*);
1.1001 +
1.1002 +
1.1003 +(*vvv--- doubled 20.9.01: ... 7.3.02 itms --> oris, because oris
1.1004 + allow for faster access to descriptions and terms *)
1.1005 +(**. check a problem (ie. itm list) for matching a problemtype .**)
1.1006 +
1.1007 +(*. check an ori for matching a problemtype by description;
1.1008 + returns true only for itms found in pbt .*)
1.1009 +fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =
1.1010 + case find_first (eq1 d) pbt of
1.1011 + SOME (_,(_,id)) => [(i,vats,true,f,
1.1012 + Cor ((d,vs), (id, pbl_ids' thy d vs))):itm]
1.1013 + | NONE => [];
1.1014 +
1.1015 +(* elem 'p' of pbt contained in itms ? *)
1.1016 +fun chk1_m (itms:itm list) p =
1.1017 + case find_first (eq2 p) itms of
1.1018 + SOME _ => true | NONE => false;
1.1019 +fun chk1_m' (oris: ori list) (p as (f,(d,t))) =
1.1020 + case find_first (eq2' p) oris of
1.1021 + SOME _ => []
1.1022 + | NONE => [(f, Mis (d, t))];
1.1023 +fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;
1.1024 +
1.1025 +fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
1.1026 +fun chk1_mis' oris ppc =
1.1027 + map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
1.1028 +
1.1029 +
1.1030 +(*. check a problem (ie. ori list) for matching a problemtype,
1.1031 + takes the max_vt for concluding completeness (FIXME could be another!) .*)
1.1032 +(* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py);
1.1033 + *)
1.1034 +fun match_oris thy prls oris (pbt,pre) =
1.1035 + let val itms = (flat o (map (chk1_ thy pbt))) oris;
1.1036 + val mvat = max_vt itms;
1.1037 + val complete = chk1_mis mvat itms pbt;
1.1038 + val pre' = check_preconds' prls pre itms mvat
1.1039 + val pb = foldl and_ (true, map fst pre')
1.1040 + in if complete andalso pb then true else false end;
1.1041 +(*run subp-rooteq.sml 'root-eq + subpbl: solve_linear'
1.1042 + until 'val nxt = ("Model_Problem",Model_Problem ["linear","univariate"...
1.1043 +> val Nd(PblObj _,[_,_,_,_,_,_,_,_,_,_,_,
1.1044 + Nd(PblObj{origin=(oris,_,_),...},[])]) = pt;
1.1045 +> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1.1046 + (#where_ o get_pbt) ["linear","univariate","equation"]);
1.1047 +> match_oris oris (pbt,pre);
1.1048 +val it = true : bool
1.1049 +
1.1050 +
1.1051 +> val (pbt,pre) =((#ppc o get_pbt) ["plain_square","univariate","equation"],
1.1052 + (#where_ o get_pbt)["plain_square","univariate","equation"]);
1.1053 +> match_oris oris (pbt,pre);
1.1054 +val it = false : bool
1.1055 +
1.1056 +
1.1057 + ---------------------------------------------------
1.1058 + run subp-rooteq.sml 'root-eq + subpbl: solve_plain_square'
1.1059 + until 'val nxt = ("Model_Problem",Model_Problem ["plain_square","univ...
1.1060 +> val Nd (PblObj _, [_,_,_,_,_,_,_,Nd (PrfObj _,[]),
1.1061 + Nd (PblObj {origin=(oris,_,_),...},[])]) = pt;
1.1062 +> val (pbt,pre) = ((#ppc o get_pbt) ["linear","univariate","equation"],
1.1063 + (#where_ o get_pbt) ["linear","univariate","equation"]);
1.1064 +> match_oris oris (pbt,pre);
1.1065 +val it = false : bool
1.1066 +
1.1067 +
1.1068 +> val (pbt,pre)=((#ppc o get_pbt) ["plain_square","univariate","equation"],
1.1069 + (#where_ o get_pbt) ["plain_square","univariate","equation"]);
1.1070 +> match_oris oris (pbt,pre);
1.1071 +val it = true : bool
1.1072 +*)
1.1073 +(*^^^--- doubled 20.9.01 *)
1.1074 +
1.1075 +
1.1076 +(*. check a problem (ie. ori list) for matching a problemtype,
1.1077 + returns items for output to math-experts .*)
1.1078 +(* val (ppc,pre) = (#ppc py, #where_ py);
1.1079 + *)
1.1080 +fun match_oris' thy oris (ppc,pre,prls) =
1.1081 +(* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));
1.1082 + *)
1.1083 + let val itms = (flat o (map (chk1_ thy ppc))) oris;
1.1084 + val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris;
1.1085 + val mvat = max_vt itms;
1.1086 + val miss = chk1_mis' oris ppc;
1.1087 + val pre' = check_preconds' prls pre itms mvat
1.1088 + val pb = foldl and_ (true, map fst pre')
1.1089 + in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
1.1090 +
1.1091 +(*. for the user .*)
1.1092 +datatype match' =
1.1093 + Matches' of item ppc
1.1094 +| NoMatch' of item ppc;
1.1095 +
1.1096 +(*. match a formalization with a problem type .*)
1.1097 +fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =
1.1098 + let val oris = prep_ori fmz thy ppc;
1.1099 + val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);
1.1100 + in if bool then Matches' (itms2itemppc thy itms pre')
1.1101 + else NoMatch' (itms2itemppc thy itms pre') end;
1.1102 +(*
1.1103 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.1104 + "solveFor x","errorBound (eps=0)","solutions L"];
1.1105 +val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
1.1106 + get_pbt ["univariate","equation"];
1.1107 +match_pbl fmz pbt;
1.1108 +*)
1.1109 +
1.1110 +
1.1111 +(*. refine a problem; construct pblRD while scanning .*)
1.1112 +(* val (pblRD,ori)=("xxx",oris);
1.1113 + val py = get_pbt ["equation"];
1.1114 + val py = get_pbt ["univariate","equation"];
1.1115 + val py = get_pbt ["linear","univariate","equation"];
1.1116 + val py = get_pbt ["root","univariate","equation"];
1.1117 + match_oris (#prls py) ori (#ppc py, #where_ py);
1.1118 +
1.1119 + *)
1.1120 +fun refin (pblRD:pblRD) ori
1.1121 +((Ptyp (pI,[py],[])):pbt ptyp) =
1.1122 + if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
1.1123 + then SOME ((pblRD @ [pI]):pblRD)
1.1124 + else NONE
1.1125 + | refin pblRD ori (Ptyp (pI,[py],pys)) =
1.1126 + if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
1.1127 + then (case refins (pblRD @ [pI]) ori pys of
1.1128 + SOME pblRD' => SOME pblRD'
1.1129 + | NONE => SOME (pblRD @ [pI]))
1.1130 + else NONE
1.1131 +and refins pblRD ori [] = NONE
1.1132 + | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =
1.1133 + (case refin pblRD ori p of
1.1134 + SOME pblRD' => SOME pblRD'
1.1135 + | NONE => refins pblRD ori pts);
1.1136 +
1.1137 +(*. refine a problem; version providing output for math-experts .*)
1.1138 +fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
1.1139 +(* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
1.1140 + (rev ["linear","system"], fmz, [(*match list*)],
1.1141 + ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
1.1142 + *)
1.1143 + let val _ = (writeln o ((curry op^)"*** pass ") o strs2str)(pblRD @ [pI])
1.1144 + val {thy,ppc,where_,prls,...} = py
1.1145 + val oris = prep_ori fmz thy ppc
1.1146 + (*8.3.02: itms!: oris ev. are _not_ complete here*)
1.1147 + val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)
1.1148 + in if b then pbls @ [Matches (rev (pblRD @ [pI]),
1.1149 + itms2itemppc thy itms pre')]
1.1150 + else pbls @ [NoMatch (rev (pblRD @ [pI]),
1.1151 + itms2itemppc thy itms pre')]
1.1152 + end
1.1153 +(* val pblRD = ["pbla"]; val fmz = fmz1; val pbls = [];
1.1154 + val Ptyp (pI,[py],pys) = hd (!ptyps);
1.1155 + refin' pblRD fmz pbls (Ptyp (pI,[py],pys));
1.1156 +*)
1.1157 + | refin' pblRD fmz pbls (Ptyp (pI,[py],pys)) =
1.1158 + let val _ = (writeln o ((curry op^)"*** pass ") o strs2str) (pblRD @ [pI])
1.1159 + val {thy,ppc,where_,prls,...} = py
1.1160 + val oris = prep_ori fmz thy ppc;
1.1161 + (*8.3.02: itms!: oris ev. are _not_ complete here*)
1.1162 + val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);
1.1163 + in if b
1.1164 + then let val pbl = Matches (rev (pblRD @ [pI]),
1.1165 + itms2itemppc thy itms pre')
1.1166 + in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
1.1167 + else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])
1.1168 + end
1.1169 +and refins' pblRD fmz pbls [] = pbls
1.1170 + | refins' pblRD fmz pbls ((p as Ptyp (pI,_,_))::pts) =
1.1171 + let val pbls' = refin' pblRD fmz pbls p
1.1172 + in case last_elem pbls' of
1.1173 + Matches _ => pbls'
1.1174 + | NoMatch _ => refins' pblRD fmz pbls' pts end;
1.1175 +
1.1176 +(*. refine a problem; version for tactic Refine_Problem .*)
1.1177 +fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
1.1178 + let (*val _ = writeln("### refin''1: pI="^pI);*)
1.1179 + val {thy,ppc,where_,prls,...} = py
1.1180 + val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
1.1181 + in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
1.1182 + else pbls @ [NoMatch_]
1.1183 + end
1.1184 +(* val pblRD = (rev o tl) pblID; val pbls = [];
1.1185 + val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);
1.1186 + *)
1.1187 + | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =
1.1188 + let (*val _ = writeln("### refin''2: pI="^pI);*)
1.1189 + val {thy,ppc,where_,prls,...} = py
1.1190 + val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);
1.1191 + in if b
1.1192 + then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
1.1193 + in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
1.1194 + else (pbls @ [NoMatch_])
1.1195 + end
1.1196 +and refins'' thy pblRD itms pbls [] = pbls
1.1197 + | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) =
1.1198 + let val pbls' = refin'' thy pblRD itms pbls p
1.1199 + in case last_elem pbls' of
1.1200 + Match_ _ => pbls'
1.1201 + | NoMatch_ => refins'' thy pblRD itms pbls' pts end;
1.1202 +
1.1203 +
1.1204 +(*. apply a fun to a ptyps node; copied from get_py .*)
1.1205 +fun app_ptyp f (d:pblID) _ [] =
1.1206 + raise error ("app_ptyp not found: "^(strs2str d))
1.1207 + | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =
1.1208 + if k=k' then f p
1.1209 + else app_ptyp f d ([k]:pblRD) pys
1.1210 + | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') =
1.1211 + if k=k' then app_ptyp f d ks pys
1.1212 + else app_ptyp f d (k::ks) pys';
1.1213 +
1.1214 +(*. for tactic Refine_Tacitly .*)
1.1215 +(*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*)
1.1216 +(* val (thy,pblID) = (assoc_thy dI',pI);
1.1217 + *)
1.1218 +fun refine_ori oris (pblID:pblID) =
1.1219 + let val opt = app_ptyp (refin ((rev o tl) pblID) oris)
1.1220 + pblID (rev pblID) (!ptyps);
1.1221 + in case opt of
1.1222 + SOME pblRD => let val (pblID':pblID) =(rev pblRD)
1.1223 + in if pblID' = pblID then NONE
1.1224 + else SOME pblID' end
1.1225 + | NONE => NONE end;
1.1226 +fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;
1.1227 +
1.1228 +(*. for tactic Refine_Problem .*);
1.1229 +(* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)
1.1230 +(* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);
1.1231 + *)
1.1232 +fun refine_pbl thy (pblID:pblID) itms =
1.1233 + case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms [])
1.1234 + pblID (rev pblID) (!ptyps)) of
1.1235 + NONE => NONE
1.1236 + | SOME (Match_ (rfd as (pI',_))) =>
1.1237 + if pblID = pI' then NONE else SOME rfd;
1.1238 +
1.1239 +
1.1240 +(*. for math-experts .*)
1.1241 +(*19.10.02FIXME: needs thy for parsing fmz*)
1.1242 +(* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID;
1.1243 + val pbls = []; val ptys = !ptyps;
1.1244 + *)
1.1245 +fun refine (fmz:fmz_) (pblID:pblID) =
1.1246 + app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps);
1.1247 +
1.1248 +
1.1249 +(*.make a guh from a reference to an element in the kestore;
1.1250 + EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)
1.1251 +fun pblID2guh (pblID:pblID) =
1.1252 + (((#guh o get_pbt) pblID)
1.1253 + handle _ => raise error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));
1.1254 +fun metID2guh (metID:metID) =
1.1255 + (((#guh o get_met) metID)
1.1256 + handle _ => raise error ("metID2guh: no 'Met_' for '"^
1.1257 + strs2str' metID ^ "'"));
1.1258 +fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID
1.1259 + | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID
1.1260 + | kestoreID2guh ketype kestoreID =
1.1261 + raise error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^
1.1262 + strs2str' kestoreID ^ "'");
1.1263 +
1.1264 +fun show_pblguhs () =
1.1265 + (print_depth 999;
1.1266 + (writeln o strs2str o (map linefeed)) (coll_pblguhs (!ptyps));
1.1267 + print_depth 3);
1.1268 +fun sort_pblguhs () =
1.1269 + (print_depth 999;
1.1270 + (writeln o strs2str o (map linefeed))
1.1271 + (((sort string_ord) o coll_pblguhs) (!ptyps));
1.1272 + print_depth 3);
1.1273 +
1.1274 +fun show_metguhs () =
1.1275 + (print_depth 999;
1.1276 + (writeln o strs2str o (map linefeed)) (coll_metguhs (!mets));
1.1277 + print_depth 3);
1.1278 +fun sort_metguhs () =
1.1279 + (print_depth 999;
1.1280 + (writeln o strs2str o (map linefeed))
1.1281 + (((sort string_ord) o coll_metguhs) (!mets));
1.1282 + print_depth 3);