1.1 --- a/src/Tools/isac/ME/ptyps.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1279 +0,0 @@
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);