diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/ctree.sml --- a/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:36:20 2016 +0100 @@ -172,31 +172,31 @@ val pos_plus : int -> pos' -> pos' val lev_back' : pos' -> pos' (* for inform.sml *) - datatype ptree = EmptyPtree | Nd of ppobj * ptree list - val e_ptree : ptree (* TODO: replace by EmptyPtree*) - val existpt' : pos' -> ptree -> bool (* for interface.sml *) - val exist_lev_on' : ptree -> pos' -> bool (* for interface.sml *) + 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 exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *) val is_interpos : pos' -> bool (* for interface.sml *) - val lev_on' : ptree -> pos' -> pos' (* for interface.sml *) - val lev_pred' : ptree -> pos' -> pos' (* for interface.sml *) - val move_up : pos -> ptree -> pos' -> pos' (* for interface.sml *) - val movelevel_dn : pos -> ptree -> pos' -> pos' (* for interface.sml *) - val movelevel_up : pos -> ptree -> pos' -> pos' (* for interface.sml *) - val movecalchd_up : ptree -> pos' -> pos' (* for interface.sml *) - val par_pblobj : ptree -> pos -> pos - val ins_chn : ptree list -> ptree -> pos -> ptree (* for solve.sml *) - val children : ptree -> ptree list (* for solve.sml *) - val get_nd : ptree -> pos -> ptree (* for solve.sml *) + val lev_on' : ctree -> pos' -> pos' (* for interface.sml *) + val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *) + val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *) + val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *) + val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *) + val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *) + val par_pblobj : ctree -> pos -> pos + 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 : ptree * pos' -> bool (* for mathengine.sml *) - val is_curr_endof_calc : ptree -> pos' -> bool (* for interface.sml *) + val just_created : ctree * pos' -> bool (* for mathengine.sml *) + val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *) val e_origin : ori list * spec * term (* for mathengine.sml *) - val move_dn : pos -> ptree -> pos' -> pos' + val move_dn : pos -> ctree -> pos' -> pos' val is_pblobj : ppobj -> bool - val is_pblobj' : ptree -> pos -> bool - val is_pblnd : ptree -> bool - val last_onlev : ptree -> pos -> bool + val is_pblobj' : ctree -> pos -> bool + val is_pblnd : ctree -> bool + val last_onlev : ctree -> pos -> bool val g_spec : ppobj -> spec val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option @@ -210,37 +210,37 @@ 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 : ptree -> pos' -> istate * Proof.context (* for script.sml *) - val get_istate : ptree -> pos' -> istate (* for script.sml *) - val get_ctxt : ptree -> pos' -> Proof.context - val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a - val get_curr_formula : ptree * pos' -> term - val get_assumptions_ : ptree -> pos' -> term list (* for appl.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 : ctree * pos' -> term + val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *) - val append_result : ptree -> pos -> istate * Proof.context -> result -> - ostate -> ptree * 'a list + val append_result : ctree -> pos -> istate * Proof.context -> result -> + ostate -> ctree * 'a list val append_atomic : (* for solve.sml *) - pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ptree -> ptree - val cappend_atomic : ptree -> pos -> istate * Proof.context -> term -> tac -> result -> - ostate -> ptree * pos' list - val cappend_form : ptree -> pos -> istate * Proof.context -> term -> ptree * pos' list - val cappend_problem : ptree -> pos -> istate * Proof.context -> fmz -> - ori list * spec * term -> ptree * pos' list + pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree + val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result -> + ostate -> ctree * pos' list + val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list + val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz -> + ori list * spec * term -> ctree * pos' list - val update_branch : ptree -> pos -> branch -> ptree - val update_ctxt : ptree -> pos -> Proof.context -> ptree - val update_env : ptree -> pos -> (istate * Proof.context) option -> ptree - val update_oris : ptree -> pos -> ori list -> ptree - val update_orispec : ptree -> pos -> spec -> ptree - val update_pbl : ptree -> pos -> itm list -> ptree - val update_pblppc : ptree -> pos -> itm list -> ptree (* =vvv= ? *) - val update_pblID : ptree -> pos -> pblID -> ptree (* =^^^= ? *) - val update_met : ptree -> pos -> itm list -> ptree (* =vvv= ? *) - val update_metppc : ptree -> pos -> itm list -> ptree (* =^^^= ? *) - val update_metID : ptree -> pos -> metID -> ptree - val update_domID : ptree -> pos -> domID -> ptree - val update_spec : ptree -> pos -> spec -> ptree - val update_tac : ptree -> pos -> tac -> ptree + val update_branch : ctree -> pos -> branch -> ctree + val update_ctxt : ctree -> pos -> Proof.context -> ctree + val update_env : ctree -> pos -> (istate * Proof.context) option -> 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_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *) + val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *) + val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *) + val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *) + val update_metID : ctree -> pos -> metID -> ctree + val update_domID : ctree -> pos -> domID -> ctree + val update_spec : ctree -> pos -> spec -> ctree + val update_tac : ctree -> pos -> tac -> ctree val e_ctxt : Proof.context val is_e_ctxt : Proof.context -> bool (* for appl.sml *) @@ -252,34 +252,34 @@ val get_somespec' : spec -> spec -> spec exception PTREE of string; (* for appl.sml *) - val par_pbl_det : ptree -> pos -> bool * pos * rls + val par_pbl_det : ctree -> pos -> bool * pos * rls (* for rewtools.sml *) val rule2tac : theory -> (term * term) list -> rule -> tac val eq_tac : tac * tac -> bool (* for script.sml *) - val rootthy : ptree -> theory + val rootthy : ctree -> theory (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val update_loc' : ptree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ptree - val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ptree -> ptree + val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree + val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree val g_res : ppobj -> term - val pr_ptree : (pos -> ppobj -> string) -> ptree -> string + val pr_ctree : (pos -> ppobj -> string) -> ctree -> string val pr_short : pos -> ppobj -> string - val existpt : pos -> ptree -> bool + val existpt : pos -> ctree -> bool val is_empty_tac : tac -> bool val e_subs : string list val e_sube : cterm' list val g_branch : ppobj -> branch val g_ctxt : ppobj -> Proof.context val g_fmz : ppobj -> fmz - val get_allp : pos' list -> pos * (int list * pos_) -> ptree -> pos' list - val get_allps : (pos * pos_) list -> posel list -> ptree list -> pos' list - val get_allpos' : pos * posel -> ptree -> pos' list - val get_allpos's : pos * posel -> ptree list -> (pos * pos_) list - val cut_bottom : pos * posel -> ptree -> (ptree * pos' list) * bool - val cut_tree : ptree -> pos * 'a -> ptree * pos' list - val cut_level : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list - val cut_level_'_ : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list - val get_trace : ptree -> int list -> int list -> int list list + 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_tree : ctree -> pos * 'a -> ctree * pos' list + 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 ----------------------------------------------------------/*) @@ -289,41 +289,41 @@ sig val Ets : ets exception PTREE of string val append_atomic : - pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ptree -> ptree - val append_form : int list -> istate * Proof.context -> term -> ptree -> ptree - val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ptree -> ptree - val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ptree -> ptree - val append_result : ptree -> pos -> istate * Proof.context -> term * term list -> ostate -> ptree * 'a list - val appl_branch : (ppobj -> bool) * (posel -> ptree list -> ptree list) -> ptree -> int list -> ptree * bool - val appl_obj : (ppobj -> ppobj) -> ptree -> pos -> ptree - val appl_to_node : (ppobj -> ppobj) -> ptree -> ptree + 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 : - ptree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ptree * pos' list - val cappend_form : ptree -> pos -> istate * Proof.context -> term -> ptree * pos' list - val cappend_parent : ptree -> pos -> istate * Proof.context -> term -> tac -> branch -> ptree * pos' list + 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 : - ptree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ptree * pos' list + ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list eqtype cellID - val children : ptree -> ptree list + val children : ctree -> ctree list type cid = cellID list datatype con = land | lor - val cut_bottom : pos * posel -> ptree -> (ptree * pos' list) * bool - val cut_level : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list - val cut_level_'_ : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list - val cut_levup : pos' list -> bool -> ptree -> ptree -> posel list * posel -> ptree -> ptree * pos' list - val cut_tree : ptree -> pos * 'a -> ptree * 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 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 : ptree -> pos -> ptree + 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_ptree : ptree + val e_ctree : ctree val e_scrstate : scrstate val e_sube : cterm' list val e_subs : string list @@ -333,9 +333,9 @@ 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' : ptree -> pos' -> bool - val existpt : pos -> ptree -> bool - val existpt' : pos' -> ptree -> bool + 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 @@ -345,48 +345,48 @@ val g_env : ppobj -> (istate * Proof.context) option val g_fmz : ppobj -> fmz val g_form : ppobj -> term - val g_form' : ptree -> 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' : ptree -> ostate + val g_ostate' : ctree -> ostate val g_pbl : ppobj -> itm list val g_res : ppobj -> term - val g_res' : ptree -> 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) -> ptree -> 'a list - val get_allp : pos' list -> pos * (int list * pos_) -> ptree -> pos' list - val get_allpos' : pos * posel -> ptree -> pos' list - val get_allpos's : pos * posel -> ptree list -> (pos * pos_) list - val get_allps : (pos * pos_) list -> posel list -> ptree list -> pos' list - val get_alls : (ppobj -> 'a) -> ptree list -> 'a list - val get_assumptions_ : ptree -> pos * pos_ -> term list - val get_ctxt : ptree -> pos * pos_ -> Proof.context - val get_curr_formula : ptree * (pos * pos_) -> term - val get_istate : ptree -> pos * pos_ -> istate - val get_loc : ptree -> pos * pos_ -> istate * Proof.context - val get_nd : ptree -> pos -> ptree - val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a + 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 : ptree -> int list -> int list -> int list list - val gpt_cell : ptree -> lrd option + 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 : ptree list -> ptree -> int list -> ptree + val ins_chn : ctree list -> ctree -> int list -> ctree val ins_nth : int -> 'a -> 'a list -> 'a list - val insert_pt : ppobj -> ptree -> int list -> ptree - val is_curr_endof_calc : ptree -> pos' -> bool + 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 : ptree -> bool + val is_pblnd : ctree -> bool val is_pblobj : ppobj -> bool - val is_pblobj' : ptree -> pos -> bool + val is_pblobj' : ctree -> pos -> bool val is_prfobj : ppobj -> bool val is_rewset : tac -> bool val is_rewtac : tac -> bool @@ -394,35 +394,35 @@ datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate val istate2str : istate -> string val istates2str : istate option * istate option -> string - val just_created : ptree * pos' -> bool + val just_created : ctree * pos' -> bool val just_created_ : ppobj -> bool - val last_onlev : ptree -> pos -> 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' : ptree -> pos' -> pos' + val lev_on' : ctree -> pos' -> pos' val lev_onFrm : pos' -> pos' val lev_pred : pos -> pos - val lev_pred' : ptree -> pos' -> pos' + val lev_pred' : ctree -> pos' -> pos' val lev_up : pos -> pos val lev_up_ : pos' -> pos' - val move_dn : pos -> ptree -> int list * pos_ -> int list * pos_ - val move_up : int list -> ptree -> int list * pos_ -> int list * pos_ - val movecalchd_up : ptree -> pos' -> pos' - val movelevel_dn : int list -> ptree -> int list * pos_ -> int list * pos_ - val movelevel_up : int list -> ptree -> int list * pos_ -> int list * 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 : ptree -> pos -> ptree list * pos - val par_pbl_det : ptree -> pos -> bool * pos * rls - val par_pblobj : ptree -> pos -> pos + 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 @@ -449,12 +449,12 @@ 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_ptree : (pos -> ppobj -> string) -> ptree -> 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 ptree = EmptyPtree | Nd of ppobj * ptree list + datatype ctree = EmptyPtree | Nd of ppobj * ctree list val rep_pblobj : ppobj -> {branch: branch, @@ -494,7 +494,7 @@ val res2str : term * term list -> string val rls_of : tac -> rls' val rls_of_rewset : tac -> rls' * subst option - val rootthy : ptree -> theory + val rootthy : ctree -> theory val rta2str : rule * (term * term list) -> string val rule2tac : theory -> (term * term) list -> rule -> tac val safe2str : safe -> string @@ -558,21 +558,21 @@ val test_trans : ppobj -> bool val thm_of_rew : tac -> thmID * subst option val topt2str : term option -> string - val update_branch : ptree -> pos -> branch -> ptree - val update_ctxt : ptree -> pos -> Proof.context -> ptree - val update_domID : ptree -> pos -> domID -> ptree - val update_env : ptree -> pos -> (istate * Proof.context) option -> ptree - val update_loc' : ptree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ptree - val update_met : ptree -> pos -> itm list -> ptree - val update_metID : ptree -> pos -> metID -> ptree - val update_metppc : ptree -> pos -> itm list -> ptree - val update_oris : ptree -> pos -> ori list -> ptree - val update_orispec : ptree -> pos -> spec -> ptree - val update_pbl : ptree -> pos -> itm list -> ptree - val update_pblID : ptree -> pos -> pblID -> ptree - val update_pblppc : ptree -> pos -> itm list -> ptree - val update_spec : ptree -> pos -> spec -> ptree - val update_tac : ptree -> pos -> tac -> ptree end + 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 *) (**) @@ -629,7 +629,7 @@ | str2pos_ str = error ("str2pos_: wrong argument = " ^ str) type pos' = pos * pos_; -(*WN0312 remembering interator (pos * pos_) for ptree +(*WN0312 remembering interator (pos * pos_) for ctree pos : lev_on, lev_dn, lev_up, lev_onFrm, lev_dnRes (..see solve Apply_Method !) pos_: @@ -1159,7 +1159,7 @@ fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets; -type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*) +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*) @@ -1212,11 +1212,11 @@ but it is crucial if the first tactic in a script is eg. 'Subproblem'; see 'type tac ', Apply_Method. .*) -datatype ptree = +datatype ctree = EmptyPtree - | Nd of ppobj * (ptree list); -val e_ptree = EmptyPtree; -type state = ptree * pos + | Nd of ppobj * (ctree list); +val e_ctree = EmptyPtree; +type state = ctree * pos fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) = {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate}; @@ -1279,7 +1279,7 @@ fun lev_of (p,_) = length p; -(** convert ptree to a string **) +(** convert ctree to a string **) (* convert a pos from list to string *) fun pr_pos ps = (space_implode "." (map string_of_int ps))^". "; @@ -1301,8 +1301,8 @@ ((ints2str c) ^" "^ (term2str form) ^ "\n"); *) -(* convert ptree *) -fun pr_ptree f pt = +(* convert ctree *) +fun pr_ctree f pt = let fun pr_pt pfn _ EmptyPtree = "" | pr_pt pfn ps (Nd (b, [])) = pfn ps b @@ -1321,11 +1321,11 @@ [Nd("xx2.1.",[]), Nd("xx2.2.",[])]), Nd("xx3",[])]); -> tracing (pr_ptree prfn (!pt)); +> tracing (pr_ctree prfn (!pt)); *) -(** access the branches of ptree **) +(** access the branches of ctree **) fun ins_nth 1 e l = e::l | ins_nth n e [] = raise PTREE "ins_nth n e []" @@ -1450,7 +1450,7 @@ fun last_onlev pt pos = not (existpt (lev_on pos) pt); -(*.find the position of the next parent which is a PblObj in ptree.*) +(*.find the position of the next parent which is a PblObj in ctree.*) fun par_pblobj pt [] = [] | par_pblobj pt p = let fun par pt [] = [] @@ -1468,7 +1468,7 @@ end; in par (lev_up p) end; -(*.get the children of a node in ptree.*) +(*.get the children of a node in ctree.*) fun children (Nd (PblObj _, cn)) = cn | children (Nd (PrfObj _, cn)) = cn; @@ -1492,7 +1492,7 @@ -(*.get from the whole ptree by f : ppobj -> 'a.*) +(*.get from the whole ctree by f : ppobj -> 'a.*) fun get_all f EmptyPtree = [] | get_all f (Nd (b, [])) = [f b] | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs) @@ -1500,7 +1500,7 @@ | get_alls f pts = flat (map (get_all f) pts); -(*.insert obj b into ptree at pos, ev.overwriting this pos. +(*.insert obj b into ctree at pos, ev.overwriting this pos. covers library.ML TODO.WN110315 rename*) fun insert_pt b EmptyPtree [] = Nd (b, []) | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _" @@ -1511,7 +1511,7 @@ Nd (b', repl_app bs p (insert_pt b (nth p bs) ps)); (* > type ppobj = string; -> tracing (pr_ptree prfn (!pt)); +> tracing (pr_ctree prfn (!pt)); (*val pt = Unsynchronized.ref Empty;*) pt:= insert_pt ("root'":ppobj) EmptyPtree []; pt:= insert_pt ("xx1":ppobj) (!pt) [1]; @@ -1677,7 +1677,7 @@ val e_ptform' = ModSpec e_ocalhd; (*.applies (snd f) to the branches at a pos if ((fst f) b), - f : (ppobj -> bool) * (int -> ptree list -> ptree list).*) + f : (ppobj -> bool) * (int -> ctree list -> ctree list).*) fun appl_branch f EmptyPtree [] = (EmptyPtree, false) | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _" @@ -1777,7 +1777,7 @@ +++ see Isabelle/../library.ML*) -(**.development for extracting an 'interval' from ptree.**) +(**.development for extracting an 'interval' from ctree.**) (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo actually used (inefficient) version with move_dn: see modspec.sml*) @@ -1812,7 +1812,7 @@ (getnd i ( b,[0]) [99999] nd) @ (getnds ~99999 false (lev_on b,[0]) q nds); in -(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes +(*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous) (1) the 'f' are given (1a) by 'from' if 'f' = the respective element of 'from' (left margin) @@ -1849,7 +1849,7 @@ val metID = if mI = e_metID then mI' else mI in (domID, pblID, metID) end; -(*extract a formula or model from ptree for itms2itemppc or model2xml*) +(*extract a formula or model from ctree for itms2itemppc or model2xml*) fun preconds2str bts = (strs2str o (map (linefeed o pair2str o (apsnd term2str) o @@ -1864,9 +1864,9 @@ fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj; -(**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**) +(**.functions for the 'ctree iterator' as seen from the FE-Kernel interface.**) -(*move one step down into existing nodes of ptree; regard TransitiveB +(*move one step down into existing nodes of ctree; regard TransitiveB ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~################## fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*) (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI); @@ -1936,7 +1936,7 @@ else (P@[p+1], if is_pblnd (nth (p+1) ns) then Pbl else Frm); *) -(*.move one step down into existing nodes of ptree; skip Res = Frm.nxt; +(*.move one step down into existing nodes of ctree; skip Res = Frm.nxt; move_dn at the end of the calc-tree raises PTREE.*) fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*) (case p_ of @@ -1980,7 +1980,7 @@ then Pbl else Frm); -(*.go one level down into ptree.*) +(*.go one level down into ctree.*) fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*) if is_pblobj c then if null ns @@ -2017,7 +2017,7 @@ -(*.go to the previous position in ptree; regard TransitiveB.*) +(*.go to the previous position in ctree; regard TransitiveB.*) fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*) if is_pblobj c then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*) @@ -2048,7 +2048,7 @@ -(*.go one level up in ptree; sets the position on Frm.*) +(*.go one level up in ctree; sets the position on Frm.*) fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*) raise PTREE "pos not existent" @@ -2110,8 +2110,8 @@ (*.get all positions of certain intervals on the ctree.*) (*OLD VERSION without move_dn; kept for occasional redesign - get all pos's to be cut in a ptree - below a pos or from a ptree list after i-th element (NO level_up).*) + get all pos's to be cut in a ctree + below a pos or from a ctree list after i-th element (NO level_up).*) fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list) | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*) if g_ostate b = Incomplete @@ -2143,7 +2143,7 @@ (*.cut branches.*) (*before WN041019...... val cut_branch = (test_trans, curry take): - (ppobj -> bool) * (int -> ptree list -> ptree list); + (ppobj -> bool) * (int -> ctree list -> ctree list); .. formlery used for ... fun cut_tree''' _ [] = EmptyPtree | cut_tree''' pt pos = @@ -2211,11 +2211,11 @@ (*########/ inserted from ctreeNEW.sml \#################################**) -(*.get all positions in a ptree until ([],Res) or ostate=Incomplete +(*.get all positions in a ctree until ([],Res) or ostate=Incomplete val get_allp = fn : pos' list -> : accumulated, start with [] pos -> : the offset for subtrees wrt the root - ptree -> : (sub)tree + ctree -> : (sub)tree pos' : initialization (the last pos' before ...) -> pos' list : of positions in this (sub) tree (relative to the root) .*) @@ -2261,11 +2261,11 @@ (*cut_bottom new sml603..608 cut the level at the bottom of the pos (used by cappend_...) and handle the parent in order to avoid extra case for root -fn: ptree -> : the _whole_ ptree for cut_levup +fn: ctree -> : the _whole_ ctree for cut_levup pos * posel -> : the pos after split_last - ptree -> : the parent of the Nd to be cut + ctree -> : the parent of the Nd to be cut return - (ptree * : the updated ptree + (ctree * : the updated ctree pos' list) * : the pos's cut bool : cutting shall be continued on the higher level(s) *) @@ -2305,12 +2305,12 @@ args pos' list -> : for accumulation bool -> : cutting shall be continued on the higher level(s) - ptree -> : the whole ptree for 'get_nd pt P' on each level - ptree -> : the Nd from the lower level for insertion at path + ctree -> : the whole ctree for 'get_nd pt P' on each level + ctree -> : the Nd from the lower level for insertion at path pos * posel -> : pos=path split for convenience - ptree -> : Nd the children of are under consideration on this call + ctree -> : Nd the children of are under consideration on this call returns : - ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut + ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut .*) fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) = let (*divide level into 3 parts...*)