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

  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.

#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'

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

    (string * (term * 'a)) list * (string * (term * 'b)) list -> Spec.T -> Pos.pos_ * Tactic.input

  val reset_calchead : Calc.T -> Calc.T

  val get_ocalhd : Calc.T -> Ctree.ocalhd

  val ocalhd_complete : I_Model.T -> (bool * term) list -> ThyC.id * Problem.id * Method.id -> bool

  val all_modspec : Calc.T -> Calc.T 

  val complete_metitms : O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T

  val insert_ppc' : I_Model.single -> I_Model.T -> I_Model.T

  val complete_mod : Calc.T -> Calc.T

  val is_complete_mod : Calc.T -> bool

  val complete_spec : Calc.T -> Calc.T

  val is_complete_spec : Calc.T -> bool

  val some_spec : Spec.T -> Spec.T -> Spec.T

  (* these could go to Ctree ..*)

  val show_pt : Ctree.ctree -> unit

  val show_pt_tac : Ctree.ctree -> unit

  val pt_extract : Calc.T -> Ctree.ptform * Tactic.input option * term list 

  val get_interval : Pos.pos' -> Pos.pos' -> int -> Ctree.ctree -> (Pos.pos' * term * Tactic.input option) list

  val match_ags : theory -> Model_Pattern.T -> term list -> O_Model.T

  val match_ags_msg : Problem.id -> term -> term list -> unit

  val oris2fmz_vals : O_Model.T -> string list * term list

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

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

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

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

  val nxt_add: theory -> O_Model.T -> (string * (term * 'a)) list -> (int * Model_Def.variants * bool * string * I_Model.feedback) list -> (string * string) option

  val is_error: I_Model.feedback -> bool

  val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * I_Model.T -> I_Model.T * I_Model.T

  val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'

  val vals_of_oris : O_Model.T -> term list

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

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

  val e_calcstate : Calc.T * State_Steps.T

  val e_calcstate' : calcstate'

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

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

  val postermtacs2str: (Pos.pos' * term * Tactic.input option) list -> string

  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: Model_Pattern.T -> O_Model.single -> I_Model.single

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

  val mtc: theory -> Model_Pattern.single -> term -> O_Model.preori option

  val cpy_nam: Model_Pattern.T -> O_Model.preori list -> Model_Pattern.single -> O_Model.preori

  val get: Calc.T -> I_Model.T * O_Model.T * ThyC.id * Spec.id * Spec.id *

        I_Model.T * ThyC.id * Spec.id * Spec.id * Proof.context

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

  val insert_ppc: theory -> I_Model.single -> I_Model.T -> I_Model.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 chk_vars : term Model.ppc -> string * term list

  val unbound_ppc : term Model.ppc -> term list

  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 Chead(** ): CALC_HEAD( **) =

struct

(**)

(** datatypes **)

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

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

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

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

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

   because the tacis hold enough information for efficiently rebuilding

   this state just by "fun generate "

*)

type calcstate = 

  Calc.T *      (* the calc-state to which the tacis could be applied *)

  State_Steps.T (* ev. several (hidden) steps; 

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

val e_calcstate = ((Ctree.EmptyPtree, Pos.e_pos'), [State_Steps.single_empty]);

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

  State_Steps.T * (* cas. several (hidden) steps;

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

  Pos.pos' list *     (* a "continuous" sequence of pos', deleted by application of taci list *)     

  Calc.T          (* the calc-state resulting from the application of tacis               *)

val e_calcstate' = ([State_Steps.single_empty], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos')) : calcstate';

(* 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: (bool * term) list)) andalso 

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

(* ["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) = 

	  ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts) 

	  handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts)

  in (split_list o (map ori2fmz_vals)) oris end

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

fun seek_ppc _ [] = NONE

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

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

fun is_error (I_Model.Cor _) = false

  | is_error (I_Model.Sup _) = false

  | is_error (I_Model.Inc _) = false

  | is_error (I_Model.Mis _) = false

  | is_error _ = true

(* 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 => 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 (Specify.itm_out thy itm_)

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

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

  | mk_delete _ str _ = 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 _ = 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' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')

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

     else

       case find_first (is_error o #5) pbl of

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

	         (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') => (Pbl, mk_additem fd ct')

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

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

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

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

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

		        else

			        case find_first (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 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 (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') => (Met, mk_additem fd ct')

      | NONE => 

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

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

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

		     else (Met, Tactic.Apply_Method mI)))

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

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

	    Input_Descript.split' (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): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"

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

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

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

	        ^ "*** checked by theory: " ^ Context.theory_name 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" ^ UnparseC.term 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 '" ^ Model_Pattern.to_string 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) = Input_Descript.join'''' (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 "^ UnparseC.term 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 = O_Model.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 " ^ Model_Pattern.to_string pats ^ "\n"

       ^ "*** stac   '" ^ UnparseC.term stac ^ "' has the ...\n"

       ^ "*** arg-list " ^ UnparseC.terms 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: " ^ (I_Model.feedback_to_string (ThyC.to_ctxt 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 = I_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 ((I_Model.d_in o #5) itm)) ppc' end

fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_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 = Problem.id_empty then [] else pI) 

	   | Met => Generate.Method mI

	   | pos => 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, 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, ...} = Specify.get_met cmI

      in 

        case I_Model.add_single ctxt sel oris met ppc ct of

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

    	      let

              val met' = insert_ppc thy itm met

    	        val (p, pt') =

    	         case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Met)) 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_spec Met pb oris (dI',pI',mI') (pbl,met') 

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

    	      in 

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

            end

        | I_Model.Err msg =>

    	      let

              val pre' = Stool.check_preconds thy prls pre met

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

    	        val (p_, _) =

    	          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

              (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, ...} = Specify.get_pbt cpI

      in

        case I_Model.add_single ctxt sel oris pbl ppc ct of

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

	          let

	            val pbl' = insert_ppc thy itm pbl

	            val (p, pt') =

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

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

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

(* only for getting final p_ ..*)

	            val pre = Stool.check_preconds 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 Specify.get_met) cmI) (dI, pI, mI);

	          in

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

            end

        | I_Model.Err msg =>

	          let

              val pre = Stool.check_preconds 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 Specify.get_met) 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, 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)

      | _ => 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.add_single ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of

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

	        let

	          val pbl' = insert_ppc 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 => error ("nxt_specif_additem: uncovered case of" ^ sel)

		        val (p, c, pt') =

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

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

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

	        in

	          ([(tac, tac_, ((p, Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, 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, 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)

      | _ => 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.add_single ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of

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

	        let

	          val met' = insert_ppc 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 => error ("nxt_specif_additem Met: uncovered case of" ^ sel)

	          val (p, c, pt') =

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

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

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

	        in

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

	        end

      | I_Model.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.pos'2str p)

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

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

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

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

(* filter out oris which have same description in itms *)

fun filter_outs oris [] = oris

  | filter_outs oris (i::itms) = 

    let

      val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris

    in

      filter_outs ors itms

    end

(* filter oris which are in pbt, too *)

fun filter_pbt oris pbt =

  let

    val dscs = map (fst o snd) pbt

  in

    filter ((member op= dscs) o (#4)) oris

  end

(* combine itms from pbl + met and complete them wrt. pbt *)

(* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)

fun complete_metitms oris pits mits met = 

  let

    val vat = I_Model.max_vt pits;

    val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)

    val ors = filter ((member_swap op= vat) o (#2)) oris

    val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)

  in

    itms @ (map (ori2Coritm met) os)

  end

(* complete model and guard of a calc-head *)

fun complete_mod_ (oris, mpc, ppc, probl) =

  let

    val pits = filter_out ((curry op= false) o (#3)) probl

    val vat = if probl = [] then 1 else I_Model.max_vt probl

    val pors = filter ((member_swap op = vat) o (#2)) oris

    val pors = filter_outs pors pits (*which are in pbl already*)

    val pors = (filter_pbt pors ppc) (*which are in pbt, too*)

    val pits = pits @ (map (ori2Coritm ppc) pors)

    val mits = complete_metitms oris pits [] mpc

  in (pits, mits) end

fun some_spec (odI, opI, omI) (dI, pI, mI) =

  (if dI = ThyC.id_empty then odI else dI,

   if pI = Problem.id_empty then opI else pI,

   if mI = Method.id_empty then omI else mI)

(* get the values from oris; handle the term list w.r.t. penv *)

fun vals_of_oris (oris: O_Model.T) =

  ((map (Model.mkval' o (#5))) o 

    (filter ((member_swap op= 1) o (#2)))) oris

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

(* check pbltypes, announces one failure a time *)

fun chk_vars ctppc = 

  let

    val {Given = gi, Where = wh, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc TermC.vars ctppc)

    val chked = subtract op = gi wh

  in

    if chked <> [] then ("wh\\gi", chked)

    else

      let val chked = subtract op = (union op = gi fi) re

      in

        if chked  <> []

	      then ("re\\(gi union fi)", chked)

	      else ("ok", []) 

      end

  end

(* check a new pbltype: variables (Free) unbound by given, find*) 

fun unbound_ppc ctppc =

  let

    val {Given = gi, Find = fi, Relate = re, ...} = Specify.appc flat (Specify.mappc TermC.vars ctppc)

  in

    distinct (subtract op = (union op = gi fi) re)

  end

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

	  | _ => error "complete_mod: unvered case get_obj"

  	val (_, pI, mI) = some_spec ospec spec

  	val mpc = (#ppc o Specify.get_met) mI

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

  	val (pits, mits) = complete_mod_ (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, ...} = Specify.get_met mI

    val (_, vals) = oris2fmz_vals pors

	  val ctxt = ContextC.initialise dI vals

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

      map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)

  in

    (pt, (p, Pos.Met))

  end

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

fun is_complete_mod_ [] = false

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

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

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

    then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p

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

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

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

    then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p

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

  | is_complete_mod (_, pos) =

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

(* have (thy, pbl, met) _all_ been specified explicitly ? *)

fun is_complete_spec (pt, pos as (p, _)) = 

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

  then error ("is_complete_spec: called by PrfObj at " ^ Pos.pos'2str pos)

  else

    let val (dI,pI,mI) = Ctree.get_obj Ctree.g_spec pt p

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

(* complete empty items in specification from origin (pbl, met ev.refined);

   assumes 'is_complete_mod' *)

fun complete_spec (pt, pos as (p, _)) = 

  let

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

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

    | _ => error "complete_spec: uncovered case get_obj"

    val pt = Ctree.update_spec pt p (some_spec ospec spec)

  in

    (pt, pos)

  end

fun is_complete_modspec ptp = is_complete_mod ptp andalso is_complete_spec ptp

fun pt_model (Ctree.PblObj {meth, spec, origin = (_, spec', hdl), ...}) Met =

    let

      val (_, _, metID) = Ctree.get_somespec' spec spec'

	    val pre = if metID = Method.id_empty then []

	      else

	        let

	          val {prls, pre= where_, ...} = Specify.get_met metID

	          val pre = Stool.check_preconds' prls where_ meth 0

		      in pre end

	    val allcorrect = is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))

    in

      Ctree.ModSpec (allcorrect, Met, hdl, meth, pre, spec)

    end

  | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ...}) _(*Frm,Pbl*) =

    let

      val (_, pI, _) = Ctree.get_somespec' spec spec'

      val pre = if pI = Problem.id_empty then []

	      else

	        let

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

	          val pre = Stool.check_preconds' prls where_ probl 0

	        in pre end

	    val allcorrect = is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))

    in

      Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, pre, spec)

    end

  | pt_model _ _ = error "pt_model: uncovered definition"

fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form

  | pt_form (Ctree.PblObj {probl, spec, origin = (_, spec', _), ...}) =

    let

      val (dI, pI, _) = Ctree.get_somespec' spec spec'

      val {cas, ...} = Specify.get_pbt pI

    in case cas of

      NONE => Ctree.Form (Auto_Prog.pblterm dI pI)

    | SOME t => Ctree.Form (subst_atomic (I_Model.mk_env probl) t)

    end

(* pt_extract returns

      # the formula at pos

      # the tactic applied to this formula

      # the list of assumptions generated at this formula

	(by application of another tac to the preceding formula !)

   pos is assumed to come from the frontend, ie. generated by moveDown.

   Notes: cannot be in ctree.sml, because ModSpec has to be calculated. 

   TODO 110417 get assumptions from ctxt !?

*)

fun pt_extract (pt, ([], Res)) =

    (* WN120512: returns Check_Postcondition WRONGLY see --- build fun is_exactly_equal *)

    let

      val (f, asm) = Ctree.get_obj Ctree.g_result pt []

    in (Ctree.Form f, NONE, asm) end

  | pt_extract (pt,(p,Res)) =

    let

      val (f, asm) = Ctree.get_obj Ctree.g_result pt p

      val tac =

        if Ctree.last_onlev pt p

        then

          if Ctree.is_pblobj' pt (Pos.lev_up p)

          then

            let

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

                Ctree.PblObj{spec = (_, pI, _), ...} => pI

              | _ => error "pt_extract last_onlev: uncovered case get_obj"

            in if pI = Problem.id_empty then NONE else SOME (Tactic.Check_Postcond pI) end

		      else SOME Tactic.End_Trans (* WN0502 TODO for other branches *)

		    else

		      let val p' = Pos.lev_on p

		      in

		        if Ctree.is_pblobj' pt p'

		        then

		          let

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

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

		            | _ => error "pt_extract \<not>last_onlev: uncovered case get_obj"

		          in SOME (Tactic.Subproblem (dI, pI)) end

		        else

		          if f = Ctree.get_obj Ctree.g_form pt p'

		          then SOME (Ctree.get_obj Ctree.g_tac pt p') (*because this Frm ~~~is not on worksheet*)

		          else SOME (Tactic.Take (UnparseC.term (Ctree.get_obj Ctree.g_form pt p')))

		      end

    in (Ctree.Form f, tac, asm) end

  | pt_extract (pt, (p,p_(*Frm,Pbl*))) =

      let

        val ppobj = Ctree.get_obj I pt p

        val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p

        val tac = Ctree.g_tac ppobj

      in (f, SOME tac, []) end

(** 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 _ _ = error "formres: uncovered definition" 

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

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

  | form _ _ = 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 an 'interval' 'from' 'to' of formulae from a ctree **)

(* WN0401 this functionality belongs to ctree.sml *)

fun eq_pos' (p1, Frm) (p2, Pos.Frm) = p1 = p2

  | eq_pos' (p1, Res) (p2, Pos.Res) = p1 = p2

  | eq_pos' (p1, Pbl) (p2, p2_) =

    p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)

  | eq_pos' (p1, Met) (p2, p2_) =

    p1 = p2 andalso (case p2_ of Pbl => true | Met => true | _ => false)

  | eq_pos' _ _ = false;

(* get an 'interval' from the ctree; 'interval' is w.r.t. the 

   total ordering Position#compareTo(Position p) in the java-code

val get_interval = fn :

      pos' ->     : from is "move_up 1st-element" to return

      pos' -> 	  : to the last element to be returned; from < to

      int -> 	    : level: 0 gets the flattest sub-tree possible, 999 the deepest

      ctree -> 	  : 

      (pos' * 	  : of the formula

       Term.term) : the formula

	  list                                                           *)

fun get_interval from to level pt =

  let

    fun get_inter c (from) (to) lev pt =

	    if eq_pos' from to orelse from = ([], Pos.Res)

	    then

	      let val (f, tacopt, _) = pt_extract (pt, from)

	      in case f of

	        Ctree.ModSpec (_, _, headline, _, _, _) => c @ [(from, headline, NONE)] 

	      | Ctree.Form t => c @ [(from, t, tacopt)]

	      end

	    else 

	      if lev < Pos.lev_of from

	      then (get_inter c (Ctree.move_dn [] pt from) to lev pt)

		      handle (Ctree.PTREE _(*from move_dn too far*)) => c

		    else

		      let

		        val (f, tacopt, _) = pt_extract (pt, from)

		        val term = case f of

		          Ctree.ModSpec (_,_,headline,_,_,_) => headline

				    | Ctree.Form t => t

		      in (get_inter (c @ [(from, term, tacopt)]) (Ctree.move_dn [] pt from) to lev pt)

		        handle (Ctree.PTREE _(*from move_dn too far*)) => c @ [(from, term, tacopt)]

		      end

  in get_inter [] from to level pt end

fun posterm2str (pos, t, _) = "(" ^ Pos.pos'2str pos ^ ", " ^ UnparseC.term t ^ ")"

fun posterms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posterm2str)) pfs

fun postermtac2str (pos, t, SOME tac) =

      Pos.pos'2str pos ^ ", " ^ UnparseC.term t ^ "\n" ^ indent 10 ^ Tactic.input_to_string tac

  | postermtac2str (pos, t, NONE) =

      Pos.pos'2str pos ^ ", " ^ UnparseC.term t

fun postermtacs2str pfts = (strs2str' o (map (curry op ^ "\n")) o (map postermtac2str)) pfts

(* WN050225 omits the last step, if pt is incomplete *)

fun show_pt pt = tracing (posterms2str (get_interval ([], Pos.Frm) ([], Pos.Res) 99999 pt))

fun show_pt_tac pt = tracing (postermtacs2str (get_interval ([], Pos.Frm) ([], Pos.Res) 99999 pt))

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

fun get_ocalhd (pt, (p, 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)

	    | _ => error "get_ocalhd Pbl: uncovered case get_obj"

      val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))

      val pre = Stool.check_preconds (ThyC.get_theory "Isac_Knowledge") prls where_ probl

    in