(* the problems and methods as stored in hierarchies

   author Walther Neuper 1998

   (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 (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))

  | itm_2item _ (Syn c)            = SyntaxE c

  | itm_2item _ (Typ c)            = TypeE c

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

    Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))

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

    Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy (d,ts)))

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

    Missing (Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ 

	     Syntax.string_of_term (thy2ctxt' "Isac") 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)

  | _  => raise 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}

  | _  => raise 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*)

  | _  => raise 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);

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

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

(*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 _ => raise error ("split_dsc: called with "^

			   (Syntax.string_of_term (thy2ctxt' "Isac") 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 _ => raise 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 _ => raise error ("split_did: doesn't match (hd,[arg]) for t = "

          ^(Syntax.string_of_term (thy2ctxt' "Script") t));

(*create output-string for itm_*)

fun itm_out thy (Cor ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))

  | itm_out thy (Syn c)      = c

  | itm_out thy (Typ c)      = c

  | itm_out thy (Inc ((d,ts),_)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))

  | itm_out thy (Sup (d,ts)) = (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))

  | itm_out thy (Mis (d,pid)) = 

    Syntax.string_of_term (thy2ctxt' "Isac") d ^" "^ 

    Syntax.string_of_term (thy2ctxt' "Isac") pid;

(*22.11.00 unused				     

fun itm_ppc2str thy ipc = (ppc2str o (mappc (itm__2str thy))) ipc;*)

(*--3.3.

fun itms2dts itms = 

  let 

    fun coll itms' [] = itms'

      | coll itms' (i::itms) = 

      case i of

	(Cor (d,ts)) => coll (itms' @ [(d,ts)]) itms 

      | (Syn c)      => coll (itms'           ) itms 

      | (Typ c)      => coll (itms'           ) itms 

      | (Fal (d,ts)) => coll (itms' @ [(d,ts)]) itms 

      | (Inc (d,ts)) => coll (itms' @ [(d,ts)]) itms 

      | (Sup (d,ts)) => coll (itms' @ [(d,ts)]) itms

  in coll [] itms end;

*)

(*--3.3.00

fun itm2item ((_,_,_,_,Cor (d,ts)):itm) = 

	      Correct (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))

  | itm2item (_,_,_,_,Syn (c))    = SyntaxE c

  | itm2item (_,_,_,_,Typ (c))    = TypeE c

  | itm2item (_,_,_,_,Fal (d,ts)) = 

	      False (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))

  | itm2item (_,_,_,_,Inc (d,ts)) = 

	      Incompl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)))

  | itm2item (_,_,_,_,Sup (d,ts)) = 

	      Superfl (Syntax.string_of_term (thy2ctxt' "Isac") (comp_dts thy(d,ts)));

*)

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;

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

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

(* --- 9.3.fun add_field dscs (d,ts) = 

  if d mem (get_dsc_in dscs "#Given") 

    then ("#Given",d,ts:term list)

  else if d mem (get_dsc_in dscs "#Find") 

	 then ("#Find",d,ts)

       else if d mem (get_dsc_in dscs "#Relate") 

	      then ("#Relate",d,ts)

	    else ("#undef",d,ts);

(* 28.1.00      raise error ("add_field: '"^

			      (Syntax.string_of_term (thy2ctxt' "Isac") d)^

			      "' not in ppc-description ");         *)

 ------9.3. *)

(* 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*)

     | _ => raise error ("add_field: "^

			 (Syntax.string_of_term (thy2ctxt' "Isac") 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*)    

      (*raise error ("add_field': "^

		     (Syntax.string_of_term (thy2ctxt' "Isac") d)^

		     " not in met"*)

      | _ => raise error ("add_field': "^

			 (Syntax.string_of_term (thy2ctxt' "Isac") 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 [] = raise 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 [] = raise 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 _ [] = raise 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 [] = raise 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 [] _ _ = []

  | prep_ori fmz thy pbt =

  let

    val ctopts = map (parse thy) fmz

    val _= (*FIXME.WN060916 improve error report*)

	if null (filter is_none ctopts) then ()

	else raise error ("prep_ori: SYNTAX ERROR in " ^ strs2str' fmz)

    val dts = map ((split_dts thy) o term_of o the) ctopts

    val ori = map (add_field thy pbt) dts;

(*    val ori = map (flat3 o (pair "#undef")) dts; *)

    val ori' = add_variants ori;

    val maxv = max (map fst ori');

    val maxv = if maxv = 0 then 1(*only 1 variant*) else maxv;

    val ori'' = coll_variants ori';

    val ori''' = map (apfst (replace_0 maxv)) ori'';

    val ori'''' = add_id ori'''

  in (map flattup ori''''):ori list end;

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

(*.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;

(* 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  *)

      calc       : calc list,  (*040207: <--- calclist' in fun prep_met      *)

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

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

      (* compare type pbt:*)

      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 "*___"

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

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

      (*script*)  

      scr: scr (*prep_met requires either script or string "empty_script"*)

	   };

(* ------- template ------------------------------------------------------

store_met

    (prep_met *.thy

	      ([(*"EqSystem","normalize"*)],

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

		("#Find"  ,[  (*dont forget typing non-reals        *)]),

		("#Relate",[])(*may be omitted                      *)  ],

	       {calc = [],             (*filled autom. in prep_met      *)

		crls = Erls,           (*for check_elementwise          *)

		prls = Erls,           (*for evaluating preds in guard  *)

		nrls = Erls,           (*can.simplifier for all formulae*)

		rew_ord'="tless_true", (*for rules in Detail            *)

		rls' = Erls,     (*erls, the eval_rls for cond. in rules*)

		srls = Erls},          (*for evaluating list expr in scr*)

	       "empty_script"

	       ));

---------- template ----------------------------------------------------*)

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, nrls = e_rls,

	      (*asm_thm = []: thm' list,

	      asm_rls = []: rls' list,*)

	      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);*)

(*deprecated due to 'type pat'*)

type pbt_ = (string *  (* field "#Given",..*)

	      (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*)

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

val e_pbt = {guh="pbl_empty",mathauthors=[],init=e_pblID,thy=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 (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  (theory "Pure") metID metID (!mets);

fun get_the (theID:theID) = get_py  (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 d pbt [k] [] = [Ptyp (k, [pbt],[])]

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

((*writeln("### 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) =

((*writeln("### 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 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'.*)

(* val (met as {guh,...}, metID) = 

       ((prep_met EqSystem.thy "met_eqsys" [] e_metID

	      (["EqSystem"],

	       [],

	       {rew_ord'="tless_true", rls' = Erls, calc = [], 

		srls = Erls, prls = Erls, crls = Erls, nrls = Erls},

	       "empty_script"

	       )));

   *)

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"] ...// raise 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 _ => raise error 

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

			 (strs2str pblID)))

		   | _ =>

		     (raise 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 _ => raise error 

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

			 (strs2str pblID)))

		   | _ =>

		     (raise 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 _ => raise error 

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

			 (strs2str pblID)))

		   | _ =>

		     (raise 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, 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

		     [] => []

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

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

		     handle _ => raise error 

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

			 (strs2str metID)))

		   | _ =>

		     (raise 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

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

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

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

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

		     handle _ => raise error 

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

			 (strs2str metID)))

		   | _ =>

		     (raise 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

		     [] => []

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

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

		     handle _ => raise error 

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

			 (strs2str metID)))

		   | _ =>

		     (raise 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

		     [] => []

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

		     ((map (parse_patt thy) wh')

		     handle _ => raise error 

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

			 (strs2str metID)))

		   | _ =>

		     (raise 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 ((map (curry assoc1 (!calclist'))) o (map op_of_calc) o 

		      (filter is_calc) o stacpbls) sc, 

	 crls=cr, nrls=nr, scr=Script 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' thy 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' thy 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' thy 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)) => raise 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;