(* the problems and methods as stored in hierarchies

   author Walther Neuper 1998, Mathias Lehnfeld

   (c) due to copyright terms

*)

signature MODEL_SPECIFY =

sig

  type field

  (* for calchead.sml, if below at left margin *)

  val prep_ori : Selem.fmz_ -> theory -> field list -> Model.ori list * Proof.context

  val add_id : 'a list -> (int * 'a) list

  val add_field' : theory -> field list -> Model.ori list -> Model.ori list

  val match_itms_oris : theory -> Model.itm list -> field list * term list * rls ->

    Model.ori list -> bool * (Model.itm list * (bool * term) list)

  val refine_ori : Model.ori list -> pblID -> pblID option

  val refine_ori' : Model.ori list -> pblID -> pblID

  val refine_pbl : theory -> pblID -> Model.itm list -> (pblID * (Model.itm list * (bool * term) list)) option

  val appc : ('a list -> 'b list) -> 'a Model.ppc -> 'b Model.ppc

  val mappc : ('a -> 'b) -> 'a Model.ppc -> 'b Model.ppc

  val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc   (* for generate.sml *)

  val get_pbt : pblID -> pbt

  val get_met : metID -> met                                                (* for generate.sml *)

  val get_met' : theory -> metID -> met                            (* for pbl-met-hierarchy.sml *)

  val get_the : theID -> thydata                                              (* for inform.sml *)

  type pblRD = string list                                         (* for pbl-met-hierarchy.sml *)

  val format_pblIDl : string list list -> string                       (* for thy-hierarchy.sml *)

  val scan : string list -> 'a ptyp list -> string list list           (* for thy-hierarchy.sml *)

  val itm_out : theory -> Model.itm_ -> string

  val dsc_unknown : term

  val pblID2guh : pblID -> guh                                             (* for datatypes.sml *)

  val metID2guh : metID -> guh                                             (* for datatypes.sml *)

  val kestoreID2guh : ketype -> kestoreID -> guh                           (* for datatypes.sml *)

  val guh2kestoreID : guh -> string list                                   (* for interface.sml *)

  (* for Knowledge/, if below at left margin *)

  val prep_pbt : theory -> guh -> string list -> pblID ->

    string list * (string * string list) list * rls * string option * metID list -> pbt * pblID

  val prep_met : theory -> string -> string list -> pblID ->

     string list * (string * string list) list *

     {calc: 'a, crls: rls, errpats: errpat list, nrls: rls, prls: rls, rew_ord': rew_ord', rls': rls, srls: rls}

     * string -> met * metID

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val show_ptyps : unit -> unit

  val show_mets : unit -> unit

  datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc

  val match_pbl : Selem.fmz_ -> pbt -> match'

  val refine : Selem.fmz_ -> pblID -> Stool.match list

  val e_errpat : errpat

  val show_pblguhs : unit -> unit

  val sort_pblguhs : unit -> unit

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  val e_fillpat : string * term * string

  val coll_vats : ''a list * ('b * ''a list * 'c * 'd * 'e) -> ''a list

  val filter_vat : Model.ori list -> int -> Model.ori list

  val show_metguhs : unit -> unit

  val sort_metguhs : unit -> unit

end

structure Specify(**) : MODEL_SPECIFY(**) =

struct

open Model

type field = string * (term * term)

val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory Script})) "unknown::'a => unknow";

fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (term2str (Model.comp_dts (d, ts)))

  | itm_2item _ (Model.Syn c) = Model.SyntaxE c

  | itm_2item _ (Model.Typ c) = Model.TypeE c

  | itm_2item _ (Model.Inc ((d, ts), _)) = Model.Incompl (term2str (Model.comp_dts (d, ts)))

  | itm_2item _ (Model.Sup (d, ts)) = Model.Superfl (term2str (Model.comp_dts (d, ts)))

  | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (term2str d ^ " " ^ term2str pid)

  | itm_2item _ _ = error "itm_2item: uncovered definition"

fun mappc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} = 

  {Given= map f gi, Where = map f wh, Find = map f fi, With = map f wi, Relate = map f re}

fun appc f {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} = 

  {Given = f gi, Where = f wh, Find = f fi, With = f wi, Relate = f re}

fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =

  case sel of

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

  | "#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, Where = _, Find = fi, With = wi, Relate = re} wh =

  {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}

(* split a term into description and (id | structured variable) for pbt, met.ppc *)

fun split_did t =

  let

    val (hd, arg) = case strip_comb t of

      (hd, [arg]) => (hd, arg)

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

  in (hd, arg) end

(*create output-string for itm_*)

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

  | itm_out _ (Model.Syn c) = c

  | itm_out _ (Model.Typ c) = c

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

  | itm_out _ (Model.Sup (d, ts)) = term2str (Model.comp_dts (d, ts))

  | itm_out _ (Model.Mis (d, pid)) = term2str d ^ " " ^ term2str pid

  | itm_out _ _ = error "itm_out: uncovered definition"

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

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

fun itms2itemppc thy itms pre =

  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 Model.empty_ppc itms;

  in add_where gfr (map boolterm2item pre) end;

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

fun add_field (_: theory) pbt (d,ts) = 

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

  in case filter (eq d) pbt of

       [(fi, (_, _))] => (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                        *)

fun add_field' (_: theory) mpc ori =

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

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

      case filter (eq d) mpc of

	[(fi, (_, _))] => [(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) end;

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

   a plateau with length 1 is marked with 0         *)

fun mark _ [] = error "mark []"

  | mark eq xs =

    let

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

        | mar _ _ [] _ = error "mark []"

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

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

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

  | coll_variants _ = error "coll_variants: called with []";

fun replace_0 vm [0] = intsto vm

  | replace_0 _ vs = vs;

fun add_id [] = error "add_id []"

  | add_id xs =

    let

      fun add _ [] = []

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

    in add 1 xs end;

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

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

  | prep_ori fmz thy pbt =

    let

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

      val ori = map (add_field thy pbt o Model.split_dts o the o TermC.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;

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

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

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

(* pblID are reverted _on calling_ the retrieve-funs *)

type pblRD = (*e.g. ["equations","univariate","normalise"] for internal retrieval *)

  pblID;     (*e.g. ["normalise","univariate","equations"] presented to student   *)

(* apply a fun to a ptyps node *)

fun app_ptyp x = app_py (get_ptyps ()) x;

(* TODO: generalize search for subthy *)

fun get_pbt (pblID: pblID) = get_py (get_ptyps ()) pblID (rev pblID)

(* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)

fun get_met (metID : metID) = get_py (get_mets ()) metID metID;

fun get_met' thy (metID : metID) = get_py (KEStore_Elems.get_mets thy) metID metID;

fun get_the (theID : theID) = get_py (get_thes ()) theID theID;

(* lookup a guh in hierarchy of problems / methods depending on fst 4 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, [{guh, ...} : pbt], ns)) =

	        if gu = guh then SOME ((ids @ [id]) : kestoreID) else nodes (ids @ [id]) gu ns

	        | node _ _ _ = error "guh2kestoreID node: uncovered fun def."

	      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 (get_ptyps ()) of

	      SOME id => rev id

	    | NONE => error ("guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in ptyps")

      end

  | "met_" =>

	    let

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

	        if gu = guh then SOME ((ids @ [id]) : kestoreID) else nodes (ids @ [id]) gu ns

	        | node _ _ _ = error "guh2kestoreID node: uncovered fun def."

	      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 (get_mets ()) of

	      SOME id => id

	    | NONE => error ("guh2kestoreID: \"" ^ guh ^ "\" " ^ "not found in mets")

      end

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

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

    let

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

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

      val gi = (case gi of

		    [] => []

		  | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.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 = map (pair "#Given") gi;

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

		  val fi = (case fi of

		    [] => []

		  | ((_, fi') :: []) => (map (split_did o Thm.term_of o the o (TermC.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 Thm.term_of o the o (TermC.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 (TermC.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 ((Thm.term_of o the o (TermC.parse thy)) s),

			  prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID): pbt * pblID

    end;

(* prepare met for storage analogous to pbt *)

fun prep_met thy guh maa init

	    (metID, ppc: (string * string list) list,

        {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,

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

    let

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

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

      val gi = (case gi of

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

		  | ((_, gi') :: []) => (map (split_did o Thm.term_of o the o (TermC.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 Thm.term_of o the o (TermC.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 Thm.term_of o the o (TermC.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 (TermC.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 = ((TermC.inst_abs o Thm.term_of o the o (TermC.parse thy)) scr)

		  val calc = if scr = "empty_script" then [] else LTool.get_calcs thy sc

    in

      ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,

         erls = rls, srls = srls, prls = prls, calc = calc,

         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 [])) (get_ptyps ()); (* for tests *)

fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)

(* transform oris *)

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

fun filter_vat oris i = filter ((member_swap op = i) o (#2 : Model.ori -> int list)) oris;

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

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

fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", Model.Sup (d, ts));

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

fun field_eq f (_, _, f', _, _) = 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_ (_: theory) pbt (i, vats, b, f, Model.Cor ((d, vs), _)) =

    (case find_first (eq1 d) pbt of 

      SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))

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

  | chk_ _ pbt (i, vats, b, f, Model.Inc ((d, vs), _)) =

    (case find_first (eq1 d) pbt of 

      SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))

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

  | chk_ _ _ (itm as (_, _, _, _, Model.Syn _)) = itm

  | chk_ _ _ (itm as (_, _, _, _, Model.Typ _)) = itm

  | chk_ _ pbt (i, vats, b, f, Model.Sup (d, vs)) =

    (case find_first (eq1 d) pbt of 

      SOME (_, (_, id)) => (i, vats, b, f, Model.Cor ((d,vs), (id, Model.pbl_ids' d vs)))

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

  | chk_ _ pbt (i, vats, _, f, Model.Mis (d, vs)) =

    (case find_first (eq1 d) pbt of

      SOME (_, _) => error "chk_: ((i,vats,b,f,Model.Cor ((d,vs),(id, Model.pbl_ids' d vs))):itm)"

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

  | chk_ _ _ _ = error "chk_: uncovered fun def.";

fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = Model.d_in itm_;

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

fun eq0 (0, _, _, _, _) = 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_) :: its) =

    add_idvat (itms @ [(i,[],b,f,itm_)]) (i + 1) mvat its;

                       (* ^^ mvat ...meaningless with pbl-identifier *)

(* find elements of pbt not contained in itms;

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

fun chk_m itms 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, Model.Mis (d, id))]);

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 Model.max_vt for concluding completeness (could be another!) *)

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 = Model.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' = Stool.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 Model.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                                           *)

fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =

  let 

 (*0*)val mv = Model.max_vt pbl;

      fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = Model.d_in itm_;

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

				SOME _ => false | NONE => true;

 (*1*)val mis = (filter (notmem pbl)) pbt;

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

      fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, Model.Mis (d, pid));

 (*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, _, _, _) = member op = vats mv;

      val newitms = filter mem_vat news;

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

      val pre' = Stool.check_preconds' prls pre itms' mv;

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

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

(** 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_ (_: theory) pbt (i, vats, f, d, vs) =

  case find_first (eq1 d) pbt of 

	  SOME (_, (_, id)) => [(i, vats, true, f, Model.Cor ((d, vs), (id, Model.pbl_ids' d vs)))]

  | NONE => [];

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

fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;

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

  case find_first (eq2' p) oris of

	  SOME _ => []

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

fun pair0vatsfalse (f, itm_) = (0, [], false, f, 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 Model.max_vt for concluding completeness (FIXME could be another!) *)

fun match_oris thy prls oris (pbt,pre) = 

  let

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

    val mvat = Model.max_vt itms;

    val complete = chk1_mis mvat itms pbt;

    val pre' = Stool.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) =

  let

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

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

    val mvat = Model.max_vt itms;

    val miss = chk1_mis' oris ppc;

    val pre' = Stool.check_preconds' prls pre itms mvat;

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

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

datatype match' = (* for the user *)

  Matches' of Model.item Model.ppc

| NoMatch' of Model.item Model.ppc;

(* match a formalization with a problem type, for tests *)

fun match_pbl 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;

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

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

  | refin _ _ _ = error "refin: uncovered fun def."

and refins _ _ [] = NONE

  | refins pblRD ori ((p as Ptyp _) :: 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;

      (* WN020803: itms!: oris might _not_ be complete here *)

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

    in

      if b

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

      else pbls @ [Stool.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;

      (* WN020803: itms!: oris might _not_ be complete here *)

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

    in

      if b 

      then

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

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

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

    end

  | refin' _ _ _ _ = error "refin': uncovered fun def."

and refins' _ _ pbls [] = pbls

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

    let

      val pbls' = refin' pblRD fmz pbls p

    in

      case last_elem pbls' of

        Stool.Matches _ => pbls'

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

    end;

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

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

    let

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

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

    in

      if b

      then pbls @ [Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))]

      else pbls @ [Stool.NoMatch_] 

    end

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

    let

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

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

    in if b 

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

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

       else (pbls @ [Stool.NoMatch_])

    end

  | refin'' _ _ _ _ _ = error "refin': uncovered fun def."

and refins'' _ _ _ pbls [] = pbls

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

    let

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

    in case last_elem pbls' of

      Stool.Match_ _ => pbls'

    | Stool.NoMatch_ => refins'' thy pblRD itms pbls' pts

  end;

(* for tactic Refine_Tacitly

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

fun refine_ori oris (pblID: pblID) =

  let

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

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

fun refine_pbl thy (pblID: pblID) itms =

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

	  NONE => NONE

  | SOME (Stool.Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd

  | _ => error "refine_pbl: uncovered case refined_";

(* for math-experts and test;

   FIXME.WN021019: needs thy for parsing fmz *)

fun refine fmz pblID =

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

(* 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 () = (* for tests *)

  (tracing o strs2str o (map linefeed)) (coll_pblguhs (get_ptyps ()))

fun sort_pblguhs () = (* for tests *)

  (tracing o strs2str o (map linefeed)) (((sort string_ord) o coll_pblguhs) (get_ptyps ()))

fun show_metguhs () = (* for tests *)

  (tracing o strs2str o (map linefeed)) (coll_metguhs (get_mets ()))

fun sort_metguhs () = (* for tests *)

  (tracing o strs2str o (map linefeed)) (((sort string_ord) o coll_metguhs) (get_mets ()))

end