(* Specify-phase: specifying and modeling a problem or a subproblem. The

    most important types are declared in mstools.sml.

    author: Walther Neuper

    991122

    (c) due to copyright terms

 use"ME/calchead.sml";

 use"calchead.sml";

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 (* TODO interne Funktionen aus sig entfernen *)

 signature CALC_HEAD =

   sig

     datatype additm = Add of SpecifyTools.itm | Err of string

     val all_dsc_in : SpecifyTools.itm_ list -> Term.term list

     val all_modspec : ptree * pos' -> ptree * pos'

     datatype appl = Appl of tac_ | Notappl of string

     val appl_add :

        theory ->

        string ->

        SpecifyTools.ori list ->

        SpecifyTools.itm list ->

        (string * (Term.term * Term.term)) list -> cterm' -> additm

     type calcstate

     type calcstate'

     val chk_vars : term ppc -> string * Term.term list

     val chktyp :

        theory -> int * term list * term list -> term

     val chktyps :

        theory -> term list * term list -> term list

     val complete_metitms :

    SpecifyTools.ori list ->

    SpecifyTools.itm list ->

    SpecifyTools.itm list -> pat list -> SpecifyTools.itm list

     val complete_mod_ : ori list * pat list * pat list * itm list ->

 			itm list * itm list

     val complete_mod : ptree * pos' -> ptree * (pos * pos_)

     val complete_spec : ptree * pos' -> ptree * pos'

     val cpy_nam :

        pat list -> preori list -> pat -> preori

     val e_calcstate : calcstate

     val e_calcstate' : calcstate'

     val eq1 : ''a -> 'b * (''a * 'c) -> bool

     val eq3 :

        ''a -> Term.term -> 'b * 'c * 'd * ''a * SpecifyTools.itm_ -> bool

     val eq4 : ''a -> 'b * ''a list * 'c * 'd * 'e -> bool

     val eq5 :

        'a * 'b * 'c * 'd * SpecifyTools.itm_ ->

        'e * 'f * 'g * Term.term * 'h -> bool

     val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool

     val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool

     val f_mout : theory -> mout -> Term.term

     val filter_outs :

        SpecifyTools.ori list ->

        SpecifyTools.itm list -> SpecifyTools.ori list

     val filter_pbt :

        SpecifyTools.ori list ->

        ('a * (Term.term * 'b)) list -> SpecifyTools.ori list

     val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a

     val foldr1 : ('a * 'a -> 'a) -> 'a list -> 'a

     val form : 'a -> ptree -> (string * ('a * pos_) * Term.term) list

     val formres : 'a -> ptree -> (string * ('a * pos_) * Term.term) list

     val gen_ins' : ('a * 'a -> bool) -> 'a * 'a list -> 'a list

     val get_formress :

        (string * (pos * pos_) * Term.term) list list ->

        pos -> ptree list -> (string * (pos * pos_) * Term.term) list

     val get_forms :

        (string * (pos * pos_) * Term.term) list list ->

        posel list -> ptree list -> (string * (pos * pos_) * Term.term) list

     val get_interval : pos' -> pos' -> int -> ptree -> (pos' * term) list

     val get_ocalhd : ptree * pos' -> ocalhd

     val get_spec_form : tac_ -> pos' -> ptree -> mout

     val geti_ct :

        theory ->

        SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'

     val getr_ct : theory -> SpecifyTools.ori -> string * cterm'

     val has_list_type : Term.term -> bool

     val header : pos_ -> pblID -> metID -> pblmet

     val insert_ppc :

        theory ->

        int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->

        SpecifyTools.itm list -> SpecifyTools.itm list

     val insert_ppc' :

        SpecifyTools.itm -> SpecifyTools.itm list -> SpecifyTools.itm list

     val is_complete_mod : ptree * pos' -> bool

     val is_complete_mod_ : SpecifyTools.itm list -> bool

     val is_complete_modspec : ptree * pos' -> bool

     val is_complete_spec : ptree * pos' -> bool

     val is_copy_named : 'a * ('b * Term.term) -> bool

     val is_copy_named_idstr : string -> bool

     val is_error : SpecifyTools.itm_ -> bool

     val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool

     val is_known :

        theory ->

        string ->

        SpecifyTools.ori list ->

        Term.term -> string * SpecifyTools.ori * Term.term list

     val is_list_type : Term.typ -> bool

     val is_notyet_input :

        theory ->

        SpecifyTools.itm list ->

        Term.term list ->

        SpecifyTools.ori ->

        ('a * (Term.term * Term.term)) list -> string * SpecifyTools.itm

     val is_parsed : SpecifyTools.itm_ -> bool

     val is_untouched : SpecifyTools.itm -> bool

     val matc :

        theory ->

        pat list ->

        Term.term list ->

        (int list * string * Term.term * Term.term list) list ->

        (int list * string * Term.term * Term.term list) list

     val match_ags :

        theory -> pat list -> Term.term list -> SpecifyTools.ori list

     val maxl : int list -> int

     val match_ags_msg : string list -> Term.term -> Term.term list -> unit

     val memI : ''a list -> ''a -> bool

     val mk_additem : string -> cterm' -> tac

     val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac

     val mtc :

        theory -> pat -> Term.term -> SpecifyTools.preori option

     val nxt_add :

        theory ->

        SpecifyTools.ori list ->

        (string * (Term.term * 'a)) list ->

        SpecifyTools.itm list -> (string * cterm') option

     val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_

     val nxt_spec :

        pos_ ->

        bool ->

        SpecifyTools.ori list ->

        spec ->

        SpecifyTools.itm list * SpecifyTools.itm list ->

        (string * (Term.term * 'a)) list * (string * (Term.term * 'b)) list ->

        spec -> pos_ * tac

     val nxt_specif : tac -> ptree * (int list * pos_) -> calcstate'

     val nxt_specif_additem :

        string -> cterm' -> ptree * (int list * pos_) -> calcstate'

     val nxt_specify_init_calc : fmz -> calcstate

     val ocalhd_complete :

        SpecifyTools.itm list ->

        (bool * Term.term) list -> domID * pblID * metID -> bool

     val ori2Coritm :

 	pat list -> ori -> itm

     val ori_2itm :

        'a ->

        SpecifyTools.itm_ ->

        Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm

     val overwrite_ppc :

        theory ->

        int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->

        SpecifyTools.itm list ->

        (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list

     val parse_ok : SpecifyTools.itm_ list -> bool

     val posform2str : pos' * ptform -> string

     val posforms2str : (pos' * ptform) list -> string

     val posterms2str : (pos' * term) list -> string (*tests only*)

     val ppc135list : 'a SpecifyTools.ppc -> 'a list

     val ppc2list : 'a SpecifyTools.ppc -> 'a list

     val pt_extract :

        ptree * (int list * pos_) ->

        ptform * tac option * Term.term list

     val pt_form : ppobj -> ptform

     val pt_model : ppobj -> pos_ -> ptform

     val reset_calchead : ptree * pos' -> ptree * pos'

     val seek_oridts :

        theory ->

        string ->

        Term.term * Term.term list ->

        (int * SpecifyTools.vats * string * Term.term * Term.term list) list

        -> string * SpecifyTools.ori * Term.term list

     val seek_orits :

        theory ->

        string ->

        Term.term list ->

        (int * SpecifyTools.vats * string * Term.term * Term.term list) list

        -> string * SpecifyTools.ori * Term.term list

     val seek_ppc :

        int -> SpecifyTools.itm list -> SpecifyTools.itm option

     val show_pt : ptree -> unit

     val some_spec : spec -> spec -> spec

     val specify :

        tac_ ->

        pos' ->

        cid ->

        ptree ->

        (posel list * pos_) * ((posel list * pos_) * istate) * mout * tac *

        safe * ptree

     val specify_additem :

        string ->

        cterm' * 'a ->

        int list * pos_ ->

        'b ->

        ptree ->

        (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree

     val tag_form : theory -> term * term -> term

     val test_types : theory -> Term.term * Term.term list -> string

     val typeless : Term.term -> Term.term

     val unbound_ppc : term SpecifyTools.ppc -> Term.term list

     val vals_of_oris : SpecifyTools.ori list -> Term.term list

     val variants_in : Term.term list -> int

     val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list

     val vars_of_pbl_' : ('a * ('b * Term.term)) list -> Term.term list

   end

 (*---------------------------------------------------------------------*)

 structure CalcHead (**): CALC_HEAD(**) =

 struct

 (*---------------------------------------------------------------------*)

 (* datatypes *)

 (*.the state wich is stored after each step of calculation; it contains

    the calc-state and a list of [tac,istate](="tacis") to be applied.

    the last_elem tacis is the first to apply to the calc-state and

    the (only) one shown to the front-end as the 'proposed tac'.

    the calc-state resulting from the application of tacis is not stored,

    because the tacis hold enought information for efficiently rebuilding

    this state just by "fun generate ".*)

 type calcstate = 

      (ptree * pos') *    (*the calc-state to which the tacis could be applied*)

      (taci list);        (*ev. several (hidden) steps; 

                            in REVERSE order: first tac_ to apply is last_elem*)

 val e_calcstate = ((EmptyPtree, e_pos'), [e_taci]):calcstate;

 (*the state used during one calculation within the mathengine; it contains

   a list of [tac,istate](="tacis") which generated the the calc-state;

   while this state's tacis are extended by each (internal) step,

   the calc-state is used for creating new nodes in the calc-tree

   (eg. applicable_in requires several particular nodes of the calc-tree)

   and then replaced by the the newly created;

   on leave of the mathengine the resuing calc-state is dropped anyway,

   because the tacis hold enought information for efficiently rebuilding

   this state just by "fun generate ".*)

 type calcstate' = 

      taci list *        (*cas. several (hidden) steps; 

                           in REVERSE order: first tac_ to apply is last_elem*)

      pos' list *        (*a "continuous" sequence of pos',

 			 deleted by application of taci list*)     

      (ptree * pos');    (*the calc-state resulting from the application of tacis*)

 val e_calcstate' = ([e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';

 (*FIXXXME.WN020430 intermediate hack for fun ass_up*)

 fun f_mout thy (Form' (FormKF (_,_,_,_,f))) = (term_of o the o (parse thy)) f

   | f_mout thy _ = raise error "f_mout: not called with formula";

 (*.is the calchead complete ?.*)

 fun ocalhd_complete (its: itm list) (pre: (bool * term) list) (dI,pI,mI) = 

     foldl and_ (true, map #3 its) andalso 

     foldl and_ (true, map #1 pre) andalso 

     dI<>e_domID andalso pI<>e_pblID andalso mI<>e_metID;

 (* make a term 'typeless' for comparing with another 'typeless' term;

    'type-less' usually is illtyped                                  *)

 fun typeless (Const(s,_)) = (Const(s,e_type)) 

   | typeless (Free(s,_)) = (Free(s,e_type))

   | typeless (Var(n,_)) = (Var(n,e_type))

   | typeless (Bound i) = (Bound i)

   | typeless (Abs(s,_,t)) = Abs(s,e_type, typeless t)

   | typeless (t1 $ t2) = (typeless t1) $ (typeless t2);

 (*

 > val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";

 > val (_,t1) = split_dsc_t hs (term_of ct);

 > val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";

 > val (_,t2) = split_dsc_t hs (term_of ct);

 > typeless t1 = typeless t2;

 val it = true : bool

 *)

 (*.to an input (d,ts) find the according ori and insert the ts.*)

 (*WN.11.03: + dont take first inter<>[]*)

 fun seek_oridts thy sel (d,ts) [] = 

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

    "' not found (typed)", (0,[],sel,d,ts):ori, [])

   (* val (id,vat,sel',d',ts')::oris = ori;

      val (id,vat,sel',d',ts') = ori;

      *)

   | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =

     if sel = sel' andalso d=d' andalso (inter op = ts ts') <> [] 

     then if sel = sel' 

 	 then ("", 

                (id,vat,sel,d, inter op = ts ts'):ori, 

                ts')

 	 else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts))) 

                ^ " not for " ^ sel, 

                e_ori_, 

                [])

     else seek_oridts thy sel (d,ts) oris;

 (*.to an input (_,ts) find the according ori and insert the ts.*)

 fun seek_orits thy sel ts [] = 

   ("'"^

    (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^

    "' not found (typed)", e_ori_, [])

   | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =

     if sel = sel' andalso (inter op = ts ts') <> [] 

       then if sel = sel' 

 	   then ("",

                  (id,vat,sel,d, inter op = ts ts'):ori, 

                  ts')

 	   else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)

                  ^ " not for "^sel, 

                  e_ori_, 

                  [])

     else seek_orits thy sel ts oris;

 (* false

 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;

 > seek_orits thy sel ts [(id,vat,sel',d,ts')];

 uncaught exception TYPE

 > seek_orits thy sel ts [];

 uncaught exception TYPE

 *)

 (*find_first item with #1 equal to id*)

 fun seek_ppc id [] = NONE

   | seek_ppc id (p::(ppc:itm list)) =

     if id = #1 p then SOME p else seek_ppc id ppc;

 (*---------------------------------------------(3) nach ptyps.sml 23.3.02*)

 datatype appl = Appl of tac_ | Notappl of string;

 fun ppc2list ({Given=gis,Where=whs,Find=fis,

 	       With=wis,Relate=res}: 'a ppc) =

   gis @ whs @ fis @ wis @ res;

 fun ppc135list ({Given=gis,Find=fis,Relate=res,...}: 'a ppc) =

   gis @ fis @ res;

 (* get the number of variants in a problem in 'original',

    assumes equal descriptions in immediate sequence    *)

 fun variants_in ts =

   let fun eq(x,y) = head_of x = head_of y;

     fun cnt eq [] y n = ([n],[])

       | cnt eq (x::xs) y n = if eq(x,y) then cnt eq xs y (n+1)

 			     else ([n], x::xs);

     fun coll eq  xs [] = xs

       | coll eq  xs (y::ys) = 

       let val (n,ys') = cnt eq (y::ys) y 0;

       in if ys' = [] then xs @ n else coll eq  (xs @ n) ys' end;

     val vts = subtract op = [1] (distinct (coll eq [] ts));

   in case vts of [] => 1 | [n] => n

       | _ => error "different variants in formalization" end;

 (*

 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;

 val it = ([3],[4,5,5,5,5,5]) : int list * int list

 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5];

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

 *)

 fun is_list_type (Type("List.list",_)) = true

   | is_list_type _ = false;

 (* fun destr (Type(str,sort)) = (str,sort);

 > val (SOME ct) = parse thy "lll::real list";

 > val ty = (#T o rep_cterm) ct;

 > is_list_type ty;

 val it = true : bool 

 > destr ty;

 val it = ("List.list",["RealDef.real"]) : string * typ list

 > atomty ((#t o rep_cterm) ct);

 *** -------------

 *** Free ( lll, real list)

 val it = () : unit

 > val (SOME ct) = parse thy "[lll::real]";

 > val ty = (#T o rep_cterm) ct;

 > is_list_type ty;

 val it = true : bool 

 > destr ty;

 val it = ("List.list",["'a"]) : string * typ list

 > atomty ((#t o rep_cterm) ct);

 *** -------------

 *** Const ( List.list.Cons, [real, real list] => real list)

 ***   Free ( lll, real)

 ***   Const ( List.list.Nil, real list) 

 > val (SOME ct) = parse thy "lll";

 > val ty = (#T o rep_cterm) ct;

 > is_list_type ty;

 val it = false : bool  *)

 fun has_list_type (Free(_,T)) = is_list_type T

   | has_list_type _ = false;

 (*

 > val (SOME ct) = parse thy "lll::real list";

 > has_list_type (term_of ct);

 val it = true : bool

 > val (SOME ct) = parse thy "[lll::real]";

 > has_list_type (term_of ct);

 val it = false : bool *)

 fun is_parsed (Syn _) = false

   | is_parsed _ = true;

 fun parse_ok its = foldl and_ (true, map is_parsed its);

 fun all_dsc_in itm_s =

   let    

     fun d_in (Cor ((d,_),_)) = [d]

       | d_in (Syn c) = []

       | d_in (Typ c) = []

       | d_in (Inc ((d,_),_)) = [d]

       | d_in (Sup (d,_)) = [d]

       | d_in (Mis (d,_)) = [d];

   in (flat o (map d_in)) itm_s end;  

 (* 30.1.00 ---

 fun is_Syn (Syn _) = true

   | is_Syn (Typ _) = true

   | is_Syn _ = false;

  --- *)

 fun is_error (Cor (_,ts)) = false

   | is_error (Sup (_,ts)) = false

   | is_error (Inc (_,ts)) = false

   | is_error (Mis (_,ts)) = false

   | is_error _ = true;

 (* 30.1.00 ---

 fun ct_in (Syn (c)) = c

   | ct_in (Typ (c)) = c

   | ct_in _ = raise error "ct_in called for Cor .. Sup";

  --- *)

 (*#############################################################*)

 (*#############################################################*)

 (* vvv--- aus nnewcode.sml am 30.1.00 ---vvv *)

 (* testdaten besorgen:

    use"test-coil-kernel.sml";

    val (PblObj{origin=(oris,_,_),meth={ppc=itms,...},...}) = 

         get_obj I pt p;

   *)

 (* given oris, ppc, 

    variant V: oris union ppc => int, id ID: oris union ppc => int

    ppc is_complete == 

      EX vt:V. ALL r:oris --> EX i:ppc. ID r = ID i  &  complete i

    and

      @vt = max sum(i : ppc) V i

 *)

 (*

 > ((vts_cnt (vts_in itms))) itms;

 ---^^--test 10.3.

 > val vts = vts_in itms;

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

 > val nvts = vts_cnt vts itms;

 val nvts = [(1,6),(2,5),(3,7)] : (int * int) list

 > val mx = max2 nvts;

 val mx = (3,7) : int * int

 > val v = max_vt itms;

 val v = 3 : int

 --------------------------

 > 

 *)

 (*.get the first term in ts from ori.*)

 (* val (_,_,fd,d,ts) = hd miss;

    *)

 fun getr_ct thy ((_,_,fd,d,ts):ori) =

   (fd, ((Syntax.string_of_term (thy2ctxt thy)) o 

         (comp_dts thy)) (d,[hd ts]):cterm');

 (* val t = comp_dts thy (d,[hd ts]);

    *)

 (* get a term from ori, notyet input in itm *)

 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =  

   (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy)) 

            (d, subtract op = (ts_in itm_) ts):cterm');

 (* test-maximum.sml fmy <> [], Init_Proof ...

    val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;

    val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";

    atomty d;

    atomty d';

    atomty (hd ts);

    atomty ts';

    cterm_of thy (d $ (hd ts));

    cterm_of thy (d' $ ts');

    comp_dts thy (d,ts);

    *)

 (* in FE dsc, not dat: this is in itms ...*)

 fun is_untouched ((_,_,false,_,Inc((_,[]),_)):itm) = true

   | is_untouched _ = false;

 (* select an item in oris, notyet input in itms 

    (precondition: in itms are only Cor, Sup, Inc) *)

 local infix mem;

 fun x mem [] = false

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

 in 

 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)

   let

     fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0; 

     fun is_elem itms (f,(d,t)) = 

       case find_first (test_d d) itms of 

 	SOME _ => true | NONE => false;

   in case filter_out (is_elem itms) pbt of

 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;

    *)

     (f,(d,_))::itms => 

       SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')

   | _ => NONE end

 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);

    *)

   | nxt_add thy oris pbt itms =

   let

     fun testr_vt v ori = (curry (op mem) v) (#2 (ori:ori))

       andalso (#3 ori) <>"#undef";

     fun testi_vt v itm = (curry (op mem) v) (#2 (itm:itm));

     fun test_id ids r = curry (op mem) (#1 (r:ori)) ids;

 (* val itm = hd icl; val (_,_,_,d,ts) = v6;

    *)

     fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = 

 	(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);

     fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false

       | false_and_not_Sup (i,v,false,f, _) = true

       | false_and_not_Sup  _ = false;

     val v = if itms = [] then 1 else max_vt itms;

     val vors = if v = 0 then oris else filter (testr_vt v) oris;(*oris..vat*)

     val vits = if v = 0 then itms (*because of dsc without dat*)

 	       else filter (testi_vt v) itms;                   (*itms..vat*)

     val icl = filter false_and_not_Sup vits; (* incomplete *)

   in if icl = [] 

      then case filter_out (test_id (map #1 vits)) vors of

 	      [] => NONE

 	    (* val miss = filter_out (test_id (map #1 vits)) vors;

 	       *)

 	    | miss => SOME (getr_ct thy (hd miss))

      else

 	 case find_first (test_subset (hd icl)) vors of

 	     (* val SOME ori = find_first (test_subset (hd icl)) vors;

 	      *)

 	     NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"

 	   | SOME ori => SOME (geti_ct thy ori (hd icl))

   end

 end;

 fun mk_delete thy "#Given"  itm_ = Del_Given   (itm_out thy itm_)

   | mk_delete thy "#Find"   itm_ = Del_Find    (itm_out thy itm_)

   | mk_delete thy "#Relate" itm_ = Del_Relation(itm_out thy itm_)

   | mk_delete thy str _ = 

   raise error ("mk_delete: called with field '"^str^"'");

 fun mk_additem "#Given" ct = Add_Given ct

   | mk_additem "#Find"  ct = Add_Find ct    

   | mk_additem "#Relate"ct = Add_Relation ct

   | mk_additem str _ = 

   raise error ("mk_additem: called with field '"^str^"'");

 (* find the next tac in specify (except nxt_model_pbl)

    4.00.: TODO: do not return a pos !!!

           (sind from DG comes the _OLD_ writepos)*)

 (* 

 > val (pbl,pbt,mpc) =(pbl',get_pbt cpI,(#ppc o get_met) cmI);

 > val (dI,pI,mI) = empty_spec;

 > nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))

   ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);

 at Init_Proof:

 > val met = [];val (pbt,mpc) = (get_pbt pI',(#ppc o get_met) mI');

 > val (dI,pI,mI) = empty_spec;

 > nxt_spec Pbl (oris:ori list) ((dI',pI',mI'):spec(*original*))

   ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec);

   *)

 (*. determine the next step of specification;

     not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))

 eg. in rootpbl 'no_met': 

 args:

   preok          predicates are _all_ ok, or problem matches completely

   oris           immediately from formalization 

   (dI',pI',mI')  specification coming from author/parent-problem

   (pbl,          item lists specified by user

    met)          -"-, tacitly completed by copy_probl

   (dI,pI,mI)     specification explicitly done by the user

   (pbt, mpc)     problem type, guard of method

 .*)

 (* val (preok,pbl,pbt,mpc)=(pb,pbl',(#ppc o get_pbt) cpI,(#ppc o get_met) cmI);

    val (preok,pbl,pbt,mpc)=(pb,pbl',ppc,(#ppc o get_met) cmI);

    val (Pbl, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =

        (p_, pb, oris, (dI',pI',mI'), (probl,meth), 

 	(ppc, (#ppc o get_met) cmI), (dI,pI,mI));

    *)

 fun nxt_spec Pbl preok (oris:ori list) ((dI',pI',mI'):spec)

   ((pbl:itm list), (met:itm list)) (pbt,mpc) ((dI,pI,mI):spec) = 

   ((*writeln"### nxt_spec Pbl";*)

    if dI'=e_domID andalso dI=e_domID then (Pbl, Specify_Theory dI')

    else if pI'=e_pblID andalso pI=e_pblID then (Pbl, Specify_Problem pI')

 	else case find_first (is_error o #5) (pbl:itm list) of

 	  SOME (_,_,_,fd,itm_) => 

 	      (Pbl, mk_delete 

 	       (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)

 	| NONE => 

 	    ((*writeln"### nxt_spec is_error NONE";*)

 	     case nxt_add (assoc_thy (if dI=e_domID then dI' else dI)) 

 		 oris pbt pbl of

 (* val SOME (fd,ct') = nxt_add (assoc_thy (if dI=e_domID then dI' else dI)) 

                        oris pbt pbl;

   *)

 	       SOME (fd,ct') => ((*writeln"### nxt_spec nxt_add SOME";*)

 				 (Pbl, mk_additem fd ct'))

 	     | NONE => (*pbl-items complete*)

 	       if not preok then (Pbl, Refine_Problem pI')

 	       else

 		 if dI = e_domID then (Pbl, Specify_Theory dI')

 		 else if pI = e_pblID then (Pbl, Specify_Problem pI')

 		      else if mI = e_metID then (Pbl, Specify_Method mI')

 			   else

 			     case find_first (is_error o #5) met of

 			       SOME (_,_,_,fd,itm_) => 

 				   (Met, mk_delete (assoc_thy dI) fd itm_)

 			     | NONE => 

 				 (case nxt_add (assoc_thy dI) oris mpc met of

 				      SOME (fd,ct') => (*30.8.01: pre?!?*)

 				      (Met, mk_additem fd ct')

 				    | NONE => 

 				      ((*Solv 3.4.00*)Met, Apply_Method mI))))

 (* val preok=pb; val (pbl, met) = (pbl,met');

    val (pbt,mpc)=((#ppc o get_pbt) cpI,(#ppc o get_met) cmI);

    val (Met, preok, oris, (dI',pI',mI'), (pbl,met), (pbt,mpc), (dI,pI,mI)) =

        (p_, pb, oris, (dI',pI',mI'), (probl,meth), 

 	(ppc, (#ppc o get_met) cmI), (dI,pI,mI));

    *)

   | nxt_spec Met preok oris (dI',pI',mI') (pbl, met) (pbt,mpc) (dI,pI,mI) = 

   ((*writeln"### nxt_spec Met"; *)

    case find_first (is_error o #5) met of

      SOME (_,_,_,fd,itm_) => 

 	 (Met, mk_delete (assoc_thy (if dI=e_domID then dI' else dI)) fd itm_)

    | NONE => 

        case nxt_add (assoc_thy (if dI=e_domID then dI' else dI))oris mpc met of

 	 SOME (fd,ct') => (Met, mk_additem fd ct')

        | NONE => 

 	   ((*writeln"### nxt_spec Met: nxt_add NONE";*)

 	    if dI = e_domID then (Met, Specify_Theory dI')

 	    else if pI = e_pblID then (Met, Specify_Problem pI')

 		 else if not preok then (Met, Specify_Method mI)

 		      else (Met, Apply_Method mI)));

 (* di_ pI_ mI_ pos_

 val itms = [(1,[1],true,"#Find",Cor(e_term,[e_term])):itm,

 	    (2,[2],true,"#Find",Syn("empty"))];

 *)

 (* ^^^--- aus nnewcode.sml am 30.1.00 ---^^^ *)

 (*#############################################################*)

 (*#############################################################*)

 (* vvv--- aus nnewcode.sml vor 29.1.00 ---vvv *)

 (*3.3.--

 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) = 

   (id,vt,cl,sl,Cor (d,ts)):itm

   | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =   

   raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^

 	       " not not for Syn (s:cterm')")

   | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) = 

   raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^

 	       " not not for Typ (s:cterm')")

   | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =

   (id,vt,cl,sl,Fal (d,ts))

   | update_itm (cl,d,ts) (id,vt,_,sl,Inc (_,_)) =

   (id,vt,cl,sl,Inc (d,ts))

   | update_itm (cl,d,ts) (id,vt,_,sl,Sup (_,_)) =

   (id,vt,cl,sl,Sup (d,ts));

 *)

 fun is_field_correct sel d dscpbt =

   case assoc (dscpbt, sel) of

     NONE => false

   | SOME ds => member op = ds d;

 (*. update the itm_ already input, all..from ori .*)

 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');

    *)

 fun ori_2itm thy itm_ pid all ((id,vt,fd,d,ts):ori) = 

   let 

     val ts' = union op = (ts_in itm_) ts;

     val pval = pbl_ids' thy d ts'

 	(*WN.9.5.03: FIXXXME [#0, epsilon]

 	  here would upd_penv be called for [#0, epsilon] etc. *)

     val complete = if eq_set op = (ts', all) then true else false;

   in case itm_ of

     (Cor _) => 

 	(if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts')) 

 	 else (id,vt,complete,fd,Cor((d,ts'),(pid, pval)))):itm

   | (Syn c)     => raise error ("ori_2itm wants to overwrite "^c)

   | (Typ c)     => raise error ("ori_2itm wants to overwrite "^c)

   | (Inc _) => if complete

 	       then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))

 	       else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))

   | (Sup ((*_,_*)d,ts')) => (*4.9.01 lost env*)

 	 (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))

 	 (*else (id,vt,complete,fd,Cor((d,ts'),e))*)

 (* 28.1.00: not completely clear ---^^^ etc.*)

 (* 4.9.01: Mis just copied---vvv *)

   | (Mis _) => if complete

 		     then (id,vt,true ,fd, Cor ((d,ts'),(pid, pval)))

 		     else (id,vt,false,fd, Inc ((d,ts'),(pid, pval)))

   end;

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

 fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_); 

 (* 'all' ts from ori; ts is the input; (ori carries rest of info)

    9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?

    pval: value for problem-environment _NOT_ checked for 'inter' --

    -- FIXXME.WN.11.03 the generation of penv has to go to insert_ppc

   (as it has been done for input_icalhd+insert_ppc' in 11.03)*)

 (*. is_input ori itms <=> 

     EX itm. (1) ori(field,dsc) = itm(field,dsc) & (2..4)

             (2) ori(ts) subset itm(ts)        --- Err "already input"       

 	    (3) ori(ts) inter itm(ts) = empty --- new: ori(ts)

 	    (4) -"- <> empty                  --- new: ori(ts) \\ inter .*)

 (* val(itms,(i,v,f,d,ts)) = (ppc,ori');

    *)

 fun is_notyet_input thy (itms:itm list) all ((i,v,f,d,ts):ori) pbt =

   case find_first (eq1 d) pbt of

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

                             val SOME (_,_,_,_,itm_)=find_first (eq3 f d) itms;

 			   *)

       (case find_first (eq3 f d) itms of

 	   SOME (_,_,_,_,itm_) =>

 	   let 

 	       val ts' = inter op = (ts_in itm_) ts;

 	   in if subset op = (ts, ts') 

 	      then (((strs2str' o 

 		      map (Syntax.string_of_term (thy2ctxt thy))) ts')^

 		    " already input", e_itm)                            (*2*)

 	      else ("", 

                     ori_2itm thy itm_ pid all (i,v,f,d,

                                                subtract op = ts' ts))   (*3,4*)

 	   end

 	 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[]))) 

 				 pid all (i,v,f,d,ts))                  (*1*)

 	)

     | NONE => ("", ori_2itm thy (Sup (d,ts)) 

 			      e_term all (i,v,f,d,ts));

 fun test_types thy (d,ts) =

   let 

     val s = !show_types; val _ = show_types:= true;

     val opt = (try (comp_dts thy)) (d,ts);

     val msg = case opt of 

       SOME _ => "" 

     | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^

 	     ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)

 	     ^ " is illtyped");

     val _ = show_types:= s

   in msg end;

 fun maxl [] = raise error "maxl of []"

   | maxl (y::ys) =

   let fun mx x [] = x

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

   in mx y ys end;

 (*. is the input term t known in oris ? 

     give feedback on all(?) strange input;

     return _all_ terms already input to this item (e.g. valuesFor a,b) .*)

 (*WN.11.03: from lists*)

 fun is_known thy sel ori t =

 (* val (ori,t)=(oris,term_of ct);

    *)

   let

     val ots = (distinct o flat o (map #5)) (ori:ori list);

     val oids = ((map (fst o dest_Free)) o distinct o 

 		flat o (map vars)) ots;

     val (d,ts(*,pval*)) = split_dts thy t;

     val ids = map (fst o dest_Free) 

       ((distinct o (flat o (map vars))) ts);

   in if (subtract op = oids ids) <> []

      then (("identifiers "^(strs2str' (subtract op = oids ids))^

 	    " not in example"), e_ori_, [])

      else 

 	 if d = e_term 

 	 then 

 	     if not (subset op = (map typeless ts, map typeless ots))

 	     then (("terms '"^

 		    ((strs2str' o (map (Syntax.string_of_term 

 					    (thy2ctxt thy)))) ts)^

 		    "' not in example (typeless)"), e_ori_, [])

 	     else (case seek_orits thy sel ts ori of

 		       ("", ori_ as (_,_,_,d,ts), all) =>

 		       (case test_types thy (d,ts) of

 			    "" => ("", ori_, all)

 			  | msg => (msg, e_ori_, []))

 		     | (msg,_,_) => (msg, e_ori_, []))

 	 else 

 	     if member op = (map #4 ori) d

 	     then seek_oridts thy sel (d,ts) ori

 	     else ((Syntax.string_of_term (thy2ctxt thy) d)^

 		   (*" not in example", e_ori_, []) ///11.11.03*)

 		   " not in example", (0,[],sel,d,ts), [])

   end;

 (*. for return-value of appl_add .*)

 datatype additm =

 	 Add of itm

        | Err of string;    (*error-message*)

 (*. add an item; check wrt. oris and pbt .*)

 (* in contrary to oris<>[] below, this part handles user-input

    extremely acceptive, i.e. accept input instead error-msg *)

 fun appl_add thy sel ([]:ori list) ppc pbt ct' =

 (* val (ppc,pbt,ct',env) = (pbl, (#ppc o get_pbt) cpI, ct, []:envv);

    !!!! 28.8.01: env tested _minimally_ !!!

    *)

   let 

     val i = 1 + (if ppc=[] then 0 else maxl (map #1 ppc));

   in case parse thy ct' of (*should be done in applicable_in 4.00.FIXME*)

     NONE => Add (i,[],false,sel,Syn ct')

 (* val (SOME ct) = parse thy ct';

    *)

   | SOME ct =>

       let

 	val (d,ts(*,pval*)) = split_dts thy (term_of ct);

       in if d = e_term 

 	 then Add (i,[],false,sel,Mis (dsc_unknown,hd ts(*24.3.02*)))

 	 else  

 	   (case find_first (eq1 d) pbt of

 	     NONE => Add (i,[],true,sel,Sup ((d,ts)))

 	   | SOME (f,(_,id)) =>

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

    *)

 	       let

 		 fun eq2 d ((i,_,_,_,itm_):itm) = 

 		     (d = (d_in itm_)) andalso i<>0;

 	       in case find_first (eq2 d) ppc of 

 		 NONE => Add (i,[],true,f, Cor ((d,ts), (id, (*pval*)

 							 pbl_ids' thy d ts)))

 	       | SOME (i',_,_,_,itm_) => 

 (* val SOME (i',_,_,_,itm_) = find_first (eq2 d) ppc;

    val NONE = find_first (eq2 d) ppc;

    *)

 		   if is_list_dsc d

 		   then let val ts = union op = ts (ts_in itm_) 

 			in Add (if ts_in itm_ = [] then i else i',

 				 [],true,f,Cor ((d, ts), (id, (*pval*)

 							  pbl_ids' thy d ts)))

 			end

 		   else Add (i',[],true,f,Cor ((d,ts),(id, (*pval*)

 						       pbl_ids' thy d ts)))

 	       end

 	   )

       end

   end

 (*. add ct to ppc .*)

 (*FIXXME: accept items as Sup, Syn here, too (like appl_add..oris=[] above)*)

 (* val (ppc,pbt) = (pbl, ppc);

    val (ppc,pbt) = (met, (#ppc o get_met) cmI);

    val (ppc,pbt) = (pbl, (#ppc o get_pbt) cpI);

    *)

   | appl_add thy sel oris ppc pbt(*only for upd_envv*) ct = 

   let

     val ctopt = parse thy ct;

   in case ctopt of

     NONE => Err ("syntax error in "^ct)

   | SOME ct =>(* val SOME ct = ctopt;

 		 val (msg,ori',all) = is_known thy sel oris (term_of ct);

 		 val (msg,itm) = is_notyet_input thy ppc all ori' pbt;

 		*) 

     (case is_known thy sel oris (term_of ct) of

 	 ("",ori'(*ts='ct'*), all) => 

 	 (case is_notyet_input thy ppc all ori' pbt of

 	      ("",itm)  => Add itm

 	    | (msg,_) => Err msg)

        | (msg,_,_) => Err msg)

   end;

 (* 

 > val (msg,itm) = is_notyet_input thy ppc all ori';

 val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm

 > val itm_ = #5 itm;

 > val ts = ts_in itm_;

 > map (atomty) ts; 

 *)

 (*---------------------------------------------(4) nach ptyps.sml 23.3.02*)

 (** make oris from args of the stac SubProblem and from pbt **)

 (*.can this formal argument (of a model-pattern) be omitted in the arg-list

    of a SubProblem ? see ME/ptyps.sml 'type met '.*)

 fun is_copy_named_idstr str =

     case (rev o explode) str of

 	"_"::_::"_"::_ => true

       | _ => false;

 (*> is_copy_named_idstr "v_i_";

 val it = true : bool

   > is_copy_named_idstr "e_";

 val it = false : bool 

   > is_copy_named_idstr "L___";

 val it = true : bool

 *)

 (*.should this formal argument (of a model-pattern) create a new identifier?.*)

 fun is_copy_named_generating_idstr str =

     if is_copy_named_idstr str

     then case (rev o explode) str of

 	"_"::"_"::"_"::_ => false

       | _ => true

     else false;

 (*> is_copy_named_generating_idstr "v_i_";

 val it = true : bool

   > is_copy_named_generating_idstr "L___";

 val it = false : bool

 *)

 (*.can this formal argument (of a model-pattern) be omitted in the arg-list

    of a SubProblem ? see ME/ptyps.sml 'type met '.*)

 fun is_copy_named (_,(_,t)) = (is_copy_named_idstr o free2str) t;

 (*.should this formal argument (of a model-pattern) create a new identifier?.*)

 fun is_copy_named_generating (_,(_,t)) = 

     (is_copy_named_generating_idstr o free2str) t;

 (*.split type-wrapper from scr-arg and build part of an ori;

    an type-error is reported immediately, raises an exn, 

    subsequent handling of exn provides 2nd part of error message.*)

 (*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =   WN100820 made cterm to term 

     (* val (thy, (str, (dsc, _)), (ty $ var)) =

 	   (thy,  p,               a);

        *)

     (cterm_of thy (dsc $ var);(*type check*)

      SOME ((([1], str, dsc, (*[var]*)

 	    split_dts' (dsc, var))): preori)(*:ori without leading #*))

     handle e  as TYPE _ => 

 	   (writeln (dashs 70^"\n"

 		      ^"*** ERROR while creating the items for the model of the ->problem\n"

 		      ^"*** from the ->stac with ->typeconstructor in arglist:\n"

 		      ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"

 		      ^"*** description: "^(term_detail2str dsc)

 		      ^"*** value: "^(term_detail2str var)

 		      ^"*** typeconstructor in script: "^(term_detail2str ty)

 		      ^"*** checked by theory: "^(theory2str thy)^"\n"

 		      ^"*** "^dots 66);	     

 	     print_exn e; (*raises exn again*)

 	    NONE);*)

 fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =

     (* val (thy, (str, (dsc, _)), (ty $ var)) =

 	   (thy,  p,               a);

        *)

     (cterm_of thy (dsc $ var);(*type check*)

      SOME ((([1], str, dsc, (*[var]*)

 	    split_dts' (dsc, var))): preori)(*:ori without leading #*))

     handle e  as TYPE _ => 

 	   (writeln (dashs 70^"\n"

 		      ^"*** ERROR while creating the items for the model of the ->problem\n"

 		      ^"*** from the ->stac with ->typeconstructor in arglist:\n"

 		      ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"

 		      ^"*** description: "^(term_detail2str dsc)

 		      ^"*** value: "^(term_detail2str var)

 		      ^"*** typeconstructor in script: "^(term_detail2str ty)

 		      ^"*** checked by theory: "^(theory2str thy)^"\n"

 		      ^"*** "^dots 66);	     

 	    (*WN100820 postponed: print_exn e; raises exn again*)

 	    NONE);

 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];

 > val Const ("Script.SubProblem",_) $

 	  (Const ("Pair",_) $ Free (thy', _) $

 		 (Const ("Pair",_) $ pblID' $ metID')) $ ags =

     str2term"(SubProblem (SqRoot_,[univariate,equation],\

 	    \[SqRoot_,solve_linear]) [bool_ (x+1- 2=0), real_ x])::bool list";

 > val ags = isalist2list ags;

 > mtc thy (hd pbt) (hd ags);

 val it = SOME ([1],"#Given",Const (#,#),[# $ #]) *)

 (*.match each pat of the model-pattern with an actual argument;

    precondition: copy-named vars are filtered out.*)

 fun matc thy ([]:pat list)  _  (oris:preori list) = oris

   | matc thy pbt [] _ =

     (writeln (dashs 70);

      raise error ("actual arg(s) missing for '"^pats2str pbt

 		 ^"' i.e. should be 'copy-named' by '*_._'"))

   | matc thy ((p as (s,(d,t)))::pbt) (a::ags) oris =

     (* val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =

 	   (thy,  pbt',                    ags,     []);

        (*recursion..*)

        val (thy, ((p as (s,(d,t)))::pbt), (a::ags), oris) =

 	   (thy,  pbt,                     ags,    (oris @ [ori]));

        *)

     (*del?..*)if (is_copy_named_idstr o free2str) t then oris

     else(*..del?*) let val opt = mtc thy p a;  

 	 in case opt of

 		(* val SOME ori = mtc thy p a;

 		   *)

 		SOME ori => matc thy pbt ags (oris @ [ori])

 	      | NONE => [](*WN050903 skipped by exn handled in match_ags*)

 	 end; 

 (* run subp-rooteq.sml until Init_Proof before ...

 > val Nd (PblObj {origin=(oris,_,_),...},_) = pt;(*from test/subp-rooteq.sml*)

 > fun xxxfortest (_,a,b,c,d) = (a,b,c,d);val oris = map xxxfortest oris;

  other vars as in mtc ..

 > matc thy (drop_last pbt) ags [];

 val it = ([[1],"#Given",Const #,[#]),(0,[#],"#Given",Const #,[#])],2)*)

 (*WN051014 outcommented with redesign copy-named (for omitting '#Find'

   in SubProblem); 

   kept as initial idea for generating x_1, x_2, ... for equations*)

 fun cpy_nam (pbt:pat list) (oris:preori list) (p as (field,(dsc,t)):pat) =

 (* val ((pbt:pat list), (oris:preori list), ((field,(dsc,t)):pat)) =

        (pbt',            oris',             hd (*!!!!!*) cy);

    *)

   (if is_copy_named_generating p

    then (*WN051014 kept strange old code ...*)

        let fun sel (_,_,d,ts) = comp_ts (d, ts) 

 	   val cy' = (implode o drop_last o drop_last o explode o free2str) t

 	   val ext = (last_elem o drop_last o explode o free2str) t

 	   val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*)

 	   val vals = map sel oris

 	   val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext

        in ([1], field, dsc, [mk_free (type_of t) cy_ext]):preori end

    else ([1], field, dsc, [t])

 	)

   handle _ => raise error ("cpy_nam: for "^(term2str t));

 (*> val (field,(dsc,t)) = last_elem pbt;

 > cpy_nam pbt (drop_last oris) (field,(dsc,t));

 val it = ([1],"#Find",

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

    [Free ("x_i","bool List.list")])                             *)

 (*.match the actual arguments of a SubProblem with a model-pattern

    and create an ori list (in root-pbl created from formalization).

    expects ags:pats = 1:1, while copy-named are filtered out of pats;

    copy-named pats are appended in order to get them into the model-items.*)

 fun match_ags thy (pbt:pat list) ags =

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

    val (thy, pbt, ags) = (thy, pats, ags);

    *)

     let fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

 	val pbt' = filter_out is_copy_named pbt;

 	val cy = filter is_copy_named pbt;

 	val oris' = matc thy pbt' ags [];

 	val cy' = map (cpy_nam pbt' oris') cy;

 	val ors = add_id (oris' @ cy'); 

     (*appended in order to get ^^^^^ them into the model-items*)

     in (map flattup ors):ori list end;

 (*vars as above ..

 > match_ags thy pbt ags; 

 val it =

   [(1,[1],"#Given",Const ("Descript.equality","bool => Tools.una"),

     [Const # $ (# $ #) $ Free (#,#)]),

    (2,[1],"#Given",Const ("Descript.solveFor","RealDef.real => Tools.una"),

     [Free ("x","RealDef.real")]),

    (3,[1],"#Find",

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

     [Free ("x_i","bool List.list")])] : ori list*)

 (*.report part of the error-msg which is not available in match_args.*)

 fun match_ags_msg pI stac ags =

     let val s = !show_types

 	val _ = show_types:= true

 	val pats = (#ppc o get_pbt) pI

 	val msg = (dots 70^"\n"

 		 ^"*** problem "^strs2str pI^" has the ...\n"

 		 ^"*** model-pattern "^pats2str pats^"\n"

 		 ^"*** stac   '"^term2str stac^"' has the ...\n"

 		 ^"*** arg-list "^terms2str ags^"\n"

 		 ^dashs 70)

 	val _ = show_types:= s

     in writeln msg end;

 (*get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!!*)

 fun vars_of_pbl_ pbl_ = 

     let fun var_of_pbl_ (gfr,(dsc,t)) = t

     in ((map var_of_pbl_) o (filter_out is_copy_named)) pbl_ end;

 fun vars_of_pbl_' pbl_ = 

     let fun var_of_pbl_ (gfr,(dsc,t)) = t:term

     in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end;

 fun overwrite_ppc thy itm ppc =

   let 

     fun repl ppc' (_,_,_,_,itm_) [] =

       raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ 

                    " not found")

       | repl ppc' itm (p::ppc) =

 	if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc

 	else repl (ppc' @ [p]) itm ppc

   in repl [] itm ppc end;

 (*10.3.00: insert the already compiled itm into model;

    ev. filter_out  untouched (in FE: (0,...)) item related to insert-item *)

 (* val ppc=pbl;

    *)