# HG changeset patch # User Walther Neuper # Date 1482402980 -3600 # Node ID 255c853ea2f03cbb79a11f343734fd8d473837d1 # Parent a474900d5bd270a581603cbf11df0dafcf4abe9d renamed Ctree.ptree --> Ctree.ctree diff -r a474900d5bd2 -r 255c853ea2f0 doc-isac/mat-eng-de.tex --- a/doc-isac/mat-eng-de.tex Thu Dec 22 11:12:18 2016 +0100 +++ b/doc-isac/mat-eng-de.tex Thu Dec 22 11:36:20 2016 +0100 @@ -856,7 +856,7 @@ Nd (PblObj {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, - result=#,spec=#},[]) : ptree + result=#,spec=#},[]) : ctree \end{verbatim}} Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald mehr angezeigt wird, m\"usste dieses jedoch gel\"ost sein. {\footnotesize\begin{verbatim} @@ -935,7 +935,7 @@ Nd (PblObj {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, - result=#,spec=#},[]) : ptree + result=#,spec=#},[]) : ctree \end{verbatim}} Die me erkennt den richtigen Problem type und arbeitet so weiter: {\footnotesize\begin{verbatim} diff -r a474900d5bd2 -r 255c853ea2f0 doc-isac/mat-eng-en.tex --- a/doc-isac/mat-eng-en.tex Thu Dec 22 11:12:18 2016 +0100 +++ b/doc-isac/mat-eng-en.tex Thu Dec 22 11:36:20 2016 +0100 @@ -1245,7 +1245,7 @@ \section{Initialize the calculation} -The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ptree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons. +The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ctree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons. {\footnotesize\begin{verbatim} ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met))); val mID = "Init_Proof" : string @@ -1263,9 +1263,9 @@ Nd (PblObj {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, - result=#,spec=#},[]) : ptree + result=#,spec=#},[]) : ctree \end{verbatim}}%size -The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ptree}, {\tt pos'}). +The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ctree}, {\tt pos'}). We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}: {\footnotesize\begin{verbatim} @@ -1347,7 +1347,7 @@ Nd (PblObj {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#, - result=#,spec=#},[]) : ptree + result=#,spec=#},[]) : ctree \end{verbatim}}%size The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows. {\footnotesize\begin{verbatim} diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Frontend/states.sml --- a/src/Tools/isac/Frontend/states.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Frontend/states.sml Thu Dec 22 11:36:20 2016 +0100 @@ -334,9 +334,9 @@ > !states; val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : states > assoc2 (!states, (3, 1)); -val it = SOME EmptyPtree : ptree option +val it = SOME EmptyPtree : ctree option > assoc2 (!states, (3, 2)); -val it = NONE : ptree option +val it = NONE : ctree option *) (*///7.10 fun add_calc (uI:iterID) (s:state) = diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/Interpret.thy --- a/src/Tools/isac/Interpret/Interpret.thy Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Dec 22 11:36:20 2016 +0100 @@ -8,6 +8,8 @@ begin ML_file "~~/src/Tools/isac/Interpret/mstools.sml" ML_file "~~/src/Tools/isac/Interpret/ctree.sml" + + ML_file "~~/src/Tools/isac/Interpret/ptyps.sml" ML_file "~~/src/Tools/isac/Interpret/generate.sml" ML_file "~~/src/Tools/isac/Interpret/calchead.sml" diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/appl.sml --- a/src/Tools/isac/Interpret/appl.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/appl.sml Thu Dec 22 11:36:20 2016 +0100 @@ -216,7 +216,7 @@ -(*.applicability of a tacic wrt. a calc-state (ptree,pos'). +(*.applicability of a tacic wrt. a calc-state (ctree,pos'). additionally used by next_tac in the script-interpreter for script-tacs. tests for applicability are so expensive, that results (rewrites!) are kept in the return-value of 'type tac_'. diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:36:20 2016 +0100 @@ -9,29 +9,29 @@ type calcstate' datatype appl = Appl of Ctree.tac_ | Notappl of string val nxt_specify_init_calc : Ctree.fmz -> calcstate - val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree -> - Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree - val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate' + val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree -> + Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree + val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate' val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list -> (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac - val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' - val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd + val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' + val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool - val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' + val all_modspec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list val insert_ppc' : itm -> itm list -> itm list - val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' - val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool - val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos' - val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool + val complete_mod : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' + val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool + val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos' + val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool val some_spec : spec -> spec -> spec (* these could go to Ctree ..*) - val show_pt : Ctree.ptree -> unit - val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list - val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list + val show_pt : Ctree.ctree -> unit + val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list + val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list val match_ags : theory -> pat list -> term list -> ori list val match_ags_msg : pblID -> term -> term list -> unit @@ -68,7 +68,7 @@ this state just by "fun generate " *) type calcstate = - (ptree * pos') * (* the calc-state to which the tacis could be applied *) + (ctree * pos') * (* the calc-state to which the tacis could be applied *) (Generate.taci list) (* ev. several (hidden) steps; in REVERSE order: first tac_ to apply is last_elem *) val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate; @@ -86,7 +86,7 @@ Generate.taci list * (* cas. several (hidden) steps; in REVERSE order: first tac_ to apply is last_elem *) pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *) - (ptree * pos') (* the calc-state resulting from the application of tacis *) + (ctree * pos') (* the calc-state resulting from the application of tacis *) val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate'; (* FIXXXME.WN020430 intermediate hack for fun ass_up *) @@ -697,7 +697,7 @@ if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*) then ([], e_ctxt) else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy - val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec') + val (pt, _) = cappend_problem e_ctree [] (e_istate, ctxt) (fmz, spec') (oris, (dI',pI',mI'), e_term) val pt = update_ctxt pt [] ctxt val (pbl, pre) = ([], []) @@ -951,7 +951,7 @@ if pI = e_pblID then opI else pI, if mI = e_metID then omI else mI) : spec -(* find a next applicable tac (for calcstate) and update ptree +(* find a next applicable tac (for calcstate) and update ctree (for ev. finding several more tacs due to hide) *) (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *) (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *) @@ -1087,7 +1087,7 @@ val dI = if dI = "" then theory2theory' thy else dI val mI = if mI = [] then hd met else mI val hdl = case cas of NONE => pblterm dI pI | SOME t => t - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) + val (pt,_) = cappend_problem e_ctree [] (Uistate, e_ctxt) ([], (dI, pI, mI)) ([], (dI,pI,mI), hdl) val pt = update_spec pt [] (dI, pI, mI) val pits = Generate.init_pbl' ppc @@ -1100,7 +1100,7 @@ val {ppc, ...} = Specify.get_met mI val dI = if dI = "" then "Isac" else dI val (pt, _) = - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) + cappend_problem e_ctree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*)) val pt = update_spec pt [] (dI, pI, mI) val mits = Generate.init_pbl' ppc val pt = update_met pt [] mits @@ -1108,7 +1108,7 @@ else (* new example, pepare for interactive modeling *) let val (pt, _) = - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) + cappend_problem e_ctree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term) in ((pt, ([], Pbl)), []) end | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = let (* both """"""""""""""""""""""""" either empty or complete *) @@ -1129,7 +1129,7 @@ NONE => pblterm dI pI | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t val (pt, _) = - cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) + cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) val pt = update_ctxt pt [] pctxt in ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate @@ -1396,7 +1396,7 @@ (* continue with trying 'res' only*) else get_forms (fs @ [form p nd]) (lev_on p) nds; -(** get an 'interval' 'from' 'to' of formulae from a ptree **) +(** get an 'interval' 'from' 'to' of formulae from a ctree **) (* WN0401 this functionality belongs to ctree.sml *) fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2 | eq_pos' (p1, Res) (p2, Res) = p1 = p2 @@ -1413,7 +1413,7 @@ pos' -> : to the last element to be returned; from < to int -> : level: 0 gets the flattest sub-tree possible >999 gets the deepest sub-tree possible - ptree -> : + ctree -> : (pos' * : of the formula Term.term) : the formula list *) 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...*) diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/generate.sml --- a/src/Tools/isac/Interpret/generate.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/generate.sml Thu Dec 22 11:36:20 2016 +0100 @@ -17,17 +17,17 @@ | PpcKF of pblmet * item ppc | RefinedKF of pblID * (itm list * (bool * term) list) val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context -> - Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree (* for calchead.sml------------- ^^^ *) + Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *) val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *) val init_pbl : (string * (term * 'a)) list -> itm list val init_pbl' : (string * (term * term)) list -> itm list - val embed_deriv : taci list -> Ctree.ptree * Ctree.pos' -> Ctree.pos' list * (Ctree.ptree * Ctree.pos') (* for inform.sml *) + val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *) val generate_hard : (* for solve.sml *) - theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree + theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list -> - Ctree.ptree * Ctree.pos' list * Ctree.pos' -> Ctree.ptree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *) + Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *) val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context -> - Ctree.pos' -> Ctree.ptree -> Ctree.ptree * Ctree.pos' (* for interface.sml *) + Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end @@ -86,9 +86,9 @@ not any more used for the specify-phase and for changing the phases*) type taci = (tac * (* for comparison with input tac *) - tac_ * (* for ptree generation *) - (pos' * (* after applying tac_, for ptree generation *) - (istate * Proof.context))) (* after applying tac_, for ptree generation *) + tac_ * (* for ctree generation *) + (pos' * (* after applying tac_, for ctree generation *) + (istate * Proof.context))) (* after applying tac_, for ctree generation *) val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci fun taci2str ((tac, tac_, (pos', (istate, _))):taci) = "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^ @@ -177,7 +177,7 @@ fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm) in map pbt2itm pbt end -(*generate 1 ppobj in ptree*) +(*generate 1 ppobj in ctree*) (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*) fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt = (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]), diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/inform.sml --- a/src/Tools/isac/Interpret/inform.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/inform.sml Thu Dec 22 11:36:20 2016 +0100 @@ -10,16 +10,16 @@ type imodel = iitem list type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec val fetchErrorpatterns : Ctree.tac -> errpatID list - val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd val inform : Chead.calcstate' -> string -> string * Chead.calcstate' - val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list - val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac + val find_fillpatterns : Ctree.ctree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list + val is_exactly_equal : Ctree.ctree * Ctree.pos' -> string -> string * Ctree.tac (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list - val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option + val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c) - val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate' + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos') -> term -> string * Chead.calcstate' val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option val concat_deriv : 'a * ((term * term) list -> term * term -> bool) -> rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list @@ -95,7 +95,7 @@ in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end; -(* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *) +(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *) fun cas_input hdt = let val (h, argl) = strip_comb hdt @@ -108,7 +108,7 @@ val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss val spec = (dI, pI, mI) val (pt,_) = - Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt) + Ctree.cappend_problem Ctree.e_ctree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt) val pt = Ctree.update_spec pt [] spec val pt = Ctree.update_pbl pt [] pits val pt = Ctree.update_met pt [] mits diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/mathengine.sml --- a/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:36:20 2016 +0100 @@ -9,32 +9,32 @@ signature MATH_ENGINE = sig type NEW (* TODO: refactor "fun me" with calcstate and remove *) - val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree + val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ctree val autocalc : - Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos') + Ctree.pos' list -> Ctree.pos' -> (Ctree.ctree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ctree * Ctree.pos') val locatetac : - Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos')) + Ctree.tac -> Ctree.ctree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos')) val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate' val detailstep : - Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos' - val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option + Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' + val get_pblID : Ctree.ctree * Ctree.pos' -> pblID option - val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list - val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list - val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list - val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list - val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd - val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd - val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd - val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list + val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list + val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list + val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list + val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list + val set_method : metID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd + val set_problem : pblID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd + val set_theory : thyID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd + val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) type nxt_ type lOc_ - val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree + val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ctree val f2str : Generate.mout -> cterm' - val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_ - val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_ + val loc_solve_ : string * Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_ + val loc_specify_ : Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_ ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/rewtools.sml --- a/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 11:36:20 2016 +0100 @@ -31,8 +31,8 @@ val no_thycontext : guh -> bool val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs val guh2rewtac : guh -> Ctree.subs -> Ctree.tac - val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac - val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy + val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac + val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy val distinct_Thm : rule list -> rule list val eq_Thms : string list -> rule -> bool val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) -> diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/script.sml Thu Dec 22 11:36:20 2016 +0100 @@ -8,21 +8,21 @@ signature LUCAS_INTERPRETER = sig - type step = Ctree.tac_ * Generate.mout * Ctree.ptree * Ctree.pos' * Ctree.pos' list + type step = Ctree.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list datatype locate = NotLocatable | Steps of Ctree.istate * step list val next_tac : (*diss: next-tactic-function*) - theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe) + theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe) val locate_gen : (*diss: locate-function*) - theory' * rls -> Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate + theory' * rls -> Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate (* can these functions be local to Lucin or part of LItools ? *) - val sel_rules : Ctree.ptree -> Ctree.pos' -> Ctree.tac list + val sel_rules : Ctree.ctree -> Ctree.pos' -> Ctree.tac list val init_form : 'a -> scr -> (term * term) list -> term option val tac_2tac : Ctree.tac_ -> Ctree.tac val init_scrstate : theory -> itm list -> metID -> Ctree.istate * Proof.context * scr - val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ptree -> rls * (Ctree.istate * Proof.context) * scr - val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ptree -> + val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ctree -> rls * (Ctree.istate * Proof.context) * scr + val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ctree -> rls * (Ctree.istate * Proof.context) * scr val rule2thm'' : rule -> thm'' val rule2rls' : rule -> string @@ -31,7 +31,7 @@ datatype asap = Aundef | AssOnly | AssGen datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env datatype appy_ = Napp_ | Skip_ - val appy : theory' * rls -> Ctree.ptree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy + val appy : theory' * rls -> Ctree.ctree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy val formal_args : term -> term list val get_stac : 'a -> term -> term option val go : loc_ -> term -> term @@ -40,11 +40,11 @@ val id_of_scr : term -> string val is_spec_pos : Ctree.pos_ -> bool val itms2args : 'a -> metID -> itm list -> term list - val nstep_up : theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> + val nstep_up : theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> env -> lrd list -> appy_ -> term option -> term -> appy - val sel_appl_atomic_tacs : Ctree.ptree -> Ctree.pos' -> Ctree.tac list - val stac2tac : Ctree.ptree -> theory -> term -> Ctree.tac - val stac2tac_ : Ctree.ptree -> theory -> term -> Ctree.tac * Ctree.tac_ + val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Ctree.tac list + val stac2tac : Ctree.ctree -> theory -> term -> Ctree.tac + val stac2tac_ : Ctree.ctree -> theory -> term -> Ctree.tac * Ctree.tac_ val upd_env_opt : env -> term option * term -> env ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end @@ -64,9 +64,9 @@ type step = tac_ (*transformed from associated tac *) * Generate.mout (*result with indentation etc. *) - * ptree (*containing node created by tac_ + resp. scrstate *) - * pos' (*position in ptree; ptree * pos' is the proofstate *) - * pos' list; (*of ptree-nodes probably cut (by fst tac_) *) + * ctree (*containing node created by tac_ + resp. scrstate *) + * pos' (*position in ctree; ctree * pos' is the proofstate *) + * pos' list; (*of ctree-nodes probably cut (by fst tac_) *) fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm'' | rule2thm'' r = error ("rule2thm': not defined for " ^ rule2str r); @@ -213,7 +213,7 @@ (* convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac, then convert to a 'tac_' (as required in appy). - arg ptree for pushing the thy specified in rootpbl into subpbls *) + arg ctree for pushing the thy specified in rootpbl into subpbls *) fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) = let val tid = (de_esc_underscore o strip_thy) thmID @@ -295,7 +295,7 @@ has been changed (see "datatype tac_"); if yes, recalculate result TODO.WN120106 recalculate impl.only for Substitute' args - pt : ptree for pushing the thy specified in rootpbl into subpbls + pt : ctree for pushing the thy specified in rootpbl into subpbls d : unused (planned for data for comparison) tac_ : from user (via applicable_in); to be compared with ... stac : found in Script @@ -563,8 +563,8 @@ (step list) (* list of steps done until associated stac found; initiated with the data for doing the 1st step, thus the head holds these data further on, - while the tail holds steps finished (incl.scrstate in ptree) *) -| NasApp of (* stac not associated, but applicable, ptree-node generated *) + while the tail holds steps finished (incl.scrstate in ctree) *) +| NasApp of (* stac not associated, but applicable, ctree-node generated *) scrstate * (step list) | NasNap of (* stac not associated, not applicable, nothing generated; for distinction in Or, for leaving iterations, leaving Seq, @@ -789,7 +789,7 @@ datatype locate = Steps of istate (* producing hd of step list (which was latest) for next_tac, for reporting Safe|Unsafe to DG *) - * step (* (scrstate producing this step is in ptree !) *) + * step (* (scrstate producing this step is in ctree !) *) list (* locate_gen may produce intermediate steps *) | NotLocatable; (* no (m Ass m') or (m AssWeak m') found *) @@ -798,7 +798,7 @@ or the end of the script args m : input by the user, already checked by applicable_in, - (to be searched within Or; and _not_ an m doing the step on ptree !) + (to be searched within Or; and _not_ an m doing the step on ctree !) p,pt: (incl ets) at the time of input scr : the script d : canonical simplifier for locating Take, Substitute, Subproblems etc. @@ -819,7 +819,7 @@ (case lo rss f (Thm thm) of [] => NotLocatable | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts')) - | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos') + | locate_gen (thy',srls) (m:tac_) ((pt,p):ctree * pos') (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) = let val thy = assoc_thy thy'; in case if l = [] orelse ( @@ -1042,7 +1042,7 @@ | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) => (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])), (Uistate, ctxt), (e_term, Sundef))) (*next stac*) - | next_tac thy (ptp as (pt, (p, _)):ptree * pos') (sc as Prog (_ $ body)) + | next_tac thy (ptp as (pt, (p, _)):ctree * pos') (sc as Prog (_ $ body)) (ScrState (E,l,a,v,s,_), ctxt) = (case if l = [] then appy thy ptp E [R] body NONE v else nstep_up thy ptp sc E l Skip_ a v of diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Interpret/solve.sml Thu Dec 22 11:36:20 2016 +0100 @@ -90,7 +90,7 @@ -type squ = ptree; (* TODO: safe etc. *) +type squ = ctree; (* TODO: safe etc. *) (*13.9.02-------------- type ctr = (loc * pos) list; @@ -144,7 +144,7 @@ (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos); *) -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) = +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ctree, (pos as (p,_))) = let val {srls, ...} = Specify.get_met mI; val PblObj {meth=itms, ...} = get_obj I pt p; val thy' = get_obj g_domID pt p; @@ -234,7 +234,7 @@ val pr as (p',_) = (lev_up p, Res) val pp = par_pblobj pt p val r = (fst o (get_obj g_result pt)) p' - (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*) + (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*) val thy' = get_obj g_domID pt pp val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is @@ -274,7 +274,7 @@ (*FIXME.WN050821 compare fun solve ... fun nxt_solv*) (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *) -fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) = +fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) = let val {srls,ppc,...} = Specify.get_met mI; val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p; @@ -354,7 +354,7 @@ val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt; in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end -(* find the next tac from the script, nxt_solv will update the ptree *) +(* find the next tac from the script, nxt_solv will update the ctree *) and nxt_solve_ (ptp as (pt, pos as (p,p_))) = if e_metID = get_obj g_metID pt (par_pblobj pt p) then ([], [], (pt, (p, p_))) : Chead.calcstate' @@ -390,7 +390,7 @@ | autoord CompleteSubpbl = 5 | autoord CompleteCalc = 6; -fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') = +fun complete_solve auto c (ptp as (_, p as (_,p_)): ctree * pos') = if p = ([], Res) then ("end-of-calculation", [], ptp) else @@ -420,7 +420,7 @@ else complete_solve auto (c @ c') ptp' | (_, c', ptp') => complete_solve auto (c @ c') ptp' -and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = +and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = let val (_,_,mI) = get_obj g_spec pt p val ctxt = get_ctxt pt pos diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Knowledge/DiffApp-scrpbl.sml --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Thu Dec 22 11:36:20 2016 +0100 @@ -420,7 +420,7 @@ val p = e_pos'; val c = []; val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI'))); -val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []); +val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []); val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst; (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*) diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Knowledge/Equation.thy --- a/src/Tools/isac/Knowledge/Equation.thy Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Knowledge/Equation.thy Thu Dec 22 11:36:20 2016 +0100 @@ -65,7 +65,7 @@ ML{* (*.function for handling the cas-input "solve (x+1=2, x)": - make a model which is already in ptree-internal format.*) + make a model which is already in ctree-internal format.*) (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)"); val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) "solveTest (x+1=2, x)"); diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Knowledge/Simplify.thy --- a/src/Tools/isac/Knowledge/Simplify.thy Thu Dec 22 11:12:18 2016 +0100 +++ b/src/Tools/isac/Knowledge/Simplify.thy Thu Dec 22 11:36:20 2016 +0100 @@ -56,7 +56,7 @@ (** CAS-command **) (*.function for handling the cas-input "Simplify (2*a + 3*a)": - make a model which is already in ptree-internal format.*) + make a model which is already in ctree-internal format.*) (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)"); val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info.get_theory "Simplify"))) "Simplify (2*a + 3*a)"); diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Frontend/use-cases.sml --- a/test/Tools/isac/Frontend/use-cases.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Dec 22 11:36:20 2016 +0100 @@ -316,7 +316,7 @@ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; val ip = get_pos 1 1; val (Form f, tac, asms) = pt_extract (pt, ip); @@ -557,7 +557,7 @@ autoCalculate 1 CompleteToSubpbl; refFormula 1 (get_pos 1 1); (* -1 + x = 0 *); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" then () else @@ -566,7 +566,7 @@ autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*) autoCalculate 1 CompleteToSubpbl; val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; autoCalculate 1 CompleteCalc; (*das geht ohnehin !*); val ((pt,_),_) = get_calc 1; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/calchead.sml --- a/test/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:36:20 2016 +0100 @@ -737,7 +737,7 @@ Free ("1", "Real.real")) $ Free ("x", "Real.real"))), ostate = Incomplete, result = (Const ("empty", "'a"), [])}, - []) : ptree*) + []) : ctree*) "----- WN101007 worked until here (checked same as isac2002) ---"; case nxt of ("Model_Problem", Model_Problem) => () | _ => error "clchead.sml: check specify phase step 1"; @@ -810,13 +810,13 @@ Free ("1", "Real.real")) $ Free ("x", "Real.real"))), ostate = Incomplete, result = (Const ("empty", "'a"), [])}, - []) : ptree*) -"----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED"; + []) : ctree*) +"----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED"; case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => () | _ => error "clchead.sml: check specify phase step 2"; "--- step 3 --"; val (p,_,f,nxt,_,pt) = me nxt p c pt; -"----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED"; +"----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED"; case nxt of ("Add_Given", Add_Given "integrateBy x") => () | _ => error "clchead.sml: check specify phase step 2"; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/ctree.sml --- a/test/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:36:20 2016 +0100 @@ -13,23 +13,23 @@ "-------------- fun get_ctxt -------------------------------------"; "-------------- fun update_ctxt, fun g_ctxt ----------------------"; "-------------- check positions in miniscript --------------------"; -"-------------- get_allpos' (from ptree above)--------------------"; -"-------------- cut_level (from ptree above)----------------------"; -"-------------- cut_tree (from ptree above)-----------------------"; -"=====new ptree 1a miniscript with mini-subpbl ==================="; +"-------------- get_allpos' (from ctree above)--------------------"; +"-------------- cut_level (from ctree above)----------------------"; +"-------------- cut_tree (from ctree above)-----------------------"; +"=====new ctree 1a miniscript with mini-subpbl ==================="; "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------"; -"=====new ptree 2 miniscript with mini-subpbl ===================="; -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; -"-------------- cappend (from ptree above)------------------------"; +"=====new ctree 2 miniscript with mini-subpbl ===================="; +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------"; +"-------------- cappend (from ctree above)------------------------"; "-------------- cappend minisubpbl -------------------------------"; -"=====new ptree 3 ================================================"; +"=====new ctree 3 ================================================"; "-------------- move_dn ------------------------------------------"; "-------------- move_dn: Frm -> Res ------------------------------"; "-------------- move_up ------------------------------------------"; "------ move into detail -----------------------------------------"; -"=====new ptree 3a ==============================================="; +"=====new ctree 3a ==============================================="; "-------------- move_dn in Incomplete ctree ----------------------"; -"=====new ptree 4: crooked by cut_level_'_ ======================="; +"=====new ctree 4: crooked by cut_level_'_ ======================="; (*############## development stopped 0501 ########################*) (******************************************************************) (* val SAVE_get_trace = get_trace; *) @@ -39,13 +39,13 @@ (* val get_trace = SAVE_get_trace; *) (******************************************************************) (*############## development stopped 0501 ########################*) -"=====new ptree 4 ratequation ===================================="; +"=====new ctree 4 ratequation ===================================="; "-------------- pt_extract form, tac, asm<>[] --------------------"; -"=====new ptree 5 minisubpbl ====================================="; +"=====new ctree 5 minisubpbl ====================================="; "-------------- pt_extract form, tac, asm ------------------------"; -"=====new ptree 6 minisubpbl intersteps =========================="; +"=====new ctree 6 minisubpbl intersteps =========================="; "-------------- get_allpos' new ----------------------------------"; -"-------------- cut_tree new (from ptree above)-------------------"; +"-------------- cut_tree new (from ctree above)-------------------"; "-------------- subst2subs subs2subst sube2subst subte2subst -----"; "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; @@ -105,7 +105,7 @@ val cuts = get_allp [] ([], ([],Frm)) pt; val cuts2 = get_allps [] [1] (children pt); -"ctree.sml-------------- cut_tree new (from ptree above)----------"; +"ctree.sml-------------- cut_tree new (from ctree above)----------"; val (pt', cuts) = cut_tree pt ([1],Frm); "ctree.sml-------------- cappend on complete ctree from above ----"; val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]"); @@ -139,9 +139,9 @@ show_pt pt; -"-------------- get_allpos' (from ptree above)--------------------"; -"-------------- get_allpos' (from ptree above)--------------------"; -"-------------- get_allpos' (from ptree above)--------------------"; +"-------------- get_allpos' (from ctree above)--------------------"; +"-------------- get_allpos' (from ctree above)--------------------"; +"-------------- get_allpos' (from ctree above)--------------------"; if get_allpos' ([], 1) pt = [([], Frm), ([1], Frm), @@ -206,9 +206,9 @@ -"-------------- cut_level (from ptree above)----------------------"; -"-------------- cut_level (from ptree above)----------------------"; -"-------------- cut_level (from ptree above)----------------------"; +"-------------- cut_level (from ctree above)----------------------"; +"-------------- cut_level (from ctree above)----------------------"; +"-------------- cut_level (from ctree above)----------------------"; show_pt pt; show_pt pt'; default_print_depth 99; cuts; default_print_depth 3; @@ -252,25 +252,25 @@ ([4], Res)] then () else error "ctree.sml: diff:behav. in cut_level 2a"; -if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" +if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" then () else error "ctree.sml: diff:behav. in cut_level 2b"; val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm); if cuts = [([3, 1], Res), ([3, 2], Res)] then () else error "ctree.sml: diff:behav. in cut_level 3a"; -if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n" +if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n" then () else error "ctree.sml: diff:behav. in cut_level 3b"; val (pt',cuts) = cut_level [] [3] pt ([3,1],Res); if cuts = [([3, 2], Res)] then () else error "ctree.sml: diff:behav. in cut_level 4a"; -if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n" +if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n" then () else error "ctree.sml: diff:behav. in cut_level 4b"; -"-------------- cut_tree (from ptree above)-----------------------"; -"-------------- cut_tree (from ptree above)-----------------------"; -"-------------- cut_tree (from ptree above)-----------------------"; +"-------------- cut_tree (from ctree above)-----------------------"; +"-------------- cut_tree (from ctree above)-----------------------"; +"-------------- cut_tree (from ctree above)-----------------------"; val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*) (*============ inhibit exn AK110726 ============================================== @@ -340,9 +340,9 @@ ([], Res)] then () else error "ctree.sml: diff:behav. in cut_tree 4"; -"=====new ptree 1a miniscript with mini-subpbl ==================="; -"=====new ptree 1a miniscript with mini-subpbl ==================="; -"=====new ptree 1a miniscript with mini-subpbl ==================="; +"=====new ctree 1a miniscript with mini-subpbl ==================="; +"=====new ctree 1a miniscript with mini-subpbl ==================="; +"=====new ctree 1a miniscript with mini-subpbl ==================="; val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], @@ -383,9 +383,9 @@ -"=====new ptree 2 miniscript with mini-subpbl ===================="; -"=====new ptree 2 miniscript with mini-subpbl ===================="; -"=====new ptree 2 miniscript with mini-subpbl ===================="; +"=====new ctree 2 miniscript with mini-subpbl ===================="; +"=====new ctree 2 miniscript with mini-subpbl ===================="; +"=====new ctree 2 miniscript with mini-subpbl ===================="; reset_states (); CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], ("Test", ["sqroot-test","univariate","equation","test"], @@ -401,9 +401,9 @@ if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then () else error "mini-subpbl interSteps broken"; -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------"; +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------"; +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------"; (*WN050225 intermed. outcommented val (pt', cuts) = cut_tree pt ([3,2,1],Frm); if cuts = [([3, 2, 1], Res), @@ -421,9 +421,9 @@ then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2"; -"-------------- cappend (from ptree above)------------------------"; -"-------------- cappend (from ptree above)------------------------"; -"-------------- cappend (from ptree above)------------------------"; +"-------------- cappend (from ctree above)------------------------"; +"-------------- cappend (from ctree above)------------------------"; +"-------------- cappend (from ctree above)------------------------"; val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew"); if cuts = [([3, 2, 1], Res), ([3, 2, 2], Res), @@ -452,7 +452,7 @@ "-------------- cappend minisubpbl -------------------------------"; "-------------- cappend minisubpbl -------------------------------"; "-------------- cappend minisubpbl -------------------------------"; -"=====new ptree 1 miniscript with mini-subpbl ===================="; +"=====new ctree 1 miniscript with mini-subpbl ===================="; val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], @@ -550,9 +550,9 @@ WN050225 intermed. outcommented---*) -"=====new ptree 3 ================================================"; -"=====new ptree 3 ================================================"; -"=====new ptree 3 ================================================"; +"=====new ctree 3 ================================================"; +"=====new ctree 3 ================================================"; +"=====new ctree 3 ================================================"; reset_states (); CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], @@ -665,9 +665,9 @@ if p = ([2, 6], Res) then() else error "ctree.sml: diff.behav. in move into detail"; -"=====new ptree 3a ==============================================="; -"=====new ptree 3a ==============================================="; -"=====new ptree 3a ==============================================="; +"=====new ctree 3a ==============================================="; +"=====new ctree 3a ==============================================="; +"=====new ctree 3a ==============================================="; reset_states (); CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], ("Test", ["sqroot-test","univariate","equation","test"], @@ -698,9 +698,9 @@ -"=====new ptree 4: crooked by cut_level_'_ ======================="; -"=====new ptree 4: crooked by cut_level_'_ ======================="; -"=====new ptree 4: crooked by cut_level_'_ ======================="; +"=====new ctree 4: crooked by cut_level_'_ ======================="; +"=====new ctree 4: crooked by cut_level_'_ ======================="; +"=====new ctree 4: crooked by cut_level_'_ ======================="; reset_states (); CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", @@ -733,11 +733,11 @@ moveActiveFormula 1 ([4,2],Res)(*4.2.1.*); interSteps 1 ([4,2],Res)(*..is activeFormula !?!*); val ((pt,_),_) = get_calc 1; -writeln(pr_ptree pr_short pt); +writeln(pr_ctree pr_short pt); (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]: ###########################################################################*) val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm); -writeln(pr_ptree pr_short pt); +writeln(pr_ctree pr_short pt); @@ -785,7 +785,7 @@ | SOME t => term2str (subst_atomic (mk_env probl) t) end; *) -(*.get an 'interval' from ptree down to a certain level +(*.get an 'interval' from ctree down to a certain level by 'take_fromto children' of the nodes with specific 'from' and 'to'; 'i > 0' suppresses output during recursive descent towards 'from' b: the 'from' incremented to the actual pos @@ -820,7 +820,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) @@ -834,7 +834,7 @@ (take_fromto (hdp p) (hdq q) (children pt)); end; -writeln(pr_ptree pr_short pt); +writeln(pr_ctree pr_short pt); case get_trace pt [1,3] [4,1,1] of [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => () @@ -892,9 +892,9 @@ (******************************************************************) -"=====new ptree 4 ratequation ===================================="; -"=====new ptree 4 ratequation ===================================="; -"=====new ptree 4 ratequation ===================================="; +"=====new ctree 4 ratequation ===================================="; +"=====new ctree 4 ratequation ===================================="; +"=====new ctree 4 ratequation ===================================="; reset_states (); CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", @@ -907,12 +907,12 @@ val (Form f, tac, asms) = pt_extract (pt, p); (*============ inhibit exn WN120316 ============================================== if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then () - else error "after ===new ptree 4 ratequation ==="; + else error "after ===new ctree 4 ratequation ==="; (*WN120317.TODO dropped rateq*) ============ inhibit exn WN120316 ==============================================*) if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*) andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*) -then () else error "after ===new ptree 4 ratequation ==="; +then () else error "after ===new ctree 4 ratequation ==="; "-------------- pt_extract form, tac, asm<>[] --------------------"; @@ -941,9 +941,9 @@ -"=====new ptree 5 minisubpbl ====================================="; -"=====new ptree 5 minisubpbl ====================================="; -"=====new ptree 5 minisubpbl ====================================="; +"=====new ctree 5 minisubpbl ====================================="; +"=====new ctree 5 minisubpbl ====================================="; +"=====new ctree 5 minisubpbl ====================================="; reset_states (); CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], ("Test", ["sqroot-test","univariate","equation","test"], @@ -1020,9 +1020,9 @@ | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)"; ========== inhibit exn AK110719 ==============================================*) -"=====new ptree 6 minisubpbl intersteps =========================="; -"=====new ptree 6 minisubpbl intersteps =========================="; -"=====new ptree 6 minisubpbl intersteps =========================="; +"=====new ctree 6 minisubpbl intersteps =========================="; +"=====new ctree 6 minisubpbl intersteps =========================="; +"=====new ctree 6 minisubpbl intersteps =========================="; reset_states (); CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], ("Test", ["sqroot-test","univariate","equation","test"], @@ -1117,9 +1117,9 @@ (**#################################################################**) -"-------------- cut_tree new (from ptree above)-------------------"; -"-------------- cut_tree new (from ptree above)-------------------"; -"-------------- cut_tree new (from ptree above)-------------------"; +"-------------- cut_tree new (from ctree above)-------------------"; +"-------------- cut_tree new (from ctree above)-------------------"; +"-------------- cut_tree new (from ctree above)-------------------"; show_pt pt; val b = get_obj g_branch pt []; if b = TransitiveB then () else diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/inform.sml --- a/test/Tools/isac/Interpret/inform.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Interpret/inform.sml Thu Dec 22 11:36:20 2016 +0100 @@ -63,7 +63,7 @@ appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; if str = (". ----- pblobj -----\n" ^ "1. x + 1 = 2\n" ^ @@ -183,7 +183,7 @@ appendFormula 1 "x = 2" (*|> Future.join*); val ((pt,p),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res) then () @@ -213,7 +213,7 @@ appendFormula 1 "x = 1" (*|> Future.join*); val ((pt,p),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res) then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*) @@ -242,7 +242,7 @@ autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*); appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*); val ((pt,p),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then () else error "inform.sml: diff.behav.appendFormula: Res + latEE 1"; @@ -268,7 +268,7 @@ replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; (* before AK110725 this was ". ----- pblobj -----\n @@ -313,7 +313,7 @@ replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then () else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1"; @@ -336,7 +336,7 @@ replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then () else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1"; @@ -361,7 +361,7 @@ replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1); val ((pt,p),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if p = ([1], Res) then () else error "inform.sml: diff.behav. cut calculation 2"; @@ -457,7 +457,7 @@ appendFormula 1 " x - "; (* syntax error in ' x - ' *) val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then () else error "inform.sml: diff.behav.appendFormula: syntax error"; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/mathengine.sml --- a/test/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:36:20 2016 +0100 @@ -63,7 +63,7 @@ FROM val oris = prep_ori... TO val (oris, _) = prep_ori... *) -"----- insert ctxt in ptree"; +"----- insert ctxt in ctree"; (* datatype ppobj FROM loc : istate option * istate option, TO loc : (istate * ctxt) option * (istate * ctxt) option, @@ -497,7 +497,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) = +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = (nxt, p, [], pt); val ("ok", (_, _, ptp)) = locatetac tac (pt,p) val (pt, p) = ptp; @@ -546,7 +546,7 @@ "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) cas = NONE; (*true*) val hdl = pblterm dI pI; - val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) + val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) val pt = update_ctxt pt [] pctxt; @@ -604,7 +604,7 @@ (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*) (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")}, ^^^^^^^^^^^^^^^^^^^^^^^^^^^*) -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) = +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) = (CompleteSubpbl, [], (pt',pos')); p = ([], Res) = false; member op = [Pbl,Met] p_ = false; @@ -617,7 +617,7 @@ val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); l = [] = false; nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...) @@ -651,7 +651,7 @@ existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false; apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm)); apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c; -(append_atomic p ist_res f r f' s) : ptree -> ptree; +(append_atomic p ist_res f r f' s) : ctree -> ctree; ; (* HERE THE ERROR OCCURED IN THE FIRST APPROACH getTactic 1 ([1,1],Frm); syserror in getTactic <<<<<=========================*) diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/me.sml --- a/test/Tools/isac/Interpret/me.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Interpret/me.sml Thu Dec 22 11:36:20 2016 +0100 @@ -10,9 +10,9 @@ "-----------------------------------------------------------------"; "table of contents -----------------------------------------------"; "-----------------------------------------------------------------"; -"=====new ptree 1: crippled by cut_level_'_ ======================"; +"=====new ctree 1: crippled by cut_level_'_ ======================"; "-------------- get_interval from ctree with move_dn:modspec.sml -"; -"=====new ptree 2 without changes ================================"; +"=====new ctree 2 without changes ================================"; "-------------- getFormulaeFromTo --------------------------------"; "autoCalculate"; "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; @@ -25,9 +25,9 @@ -"=====new ptree 1: crippled by cut_level_'_ ======================"; -"=====new ptree 1: crippled by cut_level_'_ ======================"; -"=====new ptree 1: crippled by cut_level_'_ ======================"; +"=====new ctree 1: crippled by cut_level_'_ ======================"; +"=====new ctree 1: crippled by cut_level_'_ ======================"; +"=====new ctree 1: crippled by cut_level_'_ ======================"; reset_states (); CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", @@ -60,12 +60,12 @@ moveActiveFormula 1 ([4,2],Res)(*4.2.1.*); interSteps 1 ([4,2],Res)(*..is activeFormula !?!*); val ((pt,_),_) = get_calc 1; -writeln(pr_ptree pr_short pt); +writeln(pr_ctree pr_short pt); (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]: ###########################################################################*) val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*) (*##########################################################################*) -writeln(pr_ptree pr_short pt); +writeln(pr_ctree pr_short pt); (*########################################################################## attention: the ctree in states is still the old (perfect) !!! ############################################################################*) @@ -75,7 +75,7 @@ "-------------- get_interval from ctree with move_dn:modspec.sml -"; "-------------- get_interval from ctree with move_dn:modspec.sml -"; "-------------- get_interval from ctree with move_dn:modspec.sml -"; -writeln(pr_ptree pr_short pt); +writeln(pr_ctree pr_short pt); writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt)); case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of @@ -219,9 +219,9 @@ -"=====new ptree 2 without changes ================================"; -"=====new ptree 2 without changes ================================"; -"=====new ptree 2 without changes ================================"; +"=====new ctree 2 without changes ================================"; +"=====new ctree 2 without changes ================================"; +"=====new ctree 2 without changes ================================"; reset_states (); CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", @@ -233,8 +233,8 @@ val p = get_pos 1 1; val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then () - else error "after ===new ptree 2 without changes ==="; -writeln(pr_ptree pr_short pt); + else error "after ===new ctree 2 without changes ==="; +writeln(pr_ctree pr_short pt); "-------------- getFormulaeFromTo --------------------------------"; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/script.sml --- a/test/Tools/isac/Interpret/script.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Interpret/script.sml Thu Dec 22 11:36:20 2016 +0100 @@ -231,9 +231,9 @@ member op = specsteps mI; (*false*) (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*) loc_solve_; (*without _ ??? result is -> lOc writing error ???*) -(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*) +(*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*) (mI,m); (*string * tac*) -ptp (*ptree * pos'*); +ptp (*ctree * pos'*); "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp); (*val (msg, cs') = solve m (pt, pos); (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*) @@ -315,7 +315,7 @@ (*WAS stac2tac_ TODO: no match for SubProblem*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)), +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); l; (*= [R, L, R, L, R, R]*) val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v; @@ -348,7 +348,7 @@ | _ => error "integrate.sml -- me method [diff,integration] -- spec"; "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")"; -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); val (mI,m) = mk_tac'_ tac; val Appl m = applicable_in p pt m; @@ -366,7 +366,7 @@ ini = NONE; (*true*) val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt); val d = e_rls (*FIXME: get simplifier from domID*); -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt')); val thy = assoc_thy thy'; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Dec 22 11:36:20 2016 +0100 @@ -12,7 +12,7 @@ " test specify, fmz <> [] "; " test specify, fmz = [] "; " problemtypes + formalizations "; -"-------------------- ptree of {(a,b). is-max ... ----------------"; +"-------------------- ctree of {(a,b). is-max ... ----------------"; "--------- me .. scripts for maximum-example ---------------------"; "--------- autoCalc .. scripts for maximum-example ---------------"; @@ -120,9 +120,9 @@ === inhibit exn 110722=============================================================*) -"-------------------- ptree of {(a,b). is-max ... --------------------------"; -"-------------------- ptree of {(a,b). is-max ... --------------------------"; -"-------------------- ptree of {(a,b). is-max ... --------------------------"; +"-------------------- ctree of {(a,b). is-max ... --------------------------"; +"-------------------- ctree of {(a,b). is-max ... --------------------------"; +"-------------------- ctree of {(a,b). is-max ... --------------------------"; (* Teil von max-on-surface.sml, der nach Init_Proof -> prep_ori wieder l"auft @@ -231,7 +231,7 @@ val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x^3 ..." Empty_Tac TransitiveB; "--- 4 ---"; -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); (* . ----- pblobj ----- diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Knowledge/partial_fractions.sml --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 22 11:36:20 2016 +0100 @@ -36,7 +36,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method"; val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"; -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt); +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt); val ("ok", (_, _, ptp)) = locatetac tac (pt,p) val (pt, p) = ptp; "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = @@ -55,7 +55,7 @@ "----------- why not nxt = Model_Problem here ? ---------"; "----------- why not nxt = Model_Problem here ? ---------"; val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); val ("ok", (_, _, ptp)) = locatetac tac (pt,p); val (pt, p) = ptp; "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Knowledge/polyeq.sml --- a/test/Tools/isac/Knowledge/polyeq.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Knowledge/polyeq.sml Thu Dec 22 11:36:20 2016 +0100 @@ -166,7 +166,7 @@ val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*) val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*) -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt); +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt); "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p)); val (mI,m) = mk_tac'_ tac; val Appl m = applicable_in p pt m; @@ -194,7 +194,7 @@ val d = e_rls; (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is; WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*) -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *) val thy = assoc_thy thy'; @@ -216,8 +216,8 @@ val i = mk_Free (i, T); val E = upd_env E (i, v); (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*) -val [(tac_, mout, ptree, pos', xxx)] = ss; -val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)]; +val [(tac_, mout, ctree, pos', xxx)] = ss; +val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)]; (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body ... Assoc ... is correct*) "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) = diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Knowledge/rateq.sml --- a/test/Tools/isac/Knowledge/rateq.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Dec 22 11:36:20 2016 +0100 @@ -92,7 +92,7 @@ val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt; f2str f = "[x = 1 / 5]"; case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*)); -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); val (pt, p) = case locatetac tac (pt,p) of ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac"; "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) @@ -103,7 +103,7 @@ "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = @@ -279,7 +279,7 @@ test --- 'trace_script' from outside 'fun me '--- *) val (pt''', p''') = (pt, p); -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); val (pt, p) = case locatetac tac (pt,p) of ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup"; "~~~~~ step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = @@ -292,7 +292,7 @@ e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*) val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); l = []; (* = false*) "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) = diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 22 11:36:20 2016 +0100 @@ -91,7 +91,7 @@ term2str t = "1 = 2 + -2 * sqrt x"; (*... which works; thus error must be in script interpretation*) -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); val (pt, p) = case locatetac tac (pt,p) of ("ok", (_, _, ptp)) => ptp; "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Minisubpbl/100-init-rootpbl.sml --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Dec 22 11:36:20 2016 +0100 @@ -20,7 +20,7 @@ val hdl = case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t | _ => error "Minisubplb/100-init-rootpbl.sml no headline" -val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) +val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl) val pt = update_ctxt pt [] pctxt ;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Minisubpbl/150-add-given.sml --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Thu Dec 22 11:36:20 2016 +0100 @@ -11,7 +11,7 @@ (*for resuming after stepping into code*) val (p''',f''',nxt''',pt''') = (p,f,nxt,pt); -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ptree)) = (nxt, p, [], pt); +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt); val (pt, p) = case locatetac tac (pt,p) of ("ok", (_, _, ptp)) => ptp; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Minisubpbl/300-init-subpbl.sml --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 22 11:36:20 2016 +0100 @@ -35,7 +35,7 @@ val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*) (*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;*) -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = ((thy',srls), m, (pt,(p,p_)), (sc,d), is); val thy = assoc_thy thy'; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 22 11:36:20 2016 +0100 @@ -64,7 +64,7 @@ "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)), +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); val ctxt = get_ctxt pt pos; val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 22 11:36:20 2016 +0100 @@ -55,7 +55,7 @@ "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip); val thy' = get_obj g_domID pt (par_pblobj pt p); val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*) -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Prog (h $ body)), +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is); val ctxt = get_ctxt pt pos val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}"; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/OLDTESTS/root-equ.sml --- a/test/Tools/isac/OLDTESTS/root-equ.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Thu Dec 22 11:36:20 2016 +0100 @@ -264,7 +264,7 @@ ((#ppc o get_pbt) ["sqroot-test","univariate","equation","test"]); val loc = e_istate; -val (pt,pos) = (e_ptree,[]); +val (pt,pos) = (e_ctree,[]); val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term); val pt = update_branch pt [] TransitiveB; (* @@ -367,7 +367,7 @@ val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete; get_assumptions_ pt ([],Res); -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); (* aus src.24-11-99: . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) 1. sqrt(9+4*x)=sqrt x + sqrt(5+x) @@ -492,7 +492,7 @@ val (p,_,f,nxt,_,pt)= me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt; --- *) -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; *) @@ -632,7 +632,7 @@ then error "root-equ.sml: diff.behav. in me + tacs input" else (); -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^ "\n=============================================================="); diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/OLDTESTS/script.sml --- a/test/Tools/isac/OLDTESTS/script.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/OLDTESTS/script.sml Thu Dec 22 11:36:20 2016 +0100 @@ -238,7 +238,7 @@ (~1,EdUndef,1,Nundef, "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)")) then () else error "behaviour in root-expl. Free_Solve changed"; -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); ---------------------------------meNEW raises exception with not-locatable*) diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/OLDTESTS/scriptnew.sml --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Dec 22 11:36:20 2016 +0100 @@ -294,7 +294,7 @@ (* val nxt = ("End_Proof'",End_Proof');*) val (p,_,f,nxt,_,pt) = me nxt p [1] pt; -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^ "\n============================================================="); (*get_obj g_asm pt []; diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/OLDTESTS/subp-rooteq.sml --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Dec 22 11:36:20 2016 +0100 @@ -359,7 +359,7 @@ else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square"; -writeln (pr_ptree pr_short pt); +writeln (pr_ctree pr_short pt); diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/OLDTESTS/tacis.sml --- a/test/Tools/isac/OLDTESTS/tacis.sml Thu Dec 22 11:12:18 2016 +0100 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Thu Dec 22 11:36:20 2016 +0100 @@ -26,7 +26,7 @@ fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*); autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; fetchProposedTactic 1 (*'Subproblem ...' in tacis*); @@ -58,7 +58,7 @@ fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*); autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; fetchProposedTactic 1 (*'Check_Postcond linear...' in tacis*); @@ -99,14 +99,14 @@ setNextTactic 1 (Rewrite_Set "Test_simplify"); autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; setNextTactic 1 (Subproblem ("Test",["LINEAR","univariate", "equation","test"])); autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; setNextTactic 1 (Model_Problem (*["LINEAR","univariate","equation","test"]*)); @@ -138,7 +138,7 @@ setNextTactic 1 (Check_elementwise "Assumptions"); autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*); val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; + val str = pr_ctree pr_short pt; writeln str; setNextTactic 1 (Check_Postcond