(* Title:  Specify/specification.sml

   Author: Walther Neuper, 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>

  interpret 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, interpret 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, interpret 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.

*)

signature SPECIFICATION =

sig

  type T = Specification_Def.T

(*val reset: Calc.T -> Calc.T*)

  val reset_calchead: Calc.T -> Calc.T

(*val get: Calc.T -> T*)

  val get_ocalhd: Calc.T -> T

(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)

  val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool

(*val is_complete: Calc.T -> bool*)

  val is_complete_mod: Calc.T -> bool

(*/------- to Specify from Specification -------\* )

(*val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->

    Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input*)

  val nxt_spec: Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->

    Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input

(*val do_all : Calc.T -> Calc.T*)

  val all_modspec: Calc.T -> Calc.T 

(*val finish_phase: Calc.T -> Calc.T*)

  val complete_mod: Calc.T -> Calc.T

(*val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option*)

  val nxt_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (string * string) option

(*val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post*)

  val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post

(*val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post*)

  val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post

( *\------- to Specify from Specification -------/*)

(*/------- to P_Model from Specification -------\*)

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

  val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input

  val mk_additem: string -> TermC.as_string -> Tactic.input

(*\------- to P_Model from Specification -------/*)

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

  (*NONE*)

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

  val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context

  val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T

( *\--- ! 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: I_Model.single -> bool

  val is_list_type: typ -> bool

  val parse_ok: I_Model.feedback list -> bool

  val all_dsc_in: I_Model.feedback list -> term list

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

  val is_complete_modspec: Calc.T -> bool

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

    (string * Pos.pos' * term) list

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

    (string * Pos.pos' * term) list

end

(**)

structure Specification(** ): SPECIFICATION( **) =

struct

(**)

type T = Specification_Def.T;

(* is the calchead complete ? *)

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

  foldl and_ (true, map #3 (its: I_Model.T)) andalso 

  foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso 

  dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty

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

    | _ => raise ERROR "different variants in formalization"

  end

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

  | is_list_type _ = false

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

      | d_in (I_Model.Syn _) = []

      | d_in (I_Model.Typ _) = []

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

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

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

      | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)

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

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

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

  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (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, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))

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

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

  | is_untouched _ = false

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

   (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_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 = (I_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, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))

      | _ => NONE

    end

  | nxt_add thy oris _ itms =

    let

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

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

      fun test_id ids r = member op= ids (#1 (r : O_Model.single))

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

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

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

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

        | false_and_not_Sup _ = false

      val v = if itms = [] then 1 else I_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 => raise 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_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)

  | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)

  | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)

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

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

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

  | mk_additem "#Relate"ct = Tactic.Add_Relation ct

  | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"")

(*/------- to Specify from Specification -------\*)

(* 

  TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met

   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 Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) = 

    (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')

     else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')

     else

       case find_first (I_Model.is_error o #5) pbl of

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

	         (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)

	     | NONE => 

	       (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of

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

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

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

	          else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')

		        else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')

		        else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')

		        else

			        case find_first (I_Model.is_error o #5) met of

			          SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)

			        | NONE => 

			          (case nxt_add (ThyC.get_theory dI) oris mpc met of

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

				        | NONE => (Pos.Met, Tactic.Apply_Method mI))))

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

    (case find_first (I_Model.is_error o #5) met of

      SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)

    | NONE => 

      case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of

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

      | NONE => 

	      (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')

	       else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')

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

		     else (Pos.Met, Tactic.Apply_Method mI)))

  | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)

(*\------- to Specify from Specification -------/*)

(* output the headline to a ppc *)

fun header p_ pI mI =

  case p_ of

    Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI) 

	| Pos.Met => Test_Out.Method mI

	| pos => raise ERROR ("header called with "^ Pos.pos_2str pos)

fun make m_field (term_as_string, i_model) =

  case m_field of

    "#Given" => Tactic.Add_Given' (term_as_string, i_model)

  | "#Find" => Tactic.Add_Find' (term_as_string, i_model)

  | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)

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

fun get (pt, (p, _)) =

  case Ctree.get_obj I pt p of

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

      => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)

  | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";

fun specify_additem sel ct (pt, pos as (p, Pos.Met)) = 

      let

        val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)

        val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI

        val cpI = if pI = Problem.id_empty then pI' else pI

        val cmI = if mI = Method.id_empty then mI' else mI

        val {ppc, pre, prls, ...} = Method.from_store cmI

      in 

        case I_Model.check_single ctxt sel oris met ppc ct of

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

    	      let

              val met' = I_Model.add_single thy itm met

    	        val (p, pt') =

    	         case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of

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

    	        | _ => raise ERROR "specify_additem: uncovered case of generate1"

    	        val pre' = Pre_Conds.check' thy prls pre met'

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

    	        val (p_, _) =

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

    	            ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);

    	      in 

              ("ok", ([], [], (pt', (p, p_))))

            end

        | I_Model.Err msg =>

    	      let

              val pre' = Pre_Conds.check' thy prls pre met

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

    	        val (p_, _) =

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

    	            ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);

    	      in

              (msg, ([], [], (pt, (p, p_))))

    	      end

      end

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

      let

        val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)

        val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI

        val cpI = if pI = Problem.id_empty then pI' else pI

        val cmI = if mI = Method.id_empty then mI' else mI

        val {ppc, where_, prls, ...} = Problem.from_store cpI

      in

        case I_Model.check_single ctxt sel oris pbl ppc ct of

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

	          let

	            val pbl' = I_Model.add_single thy itm pbl

	            val (p, pt') =

	              case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

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

  	            | _ => raise ERROR "specify_additem: uncovered case of Specify_Step.add"

(* only for getting final p_ ..*)

	            val pre = Pre_Conds.check' thy prls where_ pbl';

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

	            val (p_, _) =

	              nxt_spec Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);

	          in

              ("ok", ([], [], (pt', (p, p_))))

            end

        | I_Model.Err msg =>

	          let

              val pre = Pre_Conds.check' thy prls where_ pbl

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

	            val (p_, _(*Tactic.input*)) =

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

	                (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)

	          in

            (msg, ([], [], (pt, (p, p_))))

	          end

      end

(*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, Pos.Pbl))) = 

    let

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

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

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

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

      val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;

      val cpI = if pI = Problem.id_empty then pI' else pI;

    in

      case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of

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

	        let

	          val pbl' = I_Model.add_single thy itm pbl

	          val (tac, tac_) = case sel of

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

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

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

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

		        val (p, c, pt') =

		          case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

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

  		        | _ => raise ERROR "nxt_specif_additem: uncovered case generate1"

	        in

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

          end	       

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

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

	        ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),

	          (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp) 

    end

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

    let

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

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

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

      | _ => raise ERROR "nxt_specif_additem Met: uncovered case get_obj"

      val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;

      val cmI = if mI = Method.id_empty then mI' else mI;

    in 

      case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of

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

	        let

	          val met' = I_Model.add_single thy itm met;

	          val (tac,tac_) = case sel of

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

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

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

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

	          val (p, c, pt') =

	            case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of

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

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

	        in

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

	        end

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

    end

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

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

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

fun tag_form thy (formal, given) =

 (let

    val gf = (head_of given) $ formal;

    val _ = Thm.global_cterm_of thy gf

  in gf end)

  handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^

    " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")

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

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

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

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

  let

    val _ = if p_ <> Pos.Pbl 

	    then raise ERROR ("###complete_mod: only impl.for Pbl, called with " ^ Pos.pos'2str pos)

	    else ()

	  val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of

	    Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)

	  | _ => raise ERROR "complete_mod: unvered case get_obj"

  	val (_, pI, mI) = References.select ospec spec

  	val mpc = (#ppc o Method.from_store) mI

  	val ppc = (#ppc o Problem.from_store) pI

  	val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)

    val pt = Ctree.update_pblppc pt p pits

	  val pt = Ctree.update_metppc pt p mits

  in (pt, (p, Pos.Met)) end

(* do all specification in one single step:

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

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

*)

fun all_modspec (pt, (p, _)) =

  let

    val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of

      Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}

        => (pors, dI, pI, mI)

    | _ => raise ERROR "all_modspec: uncovered case get_obj"

	  val {ppc, ...} = Method.from_store mI

    val (_, vals) = O_Model.values' pors

	  val ctxt = ContextC.initialise dI vals

    val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),

      map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)

  in

    (pt, (p, Pos.Met))

  end

(*/------- to I_Model from Specification -------\* )

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

fun is_complete_mod_ [] = false

  | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))

( *\------- to I_Model from Specification -------/*)

fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =

    if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 

    then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p

    else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)

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

    if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 

    then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p

    else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)

  | is_complete_mod (_, pos) =

    raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")

fun is_complete_modspec ptp = is_complete_mod ptp andalso References.are_complete ptp

(** get the formula from a ctree-node **)

(*

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

  take res from all other PrfObj's

  Designed for interSteps, outcommented 04 in favour of calcChangedEvent

*)

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

    [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]

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

    [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]

  | formres _ _ = raise ERROR "formres: uncovered definition" 

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

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

  | form _ _ = raise ERROR "form: uncovered definition" 

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

fun get_formress fs _ [] = flat fs

  | get_formress fs p (nd::nds) =

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

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

and get_forms fs _ [] = flat fs

  | get_forms fs p (nd::nds) =

    if Ctree.is_pblnd nd

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

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

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

    (* continue with trying 'res' only*)

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

(* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)

fun get_ocalhd (pt, (p, Pos.Pbl)) = 

    let

	    val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of

	      Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)

	    | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"

      val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))

      val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl

    in

      (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)

    end

  | get_ocalhd (pt, (p, Pos.Met)) = 

    let

		  val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of

		    Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)

		  | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"

      val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))

      val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth

    in

      (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)

    end

  | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"

(* at the activeFormula set the Specification 

   to empty and return a CalcHead;

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

fun reset_calchead (pt, (p,_)) = 

  let

    val () = case Ctree.get_obj I pt p of

      Ctree.PblObj _ => ()

    | _ => raise ERROR "reset_calchead: uncovered case get_obj"

    val pt = Ctree.update_pbl pt p []

    val pt = Ctree.update_met pt p []

    val pt = Ctree.update_spec pt p References.empty

  in (pt, (p, Pos.Pbl)) end

(**)end(**)