1.1 --- a/test/Tools/isac/Frontend/interface.sml Tue Jul 19 10:28:36 2011 +0200
1.2 +++ b/test/Tools/isac/Frontend/interface.sml Tue Jul 19 13:07:28 2011 +0200
1.3 @@ -136,7 +136,6 @@
1.4
1.5 (*-------------------------------------------------------------------------*)
1.6 fetchProposedTactic 1;
1.7 -(*========== inhibit exn 110310 ================================================
1.8 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.9
1.10 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.11 @@ -168,9 +167,7 @@
1.12 (*exception just above means: 'ModSpec' has been returned: error anyway*)
1.13 if term2str f = "[x = 1]" then () else
1.14 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
1.15 -============ inhibit exn 110310 ==============================================*)
1.16
1.17 -(*========== inhibit exn 110620 ================================================
1.18 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.19 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.20 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
1.21 @@ -193,7 +190,6 @@
1.22 if get_pos 1 1 = ([], Res) then () else
1.23 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
1.24 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
1.25 -============ inhibit exn 110620 ==============================================*)
1.26
1.27 "--------- miniscript with mini-subpbl ------------------";
1.28 "--------- miniscript with mini-subpbl ------------------";
1.29 @@ -407,8 +403,9 @@
1.30 ["Test","solve_linear"]))];
1.31 Iterator 1;
1.32 moveActiveRoot 1;
1.33 +
1.34 + autoCalculate 1 CompleteCalcHead;
1.35 (*========== inhibit exn 110718 ================================================
1.36 - autoCalculate 1 CompleteCalcHead;
1.37 refFormula 1 (get_pos 1 1);
1.38 val ((pt,p),_) = get_calc 1;
1.39
1.40 @@ -479,8 +476,8 @@
1.41 ["Test","solve_linear"]))];
1.42 Iterator 1;
1.43 moveActiveRoot 1;
1.44 -(*========== inhibit exn 110718 ================================================
1.45 - autoCalculate 1 CompleteModel;
1.46 + autoCalculate 1 CompleteModel;
1.47 +(*========== inhibit exn 110718 ================================================
1.48 refFormula 1 (get_pos 1 1);
1.49
1.50 setProblem 1 ["linear","univariate","equation","test"];
1.51 @@ -572,17 +569,15 @@
1.52 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
1.53 val ((pt,_),_) = get_calc 1;
1.54 val p = get_pos 1 1;
1.55 -(*========== inhibit exn 110622 ================================================
1.56 +
1.57 val (Form f, tac, asms) = pt_extract (pt, p);
1.58 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1.59 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
1.60 -============ inhibit exn 110622 ==============================================*)
1.61
1.62
1.63 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.64 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.65 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
1.66 -(*========== inhibit exn 110622 ================================================
1.67 states:=[];
1.68 CalcTree
1.69 [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
1.70 @@ -590,6 +585,9 @@
1.71 Iterator 1;
1.72 moveActiveRoot 1;
1.73 fetchProposedTactic 1;
1.74 +
1.75 +(*========== inhibit exn 110622 ================================================
1.76 +(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
1.77 setNextTactic 1 (Model_Problem );
1.78 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.79 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.80 @@ -704,7 +702,7 @@
1.81 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
1.82 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
1.83 ============ inhibit exn 2009 ================================================*)
1.84 -============ inhibit exn 110622 ==============================================*)
1.85 +============ inhibit exn 110719 ==============================================*)
1.86
1.87
1.88 "--------- tryMatchProblem, tryRefineProblem ------------";
1.89 @@ -787,15 +785,16 @@
1.90
1.91 fetchProposedTactic 1;
1.92 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.93 -(*========== inhibit exn 110622 ================================================
1.94 - vvvvvvvvvvvv
1.95 +
1.96 autoCalculate 1 CompleteCalc;
1.97 +(*========== inhibit exn 110719 ================================================
1.98 val ((pt,_),_) = get_calc 1;
1.99 show_pt pt;
1.100 val p = get_pos 1 1;
1.101 val (Form f, tac, asms) = pt_extract (pt, p);
1.102 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.103 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.104 +========== inhibit exn 110719 ================================================*)
1.105
1.106 (*------------^^^-inserted-----------------------------------------------*)
1.107 (*WN050904 the fetchProposedTactic's below may not have worked like that
1.108 @@ -812,6 +811,7 @@
1.109 "--------- now the calc-header is ready for enter 'solving' ----";
1.110 autoCalculate 1 CompleteCalc;
1.111
1.112 +(*============ inhibit exn 110719 ==============================================
1.113 val ((pt,_),_) = get_calc 1;
1.114 rootthy pt;
1.115 show_pt pt;
1.116 @@ -819,7 +819,7 @@
1.117 val (Form f, tac, asms) = pt_extract (pt, p);
1.118 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
1.119 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
1.120 -============ inhibit exn 110622 ==============================================*)
1.121 +============ inhibit exn 110719 ==============================================*)
1.122
1.123
1.124 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
1.125 @@ -1121,7 +1121,7 @@
1.126
1.127 fetchProposedTactic 1;
1.128 (*========== inhibit exn 110628 ================================================
1.129 - ERROR get_calc 1 not existent
1.130 + (*ERROR get_calc 1 not existent*)
1.131 setNextTactic 1 (Model_Problem );
1.132 autoCalculate 1 (Step 1);
1.133
1.134 @@ -1231,10 +1231,8 @@
1.135 val ((pt,_),_) = get_calc 1;
1.136 val p = get_pos 1 1;
1.137 val (Form f, tac, asms) = pt_extract (pt, p);
1.138 -(*========== inhibit exn 110628 ================================================
1.139 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1.140 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1.141 -============ inhibit exn 110682 ==============================================*)
1.142
1.143
1.144 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1.145 @@ -1275,7 +1273,6 @@
1.146
1.147 val ((pt,_),_) = get_calc 1;
1.148 val p = get_pos 1 1;
1.149 -(*========== inhibit exn 110628 ================================================
1.150 val (Form f, tac, asms) = pt_extract (pt, p);
1.151 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.152 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.153 @@ -1283,7 +1280,6 @@
1.154 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.155 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.156 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1.157 - ============ inhibit exn 110682 ==============================================*)
1.158
1.159 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1.160 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.161 @@ -1298,7 +1294,6 @@
1.162
1.163 val ((pt,_),_) = get_calc 2;
1.164 val p = get_pos 2 1;
1.165 -(*========== inhibit exn 110628 ================================================
1.166 val (Form f, tac, asms) = pt_extract (pt, p);
1.167 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.168 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1.169 @@ -1306,9 +1301,7 @@
1.170 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1.171 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1.172 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1.173 - ============ inhibit exn 110682 ==============================================*)
1.174
1.175 -(*========== inhibit exn 110628 ================================================
1.176 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.177 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.178 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1.179 @@ -1395,5 +1388,5 @@
1.180 val (Form f, tac, asms) = pt_extract (pt, p);
1.181 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1.182 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1.183 -============ inhibit exn 110628 ==============================================*)
1.184
1.185 +
2.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 10:28:36 2011 +0200
2.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 13:07:28 2011 +0200
2.3 @@ -1,3 +1,6 @@
2.4 +
2.5 +
2.6 +
2.7 (* tests for sml/ME/ctree.sml
2.8 authors: Walther Neuper 060113
2.9 (c) due to copyright terms
2.10 @@ -144,10 +147,8 @@
2.11 else error "new behaviour in test: miniscript with mini-subpbl";
2.12
2.13 show_pt pt;
2.14 -(*========== inhibit exn WN110319 ==============================================
2.15 -============ inhibit exn WN110319 ============================================*)
2.16
2.17 -(*=== inhibit exn ?=============================================================
2.18 +
2.19
2.20 "-------------- get_allpos' (from ptree above)--------------------";
2.21 "-------------- get_allpos' (from ptree above)--------------------";
2.22 @@ -538,7 +539,10 @@
2.23 "=====new ptree 3 ================================================";
2.24 "=====new ptree 3 ================================================";
2.25 "=====new ptree 3 ================================================";
2.26 - states:=[];
2.27 +
2.28 +(*========== inhibit exn AK110719 ==============================================
2.29 +(* ERROR: get_pos *)
2.30 +states:=[];
2.31 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
2.32 ("Test", ["sqroot-test","univariate","equation","test"],
2.33 ["Test","squ-equ-test-subpbl1"]))];
2.34 @@ -547,6 +551,7 @@
2.35
2.36 val ((pt,_),_) = get_calc 1;
2.37 show_pt pt;
2.38 +============ inhibit exn AK110719 ============================================*)
2.39
2.40 "-------------- move_dn ------------------------------------------";
2.41 "-------------- move_dn ------------------------------------------";
2.42 @@ -567,13 +572,16 @@
2.43 (*
2.44 val p = (move_dn [] pt p) handle e => print_exn_G e;
2.45 Exception PTREE end of calculation*)
2.46 +(*========== inhibit exn AK110719 ==============================================
2.47 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
2.48 +============ inhibit exn AK110719 ============================================*)
2.49 +
2.50
2.51
2.52 "-------------- move_dn: Frm -> Res ------------------------------";
2.53 "-------------- move_dn: Frm -> Res ------------------------------";
2.54 "-------------- move_dn: Frm -> Res ------------------------------";
2.55 - states := [];
2.56 + (*states := [];
2.57 CalcTree (*start of calculation, return No.1*)
2.58 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
2.59 ("Test",
2.60 @@ -596,7 +604,7 @@
2.61 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
2.62 if get_pos 1 1 = ([1], Res) then ()
2.63 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
2.64 - moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
2.65 + moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)*)
2.66
2.67
2.68 "-------------- move_up ------------------------------------------";
2.69 @@ -614,7 +622,9 @@
2.70 val p = move_up [] pt p; (*-> ([],Pbl)*)
2.71 (*val p = (move_up [] pt p) handle e => print_exn_G e;
2.72 Exception PTREE begin of calculation*)
2.73 +(*========== inhibit exn AK110719 ==============================================
2.74 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
2.75 +========== inhibit exn AK110719 ==============================================*)
2.76
2.77
2.78 "------ move into detail -----------------------------------------";
2.79 @@ -825,15 +835,18 @@
2.80 case get_trace pt [1,4] [4,3,1] of
2.81 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
2.82 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
2.83 +(*========== inhibit exn AK110719 ==============================================
2.84 case get_trace pt [4,2] [5] of
2.85 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
2.86 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
2.87 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
2.88 | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
2.89 +========== inhibit exn AK110719 ==============================================*)
2.90 case get_trace pt [] [4,4,2] of
2.91 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
2.92 [4,3],[4,3,1],[4,3,2]] => ()
2.93 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
2.94 +(*========== inhibit exn AK110719 ==============================================
2.95 case get_trace pt [] [] of
2.96 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
2.97 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
2.98 @@ -841,6 +854,7 @@
2.99 case get_trace pt [4,3] [4,3] of
2.100 [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
2.101 | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
2.102 +========== inhibit exn AK110719 ==============================================*)
2.103
2.104 "--- level 2: get pos' from start b to end p ---------------------";
2.105 "--- level 2: get pos' from start b to end p ---------------------";
2.106 @@ -964,6 +978,7 @@
2.107 []) => ()
2.108 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
2.109
2.110 +(*========== inhibit exn AK110719 ==============================================
2.111 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
2.112 case (term2str form, tac, terms2strs asm) of
2.113 ("[x = 1]", Check_elementwise "Assumptions", []) => ()
2.114 @@ -980,6 +995,7 @@
2.115 case (term2str form, tac, terms2strs asm) of
2.116 ("[x = 1]", NONE, []) => ()
2.117 | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
2.118 +========== inhibit exn AK110719 ==============================================*)
2.119
2.120 "=====new ptree 6 minisubpbl intersteps ==========================";
2.121 "=====new ptree 6 minisubpbl intersteps ==========================";
2.122 @@ -1152,9 +1168,12 @@
2.123 "-------------- cappend on complete ctree from above -------------";
2.124 show_pt pt;
2.125
2.126 +(*========== inhibit exn AK110719 ==============================================
2.127 +
2.128 "---(2) on S(606)..S(608)--------";
2.129 val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
2.130 (Tac "test") (str2term "Inres[1]",[]) Complete;
2.131 +
2.132 print_depth 99;
2.133 cuts;
2.134 print_depth 3;
2.135 @@ -1164,6 +1183,7 @@
2.136 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
2.137 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
2.138 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
2.139 +
2.140 val afterins = get_allp [] ([], ([],Frm)) pt';
2.141 print_depth 99;
2.142 afterins;
2.143 @@ -1242,6 +1262,7 @@
2.144 ([3, 2], Res),
2.145 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
2.146 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
2.147 +
2.148 val afterins = get_allp [] ([], ([],Frm)) pt';
2.149 print_depth 99;
2.150 afterins;
2.151 @@ -1335,6 +1356,8 @@
2.152 show_pt pt';
2.153 show_pt pt;
2.154 *)
2.155 +========== inhibit exn AK110719 ==============================================*)
2.156
2.157 -===== inhibit exn ?===========================================================*)
2.158
2.159 +
2.160 +
3.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 19 10:28:36 2011 +0200
3.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 19 13:07:28 2011 +0200
3.3 @@ -7,1420 +7,16 @@
3.4
3.5 ML{* writeln "**** run the test ***************************************" *}
3.6
3.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
3.8 +use"../../../test/Tools/isac/Interpret/ctree.sml"
3.9
3.10 ML{*
3.11
3.12 -hdejdhjmd
3.13 -cdscds
3.14 -sdca
3.15 -
3.16 -
3.17 -
3.18 -
3.19 -(* tests the interface of isac's SML-kernel in accordance to
3.20 - java-tests/isac.bridge.
3.21 -
3.22 -WN050707 ... if true, the test ist marked with a \label referring
3.23 -to the same UC in isac-docu.tex as the JUnit testcase.
3.24 -use"../smltest/FE-interface/interface.sml";
3.25 -use"interface.sml";
3.26 - *)
3.27 -
3.28 -"--------------------------------------------------------";
3.29 -"table of contents --------------------------------------";
3.30 -"--------------------------------------------------------";
3.31 -"within struct ------------------------------------------";
3.32 -"--------------------------------------------------------";
3.33 -"--------- encode ^ -> ^^^ ------------------------------";
3.34 -"--------------------------------------------------------";
3.35 -"exported from struct -----------------------------------";
3.36 -"--------------------------------------------------------";
3.37 -"--------- empty rootpbl --------------------------------";
3.38 -"--------- solve_linear as rootpbl FE -------------------";
3.39 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
3.40 -"--------- miniscript with mini-subpbl ------------------";
3.41 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
3.42 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.43 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
3.44 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.45 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.46 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.47 -"--------- setContext..Thy ------------------------------";
3.48 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.49 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.50 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.51 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.52 -"--------- maximum-example, UC: Modeling an example -----";
3.53 -"--------- solve_linear from pbl-hierarchy --------------";
3.54 -"--------- solve_linear as in an algebra system (CAS)----";
3.55 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.56 -"--------- getTactic, fetchApplicableTactics ------------";
3.57 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.58 -"--------- arbitrary combinations of steps --------------";
3.59 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.60 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.61 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.62 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.63 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.64 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.65 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.66 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.67 -"--------------------------------------------------------";
3.68 -
3.69 -"within struct ---------------------------------------------------";
3.70 -"within struct ---------------------------------------------------";
3.71 -"within struct ---------------------------------------------------";
3.72 -(*==================================================================
3.73 -
3.74 -
3.75 -"--------- encode ^ -> ^^^ ------------------------------";
3.76 -"--------- encode ^ -> ^^^ ------------------------------";
3.77 -"--------- encode ^ -> ^^^ ------------------------------";
3.78 -if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
3.79 -else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
3.80 -
3.81 -if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
3.82 -else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
3.83 -
3.84 -==================================================================*)
3.85 -"exported from struct --------------------------------------------";
3.86 -"exported from struct --------------------------------------------";
3.87 -"exported from struct --------------------------------------------";
3.88 -
3.89 -
3.90 -(*------------ set at startup of the Kernel --------------------------*)
3.91 - states:= []; (*resets all state information in Kernel *)
3.92 -(*----------------------------------------------------------------*)
3.93 -
3.94 -"--------- empty rootpbl --------------------------------";
3.95 -"--------- empty rootpbl --------------------------------";
3.96 -"--------- empty rootpbl --------------------------------";
3.97 - CalcTree [([], ("", [], []))];
3.98 - Iterator 1;
3.99 - moveActiveRoot 1;
3.100 - refFormula 1 (get_pos 1 1);
3.101 -(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
3.102 -
3.103 -
3.104 -"--------- solve_linear as rootpbl FE -------------------";
3.105 -"--------- solve_linear as rootpbl FE -------------------";
3.106 -"--------- solve_linear as rootpbl FE -------------------";
3.107 - states := [];
3.108 - CalcTree (*start of calculation, return No.1*)
3.109 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
3.110 - ("Test",
3.111 - ["linear","univariate","equation","test"],
3.112 - ["Test","solve_linear"]))];
3.113 - Iterator 1; (*create an active Iterator on CalcTree No.1*)
3.114 -
3.115 - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
3.116 - refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
3.117 -
3.118 -
3.119 - fetchProposedTactic 1 (*by using Iterator No.1*);
3.120 - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
3.121 - autoCalculate 1 (Step 1);
3.122 - refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
3.123 - autoCalculate 1 (Step 1);
3.124 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.125 - fetchProposedTactic 1;
3.126 - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
3.127 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
3.128 -
3.129 - fetchProposedTactic 1;
3.130 - setNextTactic 1 (Add_Given "solveFor x");
3.131 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.132 -
3.133 - fetchProposedTactic 1;
3.134 - setNextTactic 1 (Add_Find "solutions L");
3.135 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.136 -
3.137 - fetchProposedTactic 1;
3.138 - setNextTactic 1 (Specify_Theory "Test");
3.139 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.140 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.141 -
3.142 - fetchProposedTactic 1;
3.143 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
3.144 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.145 -(*-------------------------------------------------------------------------*)
3.146 - fetchProposedTactic 1;
3.147 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
3.148 -
3.149 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
3.150 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
3.151 -
3.152 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.153 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
3.154 -
3.155 -(*-------------------------------------------------------------------------*)
3.156 - fetchProposedTactic 1;
3.157 -(*========== inhibit exn 110310 ================================================
3.158 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
3.159 -
3.160 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
3.161 - (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
3.162 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
3.163 - is_complete_mod ptp;
3.164 - is_complete_spec ptp;
3.165 -
3.166 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.167 - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
3.168 - (*term2str (get_obj g_form pt [1]);*)
3.169 -(*-------------------------------------------------------------------------*)
3.170 -
3.171 - fetchProposedTactic 1;
3.172 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
3.173 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.174 -
3.175 - fetchProposedTactic 1;
3.176 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.177 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.178 -
3.179 - fetchProposedTactic 1;
3.180 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
3.181 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.182 -
3.183 - val ((pt,_),_) = get_calc 1;
3.184 - val ip = get_pos 1 1;
3.185 - val (Form f, tac, asms) = pt_extract (pt, ip);
3.186 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
3.187 - if term2str f = "[x = 1]" then () else
3.188 - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
3.189 -============ inhibit exn 110310 ==============================================*)
3.190 -
3.191 -(*========== inhibit exn 110620 ================================================
3.192 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
3.193 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
3.194 -"--------- inspect the CalcTree No.1 with Iterator No.2 -";
3.195 -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
3.196 - moveActiveRoot 1;
3.197 - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
3.198 - moveActiveDown 1;
3.199 - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
3.200 - moveActiveDown 1 ;
3.201 - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
3.202 - (*getAssumption 1 ([1],Res); TODO.WN041217*)
3.203 - moveActiveDown 1 ; refFormula 1 ([2],Res);
3.204 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
3.205 - moveActiveDown 1;
3.206 - moveActiveDown 1;
3.207 - moveActiveDown 1;
3.208 - if get_pos 1 1 = ([2], Res) then () else
3.209 - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
3.210 - moveActiveDown 1; refFormula 1 ([], Res);
3.211 - if get_pos 1 1 = ([], Res) then () else
3.212 - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
3.213 - moveActiveCalcHead 1; refFormula 1 ([],Pbl);
3.214 -============ inhibit exn 110620 ==============================================*)
3.215 -
3.216 -"--------- miniscript with mini-subpbl ------------------";
3.217 -"--------- miniscript with mini-subpbl ------------------";
3.218 -"--------- miniscript with mini-subpbl ------------------";
3.219 -"=== this sequence of fun-calls resembles fun me ===";
3.220 - states:=[]; (*start of calculation, return No.1*)
3.221 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.222 - ("Test", ["sqroot-test","univariate","equation","test"],
3.223 - ["Test","squ-equ-test-subpbl1"]))];
3.224 - Iterator 1;
3.225 -
3.226 - moveActiveRoot 1;
3.227 - refFormula 1 (get_pos 1 1);
3.228 - fetchProposedTactic 1;
3.229 - setNextTactic 1 (Model_Problem);
3.230 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
3.231 -
3.232 - fetchProposedTactic 1;
3.233 - setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
3.234 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.235 -
3.236 - fetchProposedTactic 1;
3.237 - setNextTactic 1 (Add_Given "solveFor x");
3.238 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.239 -
3.240 - fetchProposedTactic 1;
3.241 - setNextTactic 1 (Add_Find "solutions L");
3.242 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.243 -
3.244 - fetchProposedTactic 1;
3.245 - setNextTactic 1 (Specify_Theory "Test");
3.246 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.247 -
3.248 - fetchProposedTactic 1;
3.249 - setNextTactic 1 (Specify_Problem
3.250 - ["sqroot-test","univariate","equation","test"]);
3.251 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.252 -"1-----------------------------------------------------------------";
3.253 -
3.254 - fetchProposedTactic 1;
3.255 - setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
3.256 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.257 -
3.258 - fetchProposedTactic 1;
3.259 - setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
3.260 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.261 -
3.262 - fetchProposedTactic 1;
3.263 - setNextTactic 1 (Rewrite_Set "norm_equation");
3.264 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.265 -
3.266 - fetchProposedTactic 1;
3.267 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.268 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.269 -
3.270 - fetchProposedTactic 1;(*----------------Subproblem--------------------*);
3.271 - setNextTactic 1 (Subproblem ("Test",
3.272 - ["linear","univariate","equation","test"]));
3.273 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.274 -
3.275 - fetchProposedTactic 1;
3.276 - setNextTactic 1 (Model_Problem );
3.277 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.278 -
3.279 - fetchProposedTactic 1;
3.280 - setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
3.281 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.282 -
3.283 - fetchProposedTactic 1;
3.284 - setNextTactic 1 (Add_Given "solveFor x");
3.285 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.286 -
3.287 - fetchProposedTactic 1;
3.288 - setNextTactic 1 (Add_Find "solutions x_i");
3.289 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.290 -
3.291 - fetchProposedTactic 1;
3.292 - setNextTactic 1 (Specify_Theory "Test");
3.293 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.294 -
3.295 - fetchProposedTactic 1;
3.296 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
3.297 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.298 -"2-----------------------------------------------------------------";
3.299 -
3.300 - fetchProposedTactic 1;
3.301 - setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
3.302 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.303 -
3.304 - fetchProposedTactic 1;
3.305 - setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
3.306 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.307 -
3.308 - fetchProposedTactic 1;
3.309 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
3.310 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.311 -
3.312 - fetchProposedTactic 1;
3.313 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.314 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.315 -
3.316 - fetchProposedTactic 1;
3.317 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
3.318 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.319 -
3.320 - fetchProposedTactic 1;
3.321 - setNextTactic 1 (Check_elementwise "Assumptions");
3.322 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.323 -
3.324 - val xml = fetchProposedTactic 1;
3.325 - setNextTactic 1 (Check_Postcond
3.326 - ["sqroot-test","univariate","equation","test"]);
3.327 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.328 -
3.329 - val ((pt,_),_) = get_calc 1;
3.330 - val str = pr_ptree pr_short pt;
3.331 - writeln str;
3.332 - val ip = get_pos 1 1;
3.333 - val (Form f, tac, asms) = pt_extract (pt, ip);
3.334 - (*exception just above means: 'ModSpec' has been returned: error anyway*)
3.335 - if term2str f = "[x = 1]" then () else
3.336 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
3.337 -
3.338 - DEconstrCalcTree 1;
3.339 -
3.340 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
3.341 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
3.342 -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
3.343 - states:=[];
3.344 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.345 - ("Test", ["sqroot-test","univariate","equation","test"],
3.346 - ["Test","squ-equ-test-subpbl1"]))];
3.347 - Iterator 1;
3.348 - moveActiveRoot 1;
3.349 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.350 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.351 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.352 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.353 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.354 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.355 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.356 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.357 - (*here the solve-phase starts*)
3.358 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.359 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.360 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.361 - (*------------------------------------*)
3.362 -(* print_depth 13; get_calc 1;
3.363 - *)
3.364 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.365 - (*calc-head of subproblem*)
3.366 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.367 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.368 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.369 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.370 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.371 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.372 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.373 - (*solve-phase of the subproblem*)
3.374 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.375 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.376 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.377 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.378 - (*finish subproblem*)
3.379 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.380 - (*finish problem*)
3.381 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.382 -
3.383 - (*this checks the test for correctness..*)
3.384 - val ((pt,_),_) = get_calc 1;
3.385 - val p = get_pos 1 1;
3.386 - val (Form f, tac, asms) = pt_extract (pt, p);
3.387 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.388 - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
3.389 -
3.390 - DEconstrCalcTree 1;
3.391 -
3.392 -
3.393 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.394 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.395 -"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
3.396 - states:=[];
3.397 - CalcTree
3.398 - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
3.399 - ("Test",
3.400 - ["linear","univariate","equation","test"],
3.401 - ["Test","solve_linear"]))];
3.402 - Iterator 1;
3.403 - moveActiveRoot 1;
3.404 -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
3.405 -
3.406 - autoCalculate 1 CompleteCalc;
3.407 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
3.408 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
3.409 -
3.410 - val ((pt,_),_) = get_calc 1;
3.411 - val p = get_pos 1 1;
3.412 - val (Form f, tac, asms) = pt_extract (pt, p);
3.413 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.414 - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
3.415 -
3.416 -
3.417 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
3.418 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
3.419 -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
3.420 - states:=[];
3.421 - CalcTree
3.422 - [(["equality (1+-1*2+x=(0::real)", "solveFor x","solutions L"],
3.423 - ("Test",
3.424 - ["linear","univariate","equation","test"],
3.425 - ["Test","solve_linear"]))];
3.426 - Iterator 1;
3.427 - moveActiveRoot 1;
3.428 -(*========== inhibit exn 110718 ================================================
3.429 - autoCalculate 1 CompleteCalcHead;
3.430 - refFormula 1 (get_pos 1 1);
3.431 - val ((pt,p),_) = get_calc 1;
3.432 -
3.433 - autoCalculate 1 CompleteCalc;
3.434 - val ((pt,p),_) = get_calc 1;
3.435 - if p=([], Res) then () else
3.436 - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
3.437 -============ inhibit exn 110718 ==============================================*)
3.438 -
3.439 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.440 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.441 -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
3.442 - states:=[];
3.443 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.444 - ("Test", ["sqroot-test","univariate","equation","test"],
3.445 - ["Test","squ-equ-test-subpbl1"]))];
3.446 - Iterator 1;
3.447 - moveActiveRoot 1;
3.448 - autoCalculate 1 CompleteCalc;
3.449 - val ((pt,p),_) = get_calc 1; show_pt pt;
3.450 -(*
3.451 -getTactic 1 ([1],Frm);
3.452 -getTactic 1 ([1],Res);
3.453 -initContext 1 Thy_ ([1],Res);
3.454 -*)
3.455 - (*... returns calcChangedEvent with*)
3.456 - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
3.457 - getFormulaeFromTo 1 unc gen 0 (*only result*) false;
3.458 - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
3.459 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.460 -
3.461 - val ((pt,_),_) = get_calc 1;
3.462 - val p = get_pos 1 1;
3.463 - val (Form f, tac, asms) = pt_extract (pt, p);
3.464 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.465 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
3.466 -
3.467 -
3.468 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.469 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.470 -"--------- mini-subpbl AUTO CompleteCalcHead ------------";
3.471 - states:=[];
3.472 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.473 - ("Test", ["sqroot-test","univariate","equation","test"],
3.474 - ["Test","squ-equ-test-subpbl1"]))];
3.475 - Iterator 1;
3.476 - moveActiveRoot 1;
3.477 - autoCalculate 1 CompleteCalcHead;
3.478 -
3.479 -val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
3.480 - cell = NONE, ctxt = ctxt2, meth,
3.481 - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
3.482 - ["Test", "squ-equ-test-subpbl1"]),
3.483 - probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
3.484 - ([], Met)), []) = get_calc 1;
3.485 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
3.486 -else error "--- mini-subpbl AUTO CompleteCalcHead ---";
3.487 -
3.488 -
3.489 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.490 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.491 -"--------- solve_linear as rootpbl AUTO CompleteModel ---";
3.492 - states:=[];
3.493 - CalcTree
3.494 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
3.495 - ("Test",
3.496 - ["linear","univariate","equation","test"],
3.497 - ["Test","solve_linear"]))];
3.498 - Iterator 1;
3.499 - moveActiveRoot 1;
3.500 -(*========== inhibit exn 110718 ================================================
3.501 - autoCalculate 1 CompleteModel;
3.502 - refFormula 1 (get_pos 1 1);
3.503 -
3.504 -setProblem 1 ["linear","univariate","equation","test"];
3.505 -val pos = get_pos 1 1;
3.506 -setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
3.507 - refFormula 1 (get_pos 1 1);
3.508 -
3.509 -setMethod 1 ["Test","solve_linear"];
3.510 -setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
3.511 - refFormula 1 (get_pos 1 1);
3.512 - val ((pt,_),_) = get_calc 1;
3.513 - if get_obj g_spec pt [] = ("e_domID",
3.514 - ["linear", "univariate","equation","test"],
3.515 - ["Test","solve_linear"]) then ()
3.516 - else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
3.517 -
3.518 - autoCalculate 1 CompleteCalcHead;
3.519 - refFormula 1 (get_pos 1 1);
3.520 - autoCalculate 1 CompleteCalc;
3.521 - moveActiveDown 1;
3.522 - moveActiveDown 1;
3.523 - moveActiveDown 1;
3.524 - refFormula 1 (get_pos 1 1);
3.525 - val ((pt,_),_) = get_calc 1;
3.526 - val p = get_pos 1 1;
3.527 - val (Form f, tac, asms) = pt_extract (pt, p);
3.528 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.529 - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
3.530 -============ inhibit exn 110718 ==============================================*)
3.531 -
3.532 -"--------- setContext..Thy ------------------------------";
3.533 -"--------- setContext..Thy ------------------------------";
3.534 -"--------- setContext..Thy ------------------------------";
3.535 -states:=[];
3.536 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.537 - ("Test", ["sqroot-test","univariate","equation","test"],
3.538 - ["Test","squ-equ-test-subpbl1"]))];
3.539 -Iterator 1; moveActiveRoot 1;
3.540 -autoCalculate 1 CompleteCalcHead;
3.541 -autoCalculate 1 (Step 1);
3.542 -val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
3.543 -(*
3.544 -setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
3.545 -autoCalculate 1 (Step 1);
3.546 -val ((pt,p),_) = get_calc 1; show_pt pt;
3.547 -*)
3.548 -"-----^^^^^ and vvvvv do the same -----";
3.549 -setContext 1 p "thy_isac_Test-rls-Test_simplify";
3.550 -val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
3.551 -
3.552 -autoCalculate 1 (Step 1);
3.553 -setContext 1 p "thy_isac_Test-rls-Test_simplify";
3.554 -val ((pt,p),_) = get_calc 1; show_pt pt; (*3 lines, OK*)
3.555 -if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
3.556 -then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1"
3.557 -
3.558 -autoCalculate 1 CompleteCalc;
3.559 -val ((pt,p),_) = get_calc 1; show_pt pt;
3.560 -val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
3.561 -(*========== inhibit exn 110622 ================================================
3.562 - ERROR still 3 lines
3.563 -val (Form f, tac, asms) = pt_extract (pt, p);
3.564 -if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.565 -error "--- setContext..Thy --- autoCalculate CompleteCalc";
3.566 -============ inhibit exn 110622 ==============================================*)
3.567 -
3.568 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.569 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.570 -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
3.571 - states:=[];
3.572 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.573 - ("Test", ["sqroot-test","univariate","equation","test"],
3.574 - ["Test","squ-equ-test-subpbl1"]))];
3.575 - Iterator 1; moveActiveRoot 1;
3.576 - autoCalculate 1 CompleteToSubpbl;
3.577 - refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
3.578 - val ((pt,_),_) = get_calc 1;
3.579 - val str = pr_ptree pr_short pt;
3.580 - writeln str;
3.581 - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
3.582 - then () else
3.583 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
3.584 -
3.585 - autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
3.586 - autoCalculate 1 CompleteToSubpbl;
3.587 - val ((pt,_),_) = get_calc 1;
3.588 - val str = pr_ptree pr_short pt;
3.589 - writeln str;
3.590 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
3.591 - val ((pt,_),_) = get_calc 1;
3.592 - val p = get_pos 1 1;
3.593 -(*========== inhibit exn 110622 ================================================
3.594 - val (Form f, tac, asms) = pt_extract (pt, p);
3.595 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.596 - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
3.597 -============ inhibit exn 110622 ==============================================*)
3.598 -
3.599 -
3.600 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.601 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.602 -"--------- rat-eq + subpbl: no_met, NO solution dropped -";
3.603 -(*========== inhibit exn 110622 ================================================
3.604 - states:=[];
3.605 - CalcTree
3.606 - [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
3.607 - ("RatEq", ["univariate","equation"], ["no_met"]))];
3.608 - Iterator 1;
3.609 - moveActiveRoot 1;
3.610 - fetchProposedTactic 1;
3.611 - setNextTactic 1 (Model_Problem );
3.612 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.613 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.614 - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
3.615 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.616 - setNextTactic 1 (Add_Given "solveFor x");
3.617 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.618 - setNextTactic 1 (Add_Find "solutions L");
3.619 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.620 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.621 - setNextTactic 1 (Specify_Theory "RatEq");
3.622 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.623 - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
3.624 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.625 - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
3.626 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.627 - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
3.628 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.629 - setNextTactic 1 (Rewrite_Set "RatEq_simplify");
3.630 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.631 - setNextTactic 1 (Rewrite_Set "norm_Rational");
3.632 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.633 - setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
3.634 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.635 - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
3.636 - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
3.637 - "univariate","equation"]));
3.638 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.639 - setNextTactic 1 (Model_Problem );
3.640 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.641 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.642 - setNextTactic 1 (Add_Given
3.643 - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
3.644 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.645 - setNextTactic 1 (Add_Given "solveFor x");
3.646 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.647 - setNextTactic 1 (Add_Find "solutions x_i");
3.648 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.649 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.650 - setNextTactic 1 (Specify_Theory "PolyEq");
3.651 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.652 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
3.653 - "univariate","equation"]);
3.654 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.655 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
3.656 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.657 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
3.658 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.659 - setNextTactic 1 (Rewrite ("all_left",""));
3.660 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.661 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
3.662 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.663 - (* __________ for "16 + 12 * x = 0"*)
3.664 - setNextTactic 1 (Subproblem ("PolyEq",
3.665 - ["degree_1","polynomial","univariate","equation"]));
3.666 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.667 - setNextTactic 1 (Model_Problem );
3.668 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.669 -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
3.670 - setNextTactic 1 (Add_Given
3.671 - "equality (16 + 12 * x = 0)");
3.672 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.673 - setNextTactic 1 (Add_Given "solveFor x");
3.674 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.675 - setNextTactic 1 (Add_Find "solutions x_i");
3.676 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.677 -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
3.678 - setNextTactic 1 (Specify_Theory "PolyEq");
3.679 - (*------------- some trials in the problem-hierarchy ---------------*)
3.680 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
3.681 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
3.682 - setNextTactic 1 (Refine_Problem ["univariate","equation"]);
3.683 -
3.684 - (*------------------------------------------------------------------*)
3.685 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.686 - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
3.687 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.688 - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
3.689 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.690 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
3.691 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.692 - setNextTactic 1 (Rewrite_Set "polyeq_simplify");
3.693 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.694 - (*==================================================================*)
3.695 - setNextTactic 1 Or_to_List;
3.696 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.697 - setNextTactic 1 (Check_elementwise "Assumptions");
3.698 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.699 - setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
3.700 - "univariate","equation"]);
3.701 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.702 - setNextTactic 1 (Check_Postcond ["normalize","polynomial",
3.703 - "univariate","equation"]);
3.704 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.705 -(*========== inhibit exn 2009 ==================================================
3.706 -*** exception TYPE raised (line 460 of "old_goals.ML"):
3.707 -*** Type error in application: Incompatible operand type
3.708 -***
3.709 -*** Operator: equality :: bool => una
3.710 -*** Operand: [((x * 3) = -4)] :: bool list
3.711 -***
3.712 -*** bool => una
3.713 -*** bool list
3.714 -*** equality
3.715 -*** [x * 3 = -4]
3.716 -
3.717 - setNextTactic 1 (Check_elementwise "Assumptions");
3.718 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
3.719 - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
3.720 - val (ptp,_) = get_calc 1;
3.721 - val (Form t,_,_) = pt_extract ptp;
3.722 - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
3.723 - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
3.724 -============ inhibit exn 2009 ================================================*)
3.725 -============ inhibit exn 110622 ==============================================*)
3.726 -
3.727 -
3.728 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.729 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.730 -"--------- tryMatchProblem, tryRefineProblem ------------";
3.731 -(*{\bf\UC{Having \isac{} Refine the Problem
3.732 - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
3.733 - * x^^^2 + 4*x + 5 = 2
3.734 -see isac.bridge.TestSpecify#testMatchRefine*)
3.735 - DEconstrCalcTree 1;
3.736 - CalcTree
3.737 - [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],
3.738 - ("Isac",
3.739 - ["univariate","equation"],
3.740 - ["no_met"]))];
3.741 - Iterator 1;
3.742 - moveActiveRoot 1;
3.743 -
3.744 - fetchProposedTactic 1;
3.745 - setNextTactic 1 (Model_Problem );
3.746 - (*..this tactic should be done 'tacitly', too !*)
3.747 -
3.748 -(*
3.749 -autoCalculate 1 CompleteCalcHead;
3.750 -checkContext 1 ([],Pbl) "pbl_equ_univ";
3.751 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.752 -*)
3.753 -
3.754 - autoCalculate 1 (Step 1);
3.755 -
3.756 - fetchProposedTactic 1;
3.757 - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");
3.758 - autoCalculate 1 (Step 1);
3.759 -
3.760 - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
3.761 -initContext 1 Pbl_ ([],Pbl);
3.762 -initContext 1 Met_ ([],Pbl);
3.763 -
3.764 - "--------- this match will show some incomplete items: ---------";
3.765 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.766 -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
3.767 -
3.768 -
3.769 - fetchProposedTactic 1;
3.770 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
3.771 -
3.772 - fetchProposedTactic 1;
3.773 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
3.774 -
3.775 - "--------- this is a matching model (all items correct): -------";
3.776 -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
3.777 - "--------- this is a NOT matching model (some 'false': ---------";
3.778 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
3.779 -
3.780 - "--------- find out a matching problem: ------------------------";
3.781 - "--------- find out a matching problem (FAILING: no new pbl) ---";
3.782 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
3.783 -
3.784 - "--------- find out a matching problem (SUCCESSFUL) ------------";
3.785 - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
3.786 -
3.787 - "--------- tryMatch, tryRefine did not change the calculation -";
3.788 - "--------- this is done by <TRANSFER> on the pbl-browser: ------";
3.789 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
3.790 - "univariate","equation"]);
3.791 - autoCalculate 1 (Step 1);
3.792 -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
3.793 - and Specify_Theory skipped in comparison to below ---^^^-inserted *)
3.794 -(*------------vvv-inserted-----------------------------------------------*)
3.795 - fetchProposedTactic 1;
3.796 - setNextTactic 1 (Specify_Problem ["normalize","polynomial",
3.797 - "univariate","equation"]);
3.798 - autoCalculate 1 (Step 1);
3.799 -
3.800 -(*and Specify_Theory skipped by fetchProposedTactic ?!?*)
3.801 -
3.802 - fetchProposedTactic 1;
3.803 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
3.804 - autoCalculate 1 (Step 1);
3.805 -
3.806 - fetchProposedTactic 1;
3.807 - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
3.808 -(*========== inhibit exn 110622 ================================================
3.809 - vvvvvvvvvvvv
3.810 - autoCalculate 1 CompleteCalc;
3.811 - val ((pt,_),_) = get_calc 1;
3.812 - show_pt pt;
3.813 - val p = get_pos 1 1;
3.814 - val (Form f, tac, asms) = pt_extract (pt, p);
3.815 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
3.816 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
3.817 -
3.818 -(*------------^^^-inserted-----------------------------------------------*)
3.819 -(*WN050904 the fetchProposedTactic's below may not have worked like that
3.820 - before, too, because there was no check*)
3.821 - fetchProposedTactic 1;
3.822 - setNextTactic 1 (Specify_Theory "PolyEq");
3.823 - autoCalculate 1 (Step 1);
3.824 -
3.825 - fetchProposedTactic 1;
3.826 - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
3.827 - autoCalculate 1 (Step 1);
3.828 -
3.829 - fetchProposedTactic 1;
3.830 - "--------- now the calc-header is ready for enter 'solving' ----";
3.831 - autoCalculate 1 CompleteCalc;
3.832 -
3.833 - val ((pt,_),_) = get_calc 1;
3.834 -rootthy pt;
3.835 - show_pt pt;
3.836 - val p = get_pos 1 1;
3.837 - val (Form f, tac, asms) = pt_extract (pt, p);
3.838 - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
3.839 - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
3.840 -============ inhibit exn 110622 ==============================================*)
3.841 -
3.842 -
3.843 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.844 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.845 -"--------- modifyCalcHead, resetCalcHead, modelProblem --";
3.846 - states:=[];
3.847 - DEconstrCalcTree 1;
3.848 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.849 - ("Test", ["sqroot-test","univariate","equation","test"],
3.850 - ["Test","squ-equ-test-subpbl1"]))];
3.851 - Iterator 1;
3.852 - moveActiveRoot 1;
3.853 -
3.854 - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
3.855 - "solve (x+1=2, x)",(*the headline*)
3.856 - [Given ["equality (x+1=2)", "solveFor x"],
3.857 - Find ["solutions L"](*,Relate []*)],
3.858 - Pbl,
3.859 - ("Test",
3.860 - ["sqroot-test","univariate","equation","test"],
3.861 - ["Test","squ-equ-test-subpbl1"]));
3.862 -
3.863 -val ((Nd (PblObj {env = NONE,
3.864 - fmz = (fm, tpm),
3.865 - loc = (SOME scrst_ctxt, NONE),
3.866 - ctxt,
3.867 - cell = NONE,
3.868 - meth,
3.869 - spec = (thy,
3.870 - ["sqroot-test", "univariate", "equation", "test"],
3.871 - ["Test", "squ-equ-test-subpbl1"]),
3.872 - probl,
3.873 - branch = TransitiveB,
3.874 - origin,
3.875 - ostate = Incomplete,
3.876 - result},
3.877 - []),
3.878 - ([], Pbl)),
3.879 - []) = get_calc 1;
3.880 -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
3.881 -if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
3.882 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
3.883 -
3.884 -resetCalcHead 1;
3.885 -modelProblem 1;
3.886 -
3.887 -get_calc 1;
3.888 -val ((Nd (PblObj {env = NONE,
3.889 - fmz = (fm, tpm),
3.890 - loc = (SOME scrst_ctxt, NONE),
3.891 - ctxt,
3.892 - cell = NONE,
3.893 - meth,
3.894 - spec = ("e_domID", ["e_pblID"], ["e_metID"]),
3.895 - probl,
3.896 - branch = TransitiveB,
3.897 - origin,
3.898 - ostate = Incomplete,
3.899 - result},
3.900 - []),
3.901 - ([], Pbl)),
3.902 - []) = get_calc 1;
3.903 -if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
3.904 -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
3.905 -
3.906 -"--------- maximum-example, UC: Modeling an example -----";
3.907 -"--------- maximum-example, UC: Modeling an example -----";
3.908 -"--------- maximum-example, UC: Modeling an example -----";
3.909 -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
3.910 -see isac.bridge.TestModel#testEditItems
3.911 -*)
3.912 - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
3.913 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
3.914 - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
3.915 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
3.916 - (*^^^ these are the elements for the root-problem (in variants)*)
3.917 - (*vvv these are elements required for subproblems*)
3.918 - "boundVariable a","boundVariable b","boundVariable alpha",
3.919 - "interval {x::real. 0 <= x & x <= 2*r}",
3.920 - "interval {x::real. 0 <= x & x <= 2*r}",
3.921 - "interval {x::real. 0 <= x & x <= pi}",
3.922 - "errorBound (eps=(0::real))"]
3.923 - (*specifying is not interesting for this example*)
3.924 - val spec = ("DiffApp", ["maximum_of","function"],
3.925 - ["DiffApp","max_by_calculus"]);
3.926 - (*the empty model with descriptions for user-guidance by Model_Problem*)
3.927 - val empty_model = [Given ["fixedValues []"],
3.928 - Find ["maximum", "valuesFor"],
3.929 - Relate ["relations []"]];
3.930 - states:=[];
3.931 - DEconstrCalcTree 1;
3.932 - CalcTree [(elems, spec)];
3.933 - Iterator 1;
3.934 - moveActiveRoot 1;
3.935 - refFormula 1 (get_pos 1 1);
3.936 - (*this gives a completely empty model*)
3.937 -
3.938 - fetchProposedTactic 1;
3.939 -(*fill the CalcHead with Descriptions...*)
3.940 - setNextTactic 1 (Model_Problem );
3.941 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.942 -
3.943 - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
3.944 - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
3.945 - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
3.946 - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
3.947 - "Problem (DiffApp.thy, [maximum_of, function])",
3.948 - (*the head-form ^^^ is not used for input here*)
3.949 - [Given ["fixedValues [r=Arbfix]"(*new input*)],
3.950 - Find ["maximum b"(*new input*), "valuesFor"],
3.951 - Relate ["relations"]],
3.952 - (*input (Arbfix will dissappear soon)*)
3.953 - Pbl (*belongsto*),
3.954 - e_spec (*no input to the specification*));
3.955 -
3.956 - (*the user does not know, what 'superfluous' for 'maximum b' may mean
3.957 - and asks what to do next*)
3.958 - fetchProposedTactic 1;
3.959 - (*the student follows the advice*)
3.960 - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
3.961 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
3.962 -
3.963 - (*this input completes the model*)
3.964 - modifyCalcHead 1 (([],Pbl), "not used here",
3.965 - [Given ["fixedValues [r=Arbfix]"],
3.966 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.967 - Relate ["relations [A=a*b, \
3.968 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
3.969 -
3.970 - (*specification is not interesting an should be skipped by the dialogguide;
3.971 - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
3.972 - modifyCalcHead 1 (([],Pbl), "not used here",
3.973 - [Given ["fixedValues [r=Arbfix]"],
3.974 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.975 - Relate ["relations [A=a*b, \
3.976 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
3.977 - ("DiffApp", ["e_pblID"], ["e_metID"]));
3.978 - modifyCalcHead 1 (([],Pbl), "not used here",
3.979 - [Given ["fixedValues [r=Arbfix]"],
3.980 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.981 - Relate ["relations [A=a*b, \
3.982 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
3.983 - ("DiffApp", ["maximum_of","function"],
3.984 - ["e_metID"]));
3.985 - modifyCalcHead 1 (([],Pbl), "not used here",
3.986 - [Given ["fixedValues [r=Arbfix]"],
3.987 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
3.988 - Relate ["relations [A=a*b, \
3.989 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
3.990 - ("DiffApp", ["maximum_of","function"],
3.991 - ["DiffApp","max_by_calculus"]));
3.992 - (*this final calcHead now has STATUS 'complete' !*)
3.993 - DEconstrCalcTree 1;
3.994 -
3.995 -"--------- solve_linear from pbl-hierarchy --------------";
3.996 -"--------- solve_linear from pbl-hierarchy --------------";
3.997 -"--------- solve_linear from pbl-hierarchy --------------";
3.998 - states:=[];
3.999 - val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
3.1000 - CalcTree [(fmz, sp)];
3.1001 - Iterator 1; moveActiveRoot 1;
3.1002 - refFormula 1 (get_pos 1 1);
3.1003 - modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",
3.1004 - [Given ["equality (1+-1*2+x=0)", "solveFor x"],
3.1005 - Find ["solutions L"]],
3.1006 - Pbl,
3.1007 - ("Test", ["linear","univariate","equation","test"],
3.1008 - ["Test","solve_linear"]));
3.1009 - autoCalculate 1 CompleteCalc;
3.1010 - refFormula 1 (get_pos 1 1);
3.1011 - val ((pt,_),_) = get_calc 1;
3.1012 - val p = get_pos 1 1;
3.1013 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1014 - if term2str f = "[x = 1]" andalso p = ([], Res)
3.1015 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
3.1016 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
3.1017 -
3.1018 -"--------- solve_linear as in an algebra system (CAS)----";
3.1019 -"--------- solve_linear as in an algebra system (CAS)----";
3.1020 -"--------- solve_linear as in an algebra system (CAS)----";
3.1021 - states:=[];
3.1022 - val (fmz, sp) = ([], ("", [], []));
3.1023 - CalcTree [(fmz, sp)];
3.1024 - Iterator 1; moveActiveRoot 1;
3.1025 - modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
3.1026 - autoCalculate 1 CompleteCalc;
3.1027 - refFormula 1 (get_pos 1 1);
3.1028 - val ((pt,_),_) = get_calc 1;
3.1029 - val p = get_pos 1 1;
3.1030 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1031 - if term2str f = "[x = 1]" andalso p = ([], Res)
3.1032 - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
3.1033 - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
3.1034 -
3.1035 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.1036 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.1037 -"--------- interSteps: on 'miniscript with mini-subpbl' -";
3.1038 - states:=[];
3.1039 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1040 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1041 - ["Test","squ-equ-test-subpbl1"]))];
3.1042 - Iterator 1;
3.1043 - moveActiveRoot 1;
3.1044 - autoCalculate 1 CompleteCalc;
3.1045 - val ((pt,_),_) = get_calc 1;
3.1046 - show_pt pt;
3.1047 -
3.1048 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
3.1049 - interSteps 1 ([2],Res);
3.1050 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
3.1051 - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
3.1052 - getFormulaeFromTo 1 unc gen 1 false;
3.1053 -
3.1054 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
3.1055 - interSteps 1 ([3,2],Res);
3.1056 - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
3.1057 - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
3.1058 - getFormulaeFromTo 1 unc gen 1 false;
3.1059 -
3.1060 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
3.1061 - interSteps 1 ([3],Res) (*no new steps in subproblems*);
3.1062 - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
3.1063 - getFormulaeFromTo 1 unc gen 1 false;
3.1064 -
3.1065 - (*UC\label{SOLVE:INFO:intermediate-steps}*)
3.1066 - interSteps 1 ([],Res) (*no new steps in subproblems*);
3.1067 - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
3.1068 - getFormulaeFromTo 1 unc gen 1 false;
3.1069 -
3.1070 -
3.1071 -"--------- getTactic, fetchApplicableTactics ------------";
3.1072 -"--------- getTactic, fetchApplicableTactics ------------";
3.1073 -"--------- getTactic, fetchApplicableTactics ------------";
3.1074 - states:=[];
3.1075 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1076 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1077 - ["Test","squ-equ-test-subpbl1"]))];
3.1078 - Iterator 1; moveActiveRoot 1;
3.1079 - autoCalculate 1 CompleteCalc;
3.1080 - val ((pt,_),_) = get_calc 1;
3.1081 - show_pt pt;
3.1082 -
3.1083 - (*UC\label{SOLVE:HIDE:getTactic}*)
3.1084 - getTactic 1 ([],Pbl);
3.1085 - getTactic 1 ([1],Res);
3.1086 - getTactic 1 ([3],Pbl);
3.1087 - getTactic 1 ([3,1],Frm);
3.1088 - getTactic 1 ([3],Res);
3.1089 - getTactic 1 ([],Res);
3.1090 -
3.1091 -(*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
3.1092 - fetchApplicableTactics 1 99999 ([],Pbl);
3.1093 - fetchApplicableTactics 1 99999 ([1],Res);
3.1094 - fetchApplicableTactics 1 99999 ([3],Pbl);
3.1095 - fetchApplicableTactics 1 99999 ([3,1],Res);
3.1096 - fetchApplicableTactics 1 99999 ([3],Res);
3.1097 - fetchApplicableTactics 1 99999 ([],Res);
3.1098 -
3.1099 -
3.1100 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.1101 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.1102 -"--------- getAssumptions, getAccumulatedAsms -----------";
3.1103 -states:=[];
3.1104 -CalcTree
3.1105 -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
3.1106 - "solveFor x","solutions L"],
3.1107 - ("RatEq",["univariate","equation"],["no_met"]))];
3.1108 -Iterator 1; moveActiveRoot 1;
3.1109 -autoCalculate 1 CompleteCalc;
3.1110 -val ((pt,_),_) = get_calc 1;
3.1111 -val p = get_pos 1 1;
3.1112 -val (Form f, tac, asms) = pt_extract (pt, p);
3.1113 -if map term2str asms =
3.1114 - ["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",
3.1115 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
3.1116 - "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
3.1117 - "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
3.1118 -andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
3.1119 -else error "TODO compare 2002--2011";
3.1120 -
3.1121 -(*UC\label{SOLVE:HELP:assumptions}*)
3.1122 -getAssumptions 1 ([3], Res);
3.1123 -getAssumptions 1 ([5], Res);
3.1124 -(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
3.1125 -getAccumulatedAsms 1 ([3], Res);
3.1126 -getAccumulatedAsms 1 ([5], Res);
3.1127 -
3.1128 -
3.1129 -"--------- arbitrary combinations of steps --------------";
3.1130 -"--------- arbitrary combinations of steps --------------";
3.1131 -"--------- arbitrary combinations of steps --------------";
3.1132 - states:=[];
3.1133 - CalcTree (*start of calculation, return No.1*)
3.1134 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
3.1135 - ("Test",
3.1136 - ["linear","univariate","equation","test"],
3.1137 - ["Test","solve_linear"]))];
3.1138 - Iterator 1; moveActiveRoot 1;
3.1139 -
3.1140 - fetchProposedTactic 1;
3.1141 -(*========== inhibit exn 110628 ================================================
3.1142 - ERROR get_calc 1 not existent
3.1143 - setNextTactic 1 (Model_Problem );
3.1144 - autoCalculate 1 (Step 1);
3.1145 -
3.1146 - fetchProposedTactic 1;
3.1147 - fetchProposedTactic 1;
3.1148 -
3.1149 - setNextTactic 1 (Add_Find "solutions L");
3.1150 - setNextTactic 1 (Add_Find "solutions L");
3.1151 -
3.1152 - autoCalculate 1 (Step 1);
3.1153 - autoCalculate 1 (Step 1);
3.1154 -
3.1155 - setNextTactic 1 (Specify_Theory "Test");
3.1156 - fetchProposedTactic 1;
3.1157 - autoCalculate 1 (Step 1);
3.1158 -
3.1159 - autoCalculate 1 (Step 1);
3.1160 - autoCalculate 1 (Step 1);
3.1161 - autoCalculate 1 (Step 1);
3.1162 - autoCalculate 1 (Step 1);
3.1163 -(*------------------------- end calc-head*)
3.1164 -
3.1165 - fetchProposedTactic 1;
3.1166 - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
3.1167 - autoCalculate 1 (Step 1);
3.1168 -
3.1169 - setNextTactic 1 (Rewrite_Set "Test_simplify");
3.1170 - fetchProposedTactic 1;
3.1171 - autoCalculate 1 (Step 1);
3.1172 -
3.1173 - autoCalculate 1 CompleteCalc;
3.1174 - val ((pt,_),_) = get_calc 1;
3.1175 - val p = get_pos 1 1;
3.1176 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1177 - if term2str f = "[x = 1]" andalso p = ([], Res) then () else
3.1178 - error "FE-interface.sml: diff.behav. in combinations of steps";
3.1179 -============ inhibit exn 11062 ==============================================*)
3.1180 -
3.1181 -
3.1182 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.1183 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.1184 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
3.1185 - states:=[];
3.1186 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1187 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1188 - ["Test","squ-equ-test-subpbl1"]))];
3.1189 - Iterator 1;
3.1190 - moveActiveRoot 1;
3.1191 - autoCalculate 1 CompleteCalcHead;
3.1192 - autoCalculate 1 (Step 1);
3.1193 - autoCalculate 1 (Step 1);
3.1194 - appendFormula 1 "-1 + x = 0";
3.1195 - (*... returns calcChangedEvent with*)
3.1196 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
3.1197 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1198 -
3.1199 - val ((pt,_),_) = get_calc 1;
3.1200 - val p = get_pos 1 1;
3.1201 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1202 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
3.1203 - error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
3.1204 -
3.1205 -
3.1206 -
3.1207 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.1208 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.1209 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
3.1210 - states:=[];
3.1211 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1212 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1213 - ["Test","squ-equ-test-subpbl1"]))];
3.1214 - Iterator 1;
3.1215 - moveActiveRoot 1;
3.1216 - autoCalculate 1 CompleteCalcHead;
3.1217 - autoCalculate 1 (Step 1);
3.1218 - autoCalculate 1 (Step 1);
3.1219 - appendFormula 1 "x - 1 = 0";
3.1220 - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
3.1221 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1222 - (*11 elements !!!*)
3.1223 -
3.1224 - val ((pt,_),_) = get_calc 1;
3.1225 - val p = get_pos 1 1;
3.1226 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1227 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
3.1228 - error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
3.1229 -
3.1230 -
3.1231 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.1232 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.1233 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
3.1234 - states:=[];
3.1235 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1236 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1237 - ["Test","squ-equ-test-subpbl1"]))];
3.1238 - Iterator 1;
3.1239 - moveActiveRoot 1;
3.1240 - autoCalculate 1 CompleteCalcHead;
3.1241 - autoCalculate 1 (Step 1);
3.1242 - autoCalculate 1 (Step 1);
3.1243 - appendFormula 1 "x = 1";
3.1244 - (*... returns calcChangedEvent with*)
3.1245 - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
3.1246 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1247 - (*6 elements !!!*)
3.1248 -
3.1249 - val ((pt,_),_) = get_calc 1;
3.1250 - val p = get_pos 1 1;
3.1251 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1252 -(*========== inhibit exn 110628 ================================================*)
3.1253 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
3.1254 - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
3.1255 -(*============ inhibit exn 110682 ==============================================*)
3.1256 -
3.1257 -
3.1258 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.1259 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.1260 -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
3.1261 - states:=[];
3.1262 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1263 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1264 - ["Test","squ-equ-test-subpbl1"]))];
3.1265 - Iterator 1;
3.1266 - moveActiveRoot 1;
3.1267 - autoCalculate 1 CompleteCalcHead;
3.1268 - autoCalculate 1 (Step 1);
3.1269 - autoCalculate 1 (Step 1);
3.1270 - appendFormula 1 "x - 4711 = 0";
3.1271 - (*... returns <ERROR> no derivation found </ERROR>*)
3.1272 -
3.1273 - val ((pt,_),_) = get_calc 1;
3.1274 - val p = get_pos 1 1;
3.1275 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1276 - if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
3.1277 - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
3.1278 -
3.1279 -
3.1280 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.1281 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.1282 -"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
3.1283 - states:=[];
3.1284 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1285 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1286 - ["Test","squ-equ-test-subpbl1"]))];
3.1287 - Iterator 1;
3.1288 - moveActiveRoot 1;
3.1289 - autoCalculate 1 CompleteCalc;
3.1290 - moveActiveFormula 1 ([2],Res);
3.1291 - replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
3.1292 - (*... returns <ERROR> formula not changed </ERROR>*)
3.1293 -
3.1294 - val ((pt,_),_) = get_calc 1;
3.1295 - val p = get_pos 1 1;
3.1296 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1297 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
3.1298 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
3.1299 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
3.1300 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
3.1301 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
3.1302 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
3.1303 -
3.1304 -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
3.1305 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1306 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1307 - ["Test","squ-equ-test-subpbl1"]))];
3.1308 - Iterator 2;
3.1309 - moveActiveRoot 2;
3.1310 - autoCalculate 2 CompleteCalc;
3.1311 - moveActiveFormula 2 ([2],Res);
3.1312 - replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
3.1313 - (*... returns <ERROR> formula not changed </ERROR>*)
3.1314 -
3.1315 - val ((pt,_),_) = get_calc 2;
3.1316 - val p = get_pos 2 1;
3.1317 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1318 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
3.1319 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
3.1320 - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
3.1321 - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
3.1322 - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
3.1323 - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
3.1324 -
3.1325 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.1326 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.1327 -"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
3.1328 - states:=[];
3.1329 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1330 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1331 - ["Test","squ-equ-test-subpbl1"]))];
3.1332 - Iterator 1;
3.1333 - moveActiveRoot 1;
3.1334 - autoCalculate 1 CompleteCalc;
3.1335 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
3.1336 - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
3.1337 - (*... returns calcChangedEvent with*)
3.1338 - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
3.1339 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1340 -
3.1341 - val ((pt,_),_) = get_calc 1;
3.1342 - show_pt pt;
3.1343 - val p = get_pos 1 1;
3.1344 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1345 - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
3.1346 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
3.1347 -(* for getting the list in whole length ...
3.1348 -print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
3.1349 - *)
3.1350 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
3.1351 - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
3.1352 - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
3.1353 - ([2, 8], Res), ([2, 9], Res), ([2], Res)
3.1354 -(*WN060727 {cutlevup->test_trans} removed: ,
3.1355 - ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
3.1356 - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
3.1357 -
3.1358 -
3.1359 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.1360 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.1361 -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
3.1362 - states:=[];
3.1363 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1364 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1365 - ["Test","squ-equ-test-subpbl1"]))];
3.1366 - Iterator 1;
3.1367 - moveActiveRoot 1;
3.1368 - autoCalculate 1 CompleteCalc;
3.1369 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
3.1370 - replaceFormula 1 "x = 1"; (*<-------------------------------------*)
3.1371 - (*... returns calcChangedEvent with ...*)
3.1372 - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
3.1373 - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
3.1374 - (*9 elements !!!*)
3.1375 -
3.1376 - val ((pt,_),_) = get_calc 1;
3.1377 - show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
3.1378 - val (t,_) = get_obj g_result pt [3,2]; term2str t;
3.1379 - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
3.1380 - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
3.1381 - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
3.1382 - ([3,2],Res)] then () else
3.1383 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
3.1384 -
3.1385 - val p = get_pos 1 1;
3.1386 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1387 - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
3.1388 - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
3.1389 -
3.1390 -
3.1391 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.1392 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.1393 -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
3.1394 - states:=[];
3.1395 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
3.1396 - ("Test", ["sqroot-test","univariate","equation","test"],
3.1397 - ["Test","squ-equ-test-subpbl1"]))];
3.1398 - Iterator 1;
3.1399 - moveActiveRoot 1;
3.1400 - autoCalculate 1 CompleteCalc;
3.1401 - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
3.1402 - replaceFormula 1 "x - 4711 = 0";
3.1403 - (*... returns <ERROR> no derivation found </ERROR>*)
3.1404 -
3.1405 - val ((pt,_),_) = get_calc 1;
3.1406 - show_pt pt;
3.1407 - val p = get_pos 1 1;
3.1408 - val (Form f, tac, asms) = pt_extract (pt, p);
3.1409 - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
3.1410 - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
3.1411 -
3.1412 -
3.1413
3.1414 *}
3.1415
3.1416 end
3.1417
3.1418
3.1419 -(*=== inhibit exn ?=============================================================
3.1420 -===== inhibit exn ?===========================================================*)
3.1421 -
3.1422
3.1423 (*========== inhibit exn 110719 ================================================
3.1424 ============ inhibit exn 110719 ==============================================*)