(* the problems and methods as stored in hierarchies

    author Walther Neuper 1998, Mathias Lehnfeld

    (c) due to copyright terms

 *)

 signature MODEL_SPECIFY =

 sig

   val get_fun_ids : theory -> (string * typ) list

   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 * Rule.rls ->

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

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

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

   val refine_pbl : theory -> Celem.pblID -> Model.itm list ->

     (Celem.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 : Celem.pblID -> Celem.pbt

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

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

   val get_the : Celem.theID -> Celem.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 Celem.ptyp list -> string list list     (* for thy-hierarchy.sml *)

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

   val dsc_unknown : term

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

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

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

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

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

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

     string list * (string * string list) list * Rule.rls * string option * Celem.metID list ->

       Celem.pbt * Celem.pblID

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

      string list * (string * string list) list *

        {calc: 'a, crls: Rule.rls, errpats: Rule.errpat list, nrls: Rule.rls, prls: Rule.rls,

          rew_ord': Rule.rew_ord', rls': Rule.rls, srls: Rule.rls} * thm ->

      Celem.met * Celem.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_ -> Celem.pbt -> match'

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

   val e_errpat : Rule.errpat

   val show_pblguhs : unit -> unit

   val sort_pblguhs : unit -> unit

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

   val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b

   val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list

   val coll_variants: ('a * ''b) list -> ('a list * ''b) list

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

   val max: int list -> int

   val replace_0: int -> int list -> int list

 ( *\--- ! 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

 fun fun_id_of ({scr = prog, ...} : Celem.met) = 

   case prog of

     Rule.EmptyScr => NONE

   | Rule.Prog t => 

     (case t of

       Const ("HOL.eq", _) $ Free ("t", _) $ Free ("t", _) (*=@{thm refl}*) => NONE

     | _ => SOME (LTool.get_fun_id t))

   | Rule.Rfuns _ => NONE

 (* get all data from a Ptyp tree *)

 fun get_data ptyp =

 let

   fun scan [] = []

     | scan ((Celem.Ptyp ((_, data, []))) :: []) = data

     | scan ((Celem.Ptyp ((_, data, pl))) :: []) = data @ scan pl

     | scan ((Celem.Ptyp ((_, data, []))) :: ps) = data @ scan ps

     | scan ((Celem.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps

 in scan ptyp end

 fun get_fun_ids thy =

   let 

     val mets = get_data (KEStore_Elems.get_mets thy)

     (* all mets of the respective theory PLUS of all ancestor theories*)

     val fun_ids = mets |> map fun_id_of |> filter is_some |> map the

   in 

     filter (fn (str, _) => Celem.thyID_of_derivation_name str = Context.theory_name thy) fun_ids 

   end

 type field = string * (term * term)

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

 fun itm_2item (_: theory) (Model.Cor ((d, ts), _)) = Model.Correct (Rule.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 (Rule.term2str (Model.comp_dts (d, ts)))

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

   | itm_2item _ (Model.Mis (d, pid)) = Model.Missing (Rule.term2str d ^ " " ^ Rule.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 = " ^ Rule.term2str t)

   in (hd, arg) end

 (*create output-string for itm_*)

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

   | itm_out _ (Model.Syn c) = c

   | itm_out _ (Model.Typ c) = c

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

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

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

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

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

   | boolterm2item (false, term) = Model.False (Rule.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: " ^ Rule.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': " ^ Rule.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 [] _ _ = ([], ContextC.e_ctxt)

   | prep_ori fmz thy pbt =

     let

       val ctxt = ContextC.initialise' thy fmz;

       val ori = map (add_field thy pbt o Model.split_dts 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}]): Rule.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 *)

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

 (* apply a fun to a ptyps node *)

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

 (* TODO: generalize search for subthy *)

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

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

 fun get_met metID = Celem.get_py (get_mets ()) metID metID;

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

 fun get_the theID = Celem.get_py (get_thes ()) theID theID;

 (* lookup a guh in hierarchy of problems / methods depending on fst 4 chars in guh *)

 fun guh2kestoreID guh =

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

 	  "pbl_" =>

 	    let

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

 	        if gu = guh then SOME (ids @ [id]) 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 (Celem.Ptyp (id, [{guh, ...}], ns)) =

 	        if gu = guh then SOME (ids @ [id]) 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, ev, ca, metIDs) =

     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)

     end;

 (* prepare met for storage analogous to pbt *)

 fun prep_met thy guh maa init

 	    (metID, ppc,

         {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 = LTool.prep_program scr

 		  val calc = if Thm.eq_thm (scr, @{thm refl}) 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 = Rule.Prog sc}, 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 ((Celem.Ptyp ((i, _, []))) :: []) = [id @ [i]]

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

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

   | scan id ((Celem.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 (or method) 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, ...} =

   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 (Celem.Ptyp (pI, [py], [])) =

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

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

     else NONE

   | refin pblRD ori (Celem.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 Celem.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 (Celem.Ptyp (pI, [py], [])) =

     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 (Celem.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 Celem.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 (Celem.Ptyp (pI, [py], [])) =

     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 (Celem.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 Celem.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 =

   let

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

     in case opt of 

       SOME pblRD =>

         let val pblID': Celem.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 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 = (((#guh o get_pbt) pblID)

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

 fun metID2guh metID = (((#guh o get_met) metID)

   handle _ => error ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\""));

 fun kestoreID2guh Celem.Pbl_ kestoreID = pblID2guh kestoreID

   | kestoreID2guh Celem.Met_ kestoreID = metID2guh kestoreID

   | kestoreID2guh ketype kestoreID =

     error ("kestoreID2guh: \"" ^ Celem.ketype2str ketype ^ "\" not for \"" ^ strs2str' kestoreID ^ "\"");

 fun show_pblguhs () = (* for tests *)

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

 fun sort_pblguhs () = (* for tests *)

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

 fun show_metguhs () = (* for tests *)

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

 fun sort_metguhs () = (* for tests *)

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

 end