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

   most important types are declared in mstools.sml.

   author: Walther Neuper

   991122

   (c) due to copyright terms

use"ME/calchead.sml";

use"calchead.sml";

*)

(* TODO interne Funktionen aus sig entfernen *)

signature CALC_HEAD =

  sig

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

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

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

    datatype appl = Appl of tac_ | Notappl of string

    val appl_add :

       Theory.theory ->

       string ->

       SpecifyTools.ori list ->

       SpecifyTools.itm list ->

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

    type calcstate

    type calcstate'

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

    val chktyp :

       Theory.theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm

    val chktyps :

       Theory.theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm 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.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.theory ->

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

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

    val has_list_type : Term.term -> bool

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

    val insert_ppc :

       Theory.theory ->

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

       SpecifyTools.itm list -> SpecifyTools.itm list

    val insert_ppc' :

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

    val is_complete_mod : ptree * pos' -> bool

    val is_complete_mod_ : SpecifyTools.itm list -> bool

    val is_complete_modspec : ptree * pos' -> bool

    val is_complete_spec : ptree * pos' -> bool

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

    val is_copy_named_idstr : string -> bool

    val is_error : SpecifyTools.itm_ -> bool

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

    val is_known :

       Theory.theory ->

       string ->

       SpecifyTools.ori list ->

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

    val is_list_type : Term.typ -> bool

    val is_notyet_input :

       Theory.theory ->

       SpecifyTools.itm list ->

       Term.term list ->

       SpecifyTools.ori ->

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

    val is_parsed : SpecifyTools.itm_ -> bool

    val is_untouched : SpecifyTools.itm -> bool

    val matc :

       Theory.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.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.theory -> string -> SpecifyTools.itm_ -> tac

    val mtc :

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

    val nxt_add :

       Theory.theory ->

       SpecifyTools.ori list ->

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

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

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

    val nxt_spec :

       pos_ ->

       bool ->

       SpecifyTools.ori list ->

       spec ->

       SpecifyTools.itm list * SpecifyTools.itm list ->

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

       spec -> pos_ * tac

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

    val nxt_specif_additem :

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

    val nxt_specify_init_calc : fmz -> calcstate

    val ocalhd_complete :

       SpecifyTools.itm list ->

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

    val ori2Coritm :

	pat list -> ori -> itm

    val ori_2itm :

       'a ->

       SpecifyTools.itm_ ->

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

    val overwrite_ppc :

       Theory.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 Library.option * Term.term list

    val pt_form : ppobj -> ptform

    val pt_model : ppobj -> pos_ -> ptform

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

    val seek_oridts :

       Theory.theory ->

       string ->

       Term.term * Term.term list ->

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

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

    val seek_orits :

       Theory.theory ->

       string ->

       Term.term list ->

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

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

    val seek_ppc :

       int -> SpecifyTools.itm list -> SpecifyTools.itm Library.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.theory -> Thm.cterm * Thm.cterm -> Thm.cterm

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

    val typeless : Term.term -> Term.term

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

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

    val variants_in : Term.term list -> int

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

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

  end

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

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

struct

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

(* datatypes *)

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

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

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

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

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

   because the tacis hold enought information for efficiently rebuilding

   this state just by "fun generate ".*)

type calcstate = 

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

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

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

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

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

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

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

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

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

  and then replaced by the the newly created;

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

  because the tacis hold enought information for efficiently rebuilding

  this state just by "fun generate ".*)

type calcstate' = 

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

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

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

			 deleted by application of taci list*)     

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

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

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

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

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

(*.is the calchead complete ?.*)

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

    foldl and_ (true, map #3 its) andalso 

    foldl and_ (true, map #1 pre) andalso 

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

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

   'type-less' usually is illtyped                                  *)

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

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

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

  | typeless (Bound i) = (Bound i)

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

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

(*

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

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

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

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

> typeless t1 = typeless t2;

val it = true : bool

*)

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

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

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

  ("'"^(string_of_cterm (comp_dts thy (d,ts)))^

 (*"' not found (typed)", e_ori_:ori, [])          ///11.11.03*)

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

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

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

     *)

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

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

      then if sel = sel' 

	     then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')

	   else ((string_of_cterm (comp_dts thy(d,ts)))^

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

    else seek_oridts thy sel (d,ts) oris;

(*FIXXXME.WN.11.03: + dont take first inter<>[] .. ev. variants are following:

 thus take largest intersection !!!

 if sel NOTok .. then the correct itm should NOT be overwritten by insert_ppc*)

(*fun eq7 d (_,_,_,d',_) = d = d';

fun inter_length ((_,_,_,_,ts), (_,_,_,_,ts')) = (length ts) < (length ts');

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

  ("'"^(string_of_cterm (comp_dts thy (d,ts)))^

 (*"' not found (typed)", e_ori_:ori, [])          ///11.11.03*)

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

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

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

     *)

  | seek_oridts _ sel (d,ts) oris =

    let val dscOK = filter (eq7 d) oris; 

    in if dscOK = [] then ("'"^(string_of_cterm (comp_dts thy (d,ts)))^

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

       else let val (id,vat,sel',d',ts') = gen_max inter_length dscOK;

	    in if sel = sel' then ("",(id,vat,sel,d,ts inter ts'), [])

	       else ("wrong field",(id,vat,sel,d,ts inter ts'), []) end

    end;

--------------------didnt work with Add_Given/_Find/_Relation 11.03*)

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

fun seek_orits thy sel ts [] = 

  ("'"^

   (strs2str (map (Sign.string_of_term (sign_of thy)) ts))^

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

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

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

      then if sel = sel' 

	   then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')

	   else (((strs2str' o map (Sign.string_of_term (sign_of thy))) ts)^

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

    else seek_orits thy sel ts oris;

(* false

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

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

uncaught exception TYPE

> seek_orits thy sel ts [];

uncaught exception TYPE

*)

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

fun seek_ppc id [] = None

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

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

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

datatype appl = Appl of tac_ | Notappl of string;

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

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

  gis @ whs @ fis @ wis @ res;

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

  gis @ fis @ res;

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

   assumes equal descriptions in immediate sequence    *)

fun variants_in ts =

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

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

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

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

    fun coll eq  xs [] = xs

      | coll eq  xs (y::ys) = 

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

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

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

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

(*fdcrs = descriptions in formalization

  unused 22.11.00

fun is_already_input thy fdcrs ts t = 

  let 

    val tss = flat (map isalist2list ts);

(*28.1.     val (dcr,t') = split_dsc_t fdcrs t; *)

    val (dcr,[t']) = split_dts t;

  in if (typeless t') mem (map typeless tss)

            then ("term '"^(Sign.string_of_term (sign_of thy) t')^

		  "' already input")

	  else "" end;

> val pts = appc (map (term_of o the o (parse thy))) pbl;

> val ts = #Relate pts;

> val t = (term_of o the o (parse thy))"(A=#2*a*b - a^^^#2)";

> is_already_input thy ts t;

val it = "term 'A = #2 * a * b - a ^^^ #2' already input" : string

> val t = (term_of o the o (parse thy))"a=#2*R*sin alpha";

> is_already_input thy ts t;

val it = "term 'a = #2 * R * sin alpha' already input" : string

> val t = (term_of o the o (parse thy))"a=R*sin alpha";

> is_already_input thy ts t;

val it = "" : string

*)

fun is_parsed (Syn _) = false

  | is_parsed _ = true;

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

fun all_dsc_in itm_s =

  let    

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

      | d_in (Syn c) = []

      | d_in (Typ c) = []

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

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

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

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

(* 30.1.00 ---

fun is_Syn (Syn _) = true

  | is_Syn (Typ _) = true

  | is_Syn _ = false;

 --- *)

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

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

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

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

  | is_error _ = true;

(* 30.1.00 ---

fun ct_in (Syn (c)) = c

  | ct_in (Typ (c)) = c

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

 --- *)

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

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

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

(* testdaten besorgen:

   use"test-coil-kernel.sml";

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

        get_obj I pt p;

  *)

(* given oris, ppc, 

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

   ppc is_complete == 

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

   and

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

*)

(*

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

---^^--test 10.3.

> val vts = vts_in itms;

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

> val nvts = vts_cnt vts itms;

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

> val mx = max2 nvts;

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

> val v = max_vt itms;

val v = 3 : int

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

> 

*)

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

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

   *)

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

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

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

   *)

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

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

  (fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');

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

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

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

   atomty d;

   atomty d';

   atomty (hd ts);

   atomty ts';

   cterm_of (sign_of thy) (d $ (hd ts));

   cterm_of (sign_of thy) (d' $ ts');

   comp_dts thy (d,ts);

   *)

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

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

  | is_untouched _ = false;

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

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

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, (string_of_cterm o comp_dts thy) (d,[]):cterm')

  | _ => None end

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

   *)

  | nxt_add thy oris pbt itms =

  let

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

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

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

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

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

   *)

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

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

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

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

      | false_and_not_Sup  _ = false;

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

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

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

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

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

  in if icl = [] 

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

	      [] => None

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

	       *)

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

     else

	 case find_first (test_subset (hd icl)) vors of

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

	      *)

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

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

  end;

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

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

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

  | mk_delete thy str _ = 

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

fun mk_additem "#Given" ct = Add_Given ct

  | mk_additem "#Find"  ct = Add_Find ct    

  | mk_additem "#Relate"ct = Add_Relation ct

  | mk_additem str _ = 

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

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

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

          (sind from DG comes the _OLD_ writepos)*)

(* 

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

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

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

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

at Init_Proof:

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

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

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

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

  *)

(*. determine the next step of specification;

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

eg. in rootpbl 'no_met': 

args:

  preok          predicates are _all_ ok, or problem matches completely

  oris           immediately from formalization 

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

  (pbl,          item lists specified by user

   met)          -"-, tacitly completed by copy_probl

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

  (pbt, mpc)     problem type, guard of method

.*)

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

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

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

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

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

   *)

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

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

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

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

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

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

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

	      (Pbl, mk_delete 

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

	| None => 

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

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

		 oris pbt pbl of

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

                       oris pbt pbl;

  *)

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

				 (Pbl, mk_additem fd ct'))

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

	       if not preok then (Pbl, Refine_Problem pI')

	       else

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

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

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

			   else

			     case find_first (is_error o #5) met of

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

				   (Met, mk_delete (assoc_thy dI) fd itm_)

			     | None => 

				 (case nxt_add (assoc_thy dI) oris mpc met of

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

				      (Met, mk_additem fd ct')

				    | None => 

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

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

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

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

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

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

   *)

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

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

   case find_first (is_error o #5) met of

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

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

   | None => 

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

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

       | None => 

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

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

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

		 else if not preok then (Met, Specify_Method mI)

		      else (Met, Apply_Method mI)));

(* di_ pI_ mI_ pos_

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

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

*)

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

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

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

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

(*3.3.--

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

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

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

  raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^

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

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

  raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^

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

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

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

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

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

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

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

*)

fun is_field_correct sel d dscpbt =

  case assoc (dscpbt, sel) of

    None => false

  | Some ds => d mem ds;

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

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

   *)

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

  let 

    val ts' = (ts_in itm_) union ts;

    val pval = pbl_ids' thy d ts'

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

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

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

  in case itm_ of

    (Cor _) => 

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

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

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

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

  | (Inc _) => if complete

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

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

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

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

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

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

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

  | (Mis _) => if complete

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

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

  end;

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

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

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

   9.01: this + ori_2itm is _VERY UNCLEAR_ ? overhead ?

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

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

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

(*. is_input ori itms <=> 

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

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

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

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

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

   *)

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

  case find_first (eq1 d) pbt of

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

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

			   *)

      (case find_first (eq3 f d) itms of

	   Some (_,_,_,_,itm_) =>

	   let 

	       val ts' = (ts_in itm_) inter ts;

	   in if ts subset ts' 

	      then (((strs2str' o 

		      map (Sign.string_of_term (sign_of thy))) ts')^

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

	      else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts'))    (*3,4*)

	   end

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

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

	)

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

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

(*------------------------------------------------

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

fun is_notyet_input thy itms pval all ((id,vt,fd,d,ts):ori) pbt =

  case find_first (eq1 d) pbt of

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

                              *)

      (case seek_ppc id itms of

	   Some (id',_,_,_,itm_) =>

	   let 

	       val ts' = (ts_in itm_) inter ts;

	   in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all 

					    (id,vt,fd,d,(ts_in itm_)@ts))

	      else (((strs2str' o 

		      map (Sign.string_of_term (sign_of thy))) ts')^

		    " already input", e_itm) end

	 | None => 

	   if all = ts 

	   then ("", ori_2itm (Cor ((e_term,[]),(pid,[])))

			      (pid, pval) all (id,vt,fd,d,ts))

	   else ("", ori_2itm (Inc ((e_term,[]),(e_term,[]))) 

			      (pid, pval) all (id,vt,fd,d,ts))

	)

    | None => ("", ori_2itm (Sup (e_term,[])) 

			      (e_term, []) all (id,vt,fd,d,ts));----*)

fun test_types thy (d,ts) =

  let 

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

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

    val msg = case opt of 

      Some _ => "" 

    | None => ((Sign.string_of_term  (sign_of thy) d)^" "^

	     ((strs2str' o map (Sign.string_of_term(sign_of thy)))ts)

	     ^" is illtyped");

    val _ = show_types:= s

  in msg end;

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

  | maxl (y::ys) =

  let fun mx x [] = x

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

  in mx y ys end;

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

    give feedback on all(?) strange input;

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

(*WN.11.03: from lists*)

fun is_known thy sel ori t =

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

   *)

  let

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

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

		flat o (map vars)) ots;

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

    val ids = map (fst o dest_Free) 

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

  in if (ids \\ oids) <> []

     then (("identifiers "^(strs2str' (ids \\ oids))^

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

     else 

	 if d = e_term 

	 then 

	     if not ((map typeless ts) subset (map typeless ots))

	     then (("terms '"^

		    ((strs2str' o (map (Sign.string_of_term 

					    (sign_of thy)))) ts)^

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

	     else (case seek_orits thy sel ts ori of

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

		       (case test_types thy (d,ts) of

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

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

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

	 else 

	     if d mem (map #4 ori) 

	     then seek_oridts thy sel (d,ts) ori

	     else ((Sign.string_of_term (sign_of thy) d)^

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

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

  end;

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

datatype additm =

	 Add of itm

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

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

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

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

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

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

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

   *)

  let 

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

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

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

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

   *)

  | Some ct =>

      let

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

      in if d = e_term 

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

	 else  

	   (case find_first (eq1 d) pbt of

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

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

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

   *)

	       let

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

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

	       in case find_first (eq2 d) ppc of 

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

							 pbl_ids' thy d ts)))

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

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

   val None = find_first (eq2 d) ppc;

   *)

		   if is_list_dsc d

		   then let val ts = ts union (ts_in itm_) 

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

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

							  pbl_ids' thy d ts)))

			end

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

						       pbl_ids' thy d ts)))

	       end

	   )

      end

  end

(*. add ct to ppc .*)

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

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

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

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

   *)

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

  let

    val ctopt = parse thy ct;

  in case ctopt of

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

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

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

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

		*) 

    (case is_known thy sel oris (term_of ct) of

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

	 (case is_notyet_input thy ppc all ori' pbt of

	      ("",itm)  => Add itm

	    | (msg,_) => Err msg)

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

  end;

(* 

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

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

> val itm_ = #5 itm;

> val ts = ts_in itm_;

> map (atomty) ts; 

*)

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

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

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

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

fun is_copy_named_idstr str =

    case (rev o explode) str of

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