1.1 --- a/src/Tools/isac/ProgLang/Tools.thy Thu Jul 28 11:22:54 2011 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Tools.thy Thu Jul 28 11:37:05 2011 +0200
1.3 @@ -64,9 +64,9 @@
1.4 (tracing"### or2list _ = _";list2isalist bool [t])
1.5 | or2list ors =
1.6 (tracing"### or2list _ | _";
1.7 - let fun get ls (Const ("op |",_) $ o1 $ o2) =
1.8 + let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
1.9 case o2 of
1.10 - Const ("op |",_) $ _ $ _ => get (ls @ [o1]) o2
1.11 + Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
1.12 | _ => ls @ [o1, o2]
1.13 in (((list2isalist bool) o (get [])) ors)
1.14 handle _ => error ("or2list: no ORs= "^(term2str ors)) end
2.1 --- a/test/Tools/isac/Frontend/interface.sml Thu Jul 28 11:22:54 2011 +0200
2.2 +++ b/test/Tools/isac/Frontend/interface.sml Thu Jul 28 11:37:05 2011 +0200
2.3 @@ -792,10 +792,8 @@
2.4 show_pt pt;
2.5 val p = get_pos 1 1;
2.6 val (Form f, tac, asms) = pt_extract (pt, p);
2.7 -(*========== inhibit exn 110719 ================================================
2.8 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.9 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.10 -========== inhibit exn 110719 ================================================*)
2.11
2.12 (*------------^^^-inserted-----------------------------------------------*)
2.13 (*WN050904 the fetchProposedTactic's below may not have worked like that
2.14 @@ -816,28 +814,9 @@
2.15 rootthy pt;
2.16 show_pt pt;
2.17 val p = get_pos 1 1;
2.18 -
2.19 -(*============ inhibit exn AK110719 ==============================================
2.20 -(* ERROR: execption Bind raised *)
2.21 val (Form f, tac, asms) = pt_extract (pt, p);
2.22 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
2.23 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
2.24 -============ inhibit exn AK110719 ==============================================*)
2.25 -
2.26 -(* (* AK110727 Debugging (to be continued) *)
2.27 - asms; (*term list (!)*)
2.28 - print_depth 99;
2.29 - pt_extract (pt, p); (* ptform * tac option * term list*)
2.30 - (Form f, tac, asms);
2.31 - val (myval,myval2,myval3s) = pt_extract (pt,p);
2.32 -
2.33 -"~~~~~ fun pt_extract, args:"; val ((pt, pos as (p,p_(*Frm,Pbl*)))) = ((pt, p));
2.34 - val ppobj = get_obj I pt p;
2.35 - is_pblobj ppobj; (*true*)
2.36 - pt_model ppobj p_;
2.37 - val tac = g_tac ppobj;
2.38 - (f, SOME tac, []) (* term * tac option * 'a list (!) *)
2.39 -*)
2.40
2.41 DEconstrCalcTree 1;
2.42
3.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu Jul 28 11:22:54 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Jul 28 11:37:05 2011 +0200
3.3 @@ -16,6 +16,7 @@
3.4 "----------- fun autocalc -------------------------------";
3.5 "----------- fun autoCalculate --------------------------";
3.6 "----------- fun autoCalculate..CompleteCalc ------------";
3.7 +"----------- search for Or_to_List ----------------------";
3.8 "--------------------------------------------------------";
3.9 "--------------------------------------------------------";
3.10 "--------------------------------------------------------";
3.11 @@ -424,5 +425,48 @@
3.12 then () else error "autoCalculate..CompleteCalc: ctxt at final result";
3.13
3.14
3.15 +"----------- search for Or_to_List ----------------------";
3.16 +"----------- search for Or_to_List ----------------------";
3.17 +"--------- search for Or_to_List ------------------------";
3.18 +val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
3.19 +val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
3.20 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
3.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
3.41 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) =
3.42 + (nxt, p, [], pt);
3.43 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
3.44 +val (pt, p) = ptp;
3.45 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
3.46 + (p, ((pt, e_pos'),[]));
3.47 +val pIopt = get_pblID (pt,ip);
3.48 +ip = ([],Res); (*false*)
3.49 +ip = p; (*false*)
3.50 +member op = [Pbl,Met] p_; (*false*)
3.51 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
3.52 +e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
3.53 +val thy' = get_obj g_domID pt (par_pblobj pt p);
3.54 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.55 +val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*)
3.56 +case tac_ of Or_to_List' _ => ()
3.57 +| _ => error "Or_to_List broken ?"
3.58
3.59
4.1 --- a/test/Tools/isac/ProgLang/tools.sml Thu Jul 28 11:22:54 2011 +0200
4.2 +++ b/test/Tools/isac/ProgLang/tools.sml Thu Jul 28 11:37:05 2011 +0200
4.3 @@ -8,6 +8,7 @@
4.4 "table of contents -----------------------------------------------";
4.5 "-----------------------------------------------------------------";
4.6 "----------- fun matchsub ----------------------------------------";
4.7 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.8 "-----------------------------------------------------------------";
4.9 "-----------------------------------------------------------------";
4.10 "-----------------------------------------------------------------";
4.11 @@ -22,3 +23,19 @@
4.12 if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")
4.13 then () else error "tools.sml matchsub (a + (b + c)) + d";
4.14
4.15 +
4.16 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.17 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.18 +"----------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc -";
4.19 +"see: --------- search for Or_to_List ---";
4.20 +case or2list HOLogic.true_const of Const ("Tools.UniversalList", _) => ()
4.21 + | _ => error "Tools.UniversalList changed";
4.22 +case or2list HOLogic.false_const of Const ("List.list.Nil", _) => ()
4.23 + | _ => error "Tools.UniversalList changed";
4.24 +val t = (str2term "x=3");
4.25 +if term2str (or2list t) = "[x = 3]" then ()
4.26 +else error "or2list changed";
4.27 +val t = (str2term "x=3 | x=-3 | x=0");
4.28 +if term2str (or2list t) = "[x = 3, x = -3, x = 0]" then ()
4.29 +else error "HOL.eq ? HOL.disj ? changed";
4.30 +
5.1 --- a/test/Tools/isac/Test_Isac.thy Thu Jul 28 11:22:54 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jul 28 11:37:05 2011 +0200
5.3 @@ -101,10 +101,10 @@
5.4 use "calcelems.sml"
5.5 use "ProgLang/termC.sml"
5.6 use "ProgLang/calculate.sml"
5.7 - use "ProgLang/rewrite.sml" (*?complete?*)
5.8 + use "ProgLang/rewrite.sml" (*LINKS*)
5.9 (*use "ProgLang/listC.sml" 2002*)
5.10 - use "ProgLang/scrtools.sml" (*complete*)
5.11 - use "ProgLang/tools.sml" (*complete*)
5.12 + use "ProgLang/scrtools.sml"
5.13 + use "ProgLang/tools.sml"
5.14 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
5.15 ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
5.16 use "Minisubpbl/000-comments.sml"
5.17 @@ -141,7 +141,7 @@
5.18 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
5.19 use "Frontend/messages.sml" (*new 2011*)
5.20 use "Frontend/states.sml" (*new 2011*)
5.21 - use "Frontend/interface.sml" (*complete*)
5.22 + use "Frontend/interface.sml"
5.23 use "print_exn_G.sml" (*new 2011*)
5.24 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
5.25 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
5.26 @@ -161,19 +161,19 @@
5.27 (*use "Knowledge/polyeq.sml" 2002*)
5.28 (*use "Knowledge/rlang.sml" 2002???*)
5.29 use "Knowledge/calculus.sml" (*new 2011*)
5.30 - use "Knowledge/trig.sml" (*complete*)
5.31 + use "Knowledge/trig.sml"
5.32 use "Knowledge/logexp.sml" (*part.*)
5.33 use "Knowledge/diff.sml" (*part.*)
5.34 use "Knowledge/integrate.sml" (*part. was complete 2009-2
5.35 diff.emacs--jedit*)
5.36 use "Knowledge/eqsystem.sml" (*part.*)
5.37 - use "Knowledge/test.sml" (*complete*)
5.38 + use "Knowledge/test.sml"
5.39 use "Knowledge/polyminus.sml" (*part.*)
5.40 - use "Knowledge/vect.sml" (*complete*)
5.41 + use "Knowledge/vect.sml"
5.42 use "Knowledge/diffapp.sml" (*part.*)
5.43 use "Knowledge/biegelinie.sml" (*part.*)
5.44 use "Knowledge/algein.sml" (*part.*)
5.45 - use "Knowledge/diophanteq.sml" (*complete*)
5.46 + use "Knowledge/diophanteq.sml"
5.47 use "Knowledge/isac.sml" (*part.*)
5.48 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
5.49 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
6.1 --- a/test/Tools/isac/Test_Some.thy Thu Jul 28 11:22:54 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jul 28 11:37:05 2011 +0200
6.3 @@ -7,1406 +7,21 @@
6.4
6.5 use"../../../test/Tools/isac/ProgLang/rewrite.sml"
6.6
6.7 +
6.8 +ML{*
6.9 +*}
6.10 +
6.11 ML {*
6.12
6.13 -(* tests the interface of isac's SML-kernel in accordance to
6.14 - java-tests/isac.bridge.
6.15 +*}
6.16 +ML{*
6.17
6.18 -WN050707 ... if true, the test ist marked with a \label referring
6.19 -to the same UC in isac-docu.tex as the JUnit testcase.
6.20 -use"../smltest/FE-interface/interface.sml";
6.21 -use"interface.sml";
6.22 - *)
6.23 -
6.24 -"--------------------------------------------------------";
6.25 -"table of contents --------------------------------------";
6.26 -"--------------------------------------------------------";
6.27 -"within struct ------------------------------------------";
6.28 -"--------------------------------------------------------";
6.29 -"--------- encode ^ -> ^^^ ------------------------------";
6.30 -"--------------------------------------------------------";
6.31 -"exported from struct -----------------------------------";
6.32 -"--------------------------------------------------------";
6.33 -"--------- empty rootpbl --------------------------------";
6.34 -"--------- solve_linear as rootpbl FE -------------------";
6.35 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
6.36 -"--------- miniscript with mini-subpbl ------------------";
6.37 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
6.38 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
6.39 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
6.40 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
6.41 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
6.42 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
6.43 -"--------- setContext..Thy ------------------------------";
6.44 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
6.45 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
6.46 -"--------- tryMatchProblem, tryRefineProblem ------------";
6.47 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
6.48 -"--------- maximum-example, UC: Modeling an example -----";
6.49 -"--------- solve_linear from pbl-hierarchy --------------";
6.50 -"--------- solve_linear as in an algebra system (CAS)----";
6.51 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
6.52 -"--------- getTactic, fetchApplicableTactics ------------";
6.53 -"--------- getAssumptions, getAccumulatedAsms -----------";
6.54 -"--------- arbitrary combinations of steps --------------";
6.55 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
6.56 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
6.57 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
6.58 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
6.59 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
6.60 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
6.61 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
6.62 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
6.63 -"--------------------------------------------------------";
6.64 -
6.65 -"within struct ---------------------------------------------------";
6.66 -"within struct ---------------------------------------------------";
6.67 -"within struct ---------------------------------------------------";
6.68 -(*==================================================================
6.69 -
6.70 -
6.71 -"--------- encode ^ -> ^^^ ------------------------------";
6.72 -"--------- encode ^ -> ^^^ ------------------------------";
6.73 -"--------- encode ^ -> ^^^ ------------------------------";
6.74 -if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
6.75 -else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
6.76 -
6.77 -if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
6.78 -else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
6.79 -
6.80 -==================================================================*)
6.81 -"exported from struct --------------------------------------------";
6.82 -"exported from struct --------------------------------------------";
6.83 -"exported from struct --------------------------------------------";
6.84 -
6.85 -
6.86 -(*------------ set at startup of the Kernel ----------------------*)
6.87 - states:= []; (*resets all state information in Kernel *)
6.88 -(*----------------------------------------------------------------*)
6.89 -
6.90 -"--------- empty rootpbl --------------------------------";
6.91 -"--------- empty rootpbl --------------------------------";
6.92 -"--------- empty rootpbl --------------------------------";
6.93 - CalcTree [([], ("", [], []))];
6.94 - Iterator 1;
6.95 - moveActiveRoot 1;
6.96 - refFormula 1 (get_pos 1 1);
6.97 -(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
6.98 -DEconstrCalcTree 1;
6.99 -
6.100 -"--------- solve_linear as rootpbl FE -------------------";
6.101 -"--------- solve_linear as rootpbl FE -------------------";
6.102 -"--------- solve_linear as rootpbl FE -------------------";
6.103 - CalcTree (*start of calculation, return No.1*)
6.104 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
6.105 - ("Test",
6.106 - ["linear","univariate","equation","test"],
6.107 - ["Test","solve_linear"]))];
6.108 - Iterator 1; (*create an active Iterator on CalcTree No.1*)
6.109 -
6.110 - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
6.111 - refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
6.112 -
6.113 -
6.114 - fetchProposedTactic 1 (*by using Iterator No.1*);
6.115 - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
6.116 - autoCalculate 1 (Step 1);
6.117 - refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
6.118 - autoCalculate 1 (Step 1);
6.119 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
6.120 - fetchProposedTactic 1;
6.121 - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = (0::real))");
6.122 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
6.123 -
6.124 - fetchProposedTactic 1;
6.125 - setNextTactic 1 (Add_Given "solveFor x");
6.126 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.127 -
6.128 - fetchProposedTactic 1;
6.129 - setNextTactic 1 (Add_Find "solutions L");
6.130 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.131 -
6.132 - fetchProposedTactic 1;
6.133 - setNextTactic 1 (Specify_Theory "Test");
6.134 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.135 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
6.136 -
6.137 - fetchProposedTactic 1;
6.138 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
6.139 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.140 -(*-------------------------------------------------------------------------*)
6.141 - fetchProposedTactic 1;
6.142 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
6.143 -
6.144 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
6.145 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
6.146 -
6.147 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.148 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
6.149 -
6.150 -(*-------------------------------------------------------------------------*)
6.151 - fetchProposedTactic 1;
6.152 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
6.153 -
6.154 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
6.155 - (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
6.156 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
6.157 - is_complete_mod ptp;
6.158 - is_complete_spec ptp;
6.159 -
6.160 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.161 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
6.162 - (*term2str (get_obj g_form pt [1]);*)
6.163 -(*-------------------------------------------------------------------------*)
6.164 -
6.165 - fetchProposedTactic 1;
6.166 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
6.167 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.168 -
6.169 - fetchProposedTactic 1;
6.170 - setNextTactic 1 (Rewrite_Set "Test_simplify");
6.171 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.172 -
6.173 - fetchProposedTactic 1;
6.174 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
6.175 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.176 -
6.177 - val ((pt,_),_) = get_calc 1;
6.178 - val ip = get_pos 1 1;
6.179 - val (Form f, tac, asms) = pt_extract (pt, ip);
6.180 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
6.181 - if term2str f = "[x = 1]" then () else
6.182 - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
6.183 -
6.184 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
6.185 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
6.186 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
6.187 -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
6.188 - moveActiveRoot 1;
6.189 - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
6.190 - moveActiveDown 1;
6.191 - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
6.192 - moveActiveDown 1 ;
6.193 - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
6.194 - (*getAssumption 1 ([1],Res); TODO.WN041217*)
6.195 - moveActiveDown 1 ; refFormula 1 ([2],Res);
6.196 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
6.197 - moveActiveDown 1;
6.198 - moveActiveDown 1;
6.199 - moveActiveDown 1;
6.200 - if get_pos 1 1 = ([2], Res) then () else
6.201 - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
6.202 - moveActiveDown 1; refFormula 1 ([], Res);
6.203 - if get_pos 1 1 = ([], Res) then () else
6.204 - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
6.205 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
6.206 -DEconstrCalcTree 1;
6.207 -
6.208 -"--------- miniscript with mini-subpbl ------------------";
6.209 -"--------- miniscript with mini-subpbl ------------------";
6.210 -"--------- miniscript with mini-subpbl ------------------";
6.211 -"=== this sequence of fun-calls resembles fun me ===";
6.212 - states:=[]; (*start of calculation, return No.1*)
6.213 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.214 - ("Test", ["sqroot-test","univariate","equation","test"],
6.215 - ["Test","squ-equ-test-subpbl1"]))];
6.216 - Iterator 1;
6.217 -
6.218 - moveActiveRoot 1;
6.219 - refFormula 1 (get_pos 1 1);
6.220 - fetchProposedTactic 1;
6.221 - setNextTactic 1 (Model_Problem);
6.222 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
6.223 -
6.224 - fetchProposedTactic 1;
6.225 - setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
6.226 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.227 -
6.228 - fetchProposedTactic 1;
6.229 - setNextTactic 1 (Add_Given "solveFor x");
6.230 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.231 -
6.232 - fetchProposedTactic 1;
6.233 - setNextTactic 1 (Add_Find "solutions L");
6.234 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.235 -
6.236 - fetchProposedTactic 1;
6.237 - setNextTactic 1 (Specify_Theory "Test");
6.238 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.239 -
6.240 - fetchProposedTactic 1;
6.241 - setNextTactic 1 (Specify_Problem
6.242 - ["sqroot-test","univariate","equation","test"]);
6.243 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.244 -"1-----------------------------------------------------------------";
6.245 -
6.246 - fetchProposedTactic 1;
6.247 - setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
6.248 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.249 -
6.250 - fetchProposedTactic 1;
6.251 - setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
6.252 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.253 -
6.254 - fetchProposedTactic 1;
6.255 - setNextTactic 1 (Rewrite_Set "norm_equation");
6.256 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.257 -
6.258 - fetchProposedTactic 1;
6.259 - setNextTactic 1 (Rewrite_Set "Test_simplify");
6.260 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.261 -
6.262 - fetchProposedTactic 1;(*----------------Subproblem--------------------*);
6.263 - setNextTactic 1 (Subproblem ("Test",
6.264 - ["linear","univariate","equation","test"]));
6.265 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.266 -
6.267 - fetchProposedTactic 1;
6.268 - setNextTactic 1 (Model_Problem );
6.269 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.270 -
6.271 - fetchProposedTactic 1;
6.272 - setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
6.273 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.274 -
6.275 - fetchProposedTactic 1;
6.276 - setNextTactic 1 (Add_Given "solveFor x");
6.277 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.278 -
6.279 - fetchProposedTactic 1;
6.280 - setNextTactic 1 (Add_Find "solutions x_i");
6.281 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.282 -
6.283 - fetchProposedTactic 1;
6.284 - setNextTactic 1 (Specify_Theory "Test");
6.285 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.286 -
6.287 - fetchProposedTactic 1;
6.288 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
6.289 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.290 -"2-----------------------------------------------------------------";
6.291 -
6.292 - fetchProposedTactic 1;
6.293 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
6.294 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.295 -
6.296 - fetchProposedTactic 1;
6.297 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
6.298 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.299 -
6.300 - fetchProposedTactic 1;
6.301 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
6.302 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.303 -
6.304 - fetchProposedTactic 1;
6.305 - setNextTactic 1 (Rewrite_Set "Test_simplify");
6.306 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.307 -
6.308 - fetchProposedTactic 1;
6.309 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
6.310 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.311 -
6.312 - fetchProposedTactic 1;
6.313 - setNextTactic 1 (Check_elementwise "Assumptions");
6.314 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.315 -
6.316 - val xml = fetchProposedTactic 1;
6.317 - setNextTactic 1 (Check_Postcond
6.318 - ["sqroot-test","univariate","equation","test"]);
6.319 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.320 -
6.321 - val ((pt,_),_) = get_calc 1;
6.322 - val str = pr_ptree pr_short pt;
6.323 - writeln str;
6.324 - val ip = get_pos 1 1;
6.325 - val (Form f, tac, asms) = pt_extract (pt, ip);
6.326 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
6.327 - if term2str f = "[x = 1]" then () else
6.328 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
6.329 - DEconstrCalcTree 1;
6.330 -
6.331 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
6.332 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
6.333 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
6.334 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.335 - ("Test", ["sqroot-test","univariate","equation","test"],
6.336 - ["Test","squ-equ-test-subpbl1"]))];
6.337 - Iterator 1;
6.338 - moveActiveRoot 1;
6.339 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.340 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.341 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.342 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.343 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.344 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.345 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.346 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.347 - (*here the solve-phase starts*)
6.348 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.349 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.350 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.351 - (*------------------------------------*)
6.352 -(* print_depth 13; get_calc 1;
6.353 - *)
6.354 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.355 - (*calc-head of subproblem*)
6.356 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.357 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.358 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.359 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.360 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.361 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.362 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.363 - (*solve-phase of the subproblem*)
6.364 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.365 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.366 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.367 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.368 - (*finish subproblem*)
6.369 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.370 - (*finish problem*)
6.371 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.372 -
6.373 - (*this checks the test for correctness..*)
6.374 - val ((pt,_),_) = get_calc 1;
6.375 - val p = get_pos 1 1;
6.376 - val (Form f, tac, asms) = pt_extract (pt, p);
6.377 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
6.378 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
6.379 - DEconstrCalcTree 1;
6.380 -
6.381 -
6.382 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
6.383 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
6.384 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
6.385 - CalcTree
6.386 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
6.387 - ("Test",
6.388 - ["linear","univariate","equation","test"],
6.389 - ["Test","solve_linear"]))];
6.390 - Iterator 1;
6.391 - moveActiveRoot 1;
6.392 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
6.393 -
6.394 - autoCalculate 1 CompleteCalc;
6.395 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
6.396 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
6.397 -
6.398 - val ((pt,_),_) = get_calc 1;
6.399 - val p = get_pos 1 1;
6.400 - val (Form f, tac, asms) = pt_extract (pt, p);
6.401 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
6.402 - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
6.403 -DEconstrCalcTree 1;
6.404 -
6.405 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
6.406 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
6.407 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
6.408 -(* ERROR: error in kernel ?? *)
6.409 - CalcTree
6.410 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
6.411 - ("Test",
6.412 - ["linear","univariate","equation","test"],
6.413 - ["Test","solve_linear"]))];
6.414 - Iterator 1;
6.415 - moveActiveRoot 1;
6.416 -
6.417 - autoCalculate 1 CompleteCalcHead;
6.418 - refFormula 1 (get_pos 1 1);
6.419 - val ((pt,p),_) = get_calc 1;
6.420 -
6.421 - autoCalculate 1 CompleteCalc;
6.422 - val ((pt,p),_) = get_calc 1;
6.423 - if p=([], Res) then () else
6.424 - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
6.425 -DEconstrCalcTree 1;
6.426 -
6.427 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
6.428 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
6.429 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
6.430 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.431 - ("Test", ["sqroot-test","univariate","equation","test"],
6.432 - ["Test","squ-equ-test-subpbl1"]))];
6.433 - Iterator 1;
6.434 - moveActiveRoot 1;
6.435 - autoCalculate 1 CompleteCalc;
6.436 - val ((pt,p),_) = get_calc 1; show_pt pt;
6.437 -(*
6.438 -getTactic 1 ([1],Frm);
6.439 -getTactic 1 ([1],Res);
6.440 -initContext 1 Thy_ ([1],Res);
6.441 -*)
6.442 - (*... returns calcChangedEvent with*)
6.443 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
6.444 - getFormulaeFromTo 1 unc gen 0 (*only result*) false;
6.445 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
6.446 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
6.447 -
6.448 - val ((pt,_),_) = get_calc 1;
6.449 - val p = get_pos 1 1;
6.450 - val (Form f, tac, asms) = pt_extract (pt, p);
6.451 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
6.452 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
6.453 -DEconstrCalcTree 1;
6.454 -
6.455 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
6.456 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
6.457 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
6.458 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.459 - ("Test", ["sqroot-test","univariate","equation","test"],
6.460 - ["Test","squ-equ-test-subpbl1"]))];
6.461 - Iterator 1;
6.462 - moveActiveRoot 1;
6.463 - autoCalculate 1 CompleteCalcHead;
6.464 -
6.465 -val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
6.466 - cell = NONE, ctxt = ctxt2, meth,
6.467 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
6.468 - ["Test", "squ-equ-test-subpbl1"]),
6.469 - probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
6.470 - ([], Met)), []) = get_calc 1;
6.471 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
6.472 -else error "--- mini-subpbl AUTO CompleteCalcHead ---";
6.473 -DEconstrCalcTree 1;
6.474 -
6.475 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
6.476 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
6.477 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
6.478 - CalcTree
6.479 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
6.480 - ("Test",
6.481 - ["linear","univariate","equation","test"],
6.482 - ["Test","solve_linear"]))];
6.483 - Iterator 1;
6.484 - moveActiveRoot 1;
6.485 - autoCalculate 1 CompleteModel;
6.486 - refFormula 1 (get_pos 1 1);
6.487 -
6.488 -setProblem 1 ["linear","univariate","equation","test"];
6.489 -val pos = get_pos 1 1;
6.490 -setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
6.491 - refFormula 1 (get_pos 1 1);
6.492 -
6.493 -setMethod 1 ["Test","solve_linear"];
6.494 -setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
6.495 - refFormula 1 (get_pos 1 1);
6.496 - val ((pt,_),_) = get_calc 1;
6.497 - if get_obj g_spec pt [] = ("e_domID",
6.498 - ["linear", "univariate","equation","test"],
6.499 - ["Test","solve_linear"]) then ()
6.500 - else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
6.501 -
6.502 - autoCalculate 1 CompleteCalcHead;
6.503 - refFormula 1 (get_pos 1 1);
6.504 - autoCalculate 1 CompleteCalc;
6.505 - moveActiveDown 1;
6.506 - moveActiveDown 1;
6.507 - moveActiveDown 1;
6.508 - refFormula 1 (get_pos 1 1);
6.509 - val ((pt,_),_) = get_calc 1;
6.510 - val p = get_pos 1 1;
6.511 - val (Form f, tac, asms) = pt_extract (pt, p);
6.512 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
6.513 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
6.514 -DEconstrCalcTree 1;
6.515 -
6.516 -"--------- setContext..Thy ------------------------------";
6.517 -"--------- setContext..Thy ------------------------------";
6.518 -"--------- setContext..Thy ------------------------------";
6.519 - states:=[];
6.520 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.521 - ("Test", ["sqroot-test","univariate","equation","test"],
6.522 - ["Test","squ-equ-test-subpbl1"]))];
6.523 - Iterator 1; moveActiveRoot 1;
6.524 - autoCalculate 1 CompleteCalcHead;
6.525 - autoCalculate 1 (Step 1);
6.526 - val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
6.527 - (*
6.528 - setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
6.529 - autoCalculate 1 (Step 1);
6.530 - val ((pt,p),_) = get_calc 1; show_pt pt;
6.531 - *)
6.532 -"-----^^^^^ and vvvvv do the same -----";
6.533 - setContext 1 p "thy_isac_Test-rls-Test_simplify";
6.534 - val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
6.535 -
6.536 - autoCalculate 1 (Step 1);
6.537 - setContext 1 p "thy_isac_Test-rls-Test_simplify";
6.538 - val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
6.539 - val (Form f, tac, asms) = pt_extract (pt, p);
6.540 - if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
6.541 - then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
6.542 -
6.543 - autoCalculate 1 CompleteCalc;
6.544 - val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
6.545 - val (Form f, tac, asms) = pt_extract (pt, p);
6.546 -
6.547 - if term2str f = "[x = 1]" andalso p = ([], Res) then ()
6.548 - else error "--- setContext..Thy --- autoCalculate CompleteCalc";
6.549 - DEconstrCalcTree 1;
6.550 -
6.551 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
6.552 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
6.553 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
6.554 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.555 - ("Test", ["sqroot-test","univariate","equation","test"],
6.556 - ["Test","squ-equ-test-subpbl1"]))];
6.557 - Iterator 1; moveActiveRoot 1;
6.558 - autoCalculate 1 CompleteToSubpbl;
6.559 - refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
6.560 - val ((pt,_),_) = get_calc 1;
6.561 - val str = pr_ptree pr_short pt;
6.562 - writeln str;
6.563 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
6.564 - then () else
6.565 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
6.566 -
6.567 - autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
6.568 - autoCalculate 1 CompleteToSubpbl;
6.569 - val ((pt,_),_) = get_calc 1;
6.570 - val str = pr_ptree pr_short pt;
6.571 - writeln str;
6.572 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
6.573 - val ((pt,_),_) = get_calc 1;
6.574 - val p = get_pos 1 1;
6.575 -
6.576 - val (Form f, tac, asms) = pt_extract (pt, p);
6.577 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
6.578 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
6.579 -DEconstrCalcTree 1;
6.580 -
6.581 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
6.582 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
6.583 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
6.584 - CalcTree
6.585 - [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
6.586 - ("RatEq", ["univariate","equation"], ["no_met"]))];
6.587 - Iterator 1;
6.588 - moveActiveRoot 1;
6.589 - fetchProposedTactic 1;
6.590 -
6.591 - setNextTactic 1 (Model_Problem);
6.592 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.593 -
6.594 - setNextTactic 1 (Specify_Theory "RatEq");
6.595 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.596 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
6.597 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.598 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
6.599 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.600 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
6.601 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.602 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
6.603 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.604 - setNextTactic 1 (Rewrite_Set "norm_Rational");
6.605 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.606 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
6.607 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.608 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
6.609 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
6.610 - "univariate","equation"]));
6.611 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.612 - setNextTactic 1 (Model_Problem );
6.613 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.614 - setNextTactic 1 (Specify_Theory "PolyEq");
6.615 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.616 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
6.617 - "univariate","equation"]);
6.618 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.619 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
6.620 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.621 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
6.622 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.623 - setNextTactic 1 (Rewrite ("all_left",""));
6.624 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.625 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
6.626 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.627 - (* __________ for "16 + 12 * x = 0"*)
6.628 - setNextTactic 1 (Subproblem ("PolyEq",
6.629 - ["degree_1","polynomial","univariate","equation"]));
6.630 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.631 - setNextTactic 1 (Model_Problem );
6.632 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.633 - setNextTactic 1 (Specify_Theory "PolyEq");
6.634 - (*------------- some trials in the problem-hierarchy ---------------*)
6.635 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
6.636 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
6.637 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
6.638 - (*------------------------------------------------------------------*)
6.639 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.640 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
6.641 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.642 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
6.643 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.644 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
6.645 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.646 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
6.647 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.648 - (*==================================================================*)
6.649 - setNextTactic 1 Or_to_List;
6.650 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.651 - setNextTactic 1 (Check_elementwise "Assumptions");
6.652 - (*WAS: exception Match raised (line 1218 of ".../script.sml")*)
6.653 -"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
6.654 -val ((pt, _), _) = get_calc cI;
6.655 -val ip = get_pos cI 1;
6.656 -(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
6.657 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
6.658 -val (mI,m) = mk_tac'_ tac;
6.659 -val Appl m = applicable_in p pt m;
6.660 -member op = specsteps mI (*false*);
6.661 -(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
6.662 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
6.663 -(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
6.664 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
6.665 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
6.666 - val thy' = get_obj g_domID pt (par_pblobj pt p);
6.667 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
6.668 - val d = e_rls;
6.669 -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
6.670 - WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
6.671 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
6.672 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
6.673 - ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
6.674 -val thy = assoc_thy thy';
6.675 -l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
6.676 -(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
6.677 - ... Assoc ... is correct*)
6.678 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
6.679 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
6.680 -1 < length l (*true*);
6.681 -val up = drop_last l;
6.682 - term2str (go up sc);
6.683 - (go up sc);
6.684 -(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
6.685 - ... ???? ... is correct*)
6.686 -"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
6.687 - (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
6.688 - val l = drop_last l; (*comes from e, goes to Abs*)
6.689 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
6.690 - val i = mk_Free (i, T);
6.691 - val E = upd_env E (i, v);
6.692 -(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
6.693 -val [(tac_, mout, ptree, pos', xxx)] = ss;
6.694 -val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
6.695 -(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
6.696 - ... Assoc ... is correct*)
6.697 -"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
6.698 - ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
6.699 -val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
6.700 - val ctxt = get_ctxt pt (p,p_)
6.701 - val p' = lev_on p : pos;
6.702 -(* WAS val NotAss = assod pt d m stac
6.703 - ... Ass ... is correct*)
6.704 -"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
6.705 - (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
6.706 -consts = consts' (*WAS false*);
6.707 -(*==================================================================*)
6.708 -
6.709 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.710 - setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
6.711 - "univariate","equation"]);
6.712 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.713 - setNextTactic 1 (Check_Postcond ["normalize","polynomial",
6.714 - "univariate","equation"]);
6.715 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
6.716 - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
6.717 - val (ptp,_) = get_calc 1;
6.718 - val (Form t,_,_) = pt_extract ptp;
6.719 - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
6.720 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
6.721 -DEconstrCalcTree 1;
6.722 -
6.723 -"--------- tryMatchProblem, tryRefineProblem ------------";
6.724 -"--------- tryMatchProblem, tryRefineProblem ------------";
6.725 -"--------- tryMatchProblem, tryRefineProblem ------------";
6.726 -(*{\bf\UC{Having \isac{} Refine the Problem
6.727 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
6.728 - * x^^^2 + 4*x + 5 = 2
6.729 -see isac.bridge.TestSpecify#testMatchRefine*)
6.730 - CalcTree
6.731 - [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
6.732 - ("Isac",
6.733 - ["univariate","equation"],
6.734 - ["no_met"]))];
6.735 - Iterator 1;
6.736 - moveActiveRoot 1;
6.737 -
6.738 - fetchProposedTactic 1;
6.739 - setNextTactic 1 (Model_Problem );
6.740 - (*..this tactic should be done 'tacitly', too !*)
6.741 -
6.742 -(*
6.743 -autoCalculate 1 CompleteCalcHead;
6.744 -checkContext 1 ([],Pbl) "pbl_equ_univ";
6.745 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
6.746 -*)
6.747 -
6.748 - autoCalculate 1 (Step 1);
6.749 -
6.750 - fetchProposedTactic 1;
6.751 - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
6.752 - autoCalculate 1 (Step 1);
6.753 -
6.754 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
6.755 -initContext 1 Pbl_ ([],Pbl);
6.756 -initContext 1 Met_ ([],Pbl);
6.757 -
6.758 - "--------- this match will show some incomplete items: ---------";
6.759 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
6.760 -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
6.761 -
6.762 -
6.763 - fetchProposedTactic 1;
6.764 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
6.765 -
6.766 - fetchProposedTactic 1;
6.767 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
6.768 -
6.769 - "--------- this is a matching model (all items correct): -------";
6.770 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
6.771 - "--------- this is a NOT matching model (some 'false': ---------";
6.772 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
6.773 -
6.774 - "--------- find out a matching problem: ------------------------";
6.775 - "--------- find out a matching problem (FAILING: no new pbl) ---";
6.776 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
6.777 -
6.778 - "--------- find out a matching problem (SUCCESSFUL) ------------";
6.779 - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
6.780 -
6.781 - "--------- tryMatch, tryRefine did not change the calculation -";
6.782 - "--------- this is done by <TRANSFER> on the pbl-browser: ------";
6.783 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
6.784 - "univariate","equation"]);
6.785 - autoCalculate 1 (Step 1);
6.786 -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
6.787 - and Specify_Theory skipped in comparison to below ---^^^-inserted *)
6.788 -(*------------vvv-inserted-----------------------------------------------*)
6.789 - fetchProposedTactic 1;
6.790 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
6.791 - "univariate","equation"]);
6.792 - autoCalculate 1 (Step 1);
6.793 -
6.794 -(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
6.795 -
6.796 - fetchProposedTactic 1;
6.797 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
6.798 - autoCalculate 1 (Step 1);
6.799 -
6.800 - fetchProposedTactic 1;
6.801 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
6.802 -
6.803 - autoCalculate 1 CompleteCalc;
6.804 -
6.805 - val ((pt,_),_) = get_calc 1;
6.806 - show_pt pt;
6.807 - val p = get_pos 1 1;
6.808 - val (Form f, tac, asms) = pt_extract (pt, p);
6.809 -(*========== inhibit exn 110719 ================================================
6.810 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
6.811 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
6.812 -========== inhibit exn 110719 ================================================*)
6.813 -
6.814 -(*------------^^^-inserted-----------------------------------------------*)
6.815 -(*WN050904 the fetchProposedTactic's below may not have worked like that
6.816 - before, too, because there was no check*)
6.817 - fetchProposedTactic 1;
6.818 - setNextTactic 1 (Specify_Theory "PolyEq");
6.819 - autoCalculate 1 (Step 1);
6.820 -
6.821 - fetchProposedTactic 1;
6.822 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
6.823 - autoCalculate 1 (Step 1);
6.824 -
6.825 - fetchProposedTactic 1;
6.826 - "--------- now the calc-header is ready for enter 'solving' ----";
6.827 - autoCalculate 1 CompleteCalc;
6.828 -
6.829 - val ((pt,_),_) = get_calc 1;
6.830 - rootthy pt;
6.831 - show_pt pt;
6.832 - val p = get_pos 1 1;
6.833 -
6.834 -(*============ inhibit exn AK110719 ==============================================
6.835 -(* ERROR: execption Bind raised *)
6.836 - val (Form f, tac, asms) = pt_extract (pt, p);
6.837 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
6.838 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
6.839 -============ inhibit exn AK110719 ==============================================*)
6.840 -
6.841 -(* (* AK110727 Debugging (to be continued) *)
6.842 - asms; (*term list (!)*)
6.843 - print_depth 99;
6.844 - pt_extract (pt, p); (* ptform * tac option * term list*)
6.845 - (Form f, tac, asms);
6.846 - val (myval,myval2,myval3s) = pt_extract (pt,p);
6.847 -
6.848 -"~~~~~ fun pt_extract, args:"; val ((pt, pos as (p,p_(*Frm,Pbl*)))) = ((pt, p));
6.849 - val ppobj = get_obj I pt p;
6.850 - is_pblobj ppobj; (*true*)
6.851 - pt_model ppobj p_;
6.852 - val tac = g_tac ppobj;
6.853 - (f, SOME tac, []) (* term * tac option * 'a list (!) *)
6.854 -*)
6.855 -
6.856 -DEconstrCalcTree 1;
6.857 -
6.858 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
6.859 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
6.860 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
6.861 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.862 - ("Test", ["sqroot-test","univariate","equation","test"],
6.863 - ["Test","squ-equ-test-subpbl1"]))];
6.864 - Iterator 1;
6.865 - moveActiveRoot 1;
6.866 -
6.867 - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
6.868 - "solve (x+1=2, x)",(*the headline*)
6.869 - [Given ["equality (x+1=(2::real))", "solveFor x"],
6.870 - Find ["solutions L"](*,Relate []*)],
6.871 - Pbl,
6.872 - ("Test",
6.873 - ["sqroot-test","univariate","equation","test"],
6.874 - ["Test","squ-equ-test-subpbl1"]));
6.875 -
6.876 -val ((Nd (PblObj {env = NONE,
6.877 - fmz = (fm, tpm),
6.878 - loc = (SOME scrst_ctxt, NONE),
6.879 - ctxt,
6.880 - cell = NONE,
6.881 - meth,
6.882 - spec = (thy,
6.883 - ["sqroot-test", "univariate", "equation", "test"],
6.884 - ["Test", "squ-equ-test-subpbl1"]),
6.885 - probl,
6.886 - branch = TransitiveB,
6.887 - origin,
6.888 - ostate = Incomplete,
6.889 - result},
6.890 - []),
6.891 - ([], Pbl)),
6.892 - []) = get_calc 1;
6.893 -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
6.894 -if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
6.895 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
6.896 -
6.897 -resetCalcHead 1;
6.898 -modelProblem 1;
6.899 -
6.900 -get_calc 1;
6.901 -val ((Nd (PblObj {env = NONE,
6.902 - fmz = (fm, tpm),
6.903 - loc = (SOME scrst_ctxt, NONE),
6.904 - ctxt,
6.905 - cell = NONE,
6.906 - meth,
6.907 - spec = ("e_domID", ["e_pblID"], ["e_metID"]),
6.908 - probl,
6.909 - branch = TransitiveB,
6.910 - origin,
6.911 - ostate = Incomplete,
6.912 - result},
6.913 - []),
6.914 - ([], Pbl)),
6.915 - []) = get_calc 1;
6.916 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
6.917 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
6.918 -
6.919 -"--------- maximum-example, UC: Modeling an example -----";
6.920 -"--------- maximum-example, UC: Modeling an example -----";
6.921 -"--------- maximum-example, UC: Modeling an example -----";
6.922 -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
6.923 -see isac.bridge.TestModel#testEditItems
6.924 -*)
6.925 - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
6.926 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
6.927 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
6.928 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
6.929 - (*^^^ these are the elements for the root-problem (in variants)*)
6.930 - (*vvv these are elements required for subproblems*)
6.931 - "boundVariable a","boundVariable b","boundVariable alpha",
6.932 - "interval {x::real. 0 <= x & x <= 2*r}",
6.933 - "interval {x::real. 0 <= x & x <= 2*r}",
6.934 - "interval {x::real. 0 <= x & x <= pi}",
6.935 - "errorBound (eps=(0::real))"]
6.936 - (*specifying is not interesting for this example*)
6.937 - val spec = ("DiffApp", ["maximum_of","function"],
6.938 - ["DiffApp","max_by_calculus"]);
6.939 - (*the empty model with descriptions for user-guidance by Model_Problem*)
6.940 - val empty_model = [Given ["fixedValues []"],
6.941 - Find ["maximum", "valuesFor"],
6.942 - Relate ["relations []"]];
6.943 - DEconstrCalcTree 1;
6.944 -
6.945 -"#################################################################";
6.946 -
6.947 - CalcTree [(elems, spec)];
6.948 - Iterator 1;
6.949 - moveActiveRoot 1;
6.950 - refFormula 1 (get_pos 1 1);
6.951 - (*this gives a completely empty model*)
6.952 -
6.953 - fetchProposedTactic 1;
6.954 -(*fill the CalcHead with Descriptions...*)
6.955 - setNextTactic 1 (Model_Problem );
6.956 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.957 -
6.958 - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
6.959 - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
6.960 - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
6.961 - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
6.962 - "Problem (DiffApp.thy, [maximum_of, function])",
6.963 - (*the head-form ^^^ is not used for input here*)
6.964 - [Given ["fixedValues [r=Arbfix]"(*new input*)],
6.965 - Find ["maximum b"(*new input*), "valuesFor"],
6.966 - Relate ["relations"]],
6.967 - (*input (Arbfix will dissappear soon)*)
6.968 - Pbl (*belongsto*),
6.969 - e_spec (*no input to the specification*));
6.970 -
6.971 - (*the user does not know, what 'superfluous' for 'maximum b' may mean
6.972 - and asks what to do next*)
6.973 - fetchProposedTactic 1;
6.974 - (*the student follows the advice*)
6.975 - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
6.976 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
6.977 -
6.978 - (*this input completes the model*)
6.979 - modifyCalcHead 1 (([],Pbl), "not used here",
6.980 - [Given ["fixedValues [r=Arbfix]"],
6.981 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.982 - Relate ["relations [A=a*b, \
6.983 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
6.984 -
6.985 - (*specification is not interesting and should be skipped by the dialogguide;
6.986 - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
6.987 - modifyCalcHead 1 (([],Pbl), "not used here",
6.988 - [Given ["fixedValues [r=Arbfix]"],
6.989 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.990 - Relate ["relations [A=a*b, \
6.991 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
6.992 - ("DiffApp", ["e_pblID"], ["e_metID"]));
6.993 - modifyCalcHead 1 (([],Pbl), "not used here",
6.994 - [Given ["fixedValues [r=Arbfix]"],
6.995 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.996 - Relate ["relations [A=a*b, \
6.997 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
6.998 - ("DiffApp", ["maximum_of","function"],
6.999 - ["e_metID"]));
6.1000 - modifyCalcHead 1 (([],Pbl), "not used here",
6.1001 - [Given ["fixedValues [r=Arbfix]"],
6.1002 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
6.1003 - Relate ["relations [A=a*b, \
6.1004 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
6.1005 - ("DiffApp", ["maximum_of","function"],
6.1006 - ["DiffApp","max_by_calculus"]));
6.1007 - (*this final calcHead now has STATUS 'complete' !*)
6.1008 - DEconstrCalcTree 1;
6.1009 -
6.1010 -"--------- solve_linear from pbl-hierarchy --------------";
6.1011 -"--------- solve_linear from pbl-hierarchy --------------";
6.1012 -"--------- solve_linear from pbl-hierarchy --------------";
6.1013 - val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
6.1014 - CalcTree [(fmz, sp)];
6.1015 - Iterator 1; moveActiveRoot 1;
6.1016 - refFormula 1 (get_pos 1 1);
6.1017 - modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
6.1018 - [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
6.1019 - Find ["solutions L"]],
6.1020 - Pbl,
6.1021 - ("Test", ["linear","univariate","equation","test"],
6.1022 - ["Test","solve_linear"]));
6.1023 - autoCalculate 1 CompleteCalc;
6.1024 - refFormula 1 (get_pos 1 1);
6.1025 - val ((pt,_),_) = get_calc 1;
6.1026 - val p = get_pos 1 1;
6.1027 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1028 - if term2str f = "[x = 1]" andalso p = ([], Res)
6.1029 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
6.1030 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
6.1031 - DEconstrCalcTree 1;
6.1032 -
6.1033 -"--------- solve_linear as in an algebra system (CAS)----";
6.1034 -"--------- solve_linear as in an algebra system (CAS)----";
6.1035 -"--------- solve_linear as in an algebra system (CAS)----";
6.1036 - val (fmz, sp) = ([], ("", [], []));
6.1037 - CalcTree [(fmz, sp)];
6.1038 - Iterator 1; moveActiveRoot 1;
6.1039 - modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
6.1040 - autoCalculate 1 CompleteCalc;
6.1041 - refFormula 1 (get_pos 1 1);
6.1042 - val ((pt,_),_) = get_calc 1;
6.1043 - val p = get_pos 1 1;
6.1044 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1045 - if term2str f = "[x = 1]" andalso p = ([], Res)
6.1046 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
6.1047 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
6.1048 -DEconstrCalcTree 1;
6.1049 -
6.1050 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
6.1051 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
6.1052 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
6.1053 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1054 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1055 - ["Test","squ-equ-test-subpbl1"]))];
6.1056 - Iterator 1;
6.1057 - moveActiveRoot 1;
6.1058 - autoCalculate 1 CompleteCalc;
6.1059 - val ((pt,_),_) = get_calc 1;
6.1060 - show_pt pt;
6.1061 -
6.1062 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
6.1063 - interSteps 1 ([2],Res);
6.1064 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
6.1065 - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
6.1066 - getFormulaeFromTo 1 unc gen 1 false;
6.1067 -
6.1068 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
6.1069 - interSteps 1 ([3,2],Res);
6.1070 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
6.1071 - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
6.1072 - getFormulaeFromTo 1 unc gen 1 false;
6.1073 -
6.1074 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
6.1075 - interSteps 1 ([3],Res) (*no new steps in subproblems*);
6.1076 - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
6.1077 - getFormulaeFromTo 1 unc gen 1 false;
6.1078 -
6.1079 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
6.1080 - interSteps 1 ([],Res) (*no new steps in subproblems*);
6.1081 - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
6.1082 - getFormulaeFromTo 1 unc gen 1 false;
6.1083 -DEconstrCalcTree 1;
6.1084 -
6.1085 -"--------- getTactic, fetchApplicableTactics ------------";
6.1086 -"--------- getTactic, fetchApplicableTactics ------------";
6.1087 -"--------- getTactic, fetchApplicableTactics ------------";
6.1088 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1089 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1090 - ["Test","squ-equ-test-subpbl1"]))];
6.1091 - Iterator 1; moveActiveRoot 1;
6.1092 - autoCalculate 1 CompleteCalc;
6.1093 - val ((pt,_),_) = get_calc 1;
6.1094 - show_pt pt;
6.1095 -
6.1096 - (*UC\label{SOLVE:HIDE:getTactic}*)
6.1097 - getTactic 1 ([],Pbl);
6.1098 - getTactic 1 ([1],Res);
6.1099 - getTactic 1 ([3],Pbl);
6.1100 - getTactic 1 ([3,1],Frm);
6.1101 - getTactic 1 ([3],Res);
6.1102 - getTactic 1 ([],Res);
6.1103 -
6.1104 -(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
6.1105 - fetchApplicableTactics 1 99999 ([],Pbl);
6.1106 - fetchApplicableTactics 1 99999 ([1],Res);
6.1107 - fetchApplicableTactics 1 99999 ([3],Pbl);
6.1108 - fetchApplicableTactics 1 99999 ([3,1],Res);
6.1109 - fetchApplicableTactics 1 99999 ([3],Res);
6.1110 - fetchApplicableTactics 1 99999 ([],Res);
6.1111 -DEconstrCalcTree 1;
6.1112 -
6.1113 -"--------- getAssumptions, getAccumulatedAsms -----------";
6.1114 -"--------- getAssumptions, getAccumulatedAsms -----------";
6.1115 -"--------- getAssumptions, getAccumulatedAsms -----------";
6.1116 -CalcTree
6.1117 -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
6.1118 - "solveFor x","solutions L"],
6.1119 - ("RatEq",["univariate","equation"],["no_met"]))];
6.1120 -Iterator 1; moveActiveRoot 1;
6.1121 -autoCalculate 1 CompleteCalc;
6.1122 -val ((pt,_),_) = get_calc 1;
6.1123 -val p = get_pos 1 1;
6.1124 -val (Form f, tac, asms) = pt_extract (pt, p);
6.1125 -if map term2str asms =
6.1126 - ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
6.1127 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
6.1128 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
6.1129 - "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
6.1130 -andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
6.1131 -else error "TODO compare 2002--2011";
6.1132 -
6.1133 -(*UC\label{SOLVE:HELP:assumptions}*)
6.1134 -getAssumptions 1 ([3], Res);
6.1135 -getAssumptions 1 ([5], Res);
6.1136 -(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
6.1137 -getAccumulatedAsms 1 ([3], Res);
6.1138 -getAccumulatedAsms 1 ([5], Res);
6.1139 -DEconstrCalcTree 1;
6.1140 -
6.1141 -"--------- arbitrary combinations of steps --------------";
6.1142 -"--------- arbitrary combinations of steps --------------";
6.1143 -"--------- arbitrary combinations of steps --------------";
6.1144 - CalcTree (*start of calculation, return No.1*)
6.1145 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
6.1146 - ("Test",
6.1147 - ["linear","univariate","equation","test"],
6.1148 - ["Test","solve_linear"]))];
6.1149 - Iterator 1; moveActiveRoot 1;
6.1150 -
6.1151 - fetchProposedTactic 1;
6.1152 - (*ERROR get_calc 1 not existent*)
6.1153 - setNextTactic 1 (Model_Problem );
6.1154 - autoCalculate 1 (Step 1);
6.1155 - fetchProposedTactic 1;
6.1156 - fetchProposedTactic 1;
6.1157 -
6.1158 - setNextTactic 1 (Add_Find "solutions L");
6.1159 - setNextTactic 1 (Add_Find "solutions L");
6.1160 -
6.1161 - autoCalculate 1 (Step 1);
6.1162 - autoCalculate 1 (Step 1);
6.1163 -
6.1164 - setNextTactic 1 (Specify_Theory "Test");
6.1165 - fetchProposedTactic 1;
6.1166 - autoCalculate 1 (Step 1);
6.1167 -
6.1168 - autoCalculate 1 (Step 1);
6.1169 - autoCalculate 1 (Step 1);
6.1170 - autoCalculate 1 (Step 1);
6.1171 - autoCalculate 1 (Step 1);
6.1172 -(*------------------------- end calc-head*)
6.1173 -
6.1174 - fetchProposedTactic 1;
6.1175 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
6.1176 - autoCalculate 1 (Step 1);
6.1177 -
6.1178 - setNextTactic 1 (Rewrite_Set "Test_simplify");
6.1179 - fetchProposedTactic 1;
6.1180 - autoCalculate 1 (Step 1);
6.1181 -
6.1182 - autoCalculate 1 CompleteCalc;
6.1183 - val ((pt,_),_) = get_calc 1;
6.1184 - val p = get_pos 1 1;
6.1185 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1186 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
6.1187 - error "FE-interface.sml: diff.behav. in combinations of steps";
6.1188 -DEconstrCalcTree 1;
6.1189 -
6.1190 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
6.1191 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
6.1192 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
6.1193 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1194 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1195 - ["Test","squ-equ-test-subpbl1"]))];
6.1196 - Iterator 1;
6.1197 - moveActiveRoot 1;
6.1198 - autoCalculate 1 CompleteCalcHead;
6.1199 - autoCalculate 1 (Step 1);
6.1200 - autoCalculate 1 (Step 1);
6.1201 - appendFormula 1 "-1 + x = 0";
6.1202 - (*... returns calcChangedEvent with*)
6.1203 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
6.1204 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
6.1205 -
6.1206 - val ((pt,_),_) = get_calc 1;
6.1207 - val p = get_pos 1 1;
6.1208 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1209 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
6.1210 - error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
6.1211 -DEconstrCalcTree 1;
6.1212 -
6.1213 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
6.1214 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
6.1215 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
6.1216 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1217 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1218 - ["Test","squ-equ-test-subpbl1"]))];
6.1219 - Iterator 1;
6.1220 - moveActiveRoot 1;
6.1221 - autoCalculate 1 CompleteCalcHead;
6.1222 - autoCalculate 1 (Step 1);
6.1223 - autoCalculate 1 (Step 1);
6.1224 - appendFormula 1 "x - 1 = 0";
6.1225 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
6.1226 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
6.1227 - (*11 elements !!!*)
6.1228 -
6.1229 - val ((pt,_),_) = get_calc 1;
6.1230 - val p = get_pos 1 1;
6.1231 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1232 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
6.1233 - error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
6.1234 -DEconstrCalcTree 1;
6.1235 -
6.1236 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
6.1237 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
6.1238 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
6.1239 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1240 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1241 - ["Test","squ-equ-test-subpbl1"]))];
6.1242 - Iterator 1;
6.1243 - moveActiveRoot 1;
6.1244 - autoCalculate 1 CompleteCalcHead;
6.1245 - autoCalculate 1 (Step 1);
6.1246 - autoCalculate 1 (Step 1);
6.1247 - appendFormula 1 "x = 1";
6.1248 - (*... returns calcChangedEvent with*)
6.1249 - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
6.1250 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
6.1251 - (*6 elements !!!*)
6.1252 -
6.1253 - val ((pt,_),_) = get_calc 1;
6.1254 - val p = get_pos 1 1;
6.1255 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1256 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
6.1257 - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
6.1258 -DEconstrCalcTree 1;
6.1259 -
6.1260 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
6.1261 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
6.1262 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
6.1263 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1264 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1265 - ["Test","squ-equ-test-subpbl1"]))];
6.1266 - Iterator 1;
6.1267 - moveActiveRoot 1;
6.1268 - autoCalculate 1 CompleteCalcHead;
6.1269 - autoCalculate 1 (Step 1);
6.1270 - autoCalculate 1 (Step 1);
6.1271 - appendFormula 1 "x - 4711 = 0";
6.1272 - (*... returns <ERROR> no derivation found </ERROR>*)
6.1273 -
6.1274 - val ((pt,_),_) = get_calc 1;
6.1275 - val p = get_pos 1 1;
6.1276 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1277 - if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
6.1278 - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
6.1279 -DEconstrCalcTree 1;
6.1280 -
6.1281 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
6.1282 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
6.1283 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
6.1284 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1285 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1286 - ["Test","squ-equ-test-subpbl1"]))];
6.1287 - Iterator 1;
6.1288 - moveActiveRoot 1;
6.1289 - autoCalculate 1 CompleteCalc;
6.1290 - moveActiveFormula 1 ([2],Res);
6.1291 - replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
6.1292 - (*... returns <ERROR> formula not changed </ERROR>*)
6.1293 -
6.1294 - val ((pt,_),_) = get_calc 1;
6.1295 - val p = get_pos 1 1;
6.1296 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1297 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
6.1298 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
6.1299 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
6.1300 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
6.1301 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
6.1302 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
6.1303 -
6.1304 -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
6.1305 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1306 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1307 - ["Test","squ-equ-test-subpbl1"]))];
6.1308 - Iterator 2;
6.1309 - moveActiveRoot 2;
6.1310 - autoCalculate 2 CompleteCalc;
6.1311 - moveActiveFormula 2 ([2],Res);
6.1312 - replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
6.1313 - (*... returns <ERROR> formula not changed </ERROR>*)
6.1314 -
6.1315 - val ((pt,_),_) = get_calc 2;
6.1316 - val p = get_pos 2 1;
6.1317 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1318 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
6.1319 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
6.1320 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
6.1321 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
6.1322 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
6.1323 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
6.1324 -DEconstrCalcTree 1;
6.1325 -
6.1326 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
6.1327 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
6.1328 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
6.1329 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1330 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1331 - ["Test","squ-equ-test-subpbl1"]))];
6.1332 - Iterator 1;
6.1333 - moveActiveRoot 1;
6.1334 - autoCalculate 1 CompleteCalc;
6.1335 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
6.1336 - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
6.1337 - (*... returns calcChangedEvent with*)
6.1338 - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
6.1339 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
6.1340 -
6.1341 - val ((pt,_),_) = get_calc 1;
6.1342 - show_pt pt;
6.1343 - val p = get_pos 1 1;
6.1344 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1345 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
6.1346 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
6.1347 -(* for getting the list in whole length ...
6.1348 -print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
6.1349 - *)
6.1350 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
6.1351 - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
6.1352 - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
6.1353 - ([2, 8], Res), ([2, 9], Res), ([2], Res)
6.1354 -(*WN060727 {cutlevup->test_trans} removed: ,
6.1355 - ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
6.1356 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
6.1357 -DEconstrCalcTree 1;
6.1358 -
6.1359 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
6.1360 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
6.1361 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
6.1362 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1363 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1364 - ["Test","squ-equ-test-subpbl1"]))];
6.1365 - Iterator 1;
6.1366 - moveActiveRoot 1;
6.1367 - autoCalculate 1 CompleteCalc;
6.1368 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
6.1369 - replaceFormula 1 "x = 1"; (*<-------------------------------------*)
6.1370 - (*... returns calcChangedEvent with ...*)
6.1371 - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
6.1372 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
6.1373 - (*9 elements !!!*)
6.1374 -
6.1375 - val ((pt,_),_) = get_calc 1;
6.1376 - show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
6.1377 - val (t,_) = get_obj g_result pt [3,2]; term2str t;
6.1378 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
6.1379 - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
6.1380 - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
6.1381 - ([3,2],Res)] then () else
6.1382 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
6.1383 -
6.1384 - val p = get_pos 1 1;
6.1385 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1386 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
6.1387 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
6.1388 -DEconstrCalcTree 1;
6.1389 -
6.1390 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
6.1391 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
6.1392 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
6.1393 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
6.1394 - ("Test", ["sqroot-test","univariate","equation","test"],
6.1395 - ["Test","squ-equ-test-subpbl1"]))];
6.1396 - Iterator 1;
6.1397 - moveActiveRoot 1;
6.1398 - autoCalculate 1 CompleteCalc;
6.1399 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
6.1400 - replaceFormula 1 "x - 4711 = 0";
6.1401 - (*... returns <ERROR> no derivation found </ERROR>*)
6.1402 -
6.1403 - val ((pt,_),_) = get_calc 1;
6.1404 - show_pt pt;
6.1405 - val p = get_pos 1 1;
6.1406 - val (Form f, tac, asms) = pt_extract (pt, p);
6.1407 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
6.1408 - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
6.1409 -DEconstrCalcTree 1;
6.1410 -
6.1411 -
6.1412 -
6.1413 +*}
6.1414 +ML{*
6.1415 +*}
6.1416 +ML{*
6.1417 +*}
6.1418 +ML{*
6.1419 *}
6.1420 ML{*
6.1421 *}