(* Types and tools for 'modeling' und 'specifying' to be used in

    modspec.sml. The types are separated from calchead.sml into this file,

    because some of them are stored in the calc-tree, and thus are required

    _before_ ctree.sml. 

    author: Walther Neuper, Mathias Lehnfeld

    (c) due to copyright terms

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 signature SPECIFY_TOOLS =

   sig

     type envv

     datatype

       item =

           Correct of cterm'

         | False of cterm'

         | Incompl of cterm'

         | Missing of cterm'

         | Superfl of string

         | SyntaxE of string

         | TypeE of string

     val item2str : item -> string

     type itm

     val itm2str_ : Proof.context -> itm -> string

     datatype

       itm_ =

           Cor of (term * term list) * (term * term list)

         | Inc of (term * term list) * (term * term list)

         | Mis of term * term

         | Par of cterm'

         | Sup of term * term list

         | Syn of cterm'

         | Typ of cterm'

     val itm_2str : itm_ -> string

     val itm_2str_ : Proof.context -> itm_ -> string

     val itms2str_ : Proof.context -> itm list -> string

     type 'a ppc

     val ppc2str :

        {Find: string list, With: string list, Given: string list,

          Where: string list, Relate: string list} -> string

     datatype

       match =

           Matches of pblID * item ppc

         | NoMatch of pblID * item ppc

     val match2str : match -> string

     datatype

       match_ =

           Match_ of pblID * (itm list * (bool * term) list)

         | NoMatch_

     val matchs2str : match list -> string

     type ori

     val ori2str : ori -> string

     val oris2str : ori list -> string

     type preori

     val preori2str : preori -> string

     val preoris2str : preori list -> string

     type penv

     (* val penv2str_ : Proof.context -> penv -> string *)

     type vats

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

     val all_ts_in : itm_ list -> term list

     val check_preconds :

        'a ->

        rls ->

        term list -> itm list -> (bool * term) list

     val check_preconds' :

        rls ->

        term list ->

        itm list -> 'a -> (bool * term) list

    (* val chkpre2item : rls -> term -> bool * item  *)

     val pres2str : (bool * term) list -> string

    (* val evalprecond : rls -> term -> bool * term  *)

    (* val cnt : itm list -> int -> int * int *)

     val comp_dts : term * term list -> term

     val comp_dts' : term * term list -> term

     val comp_dts'' : term * term list -> string

     val comp_ts : term * term list -> term

     val d_in : itm_ -> term

     val de_item : item -> cterm'

     val declare_constraints : string -> Proof.context -> Proof.context

     val declare_constraints' : term list -> Proof.context -> Proof.context

     val dest_list : term * term list -> term list (* for testing *)

     val dest_list' : term -> term list

     val dts2str : term * term list -> string

     val e_itm : itm

   (*  val e_listBool : term  *)

   (*  val e_listReal : term  *)

     val e_ori : ori

     val e_ori_ : ori

     val empty_ppc : item ppc

    (* val empty_ppc_ct' : cterm' ppc *)

    (* val getval : term * term list -> term * term *)

    (*val head_precond :

        domID * pblID * 'a ->

        term option ->

        rls ->

        term list ->

        itm list -> 'b -> term * (bool * term) list*)

    (* val init_item : string -> item *)

    (* val is_matches : match -> bool *)

    (* val is_matches_ : match_ -> bool *)

     val is_var : term -> bool

    (* val item_ppc :

        string ppc -> item ppc  *)

     val itemppc2str : item ppc -> string

    (* val matches_pblID : match -> pblID *)

     val max2 : ('a * int) list -> 'a * int

     val max_vt : itm list -> int

     val mk_e : itm_ -> (term * term) list

     val mk_en : int -> itm -> (term * term) list

     val mk_env : itm list -> (term * term) list

     val mkval : 'a -> term list -> term

     val mkval' : term list -> term

    (* val pblID_of_match : match -> pblID *)

     val pbl_ids : Proof.context -> term -> term -> term list

     val pbl_ids' : term -> term list -> term list

    (* val pen2str : theory -> term * term list -> string *)

     val penvval_in : itm_ -> term list

     val refined : match list -> pblID

     val refined_ :

        match_ list -> match_ option

   (*  val refined_IDitms :

        match list -> match option  *)

     val split_dts : term -> term * term list

     val split_dts' : term * term -> term list

   (*  val take_apart : term -> term list  *)

   (*  val take_apart_inv : term list -> term *)

     val ts_in : itm_ -> term list

    (* val unique : term  *)

     val untouched : itm list -> bool

     val upd :

        Proof.context ->

        (''a * (''b * term list) list) list ->

        term ->

        ''b * term -> ''a -> ''a * (''b * term list) list

     val upd_envv :

        Proof.context ->

        envv ->

        vats ->

        term -> term -> term -> envv

     val upd_penv :

        Proof.context ->

        (''a * term list) list ->

        term -> ''a * term -> (''a * term list) list

    (* val upds_envv :

        Proof.context ->

        envv ->

        (vats * term * term * term) list ->

        envv                         *)

     val vts_cnt : int list -> itm list -> (int * int) list

     val vts_in : itm list -> int list

    (* val w_itms2str_ : Proof.context -> itm list -> unit *)

     val get_assumptions : Proof.context -> term list

     val insert_assumptions : term list -> Proof.context -> Proof.context

     val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context

     val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context

   end

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

 structure SpecifyTools : SPECIFY_TOOLS =

 struct

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

 val script_parse = the o (@{theory Script} |> thy2ctxt |> parseNEW);

 val e_listReal = script_parse "[]::(real list)";

 val e_listBool = script_parse "[]::(bool list)";

 (*.take list-term apart w.r.t. handling elementwise input.*)

 fun take_apart t =

     let val elems = isalist2list t

     in map ((list2isalist (type_of (hd elems))) o single) elems end;

 (*val t = str2term "[a, b]";

 > val ts = take_apart t; tracing (terms2str ts);

 ["[a]","[b]"] 

 > t = (take_apart_inv o take_apart) t;

 true*)

 fun take_apart_inv ts =

     let val elems = (flat o (map isalist2list)) ts;

     in list2isalist (type_of (hd elems)) elems end;

 (*val ts = [str2term "[a]", str2term "[b]"];

 > val t = take_apart_inv ts; term2str t;

 "[a, b]"

 ts = (take_apart o take_apart_inv) ts;

 true*)

 (*.revert split_dts only for ts; compare comp_dts.*)

 fun comp_ts (d, ts) = 

     if is_list_dsc d

     then if is_list (hd ts)

 	 then if is_unl d

 	      then (hd ts)            (*e.g. someList [1,3,2]*)

 	      else (take_apart_inv ts) 

 	 (*             SML[ [a], [b] ]SML --> [a,b]             *)

 	 else (hd ts) (*a variable or metavariable for a list*)

     else (hd ts);

 (*.revert split_.

  WN050903 we do NOT know which is from subtheory, description or term;

  typecheck thus may lead to TYPE-error 'unknown constant';

  solution: typecheck with (Thy_Info.get_theory "Isac"); i.e. arg 'thy' superfluous*)

 (*fun comp_dts thy (d,[]) = 

     Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)

 	     (Thy_Info.get_theory "Isac")

 	     (*comp_dts:FIXXME stay with term for efficiency !!!*)

 	     (if is_reall_dsc d then (d $ e_listReal)

 	      else if is_booll_dsc d then (d $ e_listBool)

 	      else d)

   | comp_dts (d,ts) =

     (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)

 	      (Thy_Info.get_theory "Isac")

 	      (*comp_dts:FIXXME stay with term for efficiency !!*)

 	      (d $ (comp_ts (d, ts)))

        handle _ => error ("comp_dts: "^(term2str d)^

 				" $ "^(term2str (hd ts))));*)

 fun comp_dts (d,[]) = 

 	     (if is_reall_dsc d then (d $ e_listReal)

 	      else if is_booll_dsc d then (d $ e_listBool)

 	      else d)

   | comp_dts (d,ts) =

 	      (d $ (comp_ts (d, ts)))

        handle _ => error ("comp_dts: "^(term2str d)^

 				" $ "^(term2str (hd ts))); 

 (*25.8.03*)

 fun comp_dts' (d,[]) = 

     if is_reall_dsc d then (d $ e_listReal)

     else if is_booll_dsc d then (d $ e_listBool)

     else d

   | comp_dts' (d,ts) = (d $ (comp_ts (d, ts)))

        handle _ => error ("comp_dts': "^(term2str d)^

 				" $ "^(term2str (hd ts))); 

 (*val t = str2term "maximum A"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 val it = "maximum A" : cterm

 > val t = str2term "fixedValues [r=Arbfix]"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "fixedValues [r = Arbfix]"

 > val t = str2term "valuesFor [a]"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "valuesFor [a]"

 > val t = str2term "valuesFor [a,b]"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "valuesFor [a, b]"

 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"

 > val t = str2term "boundVariable a";

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "boundVariable a"

 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "interval {x. 0 <= x & x <= 2 * r}"

 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"

 > val t = str2term "solveFor x"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "solveFor x"

 > val t = str2term "errorBound (eps=0)"; 

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "errorBound (eps = 0)"

 > val t = str2term "solutions L";

 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts);

 "solutions L"

 before 6.5.03:

 > val t = (term_of o the o (parse thy)) "testdscforlist [#1]";

 > val (d,ts) = split_dts t;

 > comp_dts thy (d,ts);

 val it = "testdscforlist [#1]" : cterm

 > val t = (term_of o the o (parse thy)) "(A::real)";

 > val (d,ts) = split_dts t;

 val d = Const ("empty","empty") : term

 val ts = [Free ("A","RealDef.real")] : term list

 > val t = (term_of o the o (parse thy)) "[R=(R::real)]";

 > val (d,ts) = split_dts t;

 val d = Const ("empty","empty") : term

 val ts = [Const # $ Free # $ Free (#,#)] : term list

 > val t = (term_of o the o (parse thy)) "[#1,#2]";

 > val (d,ts) = split_dts t;

 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED

 *)

 (*for input_icalhd 11.03*)

 fun comp_dts'' (d,[]) = 

     if is_reall_dsc d then term2str (d $ e_listReal)

     else if is_booll_dsc d then term2str (d $ e_listBool)

     else term2str d

   | comp_dts'' (d,ts) = term2str (d $ (comp_ts (d, ts)))

        handle _ => error ("comp_dts'': "^(term2str d)^

 				" $ "^(term2str (hd ts))); 

 (* this may decompose an object-language isa-list;

    use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)

 fun dest_list' t = if is_list t then isalist2list t  else [t];

 (*fun is_metavar (Free (str, _)) =

     if (last_elem o Symbol.explode) str = "_" then true else false

   | is_metavar _ = false;*)

 fun is_var (Free _) = true

   | is_var _ = false;

 (*.special handling for lists. ?WN:14.5.03 ??!?*)

 fun dest_list (d,ts) = 

   let fun dest t = 

     if is_list_dsc d andalso not (is_unl d) 

       andalso not (is_var t) (*..for pbt*)

       then isalist2list t  else [t]

   in (flat o (map dest)) ts end;

 (*.decompose an input into description, terms (ev. elems of lists),

     and the value for the problem-environment; inv to comp_dts .*)

 (*WN.8.6.03: corrected with minimal effort,

 fn : theory -> term ->

      term *       description

      term list *  lists decomposed for elementwise input

      term list    pbl_ids not _HERE_: dont know which list-elems input*)

 fun split_dts (t as d $ arg) =

       if is_dsc d then

         if is_list_dsc d andalso is_list arg andalso is_unl d |> not then

           (d, take_apart arg) else

           (d, [arg]) else

         (e_term, dest_list' t)

   | split_dts t =

       let val t' as (h, _) = strip_comb t;

       in if is_dsc h then

         (h, dest_list t') else

         (e_term, dest_list' t)

       end;

 (* tests see fun comp_dts 

 > val t = str2term "someList []";

 > val (_,ts) = split_dts thy t; tracing (terms2str ts);

 ["[]"]

 > val t = str2term "valuesFor []";

 > val (_,ts) = split_dts thy t; tracing (terms2str ts);

 ["[]"]*)

 (*.version returning ts only.*)

 fun split_dts' (d, arg) = 

     if is_dsc d

     then if is_list_dsc d

 	 then if is_list arg

 	      then if is_unl d

 		   then ([arg])                 (*e.g. someList [1,3,2]*)

 		   else (take_apart arg)(*[a,b] --> SML[ [a], [b] ]SML*)

 	      else ([arg])      (*a variable or metavariable for a list*)

 	 else ([arg])

     else (dest_list' arg(*9.01 ???*))

   | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*)

   let val (h,argl) = strip_comb t

   in if (not o is_dsc) h then (dest_list' t)

      else (dest_list (h,argl))

   end;

 (*27.8.01: problem-environment

 WN.6.5.03: FIXXME reconsider if penv is worth the effort --

            -- just rerun a whole expl with num/var may show the same ?!

 WN.9.5.03: penv-concept stalled, immediately generate script env !

            but [#0, epsilon] only outcommented for eventual reconsideration  

 *)

 type penv = (term     (*err_*)

 	     * (term list)  (*[#0, epsilon] 9.5.03 outcommented*)

 	     ) list;

 fun pen2str ctxt (t, ts) =

     pair2str (term_to_string'  ctxt t, 

       (strs2str' o map (term_to_string'  ctxt)) ts);

 fun penv2str_ thy (penv:penv) = (strs2str' o (map (pen2str thy))) penv;

 (*

   9.5.03: still unused, but left for eventual future development*)

 type envv = (int * penv) list; (*over variants*)

 (*. 14.9.01: not used after putting penv-values into itm_

       make the result of split_* a value of problem-environment .*)

 fun mkval dsc [] = error "mkval called with []"

   | mkval dsc [t] = t

   | mkval dsc ts = list2isalist ((type_of o hd) ts) ts;

 (*WN.12.12.03*)

 fun mkval' x = mkval e_term x;

 (*. get the constant value from a penv .*)

 fun getval (id, values) = 

     case values of

 	[] => error ("penv_value: no values in '" ^ term2str id)

       | [v] => (id, v)

       | (v1::v2::_) => (case v1 of 

 			     Const ("Script.Arbfix",_) => (id, v2)

 			   | _ => (id, v1));

 (*

   val e_ = (term_of o the o (parse thy)) "e_::bool";

   val ev = (term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0";

   val v_ = (term_of o the o (parse thy)) "v_";

   val vv = (term_of o the o (parse thy)) "x";

   val r_ = (term_of o the o (parse thy)) "err_::bool";

   val rv1 = (term_of o the o (parse thy)) "#0";

   val rv2 = (term_of o the o (parse thy)) "eps";

   val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv;

   map getval penv;

 [(Free ("e_","bool"),

   Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")),

  (Free ("v_","RealDef.real"),Free ("x","RealDef.real")),

  (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list      

 *)

 (*==========================================================================

 23.3.02 TODO: ideas on redesign of type itm_,type item,type ori,type item ppc

 (1) kinds of itms:

   (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)

         =(presently) Mis (? should be Inc initially, and Mis after match_itms?)

   (1.2)  Syn,Typ,Sup: not related to oris

     Syn, Typ (presently) should be accepted in appl_add (instead Error')

     Sup      (presently) should be accepted in appl_add (instead Error')

          _could_ be w.r.t current vat (and then _is_ related to vat

     Mis should _not_ be  made Inc ((presently, by appl_add & match_itms)

 - dsc in itm_ is timeconsuming -- keep id for respective queries ?

 - order of items in ppc should be stable w.r.t order of itms

 - stepwise input of itms --- match_itms (in one go) ..not coordinated

   - unify code

   - match_itms / match_itms_oris ..2 versions ?!

     (fast, for refine / slow, for modeling)

 - clarify: efficiency <--> simplicity !!!

   ?: shift dsc itm_ -> itm | discard int in ori,itm | take int instead dsc 

     | take int for perserving order of item ppc in itms 

     | make all(!?) handling of itms stable against reordering(?)

     | field in ori ?? (not from fmz!) -- meant for efficiency (not doc!???)

       -"- "#undef" ?= not touched ?= (id,..)

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

 27.3.02:

 def: type pbt = (field, (dsc, pid)) *** design considerations ***

 (1) fmz + pbt -> oris

 (2) input + oris -> itm

 (3) match_itms      : schnell(?) f"ur refine

     match_itms_oris : r"uckmeldung f"ur item ppc

 (1.1) in oris fehlt daher pid: (i,v,f,d,ts,pid)

 ---------- ^^^^^ --- dh. pbt meist als argument zu viel !!!

 (3.1) abwarten, wie das matchen mehr unterschiedlicher pbt's sich macht;

       wenn Problem pbt v"ollig neue, dann w"are eigentlich n"otig ????:

       (a) (_,_,d1,ts,_):ori + pbt -> (i,vt,d2,ts,pid)  dh.vt neu  ????

       (b) 

 ==========================================================================*)

 (*the internal representation of a models' item

   4.9.01: not consistent:

   after Init_Proof 'Inc', but after copy_probl 'Mis' - for same situation

   (involves 'is_error');

   bool in itm really necessary ???*)

 datatype itm_ = 

     Cor of (term *              (* description *)

 	    (term list)) *      (* for list: elem-wise input *) 

 	   (*split_dts <-> comp_dts*)

 	   (term * (term list)) (* elem of penv *)

 	 (*9.5.03:  ---- is already for script -- penv delayed to future*)

   | Syn of cterm'

   | Typ of cterm'

   | Inc of (term * (term list))	* (term * (term list)) (*lists,

 				+ init_pbl WN.11.03 FIXXME: empty penv .. bad

                                 init_pbl should return Mis !!!*)

   | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)

   | Mis of (term * term)        (* after re-specification pbt-item not found 

                                    in pbl: only dsc, pid_*)

   | Par of cterm';  (*internal state from fun parsitm*)

 type vats = int list;      (*variants in formalizations*)

 (*.data-type for working on pbl/met-ppc: 

    in pbl initially holds descriptions (only) for user guidance.*)

 type itm = 

   int *        (* id  =0 .. untouched - descript (only) from init 

 		  23.3.02: seems to correspond to ori (fun insert_ppc)

 		           <> maintain order in item ppc?*)

   vats *       (* variants - copy from ori *)

   bool *       (* input on this item is not/complete *)

   string *     (* #Given | #Find | #Relate *)

   itm_;        (*  *)

 (* use"ME/sequent.sml";

    *)

 val e_itm = (0,[],false,"e_itm",Syn"e_itm"):itm;

 (*in CalcTree/Subproblem an 'untouched' model is created

   FIXME.WN.9.03 model should be filled to 'untouched' by Model/Refine_Problem*)

 fun untouched (itms: itm list) = 

     foldl and_ (true ,map ((curry op= 0) o #1) itms);

 (*> untouched [];

 val it = true : bool

 > untouched [e_itm];

 val it = true : bool

 > untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")];

 val it = false : bool*)

 (* find most frequent variant v in itms *)

 fun vts_in itms = (distinct o flat o (map #2)) (itms:itm list);

 fun cnt itms v = (v,(length o (filter (curry op= v)) o 

 		     flat o (map #2)) (itms:itm list));

 fun vts_cnt vts itms = map (cnt itms) vts;

 fun max2 [] = error "max2 of []"

   | max2 (y::ys) =

   let fun mx (a,x) [] = (a,x)

 	| mx (a,x) ((b,y)::ys) = 

     if x < y then mx (b,y) ys else mx (a,x) ys;

 in mx y ys end;

 (*. find the variant with most items already input .*)

 fun max_vt itms = 

     let val vts = (vts_cnt (vts_in itms)) itms;

     in if vts = [] then 0 else (fst o max2) vts end;

 (* TODO ev. make more efficient by avoiding flat *)

 fun mk_e (Cor (_, iv)) = [getval iv]

   | mk_e (Syn _) = []

   | mk_e (Typ _) = [] 

   | mk_e (Inc (_, iv)) = [getval iv]

   | mk_e (Sup _) = []

   | mk_e (Mis _) = [];

 fun mk_en vt ((i,vts,b,f,itm_):itm) =

     if member op = vts vt then mk_e itm_ else [];

 (*. extract the environment from an item list; 

     takes the variant with most items .*)

 fun mk_env itms = 

     let val vt = max_vt itms

     in (flat o (map (mk_en vt))) itms end;

 (*. example as provided by an author, complete w.r.t. pbt specified 

     not touched by any user action                                 .*)

 type ori = (int *      (* id: 10.3.00ff impl. only <>0 .. touched 

 			  21.3.02: insert_ppc needs it ! ?:purpose maintain

 				   order in item ppc ???*)

 	    vats *     (* variants 21.3.02: related to pbt..discard ?*)

 	    string *   (* #Given | #Find | #Relate 21.3.02: discard ?*)

 	    term *     (* description *)

 	    term list  (* isalist2list t | [t] *)

 	    );

 val e_ori_ = (0,[],"",e_term,[e_term]):ori;

 val e_ori = (0,[],"",e_term,[e_term]):ori;

 fun ori2str ((i,vs,fi,t,ts):ori) = 

     "("^(string_of_int i)^", "^((strs2str o (map string_of_int)) vs)^", "^fi^","^

     (term2str t)^", "^((strs2str o (map term2str)) ts)^")";

 val oris2str = 

     let (*val s = !show_types

 	val _ = show_types:= true*)

 	val str = (strs2str' o (map (linefeed o ori2str)))

 	(*val _ = show_types:= s*)

     in str end;

 (*.an or without leading integer.*)

 type preori = (vats *  

 	       string *   

 	       term *     

 	       term list);

 fun preori2str ((vs,fi,t,ts):preori) = 

     "("^((strs2str o (map string_of_int)) vs)^", "^fi^", "^

     (term2str t)^", "^((strs2str o (map term2str)) ts)^")";

 val preoris2str = (strs2str' o (map (linefeed o preori2str)));

 (*. given the input value (from split_dts)

     make the value in a problem-env according to description-type .*)

 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)

 fun pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) v =

     if is_list v 

     then [v]         (*eg. [r=Arbfix]*)

     else (case v of  (*eg. eps=#0*)

 	      (Const ("HOL.eq",_) $ l $ r) => [r,l]

 	    | _ => error ("pbl_ids Tools.nam: no equality " ^ term_to_string'  ctxt v))

   | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.una",_)]))) v = [v]

   | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) v = [v]

   | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.str",_)]))) v = [v]

   | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) v = [v] 

   | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))v = [v] 

   | pbl_ids ctxt (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))v = [v] 

   | pbl_ids ctxt _ v = 

     error ("pbl_ids: not implemented for " ^ term2str v);

 (*

 val t as t1 $ t2 = str2term "antiDerivativeName M_b";

 pbl_ids ctxt t1 t2;

   val t = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";

   val (d,argl) = strip_comb t;

   is_dsc d;                      (*see split_dts*)

   dest_list (d,argl);

   val (_ $ v) = t;

   is_list v;

   pbl_ids ctxt d v;

 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $

        (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..

   val (dsc,vl) = (split_dts o term_of o the o (parse thy)) "solveFor x";

 val dsc = Const ("Descript.solveFor","RealDef.real => Tools.una") : term

 val vl = Free ("x","RealDef.real") : term 

   val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";

   pbl_ids ctxt dsc vl;

 val it = [Free ("x","RealDef.real")] : term list

   val (dsc,vl) = (split_dts o term_of o the o(parse thy))

 		       "errorBound (eps=#0)";

   val (dsc,id) = (split_did o term_of o the o(parse thy)) "errorBound err_";

   pbl_ids ctxt dsc vl;

 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list     *)

 (*. given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))

     make the value in a problem-env according to description-type .*)

 (*28.8.01: .nam and .una impl. properly, others copied .. TODO*)

 fun pbl_ids' (Const(_,Type("fun",[_,Type("Tools.nam",_)]))) vs =

     (case vs of 

 	 [] => error ("pbl_ids' Tools.nam called with []")

        | [t] => (case t of  (*eg. eps=#0*)

 		     (Const ("HOL.eq",_) $ l $ r) => [r,l]

 		   | _ => 

                      error ("pbl_ids' Tools.nam: no equality " ^ term2str t))

        | vs' => vs (*14.9.01: ???TODO *))

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs 

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreall",_)])))vs = vs 

   | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unknown",_)])))vs = vs 

   | pbl_ids'  _ vs = 

     error ("pbl_ids': not implemented for " ^ terms2str vs);

 (*9.5.03 penv postponed: pbl_ids'*)

 fun pbl_ids' d vs = [comp_ts (d, vs)];

 (*14.9.01: not used after putting values for penv into itm_

   WN.5.5.03: used in upd .. upd_envv*)

 fun upd_penv ctxt penv dsc (id, vl) =

 (tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

  tracing"### upd_penv used !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!";

   overwrite (penv, (id, pbl_ids ctxt dsc vl))

 );

 (* 

   val penv = [];

   val (dsc,vl) = (split_did o term_of o the o (parse thy)) "solveFor x";

   val (dsc,id) = (split_did o term_of o the o (parse thy)) "solveFor v_";

   val penv = upd_penv thy penv dsc (id, vl);

 [(Free ("v_","RealDef.real"),

   [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])]

 : (term * term list) list                                                     

   val (dsc,vl) = (split_did o term_of o the o(parse thy))"errorBound (eps=#0)";

   val (dsc,id) = (split_did o term_of o the o(parse thy))"errorBound err_";

   upd_penv thy penv dsc (id, vl);

 [(Free ("v_","RealDef.real"),

   [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]),

  (Free ("err_","bool"),

   [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])]

 : (term * term list) list    ^.........!!!!

 *)

 (*WN.9.5.03: not reconsidered; looks strange !!!*)

 fun upd thy envv dsc (id, vl) i =

     let val penv = case assoc (envv, i) of

 		       SOME e => e

 		     | NONE => [];

         val penv' = upd_penv thy penv dsc (id, vl);

     in (i, penv') end;

 (*

   val i = 2;

   val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

   val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";

   val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";

   upd thy envv dsc (id, vl) i;

 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])

   : int * (term * term list) list*)

 (*14.9.01: not used after putting pre-penv into itm_*)

 fun upd_envv thy (envv:envv) (vats:vats) dsc id vl  =

     let val vats = if length vats = 0 

 		   then (*unknown id to _all_ variants*)

 		       if length envv = 0 then [1]

 		       else (intsto o length) envv 

 		   else vats

 	fun isin vats (i,_) = member op = vats i;

 	val envs_notin_vat = filter_out (isin vats) envv;

     in ((map (upd thy envv dsc (id, vl)) vats) @ envs_notin_vat):envv end;

 (*

   val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv;

   val vats = [2] 

   val (dsc,vl) = (split_did o term_of o the o(parse thy))"boundVariable b";

   val (dsc,id) = (split_did o term_of o the o(parse thy))"boundVariable v_";

   val envv = upd_envv thy envv vats dsc id vl;

 val envv = [(2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])])]

   : (int * (term * term list) list) list

   val vats = [1,2,3];

   val (dsc,vl) = (split_did o term_of o the o(parse thy))"maximum A";

   val (dsc,id) = (split_did o term_of o the o(parse thy))"maximum m_";

   upd_envv thy envv vats dsc id vl;

 [(1,[(Free ("m_","bool"),[Free ("A","bool")])]),

  (2,

   [(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")]),

    (Free ("m_","bool"),[Free ("A","bool")])]),

  (3,[(Free ("m_","bool"),[Free ("A","bool")])])]

 : (int * (term * term list) list) list

   val env = []:envv;

   val (d,ts) = (split_dts o term_of o the o (parse thy))

 		   "fixedValues [r=Arbfix]";

   val (_,id) = (split_did o term_of o the o (parse thy))"fixedValues fix_";

   val vats = [1,2,3];

   val env = upd_envv thy env vats d id (mkval ts);

 *)

 (*. update envv by folding from a list of arguments .*)

 fun upds_envv thy envv [] = envv

   | upds_envv thy envv ((vs, dsc, id, vl)::ps) = 

     upds_envv thy (upd_envv thy envv vs dsc id vl) ps;

 (* eval test-maximum.sml until Specify_Method ...

   val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];

   val met = (#ppc o get_met) mI;

   val envv = [];

   val eargs = flat eargs;

   val (vs, dsc, id, vl) = hd eargs;

   val envv = upds_envv thy envv [(vs, dsc, id, vl)];

   val (vs, dsc, id, vl) = hd (tl eargs);

   val envv = upds_envv thy envv [(vs, dsc, id, vl)];

   val (vs, dsc, id, vl) = hd (tl (tl eargs));

   val envv = upds_envv thy envv [(vs, dsc, id, vl)];

   val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));

   val envv = upds_envv thy envv [(vs, dsc, id, vl)];

 [(1,

   [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),

    (Free ("m_","bool"),[Free (#,#)]),

    (Free ("vs_","bool List.list"),[# $ # $ Const #]),

    (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),

  (2,

   [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),

    (Free ("m_","bool"),[Free (#,#)]),

    (Free ("vs_","bool List.list"),[# $ # $ Const #]),

    (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]),

  (3,

   [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),

    (Free ("m_","bool"),[Free (#,#)]),

    (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)

 (*for _output_ of the items of a Model*)

 datatype item = 

     Correct of cterm' (*labels a correct formula (type cterm')*)

   | SyntaxE of string (**)

   | TypeE   of string (**)

   | False   of cterm' (*WN050618 notexistent in itm_: only used in Where*)

   | Incompl of cterm' (**)

   | Superfl of string (**)

   | Missing of cterm';

 fun item2str (Correct  s) ="Correct " ^ s

   | item2str (SyntaxE  s) ="SyntaxE " ^ s

   | item2str (TypeE    s) ="TypeE " ^ s

   | item2str (False    s) ="False " ^ s

   | item2str (Incompl  s) ="Incompl " ^ s

   | item2str (Superfl  s) ="Superfl " ^ s

   | item2str (Missing  s) ="Missing " ^ s;

 (*make string for error-msgs*)

 fun itm_2str_ ctxt (Cor ((d,ts), penv)) = 

     "Cor " ^ term_to_string'  ctxt (comp_dts (d,ts)) ^ " ," ^ pen2str ctxt penv

   | itm_2str_ ctxt (Syn c) = "Syn " ^ c

   | itm_2str_ ctxt (Typ c) = "Typ " ^ c

   | itm_2str_ ctxt (Inc ((d,ts), penv)) = 

     "Inc " ^ term_to_string'  ctxt (comp_dts (d,ts)) ^ " ," ^ pen2str ctxt penv

   | itm_2str_ ctxt (Sup (d,ts)) = 

     "Sup " ^ term_to_string'  ctxt (comp_dts (d,ts))

   | itm_2str_ ctxt (Mis (d,pid)) = 

     "Mis "^ term_to_string'  ctxt d ^ " " ^ term_to_string'  ctxt pid

   | itm_2str_ ctxt (Par s) = "Trm "^s;

 fun itm_2str t = itm_2str_ (thy2ctxt' "Isac") t;

 fun itm2str_ ctxt ((i,is,b,s,itm_):itm) = 

     "("^(string_of_int i)^" ,"^(ints2str' is)^" ,"^(bool2str b)^" ,"^

     s^" ,"^(itm_2str_ ctxt itm_)^")";

 fun itms2str_ ctxt itms = strs2str' (map (linefeed o (itm2str_ ctxt)) itms);

 fun w_itms2str_ ctxt itms = tracing (itms2str_ ctxt itms);

 fun init_item str = SyntaxE str;

 type 'a ppc = 

     {Given : 'a list,

      Where: 'a list,

      Find  : 'a list,

      With : 'a list,

      Relate: 'a list};

 fun ppc2str {Given=Given,Where=Where,Find=Find,With=With,Relate=Relate}=

     ("{Given =" ^ (strs2str Given ) ^

      ",Where=" ^ (strs2str Where) ^

      ",Find  =" ^ (strs2str Find  ) ^

      ",With =" ^ (strs2str With ) ^

      ",Relate=" ^ (strs2str Relate) ^ "}");

 fun item_ppc ({Given = gi,Where= wh,

 		 Find = fi,With = wi,Relate= re}: string ppc) =

   {Given = map init_item gi,Where= map init_item wh,

    Find = map init_item fi,With = map init_item wi,

    Relate= map init_item re}:item ppc;

 fun itemppc2str ({Given=Given,Where=Where,

 		 Find=Find,With=With,Relate=Relate}:item ppc)=

     ("{Given =" ^ ((strs2str' o (map item2str))	 Given ) ^

      ",Where=" ^ ((strs2str' o (map item2str))	 Where) ^

      ",Find  =" ^ ((strs2str' o (map item2str))	 Find  ) ^

      ",With =" ^ ((strs2str' o (map item2str))	 With ) ^

      ",Relate=" ^ ((strs2str' o (map item2str))	 Relate) ^ "}");

 fun de_item (Correct x) = x

   | de_item (SyntaxE x) = x

   | de_item (TypeE   x) = x

   | de_item (False   x) = x

   | de_item (Incompl x) = x

   | de_item (Superfl x) = x

   | de_item (Missing x) = x;

 val empty_ppc ={Given = [],

 		Where= [],

 		Find  = [], 

 		With = [],

 		Relate= []}:item ppc;

 val empty_ppc_ct' ={Given = [],

 		Where = [],

 		Find  = [], 

 		With  = [],

 		Relate= []}:cterm' ppc;

 datatype match = 

   Matches of pblID * item ppc

 | NoMatch of pblID * item ppc;

 fun match2str (Matches (pI, ppc)) = 

     "Matches ("^(strs2str pI)^", "^(itemppc2str ppc)^")"

   | match2str(NoMatch (pI, ppc)) = 

     "NoMatch ("^(strs2str pI)^", "^(itemppc2str ppc)^")";

 fun matchs2str ms = (strs2str o (map match2str)) ms;

 fun pblID_of_match (Matches (pI,_)) = pI

   | pblID_of_match (NoMatch (pI,_)) = pI;

 (*10.03 for Refine_Problem*)

 datatype match_ = 

   Match_ of pblID * ((itm list) * ((bool * term) list))

 | NoMatch_;

 (*. the refined pbt is the last_element Matches in the list .*)

 fun is_matches (Matches _) = true

   | is_matches _ = false;

 fun matches_pblID (Matches (pI,_)) = pI;

 fun refined ms = ((matches_pblID o the o (find_first is_matches) o rev) ms)

     handle _ => []:pblID;

 fun refined_IDitms ms = ((find_first is_matches) o rev) ms;

 (*. the refined pbt is the last_element Matches in the list,

     for Refine_Problem, tryrefine .*)

 fun is_matches_ (Match_ _) = true

   | is_matches_ _ = false;

 fun refined_ ms = ((find_first is_matches_) o rev) ms;

 fun ts_in (Cor ((_,ts),_)) = ts

   | ts_in (Syn  (c)) = []

   | ts_in (Typ  (c)) = []

   | ts_in (Inc ((_,ts),_)) = ts

   | ts_in (Sup (_,ts)) = ts

   | ts_in (Mis _) = [];

 (*WN050629 unused*)

 fun all_ts_in itm_s = (flat o (map ts_in)) itm_s;

 val unique = (term_of o the o (parse (Thy_Info.get_theory "Real"))) "UnIqE_tErM";

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

   | d_in (Syn  (c)) = (tracing("*** d_in: Syn ("^c^")"); unique)

   | d_in (Typ  (c)) = (tracing("*** d_in: Typ ("^c^")"); unique)

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

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

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

 fun dts2str (d,ts) = pair2str (term2str d, terms2str ts);

 fun penvval_in (Cor ((d,_),(_,ts))) = [comp_ts (d,ts)]

   | penvval_in (Syn  (c)) = (tracing("*** penvval_in: Syn ("^c^")"); [])

   | penvval_in (Typ  (c)) = (tracing("*** penvval_in: Typ ("^c^")"); [])

   | penvval_in (Inc (_,(_,ts))) = ts

   | penvval_in (Sup dts) = (tracing("*** penvval_in: Sup "^(dts2str dts)); [])

   | penvval_in (Mis (d,t)) = (tracing("*** penvval_in: Mis "^

 				      (pair2str(term2str d, term2str t))); []);

 (*. check a predicate labelled with indication of incomplete substitution;

 rls ->    (*for eval_true*)

 bool * 	  (*have _all_ variables(Free) from the model-pattern 

             been substituted by a value from the pattern's environment ?*)

 term (*the precondition*)

 ->

 bool * 	  (*has the precondition evaluated to true*)

 term (*the precondition (for map)*)

 .*)

 fun evalprecond prls (false, pre) = 

   (*NOT ALL Free's have been substituted, eg. because of incomplete model*)

     (false, pre)

   | evalprecond prls (true, pre) =

 (* val (prls, pre) = (prls, hd pres');

    val (prls, pre) = (prls, hd (tl pres'));

    *)

     if eval_true (assoc_thy "Isac") (*for Pattern.match   *)

 		 [pre] prls             (*pre parsed, prls.thy*)

     then (true , pre)

     else (false , pre);

 fun pre2str (b, t) = pair2str(bool2str b, term2str t);

 fun pres2str pres = strs2str' (map (linefeed o pre2str) pres);

 (* check preconditions, return true if all true *)

 fun check_preconds' _ [] _ _ = []  (*empty preconditions are true*)

   | check_preconds' prls pres pbl _(*FIXME.WN0308 mvat re-introduce*) =

     let val env = mk_env pbl;

         val pres' = map (subst_atomic_all env) pres;

     in map (evalprecond prls) pres' end;

 fun check_preconds thy prls pres pbl = 

     check_preconds' prls pres pbl (max_vt pbl);

 fun declare_constraints' ts ctxt =

       fold Variable.declare_constraints (flat (map vars ts)) ctxt;

 (*WN110613 fun declare_constraints' shall replace fun declare_constraints*)

 fun declare_constraints t ctxt =

     let

       fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of

               (_, _::_) => (Free (v,T)::get_vars vs)

             | (_, []  ) => get_vars vs) (*filter out nums as long as 

                                           we have Free ("123",_)*)

         | get_vars [] = [];

       val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;

     in fold Variable.declare_constraints ts ctxt end;

 structure Context_Data = Proof_Data

   (type T = term list

    fun init _ = []);

 fun get_assumptions ctxt = Context_Data.get ctxt

 fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs))

 (* transfer assumptions from one to another ctxt.

    does NOT respect scope: in a calculation identifiers are unique.

    but environments are scoped as usual in Luacs-interpretation.

    WN110520 redo (1) take declare_constraints (2) with combinators*)

 fun transfer_asms_from_to from_ctxt to_ctxt =

   let

     val to_vars = get_assumptions to_ctxt |> map vars |> flat

     fun transfer [] to_ctxt = to_ctxt

         | transfer (from_asm::fas) to_ctxt =

             if inter op = (vars from_asm) to_vars = []

             then transfer fas to_ctxt

             else transfer fas (insert_assumptions [from_asm] to_ctxt)

   in transfer (get_assumptions from_ctxt) to_ctxt end

 (* exported from a subproblem to the context of the calling method:

    # 'scrval': the result of script interpretation and

    # those assumptions in the subproblem wich contain a variable known

      in the calling method. *)

 fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt =

   let val caller_ctxt = (scrval |> dest_list' |> insert_assumptions) caller_ctxt

   in transfer_asms_from_to sub_ctxt caller_ctxt end;

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

 end

 open SpecifyTools;

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