# HG changeset patch
# User Walther Neuper <wneuper@ist.tugraz.at>
# Date 1482404116 -3600
# Node ID ee5efb0697f6ef08e993a18aac2c95bf7ac8440b
# Parent  255c853ea2f03cbb79a11f343734fd8d473837d1
tuned

diff -r 255c853ea2f0 -r ee5efb0697f6 src/Tools/isac/Interpret/ctree.sml
--- a/src/Tools/isac/Interpret/ctree.sml	Thu Dec 22 11:36:20 2016 +0100
+++ b/src/Tools/isac/Interpret/ctree.sml	Thu Dec 22 11:55:16 2016 +0100
@@ -284,296 +284,6 @@
   val branch2str : branch -> string
 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
 end
-(*
-structure Ctree :
-sig
-  val Ets : ets exception PTREE of string
-  val append_atomic :
-     pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree
-  val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree
-  val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree
-  val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
-  val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list
-  val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool
-  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
-  val cappend_atomic :
-     ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list
-  val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
-  val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list
-  val cappend_problem :
-     ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list
-  eqtype cellID
-  val children : ctree -> ctree list
-  type cid = cellID list
-  datatype con = land | lor
-  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 cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list
-  val cut_tree : ctree -> pos * 'a -> ctree * pos' list
-  val cutlevup : ppobj -> bool
-  val del_res : ppobj -> ppobj
-  val delete_result : ctree -> pos -> ctree
-  val e_ctxt : Proof.context
-  val e_fmz : 'a list * spec
-  val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
-  val e_origin : ori list * spec * term
-  val e_ptform : ptform
-  val e_ptform' : ptform
-  val e_ctree : ctree
-  val e_scrstate : scrstate
-  val e_sube : cterm' list
-  val e_subs : string list
-  val e_subte : term list
-  val empty_envp : envp 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 exist_lev_on' : ctree -> pos' -> bool
-  val existpt : pos -> ctree -> bool
-  val existpt' : pos' -> ctree -> bool
-  type fmz = fmz_ * spec
-  type fmz_ = cterm' list
-  val g_branch : ppobj -> branch
-  val g_cell : ppobj -> lrd option
-  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_form' : ctree -> 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_ostate : ppobj -> ostate
-  val g_ostate' : ctree -> ostate
-  val g_pbl : ppobj -> itm list
-  val g_res : ppobj -> term
-  val g_res' : ctree -> term
-  val g_result : ppobj -> term * term list
-  val g_spec : ppobj -> spec
-  val g_tac : ppobj -> tac
-  val get_all : (ppobj -> 'a) -> ctree -> 'a list
-  val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
-  val get_allpos' : pos * posel -> ctree -> pos' list
-  val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
-  val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
-  val get_alls : (ppobj -> 'a) -> ctree list -> 'a list
-  val get_assumptions_ : ctree -> pos * pos_ -> term list
-  val get_ctxt : ctree -> pos * pos_ -> Proof.context
-  val get_curr_formula : ctree * (pos * pos_) -> term
-  val get_istate : ctree -> pos * pos_ -> istate
-  val get_loc : ctree -> pos * pos_ -> istate * Proof.context
-  val get_nd : ctree -> pos -> ctree
-  val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
-  val get_somespec : spec -> spec -> spec
-  val get_somespec' : spec -> spec -> spec
-  val get_trace : ctree -> int list -> int list -> int list list
-  val gpt_cell : ctree -> lrd option
-  type iist = istate option * istate option
-  val ind : pos' -> int
-  val ins_chn : ctree list -> ctree -> int list -> ctree
-  val ins_nth : int -> 'a -> 'a list -> 'a list
-  val insert_pt : ppobj -> ctree -> int list -> ctree
-  val is_curr_endof_calc : ctree -> pos' -> bool
-  val is_e_ctxt : Proof.context -> bool
-  val is_empty_tac : tac -> bool
-  val is_interpos : pos' -> bool
-  val is_pblnd : ctree -> bool
-  val is_pblobj : ppobj -> bool
-  val is_pblobj' : ctree -> pos -> bool
-  val is_prfobj : ppobj -> bool
-  val is_rewset : tac -> bool
-  val is_rewtac : tac -> bool
-  val isasub2subst : term -> (term * term) list
-  datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
-  val istate2str : istate -> string
-  val istates2str : istate option * istate option -> string
-  val just_created : ctree * pos' -> bool
-  val just_created_ : ppobj -> bool
-  val last_onlev : ctree -> pos -> bool
-  val lev_back' : pos' -> pos'
-  val lev_dn : posel list -> posel list
-  val lev_dnRes : pos' -> pos'
-  val lev_dn_ : pos' -> pos'
-  val lev_of : pos' -> int
-  val lev_on : pos -> posel list
-  val lev_on' : ctree -> pos' -> pos'
-  val lev_onFrm : pos' -> pos'
-  val lev_pred : pos -> pos
-  val lev_pred' : ctree -> pos' -> pos'
-  val lev_up : pos -> pos
-  val lev_up_ : pos' -> pos'
-  val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_
-  val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
-  val movecalchd_up : ctree -> pos' -> pos'
-  val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
-  val movelevel_up : int list -> ctree -> int list * pos_ -> 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 : ocalhd -> string
-  datatype ostate = Complete | Incomplete | Inconsistent
-  val ostate2str : ostate -> string
-  val par_children : ctree -> pos -> ctree list * pos
-  val par_pbl_det : ctree -> pos -> bool * pos * rls
-  val par_pblobj : ctree -> pos -> pos
-  type pos = posel list
-  type pos' = pos * pos_
-  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
-  val pos_plus : int -> pos * pos_ -> pos'
-  eqtype posel
-  val posless : int list -> int list -> bool
-  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: term * term list, spec: spec}
-     | PrfObj of
-     {branch: branch,
-      cell: lrd option,
-      form: term,
-      loc: (istate * Proof.context) option * (istate * Proof.context) option,
-      ostate: ostate, result: term * term list, tac: tac}
-  val pr_pos : int list -> string
-  val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
-  val pr_short : pos -> ppobj -> string
-  val pre_pos : pos -> pos
-  val preconds2str : (bool * term) list -> string
-  datatype ptform = Form of term | ModSpec of ocalhd
-  datatype ctree = EmptyPtree | Nd of ppobj * ctree list
-  val rep_pblobj :
-     ppobj ->
-     {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: term * term list, spec: spec}
-  val rep_prfobj :
-     ppobj ->
-     {branch: branch,
-      cell: lrd option,
-      form: term,
-      loc: (istate * Proof.context) option * (istate * Proof.context) option,
-      ostate: ostate, result: term * term list, tac: tac}
-  val repl : 'a list -> int -> 'a -> 'a list
-  val repl_app : 'a list -> int -> 'a -> 'a list
-  val repl_branch : branch -> ppobj -> ppobj
-  val repl_ctxt : Proof.context -> ppobj -> ppobj
-  val repl_domID : domID -> ppobj -> ppobj
-  val repl_env : (istate * Proof.context) option -> ppobj -> ppobj
-  val repl_form : term -> ppobj -> ppobj
-  val repl_loc : (istate * Proof.context) option * (istate * Proof.context) option -> ppobj -> ppobj
-  val repl_met : itm list -> ppobj -> ppobj
-  val repl_metID : metID -> ppobj -> ppobj
-  val repl_oris : ori list -> ppobj -> ppobj
-  val repl_orispec : spec -> ppobj -> ppobj
-  val repl_pbl : itm list -> ppobj -> ppobj
-  val repl_pblID : pblID -> ppobj -> ppobj
-  val repl_result :
-     (istate * Proof.context) option * (istate * Proof.context) option ->
-     term * term list -> ostate -> ppobj -> ppobj
-  val repl_spec : spec -> ppobj -> ppobj
-  val repl_tac : tac -> ppobj -> ppobj
-  val res2str : term * term list -> string
-  val rls_of : tac -> rls'
-  val rls_of_rewset : tac -> rls' * subst option
-  val rootthy : ctree -> theory
-  val rta2str : rule * (term * term list) -> string
-  val rule2tac : theory -> (term * term) list -> rule -> tac
-  val safe2str : safe -> string
-  type scrstate = env * loc_ * term option * term * safe * bool
-  val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
-  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 subte2str : term list -> string
-  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 | Group of con * int list
-     | 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
-  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 * (term * term list)
-     | Check_elementwise' of term * string * (term * term list) | 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 * (term * term list)
-     | Detail_Set_Inst' of theory' * bool * subst * rls * term * (term * term list) | Empty_Tac_
-     | End_Detail' of term * term list | End_Intersect' of term | End_Proof'' | End_Ruleset' of term
-     | End_Sequ' | End_Subproblem' of term | End_Trans' of term * term list | Free_Solve'
-     | Group' of con * int list * term | 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 * (term * term list)
-     | Rewrite_Asm' of theory' * rew_ord' * rls * bool * thm'' * term * (term * term list)
-     | Rewrite_Inst' of theory' * rew_ord' * rls * bool * subst * thm'' * term * (term * term list)
-     | Rewrite_Set' of theory' * bool * rls * term * (term * term list)
-     | Rewrite_Set_Inst' of theory' * bool * subst * rls * term * (term * term list)
-     | 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 thm_of_rew : tac -> thmID * subst option
-  val topt2str : term option -> string
-  val update_branch : ctree -> pos -> branch -> ctree
-  val update_ctxt : ctree -> pos -> Proof.context -> ctree
-  val update_domID : ctree -> pos -> domID -> ctree
-  val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
-  val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
-  val update_met : ctree -> pos -> itm list -> ctree
-  val update_metID : ctree -> pos -> metID -> ctree
-  val update_metppc : ctree -> pos -> itm list -> ctree
-  val update_oris : ctree -> pos -> ori list -> ctree
-  val update_orispec : ctree -> pos -> spec -> ctree
-  val update_pbl : ctree -> pos -> itm list -> ctree
-  val update_pblID : ctree -> pos -> pblID -> ctree
-  val update_pblppc : ctree -> pos -> itm list -> ctree
-  val update_spec : ctree -> pos -> spec -> ctree
-  val update_tac : ctree -> pos -> tac -> ctree end
-*)
 
 (**)
 structure Ctree(**): CALC_TREEE(**) =
@@ -1205,7 +915,7 @@
 	    ostate: ostate};          (* like PrfObj *)
 
 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
-   the structure has been copied from an early version of Theorema(c);
+   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,
diff -r 255c853ea2f0 -r ee5efb0697f6 src/Tools/isac/Interpret/inform.sml
--- a/src/Tools/isac/Interpret/inform.sml	Thu Dec 22 11:36:20 2016 +0100
+++ b/src/Tools/isac/Interpret/inform.sml	Thu Dec 22 11:55:16 2016 +0100
@@ -371,7 +371,7 @@
 (* compare inform with ctree.form at current pos by nrls;
    if found, embed the derivation generated during comparison
    if not, let the mat-engine compute the next ctree.form *)
-(* structure copied from complete_solve
+(* code's structure is copied from complete_solve
    CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
             all_modspec etc. has to be inserted at Subproblem'*)
 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): Chead.calcstate') ifo =