(* the problems and methods as stored in hierarchies

    author Walther Neuper 1998, Mathias Lehnfeld

    (c) due to copyright terms

 use"ME/ptyps.sml";

 use"ptyps.sml";

 *)

 (*-----------------------------------------vvv-(1) aus modspec.sml 23.3.02*)

 val dsc_unknown = (term_of o the o (parseold @{theory Script})) 

   "unknown::'a => unknow";

 (*-----------------------------------------^^^-(1) aus modspec.sml 23.3.02*)

 (*-----------------------------------------vvv-(2) aus modspec.sml 23.3.02*)

 fun itm_2item thy (Cor ((d,ts),_)) = 

     Correct (term2str (comp_dts (d,ts)))

   | itm_2item _ (Syn c)            = SyntaxE c

   | itm_2item _ (Typ c)            = TypeE c

   | itm_2item thy (Inc ((d,ts),_)) = 

     Incompl (term2str (comp_dts (d,ts)))

   | itm_2item thy (Sup (d,ts))     = 

     Superfl (term2str (comp_dts (d,ts)))

   | itm_2item _ (Mis (d,pid))   =

     Missing (term2str d ^ " " ^ term2str pid);

 (* --- 8.3.00

 fun get_dsc_in dscppc sel = ((the (assoc (dscppc, sel))):term list)

   handle _ => error ("get_dsc_in not for "^sel);

 fun dscs_in dscppc = 

   ((get_dsc_in dscppc "#Given") @

    (get_dsc_in dscppc "#Find") @

    (get_dsc_in dscppc "#Relate")):term list;

    --- 26.1.88

 fun get_dsc_of pblID sel = (the (assoc((snd o get_pbt) pblID, sel)));

 fun get_dsc pblID = 

   (get_dsc_of pblID "#Given") @

   (get_dsc_of pblID "#Find") @

   (get_dsc_of pblID "#Relate");

  --- *)

 fun mappc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) = 

   {Given=map f gi, Where=map f wh,

    Find=map f fi, With=map f wi, Relate=map f re}:'b ppc;

 fun appc f ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) = 

   {Given=f gi, Where=f wh,

    Find=f fi, With=f wi, Relate=f re}:'b ppc;

 (*for ppc of changing type*)

 fun sel_ppc sel ppc =

   case sel of

     "#Given" => #Given (ppc:'a ppc)

   | "#Where" => #Where (ppc:'a ppc)

   | "#Find" => #Find (ppc:'a ppc)

   | "#With" => #With (ppc:'a ppc)

   | "#Relate" => #Relate (ppc:'a ppc)

   | _  => error ("sel_ppc tried to select by '"^sel^"'");

 fun repl_sel_ppc sel

   ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =

   case sel of

     "#Given" => ({Given= x,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)

   | "#Where" => {Given=gi,Where= x,Find=fi,With=wi,Relate=re}

   | "#Find" => {Given=gi,Where=wh,Find= x,With=wi,Relate=re}

   | "#With" => {Given=gi,Where=wh,Find=fi,With= x,Relate=re}

   | "#Relate" => {Given=gi,Where=wh,Find=fi,With=wi,Relate= x}

   | _  => error ("repl_sel_ppc tried to select by '"^sel^"'");

 fun add_sel_ppc thy sel

   ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc) x =

   case sel of

     "#Given" => ({Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}:'a ppc)

   | "#Where" => {Given=gi,Where=wh@[x],Find=fi,With=wi,Relate=re}

   | "#Find"  => {Given=gi,Where=wh,Find=fi@[x],With=wi,Relate=re}

   | "#Relate"=> {Given=gi,Where=wh,Find=fi,With=wi,Relate=re@[x]}

   | "#undef" => {Given=gi@[x],Where=wh,Find=fi,With=wi,Relate=re}(*ori2itmSup*)

   | _  => error ("add_sel_ppc tried to select by '"^sel^"'");

 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =

     ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);

 (*decompose a problem-type into description and identifier

   FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)

 fun split_dsc thy t =

   (let val (hd,args) = strip_comb t

    in if is_dsc hd

       then (hd, args)

        else (e_term, [t])    (*??? 9.01 just copied*)

    end)

   handle _ => error ("split_dsc: called with " ^ term2str t);

 (*

 > val t1 = (term_of o the o (parse thy)) "errorBound err_";

 > split_dsc t1;

 (Const ("Descript.errorBound","bool => Tools.nam"),Free ("err_","bool"))

   : term * term

 > val t3 = (term_of o the o (parse thy)) "valuesFor vs_";

 > split_dsc t3;

 (Const ("Descript.valuesFor","bool List.list => Tools.toreall"),

    Free ("vs_","bool List.list")) : term * term*)

 (*. take the first two return-values; for prep_ori .*)

 (*WN.13.5.03fun split_dts' thy t =

     let val (d, ts, _) = split_dts thy t

     in (d, ts) end;*)

 (*WN.8.12.03 quick for prep_ori'*)

 fun split_dsc' t =

   (let val dsc $ var = t

   in var end)

   handle _ => error ("split_dsc': called with "^term2str t);

 (*9.3.00*)

 (* split a term into description and (id | structured variable)

    for pbt, met.ppc *)

 fun split_did t =

   (let val (hd,[arg]) = strip_comb t

   in (hd,arg) end)

   handle _ => 

          error ("split_did: doesn't match (hd,[arg]) for t = " ^term2str t);

 (*create output-string for itm_*)

 fun itm_out thy (Cor ((d,ts),_)) = term2str (comp_dts (d,ts))

   | itm_out thy (Syn c)      = c

   | itm_out thy (Typ c)      = c

   | itm_out thy (Inc ((d,ts),_)) = term2str (comp_dts (d,ts))

   | itm_out thy (Sup (d,ts)) = term2str (comp_dts (d,ts))

   | itm_out thy (Mis (d,pid)) = term2str d ^ " " ^ term2str pid;

 fun boolterm2item (true, term) = Correct (term2str term)

   | boolterm2item (false, term) = False (term2str term);

 (* use"ME/modspec.sml";

    *)

 fun itms2itemppc thy (itms:itm list) (pre:(bool * term) list) =

   let

     fun coll ppc [] = ppc

       | coll ppc ((_,_,_,field,itm_)::itms) = 

       coll (add_sel_ppc thy field ppc (itm_2item thy itm_)) itms;

     val gfr = coll empty_ppc itms;

   in add_where gfr (map boolterm2item pre) end;

 (* 9.3.00

    compare d and dsc in pbt and transfer field to pre-ori *)

 fun add_field thy pbt (d,ts) = 

   let fun eq d pt = (d = (fst o snd) pt);

   in case filter (eq d) pbt of

        [(fi,(dsc,_))] => (fi,d,ts)

      | [] => ("#undef",d,ts)   (*may come with met.ppc*)

      | _ => error ("add_field: " ^ term2str d ^ " more than once in pbt")

   end;

 (*. take over field from met.ppc at 'Specify_Method' into ori,

    i.e. also removes "#undef" fields                        .*)

 (* val (mpc, ori) =  ((#ppc o get_met) mID, oris);

    *)

 fun add_field' thy mpc (ori:ori list) =

   let fun eq d pt = (d = (fst o snd) pt);

     fun repl mpc (i,v,_,d,ts) = 

       case filter (eq d) mpc of

 	[(fi,(dsc,_))] => [(i,v,fi,d,ts)]

       | [] => [] (*25.2.02: dsc in ori, but not in met -> superfluous*)    

       | _ => error ("add_field': " ^ term2str d ^ " more than once in met");

   in (flat ((map (repl mpc)) ori)):ori list end;

 (*.mark an element with the position within a plateau;

    a plateau with length 1 is marked with 0        .*)

 fun mark eq [] = error "mark []"

   | mark eq xs =

   let

     fun mar xx eq [x] n = xx @ [(if n=1 then 0 else n,x)]

       | mar xx eq (x::x'::xs) n = 

       if eq(x,x') then mar (xx @ [(n,x)]) eq (x'::xs) (n+1)

       else mar (xx @ [(if n=1 then 0 else n,x)]) eq (x'::xs) 1;

   in mar [] eq xs 1 end;

 (*

 > val xs = [1,1,1,2,4,4,5];

 > mark (op=) xs;

 val it = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]

 *)

 (*.assumes equal descriptions to be in adjacent 'plateaus',

    items at a certain position within the plateaus form a variant;

    length = 1 ... marked with 0: covers all variants           .*)

 fun add_variants fdts = 

   let 

     fun eq (a,b) = curry op= (snd3 a) (snd3 b);

   in mark eq fdts end;

 (* collect equal elements: the model for coll_variants *)

 fun coll eq xs =

   let

     fun col xs eq x [] = xs @ [x]

       | col xs eq x (y::ys) = 

       if eq(x,y) then col xs eq x ys

       else col (xs @ [x]) eq y ys;

   in col [] eq (hd xs) xs end;

 (* 

 > val xs = [1,1,1,2,4,4,4];

 > coll (op=) xs;

 val it = [1,2,4] : int list

 *)

 fun max [] = error "max of []"

   | max (y::ys) =

   let fun mx x [] = x

 	| mx x (y::ys) = if x < y then mx y ys else mx x ys;

 in mx y ys end;

 fun gen_max _ [] = error "gen_max of []"

   | gen_max ord (y::ys) =

   let fun mx x [] = x

 	| mx x (y::ys) = if ord (x, y) then mx y ys else mx x ys;

 in mx y ys end;

 (* assumes *)

 fun coll_variants (((v,x)::vxs)) =

   let

     fun col xs (vs,x) [] = xs @ [(vs,x)]

       | col xs (vs,x) ((v',x')::vxs') = 

       if x=x' then col xs (vs @ [v'], x') vxs'

       else col (xs @ [(vs,x)]) ([v'], x') vxs';

   in col [] ([v],x) vxs end;

 (* val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];

 > col [] ([(fst o hd) xs],(snd o hd) xs) (tl xs);

 val it = [([1,2,3],1),([0],2),([1,2],4),([0],5)]  *)

 fun replace_0 vm [0] = intsto vm

   | replace_0 vm vs = vs;

 fun add_id [] = error "add_id []"

   | add_id xs =

   let fun add n [] = []

 	| add n (x::xs) = (n,x) :: add (n+1) xs;

 in add 1 xs end;

 (*

 > val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];

 > add_id xs;

 val it = [(1,([#,#,#],1)),(2,([#],2)),(3,([#,#],4)),(4,([#],5))]

  *)

 fun flattup (a,(b,(c,d,e))) = (a,b,c,d,e);

 fun flattup' (a,(b,((c,d),e))) = (a,b,c,d,e);

 fun flat3 (a,(b,c)) = (a,b,c);

 (*

  val pI = pI';

  !pbts;

 *)

 (* in root (only!) fmz may be empty: fill with ..,dsc,[]

 fun init_ori fmz thy pI =

   if fmz <> [] then prep_ori fmz thy pI (*fmz assumed complete*)

   else

     let 

       val fds = map (cons2 (fst, fst o snd)) (get_pbt pI);

       val vfds = map ((pair [1]) o (rpair [])) fds;

       val ivfds = add_id vfds

     in (map flattup' ivfds):ori list end;   10.3.00---*)

 (* val fmz = ctl; val pI=["sqroot-test","univariate","equation"];

    val (thy,pbt) = (assoc_thy dI',(#ppc o get_pbt) pI');

    val (fmz, thy, pbt) = (fmz, thy, ((#ppc o get_pbt) pI));

    *)

 fun prep_ori [] _ _ = ([], e_ctxt)

   | prep_ori fmz thy pbt =

       let

         val ctxt = Proof_Context.init_global thy |> fold declare_constraints fmz;

         val ori = map (add_field thy pbt o split_dts o the o parseNEW ctxt) fmz

           |> add_variants;

         val maxv = map fst ori |> max;

         val maxv = if maxv = 0 then 1 else maxv;

         val oris = coll_variants ori

           |> map (replace_0 maxv |> apfst)

           |> add_id

           |> map flattup;

       in (oris, ctxt) end;

 (*.the pattern for an item of a problems model or a methods guard.*)

 type pat =

   (string *     (* field               *)

 	  (term *     (* description         *)

 	     term))   (* id | arbitrary term *);

 fun pat2str ((field, (dsc, id)):pat) = 

     pair2str (field, pair2str (term2str dsc, term2str id));

 fun pats2str pats = (strs2str o (map pat2str)) pats;

 val e_errpat = ("e_errpatID", [parse_patt @{theory} "?a = ?b"], [@{thm refl}]): errpat

 val e_fillpat = ("e_fillpatID", parse_patt @{theory} "?a = _", "e_errpatID")

 (* data for methods stored in 'methods'-database*)

 type met = 

      {guh        : guh,        (*unique within this isac-knowledge           *)

       mathauthors: string list,(*copyright                                   *)

       init       : pblID,      (*WN060721 introduced mistakenly--TODO.REMOVE!*)

       rew_ord'   : rew_ord',   (*for rules in Detail

 			                           TODO.WN0509 store fun itself, see 'type pbt'*)

       erls       : rls,        (*the eval_rls for cond. in rules FIXME "rls'

 				                         instead erls in "fun prep_met"              *)

       srls       : rls,        (*for evaluating list expressions in scr      *)

       prls       : rls,        (*for evaluating predicates in modelpattern   *)

       crls       : rls,        (*for check_elementwise, ie. formulae in calc.*)

       nrls       : rls,        (*canonical simplifier specific for this met  *)

       errpats    : errpat list,(*error patterns expected in this method      *)

       calc       : calc list,  (*Theory_Data in fun prep_met                 *)

       (*branch   : TransitiveB set in append_problem at generation ob pblobj

           FIXXXME.0308: set branch from met in Apply_Method ?                *)

       ppc        : pat list,   (*.items in given, find, relate;

 	      items (in "#Find") which need not occur in the arg-list of a SubProblem

         are 'copy-named' with an identifier "*'.'".

         copy-named items are 'generating' if they are NOT "*'''" ?WN120516??

         see ME/calchead.sml 'fun is_copy_named'.                              *)

       pre        : term list,  (*preconditions in where                       *)

       scr        : scr         (*prep_met gets progam or string "empty_script"*)

 	   };

 val e_met = {guh="met_empty",mathauthors=[],init=e_metID,

 	     rew_ord' = "e_rew_ord'": rew_ord',

 	      erls = e_rls, srls = e_rls, prls = e_rls,

 	      calc = [], crls = e_rls, errpats = [], nrls= e_rls,

 	      ppc = []: (string * (term * term)) list,

 	      pre = []: term list,

 	      scr = EmptyScr: scr}:met;

 (** problem-types stored in format for usage in specify  **)

 (*25.8.01 ----

 val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)

 			     (term *   (* description      *)

 			      term))    (* id | struct-var  *)

 			     list)

 		    ) list);*)

 type pbt_ = (string *  (* field "#Given",..*)(*deprecated due to 'type pat'*)

 	      (term *   (* description      *)

 	       term));   (* id | struct-var  *)

 val e_pbt_ = ("#Undef", (e_term, e_term)):pbt_;

 type pbt = 

      {guh  : guh,         (*unique within this isac-knowledge*)

       mathauthors: string list, (*copyright*)

       init  : pblID,      (*to start refinement with*)

       thy   : theory,     (* which allows to compile that pbt

 			  TODO: search generalized for subthy (ref.p.69*)

       (*^^^ WN050912 NOT used during application of the problem,

        because applied terms may be from 'subthy' as well as from super;

        thus we take 'maxthy'; see match_ags !*)

       cas   : term option,(*'CAS-command'*)

       prls  : rls,        (* for preds in where_*)

       where_: term list,  (* where - predicates*)

       ppc   : pat list,

       (*this is the model-pattern; 

        it contains "#Given","#Where","#Find","#Relate"-patterns

        for constraints on identifiers see "fun cpy_nam"*)

       met   : metID list}; (* methods solving the pbt*)

 val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=Thy_Info.get_theory "Pure",

 	     cas=NONE,prls=Erls,where_=[],ppc=[],met=[]}:pbt;

 fun pbt2 (str, (t1, t2)) = 

     pair2str (str, pair2str (term2str t1, term2str t2));

 fun pbt2str pbt = (strs2str o (map (linefeed o pbt2))) pbt;

 val e_Ptyp = Ptyp ("e_pblID",[e_pbt],[]);

 val e_Mets = Ptyp ("e_metID",[e_met],[]);

 type ptyps = (pbt ptyp) list;

 val ptyps = Unsynchronized.ref ([e_Ptyp]:ptyps);

 type mets = (met ptyp) list;

 val mets = Unsynchronized.ref ([e_Mets]:mets);

 (**+ breadth-first search on hierarchy of problem-types +**)

 type pblRD = pblID;(*pblID are Reverted _on calling_ the retrieve-funs*)

      (* eg. ["equations","univariate","normalize"] while

 	    ["normalize","univariate","equations"] is the related pblID

       WN.24.4.03: also used for metID*)

 fun get_py thy d _ [] = 

     error ("get_pbt not found: "^(strs2str d))

   | get_py thy d [k] ((Ptyp (k',[py],_))::pys) =

     if k=k' then py

     else get_py thy d ([k]:pblRD) pys

   | get_py thy d (k::ks) ((Ptyp (k',_,pys))::pys') =

     if k=k' then get_py thy d ks pys

     else get_py thy d (k::ks) pys';

 (*> ptyps:= 

 [Ptyp ("1",[("ptyp 1",([],[]))],

 	[Ptyp ("11",[("ptyp 11",([],[]))],

 		[])

 	 ]),

  Ptyp ("2",[("ptyp 2",([],[]))],

 	[Ptyp ("21",[("ptyp 21",([],[]))],

 		[])

 	 ])

  ];

 > get_py SqRoot.thy ["1"] ["1"] (!ptyps);

 > get_py SqRoot.thy ["2","21"] ["2","21"] (!ptyps);

          _REVERSE_  .......... !!!!!!!!!!*)

 (*TODO: search generalized for subthy*)

 fun get_pbt (pblID:pblID) =

     let val pblRD = rev pblID;

     in get_py (Thy_Info.get_theory "Pure") pblID pblRD (!ptyps) end;

 (* get_pbt thy ["1"];

    get_pbt thy ["21","2"];

    *)

 (*TODO: throws exn 'get_pbt not found: ' ... confusing !!

   take 'ketype' as an argument !!!!!*)

 fun get_met (metID:metID) = get_py  (Thy_Info.get_theory "Pure") metID metID (!mets);

 fun get_the (theID:theID) = get_py  (Thy_Info.get_theory "Pure") theID theID (! thehier);

 fun del_eq k ptyps =

 let fun del k ptyps [] = ptyps

       | del k ptyps ((Ptyp (k', [p], ps))::pys) =

 	if k=k' then del k ptyps pys

 	else del k (ptyps @ [Ptyp (k', [p], ps)]) pys;

 in del k [] ptyps end;

 fun insrt _ pbt [k] [] = [Ptyp (k, [pbt],[])]

   | insrt d pbt [k] ((Ptyp (k', [p], ps))::pys) =

 ((*tracing("### insert 1: ks = "^(strs2str [k])^"    k'= "^k');*)

      if k=k'

      then ((Ptyp (k', [pbt], ps))::pys)

      else (*ev.newly added pbt is free _only_ with 'last_elem pblID'*)

 	 ((Ptyp (k', [p], ps))::(insrt d pbt [k] pys))

 )			 

   | insrt d pbt (k::ks) ((Ptyp (k', [p], ps))::pys) =

 ((*tracing("### insert 2: ks = "^(strs2str (k::ks))^"    k'= "^k');*)

      if k=k'

      then ((Ptyp (k', [p], insrt d pbt ks ps))::pys)

      else 

 	 if length pys = 0

 	 then error ("insert: not found "^(strs2str (d:pblID)))

 	 else ((Ptyp (k', [p], ps))::(insrt d pbt (k::ks) pys))

 );

 fun coll_pblguhs pbls =

     let fun node coll (Ptyp (_,[n],ns)) =

 	    [(#guh : pbt -> guh) n] @ (nodes coll ns)

 	and nodes coll [] = coll

 	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);

     in nodes [] pbls end;

 fun coll_metguhs mets =

     let fun node coll (Ptyp (_,[n],ns)) =

 	    [(#guh : met -> guh) n]

 	and nodes coll [] = coll

 	  | nodes coll (n::ns) = (node coll n) @ (nodes coll ns);

     in nodes [] mets end;

 (*.lookup a guh in hierarchy or methods depending on fst chars in guh.*)

 fun guh2kestoreID (guh:guh) =

     case (implode o (take_fromto 1 4) o Symbol.explode) guh of

 	"pbl_" =>

 	let fun node ids gu (Ptyp (id,[n as {guh,...} : pbt], ns)) =

 		if gu = guh 

 		then SOME ((ids@[id]) : kestoreID)

 		else nodes (ids@[id]) gu ns

 	    and nodes _ _ [] = NONE 

 	      | nodes ids gu (n::ns) = 

 		case node ids gu n of SOME id => SOME id

 				    | NONE =>  nodes ids gu ns

 	in case nodes [] guh (!ptyps) of

 	       SOME id => rev id

 	     | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^

 				    "not found in (!ptyps)")

 	end

       | "met_" =>

 	let fun node ids gu (Ptyp (id,[n as {guh,...} : met], ns)) =

 		if gu = guh 

 		then SOME ((ids@[id]) : kestoreID)

 		else nodes (ids@[id]) gu ns

 	    and nodes _ _ [] = NONE 

 	      | nodes ids gu (n::ns) = 

 		case node ids gu n of SOME id => SOME id

 				    | NONE =>  nodes ids gu ns

 	in case nodes [] guh (!mets) of

 	       SOME id => id

 	     | NONE => error ("guh2kestoreID: '" ^ guh ^ "' " ^

 				    "not found in (!mets)") end

       | _ => error ("guh2kestoreID called with '" ^ guh ^ "'");

 (*> guh2kestoreID "pbl_equ_univ_lin";

 val it = ["linear", "univariate", "equation"] : string list*)

 fun check_pblguh_unique (guh:guh) (pbls: (pbt ptyp) list) =

     if member op = (coll_pblguhs pbls) guh

     then error ("check_guh_unique failed with '"^guh^"';\n"^

 		      "use 'sort_pblguhs()' for a list of guhs;\n"^

 		      "consider setting 'check_guhs_unique := false'")

     else ();

 (* val (guh, mets) = ("met_test", !mets);

    *)

 fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =

     if member op = (coll_metguhs mets) guh

     then error ("check_guh_unique failed with '"^guh^"';\n"^

 		      "use 'sort_metguhs()' for a list of guhs;\n"^

 		      "consider setting 'check_guhs_unique := false'")

     else ();

 (*.the pblID has the leaf-element as first; better readability achieved;.*)

 fun store_pbt (pbt as {guh,...}, pblID) = 

     (if (!check_guhs_unique) then check_pblguh_unique guh (!ptyps) else ();

      ptyps:= insrt pblID pbt (rev pblID) (!ptyps));

 (*.the metID has the root-element as first; compare 'fun store_pbt'.*)

 fun store_met (met as {guh,...}, metID) =

     (if (!check_guhs_unique) then check_metguh_unique guh (!mets) else ();

      mets:= insrt metID met metID (!mets));

 (*. prepare problem-types before storing in pbltypes; 

     dont forget to 'check_guh_unique' before ins.*)

 fun prep_pbt thy guh maa init

 	     (pblID, dsc_dats: (string * (string list)) list, 

 		  ev:rls, ca: string option, metIDs:metID list) =

 (* val (thy, (pblID, dsc_dats: (string * (string list)) list, 

 		  ev:rls, ca: string option, metIDs:metID list)) =

        ((EqSystem.thy, (["system"],

 		       [("#Given" ,["equalities es_", "solveForVars vs_"]),

 			("#Find"  ,["solution ss___"](*___ is copy-named*))

 			],

 		       append_rls "e_rls" e_rls [(*for preds in where_*)], 

 		       SOME "solveSystem es_ vs_", 

 		       [])));

    *)

     let fun eq f (f', _) = f = f';

 	val gi = filter (eq "#Given") dsc_dats;

 (*val gi = [("#Given",["equality e_","solveFor v_"])]

   : (string * string list) list*)

 	val gi = (case gi of

 		     [] => []

 		   | ((_,gi')::[]) => 

 		     ((map (split_did o term_of o the o (parse thy)) gi')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Given' of "^

 			 (strs2str pblID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Given' in "^

 				  (strs2str pblID))));

 (*val gi =

   [(Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool")),

    (Const ("Descript.solveFor","RealDef.real => Tools.una"),

     Free ("v_","RealDef.real"))] : (term * term) list  *)

 	val gi = map (pair "#Given") gi;

 (*val gi =

   [("#Given",

     (Const ("Descript.equality","bool => Tools.una"),Free ("e_","bool"))),

    ("#Given",

     (Const ("Descript.solveFor","RealDef.real => Tools.una"),

      Free ("v_","RealDef.real")))] : (string * (term * term)) list*)

 	val fi = filter (eq "#Find") dsc_dats;

 	val fi = (case fi of

 		     [] => [](*28.8.01: ["tool"] ...// error 

 			("prep_pbt: no '#Find' in "^(strs2str pblID))*)

 (* val ((_,fi')::[]) = fi;

    *)

 		   | ((_,fi')::[]) => 

 		     ((map (split_did o term_of o the o (parse thy)) fi')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Find' of "^

 			 (strs2str pblID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Find' in "^

 				  (strs2str pblID))));

 	val fi = map (pair "#Find") fi;

 	val re = filter (eq "#Relate") dsc_dats;

 	val re = (case re of

 		     [] => []

 		   | ((_,re')::[]) => 

 		     ((map (split_did o term_of o the o (parse thy)) re')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Relate' of "^

 			 (strs2str pblID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Relate' in "^

 				  (strs2str pblID))));

 	val re = map (pair "#Relate") re;

 	val wh = filter (eq "#Where") dsc_dats;

 	val wh = (case wh of

 		     [] => []

 		   | ((_,wh')::[]) => 

 		     ((map (parse_patt thy) wh')

 		      handle _ => error 

 			("prep_pbt: syntax error in '#Where' of "^

 			 (strs2str pblID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Where' in "^

 				  (strs2str pblID))));

     in ({guh=guh,mathauthors=maa,init=init,

 	 thy=thy,cas= case ca of NONE => NONE

 			       | SOME s => 

 				 SOME ((term_of o the o (parse thy)) s),

 	 prls=ev,where_=wh,ppc= gi @ fi @ re,

 	 met=metIDs}, pblID):pbt * pblID end;

 (* prep_pbt thy (pblID, dsc_dats, metIDs);   

  val it =

   ({met=[],

     ppc=[("#Given",(Const (#,#),Free (#,#))),

          ("#Given",(Const (#,#),Free (#,#))),

          ("#Find",(Const (#,#),Free (#,#)))],

     thy={ProtoPure, ..., Atools, RatArith},

     where_=[Const ("Descript.solutions","bool List.list => Tools.toreall") $

             Free ("v_i_","bool List.list")]},["equation"]) : pbt * pblID    *)

 (*. prepare met for storage analogous to pbt .*)

 fun prep_met thy guh maa init

 	     (metID, ppc: (string * string list) list (*'#Where' -> #pre*),

     {rew_ord'=ro, rls'=rls, srls=srls, prls=prls, 

      calc = scr_isa_fns(*FIXME.040207: del - auto-done*),

      crls=cr, errpats = ep, nrls= nr}, scr) =

     let fun eq f (f', _) = f = f';

 	(*val thy = (assoc_thy o fst) metID*)

 	val gi = filter (eq "#Given") ppc;

 	val gi = (case gi of

 		     [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])

 		   | ((_,gi')::[]) => 

 		     ((map (split_did o term_of o the o (parse thy)) gi')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Given' of "^

 			 (strs2str metID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Given' in "^

 				  (strs2str metID))));

 	val gi = map (pair "#Given") gi;

 	val fi = filter (eq "#Find") ppc;

 	val fi = (case fi of

 		     [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])

 		   | ((_,fi')::[]) => 

 		     ((map (split_did o term_of o the o (parse thy)) fi')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Find' of "^

 			 (strs2str metID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Find' in "^

 				  (strs2str metID))));

 	val fi = map (pair "#Find") fi;

 	val re = filter (eq "#Relate") ppc;

 	val re = (case re of

 		     [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])

 		   | ((_,re')::[]) => 

 		     ((map (split_did o term_of o the o (parse thy)) re')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Relate' of "^

 			 (strs2str metID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Relate' in "^

 				  (strs2str metID))));

 	val re = map (pair "#Relate") re;

 	val wh = filter (eq "#Where") ppc;

 	val wh = (case wh of

 		     [] => (writeln ("prep_met: in " ^ guh ^ " #Where is empty ?!?"); [])

 		   | ((_,wh')::[]) => 

 		     ((map (parse_patt thy) wh')

 		     handle _ => error 

 			("prep_pbt: syntax error in '#Where' of "^

 			 (strs2str metID)))

 		   | _ =>

 		     (error ("prep_pbt: more than one '#Where' in "^

 				  (strs2str metID))));

 	val sc = (((inst_abs thy) o term_of o the o (parse thy)) scr)

     in ({guh=guh,mathauthors=maa,init=init,

 	 ppc=gi@fi@re, pre=wh, rew_ord'=ro, erls=rls, srls=srls, prls=prls,

 	 calc = if scr = "empty_script" then []

 		else ((assoc_calc' thy |> map) o (map op_of_calc) o 

 		      (filter is_calc) o stacpbls) sc, 

 	 crls=cr, errpats = ep, nrls= nr, scr = Prog sc}:met,

 	metID:metID)

     end;

 (**. get pblIDs of all entries in mat3D .**)

 fun format_pblID strl = enclose " [" "]" (commas_quote strl);

 fun format_pblIDl strll = enclose "[\n" "\n]\n" 

     (space_implode ",\n" (map format_pblID strll));

 fun scan _  [] = [] (* no base case, for empty doms only *)

   | scan id ((Ptyp ((i,_,[])))::[]) =      [id@[i]]

   | scan id ((Ptyp ((i,_,pl)))::[]) = scan (id@[i]) pl

   | scan id ((Ptyp ((i,_,[])))::ps) =      [id@[i]]    @(scan id ps)

   | scan id ((Ptyp ((i,_,pl)))::ps) =(scan (id@[i]) pl)@(scan id ps);

 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (!ptyps);

 (* ptyps:=[];

    show_ptyps();

    *)

 fun show_mets () = (writeln o format_pblIDl o (scan [])) (!mets);

 (*vvvvv---------- preparational work 8.01. UNUSED *)

 (**+ instantiate a problem-type +**)

 (*+ transform oris +*)

 fun coll_vats (vats, ((_,vs,_,_,_):ori)) = union op = vats vs;

 (*> coll_vats [11,22] (hd oris);

 val it = [22,11,1,2,3] : int list

 > foldl coll_vats ([],oris);

 val it = [1,2,3] : int list

 > val i=1;

 > filter ((curry (op mem) i) o #2) oris;

 val it =

   [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

    (2,[1,2,3],"#Find",Const (#,#),[Free #]),

    (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

    (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),

    (6,[1],"#undef",Const (#,#),[Free #]),

    (9,[1,2],"#undef",Const (#,#),[# $ #]),

    (11,[1,2,3],"#undef",Const (#,#),[# $ #])] : ori list *)    

 local infix mem; (*from Isabelle2002*)

 fun x mem [] = false

   | x mem (y :: ys) = x = y orelse x mem ys;

 in

 fun filter_vat oris i = 

     filter ((curry (op mem) i) o (#2 : ori -> int list)) oris;

 end;

 (*> map (filter_vat oris) [1,2,3];

 val it =

   [[(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

     (2,[1,2,3],"#Find",Const (#,#),[Free #]),

     (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

     (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),

     (6,[1],"#undef",Const (#,#),[Free #]),

     (9,[1,2],"#undef",Const (#,#),[# $ #]),

     (11,[1,2,3],"#undef",Const (#,#),[# $ #])],

    [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

     (2,[1,2,3],"#Find",Const (#,#),[Free #]),

     (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

     (4,[1,2],"#Relate",Const (#,#),[# $ #,# $ #]),

     (7,[2],"#undef",Const (#,#),[Free #]),

     (9,[1,2],"#undef",Const (#,#),[# $ #]),

     (11,[1,2,3],"#undef",Const (#,#),[# $ #])],

    [(1,[1,2,3],"#Given",Const (#,#),[# $ #]),

     (2,[1,2,3],"#Find",Const (#,#),[Free #]),

     (3,[1,2,3],"#Find",Const (#,#),[# $ #,# $ #]),

     (5,[3],"#Relate",Const (#,#),[# $ #,# $ #,# $ #]),

     (8,[3],"#undef",Const (#,#),[Free #]),

     (10,[3],"#undef",Const (#,#),[# $ #]),

     (11,[1,2,3],"#undef",Const (#,#),[# $ #])]] : ori list list*)

 fun separate_vats oris =

     let val vats = foldl coll_vats ([] : int list, oris);

     in map (filter_vat oris) vats end;

 (*^^^ end preparational work 8.01.*)

 (**. check a problem (ie. itm list) for matching a problemtype .**)

 fun eq1 d (_,(d',_)) = (d = d');

 fun itm_id ((i,_,_,_,_):itm) = i;

 fun ori_id ((i,_,_,_,_):ori) = i;

 fun ori2itmSup ((i,v,_,d,ts):ori) = ((i,v,true,"#Given",Sup(d,ts)):itm);

 (*see + add_sel_ppc                             ~~~~~~~*)

 fun field_eq f ((_,_,f',_,_):ori) = f = f';

 (*. check an item (with arbitrary itm_ from previous matchings) 

     for matching a problemtype; returns true only for itms found in pbt .*)

 fun chk_ thy pbt ((i,vats,b,f,Cor ((d,vs),_)):itm) =

     (case find_first (eq1 d) pbt of 

 	 SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),

 					      (id, pbl_ids' d vs))):itm)

        | NONE => (i,vats,false,f,Sup (d,vs)))

   | chk_ thy pbt ((i,vats,b,f,Inc ((d,vs),_)):itm) =

     (case find_first (eq1 d) pbt of 

 	SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),

 					     (id, pbl_ids' d vs))):itm)

       | NONE => (i,vats,false,f,Sup (d,vs)))

   | chk_ thy pbt (itm as (i,vats,b,f,Syn ct):itm) = itm

   | chk_ thy pbt (itm as (i,vats,b,f,Typ ct):itm) = itm

   | chk_ thy pbt ((i,vats,b,f,Sup (d,vs)):itm) =

     (case find_first (eq1 d) pbt of 

 	SOME (_,(_,id)) => ((i,vats,b,f,Cor ((d,vs),

 					     (id, pbl_ids' d vs))):itm)

       | NONE => (i,vats,false,f,Sup (d,vs)))

 (* val (i,vats,b,f,Mis (d,vs)) = i4;

    *)

   | chk_ thy pbt ((i,vats,b,f,Mis (d,vs)):itm) =

     (case find_first (eq1 d) pbt of

 (* val SOME (_,(_,id)) = find_first (eq1 d) pbt;

    *) 

 	SOME (_,(_,id)) => error "chk_: ((i,vats,b,f,Cor ((d,vs),\

 				   \(id, pbl_ids' d vs))):itm)"

       | NONE => (i,vats,false,f,Sup (d,[vs])));

 (* chk_ thy pbt i

     *)

 fun eq2 (_,(d,_)) ((_,_,_,_,itm_):itm) = d = d_in itm_;

 fun eq2' (_,(d,_)) ((_,_,_,d',_):ori) = d = d';

 fun eq0 ((0,_,_,_,_):itm) = true

   | eq0 _ = false;

 fun max_i i [] = i

   | max_i i ((id,_,_,_,_)::is) = 

     if i > id then max_i i is else max_i id is;

 fun max_id [] = 0

   | max_id ((id,_,_,_,_)::is) = max_i id is;

 fun add_idvat itms _ _ [] = itms

   | add_idvat itms i mvat (((_,_,b,f,itm_):itm)::its) =

     add_idvat (itms @ [(i,[(*mvat ...meaningless with pbl-identifier *)

 			     ],b,f,itm_):itm]) (i+1) mvat its;

 (*. find elements of pbt not contained in itms;

     if such one is untouched, return this one, otherwise create new itm .*)

 fun chk_m (itms:itm list) untouched (p as (f,(d,id))) = 

     case find_first (eq2 p) itms of

 	SOME _ => []

       | NONE => (case find_first (eq2 p) untouched of

 		     SOME itm => [itm]

 		   | NONE => [(0,[],false,f,Mis (d,id)):itm]);

 (* val itms = itms'';

    *) 

 fun chk_mis mvat itms untouched pbt = 

     let val mis = (flat o (map (chk_m itms untouched))) pbt; 

         val mid = max_id itms;

     in add_idvat [] (mid + 1) mvat mis end;

 (*. check a problem (ie. itm list) for matching a problemtype, 

     takes the max_vt for concluding completeness (could be another!) .*)

 (* val itms = itms'; val (pbt,pre) = (ppc, pre);

    val itms = itms; val (pbt,pre) = (ppc, pre);

    *)

 fun match_itms thy itms (pbt,pre,prls) = 

     (let fun okv mvat (_,vats,b,_,_) = member op = vats mvat

 				       andalso b;

 	val itms' = map (chk_ thy pbt) itms; (*all found are #3 true*)

         val mvat = max_vt itms';

 	val itms'' = filter (okv mvat) itms';

 	val untouched = filter eq0 itms;(*i.e. dsc only (from init)*)

 	val mis = chk_mis mvat itms'' untouched pbt;

 	val pre' = check_preconds' prls pre itms'' mvat

 	val pb = foldl and_ (true, map fst pre')

     in (length mis = 0 andalso pb, (itms'@ mis, pre')) end);

 (*. check a problem pbl (ie. itm list) for matching a problemtype pbt,

     for missing items get data from formalization (ie. ori list); 

     takes the max_vt for concluding completeness (could be another!) .*)

 (*  (0) determine the most frequent variant mv in pbl

     ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>

              (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;

              (3) newitms = filter (mv mem vat(news)) news 

     (4) pbt @ newitms                                           *)

 (* val (pbl, pbt, pre) = (met, mtt, pre);

    val (pbl, pbt, pre) = (itms, #ppc pbt, #where_ pbt);

    val (pbl, pbt, pre) = (itms, ppc, where_);

    *)

 fun match_itms_oris thy (pbl:itm list) (pbt, pre, prls) oris =

   let 

  (*0*)val mv = max_vt pbl;

       fun eqdsc_pbt_itm ((_,(d,_))) ((_,_,_,_,itm_):itm) = d = d_in itm_;

       fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of

 				SOME _ => false | NONE => true;

  (*1*)val mis = (*(map (cons2 (fst, fst o snd)))o*) (filter (notmem pbl)) pbt;

       fun eqdsc_ori (_,(d,_)) ((_,_,_,d',_):ori) = d = d';

       fun ori2itmMis (f,(d,pid)) ((i,v,_,_,ts):ori) = 

 	  (i,v,false,f,Mis (d,pid)):itm;

  (*2*)fun oris2itms oris mis1 = 

 	  ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;

       val news = (flat o (map (oris2itms oris))) mis;

  (*3*)fun mem_vat (_,vats,b,_,_) = member op = vats mv;

       val newitms = filter mem_vat news;

  (*4*)val itms' = pbl @ newitms;

       val pre' = check_preconds' prls pre itms' mv

       val pb = foldl and_ (true, map fst pre')

   in (length mis = 0 andalso pb, (itms', pre')) end;

     (*handle _ => (false,([],[]))*);

 (*vvv--- doubled 20.9.01: ... 7.3.02 itms  -->  oris, because oris

   allow for faster access to descriptions and terms *)

 (**. check a problem (ie. itm list) for matching a problemtype .**)

 (*. check an ori for matching a problemtype by description; 

     returns true only for itms found in pbt .*)

 fun chk1_ thy pbt ((i,vats,f,d,vs):ori) =

     case find_first (eq1 d) pbt of 

 	SOME (_,(_,id)) => [(i,vats,true,f,

 			     Cor ((d,vs), (id, pbl_ids' d vs))):itm]

       | NONE => [];

 (* elem 'p' of pbt contained in itms ? *)

 fun chk1_m (itms:itm list) p = 

     case find_first (eq2 p) itms of

 	SOME _ => true | NONE => false;

 fun chk1_m' (oris: ori list) (p as (f,(d,t))) = 

     case find_first (eq2' p) oris of

 	SOME _ => []

       | NONE => [(f, Mis (d, t))];

 fun pair0vatsfalse (f,itm_) = (0,[],false,f,itm_):itm;

 fun chk1_mis mvat itms ppc = foldl and_ (true, map (chk1_m itms) ppc);

 fun chk1_mis' oris ppc = 

     map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);

 (*. check a problem (ie. ori list) for matching a problemtype, 

     takes the max_vt for concluding completeness (FIXME could be another!) .*)

 (* val (prls,oris,pbt,pre)=(#prls py, ori, #ppc py, #where_ py);

    *)

 fun match_oris thy prls oris (pbt,pre) = 

     let val itms = (flat o (map (chk1_ thy pbt))) oris;

         val mvat = max_vt itms;

 	val complete = chk1_mis mvat itms pbt;

 	val pre' = check_preconds' prls pre itms mvat

 	val pb = foldl and_ (true, map fst pre')

     in if complete andalso pb then true else false end;

 (*. check a problem (ie. ori list) for matching a problemtype, 

     returns items for output to math-experts .*)

 fun match_oris' thy oris (ppc,pre,prls) =

 (* val (thy, oris, (ppc,pre,prls)) = (thy, oris, (ppc, where_, prls));

    *)

     let val itms = (flat o (map (chk1_ thy ppc))) oris;

 	val sups = ((map ori2itmSup) o (filter(field_eq "#undef")))oris;

         val mvat = max_vt itms;

 	val miss = chk1_mis' oris ppc;

 	val pre' = check_preconds' prls pre itms mvat

 	val pb = foldl and_ (true, map fst pre')

     in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;

 (* for the user *)

 datatype match' = 

   Matches' of item ppc

 | NoMatch' of item ppc;

 (* match a formalization with a problem type *)

 fun match_pbl (fmz:fmz_) ({thy=thy,where_=pre,ppc,prls=er,...}:pbt) =

     let val oris = prep_ori fmz thy ppc |> #1;

 	val (bool, (itms, pre')) = match_oris' thy oris (ppc,pre,er);

     in if bool then Matches' (itms2itemppc thy itms pre')

        else NoMatch' (itms2itemppc thy itms pre') end;

 (* 

 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

 	      "solveFor x","errorBound (eps=0)","solutions L"];

 val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =

     get_pbt ["univariate","equation"];

 match_pbl fmz pbt;

 *)

 (*. refine a problem; construct pblRD while scanning .*)

 (* val (pblRD,ori)=("xxx",oris);

  val py = get_pbt ["equation"];

  val py = get_pbt ["univariate","equation"];

  val py = get_pbt ["linear","univariate","equation"];

  val py = get_pbt ["root'","univariate","equation"];

  match_oris (#prls py) ori (#ppc py, #where_ py);

   *)

 fun refin (pblRD:pblRD) ori 

 ((Ptyp (pI,[py],[])):pbt ptyp) =

     if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) 

     then SOME ((pblRD @ [pI]):pblRD)

     else NONE

   | refin pblRD ori (Ptyp (pI,[py],pys)) =

     if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py) 

     then (case refins (pblRD @ [pI]) ori pys of

 	      SOME pblRD' => SOME pblRD'

 	    | NONE => SOME (pblRD @ [pI]))

     else NONE

 and refins pblRD ori [] = NONE

   | refins pblRD ori ((p as Ptyp (pI,_,_))::pts) =

     (case refin pblRD ori p of

 	 SOME pblRD' => SOME pblRD'

        | NONE => refins pblRD ori pts);

 (*. refine a problem; version providing output for math-experts .*)

 fun refin' (pblRD: pblRD) fmz pbls ((Ptyp (pI, [py], [])):pbt ptyp) =

     let

       val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])

       val {thy, ppc, where_, prls, ...} = py 

       val oris = prep_ori fmz thy ppc |> #1;

       (*8.3.02: itms!: oris ev. are _not_ complete here*)

       val (b, (itms, pre')) = match_oris' thy oris (ppc, where_, prls)

     in if b

       then pbls @ [Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]

       else pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]

     end

   | refin' pblRD fmz pbls (Ptyp (pI, [py], pys)) =

     let

       val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])

       val {thy, ppc, where_, prls, ...} = py 

       val oris = prep_ori fmz thy ppc |> #1;

       (*8.3.02: itms!: oris ev. are _not_ complete here*)

       val(b, (itms, pre')) = match_oris' thy oris (ppc,where_,prls);

     in if b 

       then let val pbl = Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')

 	      in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end

       else (pbls @ [NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')])

     end

 and refins' pblRD fmz pbls [] = pbls

   | refins' pblRD fmz pbls ((p as Ptyp (pI, _, _))::pts) =

     let val pbls' = refin' pblRD fmz pbls p

     in case last_elem pbls' of

         Matches _ => pbls'

       | NoMatch _ => refins' pblRD fmz pbls' pts

     end;

 (*. refine a problem; version for tactic Refine_Problem .*)

 fun refin'' thy (pblRD:pblRD) itms pbls ((Ptyp (pI,[py],[])):pbt ptyp) =

     let (*val _ = tracing("### refin''1: pI="^pI);*)

 	val {thy,ppc,where_,prls,...} = py 

 	val (b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);

     in if b then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]

        else pbls @ [NoMatch_] 

     end

 (* val pblRD = (rev o tl) pblID; val pbls = []; 

    val Ptyp (pI,[py],pys) = app_ptyp I pblID (rev pblID) (!ptyps);

    *)

   | refin'' thy pblRD itms pbls (Ptyp (pI,[py],pys)) =

     let (*val _ = tracing("### refin''2: pI="^pI);*)

 	val {thy,ppc,where_,prls,...} = py 

 	val(b, (itms', pre')) = match_itms thy itms (ppc,where_,prls);

     in if b 

        then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))

 	    in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end

        else (pbls @ [NoMatch_])

     end

 and refins'' thy pblRD itms pbls [] = pbls

   | refins'' thy pblRD itms pbls ((p as Ptyp (pI,_,_))::pts) =

     let val pbls' = refin'' thy pblRD itms pbls p

     in case last_elem pbls' of

 	 Match_ _ => pbls'

        | NoMatch_ => refins'' thy pblRD itms pbls' pts end;

 (*. apply a fun to a ptyps node; copied from get_py .*)

 fun app_ptyp f (d:pblID) _ [] = 

     error ("app_ptyp not found: "^(strs2str d))

   | app_ptyp f d (k::[]) ((p as Ptyp (k',[py],_))::pys) =

     if k=k' then f p

     else app_ptyp f d ([k]:pblRD) pys

   | app_ptyp f d (k::ks) ((Ptyp (k',_,pys))::pys') =

     if k=k' then app_ptyp f d ks pys

     else app_ptyp f d (k::ks) pys';

 (*. for tactic Refine_Tacitly .*)

 (*!!! oris are already created wrt. some pbt; pbt contains thy for parsing*)

 (* val (thy,pblID) = (assoc_thy dI',pI);

    *)

 fun refine_ori oris (pblID:pblID) =

     let val opt = app_ptyp (refin ((rev o tl) pblID) oris) 

 			   pblID (rev pblID) (!ptyps);

     in case opt of 

 	   SOME pblRD => let val (pblID':pblID) =(rev pblRD)

 			 in if pblID' = pblID then NONE

 			    else SOME pblID' end

 	 | NONE => NONE end;

 fun refine_ori' oris pI = (the (refine_ori oris pI)) handle _ => pI;

 (*. for tactic Refine_Problem .*); 

 (* 10.03: returnvalue -> (pIrefined, itm list) would be sufficient *)

 (* val pblID = pI; app_ptyp I pblID (rev pblID) (!ptyps);

    *)

 fun refine_pbl thy (pblID:pblID) itms =

     case refined_ (app_ptyp (refin'' thy ((rev o tl) pblID) itms []) 

 			    pblID (rev pblID) (!ptyps)) of

 	NONE => NONE

       | SOME (Match_ (rfd as (pI',_))) => 

 	if pblID = pI' then NONE else SOME rfd;

 (*. for math-experts .*)

 (*FIXME.WN021019: needs thy for parsing fmz*)

 (* val fmz = fmz1; val pblID = ["pbla"]; val pblRD = (rev o tl) pblID; 

    val pbls = []; val ptys = !ptyps;

    *)

 fun refine (fmz:fmz_) (pblID:pblID) =

   app_ptyp (refin' ((rev o tl) pblID) fmz []) pblID (rev pblID) (!ptyps);

 (*.make a guh from a reference to an element in the kestore;

    EXCEPT theory hierarchy ... compare 'fun keref2xml'.*)

 fun pblID2guh (pblID:pblID) =

     (((#guh o get_pbt) pblID)

      handle _ => error ("pblID2guh: not for '"^strs2str' pblID ^ "'"));

 fun metID2guh (metID:metID) =

     (((#guh o get_met) metID)

      handle _ => error ("metID2guh: no 'Met_' for '"^

 			      strs2str' metID ^ "'"));

 fun kestoreID2guh Pbl_ (kestoreID:kestoreID) = pblID2guh kestoreID

   | kestoreID2guh Met_ (kestoreID:kestoreID) = metID2guh kestoreID

   | kestoreID2guh ketype kestoreID =

     error ("kestoreID2guh: '" ^ ketype2str ketype ^ "' not for '" ^

 		 strs2str' kestoreID ^ "'");

 fun show_pblguhs () =

     (print_depth 999; 

      (tracing o strs2str o (map linefeed)) (coll_pblguhs (!ptyps)); 

      print_depth 3);

 fun sort_pblguhs () =

     (print_depth 999; 

      (tracing o strs2str o (map linefeed)) 

 	 (((sort string_ord) o coll_pblguhs) (!ptyps)); 

      print_depth 3);

 fun show_metguhs () =

     (print_depth 999; 

      (tracing o strs2str o (map linefeed)) (coll_metguhs (!mets)); 

      print_depth 3);

 fun sort_metguhs () =

     (print_depth 999; 

      (tracing o strs2str o (map linefeed)) 

 	 (((sort string_ord) o coll_metguhs) (!mets)); 

      print_depth 3);