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

            most important types are declared in mstools.sml.

    Author: Walther Neuper 991122, Mathias Lehnfeld

    (c) due to copyright terms

 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 :

        Proof.context ->

        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 :

        Proof.context ->

        string ->

        SpecifyTools.ori list ->

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

     val is_list_type : Term.typ -> bool

     val is_notyet_input :

        Proof.context ->

        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 oris2fmz_vals : ori list -> string list * term 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 :

        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 :

        Proof.context ->

        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 :

        Proof.context ->

        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 : Proof.context -> 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 next.

    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 enough 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))) = (Thm.term_of o the o (parse thy)) f

   | f_mout thy _ = 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;

 (*["BOOL (1+x=2)","REAL x"] --match_ags--> oris 

   --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*)

 fun oris2fmz_vals oris =

     let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) = 

 	    ((term2str o comp_dts') (dsc, ts), last_elem ts) 

 	    handle _ => error ("ori2fmz_env called with "^terms2str ts)

     in (split_list o (map ori2fmz_vals)) oris end;

 (* 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 (Thm.term_of ct);

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

 > val (_,t2) = split_dsc_t hs (Thm.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 ctxt sel (d,ts) [] =

     ("seek_oridts: input ('" ^

         (term_to_string' ctxt (comp_dts (d,ts))) ^ "') not found in oris (typed)",

       (0, [], sel, d, ts),

       [])

   | seek_oridts ctxt sel (d,ts) ((id, vat, sel', d', ts')::oris) =

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

       ("", (id, vat, sel, d, inter op = ts ts'), ts') else

       seek_oridts ctxt sel (d, ts) oris;

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

 fun seek_orits ctxt sel ts [] = 

     ("seek_orits: input (_, '" ^ strs2str (map (term_to_string' ctxt) ts) ^

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

   | seek_orits ctxt 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 (term_to_string' ctxt)) ts) ^ " not for " ^ sel, e_ori_, [])

     else seek_orits ctxt 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;

 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 (Thm.term_of ct);

 val it = true : bool

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

 > has_list_type (Thm.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 _ = 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, ((term_to_string''' thy) o comp_dts) (d,[hd ts]) : cterm');

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

    *)

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

    the term from ori is thrown back to a string in order to reuse

    machinery for immediate input by the user. *)

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

   (fd, ((term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm')

 (* 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, ((term_to_string''' thy) o comp_dts) (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;

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

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

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

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

 *)

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

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

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

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

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

 		            oris pbt pbl of

 	           SOME (fd,ct') => ((*tracing"### 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))))

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

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

 	   ((*tracing"### 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"))];

 *)

 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 itm_ pid all ((id,vt,fd,d,ts):ori) = 

   let 

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

     val pval = pbl_ids' 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)     => error ("ori_2itm wants to overwrite "^c)

   | (Typ c)     => 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 ctxt (itms:itm list) all ((i,v,f,d,ts):ori) pbt =

   case find_first (eq1 d) pbt of

     SOME (_,(_,pid)) =>

       (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 (term_to_string' ctxt)) ts') ^ " already input", e_itm)(*2*)

 	            else ("", ori_2itm itm_ pid all (i,v,f,d, subtract op = ts' ts))             (*3,4*)

 	          end

 	    | NONE => ("", ori_2itm (Inc ((e_term,[]),(pid,[]))) pid all (i,v,f,d,ts)))            (*1*)

   | NONE => ("", ori_2itm (Sup (d,ts)) e_term all (i,v,f,d,ts));

 fun test_types ctxt (d,ts) =

   let 

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

     val msg = case opt of 

       SOME _ => "" 

     | NONE => (term_to_string' ctxt d ^ " " ^

 	       (strs2str' o map (term_to_string' ctxt)) ts ^ " is illtyped");

   in msg end;

 fun maxl [] = 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) .*)

 fun is_known ctxt sel ori t =

   let

     val _ = tracing ("RM is_known: t=" ^ term2str t);

     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) = split_dts 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 (term_to_string' ctxt))) ts ^

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

 	       else 

            (case seek_orits ctxt sel ts ori of

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

 		             (case test_types ctxt (d,ts) of

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

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

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

 	     else 

 	       if member op = (map #4 ori) d

 	       then seek_oridts ctxt sel (d,ts) ori

 	       else (term_to_string' ctxt d ^ " 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 to the model; 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 ctxt sel [] ppc pbt ct =

       let

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

         in 

           case parseNEW ctxt ct of

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

           | SOME t =>

               let val (d, ts) = split_dts t;

               in 

                 if d = e_term 

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

                 else

                   (case find_first (eq1 d) pbt of

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

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

                        let fun eq2 d (i, _, _, _, 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, pbl_ids' d ts)))

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

                               if is_list_dsc d 

                               then 

                                 let

                                   val in_itm = ts_in itm_;

                                   val ts' = union op = ts in_itm;

                                   val i'' = if in_itm = [] then i else i';

                                 in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end

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

                        end)

               end

       end

   | appl_add ctxt sel oris ppc pbt str =

       case parseNEW ctxt str of

         NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")

       | SOME t => 

           case is_known ctxt sel oris t of

             ("", ori', all) => 

               (case is_notyet_input ctxt ppc all ori' pbt of

                  ("", itm) => Add itm

                | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))

           | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);

 (** 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 calcelems.sml 'type met ' *)

 fun is_copy_named_idstr str =

     case (rev o Symbol.explode) str of

 	"'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode)) 

                                   "is_copy_named_idstr: " ^ str ^ " T"); true)

       | _ => (tracing ((strs2str o (rev o Symbol.explode)) 

                                   "is_copy_named_idstr: " ^ str ^ " F"); false);

 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_idstr str =

     if is_copy_named_idstr str

     then case (rev o Symbol.explode) str of

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

       | _ => true

     else false;

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

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

 	   (thy,  p,               a);

        *)

     (Thm.global_cterm_of thy (dsc $ var);(*type check*)

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

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

     handle e as TYPE _ => 

 	   (tracing (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);

 	    (*OldGoals.print_exn e; raises exn again*)

             writeln (PolyML.makestring e);

             reraise e;

 	(*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)

 	NONE);

 (*.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 [] _ =

     (tracing (dashs 70);

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

 (* generate a new variable "x_i" name from a related given one "x"

    by use of oris relating "v_i_" (is_copy_named!) to "v_"

    e.g. (v_, x) & (v_i_, ?) --> (v_i_, x_i) *)

 (* generate a new variable "x_i" name from a related given one "x"

    by use of oris relating "v_v'i'" (is_copy_named!) to "v_v"

    e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),

    but leave is_copy_named_generating as is, e.t. ss''' *)

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

   (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_n 3) o Symbol.explode o free2str) t

 	   val ext = (last_elem o drop_last o Symbol.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 _ => error ("cpy_nam: for "^(term2str t));

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

    if no 1:1 the exn raised by matc/mtc and handled at call.

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

 fun match_ags thy (pbt:pat list) 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 ^^^^^ into the model-items*)

     in (map flattup ors):ori list end;

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

 	(*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)

 	(*val _ = show_types:= s*)

     in tracing 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_) [] =

       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;

    *)

 fun insert_ppc thy itm ppc =

     let 

 	fun eq_untouched d ((0,_,_,_,itm_):itm) = (d = d_in itm_)

 	  | eq_untouched _ _ = false;

 	    val ppc' = 

 		(

 		 (*tracing("### insert_ppc: itm= "^(itm2str_ itm));*)       

 		 case seek_ppc (#1 itm) ppc of

 		     (* val SOME xxx = seek_ppc (#1 itm) ppc;

 		        *)

 		     SOME _ => (*itm updated in is_notyet_input WN.11.03*)

 		     overwrite_ppc thy itm ppc

 		   | NONE => (ppc @ [itm]));

     in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end;

 (*from Isabelle/src/Pure/library.ML, _appends_ a new element*)

 fun gen_ins' eq (x, xs) = if gen_mem eq (x, xs) then xs else xs @ [x];

 fun eq_dsc ((_,_,_,_,itm_):itm, (_,_,_,_,iitm_):itm) = 

     (d_in itm_) = (d_in iitm_);

 (*insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,

     handles superfluous items carelessly*)

 fun insert_ppc' itm itms = gen_ins' eq_dsc (itm, itms);

 (* val eee = op=;

  > gen_ins' eee (4,[1,3,5,7]);

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

 (*. output the headline to a ppc .*)

 fun header p_ pI mI =

     case p_ of Pbl => Problem (if pI = e_pblID then [] else pI) 

 	     | Met => Method mI

 	     | pos => error ("header called with "^ pos_2str pos);

 fun specify_additem sel (ct,_) (p, Met) c pt = 

       let

         val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),

   		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;

         val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

         val cpI = if pI = e_pblID then pI' else pI;

         val cmI = if mI = e_metID then mI' else mI;

         val {ppc,pre,prls,...} = get_met cmI;

       in 

         case appl_add ctxt sel oris met ppc ct of

           Add itm (*..union old input *) =>

   	        let

               val met' = insert_ppc thy itm met;

   	          val ((p, Met), _, _, pt') = 

   	            generate1 thy (case sel of

   				                       "#Given" => Add_Given'   (ct, met')

   			                       | "#Find"  => Add_Find'    (ct, met')

   			                       | "#Relate"=> Add_Relation'(ct, met')) 

   			        (Uistate, ctxt) (p, Met) pt

   	          val pre' = check_preconds thy prls pre met'

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

   	          val (p_, nxt) =

   	            nxt_spec Met pb oris (dI',pI',mI') (pbl,met') 

   	              ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);

   	        in ((p, p_), ((p, p_), Uistate),

   	          Form' (PpcKF (0,EdUndef,(length p),Nundef,

   			        (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')

             end

         | Err msg =>

   	        let

               val pre' = check_preconds thy prls pre met

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

   	          val (p_, nxt) =

   	            nxt_spec Met pb oris (dI',pI',mI') (pbl,met) 

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

   	        in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end

       end

   | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 

       let

         val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),

 		      probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;

         val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

         val cpI = if pI = e_pblID then pI' else pI;

         val cmI = if mI = e_metID then mI' else mI;

         val {ppc,where_,prls,...} = get_pbt cpI;

       in

         case appl_add ctxt sel oris pbl ppc ct of

           Add itm (*..union old input *) =>

 	          let

 	            val pbl' = insert_ppc thy itm pbl

 	            val ((p, Pbl), _, _, pt') = 

 	              generate1 thy (case sel of

 				                         "#Given" => Add_Given'   (ct, pbl')

 			                         | "#Find"  => Add_Find'    (ct, pbl')

 			                         | "#Relate"=> Add_Relation'(ct, pbl')) 

 			           (Uistate, ctxt) (p,Pbl) pt

 	            val pre = check_preconds thy prls where_ pbl'

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

 	            val (p_, nxt) =

 	              nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) 

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

 	            val ppc = if p_= Pbl then pbl' else met;

 	          in ((p,p_), ((p,p_),Uistate),

 	            Form' (PpcKF (0,EdUndef,(length p),Nundef,

 			          (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')

             end

         | Err msg =>

 	          let

               val pre = check_preconds thy prls where_ pbl

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

 	            val (p_, nxt) =

 	              nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) 

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

 	          in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end

       end;

 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= 

     let          (* either """"""""""""""" all empty or complete *)

       val thy = assoc_thy dI';

       val (oris, ctxt) = 

         if dI' = e_domID orelse pI' = e_pblID  (*andalso? WN110511*)

         then ([], e_ctxt)

   	    else pI' |> #ppc o get_pbt |> prep_ori fmz thy

       val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))

   			(oris, (dI',pI',mI'), e_term)

       val pt = update_ctxt pt [] ctxt

       val {ppc, prls, where_, ...} = get_pbt pI'

       val (pbl, pre, pb) = ([], [], false)

     in 

       case mI' of

   	    ["no_met"] => 

   	      (([], Pbl), (([], Pbl), Uistate),

   	        Form' (PpcKF (0, EdUndef, (length []), Nundef,

 			        (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),

   	        Refine_Tacitly pI', Safe, pt)

        | _ => 

   	      (([], Pbl), (([], Pbl), Uistate),

   	        Form' (PpcKF (0, EdUndef, (length []), Nundef,

   			      (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),

   	        Model_Problem, Safe, pt)

   end

     (*ONLY for STARTING modeling phase*)

   | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =

       let 

         val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_), ctxt, ...}) = get_obj I pt p

         val thy' = if dI = e_domID then dI' else dI

         val thy = assoc_thy thy'

         val {ppc,prls,where_,...} = get_pbt pI'

         val pre = check_preconds thy prls where_ pbl

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

         val ((p,_),_,_,pt) =

           generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt

         val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) 

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

       in ((p, Pbl), ((p, p_), Uistate), 

           Form' (PpcKF (0, EdUndef, length p, Nundef,

 		       (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),

           nxt, Safe, pt)

       end

     (*. called only if no_met is specified .*)     

   | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =

       let

         val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met, ctxt, ...}) = get_obj I pt p;

         val {prls,met,ppc,thy,where_,...} = get_pbt pIre

         val (domID, metID) = 

           (string_of_thy thy, if length met = 0 then e_metID else hd met)

         val ((p,_),_,_,pt) = 

 	        generate1 thy (Refine_Tacitly'(pI,pIre,domID,metID,(*pbl*)[])) 

 		        (Uistate, ctxt) pos pt

         val (pbl, pre, pb) = ([], [], false)

       in ((p, Pbl), (pos, Uistate),

         Form' (PpcKF (0,EdUndef,(length p),Nundef,

 		      (Problem pIre, itms2itemppc (assoc_thy dI') pbl pre))),

         Model_Problem, Safe, pt)

       end

   | specify (Refine_Problem' (rfd as (pI,_))) pos c pt =

       let

         val ctxt = get_ctxt pt pos

         val (pos,_,_,pt) =

           generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt

       in (pos(*p,Pbl*), (pos(*p,Pbl*),Uistate), Problems (RefinedKF rfd), 

 	      Model_Problem, Safe, pt)

       end

     (*WN110515 initialise ctxt again from itms and add preconds*)

   | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) c pt =

       let

         val (PblObj {origin=(oris,(dI',pI',mI'),_), spec=(dI,_,mI), 

 		      meth=met, ctxt, ...}) = get_obj I pt p;

         val thy = assoc_thy dI

         val ((p,Pbl),_,_,pt)= 

 	        generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt

         val dI'' = assoc_thy (if dI=e_domID then dI' else dI);

         val mI'' = if mI=e_metID then mI' else mI;

         val (_, nxt) =

           nxt_spec Pbl ok oris (dI',pI',mI') (itms, met) 

 		        ((#ppc o get_pbt) pI,(#ppc o get_met) mI'') (dI,pI,mI);

       in ((p,Pbl), (pos,Uistate),

         Form' (PpcKF (0,EdUndef,(length p),Nundef, (Problem pI, itms2itemppc dI'' itms pre))),

           nxt, Safe, pt)

       end    

     (*WN110515 initialise ctxt again from itms and add preconds*)

   | specify (Specify_Method' (mID,_,_)) (pos as (p,_)) c pt =

       let

         val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), 

 		      meth=met, ctxt, ...}) = get_obj I pt p;

         val {ppc,pre,prls,...} = get_met mID

         val thy = assoc_thy dI

         val oris = add_field' thy ppc oris;

         val dI'' = if dI=e_domID then dI' else dI;

         val pI'' = if pI = e_pblID then pI' else pI;

         val met = if met=[] then pbl else met;

         val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;

         val (pos, _, _, pt) = 

 	        generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt

         val (_,nxt) =

           nxt_spec Met (*ok*)true oris (dI',pI',mI') (pbl, itms) 

 		        ((#ppc o get_pbt) pI'',ppc) (dI'',pI'',mID);

       in (pos, (pos,Uistate),

         Form' (PpcKF (0,EdUndef,(length p),Nundef,

 		      (Method mID, itms2itemppc (assoc_thy dI'') itms pre'))),

            nxt, Safe, pt)

       end    

   | specify (Add_Given' ct) p c pt = specify_additem "#Given" ct p c pt

   | specify (Add_Find'  ct) p c pt = specify_additem "#Find"  ct p c pt

   | specify (Add_Relation' ct) p c pt=specify_additem"#Relate"ct p c pt

   | specify (Specify_Theory' domID) (pos as (p,p_)) c pt =

       let

         val p_ = case p_ of Met => Met | _ => Pbl

         val thy = assoc_thy domID;

         val (PblObj{origin=(oris,(dI',pI',mI'),_), meth=met,

 		      probl=pbl, spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;

         val mppc = case p_ of Met => met | _ => pbl;

         val cpI = if pI = e_pblID then pI' else pI;

         val {prls=per,ppc,where_=pwh,...} = get_pbt cpI

         val cmI = if mI = e_metID then mI' else mI;

         val {prls=mer,ppc=mpc,pre=mwh,...} = get_met cmI

         val pre = 

 	        case p_ of

 	          Met => (check_preconds thy mer mwh met)

 	        | _ => (check_preconds thy per pwh pbl)

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

       in

         if domID = dI

         then

           let val (p_,nxt) = nxt_spec p_ pb oris (dI',pI',mI') 

 				    (pbl,met) (ppc,mpc) (dI,pI,mI);

 	        in ((p,p_), (pos,Uistate), 

 		        Form'(PpcKF (0,EdUndef,(length p), Nundef,

 			        (header p_ pI cmI, itms2itemppc thy mppc pre))),

 		        nxt,Safe,pt)

           end

         else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)

 	        let 

 	          val ((p,p_),_,_,pt) =

               generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt

 	          val (p_,nxt) =

               nxt_spec p_ pb oris (dI',pI',mI') (pbl,met) (ppc,mpc) (domID,pI,mI);

 	        in ((p,p_), (pos,Uistate), 

 	          Form' (PpcKF (0, EdUndef, (length p),Nundef,

 			        (header p_ pI cmI, itms2itemppc thy mppc pre))),

 	          nxt, Safe,pt)

           end

       end

   | specify m' _ _ _ = 

       error ("specify: not impl. for " ^ tac_2str m');

 (*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}

   -- for input from scratch*)

 fun nxt_specif_additem sel ct (ptp as (pt, (p, Pbl))) = 

       let

         val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),

 		      probl=pbl,spec=(dI,pI,_), ctxt, ...}) = get_obj I pt p;

         val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

         val cpI = if pI = e_pblID then pI' else pI;

       in

         case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of

 	        Add itm (*..union old input *) =>

 	          let

 	            (*val _=tracing("###nxt_specif_additem: itm= "^(itm2str_ itm));*)

 	            val pbl' = insert_ppc thy itm pbl

 	            val (tac,tac_) = 

 		            case sel of

 		              "#Given" => (Add_Given    ct, Add_Given'   (ct, pbl'))

 		            | "#Find"  => (Add_Find     ct, Add_Find'    (ct, pbl'))

 		            | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))

 	            val ((p,Pbl),c,_,pt') = 

 		            generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt

 	          in ([(tac,tac_,((p,Pbl),(Uistate, ctxt)))], c, (pt',(p,Pbl))):calcstate' 

             end	       

 	      | Err msg => (*TODO.WN03 pass error-msgs to the frontend..

                        FIXME ..and dont abuse a tactic for that purpose*)

 	          ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),

 	            (e_pos', (e_istate, e_ctxt)))], [], ptp) 

       end

   | nxt_specif_additem sel ct (ptp as (pt,(p,Met))) = 

       let

         val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),

 		      probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;

         val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

         val cmI = if mI = e_metID then mI' else mI;

       in 

         case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of

           Add itm (*..union old input *) =>

 	          let

 	            val met' = insert_ppc thy itm met;

 	            val (tac,tac_) = 

 	              case sel of

 		              "#Given" => (Add_Given    ct, Add_Given'   (ct, met'))

 		            | "#Find"  => (Add_Find     ct, Add_Find'    (ct, met'))

 		            | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))

 	            val ((p,Met),c,_,pt') = 

 	              generate1 thy tac_ (Uistate, ctxt) (p,Met) pt

 	          in ([(tac,tac_,((p,Met), (Uistate, ctxt)))], c, (pt',(p,Met))) end

         | Err msg => ([(*tacis*)], [], ptp) 

           (*nxt_me collects tacis until not hide; here just no progress*)

       end;

 fun ori2Coritm pbt ((i,v,f,d,ts):ori) =

     (i,v,true,f, Cor ((d,ts),(((snd o snd o the o (find_first (eq1 d))) pbt) 

 			      handle _ => error ("ori2Coritm: dsc "^

 						term2str d^

 						"in ori, but not in pbt")

 			      ,ts))):itm;

 fun ori2Coritm (pbt:pat list) ((i,v,f,d,ts):ori) =

     ((i,v,true,f, Cor ((d,ts),((snd o snd o the o 

 			       (find_first (eq1 d))) pbt,ts))):itm)

     handle _ => (*dsc in oris, but not in pbl pat list: keep this dsc*)

     ((i,v,true,f, Cor ((d,ts),(d,ts))):itm);

 (*filter out oris which have same description in itms*)

 fun filter_outs oris [] = oris

   | filter_outs oris (i::itms) = 

     let val ors = filter_out ((curry op= ((d_in o #5) (i:itm))) o 

 			      (#4:ori -> term)) oris;

     in filter_outs ors itms end;

 fun memI a b = member op = a b;

 (*filter oris which are in pbt, too*)

 fun filter_pbt oris pbt =

     let val dscs = map (fst o snd) pbt

     in filter ((memI dscs) o (#4: ori -> term)) oris end;

 (*.combine itms from pbl + met and complete them wrt. pbt.*)

 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)

 local infix mem;

 fun x mem [] = false

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

 in 

 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met = 

 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];

    *)

     let val vat = max_vt pits;

         val itms = pits @ 

 		   (filter ((curry (op mem) vat) o (#2:itm -> int list)) mits);

 	val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;

         val os = filter_outs ors itms;

     (*WN.12.03?: does _NOT_ add itms from met ?!*)

     in itms @ (map (ori2Coritm met) os) end

 end;

 (*.complete model and guard of a calc-head .*)

 local infix mem;

 fun x mem [] = false

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

 in 

 fun complete_mod_ (oris, mpc, ppc, probl) =

     let	val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl

 	val vat = if probl = [] then 1 else max_vt probl

 	val pors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris

 	val pors = filter_outs pors pits (*which are in pbl already*)

         val pors = (filter_pbt pors ppc) (*which are in pbt, too*)

 	val pits = pits @ (map (ori2Coritm ppc) pors)

 	val mits = complete_metitms oris pits [] mpc

     in (pits, mits) end

 end;

 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =

     (if dI = e_domID then odI else dI,

      if pI = e_pblID then opI else pI,

      if mI = e_metID then omI else mI):spec;

 (*.find a next applicable tac (for calcstate) and update ptree

  (for ev. finding several more tacs due to hide).*)

 (*FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !!*)

 (*WN.24.10.03        ~~~~~~~~~~~~~~   -> tac     -> tac_      -> -"- as arg*)

 (*WN.24.10.03        fun nxt_solv   = ...................................??*)

 fun nxt_specif (tac as Model_Problem) (pt, pos as (p,p_)) =

     let

       val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p

       val (dI, pI, mI) = some_spec ospec spec

       val thy = assoc_thy dI

       val mpc = (#ppc o get_met) mI (* just for reuse complete_mod_ *)

       val {cas, ppc, ...} = get_pbt pI

       val pbl = init_pbl ppc (* fill in descriptions *)

       (*----------------if you think, this should be done by the Dialog 

        in the java front-end, search there for WN060225-modelProblem----*)

       val (pbl, met) = 

         case cas of NONE => (pbl, [])

   			| _ => complete_mod_ (oris, mpc, ppc, probl)

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

       val tac_ = Model_Problem' (pI, pbl, met)

       val (pos,c,_,pt) = generate1 thy tac_ (Uistate, ctxt) pos pt

     in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end

   | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp

   | nxt_specif (Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp

   | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp

     (*. called only if no_met is specified .*)     

   | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =

       let 

         val (PblObj {origin = (oris, (dI,_,_),_), ctxt, ...}) = get_obj I pt p

         val opt = refine_ori oris pI

       in 

         case opt of

 	        SOME pI' => 

 	          let 

               val {met,ppc,...} = get_pbt pI'

 	            val pbl = init_pbl ppc

 	            (*val pt = update_pbl pt p pbl ..done by Model_Problem*)

 	            val mI = if length met = 0 then e_metID else hd met

               val thy = assoc_thy dI

 	            val (pos,c,_,pt) = 

 		            generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[])) 

 			            (Uistate, ctxt) pos pt

 	          in ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),

 		          (pos, (Uistate, e_ctxt)))], c, (pt,pos)) 

             end

 	      | NONE => ([], [], ptp)

       end

   | nxt_specif (Refine_Problem pI) (ptp as (pt, pos as (p,_))) =

       let

         val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), probl, ctxt, ...}) = get_obj I pt p

 	      val thy = if dI' = e_domID then dI else dI'

       in 

         case refine_pbl (assoc_thy thy) pI probl of

 	        NONE => ([], [], ptp)

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

 	          let 

               val (pos,c,_,pt) = generate1 (assoc_thy thy) 

 			          (Refine_Problem' rfd) (Uistate, ctxt) pos pt

 	          in ([(Refine_Problem pI, Refine_Problem' rfd,

 			        (pos, (Uistate, e_ctxt)))], c, (pt,pos))

             end

       end

   | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =

       let

         val (PblObj {origin=(oris,(dI,_,_),_),spec=(dI',pI',_), probl, ctxt, ...}) = get_obj I pt p;

 	      val thy = assoc_thy (if dI' = e_domID then dI else dI');

         val {ppc,where_,prls,...} = get_pbt pI

 	      val pbl as (_,(itms,_)) = 

 	        if pI'=e_pblID andalso pI=e_pblID

 	        then (false, (init_pbl ppc, []))

 	        else match_itms_oris thy probl (ppc,where_,prls) oris(*FIXXXXXME?*)

 	        (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)

 	      val ((p,Pbl),c,_,pt) = 

 	        generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt

       in ([(Specify_Problem pI, Specify_Problem' (pI, pbl),

 		    (pos,(Uistate, e_ctxt)))], c, (pt,pos))

       end

   (*transfers oris (not required in pbl) to met-model for script-env

     FIXME.WN.8.03: application of several mIDs to SAME model?*)

   | nxt_specif (Specify_Method mID) (ptp as (pt, pos as (p,_))) = 

       let

         val (PblObj {origin=(oris,(dI',pI',mI'),_), probl=pbl, spec=(dI,pI,mI), 

           meth=met, ctxt, ...}) = get_obj I pt p;

         val {ppc,pre,prls,...} = get_met mID

         val thy = assoc_thy dI

         val oris = add_field' thy ppc oris;

         val dI'' = if dI=e_domID then dI' else dI;

         val pI'' = if pI = e_pblID then pI' else pI;

         val met = if met=[] then pbl else met;(*WN0602 what if more itms in met?*)

         val (ok, (itms, pre')) = match_itms_oris thy met (ppc,pre,prls ) oris;

         val (pos,c,_,pt)= 

 	        generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt

       in ([(Specify_Method mID, Specify_Method' (mID, oris, itms),

 		    (pos,(Uistate, e_ctxt)))], c, (pt,pos)) 

       end    

   | nxt_specif (Specify_Theory dI) (pt, pos as (p,Pbl)) =

       let

         val ctxt = get_ctxt pt pos

         val (dI',_,_) = get_obj g_spec pt p

 	      val (pos,c,_,pt) = 

 	        generate1 (assoc_thy "Isac") (Specify_Theory' dI)  (Uistate, ctxt) pos pt

       in  (*FIXXXME: check if pbl can still be parsed*)

 	      ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,

 	        (pt, pos))

       end

   | nxt_specif (Specify_Theory dI) (pt, pos as (p,Met)) =

       let

         val ctxt = get_ctxt pt pos

         val (dI',_,_) = get_obj g_spec pt p

 	      val (pos,c,_,pt) = 

 	        generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt

       in  (*FIXXXME: check if met can still be parsed*)

 	      ([(Specify_Theory dI, Specify_Theory' dI, (pos,(Uistate, ctxt)))], c,

 	        (pt, pos))

       end

   | nxt_specif m' _ = 

     error ("nxt_specif: not impl. for "^tac2str m');

 (* get the values from oris; handle the term list w.r.t. penv *)

 local infix mem;

 fun x mem [] = false

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

 in 

 fun vals_of_oris oris =

     ((map (mkval' o (#5:ori -> term list))) o 

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

 end;

 (* create a calc-tree with oris via an cas.refined pbl *)

 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =

       if pI <> [] 

       then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)

 	      let 

           val {cas, met, ppc, thy, ...} = get_pbt pI

 	        val dI = if dI = "" then theory2theory' thy else dI

 	        val thy = assoc_thy dI

 	        val mI = if mI = [] then hd met else mI

 	        val hdl = case cas of NONE => pblterm dI pI | SOME t => t

 	        val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))

 					  ([], (dI,pI,mI), hdl)

 	        val pt = update_spec pt [] (dI,pI,mI)

 	        val pits = init_pbl' ppc

 	        val pt = update_pbl pt [] pits

 	      in ((pt, ([] ,Pbl)), []) : calcstate end

       else 

         if mI <> [] 

         then (* from met-browser *)

 	        let 

             val {ppc,...} = get_met mI

 	          val dI = if dI = "" then "Isac" else dI

 	          val thy = assoc_thy dI;

 	          val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))

 					    ([], (dI,pI,mI), e_term(*FIXME met*));

 	          val pt = update_spec pt [] (dI,pI,mI);

 	          val mits = init_pbl' ppc;

 	          val pt = update_met pt [] mits;

 	        in ((pt, ([], Met)), []) : calcstate end

         else (* new example, pepare for interactive modeling *)

 	        let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)

 					  ([], e_spec, e_term)

 	        in ((pt, ([], Pbl)), []) : calcstate end

   | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = 

       let           (* both """"""""""""""""""""""""" either empty or complete *)

 	      val thy = assoc_thy dI

 	      val (pI, (pors, pctxt), mI) = 

 	        if mI = ["no_met"] 

 	        then 

             let 

               val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;

 		          val pI' = refine_ori' pors pI;

 		        in (pI', (pors(*refinement over models with diff.precond only*), pctxt),

 		          (hd o #met o get_pbt) pI') end

 	        else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)

 	      val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)

 	      val dI = theory2theory' (maxthy thy thy')

 	      val hdl = 

           case cas of

 		        NONE => pblterm dI pI

 		      | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;

         val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))

 				  (pors, (dI, pI, mI), hdl)

         val pt = update_ctxt pt [] pctxt

       in ((pt, ([], Pbl)), 

         fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate

       end;

 (*18.12.99*)

 fun get_spec_form (m:tac_) ((p,p_):pos') (pt:ptree) = 

 (*  case appl_spec p pt m of           /// 19.1.00

     Notappl e => Error' (Error_ e)

   | Appl => 

 *)    let val (_,_,f,_,_,_) = specify m (p,p_) [] pt

       in f end;

 (*fun tag_form thy (formal, given) = Thm.global_cterm_of thy

 	      (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819*)

 fun tag_form thy (formal, given) =

  (let

     val gf = (head_of given) $ formal;

     val _ = Thm.global_cterm_of thy gf

   in gf end)

   handle _ => error ("calchead.tag_form: " ^ term_to_string''' thy given ^

     " .. " ^ term_to_string''' thy formal ^ " ..types do not match");

 (* val formal = (the o (parse thy)) "[R::real]";

 > val given = (the o (parse thy)) "fixed_values (cs::real list)";

 > tag_form thy (formal, given);

 val it = "fixed_values [R]" : cterm

 *)

 fun chktyp thy (n, fs, gs) = 

   ((writeln o (term_to_string'''  thy) o (nth n)) fs;

    (writeln o (term_to_string''' thy) o (nth n)) gs;

    tag_form thy (nth n fs, nth n gs));

 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);

 (* #####################################################

    find the failing item:

 > val n = 2;

 > val tag__form = chktyp (n,formals,givens);

 > (type_of o Thm.term_of o (nth n)) formals; 

 > (type_of o Thm.term_of o (nth n)) givens;

 > atomty ((Thm.term_of o (nth n)) formals);

 > atomty ((Thm.term_of o (nth n)) givens);

 > atomty (Thm.term_of tag__form);

 > use_thy"isa-98-1-HOL-plus/knowl-base/DiffAppl";

  ##################################################### *)

 (* #####################################################

    testdata setup

 val origin = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::rat","(+0)"];

 val formals = map (the o (parse thy)) origin;

 val given  = ["equation (lhs=rhs)",

 	     "bound_variable bdv",   (* TODO type *) 

 	     "error_bound apx"];

 val where_ = ["e is_root_equation_in bdv",

 	      "bdv is_var",

 	      "apx is_const_expr"];

 val find   = ["L::rat set"];

 val with_  = ["L = {bdv. || ((%x. lhs) bdv) - ((%x. rhs) bdv) || < apx}"];

 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

 val givens = map (the o (parse thy)) given;

 val tag__forms = chktyps (formals, givens);

 map ((atomty) o Thm.term_of) tag__forms;

  ##################################################### *)

 (* check pbltypes, announces one failure a time *)

 (*fun chk_vars ctppc = 

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

     appc flat (mappc (vars o Thm.term_of) ctppc)

   in if (wh\\gi) <> [] then ("wh\\gi",wh\\gi)

      else if (re\\(gi union fi)) <> [] 

 	    then ("re\\(gi union fi)",re\\(gi union fi))

 	  else ("ok",[]) end;*)

 fun chk_vars ctppc = 

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

           appc flat (mappc vars ctppc)

       val chked = subtract op = gi wh

   in if chked <> [] then ("wh\\gi", chked)

      else let val chked = subtract op = (union op = gi fi) re

           in if chked  <> []

 	     then ("re\\(gi union fi)", chked)

 	     else ("ok", []) 

           end

   end;

 (* check a new pbltype: variables (Free) unbound by given, find*) 

 fun unbound_ppc ctppc =

   let val {Given=gi,Find=fi,Relate=re,...} = 

     appc flat (mappc vars ctppc)

   in distinct (*re\\(gi union fi)*) 

               (subtract op = (union op = gi fi) re) end;

 (*

 > val org = {Given=["[R=(R::real)]"],Where=[],

 	   Find=["[A::real]"],With=[],

 	   Relate=["[A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"]

 	   }:string ppc;

 > val ctppc = mappc (the o (parse thy)) org;

 > unbound_ppc ctppc;

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

 *)

 (* f, a binary operator, is nested rightassociative *)

 fun foldr1 f xs =

   let

     fun fld f (x::[]) = x

       | fld f (x::x'::[]) = f (x',x)

       | fld f (x::x'::xs) = f (fld f (x'::xs),x);

   in ((fld f) o rev) xs end;

 (*

 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";

 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));

 > val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));

 > Thm.global_cterm_of thy conj;

 val it = "(a = b & c = d) & e = f" : cterm

 *)

 (* f, a binary operator, is nested leftassociative *)

 fun foldl1 f (x::[]) = x

   | foldl1 f (x::x'::[]) = f (x,x')

   | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));

 (*

 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";

 > val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));

 > val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));

 > Thm.global_cterm_of thy conj;

 val it = "a = b & c = d & e = f & g = h" : cterm

 *)

 (* called only once, if a Subproblem has been located in the script*)

 fun nxt_model_pbl (Subproblem'((_,pblID,metID),_,_,_,_,_)) ptp =

      (case metID of

 	      ["no_met"] => 

 	        (snd3 o hd o fst3) (nxt_specif (Refine_Tacitly pblID) ptp)

       | _ => (snd3 o hd o fst3) (nxt_specif Model_Problem ptp))

         (*all stored in tac_ itms^^^^^^^^^^*)

   | nxt_model_pbl tac_ _ = 

       error ("nxt_model_pbl: called by tac= " ^ tac_2str tac_);

 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)

 fun eq4 v (_,vts,_,_,_) = member op = vts v;

 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;

 (*.complete _NON_empty calc-head for autocalc (sub-)pbl from oris

   + met from fmz; assumes pos on PblObj, meth = [].*)

 fun complete_mod (pt, pos as (p, p_):pos') =

 (* val (pt, (p, _)) = (pt, p);

    val (pt, (p, _)) = (pt, pos);

    *)

     let val _= if p_ <> Pbl 

 	       then tracing("###complete_mod: only impl.for Pbl, called with "^

 			    pos'2str pos) else ()

 	val (PblObj{origin=(oris, ospec, hdl), probl, spec, ...}) =

 	    get_obj I pt p

 	val (dI,pI,mI) = some_spec ospec spec

 	val mpc = (#ppc o get_met) mI

 	val ppc = (#ppc o get_pbt) pI

 	val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)

         val pt = update_pblppc pt p pits

 	val pt = update_metppc pt p mits

     in (pt, (p,Met):pos') end

 ;

 (*| complete_mod (pt, pos as (p, Met):pos') =

     error ("###complete_mod: only impl.for Pbl, called with "^

 		 pos'2str pos);*)

 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);

    oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)

 fun all_modspec (pt, (p,_):pos') =

   let 

     val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;

     val thy = assoc_thy dI;

 	  val {ppc, ...} = get_met mI;

     val (fmz_, vals) = oris2fmz_vals pors;

 	  val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 

       |> declare_constraints' vals

     val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);

 	  val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)

 	  val pt = update_spec pt p (dI,pI,mI);

     val pt = update_ctxt pt p ctxt

 (*

 	  val mors = prep_ori fmz_ thy ppc |> #1;

     val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);

 	  val pt = update_metppc pt p (map (ori2Coritm ppc) mors);

     (*WN110715: why pors, mors handled so differently?*)

 	  val pt = update_spec pt p (dI,pI,mI);

 *)

   in (pt, (p,Met): pos') end;

 (*WN0312: use in nxt_spec, too ? what about variants ???*)

 fun is_complete_mod_ ([]: itm list) = false

   | is_complete_mod_ itms = 

     foldl and_ (true, (map #3 itms));

 fun is_complete_mod (pt, pos as (p, Pbl): pos') =

       if (is_pblobj o (get_obj I pt)) p 

       then (is_complete_mod_ o (get_obj g_pbl pt)) p

       else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)

   | is_complete_mod (pt, pos as (p, Met)) = 

       if (is_pblobj o (get_obj I pt)) p 

       then (is_complete_mod_ o (get_obj g_met pt)) p

       else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)

   | is_complete_mod (_, pos) =

       error ("is_complete_mod called by " ^ pos'2str pos ^

 		    " (should be Pbl or Met)");

 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)

 fun is_complete_spec (pt, pos as (p,_): pos') = 

     if (not o is_pblobj o (get_obj I pt)) p 

     then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)

     else let val (dI,pI,mI) = get_obj g_spec pt p

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

 (*.complete empty items in specification from origin (pbl, met ev.refined);

   assumes 'is_complete_mod'.*)

 fun complete_spec (pt, pos as (p,_): pos') = 

     let val PblObj {origin = (_,ospec,_), spec,...} = get_obj I pt p

 	val pt = update_spec pt p (some_spec ospec spec)

     in (pt, pos) end;

 fun is_complete_modspec ptp = 

     is_complete_mod ptp andalso is_complete_spec ptp;

 fun pt_model (PblObj {meth,spec,origin=(_,spec',hdl),...}) Met =

 (* val ((PblObj {meth,spec,origin=(_,spec',hdl),...}), Met) = (ppobj, p_);

    *)

     let val (_,_,metID) = get_somespec' spec spec'

 	val pre = 

 	    if metID = e_metID then []

 	    else let val {prls,pre=where_,...} = get_met metID

 		     val pre = check_preconds' prls where_ meth 0

 		 in pre end

 	val allcorrect = is_complete_mod_ meth

 			 andalso foldl and_ (true, (map #1 pre))

     in ModSpec (allcorrect, Met, hdl, meth, pre, spec) end

   | pt_model (PblObj {probl,spec,origin=(_,spec',hdl),...}) _(*Frm,Pbl*) =

 (* val ((PblObj {probl,spec,origin=(_,spec',hdl),...}),_) = (ppobj, p_);

    *)

     let val (_,pI,_) = get_somespec' spec spec'

 	val pre =

 	    if pI = e_pblID then []

 	    else let val {prls,where_,cas,...} = get_pbt pI

 		     val pre = check_preconds' prls where_ probl 0

 		 in pre end

 	val allcorrect = is_complete_mod_ probl

 			 andalso foldl and_ (true, (map #1 pre))

     in ModSpec (allcorrect, Pbl, hdl, probl, pre, spec) end;

 fun pt_form (PrfObj {form,...}) = Form form

   | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =

     let val (dI, pI, _) = get_somespec' spec spec'

 	val {cas,...} = get_pbt pI

     in case cas of

 	   NONE => Form (pblterm dI pI)

 	 | SOME t => Form (subst_atomic (mk_env probl) t)

     end;

 (*vvv takes the tac _generating_ the formula=result, asm ok....

 fun pt_result (PrfObj {result=(t,asm), tac,...}) = 

     (Form t, 

      if null asm then NONE else SOME asm, 

      SOME tac)

   | pt_result (PblObj {result=(t,asm), origin = (_,ospec,_), spec,...}) =

     let val (_,_,metID) = some_spec ospec spec

     in (Form t, 

 	if null asm then NONE else SOME asm, 

 	if metID = e_metID then NONE else SOME (Apply_Method metID)) end;

 -------------------------------------------------------------------------*)

 (*.pt_extract returns

       # the formula at pos

       # the tactic applied to this formula

       # the list of assumptions generated at this formula

 	(by application of another tac to the preceding formula !)

    pos is assumed to come from the frontend, ie. generated by moveDown.*)

 (*cannot be in ctree.sml, because ModSpec has to be calculated*)

 fun pt_extract (pt,([],Res)) = (* WN120512: --returns--> Check_Postcondition WRONGLY

                                   see --- build fun is_exactly_equal*)

     (* ML_TODO 110417 get assumptions from ctxt !? *)

       let val (f, asm) = get_obj g_result pt []

       in (Form f, NONE, asm) end

   | pt_extract (pt,(p,Res)) =

       let

         val (f, asm) = get_obj g_result pt p

         val tac =

           if last_onlev pt p

           then

             if is_pblobj' pt (lev_up p)

             then

               let

                 val (PblObj{spec=(_,pI,_),...}) = get_obj I pt (lev_up p)

               in if pI = e_pblID then NONE else SOME (Check_Postcond pI) end

 		        else SOME End_Trans (*WN0502 TODO for other branches*)

 		      else

 		        let val p' = lev_on p

 		        in

 		          if is_pblobj' pt p'

 		          then

 		            let val (PblObj{origin = (_,(dI,pI,_),_),...}) = get_obj I pt p'

 		            in SOME (Subproblem (dI, pI)) end

 		          else

 		            if f = get_obj g_form pt p'

 		            then SOME (get_obj g_tac pt p') (*because this Frm ~~~is not on worksheet*)

 		            else SOME (Take (term2str (get_obj g_form pt p')))

 		        end

       in (Form f, tac, asm) end

   | pt_extract (pt, pos as (p,p_(*Frm,Pbl*))) =

       let

         val ppobj = get_obj I pt p

         val f = if is_pblobj ppobj then pt_model ppobj p_ else get_obj pt_form pt p

         val tac = g_tac ppobj

       in (f, SOME tac, []) end;

 (**. get the formula from a ctree-node:

  take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)

  take res from all other PrfObj's .**)

 (*designed for interSteps, outcommented 04 in favour of calcChangedEvent*)

 fun formres p (Nd (PblObj {origin = (_,_, h), result = (r, _),...}, _)) =

     [("headline", (p, Frm), h), 

      ("stepform", (p, Res), r)]

   | formres p (Nd (PrfObj {form, result = (r, _),...}, _)) = 

     [("stepform", (p, Frm), form), 

      ("stepform", (p, Res), r)];

 fun form p (Nd (PrfObj {result = (r, _),...}, _)) = 

     [("stepform", (p, Res), r)]

 (*assumes to take whole level, in particular hd -- for use in interSteps*)

 fun get_formress fs p [] = flat fs

   | get_formress fs p (nd::nds) =

     (* start with   'form+res'       and continue with trying 'res' only*)

     get_forms (fs @ [formres p nd]) (lev_on p) nds

 and get_forms fs p [] = flat fs

   | get_forms fs p (nd::nds) =

     if is_pblnd nd

     (* start again with      'form+res' ///ugly repeat with Check_elementwise

     then get_formress (fs @ [formres p nd]) (lev_on p) nds                   *)

     then get_forms    (fs @ [formres p nd]) (lev_on p) nds

     (* continue with trying 'res' only*)

     else get_forms    (fs @ [form    p nd]) (lev_on p) nds;

 (**.get an 'interval' 'from' 'to' of formulae from a ptree.**)

 (*WN050219 made robust against _'to' below or after Complete nodes

 	   by handling exn caused by move_dn*)

 (*WN0401 this functionality belongs to ctree.sml, 

 but fetching a calc_head requires calculations defined in modspec.sml

 transfer to ME/me.sml !!!

 WN051224 ^^^ doesnt hold any longer, since only the headline of a calc_head

 is returned !!!!!!!!!!!!!

 *)

 fun eq_pos' (p1,Frm) (p2,Frm) = p1 = p2

   | eq_pos' (p1,Res) (p2,Res) = p1 = p2

   | eq_pos' (p1,Pbl) (p2,p2_) = p1 = p2 andalso (case p2_ of

 						     Pbl => true

 						   | Met => true

 						   | _ => false)

   | eq_pos' (p1,Met) (p2,p2_) = p1 = p2 andalso (case p2_ of

 						     Pbl => true

 						   | Met => true

 						   | _ => false)

   | eq_pos' _ _ = false;

 (*.get an 'interval' from the ctree; 'interval' is w.r.t. the 

    total ordering Position#compareTo(Position p) in the java-code

 val get_interval = fn

     : pos' ->     : from is "move_up 1st-element" to return

       pos' -> 	  : to the last element to be returned; from < to

       int -> 	  : level: 0 gets the flattest sub-tree possible

 			   >999 gets the deepest sub-tree possible

       ptree -> 	  : 

       (pos' * 	  : of the formula

        Term.term) : the formula

 	  list

 .*)

 fun get_interval from to level pt =

   let

     fun get_inter c (from:pos') (to:pos') lev pt =

 	    if eq_pos' from to orelse from = ([],Res)

 	    (*orelse ... avoids Exception- PTREE "end of calculation" raised,

 	     if 'to' has values NOT generated by move_dn, see systest/me.sml

              TODO.WN0501: introduce an order on pos' and check "from > to"..

              ...there is an order in Java! 

              WN051224 the hack got worse with returning term instead ptform*)

 	    then

 	      let val (f,_,_) = pt_extract (pt, from)

 	      in

 	        case f of

 	          ModSpec (_,_,headline,_,_,_) => c @ [(from, headline)] 

 	        | Form t => c @ [(from, t)]

 	      end

 	    else 

 	      if lev < lev_of from

 	      then (get_inter c (move_dn [] pt from) to lev pt)

 		      handle (PTREE _(*from move_dn too far*)) => c

 		    else

 		      let

 		        val (f,_,_) = pt_extract (pt, from)

 		        val term = case f of

 		          ModSpec (_,_,headline,_,_,_) => headline

 				    | Form t => t

 		      in (get_inter (c @ [(from, term)]) (move_dn [] pt from) to lev pt)

 		        handle (PTREE _(*from move_dn too far*)) => c @ [(from, term)]

 		      end

   in get_inter [] from to level pt end;

 (*for tests*)

 fun posform2str (pos:pos', form) =

     "("^ pos'2str pos ^", "^

     (case form of 

 	 Form f => term2str f

        | ModSpec c => term2str (#3 c(*the headline*)))

     ^")";

 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o 

 			(map posform2str)) pfs;

 fun posterm2str (pos:pos', t) =

     "("^ pos'2str pos ^", "^term2str t^")";

 fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o 

 			(map posterm2str)) pfs;

 (*WN050225 omits the last step, if pt is incomplete*)

 fun show_pt pt = 

     tracing (posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));

 (*.get a calchead from a PblObj-node in the ctree; 

    preconditions must be calculated.*)

 fun get_ocalhd (pt, pos' as (p,Pbl):pos') = 

     let val PblObj {origin = (oris, ospec, hdf'), spec, probl,...} = 

 	    get_obj I pt p

 	val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))

 	val pre = check_preconds (assoc_thy"Isac") prls where_ probl

     in (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec):ocalhd end

 | get_ocalhd (pt, pos' as (p,Met):pos') = 

     let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), 

 		    spec, meth, ...} = 

 	    get_obj I pt p

 	val {prls,pre,...} = get_met (#3 (some_spec ospec spec))

 	val pre = check_preconds (assoc_thy"Isac") prls pre meth

     in (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec):ocalhd end;

 (*.at the activeFormula set the Model, the Guard and the Specification 

    to empty and return a CalcHead;

    the 'origin' remains (for reconstructing all that).*)

 fun reset_calchead (pt, pos' as (p,_):pos') = 

     let val PblObj {origin = (_, _, hdf'),...} = get_obj I pt p

 	val pt = update_pbl pt p []

 	val pt = update_met pt p []

 	val pt = update_spec pt p e_spec

     in (pt, (p,Pbl):pos') end;

 end

 open CalcHead;