1.1 --- a/doc-isac/mat-eng-de.tex Thu Dec 22 11:12:18 2016 +0100
1.2 +++ b/doc-isac/mat-eng-de.tex Thu Dec 22 11:36:20 2016 +0100
1.3 @@ -856,7 +856,7 @@
1.4 Nd
1.5 (PblObj
1.6 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.7 - result=#,spec=#},[]) : ptree
1.8 + result=#,spec=#},[]) : ctree
1.9 \end{verbatim}}
1.10 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.
1.11 {\footnotesize\begin{verbatim}
1.12 @@ -935,7 +935,7 @@
1.13 Nd
1.14 (PblObj
1.15 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
1.16 - result=#,spec=#},[]) : ptree
1.17 + result=#,spec=#},[]) : ctree
1.18 \end{verbatim}}
1.19 Die me erkennt den richtigen Problem type und arbeitet so weiter:
1.20 {\footnotesize\begin{verbatim}
2.1 --- a/doc-isac/mat-eng-en.tex Thu Dec 22 11:12:18 2016 +0100
2.2 +++ b/doc-isac/mat-eng-en.tex Thu Dec 22 11:36:20 2016 +0100
2.3 @@ -1245,7 +1245,7 @@
2.4
2.5
2.6 \section{Initialize the calculation}
2.7 -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.
2.8 +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.
2.9 {\footnotesize\begin{verbatim}
2.10 ML> val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
2.11 val mID = "Init_Proof" : string
2.12 @@ -1263,9 +1263,9 @@
2.13 Nd
2.14 (PblObj
2.15 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
2.16 - result=#,spec=#},[]) : ptree
2.17 + result=#,spec=#},[]) : ctree
2.18 \end{verbatim}}%size
2.19 -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'}).
2.20 +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'}).
2.21
2.22 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
2.23 {\footnotesize\begin{verbatim}
2.24 @@ -1347,7 +1347,7 @@
2.25 Nd
2.26 (PblObj
2.27 {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
2.28 - result=#,spec=#},[]) : ptree
2.29 + result=#,spec=#},[]) : ctree
2.30 \end{verbatim}}%size
2.31 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.
2.32 {\footnotesize\begin{verbatim}
3.1 --- a/src/Tools/isac/Frontend/states.sml Thu Dec 22 11:12:18 2016 +0100
3.2 +++ b/src/Tools/isac/Frontend/states.sml Thu Dec 22 11:36:20 2016 +0100
3.3 @@ -334,9 +334,9 @@
3.4 > !states;
3.5 val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : states
3.6 > assoc2 (!states, (3, 1));
3.7 -val it = SOME EmptyPtree : ptree option
3.8 +val it = SOME EmptyPtree : ctree option
3.9 > assoc2 (!states, (3, 2));
3.10 -val it = NONE : ptree option
3.11 +val it = NONE : ctree option
3.12 *)
3.13 (*///7.10
3.14 fun add_calc (uI:iterID) (s:state) =
4.1 --- a/src/Tools/isac/Interpret/Interpret.thy Thu Dec 22 11:12:18 2016 +0100
4.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Thu Dec 22 11:36:20 2016 +0100
4.3 @@ -8,6 +8,8 @@
4.4 begin
4.5 ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
4.6 ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
4.7 +
4.8 +
4.9 ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
4.10 ML_file "~~/src/Tools/isac/Interpret/generate.sml"
4.11 ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
5.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Dec 22 11:12:18 2016 +0100
5.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu Dec 22 11:36:20 2016 +0100
5.3 @@ -216,7 +216,7 @@
5.4
5.5
5.6
5.7 -(*.applicability of a tacic wrt. a calc-state (ptree,pos').
5.8 +(*.applicability of a tacic wrt. a calc-state (ctree,pos').
5.9 additionally used by next_tac in the script-interpreter for script-tacs.
5.10 tests for applicability are so expensive, that results (rewrites!)
5.11 are kept in the return-value of 'type tac_'.
6.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:12:18 2016 +0100
6.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:36:20 2016 +0100
6.3 @@ -9,29 +9,29 @@
6.4 type calcstate'
6.5 datatype appl = Appl of Ctree.tac_ | Notappl of string
6.6 val nxt_specify_init_calc : Ctree.fmz -> calcstate
6.7 - val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ptree ->
6.8 - Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ptree
6.9 - val nxt_specif : Ctree.tac -> Ctree.ptree * Ctree.pos' -> calcstate'
6.10 + val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
6.11 + Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Ctree.safe * Ctree.ctree
6.12 + val nxt_specif : Ctree.tac -> Ctree.ctree * Ctree.pos' -> calcstate'
6.13 val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
6.14 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
6.15
6.16 - val reset_calchead : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
6.17 - val get_ocalhd : Ctree.ptree * Ctree.pos' -> Ctree.ocalhd
6.18 + val reset_calchead : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
6.19 + val get_ocalhd : Ctree.ctree * Ctree.pos' -> Ctree.ocalhd
6.20 val ocalhd_complete : itm list -> (bool * term) list -> domID * pblID * metID -> bool
6.21 - val all_modspec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
6.22 + val all_modspec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
6.23
6.24 val complete_metitms : ori list -> itm list -> itm list -> pat list -> itm list
6.25 val insert_ppc' : itm -> itm list -> itm list
6.26
6.27 - val complete_mod : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
6.28 - val is_complete_mod : Ctree.ptree * Ctree.pos' -> bool
6.29 - val complete_spec : Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.pos'
6.30 - val is_complete_spec : Ctree.ptree * Ctree.pos' -> bool
6.31 + val complete_mod : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
6.32 + val is_complete_mod : Ctree.ctree * Ctree.pos' -> bool
6.33 + val complete_spec : Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.pos'
6.34 + val is_complete_spec : Ctree.ctree * Ctree.pos' -> bool
6.35 val some_spec : spec -> spec -> spec
6.36 (* these could go to Ctree ..*)
6.37 - val show_pt : Ctree.ptree -> unit
6.38 - val pt_extract : Ctree.ptree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list
6.39 - val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ptree -> (Ctree.pos' * term) list
6.40 + val show_pt : Ctree.ctree -> unit
6.41 + val pt_extract : Ctree.ctree * Ctree.pos' -> Ctree.ptform * Ctree.tac option * term list
6.42 + val get_interval : Ctree.pos' -> Ctree.pos' -> int -> Ctree.ctree -> (Ctree.pos' * term) list
6.43
6.44 val match_ags : theory -> pat list -> term list -> ori list
6.45 val match_ags_msg : pblID -> term -> term list -> unit
6.46 @@ -68,7 +68,7 @@
6.47 this state just by "fun generate "
6.48 *)
6.49 type calcstate =
6.50 - (ptree * pos') * (* the calc-state to which the tacis could be applied *)
6.51 + (ctree * pos') * (* the calc-state to which the tacis could be applied *)
6.52 (Generate.taci list) (* ev. several (hidden) steps;
6.53 in REVERSE order: first tac_ to apply is last_elem *)
6.54 val e_calcstate = ((EmptyPtree, e_pos'), [Generate.e_taci]) : calcstate;
6.55 @@ -86,7 +86,7 @@
6.56 Generate.taci list * (* cas. several (hidden) steps;
6.57 in REVERSE order: first tac_ to apply is last_elem *)
6.58 pos' list * (* a "continuous" sequence of pos', deleted by application of taci list *)
6.59 - (ptree * pos') (* the calc-state resulting from the application of tacis *)
6.60 + (ctree * pos') (* the calc-state resulting from the application of tacis *)
6.61 val e_calcstate' = ([Generate.e_taci], [e_pos'], (EmptyPtree, e_pos')):calcstate';
6.62
6.63 (* FIXXXME.WN020430 intermediate hack for fun ass_up *)
6.64 @@ -697,7 +697,7 @@
6.65 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
6.66 then ([], e_ctxt)
6.67 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
6.68 - val (pt, _) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz, spec')
6.69 + val (pt, _) = cappend_problem e_ctree [] (e_istate, ctxt) (fmz, spec')
6.70 (oris, (dI',pI',mI'), e_term)
6.71 val pt = update_ctxt pt [] ctxt
6.72 val (pbl, pre) = ([], [])
6.73 @@ -951,7 +951,7 @@
6.74 if pI = e_pblID then opI else pI,
6.75 if mI = e_metID then omI else mI) : spec
6.76
6.77 -(* find a next applicable tac (for calcstate) and update ptree
6.78 +(* find a next applicable tac (for calcstate) and update ctree
6.79 (for ev. finding several more tacs due to hide) *)
6.80 (* FIXXXME: unify ... fun nxt_specif = nxt_spec + applicable_in + specify !! *)
6.81 (* WN.24.10.03 ~~~~~~~~~~~~~~ -> tac -> tac_ -> -"- as arg *)
6.82 @@ -1087,7 +1087,7 @@
6.83 val dI = if dI = "" then theory2theory' thy else dI
6.84 val mI = if mI = [] then hd met else mI
6.85 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
6.86 - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
6.87 + val (pt,_) = cappend_problem e_ctree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
6.88 ([], (dI,pI,mI), hdl)
6.89 val pt = update_spec pt [] (dI, pI, mI)
6.90 val pits = Generate.init_pbl' ppc
6.91 @@ -1100,7 +1100,7 @@
6.92 val {ppc, ...} = Specify.get_met mI
6.93 val dI = if dI = "" then "Isac" else dI
6.94 val (pt, _) =
6.95 - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
6.96 + cappend_problem e_ctree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
6.97 val pt = update_spec pt [] (dI, pI, mI)
6.98 val mits = Generate.init_pbl' ppc
6.99 val pt = update_met pt [] mits
6.100 @@ -1108,7 +1108,7 @@
6.101 else (* new example, pepare for interactive modeling *)
6.102 let
6.103 val (pt, _) =
6.104 - cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
6.105 + cappend_problem e_ctree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
6.106 in ((pt, ([], Pbl)), []) end
6.107 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
6.108 let (* both """"""""""""""""""""""""" either empty or complete *)
6.109 @@ -1129,7 +1129,7 @@
6.110 NONE => pblterm dI pI
6.111 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
6.112 val (pt, _) =
6.113 - cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
6.114 + cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
6.115 val pt = update_ctxt pt [] pctxt
6.116 in
6.117 ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
6.118 @@ -1396,7 +1396,7 @@
6.119 (* continue with trying 'res' only*)
6.120 else get_forms (fs @ [form p nd]) (lev_on p) nds;
6.121
6.122 -(** get an 'interval' 'from' 'to' of formulae from a ptree **)
6.123 +(** get an 'interval' 'from' 'to' of formulae from a ctree **)
6.124 (* WN0401 this functionality belongs to ctree.sml *)
6.125 fun eq_pos' (p1, Frm) (p2, Frm) = p1 = p2
6.126 | eq_pos' (p1, Res) (p2, Res) = p1 = p2
6.127 @@ -1413,7 +1413,7 @@
6.128 pos' -> : to the last element to be returned; from < to
6.129 int -> : level: 0 gets the flattest sub-tree possible
6.130 >999 gets the deepest sub-tree possible
6.131 - ptree -> :
6.132 + ctree -> :
6.133 (pos' * : of the formula
6.134 Term.term) : the formula
6.135 list *)
7.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:12:18 2016 +0100
7.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:36:20 2016 +0100
7.3 @@ -172,31 +172,31 @@
7.4 val pos_plus : int -> pos' -> pos'
7.5 val lev_back' : pos' -> pos' (* for inform.sml *)
7.6
7.7 - datatype ptree = EmptyPtree | Nd of ppobj * ptree list
7.8 - val e_ptree : ptree (* TODO: replace by EmptyPtree*)
7.9 - val existpt' : pos' -> ptree -> bool (* for interface.sml *)
7.10 - val exist_lev_on' : ptree -> pos' -> bool (* for interface.sml *)
7.11 + datatype ctree = EmptyPtree | Nd of ppobj * ctree list
7.12 + val e_ctree : ctree (* TODO: replace by EmptyPtree*)
7.13 + val existpt' : pos' -> ctree -> bool (* for interface.sml *)
7.14 + val exist_lev_on' : ctree -> pos' -> bool (* for interface.sml *)
7.15 val is_interpos : pos' -> bool (* for interface.sml *)
7.16 - val lev_on' : ptree -> pos' -> pos' (* for interface.sml *)
7.17 - val lev_pred' : ptree -> pos' -> pos' (* for interface.sml *)
7.18 - val move_up : pos -> ptree -> pos' -> pos' (* for interface.sml *)
7.19 - val movelevel_dn : pos -> ptree -> pos' -> pos' (* for interface.sml *)
7.20 - val movelevel_up : pos -> ptree -> pos' -> pos' (* for interface.sml *)
7.21 - val movecalchd_up : ptree -> pos' -> pos' (* for interface.sml *)
7.22 - val par_pblobj : ptree -> pos -> pos
7.23 - val ins_chn : ptree list -> ptree -> pos -> ptree (* for solve.sml *)
7.24 - val children : ptree -> ptree list (* for solve.sml *)
7.25 - val get_nd : ptree -> pos -> ptree (* for solve.sml *)
7.26 + val lev_on' : ctree -> pos' -> pos' (* for interface.sml *)
7.27 + val lev_pred' : ctree -> pos' -> pos' (* for interface.sml *)
7.28 + val move_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
7.29 + val movelevel_dn : pos -> ctree -> pos' -> pos' (* for interface.sml *)
7.30 + val movelevel_up : pos -> ctree -> pos' -> pos' (* for interface.sml *)
7.31 + val movecalchd_up : ctree -> pos' -> pos' (* for interface.sml *)
7.32 + val par_pblobj : ctree -> pos -> pos
7.33 + val ins_chn : ctree list -> ctree -> pos -> ctree (* for solve.sml *)
7.34 + val children : ctree -> ctree list (* for solve.sml *)
7.35 + val get_nd : ctree -> pos -> ctree (* for solve.sml *)
7.36 val just_created_ : ppobj -> bool (* for mathengine.sml *)
7.37 - val just_created : ptree * pos' -> bool (* for mathengine.sml *)
7.38 - val is_curr_endof_calc : ptree -> pos' -> bool (* for interface.sml *)
7.39 + val just_created : ctree * pos' -> bool (* for mathengine.sml *)
7.40 + val is_curr_endof_calc : ctree -> pos' -> bool (* for interface.sml *)
7.41 val e_origin : ori list * spec * term (* for mathengine.sml *)
7.42
7.43 - val move_dn : pos -> ptree -> pos' -> pos'
7.44 + val move_dn : pos -> ctree -> pos' -> pos'
7.45 val is_pblobj : ppobj -> bool
7.46 - val is_pblobj' : ptree -> pos -> bool
7.47 - val is_pblnd : ptree -> bool
7.48 - val last_onlev : ptree -> pos -> bool
7.49 + val is_pblobj' : ctree -> pos -> bool
7.50 + val is_pblnd : ctree -> bool
7.51 + val last_onlev : ctree -> pos -> bool
7.52
7.53 val g_spec : ppobj -> spec
7.54 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
7.55 @@ -210,37 +210,37 @@
7.56 val g_env : ppobj -> (istate * Proof.context) option (* for appl.sml *)
7.57
7.58 val g_origin : ppobj -> ori list * spec * term (* for script.sml *)
7.59 - val get_loc : ptree -> pos' -> istate * Proof.context (* for script.sml *)
7.60 - val get_istate : ptree -> pos' -> istate (* for script.sml *)
7.61 - val get_ctxt : ptree -> pos' -> Proof.context
7.62 - val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a
7.63 - val get_curr_formula : ptree * pos' -> term
7.64 - val get_assumptions_ : ptree -> pos' -> term list (* for appl.sml *)
7.65 + val get_loc : ctree -> pos' -> istate * Proof.context (* for script.sml *)
7.66 + val get_istate : ctree -> pos' -> istate (* for script.sml *)
7.67 + val get_ctxt : ctree -> pos' -> Proof.context
7.68 + val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
7.69 + val get_curr_formula : ctree * pos' -> term
7.70 + val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
7.71
7.72 - val append_result : ptree -> pos -> istate * Proof.context -> result ->
7.73 - ostate -> ptree * 'a list
7.74 + val append_result : ctree -> pos -> istate * Proof.context -> result ->
7.75 + ostate -> ctree * 'a list
7.76 val append_atomic : (* for solve.sml *)
7.77 - pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ptree -> ptree
7.78 - val cappend_atomic : ptree -> pos -> istate * Proof.context -> term -> tac -> result ->
7.79 - ostate -> ptree * pos' list
7.80 - val cappend_form : ptree -> pos -> istate * Proof.context -> term -> ptree * pos' list
7.81 - val cappend_problem : ptree -> pos -> istate * Proof.context -> fmz ->
7.82 - ori list * spec * term -> ptree * pos' list
7.83 + pos -> istate * Proof.context -> term -> tac -> result -> ostate -> ctree -> ctree
7.84 + val cappend_atomic : ctree -> pos -> istate * Proof.context -> term -> tac -> result ->
7.85 + ostate -> ctree * pos' list
7.86 + val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
7.87 + val cappend_problem : ctree -> pos -> istate * Proof.context -> fmz ->
7.88 + ori list * spec * term -> ctree * pos' list
7.89
7.90 - val update_branch : ptree -> pos -> branch -> ptree
7.91 - val update_ctxt : ptree -> pos -> Proof.context -> ptree
7.92 - val update_env : ptree -> pos -> (istate * Proof.context) option -> ptree
7.93 - val update_oris : ptree -> pos -> ori list -> ptree
7.94 - val update_orispec : ptree -> pos -> spec -> ptree
7.95 - val update_pbl : ptree -> pos -> itm list -> ptree
7.96 - val update_pblppc : ptree -> pos -> itm list -> ptree (* =vvv= ? *)
7.97 - val update_pblID : ptree -> pos -> pblID -> ptree (* =^^^= ? *)
7.98 - val update_met : ptree -> pos -> itm list -> ptree (* =vvv= ? *)
7.99 - val update_metppc : ptree -> pos -> itm list -> ptree (* =^^^= ? *)
7.100 - val update_metID : ptree -> pos -> metID -> ptree
7.101 - val update_domID : ptree -> pos -> domID -> ptree
7.102 - val update_spec : ptree -> pos -> spec -> ptree
7.103 - val update_tac : ptree -> pos -> tac -> ptree
7.104 + val update_branch : ctree -> pos -> branch -> ctree
7.105 + val update_ctxt : ctree -> pos -> Proof.context -> ctree
7.106 + val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
7.107 + val update_oris : ctree -> pos -> ori list -> ctree
7.108 + val update_orispec : ctree -> pos -> spec -> ctree
7.109 + val update_pbl : ctree -> pos -> itm list -> ctree
7.110 + val update_pblppc : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
7.111 + val update_pblID : ctree -> pos -> pblID -> ctree (* =^^^= ? *)
7.112 + val update_met : ctree -> pos -> itm list -> ctree (* =vvv= ? *)
7.113 + val update_metppc : ctree -> pos -> itm list -> ctree (* =^^^= ? *)
7.114 + val update_metID : ctree -> pos -> metID -> ctree
7.115 + val update_domID : ctree -> pos -> domID -> ctree
7.116 + val update_spec : ctree -> pos -> spec -> ctree
7.117 + val update_tac : ctree -> pos -> tac -> ctree
7.118
7.119 val e_ctxt : Proof.context
7.120 val is_e_ctxt : Proof.context -> bool (* for appl.sml *)
7.121 @@ -252,34 +252,34 @@
7.122 val get_somespec' : spec -> spec -> spec
7.123 exception PTREE of string;
7.124 (* for appl.sml *)
7.125 - val par_pbl_det : ptree -> pos -> bool * pos * rls
7.126 + val par_pbl_det : ctree -> pos -> bool * pos * rls
7.127 (* for rewtools.sml *)
7.128 val rule2tac : theory -> (term * term) list -> rule -> tac
7.129 val eq_tac : tac * tac -> bool
7.130 (* for script.sml *)
7.131 - val rootthy : ptree -> theory
7.132 + val rootthy : ctree -> theory
7.133 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.134 - val update_loc' : ptree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ptree
7.135 - val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ptree -> ptree
7.136 + val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
7.137 + val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
7.138 val g_res : ppobj -> term
7.139 - val pr_ptree : (pos -> ppobj -> string) -> ptree -> string
7.140 + val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
7.141 val pr_short : pos -> ppobj -> string
7.142 - val existpt : pos -> ptree -> bool
7.143 + val existpt : pos -> ctree -> bool
7.144 val is_empty_tac : tac -> bool
7.145 val e_subs : string list
7.146 val e_sube : cterm' list
7.147 val g_branch : ppobj -> branch
7.148 val g_ctxt : ppobj -> Proof.context
7.149 val g_fmz : ppobj -> fmz
7.150 - val get_allp : pos' list -> pos * (int list * pos_) -> ptree -> pos' list
7.151 - val get_allps : (pos * pos_) list -> posel list -> ptree list -> pos' list
7.152 - val get_allpos' : pos * posel -> ptree -> pos' list
7.153 - val get_allpos's : pos * posel -> ptree list -> (pos * pos_) list
7.154 - val cut_bottom : pos * posel -> ptree -> (ptree * pos' list) * bool
7.155 - val cut_tree : ptree -> pos * 'a -> ptree * pos' list
7.156 - val cut_level : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list
7.157 - val cut_level_'_ : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list
7.158 - val get_trace : ptree -> int list -> int list -> int list list
7.159 + val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
7.160 + val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
7.161 + val get_allpos' : pos * posel -> ctree -> pos' list
7.162 + val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
7.163 + val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
7.164 + val cut_tree : ctree -> pos * 'a -> ctree * pos' list
7.165 + val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
7.166 + val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
7.167 + val get_trace : ctree -> int list -> int list -> int list list
7.168 val subte2subst : term list -> (term * term) list
7.169 val branch2str : branch -> string
7.170 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.171 @@ -289,41 +289,41 @@
7.172 sig
7.173 val Ets : ets exception PTREE of string
7.174 val append_atomic :
7.175 - pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ptree -> ptree
7.176 - val append_form : int list -> istate * Proof.context -> term -> ptree -> ptree
7.177 - val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ptree -> ptree
7.178 - val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ptree -> ptree
7.179 - val append_result : ptree -> pos -> istate * Proof.context -> term * term list -> ostate -> ptree * 'a list
7.180 - val appl_branch : (ppobj -> bool) * (posel -> ptree list -> ptree list) -> ptree -> int list -> ptree * bool
7.181 - val appl_obj : (ppobj -> ppobj) -> ptree -> pos -> ptree
7.182 - val appl_to_node : (ppobj -> ppobj) -> ptree -> ptree
7.183 + pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree -> ctree
7.184 + val append_form : int list -> istate * Proof.context -> term -> ctree -> ctree
7.185 + val append_parent : pos -> istate * Proof.context -> term -> tac -> branch -> ctree -> ctree
7.186 + val append_problem : int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree -> ctree
7.187 + val append_result : ctree -> pos -> istate * Proof.context -> term * term list -> ostate -> ctree * 'a list
7.188 + val appl_branch : (ppobj -> bool) * (posel -> ctree list -> ctree list) -> ctree -> int list -> ctree * bool
7.189 + val appl_obj : (ppobj -> ppobj) -> ctree -> pos -> ctree
7.190 + val appl_to_node : (ppobj -> ppobj) -> ctree -> ctree
7.191 datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB
7.192 val branch2str : branch -> string
7.193 val cappend_atomic :
7.194 - ptree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ptree * pos' list
7.195 - val cappend_form : ptree -> pos -> istate * Proof.context -> term -> ptree * pos' list
7.196 - val cappend_parent : ptree -> pos -> istate * Proof.context -> term -> tac -> branch -> ptree * pos' list
7.197 + ctree -> pos -> istate * Proof.context -> term -> tac -> term * term list -> ostate -> ctree * pos' list
7.198 + val cappend_form : ctree -> pos -> istate * Proof.context -> term -> ctree * pos' list
7.199 + val cappend_parent : ctree -> pos -> istate * Proof.context -> term -> tac -> branch -> ctree * pos' list
7.200 val cappend_problem :
7.201 - ptree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ptree * pos' list
7.202 + ctree -> int list -> istate * Proof.context -> fmz -> ori list * spec * term -> ctree * pos' list
7.203 eqtype cellID
7.204 - val children : ptree -> ptree list
7.205 + val children : ctree -> ctree list
7.206 type cid = cellID list
7.207 datatype con = land | lor
7.208 - val cut_bottom : pos * posel -> ptree -> (ptree * pos' list) * bool
7.209 - val cut_level : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list
7.210 - val cut_level_'_ : pos' list -> pos -> ptree -> int list * pos_ -> ptree * pos' list
7.211 - val cut_levup : pos' list -> bool -> ptree -> ptree -> posel list * posel -> ptree -> ptree * pos' list
7.212 - val cut_tree : ptree -> pos * 'a -> ptree * pos' list
7.213 + val cut_bottom : pos * posel -> ctree -> (ctree * pos' list) * bool
7.214 + val cut_level : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
7.215 + val cut_level_'_ : pos' list -> pos -> ctree -> int list * pos_ -> ctree * pos' list
7.216 + val cut_levup : pos' list -> bool -> ctree -> ctree -> posel list * posel -> ctree -> ctree * pos' list
7.217 + val cut_tree : ctree -> pos * 'a -> ctree * pos' list
7.218 val cutlevup : ppobj -> bool
7.219 val del_res : ppobj -> ppobj
7.220 - val delete_result : ptree -> pos -> ptree
7.221 + val delete_result : ctree -> pos -> ctree
7.222 val e_ctxt : Proof.context
7.223 val e_fmz : 'a list * spec
7.224 val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec
7.225 val e_origin : ori list * spec * term
7.226 val e_ptform : ptform
7.227 val e_ptform' : ptform
7.228 - val e_ptree : ptree
7.229 + val e_ctree : ctree
7.230 val e_scrstate : scrstate
7.231 val e_sube : cterm' list
7.232 val e_subs : string list
7.233 @@ -333,9 +333,9 @@
7.234 val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list
7.235 val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string
7.236 val ets2str : ets -> string
7.237 - val exist_lev_on' : ptree -> pos' -> bool
7.238 - val existpt : pos -> ptree -> bool
7.239 - val existpt' : pos' -> ptree -> bool
7.240 + val exist_lev_on' : ctree -> pos' -> bool
7.241 + val existpt : pos -> ctree -> bool
7.242 + val existpt' : pos' -> ctree -> bool
7.243 type fmz = fmz_ * spec
7.244 type fmz_ = cterm' list
7.245 val g_branch : ppobj -> branch
7.246 @@ -345,48 +345,48 @@
7.247 val g_env : ppobj -> (istate * Proof.context) option
7.248 val g_fmz : ppobj -> fmz
7.249 val g_form : ppobj -> term
7.250 - val g_form' : ptree -> term
7.251 + val g_form' : ctree -> term
7.252 val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option
7.253 val g_met : ppobj -> itm list
7.254 val g_metID : ppobj -> metID
7.255 val g_origin : ppobj -> ori list * spec * term
7.256 val g_ostate : ppobj -> ostate
7.257 - val g_ostate' : ptree -> ostate
7.258 + val g_ostate' : ctree -> ostate
7.259 val g_pbl : ppobj -> itm list
7.260 val g_res : ppobj -> term
7.261 - val g_res' : ptree -> term
7.262 + val g_res' : ctree -> term
7.263 val g_result : ppobj -> term * term list
7.264 val g_spec : ppobj -> spec
7.265 val g_tac : ppobj -> tac
7.266 - val get_all : (ppobj -> 'a) -> ptree -> 'a list
7.267 - val get_allp : pos' list -> pos * (int list * pos_) -> ptree -> pos' list
7.268 - val get_allpos' : pos * posel -> ptree -> pos' list
7.269 - val get_allpos's : pos * posel -> ptree list -> (pos * pos_) list
7.270 - val get_allps : (pos * pos_) list -> posel list -> ptree list -> pos' list
7.271 - val get_alls : (ppobj -> 'a) -> ptree list -> 'a list
7.272 - val get_assumptions_ : ptree -> pos * pos_ -> term list
7.273 - val get_ctxt : ptree -> pos * pos_ -> Proof.context
7.274 - val get_curr_formula : ptree * (pos * pos_) -> term
7.275 - val get_istate : ptree -> pos * pos_ -> istate
7.276 - val get_loc : ptree -> pos * pos_ -> istate * Proof.context
7.277 - val get_nd : ptree -> pos -> ptree
7.278 - val get_obj : (ppobj -> 'a) -> ptree -> pos -> 'a
7.279 + val get_all : (ppobj -> 'a) -> ctree -> 'a list
7.280 + val get_allp : pos' list -> pos * (int list * pos_) -> ctree -> pos' list
7.281 + val get_allpos' : pos * posel -> ctree -> pos' list
7.282 + val get_allpos's : pos * posel -> ctree list -> (pos * pos_) list
7.283 + val get_allps : (pos * pos_) list -> posel list -> ctree list -> pos' list
7.284 + val get_alls : (ppobj -> 'a) -> ctree list -> 'a list
7.285 + val get_assumptions_ : ctree -> pos * pos_ -> term list
7.286 + val get_ctxt : ctree -> pos * pos_ -> Proof.context
7.287 + val get_curr_formula : ctree * (pos * pos_) -> term
7.288 + val get_istate : ctree -> pos * pos_ -> istate
7.289 + val get_loc : ctree -> pos * pos_ -> istate * Proof.context
7.290 + val get_nd : ctree -> pos -> ctree
7.291 + val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
7.292 val get_somespec : spec -> spec -> spec
7.293 val get_somespec' : spec -> spec -> spec
7.294 - val get_trace : ptree -> int list -> int list -> int list list
7.295 - val gpt_cell : ptree -> lrd option
7.296 + val get_trace : ctree -> int list -> int list -> int list list
7.297 + val gpt_cell : ctree -> lrd option
7.298 type iist = istate option * istate option
7.299 val ind : pos' -> int
7.300 - val ins_chn : ptree list -> ptree -> int list -> ptree
7.301 + val ins_chn : ctree list -> ctree -> int list -> ctree
7.302 val ins_nth : int -> 'a -> 'a list -> 'a list
7.303 - val insert_pt : ppobj -> ptree -> int list -> ptree
7.304 - val is_curr_endof_calc : ptree -> pos' -> bool
7.305 + val insert_pt : ppobj -> ctree -> int list -> ctree
7.306 + val is_curr_endof_calc : ctree -> pos' -> bool
7.307 val is_e_ctxt : Proof.context -> bool
7.308 val is_empty_tac : tac -> bool
7.309 val is_interpos : pos' -> bool
7.310 - val is_pblnd : ptree -> bool
7.311 + val is_pblnd : ctree -> bool
7.312 val is_pblobj : ppobj -> bool
7.313 - val is_pblobj' : ptree -> pos -> bool
7.314 + val is_pblobj' : ctree -> pos -> bool
7.315 val is_prfobj : ppobj -> bool
7.316 val is_rewset : tac -> bool
7.317 val is_rewtac : tac -> bool
7.318 @@ -394,35 +394,35 @@
7.319 datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
7.320 val istate2str : istate -> string
7.321 val istates2str : istate option * istate option -> string
7.322 - val just_created : ptree * pos' -> bool
7.323 + val just_created : ctree * pos' -> bool
7.324 val just_created_ : ppobj -> bool
7.325 - val last_onlev : ptree -> pos -> bool
7.326 + val last_onlev : ctree -> pos -> bool
7.327 val lev_back' : pos' -> pos'
7.328 val lev_dn : posel list -> posel list
7.329 val lev_dnRes : pos' -> pos'
7.330 val lev_dn_ : pos' -> pos'
7.331 val lev_of : pos' -> int
7.332 val lev_on : pos -> posel list
7.333 - val lev_on' : ptree -> pos' -> pos'
7.334 + val lev_on' : ctree -> pos' -> pos'
7.335 val lev_onFrm : pos' -> pos'
7.336 val lev_pred : pos -> pos
7.337 - val lev_pred' : ptree -> pos' -> pos'
7.338 + val lev_pred' : ctree -> pos' -> pos'
7.339 val lev_up : pos -> pos
7.340 val lev_up_ : pos' -> pos'
7.341 - val move_dn : pos -> ptree -> int list * pos_ -> int list * pos_
7.342 - val move_up : int list -> ptree -> int list * pos_ -> int list * pos_
7.343 - val movecalchd_up : ptree -> pos' -> pos'
7.344 - val movelevel_dn : int list -> ptree -> int list * pos_ -> int list * pos_
7.345 - val movelevel_up : int list -> ptree -> int list * pos_ -> int list * pos_
7.346 + val move_dn : pos -> ctree -> int list * pos_ -> int list * pos_
7.347 + val move_up : int list -> ctree -> int list * pos_ -> int list * pos_
7.348 + val movecalchd_up : ctree -> pos' -> pos'
7.349 + val movelevel_dn : int list -> ctree -> int list * pos_ -> int list * pos_
7.350 + val movelevel_up : int list -> ctree -> int list * pos_ -> int list * pos_
7.351 val new_val : term -> istate -> istate
7.352 val nth : int -> 'a list -> 'a
7.353 type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec
7.354 val ocalhd2str : ocalhd -> string
7.355 datatype ostate = Complete | Incomplete | Inconsistent
7.356 val ostate2str : ostate -> string
7.357 - val par_children : ptree -> pos -> ptree list * pos
7.358 - val par_pbl_det : ptree -> pos -> bool * pos * rls
7.359 - val par_pblobj : ptree -> pos -> pos
7.360 + val par_children : ctree -> pos -> ctree list * pos
7.361 + val par_pbl_det : ctree -> pos -> bool * pos * rls
7.362 + val par_pblobj : ctree -> pos -> pos
7.363 type pos = posel list
7.364 type pos' = pos * pos_
7.365 val pos's2str : (int list * pos_) list -> string
7.366 @@ -449,12 +449,12 @@
7.367 loc: (istate * Proof.context) option * (istate * Proof.context) option,
7.368 ostate: ostate, result: term * term list, tac: tac}
7.369 val pr_pos : int list -> string
7.370 - val pr_ptree : (pos -> ppobj -> string) -> ptree -> string
7.371 + val pr_ctree : (pos -> ppobj -> string) -> ctree -> string
7.372 val pr_short : pos -> ppobj -> string
7.373 val pre_pos : pos -> pos
7.374 val preconds2str : (bool * term) list -> string
7.375 datatype ptform = Form of term | ModSpec of ocalhd
7.376 - datatype ptree = EmptyPtree | Nd of ppobj * ptree list
7.377 + datatype ctree = EmptyPtree | Nd of ppobj * ctree list
7.378 val rep_pblobj :
7.379 ppobj ->
7.380 {branch: branch,
7.381 @@ -494,7 +494,7 @@
7.382 val res2str : term * term list -> string
7.383 val rls_of : tac -> rls'
7.384 val rls_of_rewset : tac -> rls' * subst option
7.385 - val rootthy : ptree -> theory
7.386 + val rootthy : ctree -> theory
7.387 val rta2str : rule * (term * term list) -> string
7.388 val rule2tac : theory -> (term * term) list -> rule -> tac
7.389 val safe2str : safe -> string
7.390 @@ -558,21 +558,21 @@
7.391 val test_trans : ppobj -> bool
7.392 val thm_of_rew : tac -> thmID * subst option
7.393 val topt2str : term option -> string
7.394 - val update_branch : ptree -> pos -> branch -> ptree
7.395 - val update_ctxt : ptree -> pos -> Proof.context -> ptree
7.396 - val update_domID : ptree -> pos -> domID -> ptree
7.397 - val update_env : ptree -> pos -> (istate * Proof.context) option -> ptree
7.398 - val update_loc' : ptree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ptree
7.399 - val update_met : ptree -> pos -> itm list -> ptree
7.400 - val update_metID : ptree -> pos -> metID -> ptree
7.401 - val update_metppc : ptree -> pos -> itm list -> ptree
7.402 - val update_oris : ptree -> pos -> ori list -> ptree
7.403 - val update_orispec : ptree -> pos -> spec -> ptree
7.404 - val update_pbl : ptree -> pos -> itm list -> ptree
7.405 - val update_pblID : ptree -> pos -> pblID -> ptree
7.406 - val update_pblppc : ptree -> pos -> itm list -> ptree
7.407 - val update_spec : ptree -> pos -> spec -> ptree
7.408 - val update_tac : ptree -> pos -> tac -> ptree end
7.409 + val update_branch : ctree -> pos -> branch -> ctree
7.410 + val update_ctxt : ctree -> pos -> Proof.context -> ctree
7.411 + val update_domID : ctree -> pos -> domID -> ctree
7.412 + val update_env : ctree -> pos -> (istate * Proof.context) option -> ctree
7.413 + val update_loc' : ctree -> pos -> (istate * Proof.context) option * (istate * Proof.context) option -> ctree
7.414 + val update_met : ctree -> pos -> itm list -> ctree
7.415 + val update_metID : ctree -> pos -> metID -> ctree
7.416 + val update_metppc : ctree -> pos -> itm list -> ctree
7.417 + val update_oris : ctree -> pos -> ori list -> ctree
7.418 + val update_orispec : ctree -> pos -> spec -> ctree
7.419 + val update_pbl : ctree -> pos -> itm list -> ctree
7.420 + val update_pblID : ctree -> pos -> pblID -> ctree
7.421 + val update_pblppc : ctree -> pos -> itm list -> ctree
7.422 + val update_spec : ctree -> pos -> spec -> ctree
7.423 + val update_tac : ctree -> pos -> tac -> ctree end
7.424 *)
7.425
7.426 (**)
7.427 @@ -629,7 +629,7 @@
7.428 | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)
7.429
7.430 type pos' = pos * pos_;
7.431 -(*WN0312 remembering interator (pos * pos_) for ptree
7.432 +(*WN0312 remembering interator (pos * pos_) for ctree
7.433 pos : lev_on, lev_dn, lev_up,
7.434 lev_onFrm, lev_dnRes (..see solve Apply_Method !)
7.435 pos_:
7.436 @@ -1159,7 +1159,7 @@
7.437 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;
7.438
7.439
7.440 -type envp =(*9.5.03: unused, delete with field in ptree.PblObj FIXXXME*)
7.441 +type envp =(*9.5.03: unused, delete with field in ctree.PblObj FIXXXME*)
7.442 (int * term list) list * (*assoc-list: args of met*)
7.443 (int * rls) list * (*assoc-list: tacs already done ///15.9.00*)
7.444 (int * ets) list * (*assoc-list: tacs etc. already done*)
7.445 @@ -1212,11 +1212,11 @@
7.446 but it is crucial if the first tactic in a script is eg. 'Subproblem';
7.447 see 'type tac ', Apply_Method.
7.448 .*)
7.449 -datatype ptree =
7.450 +datatype ctree =
7.451 EmptyPtree
7.452 - | Nd of ppobj * (ptree list);
7.453 -val e_ptree = EmptyPtree;
7.454 -type state = ptree * pos
7.455 + | Nd of ppobj * (ctree list);
7.456 +val e_ctree = EmptyPtree;
7.457 +type state = ctree * pos
7.458
7.459 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =
7.460 {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};
7.461 @@ -1279,7 +1279,7 @@
7.462 fun lev_of (p,_) = length p;
7.463
7.464
7.465 -(** convert ptree to a string **)
7.466 +(** convert ctree to a string **)
7.467
7.468 (* convert a pos from list to string *)
7.469 fun pr_pos ps = (space_implode "." (map string_of_int ps))^". ";
7.470 @@ -1301,8 +1301,8 @@
7.471 ((ints2str c) ^" "^ (term2str form) ^ "\n");
7.472 *)
7.473
7.474 -(* convert ptree *)
7.475 -fun pr_ptree f pt =
7.476 +(* convert ctree *)
7.477 +fun pr_ctree f pt =
7.478 let
7.479 fun pr_pt pfn _ EmptyPtree = ""
7.480 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
7.481 @@ -1321,11 +1321,11 @@
7.482 [Nd("xx2.1.",[]),
7.483 Nd("xx2.2.",[])]),
7.484 Nd("xx3",[])]);
7.485 -> tracing (pr_ptree prfn (!pt));
7.486 +> tracing (pr_ctree prfn (!pt));
7.487 *)
7.488
7.489
7.490 -(** access the branches of ptree **)
7.491 +(** access the branches of ctree **)
7.492
7.493 fun ins_nth 1 e l = e::l
7.494 | ins_nth n e [] = raise PTREE "ins_nth n e []"
7.495 @@ -1450,7 +1450,7 @@
7.496 fun last_onlev pt pos = not (existpt (lev_on pos) pt);
7.497
7.498
7.499 -(*.find the position of the next parent which is a PblObj in ptree.*)
7.500 +(*.find the position of the next parent which is a PblObj in ctree.*)
7.501 fun par_pblobj pt [] = []
7.502 | par_pblobj pt p =
7.503 let fun par pt [] = []
7.504 @@ -1468,7 +1468,7 @@
7.505 end;
7.506 in par (lev_up p) end;
7.507
7.508 -(*.get the children of a node in ptree.*)
7.509 +(*.get the children of a node in ctree.*)
7.510 fun children (Nd (PblObj _, cn)) = cn
7.511 | children (Nd (PrfObj _, cn)) = cn;
7.512
7.513 @@ -1492,7 +1492,7 @@
7.514
7.515
7.516
7.517 -(*.get from the whole ptree by f : ppobj -> 'a.*)
7.518 +(*.get from the whole ctree by f : ppobj -> 'a.*)
7.519 fun get_all f EmptyPtree = []
7.520 | get_all f (Nd (b, [])) = [f b]
7.521 | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)
7.522 @@ -1500,7 +1500,7 @@
7.523 | get_alls f pts = flat (map (get_all f) pts);
7.524
7.525
7.526 -(*.insert obj b into ptree at pos, ev.overwriting this pos.
7.527 +(*.insert obj b into ctree at pos, ev.overwriting this pos.
7.528 covers library.ML TODO.WN110315 rename*)
7.529 fun insert_pt b EmptyPtree [] = Nd (b, [])
7.530 | insert_pt b EmptyPtree _ = raise PTREE "insert_pt b Empty _"
7.531 @@ -1511,7 +1511,7 @@
7.532 Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));
7.533 (*
7.534 > type ppobj = string;
7.535 -> tracing (pr_ptree prfn (!pt));
7.536 +> tracing (pr_ctree prfn (!pt));
7.537 (*val pt = Unsynchronized.ref Empty;*)
7.538 pt:= insert_pt ("root'":ppobj) EmptyPtree [];
7.539 pt:= insert_pt ("xx1":ppobj) (!pt) [1];
7.540 @@ -1677,7 +1677,7 @@
7.541 val e_ptform' = ModSpec e_ocalhd;
7.542
7.543 (*.applies (snd f) to the branches at a pos if ((fst f) b),
7.544 - f : (ppobj -> bool) * (int -> ptree list -> ptree list).*)
7.545 + f : (ppobj -> bool) * (int -> ctree list -> ctree list).*)
7.546
7.547 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)
7.548 | appl_branch f EmptyPtree _ = raise PTREE "appl_branch f Empty _"
7.549 @@ -1777,7 +1777,7 @@
7.550 +++ see Isabelle/../library.ML*)
7.551
7.552
7.553 -(**.development for extracting an 'interval' from ptree.**)
7.554 +(**.development for extracting an 'interval' from ctree.**)
7.555
7.556 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo
7.557 actually used (inefficient) version with move_dn: see modspec.sml*)
7.558 @@ -1812,7 +1812,7 @@
7.559 (getnd i ( b,[0]) [99999] nd) @
7.560 (getnds ~99999 false (lev_on b,[0]) q nds);
7.561 in
7.562 -(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
7.563 +(*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
7.564 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
7.565 (1) the 'f' are given
7.566 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
7.567 @@ -1849,7 +1849,7 @@
7.568 val metID = if mI = e_metID then mI' else mI
7.569 in (domID, pblID, metID) end;
7.570
7.571 -(*extract a formula or model from ptree for itms2itemppc or model2xml*)
7.572 +(*extract a formula or model from ctree for itms2itemppc or model2xml*)
7.573 fun preconds2str bts =
7.574 (strs2str o (map (linefeed o pair2str o
7.575 (apsnd term2str) o
7.576 @@ -1864,9 +1864,9 @@
7.577 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
7.578
7.579
7.580 -(**.functions for the 'ptree iterator' as seen from the FE-Kernel interface.**)
7.581 +(**.functions for the 'ctree iterator' as seen from the FE-Kernel interface.**)
7.582
7.583 -(*move one step down into existing nodes of ptree; regard TransitiveB
7.584 +(*move one step down into existing nodes of ctree; regard TransitiveB
7.585 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################
7.586 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
7.587 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);
7.588 @@ -1936,7 +1936,7 @@
7.589 else (P@[p+1], if is_pblnd (nth (p+1) ns)
7.590 then Pbl else Frm);
7.591 *)
7.592 -(*.move one step down into existing nodes of ptree; skip Res = Frm.nxt;
7.593 +(*.move one step down into existing nodes of ctree; skip Res = Frm.nxt;
7.594 move_dn at the end of the calc-tree raises PTREE.*)
7.595 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)
7.596 (case p_ of
7.597 @@ -1980,7 +1980,7 @@
7.598 then Pbl else Frm);
7.599
7.600
7.601 -(*.go one level down into ptree.*)
7.602 +(*.go one level down into ctree.*)
7.603 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)
7.604 if is_pblobj c
7.605 then if null ns
7.606 @@ -2017,7 +2017,7 @@
7.607
7.608
7.609
7.610 -(*.go to the previous position in ptree; regard TransitiveB.*)
7.611 +(*.go to the previous position in ctree; regard TransitiveB.*)
7.612 fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*)
7.613 if is_pblobj c
7.614 then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)
7.615 @@ -2048,7 +2048,7 @@
7.616
7.617
7.618
7.619 -(*.go one level up in ptree; sets the position on Frm.*)
7.620 +(*.go one level up in ctree; sets the position on Frm.*)
7.621 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)
7.622 raise PTREE "pos not existent"
7.623
7.624 @@ -2110,8 +2110,8 @@
7.625
7.626 (*.get all positions of certain intervals on the ctree.*)
7.627 (*OLD VERSION without move_dn; kept for occasional redesign
7.628 - get all pos's to be cut in a ptree
7.629 - below a pos or from a ptree list after i-th element (NO level_up).*)
7.630 + get all pos's to be cut in a ctree
7.631 + below a pos or from a ctree list after i-th element (NO level_up).*)
7.632 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
7.633 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
7.634 if g_ostate b = Incomplete
7.635 @@ -2143,7 +2143,7 @@
7.636 (*.cut branches.*)
7.637 (*before WN041019......
7.638 val cut_branch = (test_trans, curry take):
7.639 - (ppobj -> bool) * (int -> ptree list -> ptree list);
7.640 + (ppobj -> bool) * (int -> ctree list -> ctree list);
7.641 .. formlery used for ...
7.642 fun cut_tree''' _ [] = EmptyPtree
7.643 | cut_tree''' pt pos =
7.644 @@ -2211,11 +2211,11 @@
7.645
7.646 (*########/ inserted from ctreeNEW.sml \#################################**)
7.647
7.648 -(*.get all positions in a ptree until ([],Res) or ostate=Incomplete
7.649 +(*.get all positions in a ctree until ([],Res) or ostate=Incomplete
7.650 val get_allp = fn :
7.651 pos' list -> : accumulated, start with []
7.652 pos -> : the offset for subtrees wrt the root
7.653 - ptree -> : (sub)tree
7.654 + ctree -> : (sub)tree
7.655 pos' : initialization (the last pos' before ...)
7.656 -> pos' list : of positions in this (sub) tree (relative to the root)
7.657 .*)
7.658 @@ -2261,11 +2261,11 @@
7.659 (*cut_bottom new sml603..608
7.660 cut the level at the bottom of the pos (used by cappend_...)
7.661 and handle the parent in order to avoid extra case for root
7.662 -fn: ptree -> : the _whole_ ptree for cut_levup
7.663 +fn: ctree -> : the _whole_ ctree for cut_levup
7.664 pos * posel -> : the pos after split_last
7.665 - ptree -> : the parent of the Nd to be cut
7.666 + ctree -> : the parent of the Nd to be cut
7.667 return
7.668 - (ptree * : the updated ptree
7.669 + (ctree * : the updated ctree
7.670 pos' list) * : the pos's cut
7.671 bool : cutting shall be continued on the higher level(s)
7.672 *)
7.673 @@ -2305,12 +2305,12 @@
7.674 args
7.675 pos' list -> : for accumulation
7.676 bool -> : cutting shall be continued on the higher level(s)
7.677 - ptree -> : the whole ptree for 'get_nd pt P' on each level
7.678 - ptree -> : the Nd from the lower level for insertion at path
7.679 + ctree -> : the whole ctree for 'get_nd pt P' on each level
7.680 + ctree -> : the Nd from the lower level for insertion at path
7.681 pos * posel -> : pos=path split for convenience
7.682 - ptree -> : Nd the children of are under consideration on this call
7.683 + ctree -> : Nd the children of are under consideration on this call
7.684 returns :
7.685 - ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
7.686 + ctree * pos' list : the updated parent-Nd and the pos's of the Nds cut
7.687 .*)
7.688 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
7.689 let (*divide level into 3 parts...*)
8.1 --- a/src/Tools/isac/Interpret/generate.sml Thu Dec 22 11:12:18 2016 +0100
8.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu Dec 22 11:36:20 2016 +0100
8.3 @@ -17,17 +17,17 @@
8.4 | PpcKF of pblmet * item ppc
8.5 | RefinedKF of pblID * (itm list * (bool * term) list)
8.6 val generate1 : theory -> Ctree.tac_ -> Ctree.istate * Proof.context ->
8.7 - Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree (* for calchead.sml------------- ^^^ *)
8.8 + Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree (* for calchead.sml------------- ^^^ *)
8.9 val init_istate : Ctree.tac -> term -> Ctree.istate (* for solve.sml *)
8.10 val init_pbl : (string * (term * 'a)) list -> itm list
8.11 val init_pbl' : (string * (term * term)) list -> itm list
8.12 - val embed_deriv : taci list -> Ctree.ptree * Ctree.pos' -> Ctree.pos' list * (Ctree.ptree * Ctree.pos') (* for inform.sml *)
8.13 + val embed_deriv : taci list -> Ctree.ctree * Ctree.pos' -> Ctree.pos' list * (Ctree.ctree * Ctree.pos') (* for inform.sml *)
8.14 val generate_hard : (* for solve.sml *)
8.15 - theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ptree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ptree
8.16 + theory -> Ctree.tac_ -> Ctree.pos' -> Ctree.ctree -> Ctree.pos' * Ctree.pos' list * mout * Ctree.ctree
8.17 val generate : (Ctree.tac * Ctree.tac_ * (Ctree.pos' * (Ctree.istate * Proof.context))) list ->
8.18 - Ctree.ptree * Ctree.pos' list * Ctree.pos' -> Ctree.ptree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
8.19 + Ctree.ctree * Ctree.pos' list * Ctree.pos' -> Ctree.ctree * Ctree.pos' list * Ctree.pos' (* for mathengine.sml *)
8.20 val generate_inconsistent_rew : Ctree.subs option * thm'' -> term -> Ctree.istate * Proof.context ->
8.21 - Ctree.pos' -> Ctree.ptree -> Ctree.ptree * Ctree.pos' (* for interface.sml *)
8.22 + Ctree.pos' -> Ctree.ctree -> Ctree.ctree * Ctree.pos' (* for interface.sml *)
8.23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.25 end
8.26 @@ -86,9 +86,9 @@
8.27 not any more used for the specify-phase and for changing the phases*)
8.28 type taci =
8.29 (tac * (* for comparison with input tac *)
8.30 - tac_ * (* for ptree generation *)
8.31 - (pos' * (* after applying tac_, for ptree generation *)
8.32 - (istate * Proof.context))) (* after applying tac_, for ptree generation *)
8.33 + tac_ * (* for ctree generation *)
8.34 + (pos' * (* after applying tac_, for ctree generation *)
8.35 + (istate * Proof.context))) (* after applying tac_, for ctree generation *)
8.36 val e_taci = (Empty_Tac, Empty_Tac_, (e_pos', (e_istate, e_ctxt))): taci
8.37 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
8.38 "( " ^ tac2str tac ^ ", " ^ tac_2str tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
8.39 @@ -177,7 +177,7 @@
8.40 fun pbt2itm (f, (d, t)) = ((0, [], false, f, Inc((d, [t]), (e_term, []))) : itm)
8.41 in map pbt2itm pbt end
8.42
8.43 -(*generate 1 ppobj in ptree*)
8.44 +(*generate 1 ppobj in ctree*)
8.45 (*TODO.WN0501: take calcstate as an argument (see embed_derive etc.)?specify?*)
8.46 fun generate1 thy (Add_Given' (_, itmlist)) _ (pos as (p, p_)) pt =
8.47 (pos: pos', [], PpcKF (Upblmet, Specify.itms2itemppc thy [][]),
9.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Dec 22 11:12:18 2016 +0100
9.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu Dec 22 11:36:20 2016 +0100
9.3 @@ -10,16 +10,16 @@
9.4 type imodel = iitem list
9.5 type icalhd = Ctree.pos' * cterm' * imodel * Ctree.pos_ * spec
9.6 val fetchErrorpatterns : Ctree.tac -> errpatID list
9.7 - val input_icalhd : Ctree.ptree -> icalhd -> Ctree.ptree * Ctree.ocalhd
9.8 + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
9.9 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
9.10 - val find_fillpatterns : Ctree.ptree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
9.11 - val is_exactly_equal : Ctree.ptree * Ctree.pos' -> string -> string * Ctree.tac
9.12 + val find_fillpatterns : Ctree.ctree * Ctree.pos' -> errpatID -> (fillpatID * term * thm * Ctree.subs option) list
9.13 + val is_exactly_equal : Ctree.ctree * Ctree.pos' -> string -> string * Ctree.tac
9.14
9.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.16 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
9.17 - val cas_input : term -> (Ctree.ptree * Ctree.ocalhd) option
9.18 + val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
9.19 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
9.20 - val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos') -> term -> string * Chead.calcstate'
9.21 + val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos') -> term -> string * Chead.calcstate'
9.22 val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
9.23 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
9.24 rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
9.25 @@ -95,7 +95,7 @@
9.26 in (pI, pits: itm list, mI, mits: itm list, pre, ctxt) end;
9.27
9.28
9.29 -(* check if the input term is a CAScmd and return a ptree with a _complete_ calchead *)
9.30 +(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
9.31 fun cas_input hdt =
9.32 let
9.33 val (h, argl) = strip_comb hdt
9.34 @@ -108,7 +108,7 @@
9.35 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
9.36 val spec = (dI, pI, mI)
9.37 val (pt,_) =
9.38 - Ctree.cappend_problem Ctree.e_ptree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
9.39 + Ctree.cappend_problem Ctree.e_ctree [] (Ctree.e_istate, Ctree.e_ctxt) ([], e_spec) ([], e_spec, hdt)
9.40 val pt = Ctree.update_spec pt [] spec
9.41 val pt = Ctree.update_pbl pt [] pits
9.42 val pt = Ctree.update_met pt [] mits
10.1 --- a/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:12:18 2016 +0100
10.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:36:20 2016 +0100
10.3 @@ -9,32 +9,32 @@
10.4 signature MATH_ENGINE =
10.5 sig
10.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
10.7 - val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree
10.8 + val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ctree
10.9 val autocalc :
10.10 - Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos')
10.11 + Ctree.pos' list -> Ctree.pos' -> (Ctree.ctree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ctree * Ctree.pos')
10.12 val locatetac :
10.13 - Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos'))
10.14 + Ctree.tac -> Ctree.ctree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos'))
10.15 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
10.16 val detailstep :
10.17 - Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos'
10.18 - val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option
10.19 + Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
10.20 + val get_pblID : Ctree.ctree * Ctree.pos' -> pblID option
10.21
10.22 - val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
10.23 - val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
10.24 - val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
10.25 - val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
10.26 - val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
10.27 - val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
10.28 - val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
10.29 - val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
10.30 + val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
10.31 + val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
10.32 + val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
10.33 + val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
10.34 + val set_method : metID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
10.35 + val set_problem : pblID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
10.36 + val set_theory : thyID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd
10.37 + val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
10.38
10.39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.40 type nxt_
10.41 type lOc_
10.42 - val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree
10.43 + val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ctree
10.44 val f2str : Generate.mout -> cterm'
10.45 - val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
10.46 - val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
10.47 + val loc_solve_ : string * Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_
10.48 + val loc_specify_ : Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_
10.49 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.50 end
10.51
11.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 11:12:18 2016 +0100
11.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Dec 22 11:36:20 2016 +0100
11.3 @@ -31,8 +31,8 @@
11.4 val no_thycontext : guh -> bool
11.5 val subs_from : Ctree.istate -> 'a -> guh -> Ctree.subs
11.6 val guh2rewtac : guh -> Ctree.subs -> Ctree.tac
11.7 - val get_tac_checked : Ctree.ptree -> Ctree.pos' -> Ctree.tac
11.8 - val context_thy : Ctree.ptree * Ctree.pos' -> Ctree.tac -> contthy
11.9 + val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Ctree.tac
11.10 + val context_thy : Ctree.ctree * Ctree.pos' -> Ctree.tac -> contthy
11.11 val distinct_Thm : rule list -> rule list
11.12 val eq_Thms : string list -> rule -> bool
11.13 val make_deriv : theory -> rls -> rule list -> ((term * term) list -> term * term -> bool) ->
12.1 --- a/src/Tools/isac/Interpret/script.sml Thu Dec 22 11:12:18 2016 +0100
12.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Dec 22 11:36:20 2016 +0100
12.3 @@ -8,21 +8,21 @@
12.4 signature LUCAS_INTERPRETER =
12.5 sig
12.6
12.7 - type step = Ctree.tac_ * Generate.mout * Ctree.ptree * Ctree.pos' * Ctree.pos' list
12.8 + type step = Ctree.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
12.9 datatype locate = NotLocatable | Steps of Ctree.istate * step list
12.10
12.11 val next_tac : (*diss: next-tactic-function*)
12.12 - theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
12.13 + theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> Ctree.istate * 'a -> Ctree.tac_ * (Ctree.istate * 'a) * (term * Ctree.safe)
12.14 val locate_gen : (*diss: locate-function*)
12.15 - theory' * rls -> Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
12.16 + theory' * rls -> Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> scr * 'a -> Ctree.istate * Proof.context -> locate
12.17
12.18 (* can these functions be local to Lucin or part of LItools ? *)
12.19 - val sel_rules : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
12.20 + val sel_rules : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
12.21 val init_form : 'a -> scr -> (term * term) list -> term option
12.22 val tac_2tac : Ctree.tac_ -> Ctree.tac
12.23 val init_scrstate : theory -> itm list -> metID -> Ctree.istate * Proof.context * scr
12.24 - val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ptree -> rls * (Ctree.istate * Proof.context) * scr
12.25 - val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ptree ->
12.26 + val from_pblobj' : theory' -> Ctree.pos' -> Ctree.ctree -> rls * (Ctree.istate * Proof.context) * scr
12.27 + val from_pblobj_or_detail' : theory' -> Ctree.pos' -> Ctree.ctree ->
12.28 rls * (Ctree.istate * Proof.context) * scr
12.29 val rule2thm'' : rule -> thm''
12.30 val rule2rls' : rule -> string
12.31 @@ -31,7 +31,7 @@
12.32 datatype asap = Aundef | AssOnly | AssGen
12.33 datatype appy = Appy of Ctree.tac_ * Ctree.scrstate | Napp of env | Skip of term * env
12.34 datatype appy_ = Napp_ | Skip_
12.35 - val appy : theory' * rls -> Ctree.ptree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
12.36 + val appy : theory' * rls -> Ctree.ctree * Ctree.pos' -> env -> lrd list -> term -> term option -> term -> appy
12.37 val formal_args : term -> term list
12.38 val get_stac : 'a -> term -> term option
12.39 val go : loc_ -> term -> term
12.40 @@ -40,11 +40,11 @@
12.41 val id_of_scr : term -> string
12.42 val is_spec_pos : Ctree.pos_ -> bool
12.43 val itms2args : 'a -> metID -> itm list -> term list
12.44 - val nstep_up : theory' * rls -> Ctree.ptree * Ctree.pos' -> scr -> env -> lrd list -> appy_ ->
12.45 + val nstep_up : theory' * rls -> Ctree.ctree * Ctree.pos' -> scr -> env -> lrd list -> appy_ ->
12.46 term option -> term -> appy
12.47 - val sel_appl_atomic_tacs : Ctree.ptree -> Ctree.pos' -> Ctree.tac list
12.48 - val stac2tac : Ctree.ptree -> theory -> term -> Ctree.tac
12.49 - val stac2tac_ : Ctree.ptree -> theory -> term -> Ctree.tac * Ctree.tac_
12.50 + val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Ctree.tac list
12.51 + val stac2tac : Ctree.ctree -> theory -> term -> Ctree.tac
12.52 + val stac2tac_ : Ctree.ctree -> theory -> term -> Ctree.tac * Ctree.tac_
12.53 val upd_env_opt : env -> term option * term -> env
12.54 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.55 end
12.56 @@ -64,9 +64,9 @@
12.57 type step =
12.58 tac_ (*transformed from associated tac *)
12.59 * Generate.mout (*result with indentation etc. *)
12.60 - * ptree (*containing node created by tac_ + resp. scrstate *)
12.61 - * pos' (*position in ptree; ptree * pos' is the proofstate *)
12.62 - * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
12.63 + * ctree (*containing node created by tac_ + resp. scrstate *)
12.64 + * pos' (*position in ctree; ctree * pos' is the proofstate *)
12.65 + * pos' list; (*of ctree-nodes probably cut (by fst tac_) *)
12.66
12.67 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
12.68 | rule2thm'' r = error ("rule2thm': not defined for " ^ rule2str r);
12.69 @@ -213,7 +213,7 @@
12.70
12.71 (* convert a script-tac 'stac' to a tactic 'tac';
12.72 if stac is an initac, then convert to a 'tac_' (as required in appy).
12.73 - arg ptree for pushing the thy specified in rootpbl into subpbls *)
12.74 + arg ctree for pushing the thy specified in rootpbl into subpbls *)
12.75 fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) =
12.76 let
12.77 val tid = (de_esc_underscore o strip_thy) thmID
12.78 @@ -295,7 +295,7 @@
12.79 has been changed (see "datatype tac_"); if yes, recalculate result
12.80 TODO.WN120106 recalculate impl.only for Substitute'
12.81 args
12.82 - pt : ptree for pushing the thy specified in rootpbl into subpbls
12.83 + pt : ctree for pushing the thy specified in rootpbl into subpbls
12.84 d : unused (planned for data for comparison)
12.85 tac_ : from user (via applicable_in); to be compared with ...
12.86 stac : found in Script
12.87 @@ -563,8 +563,8 @@
12.88 (step list) (* list of steps done until associated stac found;
12.89 initiated with the data for doing the 1st step,
12.90 thus the head holds these data further on,
12.91 - while the tail holds steps finished (incl.scrstate in ptree) *)
12.92 -| NasApp of (* stac not associated, but applicable, ptree-node generated *)
12.93 + while the tail holds steps finished (incl.scrstate in ctree) *)
12.94 +| NasApp of (* stac not associated, but applicable, ctree-node generated *)
12.95 scrstate * (step list)
12.96 | NasNap of (* stac not associated, not applicable, nothing generated;
12.97 for distinction in Or, for leaving iterations, leaving Seq,
12.98 @@ -789,7 +789,7 @@
12.99 datatype locate =
12.100 Steps of istate (* producing hd of step list (which was latest)
12.101 for next_tac, for reporting Safe|Unsafe to DG *)
12.102 - * step (* (scrstate producing this step is in ptree !) *)
12.103 + * step (* (scrstate producing this step is in ctree !) *)
12.104 list (* locate_gen may produce intermediate steps *)
12.105 | NotLocatable; (* no (m Ass m') or (m AssWeak m') found *)
12.106
12.107 @@ -798,7 +798,7 @@
12.108 or the end of the script
12.109 args
12.110 m : input by the user, already checked by applicable_in,
12.111 - (to be searched within Or; and _not_ an m doing the step on ptree !)
12.112 + (to be searched within Or; and _not_ an m doing the step on ctree !)
12.113 p,pt: (incl ets) at the time of input
12.114 scr : the script
12.115 d : canonical simplifier for locating Take, Substitute, Subproblems etc.
12.116 @@ -819,7 +819,7 @@
12.117 (case lo rss f (Thm thm) of
12.118 [] => NotLocatable
12.119 | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
12.120 - | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
12.121 + | locate_gen (thy',srls) (m:tac_) ((pt,p):ctree * pos')
12.122 (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
12.123 let val thy = assoc_thy thy';
12.124 in case if l = [] orelse (
12.125 @@ -1042,7 +1042,7 @@
12.126 | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
12.127 (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
12.128 (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
12.129 - | next_tac thy (ptp as (pt, (p, _)):ptree * pos') (sc as Prog (_ $ body))
12.130 + | next_tac thy (ptp as (pt, (p, _)):ctree * pos') (sc as Prog (_ $ body))
12.131 (ScrState (E,l,a,v,s,_), ctxt) =
12.132 (case if l = [] then appy thy ptp E [R] body NONE v
12.133 else nstep_up thy ptp sc E l Skip_ a v of
13.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Dec 22 11:12:18 2016 +0100
13.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Dec 22 11:36:20 2016 +0100
13.3 @@ -90,7 +90,7 @@
13.4
13.5
13.6
13.7 -type squ = ptree; (* TODO: safe etc. *)
13.8 +type squ = ctree; (* TODO: safe etc. *)
13.9
13.10 (*13.9.02--------------
13.11 type ctr = (loc * pos) list;
13.12 @@ -144,7 +144,7 @@
13.13 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
13.14 val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
13.15 *)
13.16 -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
13.17 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ctree, (pos as (p,_))) =
13.18 let val {srls, ...} = Specify.get_met mI;
13.19 val PblObj {meth=itms, ...} = get_obj I pt p;
13.20 val thy' = get_obj g_domID pt p;
13.21 @@ -234,7 +234,7 @@
13.22 val pr as (p',_) = (lev_up p, Res)
13.23 val pp = par_pblobj pt p
13.24 val r = (fst o (get_obj g_result pt)) p'
13.25 - (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
13.26 + (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
13.27 val thy' = get_obj g_domID pt pp
13.28 val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt
13.29 val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is
13.30 @@ -274,7 +274,7 @@
13.31
13.32 (*FIXME.WN050821 compare fun solve ... fun nxt_solv*)
13.33 (* nxt_solv (Apply_Method' vvv FIXME: get args in applicable_in *)
13.34 -fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
13.35 +fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) =
13.36 let
13.37 val {srls,ppc,...} = Specify.get_met mI;
13.38 val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
13.39 @@ -354,7 +354,7 @@
13.40 val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
13.41 in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
13.42
13.43 -(* find the next tac from the script, nxt_solv will update the ptree *)
13.44 +(* find the next tac from the script, nxt_solv will update the ctree *)
13.45 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
13.46 if e_metID = get_obj g_metID pt (par_pblobj pt p)
13.47 then ([], [], (pt, (p, p_))) : Chead.calcstate'
13.48 @@ -390,7 +390,7 @@
13.49 | autoord CompleteSubpbl = 5
13.50 | autoord CompleteCalc = 6;
13.51
13.52 -fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
13.53 +fun complete_solve auto c (ptp as (_, p as (_,p_)): ctree * pos') =
13.54 if p = ([], Res)
13.55 then ("end-of-calculation", [], ptp)
13.56 else
13.57 @@ -420,7 +420,7 @@
13.58 else complete_solve auto (c @ c') ptp'
13.59 | (_, c', ptp') => complete_solve auto (c @ c') ptp'
13.60
13.61 -and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') =
13.62 +and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') =
13.63 let
13.64 val (_,_,mI) = get_obj g_spec pt p
13.65 val ctxt = get_ctxt pt pos
14.1 --- a/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Thu Dec 22 11:12:18 2016 +0100
14.2 +++ b/src/Tools/isac/Knowledge/DiffApp-scrpbl.sml Thu Dec 22 11:36:20 2016 +0100
14.3 @@ -420,7 +420,7 @@
14.4 val p = e_pos'; val c = [];
14.5
14.6 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
14.7 -val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ptree, []);
14.8 +val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []);
14.9 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
14.10 (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)
14.11
15.1 --- a/src/Tools/isac/Knowledge/Equation.thy Thu Dec 22 11:12:18 2016 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Thu Dec 22 11:36:20 2016 +0100
15.3 @@ -65,7 +65,7 @@
15.4
15.5 ML{*
15.6 (*.function for handling the cas-input "solve (x+1=2, x)":
15.7 - make a model which is already in ptree-internal format.*)
15.8 + make a model which is already in ctree-internal format.*)
15.9 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)");
15.10 val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy))
15.11 "solveTest (x+1=2, x)");
16.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Thu Dec 22 11:12:18 2016 +0100
16.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Thu Dec 22 11:36:20 2016 +0100
16.3 @@ -56,7 +56,7 @@
16.4 (** CAS-command **)
16.5
16.6 (*.function for handling the cas-input "Simplify (2*a + 3*a)":
16.7 - make a model which is already in ptree-internal format.*)
16.8 + make a model which is already in ctree-internal format.*)
16.9 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
16.10 val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info.get_theory "Simplify")))
16.11 "Simplify (2*a + 3*a)");
17.1 --- a/test/Tools/isac/Frontend/use-cases.sml Thu Dec 22 11:12:18 2016 +0100
17.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Dec 22 11:36:20 2016 +0100
17.3 @@ -316,7 +316,7 @@
17.4 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
17.5
17.6 val ((pt,_),_) = get_calc 1;
17.7 - val str = pr_ptree pr_short pt;
17.8 + val str = pr_ctree pr_short pt;
17.9 writeln str;
17.10 val ip = get_pos 1 1;
17.11 val (Form f, tac, asms) = pt_extract (pt, ip);
17.12 @@ -557,7 +557,7 @@
17.13 autoCalculate 1 CompleteToSubpbl;
17.14 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
17.15 val ((pt,_),_) = get_calc 1;
17.16 - val str = pr_ptree pr_short pt;
17.17 + val str = pr_ctree pr_short pt;
17.18 writeln str;
17.19 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
17.20 then () else
17.21 @@ -566,7 +566,7 @@
17.22 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
17.23 autoCalculate 1 CompleteToSubpbl;
17.24 val ((pt,_),_) = get_calc 1;
17.25 - val str = pr_ptree pr_short pt;
17.26 + val str = pr_ctree pr_short pt;
17.27 writeln str;
17.28 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
17.29 val ((pt,_),_) = get_calc 1;
18.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:12:18 2016 +0100
18.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Dec 22 11:36:20 2016 +0100
18.3 @@ -737,7 +737,7 @@
18.4 Free ("1", "Real.real")) $
18.5 Free ("x", "Real.real"))),
18.6 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
18.7 - []) : ptree*)
18.8 + []) : ctree*)
18.9 "----- WN101007 worked until here (checked same as isac2002) ---";
18.10 case nxt of ("Model_Problem", Model_Problem) => ()
18.11 | _ => error "clchead.sml: check specify phase step 1";
18.12 @@ -810,13 +810,13 @@
18.13 Free ("1", "Real.real")) $
18.14 Free ("x", "Real.real"))),
18.15 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
18.16 - []) : ptree*)
18.17 -"----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
18.18 + []) : ctree*)
18.19 +"----- WN101007 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
18.20 case nxt of ("Add_Given", Add_Given "functionTerm (x + 1)") => ()
18.21 | _ => error "clchead.sml: check specify phase step 2";
18.22 "--- step 3 --";
18.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.24 -"----- WN101008 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
18.25 +"----- WN101008 ctree checked same as isac2002, diff. in nxt --- REPAIRED";
18.26 case nxt of ("Add_Given", Add_Given "integrateBy x") => ()
18.27 | _ => error "clchead.sml: check specify phase step 2";
18.28
19.1 --- a/test/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:12:18 2016 +0100
19.2 +++ b/test/Tools/isac/Interpret/ctree.sml Thu Dec 22 11:36:20 2016 +0100
19.3 @@ -13,23 +13,23 @@
19.4 "-------------- fun get_ctxt -------------------------------------";
19.5 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
19.6 "-------------- check positions in miniscript --------------------";
19.7 -"-------------- get_allpos' (from ptree above)--------------------";
19.8 -"-------------- cut_level (from ptree above)----------------------";
19.9 -"-------------- cut_tree (from ptree above)-----------------------";
19.10 -"=====new ptree 1a miniscript with mini-subpbl ===================";
19.11 +"-------------- get_allpos' (from ctree above)--------------------";
19.12 +"-------------- cut_level (from ctree above)----------------------";
19.13 +"-------------- cut_tree (from ctree above)-----------------------";
19.14 +"=====new ctree 1a miniscript with mini-subpbl ===================";
19.15 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
19.16 -"=====new ptree 2 miniscript with mini-subpbl ====================";
19.17 -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
19.18 -"-------------- cappend (from ptree above)------------------------";
19.19 +"=====new ctree 2 miniscript with mini-subpbl ====================";
19.20 +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
19.21 +"-------------- cappend (from ctree above)------------------------";
19.22 "-------------- cappend minisubpbl -------------------------------";
19.23 -"=====new ptree 3 ================================================";
19.24 +"=====new ctree 3 ================================================";
19.25 "-------------- move_dn ------------------------------------------";
19.26 "-------------- move_dn: Frm -> Res ------------------------------";
19.27 "-------------- move_up ------------------------------------------";
19.28 "------ move into detail -----------------------------------------";
19.29 -"=====new ptree 3a ===============================================";
19.30 +"=====new ctree 3a ===============================================";
19.31 "-------------- move_dn in Incomplete ctree ----------------------";
19.32 -"=====new ptree 4: crooked by cut_level_'_ =======================";
19.33 +"=====new ctree 4: crooked by cut_level_'_ =======================";
19.34 (*############## development stopped 0501 ########################*)
19.35 (******************************************************************)
19.36 (* val SAVE_get_trace = get_trace; *)
19.37 @@ -39,13 +39,13 @@
19.38 (* val get_trace = SAVE_get_trace; *)
19.39 (******************************************************************)
19.40 (*############## development stopped 0501 ########################*)
19.41 -"=====new ptree 4 ratequation ====================================";
19.42 +"=====new ctree 4 ratequation ====================================";
19.43 "-------------- pt_extract form, tac, asm<>[] --------------------";
19.44 -"=====new ptree 5 minisubpbl =====================================";
19.45 +"=====new ctree 5 minisubpbl =====================================";
19.46 "-------------- pt_extract form, tac, asm ------------------------";
19.47 -"=====new ptree 6 minisubpbl intersteps ==========================";
19.48 +"=====new ctree 6 minisubpbl intersteps ==========================";
19.49 "-------------- get_allpos' new ----------------------------------";
19.50 -"-------------- cut_tree new (from ptree above)-------------------";
19.51 +"-------------- cut_tree new (from ctree above)-------------------";
19.52 "-------------- subst2subs subs2subst sube2subst subte2subst -----";
19.53 "-----------------------------------------------------------------";
19.54 "-----------------------------------------------------------------";
19.55 @@ -105,7 +105,7 @@
19.56
19.57 val cuts = get_allp [] ([], ([],Frm)) pt;
19.58 val cuts2 = get_allps [] [1] (children pt);
19.59 -"ctree.sml-------------- cut_tree new (from ptree above)----------";
19.60 +"ctree.sml-------------- cut_tree new (from ctree above)----------";
19.61 val (pt', cuts) = cut_tree pt ([1],Frm);
19.62 "ctree.sml-------------- cappend on complete ctree from above ----";
19.63 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
19.64 @@ -139,9 +139,9 @@
19.65
19.66 show_pt pt;
19.67
19.68 -"-------------- get_allpos' (from ptree above)--------------------";
19.69 -"-------------- get_allpos' (from ptree above)--------------------";
19.70 -"-------------- get_allpos' (from ptree above)--------------------";
19.71 +"-------------- get_allpos' (from ctree above)--------------------";
19.72 +"-------------- get_allpos' (from ctree above)--------------------";
19.73 +"-------------- get_allpos' (from ctree above)--------------------";
19.74 if get_allpos' ([], 1) pt =
19.75 [([], Frm),
19.76 ([1], Frm),
19.77 @@ -206,9 +206,9 @@
19.78
19.79
19.80
19.81 -"-------------- cut_level (from ptree above)----------------------";
19.82 -"-------------- cut_level (from ptree above)----------------------";
19.83 -"-------------- cut_level (from ptree above)----------------------";
19.84 +"-------------- cut_level (from ctree above)----------------------";
19.85 +"-------------- cut_level (from ctree above)----------------------";
19.86 +"-------------- cut_level (from ctree above)----------------------";
19.87 show_pt pt;
19.88 show_pt pt';
19.89 default_print_depth 99; cuts; default_print_depth 3;
19.90 @@ -252,25 +252,25 @@
19.91 ([4], Res)]
19.92 then () else error "ctree.sml: diff:behav. in cut_level 2a";
19.93
19.94 -if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
19.95 +if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
19.96 then () else error "ctree.sml: diff:behav. in cut_level 2b";
19.97
19.98 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
19.99 if cuts = [([3, 1], Res), ([3, 2], Res)]
19.100 then () else error "ctree.sml: diff:behav. in cut_level 3a";
19.101 -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"
19.102 +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"
19.103 then () else error "ctree.sml: diff:behav. in cut_level 3b";
19.104
19.105 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
19.106 if cuts = [([3, 2], Res)]
19.107 then () else error "ctree.sml: diff:behav. in cut_level 4a";
19.108 -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"
19.109 +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"
19.110 then () else error "ctree.sml: diff:behav. in cut_level 4b";
19.111
19.112
19.113 -"-------------- cut_tree (from ptree above)-----------------------";
19.114 -"-------------- cut_tree (from ptree above)-----------------------";
19.115 -"-------------- cut_tree (from ptree above)-----------------------";
19.116 +"-------------- cut_tree (from ctree above)-----------------------";
19.117 +"-------------- cut_tree (from ctree above)-----------------------";
19.118 +"-------------- cut_tree (from ctree above)-----------------------";
19.119 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
19.120
19.121 (*============ inhibit exn AK110726 ==============================================
19.122 @@ -340,9 +340,9 @@
19.123 ([], Res)]
19.124 then () else error "ctree.sml: diff:behav. in cut_tree 4";
19.125
19.126 -"=====new ptree 1a miniscript with mini-subpbl ===================";
19.127 -"=====new ptree 1a miniscript with mini-subpbl ===================";
19.128 -"=====new ptree 1a miniscript with mini-subpbl ===================";
19.129 +"=====new ctree 1a miniscript with mini-subpbl ===================";
19.130 +"=====new ctree 1a miniscript with mini-subpbl ===================";
19.131 +"=====new ctree 1a miniscript with mini-subpbl ===================";
19.132 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
19.133 val (dI',pI',mI') =
19.134 ("Test",["sqroot-test","univariate","equation","test"],
19.135 @@ -383,9 +383,9 @@
19.136
19.137
19.138
19.139 -"=====new ptree 2 miniscript with mini-subpbl ====================";
19.140 -"=====new ptree 2 miniscript with mini-subpbl ====================";
19.141 -"=====new ptree 2 miniscript with mini-subpbl ====================";
19.142 +"=====new ctree 2 miniscript with mini-subpbl ====================";
19.143 +"=====new ctree 2 miniscript with mini-subpbl ====================";
19.144 +"=====new ctree 2 miniscript with mini-subpbl ====================";
19.145 reset_states ();
19.146 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.147 ("Test", ["sqroot-test","univariate","equation","test"],
19.148 @@ -401,9 +401,9 @@
19.149 if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
19.150 else error "mini-subpbl interSteps broken";
19.151
19.152 -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
19.153 -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
19.154 -"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
19.155 +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
19.156 +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
19.157 +"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
19.158 (*WN050225 intermed. outcommented
19.159 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
19.160 if cuts = [([3, 2, 1], Res),
19.161 @@ -421,9 +421,9 @@
19.162 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
19.163
19.164
19.165 -"-------------- cappend (from ptree above)------------------------";
19.166 -"-------------- cappend (from ptree above)------------------------";
19.167 -"-------------- cappend (from ptree above)------------------------";
19.168 +"-------------- cappend (from ctree above)------------------------";
19.169 +"-------------- cappend (from ctree above)------------------------";
19.170 +"-------------- cappend (from ctree above)------------------------";
19.171 val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
19.172 if cuts = [([3, 2, 1], Res),
19.173 ([3, 2, 2], Res),
19.174 @@ -452,7 +452,7 @@
19.175 "-------------- cappend minisubpbl -------------------------------";
19.176 "-------------- cappend minisubpbl -------------------------------";
19.177 "-------------- cappend minisubpbl -------------------------------";
19.178 -"=====new ptree 1 miniscript with mini-subpbl ====================";
19.179 +"=====new ctree 1 miniscript with mini-subpbl ====================";
19.180 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
19.181 val (dI',pI',mI') =
19.182 ("Test",["sqroot-test","univariate","equation","test"],
19.183 @@ -550,9 +550,9 @@
19.184
19.185 WN050225 intermed. outcommented---*)
19.186
19.187 -"=====new ptree 3 ================================================";
19.188 -"=====new ptree 3 ================================================";
19.189 -"=====new ptree 3 ================================================";
19.190 +"=====new ctree 3 ================================================";
19.191 +"=====new ctree 3 ================================================";
19.192 +"=====new ctree 3 ================================================";
19.193
19.194 reset_states ();
19.195 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.196 @@ -665,9 +665,9 @@
19.197 if p = ([2, 6], Res) then()
19.198 else error "ctree.sml: diff.behav. in move into detail";
19.199
19.200 -"=====new ptree 3a ===============================================";
19.201 -"=====new ptree 3a ===============================================";
19.202 -"=====new ptree 3a ===============================================";
19.203 +"=====new ctree 3a ===============================================";
19.204 +"=====new ctree 3a ===============================================";
19.205 +"=====new ctree 3a ===============================================";
19.206 reset_states ();
19.207 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.208 ("Test", ["sqroot-test","univariate","equation","test"],
19.209 @@ -698,9 +698,9 @@
19.210
19.211
19.212
19.213 -"=====new ptree 4: crooked by cut_level_'_ =======================";
19.214 -"=====new ptree 4: crooked by cut_level_'_ =======================";
19.215 -"=====new ptree 4: crooked by cut_level_'_ =======================";
19.216 +"=====new ctree 4: crooked by cut_level_'_ =======================";
19.217 +"=====new ctree 4: crooked by cut_level_'_ =======================";
19.218 +"=====new ctree 4: crooked by cut_level_'_ =======================";
19.219 reset_states ();
19.220 CalcTree
19.221 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
19.222 @@ -733,11 +733,11 @@
19.223 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
19.224 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
19.225 val ((pt,_),_) = get_calc 1;
19.226 -writeln(pr_ptree pr_short pt);
19.227 +writeln(pr_ctree pr_short pt);
19.228 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
19.229 ###########################################################################*)
19.230 val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
19.231 -writeln(pr_ptree pr_short pt);
19.232 +writeln(pr_ctree pr_short pt);
19.233
19.234
19.235
19.236 @@ -785,7 +785,7 @@
19.237 | SOME t => term2str (subst_atomic (mk_env probl) t)
19.238 end;
19.239 *)
19.240 -(*.get an 'interval' from ptree down to a certain level
19.241 +(*.get an 'interval' from ctree down to a certain level
19.242 by 'take_fromto children' of the nodes with specific 'from' and 'to';
19.243 'i > 0' suppresses output during recursive descent towards 'from'
19.244 b: the 'from' incremented to the actual pos
19.245 @@ -820,7 +820,7 @@
19.246 (getnd i ( b,[0]) [99999] nd) @
19.247 (getnds ~99999 false (lev_on b,[0]) q nds);
19.248 in
19.249 -(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
19.250 +(*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
19.251 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
19.252 (1) the 'f' are given
19.253 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
19.254 @@ -834,7 +834,7 @@
19.255 (take_fromto (hdp p) (hdq q) (children pt));
19.256 end;
19.257
19.258 -writeln(pr_ptree pr_short pt);
19.259 +writeln(pr_ctree pr_short pt);
19.260
19.261 case get_trace pt [1,3] [4,1,1] of
19.262 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
19.263 @@ -892,9 +892,9 @@
19.264 (******************************************************************)
19.265
19.266
19.267 -"=====new ptree 4 ratequation ====================================";
19.268 -"=====new ptree 4 ratequation ====================================";
19.269 -"=====new ptree 4 ratequation ====================================";
19.270 +"=====new ctree 4 ratequation ====================================";
19.271 +"=====new ctree 4 ratequation ====================================";
19.272 +"=====new ctree 4 ratequation ====================================";
19.273 reset_states ();
19.274 CalcTree
19.275 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
19.276 @@ -907,12 +907,12 @@
19.277 val (Form f, tac, asms) = pt_extract (pt, p);
19.278 (*============ inhibit exn WN120316 ==============================================
19.279 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
19.280 - else error "after ===new ptree 4 ratequation ===";
19.281 + else error "after ===new ctree 4 ratequation ===";
19.282 (*WN120317.TODO dropped rateq*)
19.283 ============ inhibit exn WN120316 ==============================================*)
19.284 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
19.285 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
19.286 -then () else error "after ===new ptree 4 ratequation ===";
19.287 +then () else error "after ===new ctree 4 ratequation ===";
19.288
19.289
19.290 "-------------- pt_extract form, tac, asm<>[] --------------------";
19.291 @@ -941,9 +941,9 @@
19.292
19.293
19.294
19.295 -"=====new ptree 5 minisubpbl =====================================";
19.296 -"=====new ptree 5 minisubpbl =====================================";
19.297 -"=====new ptree 5 minisubpbl =====================================";
19.298 +"=====new ctree 5 minisubpbl =====================================";
19.299 +"=====new ctree 5 minisubpbl =====================================";
19.300 +"=====new ctree 5 minisubpbl =====================================";
19.301 reset_states ();
19.302 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.303 ("Test", ["sqroot-test","univariate","equation","test"],
19.304 @@ -1020,9 +1020,9 @@
19.305 | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
19.306 ========== inhibit exn AK110719 ==============================================*)
19.307
19.308 -"=====new ptree 6 minisubpbl intersteps ==========================";
19.309 -"=====new ptree 6 minisubpbl intersteps ==========================";
19.310 -"=====new ptree 6 minisubpbl intersteps ==========================";
19.311 +"=====new ctree 6 minisubpbl intersteps ==========================";
19.312 +"=====new ctree 6 minisubpbl intersteps ==========================";
19.313 +"=====new ctree 6 minisubpbl intersteps ==========================";
19.314 reset_states ();
19.315 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.316 ("Test", ["sqroot-test","univariate","equation","test"],
19.317 @@ -1117,9 +1117,9 @@
19.318
19.319
19.320 (**#################################################################**)
19.321 -"-------------- cut_tree new (from ptree above)-------------------";
19.322 -"-------------- cut_tree new (from ptree above)-------------------";
19.323 -"-------------- cut_tree new (from ptree above)-------------------";
19.324 +"-------------- cut_tree new (from ctree above)-------------------";
19.325 +"-------------- cut_tree new (from ctree above)-------------------";
19.326 +"-------------- cut_tree new (from ctree above)-------------------";
19.327 show_pt pt;
19.328 val b = get_obj g_branch pt [];
19.329 if b = TransitiveB then () else
20.1 --- a/test/Tools/isac/Interpret/inform.sml Thu Dec 22 11:12:18 2016 +0100
20.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Dec 22 11:36:20 2016 +0100
20.3 @@ -63,7 +63,7 @@
20.4
20.5 appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
20.6 val ((pt,_),_) = get_calc 1;
20.7 - val str = pr_ptree pr_short pt;
20.8 + val str = pr_ctree pr_short pt;
20.9 if str =
20.10 (". ----- pblobj -----\n" ^
20.11 "1. x + 1 = 2\n" ^
20.12 @@ -183,7 +183,7 @@
20.13
20.14 appendFormula 1 "x = 2" (*|> Future.join*);
20.15 val ((pt,p),_) = get_calc 1;
20.16 - val str = pr_ptree pr_short pt;
20.17 + val str = pr_ctree pr_short pt;
20.18 writeln str;
20.19 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
20.20 then ()
20.21 @@ -213,7 +213,7 @@
20.22
20.23 appendFormula 1 "x = 1" (*|> Future.join*);
20.24 val ((pt,p),_) = get_calc 1;
20.25 - val str = pr_ptree pr_short pt;
20.26 + val str = pr_ctree pr_short pt;
20.27 writeln str;
20.28 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)
20.29 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
20.30 @@ -242,7 +242,7 @@
20.31 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
20.32 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
20.33 val ((pt,p),_) = get_calc 1;
20.34 - val str = pr_ptree pr_short pt;
20.35 + val str = pr_ctree pr_short pt;
20.36 writeln str;
20.37 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 ()
20.38 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
20.39 @@ -268,7 +268,7 @@
20.40
20.41 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
20.42 val ((pt,_),_) = get_calc 1;
20.43 - val str = pr_ptree pr_short pt;
20.44 + val str = pr_ctree pr_short pt;
20.45
20.46 (* before AK110725 this was
20.47 ". ----- pblobj -----\n
20.48 @@ -313,7 +313,7 @@
20.49
20.50 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
20.51 val ((pt,_),_) = get_calc 1;
20.52 - val str = pr_ptree pr_short pt;
20.53 + val str = pr_ctree pr_short pt;
20.54 writeln str;
20.55 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 ()
20.56 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
20.57 @@ -336,7 +336,7 @@
20.58
20.59 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
20.60 val ((pt,_),_) = get_calc 1;
20.61 - val str = pr_ptree pr_short pt;
20.62 + val str = pr_ctree pr_short pt;
20.63 writeln str;
20.64 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 ()
20.65 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
20.66 @@ -361,7 +361,7 @@
20.67
20.68 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
20.69 val ((pt,p),_) = get_calc 1;
20.70 - val str = pr_ptree pr_short pt;
20.71 + val str = pr_ctree pr_short pt;
20.72 writeln str;
20.73 if p = ([1], Res) then ()
20.74 else error "inform.sml: diff.behav. cut calculation 2";
20.75 @@ -457,7 +457,7 @@
20.76
20.77 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
20.78 val ((pt,_),_) = get_calc 1;
20.79 - val str = pr_ptree pr_short pt;
20.80 + val str = pr_ctree pr_short pt;
20.81 writeln str;
20.82 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
20.83 else error "inform.sml: diff.behav.appendFormula: syntax error";
21.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:12:18 2016 +0100
21.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Dec 22 11:36:20 2016 +0100
21.3 @@ -63,7 +63,7 @@
21.4 FROM val oris = prep_ori...
21.5 TO val (oris, _) = prep_ori...
21.6 *)
21.7 -"----- insert ctxt in ptree";
21.8 +"----- insert ctxt in ctree";
21.9 (* datatype ppobj
21.10 FROM loc : istate option * istate option,
21.11 TO loc : (istate * ctxt) option * (istate * ctxt) option,
21.12 @@ -497,7 +497,7 @@
21.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
21.16 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) =
21.17 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) =
21.18 (nxt, p, [], pt);
21.19 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
21.20 val (pt, p) = ptp;
21.21 @@ -546,7 +546,7 @@
21.22 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
21.23 cas = NONE; (*true*)
21.24 val hdl = pblterm dI pI;
21.25 - val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
21.26 + val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
21.27 (pors, (dI, pI, mI), hdl)
21.28 val pt = update_ctxt pt [] pctxt;
21.29
21.30 @@ -604,7 +604,7 @@
21.31 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
21.32 (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
21.33 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
21.34 -"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) =
21.35 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
21.36 (CompleteSubpbl, [], (pt',pos'));
21.37 p = ([], Res) = false;
21.38 member op = [Pbl,Met] p_ = false;
21.39 @@ -617,7 +617,7 @@
21.40 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
21.41 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
21.42 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
21.43 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
21.44 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
21.45 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
21.46 l = [] = false;
21.47 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
21.48 @@ -651,7 +651,7 @@
21.49 existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
21.50 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
21.51 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
21.52 -(append_atomic p ist_res f r f' s) : ptree -> ptree;
21.53 +(append_atomic p ist_res f r f' s) : ctree -> ctree;
21.54 ;
21.55 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
21.56 getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR> <<<<<=========================*)
22.1 --- a/test/Tools/isac/Interpret/me.sml Thu Dec 22 11:12:18 2016 +0100
22.2 +++ b/test/Tools/isac/Interpret/me.sml Thu Dec 22 11:36:20 2016 +0100
22.3 @@ -10,9 +10,9 @@
22.4 "-----------------------------------------------------------------";
22.5 "table of contents -----------------------------------------------";
22.6 "-----------------------------------------------------------------";
22.7 -"=====new ptree 1: crippled by cut_level_'_ ======================";
22.8 +"=====new ctree 1: crippled by cut_level_'_ ======================";
22.9 "-------------- get_interval from ctree with move_dn:modspec.sml -";
22.10 -"=====new ptree 2 without changes ================================";
22.11 +"=====new ctree 2 without changes ================================";
22.12 "-------------- getFormulaeFromTo --------------------------------";
22.13 "autoCalculate";
22.14 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
22.15 @@ -25,9 +25,9 @@
22.16
22.17
22.18
22.19 -"=====new ptree 1: crippled by cut_level_'_ ======================";
22.20 -"=====new ptree 1: crippled by cut_level_'_ ======================";
22.21 -"=====new ptree 1: crippled by cut_level_'_ ======================";
22.22 +"=====new ctree 1: crippled by cut_level_'_ ======================";
22.23 +"=====new ctree 1: crippled by cut_level_'_ ======================";
22.24 +"=====new ctree 1: crippled by cut_level_'_ ======================";
22.25 reset_states ();
22.26 CalcTree
22.27 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
22.28 @@ -60,12 +60,12 @@
22.29 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
22.30 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
22.31 val ((pt,_),_) = get_calc 1;
22.32 -writeln(pr_ptree pr_short pt);
22.33 +writeln(pr_ctree pr_short pt);
22.34 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
22.35 ###########################################################################*)
22.36 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
22.37 (*##########################################################################*)
22.38 -writeln(pr_ptree pr_short pt);
22.39 +writeln(pr_ctree pr_short pt);
22.40 (*##########################################################################
22.41 attention: the ctree in states is still the old (perfect) !!!
22.42 ############################################################################*)
22.43 @@ -75,7 +75,7 @@
22.44 "-------------- get_interval from ctree with move_dn:modspec.sml -";
22.45 "-------------- get_interval from ctree with move_dn:modspec.sml -";
22.46 "-------------- get_interval from ctree with move_dn:modspec.sml -";
22.47 -writeln(pr_ptree pr_short pt);
22.48 +writeln(pr_ctree pr_short pt);
22.49 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt));
22.50
22.51 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of
22.52 @@ -219,9 +219,9 @@
22.53
22.54
22.55
22.56 -"=====new ptree 2 without changes ================================";
22.57 -"=====new ptree 2 without changes ================================";
22.58 -"=====new ptree 2 without changes ================================";
22.59 +"=====new ctree 2 without changes ================================";
22.60 +"=====new ctree 2 without changes ================================";
22.61 +"=====new ctree 2 without changes ================================";
22.62 reset_states ();
22.63 CalcTree
22.64 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
22.65 @@ -233,8 +233,8 @@
22.66 val p = get_pos 1 1;
22.67 val (Form f, tac, asms) = pt_extract (pt, p);
22.68 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
22.69 - else error "after ===new ptree 2 without changes ===";
22.70 -writeln(pr_ptree pr_short pt);
22.71 + else error "after ===new ctree 2 without changes ===";
22.72 +writeln(pr_ctree pr_short pt);
22.73
22.74
22.75 "-------------- getFormulaeFromTo --------------------------------";
23.1 --- a/test/Tools/isac/Interpret/script.sml Thu Dec 22 11:12:18 2016 +0100
23.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Dec 22 11:36:20 2016 +0100
23.3 @@ -231,9 +231,9 @@
23.4 member op = specsteps mI; (*false*)
23.5 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
23.6 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
23.7 -(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
23.8 +(*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
23.9 (mI,m); (*string * tac*)
23.10 -ptp (*ptree * pos'*);
23.11 +ptp (*ctree * pos'*);
23.12 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
23.13 (*val (msg, cs') = solve m (pt, pos);
23.14 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
23.15 @@ -315,7 +315,7 @@
23.16 (*WAS stac2tac_ TODO: no match for SubProblem*)
23.17 val thy' = get_obj g_domID pt (par_pblobj pt p);
23.18 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
23.19 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
23.20 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
23.21 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
23.22 l; (*= [R, L, R, L, R, R]*)
23.23 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
23.24 @@ -348,7 +348,7 @@
23.25 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
23.26 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
23.27
23.28 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
23.29 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
23.30 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
23.31 val (mI,m) = mk_tac'_ tac;
23.32 val Appl m = applicable_in p pt m;
23.33 @@ -366,7 +366,7 @@
23.34 ini = NONE; (*true*)
23.35 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
23.36 val d = e_rls (*FIXME: get simplifier from domID*);
23.37 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
23.38 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'),
23.39 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
23.40 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
23.41 val thy = assoc_thy thy';
24.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Dec 22 11:12:18 2016 +0100
24.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Dec 22 11:36:20 2016 +0100
24.3 @@ -12,7 +12,7 @@
24.4 " test specify, fmz <> [] ";
24.5 " test specify, fmz = [] ";
24.6 " problemtypes + formalizations ";
24.7 -"-------------------- ptree of {(a,b). is-max ... ----------------";
24.8 +"-------------------- ctree of {(a,b). is-max ... ----------------";
24.9 "--------- me .. scripts for maximum-example ---------------------";
24.10 "--------- autoCalc .. scripts for maximum-example ---------------";
24.11
24.12 @@ -120,9 +120,9 @@
24.13 === inhibit exn 110722=============================================================*)
24.14
24.15
24.16 -"-------------------- ptree of {(a,b). is-max ... --------------------------";
24.17 -"-------------------- ptree of {(a,b). is-max ... --------------------------";
24.18 -"-------------------- ptree of {(a,b). is-max ... --------------------------";
24.19 +"-------------------- ctree of {(a,b). is-max ... --------------------------";
24.20 +"-------------------- ctree of {(a,b). is-max ... --------------------------";
24.21 +"-------------------- ctree of {(a,b). is-max ... --------------------------";
24.22
24.23 (* Teil von max-on-surface.sml,
24.24 der nach Init_Proof -> prep_ori wieder l"auft
24.25 @@ -231,7 +231,7 @@
24.26 val (pt,_) = cappend_parent(*pbl*) pt pos loc "f_y = d/dy x^3 ..."
24.27 Empty_Tac TransitiveB;
24.28 "--- 4 ---";
24.29 -writeln (pr_ptree pr_short pt);
24.30 +writeln (pr_ctree pr_short pt);
24.31
24.32 (*
24.33 . ----- pblobj -----
25.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 22 11:12:18 2016 +0100
25.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Thu Dec 22 11:36:20 2016 +0100
25.3 @@ -36,7 +36,7 @@
25.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
25.5 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))";
25.6 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)))";
25.7 -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
25.8 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
25.9 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
25.10 val (pt, p) = ptp;
25.11 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
25.12 @@ -55,7 +55,7 @@
25.13 "----------- why not nxt = Model_Problem here ? ---------";
25.14 "----------- why not nxt = Model_Problem here ? ---------";
25.15 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
25.16 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
25.17 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
25.18 val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
25.19 val (pt, p) = ptp;
25.20 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
26.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Thu Dec 22 11:12:18 2016 +0100
26.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Thu Dec 22 11:36:20 2016 +0100
26.3 @@ -166,7 +166,7 @@
26.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
26.5 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
26.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
26.7 -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
26.8 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
26.9 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
26.10 val (mI,m) = mk_tac'_ tac;
26.11 val Appl m = applicable_in p pt m;
26.12 @@ -194,7 +194,7 @@
26.13 val d = e_rls;
26.14 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
26.15 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
26.16 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
26.17 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'),
26.18 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
26.19 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
26.20 val thy = assoc_thy thy';
26.21 @@ -216,8 +216,8 @@
26.22 val i = mk_Free (i, T);
26.23 val E = upd_env E (i, v);
26.24 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
26.25 -val [(tac_, mout, ptree, pos', xxx)] = ss;
26.26 -val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
26.27 +val [(tac_, mout, ctree, pos', xxx)] = ss;
26.28 +val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
26.29 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
26.30 ... Assoc ... is correct*)
26.31 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
27.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Dec 22 11:12:18 2016 +0100
27.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Dec 22 11:36:20 2016 +0100
27.3 @@ -92,7 +92,7 @@
27.4 val (p''',_,f,nxt''',_,pt''') = me nxt p [1] pt;
27.5 f2str f = "[x = 1 / 5]";
27.6 case nxt of ("Check_elementwise", Check_elementwise "Assumptions") => () | _ => ((*not checked before*));
27.7 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
27.8 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
27.9 val (pt, p) = case locatetac tac (pt,p) of
27.10 ("ok", (_, _, ptp)) => ptp | _ => error "--- solve (1/x = 5.. locatetac";
27.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
27.12 @@ -103,7 +103,7 @@
27.13 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
27.14 val thy' = get_obj g_domID pt (par_pblobj pt p);
27.15 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
27.16 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
27.17 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
27.18 (sc as Prog (h $ body)),
27.19 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
27.20 "~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
27.21 @@ -279,7 +279,7 @@
27.22 test --- 'trace_script' from outside 'fun me '---
27.23 *)
27.24 val (pt''', p''') = (pt, p);
27.25 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
27.26 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
27.27 val (pt, p) = case locatetac tac (pt,p) of
27.28 ("ok", (_, _, ptp)) => ptp | _ => error "error in test setup";
27.29 "~~~~~ step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
27.30 @@ -292,7 +292,7 @@
27.31 e_metID = get_obj g_metID pt (par_pblobj pt p); (* = false*)
27.32 val thy' = get_obj g_domID pt (par_pblobj pt p);
27.33 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
27.34 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
27.35 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
27.36 (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
27.37 l = []; (* = false*)
27.38 "~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
28.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 22 11:12:18 2016 +0100
28.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 22 11:36:20 2016 +0100
28.3 @@ -91,7 +91,7 @@
28.4 term2str t = "1 = 2 + -2 * sqrt x";
28.5 (*... which works; thus error must be in script interpretation*)
28.6
28.7 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
28.8 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
28.9 val (pt, p) = case locatetac tac (pt,p) of
28.10 ("ok", (_, _, ptp)) => ptp;
28.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
29.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Dec 22 11:12:18 2016 +0100
29.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Dec 22 11:36:20 2016 +0100
29.3 @@ -20,7 +20,7 @@
29.4 val hdl =
29.5 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
29.6 | _ => error "Minisubplb/100-init-rootpbl.sml no headline"
29.7 -val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
29.8 +val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
29.9 (pors, (dI, pI, mI), hdl)
29.10 val pt = update_ctxt pt [] pctxt
29.11 ;((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate;
30.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Thu Dec 22 11:12:18 2016 +0100
30.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Thu Dec 22 11:36:20 2016 +0100
30.3 @@ -11,7 +11,7 @@
30.4 (*for resuming after stepping into code*)
30.5 val (p''',f''',nxt''',pt''') = (p,f,nxt,pt);
30.6
30.7 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ptree)) = (nxt, p, [], pt);
30.8 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt);
30.9 val (pt, p) =
30.10 case locatetac tac (pt,p) of
30.11 ("ok", (_, _, ptp)) => ptp;
31.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 22 11:12:18 2016 +0100
31.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Dec 22 11:36:20 2016 +0100
31.3 @@ -35,7 +35,7 @@
31.4 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
31.5 val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
31.6 (*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;*)
31.7 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
31.8 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'),
31.9 (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
31.10 ((thy',srls), m, (pt,(p,p_)), (sc,d), is);
31.11 val thy = assoc_thy thy';
32.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 22 11:12:18 2016 +0100
32.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Dec 22 11:36:20 2016 +0100
32.3 @@ -64,7 +64,7 @@
32.4 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
32.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
32.6 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
32.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
32.8 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)),
32.9 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
32.10 val ctxt = get_ctxt pt pos;
32.11 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
33.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 22 11:12:18 2016 +0100
33.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Dec 22 11:36:20 2016 +0100
33.3 @@ -55,7 +55,7 @@
33.4 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
33.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
33.6 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
33.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Prog (h $ body)),
33.8 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), (sc as Prog (h $ body)),
33.9 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
33.10 val ctxt = get_ctxt pt pos
33.11 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
34.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Thu Dec 22 11:12:18 2016 +0100
34.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Thu Dec 22 11:36:20 2016 +0100
34.3 @@ -264,7 +264,7 @@
34.4 ((#ppc o get_pbt)
34.5 ["sqroot-test","univariate","equation","test"]);
34.6 val loc = e_istate;
34.7 -val (pt,pos) = (e_ptree,[]);
34.8 +val (pt,pos) = (e_ctree,[]);
34.9 val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term);
34.10 val pt = update_branch pt [] TransitiveB;
34.11 (*
34.12 @@ -367,7 +367,7 @@
34.13 val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete;
34.14 get_assumptions_ pt ([],Res);
34.15
34.16 -writeln (pr_ptree pr_short pt);
34.17 +writeln (pr_ctree pr_short pt);
34.18 (* aus src.24-11-99:
34.19 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
34.20 1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
34.21 @@ -492,7 +492,7 @@
34.22 val (p,_,f,nxt,_,pt)=
34.23 me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
34.24 --- *)
34.25 -writeln (pr_ptree pr_short pt);
34.26 +writeln (pr_ctree pr_short pt);
34.27 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
34.28 *)
34.29
34.30 @@ -632,7 +632,7 @@
34.31 then error "root-equ.sml: diff.behav. in me + tacs input"
34.32 else ();
34.33
34.34 -writeln (pr_ptree pr_short pt);
34.35 +writeln (pr_ctree pr_short pt);
34.36 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^
34.37 "\n==============================================================");
34.38
35.1 --- a/test/Tools/isac/OLDTESTS/script.sml Thu Dec 22 11:12:18 2016 +0100
35.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Thu Dec 22 11:36:20 2016 +0100
35.3 @@ -238,7 +238,7 @@
35.4 (~1,EdUndef,1,Nundef,
35.5 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"))
35.6 then () else error "behaviour in root-expl. Free_Solve changed";
35.7 -writeln (pr_ptree pr_short pt);
35.8 +writeln (pr_ctree pr_short pt);
35.9 ---------------------------------meNEW raises exception with not-locatable*)
35.10
35.11
36.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Dec 22 11:12:18 2016 +0100
36.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Dec 22 11:36:20 2016 +0100
36.3 @@ -294,7 +294,7 @@
36.4 (* val nxt = ("End_Proof'",End_Proof');*)
36.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
36.6
36.7 -writeln (pr_ptree pr_short pt);
36.8 +writeln (pr_ctree pr_short pt);
36.9 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^
36.10 "\n=============================================================");
36.11 (*get_obj g_asm pt [];
37.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Dec 22 11:12:18 2016 +0100
37.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Dec 22 11:36:20 2016 +0100
37.3 @@ -359,7 +359,7 @@
37.4 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
37.5
37.6
37.7 -writeln (pr_ptree pr_short pt);
37.8 +writeln (pr_ctree pr_short pt);
37.9
37.10
37.11
38.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Thu Dec 22 11:12:18 2016 +0100
38.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Thu Dec 22 11:36:20 2016 +0100
38.3 @@ -26,7 +26,7 @@
38.4 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
38.5 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
38.6 val ((pt,_),_) = get_calc 1;
38.7 - val str = pr_ptree pr_short pt;
38.8 + val str = pr_ctree pr_short pt;
38.9 writeln str;
38.10
38.11 fetchProposedTactic 1 (*'Subproblem ...' in tacis*);
38.12 @@ -58,7 +58,7 @@
38.13 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
38.14 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*);
38.15 val ((pt,_),_) = get_calc 1;
38.16 - val str = pr_ptree pr_short pt;
38.17 + val str = pr_ctree pr_short pt;
38.18 writeln str;
38.19
38.20 fetchProposedTactic 1 (*'Check_Postcond linear...' in tacis*);
38.21 @@ -99,14 +99,14 @@
38.22 setNextTactic 1 (Rewrite_Set "Test_simplify");
38.23 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
38.24 val ((pt,_),_) = get_calc 1;
38.25 - val str = pr_ptree pr_short pt;
38.26 + val str = pr_ctree pr_short pt;
38.27 writeln str;
38.28
38.29 setNextTactic 1 (Subproblem ("Test",["LINEAR","univariate",
38.30 "equation","test"]));
38.31 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*);
38.32 val ((pt,_),_) = get_calc 1;
38.33 - val str = pr_ptree pr_short pt;
38.34 + val str = pr_ctree pr_short pt;
38.35 writeln str;
38.36
38.37 setNextTactic 1 (Model_Problem (*["LINEAR","univariate","equation","test"]*));
38.38 @@ -138,7 +138,7 @@
38.39 setNextTactic 1 (Check_elementwise "Assumptions");
38.40 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
38.41 val ((pt,_),_) = get_calc 1;
38.42 - val str = pr_ptree pr_short pt;
38.43 + val str = pr_ctree pr_short pt;
38.44 writeln str;
38.45
38.46 setNextTactic 1 (Check_Postcond