(* Title:  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

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

(* 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 ctxt sel (d,ts) [] =

    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)

                             (comp_dts (d,ts))) ^

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

     [])

  | seek_oridts ctxt 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 ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))

         ^ " not for " ^ sel, e_ori_, [])

    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 (Print_Mode.setmp [](Syntax.string_of_term 

                                           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 (Print_Mode.setmp [] (Syntax.string_of_term

                                                           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;

(*---------------------------------------------(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 _ = 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, (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt 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, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts) 

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

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

    (fd, Print_Mode.setmp [] ((Syntax.string_of_term (thy2ctxt 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, 

          ((Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt 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)) =>(* 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 (Print_Mode.setmp [] (Syntax.string_of_term 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 s = !show_types; val _ = show_types:= true;*)

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

    val msg = case opt of 

      SOME _ => "" 

    | NONE => ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) d) ^

               " " ^

	       ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term

                                                           ctxt))) ts)

	     ^ " is illtyped");

    (*val _ = show_types:= s*)

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

(*WN.11.03: from lists*)

fun is_known ctxt sel ori t =

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

   *)

  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(*,pval*)) = 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 (Print_Mode.setmp [] (Syntax.string_of_term 

					             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 ((Print_Mode.setmp [] (Syntax.string_of_term 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 t =

      let

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

      in case parse (ProofContext.theory_of ctxt) t of

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

        | SOME t' =>

          let val (d, ts) = split_dts (term_of 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 parse (ProofContext.theory_of ctxt) str of

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

        | SOME t => case is_known ctxt sel oris (term_of t) of

            ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of

              ("", itm) => Add itm

              | (msg, _) => Err msg)

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

(* 

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

*)

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

       *)

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