(* Title: calchead.sml

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

          most important types are declared in Selem and Stool (mstools.sml).

          TODO: allocate elements of structure Selem and of structure Stool appropriately.

   Author: Walther Neuper 991122, Mathias Lehnfeld

   (c) due to copyright terms

*)

(* Survey on type fmz_ .. type ori .. type itm (in probl, meth) .. formal args of root-/SubProblem

   and relations between respective list elements:                                       #1#

                  fmz      =             [ dsc $ v......................................(dsc $ v)..]

root problem on pos = ([], _)            

                  fmz_     =             [(dsc, v).......................................(dsc, v)..]

                  \<down>                                                                       

                  oris     =             [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)...........(dsc, v)..]

                  \<down>                       #Given,..,#Relate  #Find     #undef............#undef   \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

  Specify_Problem + pbl.ppc=             [(dsc,id)..(dsc,id),(dsc,id)]  \<down>                 \<down>       \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

                  itms     =             [(dsc, v)..(dsc, v),(dsc, v)]  \<down>                 \<down>       \<down>

  int.modelling                           +Cor ++++++++++Cor +Cor       \<down>                 \<down>       \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

  Specify_Method  + met.ppc=             [(dsc,id)..(dsc,id),(dsc,id)]  \<down>                 \<down>       \<down>

                  \<down>                                                     \<down>                 \<down>       \<down>

                  itms     =             [(dsc, v)..(dsc, v),(dsc, v),(dsc, v)..(dsc, v)] \<down>       \<down>

  int.modelling                                                       +Cor ++++++Cor      \<down>       \<down>

                  form.args=             [ id ..... id      , ///////  id ....... id    ] \<down>       \<down>

                  env =                  [(id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>

  interprete code env = [(id, v)..(id, v),(id, v)..(id, v)  , /////// (id, v)....(id, v)] \<down>       \<down>

    ..extends env       ^^^^^^^^^^^^^^^^   \<down>                           \<down>   \<down>              \<down>       \<down>

                                   \<down>       \<down>                           \<down>   \<down>              \<down>       \<down>

SubProblem on pos = ([2], _)       \<down>       \<down>                           \<down>   \<down>              \<down>       \<down>

                  form.args=      [id ................................ id ]\<down>              \<down>       \<down>

                  \<down>                REAL..BOOL..                            \<down>              \<down>       \<down>

                  \<down>                                                        \<down>              \<down>       \<down>

                  + met.ppc=      [(dsc,id).......................(dsc,id)]\<down>              \<down>       \<down>

                                    \<down>                               \<down>      \<down>              \<down>       \<down>

                  oris     =      [(dsc, v)...................... (dsc,   v) ........... (dsc, v)]\<down>

  Specify_Problem, int.modelling, Specify_Method, interprete code as above                 #1#    \<down>

                                                                                                  \<down>

SubProblem on pos = ([3, 4], _)                                                                   \<down>

                  form.args=              [id ...................... id ]                         \<down>

                  \<down>                        REAL..BOOL..                                           \<down>

                  + met.ppc=              [(dsc,id).............(dsc,id)]                         \<down>

                  oris     =              [(dsc, v).............(dsc, v)...................(dsc, v)] 

  Specify_Problem, int.modelling, Specify_Method, interprete code as above                    #1#

Notes:

(1) SubProblem implements sub-function calls such, that the arguments (+ pre- + post-condition)

    of the functions become concern of interactive modelling.

(2) In Isac-terms, the above concerns the phases of modelling and 

    and of specifying (Specify_Problem, Specify_Method),

    while stepwise construction of solutions is called solving.

    The latter is supported by Lucas-Interpretation of the functions' body.

(3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;

    it is as complete as possible (this has been different up to now).

(4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input.

(5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,

    add them to the model-pattern of met and let this input be done automatically;

    respective items must be in fmz.

#1# fmz contains items, which are stored in oris of the root(!)-problem.

    This allows to specify methods, which require more input as anticipated

    in writing partial_functions: such an item can be fetched from the root-problem's oris.

    A candidate for this situation is "errorBound" in case an equation cannot be solved symbolically

    and thus is solved numerically.

#2# TODO

*)

signature CALC_HEAD =

sig

  type calcstate

  type calcstate'

  datatype appl = Appl of Tac.tac_ | Notappl of string

  val nxt_specify_init_calc : Selem.fmz -> calcstate

  val specify : Tac.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->

    Ctree.pos' * (Ctree.pos' * Selem.istate) * Generate.mout * Tac.tac * Selem.safe * Ctree.ctree

  val nxt_specif : Tac.tac -> Ctree.state -> calcstate'

  val nxt_spec : Ctree.pos_ -> bool -> Model.ori list -> Celem.spec -> Model.itm list * Model.itm list ->

    (string * (term * 'a)) list * (string * (term * 'b)) list -> Celem.spec -> Ctree.pos_ * Tac.tac

  val reset_calchead : Ctree.state -> Ctree.state

  val get_ocalhd : Ctree.state -> Ctree.ocalhd

  val ocalhd_complete : Model.itm list -> (bool * term) list -> Rule.domID * Celem.pblID * Celem.metID -> bool

  val all_modspec : Ctree.state -> Ctree.state 

  val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem.pat list -> Model.itm list

  val insert_ppc' : Model.itm -> Model.itm list -> Model.itm list

  val complete_mod : Ctree.state -> Ctree.state

  val is_complete_mod : Ctree.state -> bool

  val complete_spec : Ctree.state -> Ctree.state

  val is_complete_spec : Ctree.state -> bool

  val some_spec : Celem.spec -> Celem.spec -> Celem.spec

  (* these could go to Ctree ..*)

  val show_pt : Ctree.ctree -> unit

  val show_pt_tac : Ctree.ctree -> unit

  val pt_extract : Ctree.state -> Ctree.ptform * Tac.tac option * term list 

  val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term * Tac.tac option) list

  val match_ags : theory -> Celem.pat list -> term list -> Model.ori list

  val match_ags_msg : Celem.pblID -> term -> term list -> unit

  val oris2fmz_vals : Model.ori list -> string list * term list

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

  val is_known : Proof.context -> string -> Model.ori list -> term -> string * Model.ori * term list

  val is_notyet_input : Proof.context -> Model.itm list -> term list -> Model.ori -> ('a * (term * term)) list

    -> string * Model.itm

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

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val e_calcstate : Ctree.state * Generate.taci list

  val e_calcstate' : calcstate'

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

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

  val postermtacs2str : (pos' * term * Tac.tac option) list -> string

  val vals_of_oris : Model.ori list -> term list

  val is_error : Model.itm_ -> bool

  val is_copy_named_idstr : string -> bool

  val is_copy_named_generating_idstr : string -> bool

  val is_copy_named_generating : 'a * ('b * term) -> bool

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

  val ori2Coritm : Celem.pat list -> Model.ori -> Model.itm

  val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list

  val mtc : theory -> Celem.pat -> term -> Model.preori option

  val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori

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

  val appl_add: Proof.context -> string -> Model.ori list ->

    Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm

  val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option

  val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

(*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)

  val variants_in : term list -> int

  val is_untouched : Model.itm -> bool

  val is_list_type : typ -> bool

  val parse_ok : Model.itm_ list -> bool

  val all_dsc_in : Model.itm_ list -> term list

  val chktyps : theory -> term list * term list -> term list (* only in old tests*)

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

  val unbound_ppc : term Model.ppc -> term list

  val nxt_model_pbl : Tac.tac_ -> Ctree.state -> Tac.tac_

  val is_complete_modspec : Ctree.state -> bool

  val get_formress : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->

    (string * Ctree.pos' * term) list

  val get_forms : (string * Ctree.pos' * term) list list -> Ctree.pos -> Ctree.ctree list ->

    (string * Ctree.pos' * term) list

end

structure Chead(**): CALC_HEAD(**) =

struct

open Ctree

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

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

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

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

val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]);

(*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' = 

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

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

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

(* is the calchead complete ? *)

fun ocalhd_complete its pre (dI, pI, mI) = 

  foldl and_ (true, map #3 (its: Model.itm list)) andalso 

  foldl and_ (true, map #1 (pre: (bool * term) list)) andalso 

  dI <> Rule.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID

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

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

fun oris2fmz_vals oris =

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

	  ((Rule.term2str o Model.comp_dts') (dsc, ts), last_elem ts) 

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

  in (split_list o (map ori2fmz_vals)) oris end

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

   'type-less' usually is illtyped                                  *)

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

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

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

  | typeless (Bound i) = (Bound i)

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

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

(* 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 ('" ^

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

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

      [])

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

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

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

    else seek_oridts ctxt sel (d, ts) oris

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

fun seek_orits ctxt _ ts [] = 

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

    "') not found in oris (typed)", Model.e_ori, [])

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

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

    then

      if sel = sel' 

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

      else (((strs2str' o map (Rule.term_to_string' ctxt)) ts) ^ " not for " ^ sel, Model.e_ori, [])

    else seek_orits ctxt sel ts oris

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

fun seek_ppc _ [] = NONE

  | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc

datatype appl =

  Appl of Tac.tac_      (* tactic is applicable at a certain position in the Ctree *)

| Notappl of string     (* tactic is NOT applicable                                *)

fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =

  gis @ whs @ fis @ wis @ 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 _ [] _ 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 _  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

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

  | is_list_type _ = false

fun is_parsed (Model.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 (Model.Cor ((d, _), _)) = [d]

      | d_in (Model.Syn _) = []

      | d_in (Model.Typ _) = []

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

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

      | d_in (Model.Mis (d,_)) = [d]

      | d_in i = error ("all_dsc_in: uncovered case with " ^ Model.itm_2str i)

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

fun is_error (Model.Cor _) = false

  | is_error (Model.Sup _) = false

  | is_error (Model.Inc _) = false

  | is_error (Model.Mis _) = false

  | is_error _ = true

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

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

  (fd, ((Rule.term_to_string''' thy) o Model.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) (_, _, _, fd, itm_) =

  (fd, ((Rule.term_to_string''' thy) o Model.comp_dts) (d, subtract op = (Model.ts_in itm_) ts))

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

fun is_untouched (_, _, false, _, Model.Inc ((_, []), _)) = true

  | is_untouched _ = false

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

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

(*args of nxt_add

  thy : for?

  oris: from formalization 'type fmz', structured for efficient access 

  pbt : the problem-pattern to be matched with oris in order to get itms

  itms: already input items

*)

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

    let

      fun test_d d (i, _, _, _, itm_) = (d = (Model.d_in itm_)) andalso i <> 0

      fun is_elem itms (_, (d, _)) = 

        case find_first (test_d d) itms of SOME _ => true | NONE => false

    in

      case filter_out (is_elem itms) pbt of

        (f, (d, _)) :: _ => SOME (f, ((Rule.term_to_string''' thy) o Model.comp_dts) (d, []))

      | _ => NONE

    end

  | nxt_add thy oris _ itms =

    let

      fun testr_vt v ori = member op= (#2 (ori : Model.ori)) v andalso (#3 ori) <> "#undef"

      fun testi_vt v itm = member op= (#2 (itm : Model.itm)) v

      fun test_id ids r = member op= ids (#1 (r : Model.ori))

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

        (Model.d_in (#5 (itm: Model.itm))) = d andalso subset op = (Model.ts_in (#5 itm), ts)

      fun false_and_not_Sup (_, _, false, _, Model.Sup _) = false

        | false_and_not_Sup (_, _, false, _, _) = true

        | false_and_not_Sup _ = false

      val v = if itms = [] then 1 else Model.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

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

      else

        case find_first (test_subset (hd icl)) vors of

          NONE => error "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt"

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

    end

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

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

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

  | mk_delete _ str _ = error ("mk_delete: called with field \"" ^ str ^ "\"")

fun mk_additem "#Given" ct = Tac.Add_Given ct

  | mk_additem "#Find" ct = Tac.Add_Find ct    

  | mk_additem "#Relate"ct = Tac.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 (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) = 

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

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

     else

       case find_first (is_error o #5) pbl of

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

	         (Pbl, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)

	     | NONE => 

	       (case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl of

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

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

	          if not preok then (Pbl, Tac.Refine_Problem pI')

	          else if dI = Rule.e_domID then (Pbl, Tac.Specify_Theory dI')

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

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

		        else

			        case find_first (is_error o #5) met of

			          SOME (_, _, _, fd, itm_) => (Met, mk_delete (Celem.assoc_thy dI) fd itm_)

			        | NONE => 

			          (case nxt_add (Celem.assoc_thy dI) oris mpc met of

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

				        | NONE => (Met, Tac.Apply_Method mI))))

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

    (case find_first (is_error o #5) met of

      SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)

    | NONE => 

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

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

      | NONE => 

	      (if dI = Rule.e_domID then (Met, Tac.Specify_Theory dI')

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

		     else if not preok then (Met, Tac.Specify_Method mI)

		     else (Met, Tac.Apply_Method mI)))

  | nxt_spec p _ _ _ _ _ _ = error ("nxt_spec: uncovered case with " ^ pos_2str p)

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

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

  let 

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

    val pval = Model.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

      (Model.Cor _) => 

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

	       else (id, vt, complete, fd, Model.Cor ((d, ts'), (pid, pval))))

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

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

    | (Model.Inc _) =>

      if complete

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

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

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

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

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

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

    | (Model.Mis _) => (* 4.9.01: Model.Mis just copied *)

       if complete

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

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

    | i => error ("ori_2itm: uncovered case of "^ Model.itm_2str i)

  end

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

fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (Model.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 .*)

fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =

  case find_first (eq1 d) pbt of

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

      (case find_first (eq3 f d) itms of

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

          let val ts' = inter op = (Model.ts_in itm_) ts

          in 

            if subset op = (ts, ts') 

            then (((strs2str' o map (Rule.term_to_string' ctxt)) ts') ^ " already input", Model.e_itm) (*2*)

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

	          end

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

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

fun test_types ctxt (d,ts) =

  let 

    val opt = (try Model.comp_dts) (d, ts)

    val msg = case opt of 

      SOME _ => "" 

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

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

  in msg end

(* is the term t input (or taken from fmz) known in oris ?

   give feedback on all(?) strange input;

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

fun is_known ctxt sel ori t =

  let

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

    val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots

    val (d, ts) = Model.split_dts t

    val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)

  in

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

    then ("identifiers " ^ strs2str' (subtract op = oids ids) ^ " not in example", Model.e_ori, [])

    else 

	    if d = Rule.e_term 

	    then 

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

	      then ("terms '" ^ (strs2str' o (map (Rule.term_to_string' ctxt))) ts ^

		      "' not in example (typeless)", Model.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, Model.e_ori, []))

		       | (msg, _, _) => (msg, Model.e_ori, []))

	    else 

	      if member op = (map #4 ori) d

	      then seek_oridts ctxt sel (d, ts) ori

	      else (Rule.term_to_string' ctxt d ^ " not in example", (0, [], sel, d, ts), [])

  end

datatype additm =

	Add of Model.itm   (* return-value of appl_add *)

| Err of string       (* error-message            *)

(* add an item to the model; check wrt. oris and pbt.

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

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

fun appl_add ctxt sel [] ppc pbt ct =

    let

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

      in 

        case TermC.parseNEW ctxt ct of

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

        | SOME t =>

            let val (d, ts) = Model.split_dts t

            in 

              if d = Rule.e_term 

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

              else

                (case find_first (eq1 d) pbt of

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

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

                     let fun eq2 d (i, _, _, _, itm_) = d = (Model.d_in itm_) andalso i <> 0

                     in case find_first (eq2 d) ppc of

                       NONE => Add (i, [], true, f,Model.Cor ((d, ts), (id, Model.pbl_ids' d ts)))

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

                         if LTool.is_list_dsc d 

                         then 

                           let

                             val in_itm = Model.ts_in itm_

                             val ts' = union op = ts in_itm

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

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

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

                     end)

            end

    end

  | appl_add ctxt sel oris ppc pbt str =

    case TermC.parseNEW ctxt str of

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

    | SOME t => 

        case is_known ctxt sel oris t of

          ("", ori', all) => 

            (case is_notyet_input ctxt ppc all ori' pbt of

               ("", itm) => Add itm

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

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

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

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

   of a SubProblem ? see calcelems.sml 'type met '                        *)

fun is_copy_named_idstr str =

  case (rev o Symbol.explode) str of

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

  | _ => false

fun is_copy_named (_, (_, t)) = (is_copy_named_idstr o TermC.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 TermC.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, _)) (ty $ var) =

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

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

	    Model.split_dts' (dsc, var))) (*: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): " ^ Rule.term2str dsc ^ " " ^ Rule.term2str var ^ "\n"

	        ^ "*** description: " ^ TermC.term_detail2str dsc

	        ^ "*** value: " ^ TermC.term_detail2str var

	        ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty

	        ^ "*** checked by theory: " ^ Rule.theory2str thy ^ "\n"

	        ^ "*** " ^ dots 66);

          writeln (@{make_string} e);

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

      NONE))

  | mtc _ _ t = error ("mtc: uncovered case with" ^ Rule.term2str t)

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

   precondition: copy-named vars are filtered out            *)

fun matc _ [] _ oris = oris

  | matc _ pbt [] _ =

    (tracing (dashs 70);

     error ("actual arg(s) missing for '" ^ Celem.pats2str pbt ^ "' i.e. should be 'copy-named' by '*_._'"))

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

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

    else(*..del?*)

      let val opt = mtc thy p a

      in

        case opt of

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

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

	 end

(* 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 oris (p as (field, (dsc, t))) =

  (if is_copy_named_generating p

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

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

       val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t

       val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t

       val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)

       val vals = map sel oris

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

     in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end

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

	) handle _ => error ("cpy_nam: for "^ Rule.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 then 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 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  (* cy is NOT a (formal) argument, but the fun's result *)

    val oris' = matc thy pbt' ags []

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

    val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)

  in (map flattup ors) end

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

fun match_ags_msg pI stac ags =

  let

    val pats = (#ppc o Specify.get_pbt) pI

    val msg = (dots 70 ^ "\n"

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

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

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

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

       ^ dashs 70)

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

  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_ (_, (_, 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 _ (_, _, _, _, itm_) [] =

        error ("overwrite_ppc: " ^ (Model.itm_2str_ (Rule.thy2ctxt thy) itm_) ^ " not found")

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

	      if (#1 itm) = (#1 p)

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

fun insert_ppc thy itm ppc =

  let 

    fun eq_untouched d (0, _, _, _, itm_) = (d = Model.d_in itm_)

      | eq_untouched _ _ = false

    val ppc' = case seek_ppc (#1 itm) ppc of

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

    | NONE => (ppc @ [itm])

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

fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (Model.d_in itm_ = Model.d_in iitm_)

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

   handles superfluous items carelessly                       *)

fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)

(* output the headline to a ppc *)

fun header p_ pI mI =

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

	   | Met => Generate.Method mI

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

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

    let

      val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of

        (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})

          => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)

  	  | _ => error "specify_additem: uncovered case of get_obj I pt p"

      val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI

      val cpI = if pI = Celem.e_pblID then pI' else pI

      val cmI = if mI = Celem.e_metID then mI' else mI

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

    in 

      case appl_add ctxt sel oris met ppc ct of

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

  	      let

            val met' = insert_ppc thy itm met

            val arg = case sel of

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

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

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

  		      | str => error ("specify_additem: uncovered case with " ^ str)

  	        val (p, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p, Met) pt of

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

  	        | _ => error "specify_additem: uncovered case of generate1"

  	        val pre' = Stool.check_preconds thy prls pre met'

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

  	        val (p_, nxt) =

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

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

  	      in ((p, p_), ((p, p_), Selem.Uistate),

  	        Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Selem.Safe, pt')

          end

      | Err msg =>

  	      let

            val pre' = Stool.check_preconds thy prls pre met

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

  	        val (p_, nxt) =

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

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

  	      in ((p,p_), ((p,p_),Selem.Uistate), Generate.Error' msg, nxt, Selem.Safe, pt) end

    end

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

      let

        val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of

          (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})

            => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)

  	    | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"

        val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI

        val cpI = if pI = Celem.e_pblID then pI' else pI

        val cmI = if mI = Celem.e_metID then mI' else mI

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

      in

        case appl_add ctxt sel oris pbl ppc ct of

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

	          let

	            val pbl' = insert_ppc thy itm pbl

              val arg = case sel of

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

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

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

  		        | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)

	            val (p, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p,Pbl) pt of

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

	            | _ => error "specify_additem: uncovered case of Generate.generate1"

	            val pre = Stool.check_preconds thy prls where_ pbl'

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

	            val (p_, nxt) =

	              nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)

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

	          in

	            ((p, p_), ((p, p_), Selem.Uistate),

	              Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Selem.Safe, pt')

            end

        | Err msg =>

	          let

              val pre = Stool.check_preconds thy prls where_ pbl

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

	            val (p_, nxt) =

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

	                (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)

	          in ((p, p_), ((p, p_), Selem.Uistate), Generate.Error' msg, nxt, Selem.Safe,pt) end

      end

fun specify (Tac.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ = 

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

      val thy = Celem.assoc_thy dI'

      val (oris, ctxt) = 

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

        then ([], Selem.e_ctxt)

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

      val (pt, _) = cappend_problem e_ctree [] (Selem.e_istate, ctxt) (fmz, spec')

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

      val pt = update_ctxt pt [] ctxt

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

    in 

      case mI' of

  	    ["no_met"] => 

  	      (([], Pbl), (([], Pbl), Selem.Uistate),

  	        Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),

  	        Tac.Refine_Tacitly pI', Selem.Safe, pt)

       | _ => 

  	      (([], Pbl), (([], Pbl), Selem.Uistate),

  	        Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),

  	        Tac.Model_Problem, Selem.Safe, pt)

    end

    (* ONLY for STARTING modeling phase *)

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

    let 

      val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of

        PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>

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

      | _ => error "specify (Model_Problem': uncovered case get_obj"

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

      val thy = Celem.assoc_thy thy'

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

      val pre = Stool.check_preconds thy prls where_ pbl

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

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

        Generate.generate1 thy (Tac.Model_Problem'([],pbl,met)) (Selem.Uistate, ctxt) pos pt

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

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

    in

      ((p, Pbl), ((p, p_), Selem.Uistate), 

      Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),

      nxt, Selem.Safe, pt)

    end

    (* called only if no_met is specified *)     

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

      let

        val (dI', ctxt) = case get_obj I pt p of

          PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)

        | _ => error "specify (Refine_Tacitly': uncovered case get_obj"

        val {met, thy,...} = Specify.get_pbt pIre

        val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)

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

	        Generate.generate1 thy (Tac.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Selem.Uistate, ctxt) pos pt

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

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

        Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (Celem.assoc_thy dI') pbl pre),

        Tac.Model_Problem, Selem.Safe, pt)

      end

  | specify (Tac.Refine_Problem' rfd) pos _ pt =

      let

        val ctxt = get_ctxt pt pos

        val (pos, _, _, pt) =

          Generate.generate1 (Celem.assoc_thy "Isac") (Tac.Refine_Problem' rfd) (Selem.Uistate, ctxt) pos pt

      in

        (pos(*p,Pbl*), (pos(*p,Pbl*), Selem.Uistate), Generate.RefinedKF rfd, Tac.Model_Problem, Selem.Safe, pt)

      end

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

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

      let

        val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of

          PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>

            (oris, dI', pI', mI', dI, mI, ctxt, met)

        | _ => error "specify (Specify_Problem': uncovered case get_obj"

        val thy = Celem.assoc_thy dI

        val (p, pt) =

          case  Generate.generate1 thy (Tac.Specify_Problem' (pI, (ok, (itms, pre)))) (Selem.Uistate, ctxt) pos pt of

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

          | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"

        val dI'' = Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)

        val mI'' = if mI = Celem.e_metID then mI' else mI

        val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,

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

      in

        ((p,Pbl), (pos,Selem.Uistate),

        Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),

        nxt, Selem.Safe, pt)

      end    

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

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

      let

        val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of

          PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>

             (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)

        | _ => error "specify (Specify_Problem': uncovered case get_obj"

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

        val thy = Celem.assoc_thy dI

        val dI'' = if dI = Rule.e_domID then dI' else dI

        val pI'' = if pI = Celem.e_pblID then pI' else pI

        val oris = Specify.add_field' thy ppc oris

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

        val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls) oris

(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)

val itms =

  if mI' = ["Biegelinien", "ausBelastung"]

  then itms @

    [(4, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else itms

(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)

        val (pos, _, _, pt) = 

	        Generate.generate1 thy (Tac.Specify_Method' (mID, oris, itms)) (Selem.Uistate, ctxt) pos pt

        val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms) 

		      ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)

      in

        (pos, (pos,Selem.Uistate),

        Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (Celem.assoc_thy dI'') itms pre'),

        nxt, Selem.Safe, pt)

      end    

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

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

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

  | specify (Tac.Specify_Theory' domID) (pos as (p,p_)) _ pt =

      let

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

        val thy = Celem.assoc_thy domID

        val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of

          PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>

             (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)

        | _ => error "specify (Specify_Theory': uncovered case get_obj"

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

        val cpI = if pI = Celem.e_pblID then pI' else pI

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

        val cmI = if mI = Celem.e_metID then mI' else mI

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

        val pre = case p_ of

          Met => (Stool.check_preconds thy mer mwh met)

        | _ => (Stool.check_preconds thy per pwh pbl)

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

      in

        if domID = dI

        then

          let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)

	        in

	          ((p, p_), (pos, Selem.Uistate), 

		        Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),

		        nxt, Selem.Safe, pt)

          end

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

	        let 

	          val ((p, p_), _, _, pt) = Generate.generate1 thy (Tac.Specify_Theory' domID) (Selem.Uistate, ctxt) (p,p_) pt

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

	        in

	          ((p,p_), (pos,Selem.Uistate), 

	          Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),

	          nxt, Selem.Safe, pt)

          end

      end

  | specify m' _ _ _ = error ("specify: not impl. for " ^ Tac.tac_2str m')

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

  -- for input from scratch*)

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

    let

      val (oris, dI', pI', dI, pI, pbl, ctxt) = case get_obj I pt p of

        PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>

           (oris, dI', pI', dI, pI, pbl, ctxt)

      | _ => error "specify (Specify_Theory': uncovered case get_obj"

      val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;

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

    in

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

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

	        let

	          val pbl' = insert_ppc thy itm pbl

	          val (tac, tac_) = case sel of

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

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

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

		        | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)

		        val (p, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p,Pbl) pt of

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

		        | _ => error "nxt_specif_additem: uncovered case generate1"

	        in

	          ([(tac, tac_, ((p, Pbl), (Selem.Uistate, ctxt)))], c, (pt', (p, Pbl)))

          end	       

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

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

	        ([(Tac.Tac msg, Tac.Tac_ (Rule.Thy_Info_get_theory "Isac", msg,msg,msg),

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

    end

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

    let

      val (oris, dI', mI', dI, mI, met, ctxt) = case get_obj I pt p of

        PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>

           (oris, dI', mI', dI, mI, met, ctxt)

      | _ => error "nxt_specif_additem Met: uncovered case get_obj"

      val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;

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

    in 

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

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

	        let

	          val met' = insert_ppc thy itm met;

	          val (tac,tac_) = case sel of

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

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

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

		        | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)

	          val (p, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p, Met) pt of

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

		        | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"

	        in

	          ([(tac, tac_, ((p, Met), (Selem.Uistate, ctxt)))], c, (pt', (p, Met)))

	        end

      | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)

    end

  | nxt_specif_additem _ _ (_, p) = error ("nxt_specif_additem not impl. for" ^ pos'2str p)

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

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

    handle _ => (i, v, true, f, Model.Cor ((d, ts), (d, ts)))

      (*dsc in oris, but not in pbl pat list: keep this dsc*)