(* Title: the calctree, which holds a calculation

   Author: Walther Neuper 1999

   (c) due to copyright terms

*)

signature BASIC_CALC_TREE =

sig (* vvv--- *.sml require these typs incrementally, with these exception -----------------vvv *)

  (*===\<Longrightarrow> other ?mstools.sml? =================================================================*)

  type scrstate

  datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate

  val istate2str : istate -> string

  val e_istate : istate

  type state

  type result

  type con

  type sube

  type subs

  type subte

  val sube2str : cterm' list -> string

  val sube2subst : theory -> cterm' list -> (term * term) list

  val sube2subte : cterm' list -> term list

  val subs2subst : theory -> cterm' list -> (term * term) list

  val subst2sube : (term * term) list -> cterm' list                       (* for datatypes.sml *)

  val subst2subs : (term * term) list -> cterm' list

  val subst2subs' : (term * term) list -> (string * string) list

  val subte2sube : term list -> cterm' list

  datatype tac_ =

    Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list

  | Apply_Assumption' of term list * term

  | Apply_Method' of metID * term option * istate * Proof.context

  | Begin_Sequ' | Begin_Trans' of term

  | Split_And' of term | Split_Or' of term | Split_Intersect' of term

  | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term

  | End_Sequ' | End_Trans' of result

  | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''

  | CAScmd' of term

  | Calculate' of theory' * string * term * (term * thm')

  | Check_Postcond' of pblID * result

  | Check_elementwise' of term * cterm' * result

  | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'

  | Derive' of rls

  | Detail_Set' of theory' * bool * rls * term * result

  | Detail_Set_Inst' of theory' * bool * subst * rls * term * result

  | End_Detail' of result

  | Empty_Tac_

  | Free_Solve'

  | Init_Proof' of cterm' list * spec

  | Model_Problem' of pblID * itm list * itm list

  | Or_to_List' of term * term

  | Refine_Problem' of pblID * (itm list * (bool * term) list)

  | Refine_Tacitly' of pblID * pblID * domID * metID * itm list

  | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result

  | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result

  | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result

  | Rewrite_Set' of theory' * bool * rls * term * result

  | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result

  | Specify_Method' of metID * ori list * itm list

  | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list))

  | Specify_Theory' of domID

  | Subproblem' of spec * ori list * term * Selem.fmz_ * Proof.context * term

  | Substitute' of rew_ord_ * rls * subte * term * term

  | Tac_ of theory * string * string * string

  | Take' of term | Take_Inst' of term

datatype tac =

    Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'

  | Apply_Assumption of cterm' list

  | Apply_Method of metID

  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)

  | Begin_Sequ | Begin_Trans

  | Split_And | Split_Or | Split_Intersect

  | Conclude_And | Conclude_Or | Collect_Trues

  | End_Sequ | End_Trans

  | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'

  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)

  | CAScmd of cterm'

  | Calculate of string

  | Check_Postcond of pblID

  | Check_elementwise of cterm'

  | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'

  | Derive of rls'

  | Detail_Set of rls'

  | Detail_Set_Inst of subs * rls'

  | End_Detail

  | Empty_Tac

  | Free_Solve

  | Init_Proof of cterm' list * spec

  | Model_Problem

  | Or_to_List

  | Refine_Problem of pblID

  | Refine_Tacitly of pblID

  | Rewrite of thm''

  | Rewrite_Asm of thm''

  | Rewrite_Inst of subs * thm''

  | Rewrite_Set of rls'

  | Rewrite_Set_Inst of subs * rls'

  | Specify_Method of metID

  | Specify_Problem of pblID

  | Specify_Theory of domID

  | Subproblem of domID * pblID

  | Substitute of sube

  | Tac of string

  | Take of cterm' | Take_Inst of cterm'

  val tac2str : tac -> string

  val rls_of : tac -> rls'                                                     (* for solve.sml *)

  val tac2IDstr : tac -> string

  val is_rewset : tac -> bool                                             (* for mathengine.sml *)

  val is_rewtac : tac -> bool                                              (* for interface.sml *)

  eqtype posel

  type pos = posel list

  val pos2str : int list -> string                                         (* for datatypes.sml *)

  datatype pos_ = Frm | Met | Pbl | Res | Und

  val pos_2str : pos_ -> string

  type pos'

  val pos'2str : pos' -> string

  val str2pos_ : string -> pos_                                            (* for datatypes.sml *)

  val e_pos' : pos'

  (* for generate.sml ?!? ca.*)

  datatype safe = Helpless | Safe | Sundef | Unsafe

  val tac_2str : tac_ -> string

  eqtype cellID

  datatype branch  = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB

  datatype ostate = Complete | Incomplete | Inconsistent

  datatype ppobj =

    PblObj of

     {branch: branch,

      cell: lrd option,

      loc: (istate * Proof.context) option * (istate * Proof.context) option,

      ostate: ostate,

      result: result,

      fmz: Selem.fmz,

      origin: ori list * spec * term,

      probl: itm list,

      meth: itm list,

      spec: spec,

      ctxt: Proof.context,

      env: (istate * Proof.context) option}

  | PrfObj of

     {branch: branch,

      cell: lrd option,

      loc: (istate * Proof.context) option * (istate * Proof.context) option,

      ostate: ostate,

      result: result,

      form: term,

      tac: tac}

  datatype ctree = EmptyPtree | Nd of ppobj * ctree list

  val e_ctree : ctree (* TODO: replace by EmptyPtree*)

  val existpt' : pos' -> ctree -> bool                                     (* for interface.sml *)

  val is_interpos : pos' -> bool                                           (* for interface.sml *)

  val lev_pred' : ctree -> pos' -> pos'                                    (* for interface.sml *)

  val ins_chn : ctree list -> ctree -> pos -> ctree                       (* for solve.sml *)

  val children : ctree -> ctree list                                           (* for solve.sml *)

  val get_nd : ctree -> pos -> ctree                                           (* for solve.sml *)

  val just_created_ : ppobj -> bool                                       (* for mathengine.sml *)

  val just_created : state -> bool                                 (* for mathengine.sml *)

  val e_origin : ori list * spec * term                                   (* for mathengine.sml *)

  val is_pblobj : ppobj -> bool

  val is_pblobj' : ctree -> pos -> bool

  val is_pblnd : ctree -> bool

  val g_spec : ppobj -> spec

  val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

  val g_form : ppobj -> term

  val g_pbl : ppobj -> itm list

  val g_met : ppobj -> itm list

  val g_metID : ppobj -> metID

  val g_result : ppobj -> result

  val g_tac : ppobj -> tac

  val g_domID : ppobj -> domID                           (* for appl.sml TODO: replace by thyID *)

  val g_env : ppobj -> (istate * Proof.context) option                          (* for appl.sml *)

  val g_origin : ppobj -> ori list * spec * term                              (* for script.sml *)

  val get_loc : ctree -> pos' -> istate * Proof.context                       (* for script.sml *)

  val get_istate : ctree -> pos' -> istate                                    (* for script.sml *)

  val get_ctxt : ctree -> pos' -> Proof.context

  val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a

  val get_curr_formula : state -> term

  val get_assumptions_ : ctree -> pos' -> term list                             (* for appl.sml *)

  val e_ctxt : Proof.context

  val is_e_ctxt : Proof.context -> bool                                         (* for appl.sml *)

  val new_val : term -> istate -> istate

  (* for calchead.sml *)

  type cid = cellID list

  type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

  datatype ptform = Form of term | ModSpec of ocalhd

  val get_somespec' : spec -> spec -> spec

  exception PTREE of string;

  val par_pbl_det : ctree -> pos -> bool * pos * rls                           (* for appl.sml *)

  val rule2tac : theory -> (term * term) list -> rule -> tac               (* for rewtools.sml *)

  val eq_tac : tac * tac -> bool                                             (* for script.sml *)

  val rootthy : ctree -> theory                                              (* for script.sml *)

(* ---- made visible ONLY for structure CTaccess : CALC_TREE_ACCESS --------------------------- *)

  val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree

  val existpt : pos -> ctree -> bool                                          (* also for tests *)

  val is_empty_tac : tac -> bool                                              (* also for tests *)

  val cut_tree : ctree -> pos * 'a -> ctree * pos' list                       (* also for tests *)

  val insert_pt : ppobj -> ctree -> int list -> ctree

(* ---- made visible ONLY for structure CTnavi : CALC_TREE_NAVIGATION ------------------------- *)

  val g_branch : ppobj -> branch

  val g_form' : ctree -> term

  val g_ostate : ppobj -> ostate

  val g_ostate' : ctree -> ostate

  val g_res : ppobj -> term

  val g_res' : ctree -> term 

(*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------

  val lev_on : CTbasic.pos -> CTbasic.pos                        (* duplicate in ctree-navi.sml *)

  val lev_dn : CTbasic.pos -> CTbasic.pos                        (* duplicate in ctree-navi.sml *)

  val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos   (* duplicate in ctree-navi.sml *)

   ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)

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

  val pr_ctree : (pos -> ppobj -> string) -> ctree -> string

  val pr_short : pos -> ppobj -> string

  val e_subs : string list

  val e_sube : cterm' list

  val g_ctxt : ppobj -> Proof.context

  val g_fmz : ppobj -> Selem.fmz

  val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list

  val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list

  val get_allpos' : pos * posel -> ctree -> pos' list

  val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list

  val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool

  val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list

  val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list

  val get_trace : ctree -> int list -> int list -> int list list

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

  val branch2str : branch -> string

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

end

(*

structure CTbasic :

sig exception PTREE of string val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree

  val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree

  datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB

  val branch2str : branch -> string eqtype cellID val children : ctree -> ctree list type cid = cellID list

  datatype con = land | lor datatype ctree = EmptyPtree | Nd of ppobj * ctree list

  val cut_bottom : int list * int -> ctree -> (ctree * (int list * pos_) list) * bool

  val cut_level :

     (posel list * pos_) list -> posel list -> ctree -> int list * pos_ -> ctree * (posel list * pos_) list

  val cut_level_'_ :

     (posel list * pos_) list -> posel list -> ctree -> int list * pos_ -> ctree * (posel list * pos_) list

  val cut_levup : pos' list -> bool -> ctree -> ctree -> int list * int -> ctree -> ctree * pos' list

  val cut_tree : ctree -> int list * 'a -> ctree * (int list * pos_) list val del_res : ppobj -> ppobj

  val e_ctree : ctree val e_ctxt : Proof.context val e_fmz : 'a list * spec val e_istate : istate

  val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec

  val e_origin : 'a list * spec * term val e_pos' : 'a list * pos_ val e_sube : cterm' list

  val e_subs : string list type env = (term * term) list

  type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list

  val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list

  val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string val ets2str : ets -> string

  val existpt : int list -> ctree -> bool val existpt' : int list * pos_ -> ctree -> bool

  val g_branch : ppobj -> branch

  val g_ctxt : ppobj -> Proof.context val g_domID : ppobj -> domID

  val g_env : ppobj -> (istate * Proof.context) option val g_fmz : ppobj -> fmz val g_form : ppobj -> term

  val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

  val g_met : ppobj -> itm list val g_metID : ppobj -> metID val g_origin : ppobj -> ori list * spec * term

  val g_res : ppobj -> term val g_result : ppobj -> result

  val g_spec : ppobj -> spec val g_tac : ppobj -> tac

  val get_allp : (int list * pos_) list -> int list * (int list * pos_) -> ctree -> (int list * pos_) list

  val get_allpos' : posel list * posel -> ctree -> (posel list * pos_) list

  val get_allpos's : posel list * posel -> ctree list -> (posel list * pos_) list

  val get_allps : (int list * pos_) list -> int list -> ctree list -> (int list * pos_) list

  val get_assumptions_ : ctree -> int list * pos_ -> term list

  val get_ctxt : ctree -> int list * pos_ -> Proof.context

  val get_curr_formula : ctree * (int list * pos_) -> term

  val get_istate : ctree -> int list * pos_ -> istate

  val get_loc : ctree -> int list * pos_ -> istate * Proof.context val get_nd : ctree -> int list -> ctree

  val get_obj : (ppobj -> 'a) -> ctree -> int list -> 'a

  val get_somespec' : domID * pblID * metID -> domID * pblID * metID -> domID * pblID * metID

  val get_trace : ctree -> int list -> int list -> int list list type iist = istate option * istate option

  val ins_chn : ctree list -> ctree -> int list -> ctree

  val insert_pt : ppobj -> ctree -> int list -> ctree val is_e_ctxt : Proof.context -> bool

  val is_empty_tac : tac -> bool val is_interpos : 'a * pos_ -> bool val is_pblnd : ctree -> bool

  val is_pblobj : ppobj -> bool val is_pblobj' : ctree -> int list -> bool val is_rewset : tac -> bool

  val is_rewtac : tac -> bool datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate

  val istate2str : istate -> string val istates2str : istate option * istate option -> string

  val just_created : ctree * (int list * 'a) -> bool val just_created_ : ppobj -> bool

  val lev_on : int list -> int list val lev_pred' : ctree -> int list * pos_ -> int list * pos_

  val lev_up : int list -> pos val move_dn : int list -> ctree -> int list * pos_ -> int list * pos_

  val move_up : int list -> ctree -> int list * pos_ -> int list * pos_

  val movecalchd_up : ctree -> int list * pos_ -> int list * pos_

  val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_

  val movelevel_up : int list -> ctree -> int list * 'a -> int list * pos_

  val new_val : term -> istate -> istate val nth : int -> 'a list -> 'a

  type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

  val ocalhd2str :

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

  datatype ostate = Complete | Incomplete | Inconsistent val ostate2str : ostate -> string

  val par_pbl_det : ctree -> int list -> bool * int list * rls

  val par_pblobj : ctree -> int list -> int list type pos = int list type pos' = pos * pos_

  val pos'2str : int list * pos_ -> string val pos's2str : (int list * pos_) list -> string

  val pos2str : int list -> string datatype pos_ = Frm | Met | Pbl | Res | Und

  val pos_2str : pos_ -> string eqtype posel

  datatype ppobj

  = PblObj of

    {branch: branch,

     cell: lrd option,

     ctxt: Proof.context,

     env: (istate * Proof.context) option,

     fmz: fmz,

     loc: (istate * Proof.context) option * (istate * Proof.context) option,

     meth: itm list,

     origin: ori list * spec * term, ostate: ostate, probl: itm list, result: result, spec: spec}

     | PrfObj of

     {branch: branch,

      cell: lrd option,

      form: term,

      loc: (istate * Proof.context) option * (istate * Proof.context) option,

      ostate: ostate, result: result, tac: tac}

  val pr_ctree : (int list -> ppobj -> string) -> ctree -> string val pr_pos : int list -> string

  val pr_short : int list -> ppobj -> string val preconds2str : (bool * term) list -> string

  datatype ptform = Form of term | ModSpec of ocalhd val repl : 'a list -> int -> 'a -> 'a list

  val repl_app : 'a list -> int -> 'a -> 'a list val res2str : term * term list -> string

  type result = term * term list val rls_of : tac -> rls' val rootthy : ctree -> theory

  val rta2str : rule * (term * term list) -> string

  val rule2tac : theory -> (term * term) list -> rule -> tac

  datatype safe = Helpless | Safe | Sundef | Unsafe val safe2str : safe -> string

  type scrstate = env * loc_ * term option * term * safe * bool

  val scrstate2str : subst * loc_ * term option * term * safe * bool -> string type state = ctree * pos'

  val str2pos_ : string -> pos_ type sube = cterm' list val sube2str : string list -> string

  val sube2subst : theory -> string list -> (term * term) list val sube2subte : string list -> term list

  type subs = cterm' list val subs2subst : theory -> string list -> (term * term) list

  val subst2sube : (term * term) list -> string list val subst2subs : (term * term) list -> string list

  val subst2subs' : (term * term) list -> (string * string) list type subte = term list

  val subte2sube : term list -> string list val subte2subst : term list -> (term * term) list

  datatype tac

  = Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm' | Apply_Assumption of cterm' list

     | Apply_Method of metID | Begin_Sequ | Begin_Trans | CAScmd of cterm' | Calculate of string

     | Check_Postcond of pblID | Check_elementwise of cterm' | Collect_Trues | Conclude_And | Conclude_Or

     | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm' | Derive of rls'

     | Detail_Set of rls' | Detail_Set_Inst of subs * rls' | Empty_Tac | End_Detail | End_Intersect

     | End_Proof' | End_Ruleset | End_Sequ | End_Subproblem | End_Trans | Free_Solve

     | Init_Proof of cterm' list * spec | Model_Problem | Or_to_List | Refine_Problem of pblID

     | Refine_Tacitly of pblID | Rewrite of thm'' | Rewrite_Asm of thm'' | Rewrite_Inst of subs * thm''

     | Rewrite_Set of rls' | Rewrite_Set_Inst of subs * rls' | Specify_Method of metID

     | Specify_Problem of pblID | Specify_Theory of domID | Split_And | Split_Intersect | Split_Or

     | Subproblem of domID * pblID | Substitute of sube | Tac of string | Take of cterm'

     | Take_Inst of cterm'

  val tac2IDstr : tac -> string val tac2str : tac -> string

  datatype tac_

  = Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list

     | Apply_Assumption' of term list * term

     | Apply_Method' of metID * term option * istate * Proof.context | Begin_Sequ' | Begin_Trans' of term

     | CAScmd' of term | Calculate' of theory' * string * term * (term * thm')

     | Check_Postcond' of pblID * result | Check_elementwise' of term * string * result

     | Collect_Trues' of term | Conclude_And' of term | Conclude_Or' of term | Del_Find' of cterm'

     | Del_Given' of cterm' | Del_Relation' of cterm' | Derive' of rls

     | Detail_Set' of theory' * bool * rls * term * result

     | Detail_Set_Inst' of theory' * bool * subst * rls * term * result | Empty_Tac_

     | End_Detail' of result | End_Intersect' of term | End_Proof'' | End_Ruleset' of term | End_Sequ'

     | End_Subproblem' of term | End_Trans' of result | Free_Solve' | Init_Proof' of cterm' list * spec

     | Model_Problem' of pblID * itm list * itm list | Or_to_List' of term * term

     | Refine_Problem' of pblID * (itm list * (bool * term) list)

     | Refine_Tacitly' of pblID * pblID * domID * metID * itm list

     | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result

     | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result

     | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result

     | Rewrite_Set' of theory' * bool * rls * term * result

     | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result

     | Specify_Method' of metID * ori list * itm list

     | Specify_Problem' of pblID * (bool * (itm list * (bool * term) list)) | Specify_Theory' of domID

     | Split_And' of term | Split_Intersect' of term | Split_Or' of term

     | Subproblem' of spec * ori list * term * fmz_ * Proof.context * term

     | Substitute' of rew_ord_ * rls * subte * term * term | Tac_ of theory * string * string * string

     | Take' of term | Take_Inst' of term

  val tac_2str : tac_ -> string val test_trans : ppobj -> bool val topt2str : term option -> string end*)

(**)

structure CTbasic(**): BASIC_CALC_TREE(**) =

struct

(**)

type result = term * term list

type env = (term * term) list;

datatype branch = 

	NoBranch | AndB | OrB 

| TransitiveB  (* FIXXXME.0308: set branch from met in Apply_Method

                  FIXXXME.0402: -"- in Begin_Trans'*)

| SequenceB | IntersectB | CollectB | MapB;

fun branch2str NoBranch = "NoBranch" (* for tests only *)

  | branch2str AndB = "AndB"

  | branch2str OrB = "OrB"

  | branch2str TransitiveB = "TransitiveB" 

  | branch2str SequenceB = "SequenceB"

  | branch2str IntersectB = "IntersectB"

  | branch2str CollectB = "CollectB"

  | branch2str MapB = "MapB";

datatype ostate = 

    Incomplete | Complete | Inconsistent (* WN041020 latter still unused *);

fun ostate2str Incomplete = "Incomplete" (* for tests only *)

  | ostate2str Complete = "Complete"

  | ostate2str Inconsistent = "Inconsistent";

type cellID = int;     

type cid = cellID list;

type posel = int; (* for readability in funs accessing Ctree *)

type pos = int list;

val pos2str = ints2str';

datatype pos_ = 

  Pbl    (* PblObj-position: problem-type                   *)

| Met    (* PblObj-position: method                         *)

| Frm    (* PblObj-position: -> Pbl in ME (not by moveDown !)

         |  PrfObj-position: formula                       *)

| Res    (* PblObj | PrfObj-position: result                *)

| Und;   (* undefined*)

fun pos_2str Pbl = "Pbl"

  | pos_2str Met = "Met"

  | pos_2str Frm = "Frm"

  | pos_2str Res = "Res"

  | pos_2str Und = "Und";

fun str2pos_ "Pbl" = Pbl

  | str2pos_ "Met" = Met

  | str2pos_ "Frm" = Frm

  | str2pos_ "Res" = Res

  | str2pos_ "Und" = Und

  | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)

type pos' = pos * pos_;

(*WN0312 remembering interator (pos * pos_) for ctree 

	   pos : lev_on, lev_dn, lev_up

     pos_:

# generate1 sets pos_ if possible  ...?WN0502?NOT...

# generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn

                     exceptions: Begin/End_Trans

# thus generate(1) called in

.# assy, locate_gen 

.# nxt_solv (tac_ -cases); general case: 

  val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'

# WN050220, S(604):

  generate1...(Rewrite(f,..,res))..(pos, pos_)

     cappend_atomic.................pos //////  gets f+res always!!!

        cut_tree....................pos, pos_ 

*)

fun pos'2str (p, p_) = pair2str (ints2str' p, pos_2str p_);

fun pos's2str ps = (strs2str' o (map pos'2str)) ps; (* for tests only *)

val e_pos' = ([], Und);

fun res2str (t, ts) = pair2str (term2str t, terms2str ts); (* for tests only *)

datatype safe = Sundef | Safe | Unsafe | Helpless;

fun safe2str Sundef   = "Sundef"

  | safe2str Safe     = "Safe"

  | safe2str Unsafe   = "Unsafe" 

  | safe2str Helpless = "Helpless";

type subs = cterm' list; (*16.11.00 for FE-KE*)

val e_subs = ["(bdv, x)"]; (* for tests only *)

(* argument type of tac Rewrite_Inst *)

type sube = cterm' list;

val e_sube = []: cterm' list; (* for tests only *)

fun sube2str s = strs2str s;

(* _sub_stitution as _t_erms of _e_qualities *)

type subte = term list;

val subte2sube = map term2str;

val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));

fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)

val subst2subs' = map ((apfst term2str) o (apsnd term2str));

fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;

fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;

val sube2subte = map str2term;

val subte2subst = map HOLogic.dest_eq;

type scrstate =       (*state for script interpreter*)

	 env(*stack*) (*used to instantiate tac for checking assod

		       12.03.noticed: e_ not updated during execution ?!?*)

	 * loc_       (*location of tac in script*)

	 * term option(*argument of curried functions*)

	 * term       (*value obtained by tac executed

		       updated also after a derivation by 'new_val'*)

	 * safe       (*estimation of how result will be obtained*)

	 * bool;      (*true = strongly .., false = weakly associated: 

					    only used during ass_dn/up*)

fun topt2str NONE = "NONE"

  | topt2str (SOME t) = "SOME" ^ term2str t;

fun scrstate2str (env, loc_, topt, t, safe, bool) = (* for tests only *)

  "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^ 

  term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";

(* for handling type istate see fun from_pblobj_or_detail', +? *)

datatype istate =           (*interpreter state*)

	  Uistate                 (*undefined in modspec, in '_deriv'ation*)

  | ScrState of scrstate    (*for script interpreter*)

  | RrlsState of rrlsstate; (*for reverse rewriting*)

val e_istate = (ScrState ([],[],NONE,e_term,Sundef,false));

val e_ctxt = Proof_Context.init_global @{theory "Pure"};

(* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)

fun is_e_ctxt ctxt = Theory.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});

type iist = istate option * istate option;

(*val e_iist = (e_istate, e_istate); --- sinnlos f"ur NICHT-equality-type*) 

fun rta2str (r, (t, a)) = "\n(" ^ rule2str r ^ ",(" ^ term2str t ^", " ^ terms2str a ^ "))";

fun istate2str Uistate = "Uistate"

  | istate2str (ScrState (e, l, to, t, s, b)) =

    "ScrState ("^ subst2str e ^ ",\n " ^ 

    loc_2str l ^ ", " ^ termopt2str to ^ ",\n " ^

    term2str t ^ ", " ^ safe2str s ^ ", " ^ bool2str b ^ ")"

  | istate2str (RrlsState (t, t1, rss, rtas)) = 

    "RrlsState (" ^ term2str t ^ ", " ^ term2str t1 ^ ", " ^

    (strs2str o (map (strs2str o (map rule2str)))) rss ^ ", " ^

    (strs2str o (map rta2str)) rtas ^ ")";

fun istates2str (NONE, NONE) = "(#NONE, #NONE)"  (* for tests only *)

  | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"

  | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"

  | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";

fun new_val v (ScrState (env, loc_, topt, _, safe, bool)) =

    (ScrState (env, loc_, topt, v, safe, bool))

  | new_val _ _ = error "new_val: only for ScrState";

datatype con = land | lor;

(* tactics for user at front-end.

   tac propagates the construction of the calc-tree;

   there are

   (a) 'specsteps' for the specify-phase, and others for the solve-phase

   (b) those of the solve-phase are 'initac's and others;

       initacs start with a formula different from the preceding formula.

   see 'type tac_' for the internal representation of tactics

   TODO.WN161219: replace *every* cterm' by term

*)

datatype tac =

    Add_Find of cterm' | Add_Given of cterm' | Add_Relation of cterm'

  | Apply_Assumption of cterm' list

  | Apply_Method of metID

    (* creates an "istate" in PblObj.env; in case of "init_form" 

      creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"

      a "SOME istate" at fst of "loc".

      As each step (in the solve-phase) has a resulting formula (at the front-end)

      Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)  

  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)

  | Begin_Sequ | Begin_Trans

  | Split_And | Split_Or | Split_Intersect

  | Conclude_And | Conclude_Or | Collect_Trues

  | End_Sequ | End_Trans

  | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'

  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)

  | CAScmd of cterm'

  | Calculate of string

  | Check_Postcond of pblID

  | Check_elementwise of cterm'

  | Del_Find of cterm' | Del_Given of cterm' | Del_Relation of cterm'

  | Derive of rls'                 (* WN0509 drop *)

  | Detail_Set of rls'             (* WN0509 drop *)

  | Detail_Set_Inst of subs * rls' (* WN0509 drop *)

  | End_Detail                     (* WN0509 drop *)

  | Empty_Tac

  | Free_Solve

  | Init_Proof of cterm' list * spec

  | Model_Problem

  | Or_to_List

  | Refine_Problem of pblID

  | Refine_Tacitly of pblID

   (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end

     because there all the thms are present with both (thmID, thm)

     (where user-views can show both or only one of (thmID, thm)),

     and thm is created from ThmID by assoc_thm'' when entering isabisac *)

  | Rewrite of thm''

  | Rewrite_Asm of thm''

  | Rewrite_Inst of subs * thm''

  | Rewrite_Set of rls'

  | Rewrite_Set_Inst of subs * rls'

  | Specify_Method of metID

  | Specify_Problem of pblID

  | Specify_Theory of domID

  | Subproblem of domID * pblID (* WN0509 drop *)

  | Substitute of sube

  | Tac of string               (* WN0509 drop *)

  | Take of cterm' | Take_Inst of cterm'

fun tac2str ma = case ma of

    Init_Proof (ppc, spec)  => 

      "Init_Proof "^(pair2str (strs2str ppc, spec2str spec))

  | Model_Problem           => "Model_Problem "

  | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 

  | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 

  | Add_Given cterm'        => "Add_Given " ^ cterm'

  | Del_Given cterm'        => "Del_Given " ^ cterm'

  | Add_Find cterm'         => "Add_Find " ^ cterm'

  | Del_Find cterm'         => "Del_Find " ^ cterm'

  | Add_Relation cterm'     => "Add_Relation " ^ cterm'

  | Del_Relation cterm'     => "Del_Relation " ^ cterm'

  | Specify_Theory domID    => "Specify_Theory " ^ quote domID

  | Specify_Problem pblID   => "Specify_Problem " ^ strs2str pblID

  | Specify_Method metID    => "Specify_Method " ^ strs2str metID

  | Apply_Method metID      => "Apply_Method " ^ strs2str metID

  | Check_Postcond pblID    => "Check_Postcond " ^ strs2str pblID

  | Free_Solve              => "Free_Solve"

  | Rewrite_Inst (subs, (id, thm)) =>

    "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> term2str)))

  | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> term2str)

  | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> term2str)

  | Rewrite_Set_Inst (subs, rls) => 

    "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)

  | Rewrite_Set rls         => "Rewrite_Set " ^ quote rls

  | Detail_Set rls          => "Detail_Set " ^ quote rls

  | Detail_Set_Inst (subs, rls) =>  "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)

  | End_Detail              => "End_Detail"

  | Derive rls'             => "Derive " ^ rls' 

  | Calculate op_           => "Calculate " ^ op_ 

  | Substitute sube         => "Substitute " ^ sube2str sube	     

  | Apply_Assumption ct's   => "Apply_Assumption " ^ strs2str ct's

  | Take cterm'             => "Take " ^ quote cterm'

  | Take_Inst cterm'        => "Take_Inst " ^ quote cterm'

  | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)

  | End_Subproblem          => "End_Subproblem"

  | CAScmd cterm'           => "CAScmd " ^ quote cterm'

  | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'

  | Or_to_List              => "Or_to_List "

  | Collect_Trues           => "Collect_Trues"

  | Empty_Tac               => "Empty_Tac"

  | Tac string              => "Tac " ^ string

  | End_Proof'              => "tac End_Proof'"

  | _                       => "tac2str not impl. for ?!";

fun is_empty_tac tac = case tac of Empty_Tac => true | _ => false

fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2

  | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2

  | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2

  | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2

  | eq_tac (Calculate id1, Calculate id2) = id1 = id2

  | eq_tac _ = false

fun is_rewset (Rewrite_Set_Inst _) = true

  | is_rewset (Rewrite_Set _) = true 

  | is_rewset _ = false;

fun is_rewtac (Rewrite _) = true

  | is_rewtac (Rewrite_Inst _) = true

  | is_rewtac (Rewrite_Asm _) = true

  | is_rewtac tac = is_rewset tac;

fun tac2IDstr ma = case ma of

    Model_Problem => "Model_Problem"

  | Refine_Tacitly _ => "Refine_Tacitly"

  | Refine_Problem _ => "Refine_Problem"

  | Add_Given _ => "Add_Given"

  | Del_Given _ => "Del_Given"

  | Add_Find _ => "Add_Find"

  | Del_Find _ => "Del_Find"

  | Add_Relation _ => "Add_Relation"

  | Del_Relation _ => "Del_Relation"

  | Specify_Theory _ => "Specify_Theory"

  | Specify_Problem _ => "Specify_Problem"

  | Specify_Method _ => "Specify_Method"

  | Apply_Method _ => "Apply_Method"

  | Check_Postcond _ => "Check_Postcond"

  | Free_Solve => "Free_Solve"

  | Rewrite_Inst _ => "Rewrite_Inst"

  | Rewrite _ => "Rewrite"

  | Rewrite_Asm _ => "Rewrite_Asm"

  | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"

  | Rewrite_Set _ => "Rewrite_Set"

  | Detail_Set _ => "Detail_Set"

  | Detail_Set_Inst _ => "Detail_Set_Inst"

  | Derive _ => "Derive "

  | Calculate _ => "Calculate "

  | Substitute _ => "Substitute" 

  | Apply_Assumption _ => "Apply_Assumption"

  | Take _ => "Take"

  | Take_Inst _ => "Take_Inst"

  | Subproblem _ => "Subproblem"

  | End_Subproblem => "End_Subproblem"

  | CAScmd _ => "CAScmd"

  | Check_elementwise _ => "Check_elementwise"

  | Or_to_List => "Or_to_List "

  | Collect_Trues => "Collect_Trues"

  | Empty_Tac => "Empty_Tac"

  | Tac _ => "Tac "

  | End_Proof' => "End_Proof'"

  | _ => "tac2str not impl. for ?!";

fun rls_of (Rewrite_Set_Inst (_, rls)) = rls

  | rls_of (Rewrite_Set rls) = rls

  | rls_of tac = error ("rls_of: called with tac \"" ^ tac2IDstr tac ^ "\"");

fun rule2tac thy _ (Calc (opID, thm)) = Calculate (assoc_calc thy opID)

  | rule2tac _ [] (Thm thm'') = Rewrite thm''

  | rule2tac _ subst (Thm thm'') = 

    Rewrite_Inst (subst2subs subst, thm'')

  | rule2tac _ [] (Rls_ rls) = Rewrite_Set (id_rls rls)

  | rule2tac _ subst (Rls_ rls) = 

    Rewrite_Set_Inst (subst2subs subst, (id_rls rls))

  | rule2tac _ _ rule = 

    error ("rule2tac: called with \"" ^ rule2str rule ^ "\"");

(* tactics for for internal use, compare "tac" for user at the front-end.

  tac_ contains results from check in 'fun applicable_in'.

  This is useful for costly results, e.g. from rewriting;

  however, these results might be changed by Scripts like

      "      eq = (Rewrite_Set ansatz_rls False) eql;" ^

      "      eq = drop_questionmarks eq;" ^

      "      eq = (Rewrite_Set equival_trans False) eq;" ^

  TODO.WN120106 ANALOGOUSLY TO Substitute':

  So tac_ contains the term t the result was calculated from

  in order to compare t with t' possibly changed by "Expr "

  and re-calculate result if t<>t'

  TODO.WN161219: replace *every* cterm' by term

*)

  datatype tac_ =

    Add_Find' of cterm' * itm list | Add_Given' of cterm' * itm list | Add_Relation' of cterm' * itm list

  | Apply_Assumption' of term list * term

  | Apply_Method' of metID * term option * istate * Proof.context

  (*/--- TODO: re-design ? -----------------------------------------------------------------\*)

  | Begin_Sequ' | Begin_Trans' of term

  | Split_And' of term | Split_Or' of term | Split_Intersect' of term

  | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term

  | End_Sequ' | End_Trans' of result

  | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''

  (*\--- TODO: re-design ? -----------------------------------------------------------------/*)

  | CAScmd' of term

  | Calculate' of theory' * string * term * (term * thm')

  | Check_Postcond' of pblID *

    result       (* returnvalue of script in solve *)

  | Check_elementwise' of (*special case:*)

    term *       (* (1) the current formula: [x=1,x=...]     *)

    string *     (* (2) the pred from Check_elementwise      *)

    result       (* (3) composed from (1) and (2): {x. pred} *)

  | Del_Find' of cterm' | Del_Given' of cterm' | Del_Relation' of cterm'

  | Derive' of rls

  | Detail_Set' of theory' * bool * rls * term * result

  | Detail_Set_Inst' of theory' * bool * subst * rls * term * result

  | End_Detail' of result

  | Empty_Tac_

  | Free_Solve'

  | Init_Proof' of cterm' list * spec

  | Model_Problem' of pblID * 

    itm list *  (* the 'untouched' pbl        *)

    itm list    (* the casually completed met *)

  | Or_to_List' of term * term

  | Refine_Problem' of pblID * (itm list * (bool * term) list)

  | Refine_Tacitly' of

    pblID *     (* input*)

    pblID *     (* the refined from applicable_in                                       *)

    domID *     (* from new pbt?! filled in specify                                     *)

    metID *     (* from new pbt?! filled in specify                                     *)

    itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)

  | Rewrite' of theory' * rew_ord' * rls * bool * thm'' * term * result

  | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * result

  | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * result

  | Rewrite_Set' of theory' * bool * rls * term * result

  | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * result

  | Specify_Method' of metID * ori list * itm list

  | Specify_Problem' of pblID * 

    (bool *                  (* matches	      *)

      (itm list *            (* ppc	          *)

        (bool * term) list)) (* preconditions *)

  | Specify_Theory' of domID

  | Subproblem' of

    spec * 

		(ori list) *    (* filled in assod Subproblem'        *)

		term *          (* -"-, headline of calc-head         *)

		Selem.fmz_ * 

    Proof.context * (* transported from assod to generate1*)

		term            (* Subproblem(dom,pbl) OR cascmd      *)  

  | Substitute' of

    rew_ord_ *  (* for re-calculation                      *)

    rls *       (* for re-calculation                      *)

    subte *     (* the 'substitution': terms of type bool  *)

    term *      (* to be substituted in                    *)

    term        (* resulting from the substitution         *)

  | Tac_ of theory * string * string * string

  | Take' of term | Take_Inst' of term

fun tac_2str ma = case ma of

    Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, spec2str spec)

  | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID

  | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^

    strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"

  | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"

  | Add_Given' _ => "Add_Given' "(*^cterm'*)

  | Del_Given' _ => "Del_Given' "(*^cterm'*)

  | Add_Find' _ => "Add_Find' "(*^cterm'*)

  | Del_Find' _ => "Del_Find' "(*^cterm'*)

  | Add_Relation' _ => "Add_Relation' "(*^cterm'*)

  | Del_Relation' _ => "Del_Relation' "(*^cterm'*)

  | Specify_Theory' domID => "Specify_Theory' " ^ quote domID

  | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^ 

    spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))

  | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ 

    metID2str pI ^ ", " ^ oris2str oris ^ ", )"

  | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID

  | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^

      (spair2str (strs2str pblID, spair2str (term2str scval, terms2str asm)))

  | Free_Solve' => "Free_Solve'"

  | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)

  | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)

  | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)

  | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)

  | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^

    "," ^ id_rls rls' ^ "," ^ term2str f ^ ",(" ^ term2str f' ^ "," ^ terms2str asm ^ "))"

  | End_Detail' _ => "End_Detail' xxx"

  | Detail_Set' _ => "Detail_Set' xxx"

  | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"

  | Derive' rls => "Derive' " ^ id_rls rls

  | Calculate'  _ => "Calculate' "

  | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    

  | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)

  | Take' _(*cterm'*) => "Take' "(*^(quote cterm'	)*)

  | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)

  | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => 

    "Subproblem' "(*^(pair2str (domID, strs2str ,))*)

  | End_Subproblem' _ => "End_Subproblem'"

  | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)

  | Empty_Tac_ => "Empty_Tac_"

  | Tac_ (_,form,id,result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"

  | _  => "tac_2str not impl. for arg";

(* executed tactics (tac_s) with local environment etc.;

  used for continuing eval script + for generate *)

type ets =

  (loc_ *  (* of tactic in scr, tactic (weakly) associated with tac_                            *)

   (tac_ * (* (for generate)                                                                    *)

    env *  (* with 'tactic=result' as  rule, tactic ev. _not_ ready: for handling 'parallel let'*)

    env *  (* with results of (ready) tacs                                                      *)

    term * (* itr_arg of tactic, for upd. env at Repeat, Try                                    *)

    term * (* result value of the tac                                                           *)

    safe))

  list;

fun ets2s (l,(m,eno,env,iar,res,s)) = 

  "\n(" ^ loc_2str l ^ ",(" ^ tac_2str m ^

  ",\n  ens= " ^ subst2str eno ^

  ",\n  env= " ^ subst2str env ^

  ",\n  iar= " ^ term2str iar ^

  ",\n  res= " ^ term2str res ^

  ",\n  " ^ safe2str s ^ "))";

fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; (* for tests only *)

type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)

  (int * term list) list * (* assoc-list: args of met*)

  (int * rls) list *       (* assoc-list: tacs already done ///15.9.00*)

  (int * ets) list *       (* assoc-list: tacs etc. already done*)

  (string * pos) list;     (* asms * from where*)

datatype ppobj = (* TODO: arrange according to signature *)

  PrfObj of 

   {cell  : lrd option,       (* where in form tac has been applied, FIXME.WN0607 rename field *)

	  form  : term,             (* where tac is applied to                                       *)

	  tac   : tac,              (* also in istate                                                *)

	  loc   : (istate *         (* script interpreter state                                      *)

	           Proof.context)   (* context for provers, type inference                           *)

            option *          (* both for interpreter location on Frm, Pbl, Met                *)

            (istate *         (* script interpreter state                                      *)

             Proof.context)   (* context for provers, type inference                           *)

            option,           (* both for interpreter location on Res                          *)

                              (*(NONE,NONE) <==> e_istate ! see update_loc, get_loc            *)

	  branch: branch,           (* only rudimentary                                              *)

	  result: result,           (* result and assumptions                                        *)

	  ostate: ostate}           (* Complete <=> result is OK                                     *)

| PblObj of 

   {cell  : lrd option,       (* unused: meaningful only for some _Prf_Obj                     *)

    fmz   : Selem.fmz,        (* from init:FIXME never use this spec;-drop                     *)

    origin: (ori list) *      (* representation from fmz+pbt

                                 for efficiently adding items in probl, meth                   *)

	           spec *           (* updated by Refine_Tacitly                                     *)

	           term,            (* headline of calc-head, as calculated initially(!)             *)

    spec  : spec,             (* explicitly input                                              *)

    probl : itm list,         (* itms explicitly input                                         *)

    meth  : itm list,         (* itms automatically added to copy of probl                     *)

    ctxt  : Proof.context,    (* WN110513 introduced to avoid [*] [**]                         *)

    env   : (istate * Proof.context) option, (* istate only for initac in script              

                                 context for specify phase on this node NO..                  

..NO: this conflicts with init_form/initac: see Apply_Method without init_form                 *)

    loc   : (istate * Proof.context) option * (istate * (* like PrfObj                         *)

              Proof.context) option, (* for spec-phase [*], NO..

..NO: raises errors not tracable on WN110513 [**]                                              *)                               

    branch: branch,           (* like PrfObj                                                   *)

    result: result,           (* like PrfObj                                                   *)

    ostate: ostate};          (* like PrfObj                                                   *)

(* this tree contains isac's calculations;

   the tree's structure has been copied from an early version of Theorema(c);

   it has the disadvantage, that there is no space 

   for the first tactic in a script generating the first formula at (p,Frm);

   this trouble has been covered by 'init_form' and 'Take' so far,

   but it is crucial if the first tactic in a script is eg. 'Subproblem';

   see 'type tac', Apply_Method.

*)

datatype ctree = 

  EmptyPtree

| Nd of ppobj * (ctree list);

val e_ctree = EmptyPtree;

type state = ctree * pos'

fun is_pblobj (PblObj _) = true

  | is_pblobj _ = false;

exception PTREE of string;

fun nth _ [] = raise PTREE "nth _ []"

  | nth 1 (x :: _) = x

  | nth n (_ :: xs) = nth (n - 1) xs;

(*> nth 2 [11,22,33]; -->> val it = 22 : int*)

(** convert ctree to a string **)

(* convert a pos from list to string *)

fun pr_pos ps = (space_implode "." (map string_of_int ps))^".   ";

(* show hd origin or form only *)

fun pr_short p (PblObj _) =  pr_pos p  ^ " ----- pblobj -----\n"               (* for tests only *)

  | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ term2str form ^ "\n";

fun pr_ctree f pt =                                                            (* for tests only *)

  let

    fun pr_pt _ _  EmptyPtree = ""

      | pr_pt pfn ps (Nd (b, [])) = pfn ps b

      | pr_pt pfn ps (Nd (b, ts)) = pfn ps b ^ prts pfn ps 1 ts

    and prts _ _ _ [] = ""

      | prts pfn ps p (t :: ts) = (pr_pt pfn (ps @ [p]) t)^

      (prts pfn ps (p + 1) ts)

  in pr_pt f [] pt end;

(** access the branches of ctree **)

fun repl [] _ _ = raise PTREE "repl [] _ _"

  | repl (_ :: ls) 1 e = e :: ls

  | repl (l :: ls) n e = l :: (repl ls (n-1) e);

fun repl_app ls n e = 

  let

    val lim = 1 + length ls

  in

    if n > lim

    then raise PTREE "repl_app: n > lim"

    else if n = lim

      then ls @ [e]

      else repl ls n e end;

(* get from obj at pos by f : ppobj -> 'a *)

fun get_obj _ EmptyPtree _ = raise PTREE "get_obj f EmptyPtree"

  | get_obj f (Nd (b, _)) [] = f b

  | get_obj f (Nd (_, bs)) (p :: ps) =

    let

      val _ = (nth p bs)

      handle _ => raise PTREE ("get_obj: pos = " ^ ints2str' (p::ps) ^ " does not exist");

    in