# HG changeset patch # User Alexander Kargl # Date 1311073648 -7200 # Node ID 5b996050e25f20d7507ab67e44befad60b854daa # Parent 25ca8a204fd8d05610d9a5d9da9918928ff412c7 intermed: uncommented tests diff -r 25ca8a204fd8 -r 5b996050e25f test/Tools/isac/Frontend/interface.sml --- a/test/Tools/isac/Frontend/interface.sml Tue Jul 19 10:28:36 2011 +0200 +++ b/test/Tools/isac/Frontend/interface.sml Tue Jul 19 13:07:28 2011 +0200 @@ -136,7 +136,6 @@ (*-------------------------------------------------------------------------*) fetchProposedTactic 1; -(*========== inhibit exn 110310 ================================================ val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; setNextTactic 1 (Apply_Method ["Test","solve_linear"]); @@ -168,9 +167,7 @@ (*exception just above means: 'ModSpec' has been returned: error anyway*) if term2str f = "[x = 1]" then () else error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl"; -============ inhibit exn 110310 ==============================================*) -(*========== inhibit exn 110620 ================================================ "--------- inspect the CalcTree No.1 with Iterator No.2 -"; "--------- inspect the CalcTree No.1 with Iterator No.2 -"; "--------- inspect the CalcTree No.1 with Iterator No.2 -"; @@ -193,7 +190,6 @@ if get_pos 1 1 = ([], Res) then () else error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2"; moveActiveCalcHead 1; refFormula 1 ([],Pbl); -============ inhibit exn 110620 ==============================================*) "--------- miniscript with mini-subpbl ------------------"; "--------- miniscript with mini-subpbl ------------------"; @@ -407,8 +403,9 @@ ["Test","solve_linear"]))]; Iterator 1; moveActiveRoot 1; + + autoCalculate 1 CompleteCalcHead; (*========== inhibit exn 110718 ================================================ - autoCalculate 1 CompleteCalcHead; refFormula 1 (get_pos 1 1); val ((pt,p),_) = get_calc 1; @@ -479,8 +476,8 @@ ["Test","solve_linear"]))]; Iterator 1; moveActiveRoot 1; -(*========== inhibit exn 110718 ================================================ - autoCalculate 1 CompleteModel; + autoCalculate 1 CompleteModel; +(*========== inhibit exn 110718 ================================================ refFormula 1 (get_pos 1 1); setProblem 1 ["linear","univariate","equation","test"]; @@ -572,17 +569,15 @@ autoCalculate 1 CompleteCalc; (*das geht ohnehin !*); val ((pt,_),_) = get_calc 1; val p = get_pos 1 1; -(*========== inhibit exn 110622 ================================================ + val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "[x = 1]" andalso p = ([], Res) then () else error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1"; -============ inhibit exn 110622 ==============================================*) "--------- rat-eq + subpbl: no_met, NO solution dropped -"; "--------- rat-eq + subpbl: no_met, NO solution dropped -"; "--------- rat-eq + subpbl: no_met, NO solution dropped -"; -(*========== inhibit exn 110622 ================================================ states:=[]; CalcTree [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"], @@ -590,6 +585,9 @@ Iterator 1; moveActiveRoot 1; fetchProposedTactic 1; + +(*========== inhibit exn 110622 ================================================ +(*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*) setNextTactic 1 (Model_Problem ); autoCalculate 1 (Step 1); fetchProposedTactic 1; (*-----since Model_Problem + complete_mod_ in case cas of SOME-----* @@ -704,7 +702,7 @@ if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then () else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO .."; ============ inhibit exn 2009 ================================================*) -============ inhibit exn 110622 ==============================================*) +============ inhibit exn 110719 ==============================================*) "--------- tryMatchProblem, tryRefineProblem ------------"; @@ -787,15 +785,16 @@ fetchProposedTactic 1; setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); -(*========== inhibit exn 110622 ================================================ - vvvvvvvvvvvv + autoCalculate 1 CompleteCalc; +(*========== inhibit exn 110719 ================================================ val ((pt,_),_) = get_calc 1; show_pt pt; val p = get_pos 1 1; val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; +========== inhibit exn 110719 ================================================*) (*------------^^^-inserted-----------------------------------------------*) (*WN050904 the fetchProposedTactic's below may not have worked like that @@ -812,6 +811,7 @@ "--------- now the calc-header is ready for enter 'solving' ----"; autoCalculate 1 CompleteCalc; +(*============ inhibit exn 110719 ============================================== val ((pt,_),_) = get_calc 1; rootthy pt; show_pt pt; @@ -819,7 +819,7 @@ val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; -============ inhibit exn 110622 ==============================================*) +============ inhibit exn 110719 ==============================================*) "--------- modifyCalcHead, resetCalcHead, modelProblem --"; @@ -1121,7 +1121,7 @@ fetchProposedTactic 1; (*========== inhibit exn 110628 ================================================ - ERROR get_calc 1 not existent + (*ERROR get_calc 1 not existent*) setNextTactic 1 (Model_Problem ); autoCalculate 1 (Step 1); @@ -1231,10 +1231,8 @@ val ((pt,_),_) = get_calc 1; val p = get_pos 1 1; val (Form f, tac, asms) = pt_extract (pt, p); -(*========== inhibit exn 110628 ================================================ if term2str f = "x = 1" andalso p = ([3,2], Res) then () else error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2"; -============ inhibit exn 110682 ==============================================*) "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; @@ -1275,7 +1273,6 @@ val ((pt,_),_) = get_calc 1; val p = get_pos 1 1; -(*========== inhibit exn 110628 ================================================ val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1"; @@ -1283,7 +1280,6 @@ [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2"; - ============ inhibit exn 110682 ==============================================*) (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*) CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], @@ -1298,7 +1294,6 @@ val ((pt,_),_) = get_calc 2; val p = get_pos 2 1; -(*========== inhibit exn 110628 ================================================ val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1"; @@ -1306,9 +1301,7 @@ [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b"; - ============ inhibit exn 110682 ==============================================*) -(*========== inhibit exn 110628 ================================================ "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; @@ -1395,5 +1388,5 @@ val (Form f, tac, asms) = pt_extract (pt, p); if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; -============ inhibit exn 110628 ==============================================*) + diff -r 25ca8a204fd8 -r 5b996050e25f test/Tools/isac/Interpret/ctree.sml --- a/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 10:28:36 2011 +0200 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 13:07:28 2011 +0200 @@ -1,3 +1,6 @@ + + + (* tests for sml/ME/ctree.sml authors: Walther Neuper 060113 (c) due to copyright terms @@ -144,10 +147,8 @@ else error "new behaviour in test: miniscript with mini-subpbl"; show_pt pt; -(*========== inhibit exn WN110319 ============================================== -============ inhibit exn WN110319 ============================================*) -(*=== inhibit exn ?============================================================= + "-------------- get_allpos' (from ptree above)--------------------"; "-------------- get_allpos' (from ptree above)--------------------"; @@ -538,7 +539,10 @@ "=====new ptree 3 ================================================"; "=====new ptree 3 ================================================"; "=====new ptree 3 ================================================"; - states:=[]; + +(*========== inhibit exn AK110719 ============================================== +(* ERROR: get_pos *) +states:=[]; CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], ("Test", ["sqroot-test","univariate","equation","test"], ["Test","squ-equ-test-subpbl1"]))]; @@ -547,6 +551,7 @@ val ((pt,_),_) = get_calc 1; show_pt pt; +============ inhibit exn AK110719 ============================================*) "-------------- move_dn ------------------------------------------"; "-------------- move_dn ------------------------------------------"; @@ -567,13 +572,16 @@ (* val p = (move_dn [] pt p) handle e => print_exn_G e; Exception PTREE end of calculation*) +(*========== inhibit exn AK110719 ============================================== if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn"; +============ inhibit exn AK110719 ============================================*) + "-------------- move_dn: Frm -> Res ------------------------------"; "-------------- move_dn: Frm -> Res ------------------------------"; "-------------- move_dn: Frm -> Res ------------------------------"; - states := []; + (*states := []; CalcTree (*start of calculation, return No.1*) [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], ("Test", @@ -596,7 +604,7 @@ moveActiveDown 1; (* pos does not exist *) if get_pos 1 1 = ([1], Res) then () else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)"; - moveActiveDown 1; (* pos does not exist *) + moveActiveDown 1; (* pos does not exist *)*) "-------------- move_up ------------------------------------------"; @@ -614,7 +622,9 @@ val p = move_up [] pt p; (*-> ([],Pbl)*) (*val p = (move_up [] pt p) handle e => print_exn_G e; Exception PTREE begin of calculation*) +(*========== inhibit exn AK110719 ============================================== if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up"; +========== inhibit exn AK110719 ==============================================*) "------ move into detail -----------------------------------------"; @@ -825,15 +835,18 @@ case get_trace pt [1,4] [4,3,1] of [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => () | _ => error "diff.behav.in ctree.sml: get_interval lev 1c"; +(*========== inhibit exn AK110719 ============================================== case get_trace pt [4,2] [5] of (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_), ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*) [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>() | _ => error "diff.behav.in ctree.sml: get_interval lev 1d"; +========== inhibit exn AK110719 ==============================================*) case get_trace pt [] [4,4,2] of [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2], [4,3],[4,3,1],[4,3,2]] => () | _ => error "diff.behav.in ctree.sml: get_interval lev 1e"; +(*========== inhibit exn AK110719 ============================================== case get_trace pt [] [] of [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2], [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => () @@ -841,6 +854,7 @@ case get_trace pt [4,3] [4,3] of [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => () | _ => error "diff.behav.in ctree.sml: get_interval lev 1g"; +========== inhibit exn AK110719 ==============================================*) "--- level 2: get pos' from start b to end p ---------------------"; "--- level 2: get pos' from start b to end p ---------------------"; @@ -964,6 +978,7 @@ []) => () | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)"; +(*========== inhibit exn AK110719 ============================================== val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res)); case (term2str form, tac, terms2strs asm) of ("[x = 1]", Check_elementwise "Assumptions", []) => () @@ -980,6 +995,7 @@ case (term2str form, tac, terms2strs asm) of ("[x = 1]", NONE, []) => () | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)"; +========== inhibit exn AK110719 ==============================================*) "=====new ptree 6 minisubpbl intersteps =========================="; "=====new ptree 6 minisubpbl intersteps =========================="; @@ -1152,9 +1168,12 @@ "-------------- cappend on complete ctree from above -------------"; show_pt pt; +(*========== inhibit exn AK110719 ============================================== + "---(2) on S(606)..S(608)--------"; val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]") (Tac "test") (str2term "Inres[1]",[]) Complete; + print_depth 99; cuts; print_depth 3; @@ -1164,6 +1183,7 @@ ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then () else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts"; + val afterins = get_allp [] ([], ([],Frm)) pt'; print_depth 99; afterins; @@ -1242,6 +1262,7 @@ ([3, 2], Res), (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts"; + val afterins = get_allp [] ([], ([],Frm)) pt'; print_depth 99; afterins; @@ -1335,6 +1356,8 @@ show_pt pt'; show_pt pt; *) +========== inhibit exn AK110719 ==============================================*) -===== inhibit exn ?===========================================================*) + + diff -r 25ca8a204fd8 -r 5b996050e25f test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Tue Jul 19 10:28:36 2011 +0200 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 19 13:07:28 2011 +0200 @@ -7,1420 +7,16 @@ ML{* writeln "**** run the test ***************************************" *} -use"../../../test/Tools/isac/Frontend/interface.sml" +use"../../../test/Tools/isac/Interpret/ctree.sml" ML{* -hdejdhjmd -cdscds -sdca - - - - -(* tests the interface of isac's SML-kernel in accordance to - java-tests/isac.bridge. - -WN050707 ... if true, the test ist marked with a \label referring -to the same UC in isac-docu.tex as the JUnit testcase. -use"../smltest/FE-interface/interface.sml"; -use"interface.sml"; - *) - -"--------------------------------------------------------"; -"table of contents --------------------------------------"; -"--------------------------------------------------------"; -"within struct ------------------------------------------"; -"--------------------------------------------------------"; -"--------- encode ^ -> ^^^ ------------------------------"; -"--------------------------------------------------------"; -"exported from struct -----------------------------------"; -"--------------------------------------------------------"; -"--------- empty rootpbl --------------------------------"; -"--------- solve_linear as rootpbl FE -------------------"; -"--------- inspect the CalcTree No.1 with Iterator No.2 -"; -"--------- miniscript with mini-subpbl ------------------"; -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; -"--------- solve_linear as rootpbl AUTO CompleteCalc ----"; -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; -"--------- mini-subpbl AUTO CompleteCalcHead ------------"; -"--------- solve_linear as rootpbl AUTO CompleteModel ---"; -"--------- setContext..Thy ------------------------------"; -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; -"--------- rat-eq + subpbl: no_met, NO solution dropped -"; -"--------- tryMatchProblem, tryRefineProblem ------------"; -"--------- modifyCalcHead, resetCalcHead, modelProblem --"; -"--------- maximum-example, UC: Modeling an example -----"; -"--------- solve_linear from pbl-hierarchy --------------"; -"--------- solve_linear as in an algebra system (CAS)----"; -"--------- interSteps: on 'miniscript with mini-subpbl' -"; -"--------- getTactic, fetchApplicableTactics ------------"; -"--------- getAssumptions, getAccumulatedAsms -----------"; -"--------- arbitrary combinations of steps --------------"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; -"--------------------------------------------------------"; - -"within struct ---------------------------------------------------"; -"within struct ---------------------------------------------------"; -"within struct ---------------------------------------------------"; -(*================================================================== - - -"--------- encode ^ -> ^^^ ------------------------------"; -"--------- encode ^ -> ^^^ ------------------------------"; -"--------- encode ^ -> ^^^ ------------------------------"; -if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then () -else error "interface.sml: diff.behav. in encode ^ -> ^^^ "; - -if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then () -else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ "; - -==================================================================*) -"exported from struct --------------------------------------------"; -"exported from struct --------------------------------------------"; -"exported from struct --------------------------------------------"; - - -(*------------ set at startup of the Kernel --------------------------*) - states:= []; (*resets all state information in Kernel *) -(*----------------------------------------------------------------*) - -"--------- empty rootpbl --------------------------------"; -"--------- empty rootpbl --------------------------------"; -"--------- empty rootpbl --------------------------------"; - CalcTree [([], ("", [], []))]; - Iterator 1; - moveActiveRoot 1; - refFormula 1 (get_pos 1 1); -(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*) - - -"--------- solve_linear as rootpbl FE -------------------"; -"--------- solve_linear as rootpbl FE -------------------"; -"--------- solve_linear as rootpbl FE -------------------"; - states := []; - CalcTree (*start of calculation, return No.1*) - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], - ("Test", - ["linear","univariate","equation","test"], - ["Test","solve_linear"]))]; - Iterator 1; (*create an active Iterator on CalcTree No.1*) - - moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*); - refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*); - - - fetchProposedTactic 1 (*by using Iterator No.1*); - setNextTactic 1 (Model_Problem); (*by using Iterator No.1*) - autoCalculate 1 (Step 1); - refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*); - autoCalculate 1 (Step 1); -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----* - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions L"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Theory "Test"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*) - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); -(*-------------------------------------------------------------------------*) - fetchProposedTactic 1; - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - - setNextTactic 1 (Specify_Method ["Test","solve_linear"]); - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - -(*-------------------------------------------------------------------------*) - fetchProposedTactic 1; -(*========== inhibit exn 110310 ================================================ - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - - setNextTactic 1 (Apply_Method ["Test","solve_linear"]); - (*ERROR.110620 .. end-of-calculation*) - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - is_complete_mod ptp; - is_complete_spec ptp; - - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - (*term2str (get_obj g_form pt [1]);*) -(*-------------------------------------------------------------------------*) - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "Test_simplify"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - val ((pt,_),_) = get_calc 1; - val ip = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, ip); - (*exception just above means: 'ModSpec' has been returned: error anyway*) - if term2str f = "[x = 1]" then () else - error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl"; -============ inhibit exn 110310 ==============================================*) - -(*========== inhibit exn 110620 ================================================ -"--------- inspect the CalcTree No.1 with Iterator No.2 -"; -"--------- inspect the CalcTree No.1 with Iterator No.2 -"; -"--------- inspect the CalcTree No.1 with Iterator No.2 -"; -(*WN041118: inspection shifted to Iterator No.1, because others need pos'*) - moveActiveRoot 1; - refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*) - moveActiveDown 1; - refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*) - moveActiveDown 1 ; - refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*) - (*getAssumption 1 ([1],Res); TODO.WN041217*) - moveActiveDown 1 ; refFormula 1 ([2],Res); - moveActiveCalcHead 1; refFormula 1 ([],Pbl); - moveActiveDown 1; - moveActiveDown 1; - moveActiveDown 1; - if get_pos 1 1 = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2"; - moveActiveDown 1; refFormula 1 ([], Res); - if get_pos 1 1 = ([], Res) then () else - error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2"; - moveActiveCalcHead 1; refFormula 1 ([],Pbl); -============ inhibit exn 110620 ==============================================*) - -"--------- miniscript with mini-subpbl ------------------"; -"--------- miniscript with mini-subpbl ------------------"; -"--------- miniscript with mini-subpbl ------------------"; -"=== this sequence of fun-calls resembles fun me ==="; - states:=[]; (*start of calculation, return No.1*) - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - - moveActiveRoot 1; - refFormula 1 (get_pos 1 1); - fetchProposedTactic 1; - setNextTactic 1 (Model_Problem); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*) - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "equality (x + 1 = 2)"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions L"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Theory "Test"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Problem - ["sqroot-test","univariate","equation","test"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); -"1-----------------------------------------------------------------"; - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "norm_equation"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "Test_simplify"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1;(*----------------Subproblem--------------------*); - setNextTactic 1 (Subproblem ("Test", - ["linear","univariate","equation","test"])); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Model_Problem ); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "equality (-1 + x = 0)"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions x_i"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Theory "Test"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); -"2-----------------------------------------------------------------"; - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["Test","solve_linear"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Apply_Method ["Test","solve_linear"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "Test_simplify"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - fetchProposedTactic 1; - setNextTactic 1 (Check_elementwise "Assumptions"); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - val xml = fetchProposedTactic 1; - setNextTactic 1 (Check_Postcond - ["sqroot-test","univariate","equation","test"]); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; - writeln str; - val ip = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, ip); - (*exception just above means: 'ModSpec' has been returned: error anyway*) - if term2str f = "[x = 1]" then () else - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; - - DEconstrCalcTree 1; - -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; -"--------- mini-subpbl AUTOCALCULATE Step 1 -------------"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - (*here the solve-phase starts*) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - (*------------------------------------*) -(* print_depth 13; get_calc 1; - *) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - (*calc-head of subproblem*) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - (*solve-phase of the subproblem*) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - (*finish subproblem*) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - (*finish problem*) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - (*this checks the test for correctness..*) - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in miniscript with mini-subpb"; - - DEconstrCalcTree 1; - - -"--------- solve_linear as rootpbl AUTO CompleteCalc ----"; -"--------- solve_linear as rootpbl AUTO CompleteCalc ----"; -"--------- solve_linear as rootpbl AUTO CompleteCalc ----"; - states:=[]; - CalcTree - [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"], - ("Test", - ["linear","univariate","equation","test"], - ["Test","solve_linear"]))]; - Iterator 1; - moveActiveRoot 1; -getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false; - - autoCalculate 1 CompleteCalc; - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res)); - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE "; - - -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; -"--------- solve_linear as rootpbl AUTO CompleteHead/Calc "; - states:=[]; - CalcTree - [(["equality (1+-1*2+x=(0::real)", "solveFor x","solutions L"], - ("Test", - ["linear","univariate","equation","test"], - ["Test","solve_linear"]))]; - Iterator 1; - moveActiveRoot 1; -(*========== inhibit exn 110718 ================================================ - autoCalculate 1 CompleteCalcHead; - refFormula 1 (get_pos 1 1); - val ((pt,p),_) = get_calc 1; - - autoCalculate 1 CompleteCalc; - val ((pt,p),_) = get_calc 1; - if p=([], Res) then () else - error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc "; -============ inhibit exn 110718 ==============================================*) - -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; -"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - val ((pt,p),_) = get_calc 1; show_pt pt; -(* -getTactic 1 ([1],Frm); -getTactic 1 ([1],Res); -initContext 1 Thy_ ([1],Res); -*) - (*... returns calcChangedEvent with*) - val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res)); - getFormulaeFromTo 1 unc gen 0 (*only result*) false; - getFormulaeFromTo 1 unc gen 1 (*only level 1*) false; - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; - - -"--------- mini-subpbl AUTO CompleteCalcHead ------------"; -"--------- mini-subpbl AUTO CompleteCalcHead ------------"; -"--------- mini-subpbl AUTO CompleteCalcHead ------------"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalcHead; - -val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE), - cell = NONE, ctxt = ctxt2, meth, - spec = ("Test", ["sqroot-test", "univariate", "equation", "test"], - ["Test", "squ-equ-test-subpbl1"]), - probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []), - ([], Met)), []) = get_calc 1; -if length meth = 3 andalso length probl = 3 (*just some items tested*) then () -else error "--- mini-subpbl AUTO CompleteCalcHead ---"; - - -"--------- solve_linear as rootpbl AUTO CompleteModel ---"; -"--------- solve_linear as rootpbl AUTO CompleteModel ---"; -"--------- solve_linear as rootpbl AUTO CompleteModel ---"; - states:=[]; - CalcTree - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], - ("Test", - ["linear","univariate","equation","test"], - ["Test","solve_linear"]))]; - Iterator 1; - moveActiveRoot 1; -(*========== inhibit exn 110718 ================================================ - autoCalculate 1 CompleteModel; - refFormula 1 (get_pos 1 1); - -setProblem 1 ["linear","univariate","equation","test"]; -val pos = get_pos 1 1; -setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]); - refFormula 1 (get_pos 1 1); - -setMethod 1 ["Test","solve_linear"]; -setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]); - refFormula 1 (get_pos 1 1); - val ((pt,_),_) = get_calc 1; - if get_obj g_spec pt [] = ("e_domID", - ["linear", "univariate","equation","test"], - ["Test","solve_linear"]) then () - else error "FE-interface.sml: diff.behav. in setProblem, setMethod"; - - autoCalculate 1 CompleteCalcHead; - refFormula 1 (get_pos 1 1); - autoCalculate 1 CompleteCalc; - moveActiveDown 1; - moveActiveDown 1; - moveActiveDown 1; - refFormula 1 (get_pos 1 1); - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6"; -============ inhibit exn 110718 ==============================================*) - -"--------- setContext..Thy ------------------------------"; -"--------- setContext..Thy ------------------------------"; -"--------- setContext..Thy ------------------------------"; -states:=[]; -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; -Iterator 1; moveActiveRoot 1; -autoCalculate 1 CompleteCalcHead; -autoCalculate 1 (Step 1); -val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*) -(* -setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*) -autoCalculate 1 (Step 1); -val ((pt,p),_) = get_calc 1; show_pt pt; -*) -"-----^^^^^ and vvvvv do the same -----"; -setContext 1 p "thy_isac_Test-rls-Test_simplify"; -val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*) - -autoCalculate 1 (Step 1); -setContext 1 p "thy_isac_Test-rls-Test_simplify"; -val ((pt,p),_) = get_calc 1; show_pt pt; (*3 lines, OK*) -if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0" -then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1" - -autoCalculate 1 CompleteCalc; -val ((pt,p),_) = get_calc 1; show_pt pt; -val (((pt,_),_), p) = (get_calc 1, get_pos 1 1); -(*========== inhibit exn 110622 ================================================ - ERROR still 3 lines -val (Form f, tac, asms) = pt_extract (pt, p); -if term2str f = "[x = 1]" andalso p = ([], Res) then () else -error "--- setContext..Thy --- autoCalculate CompleteCalc"; -============ inhibit exn 110622 ==============================================*) - -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; -"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; moveActiveRoot 1; - autoCalculate 1 CompleteToSubpbl; - refFormula 1 (get_pos 1 1); (* -1 + x = 0 *); - val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; - writeln str; - if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n" - then () else - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1"; - - autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*) - autoCalculate 1 CompleteToSubpbl; - val ((pt,_),_) = get_calc 1; - val str = pr_ptree pr_short pt; - writeln str; - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*); - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; -(*========== inhibit exn 110622 ================================================ - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1"; -============ inhibit exn 110622 ==============================================*) - - -"--------- rat-eq + subpbl: no_met, NO solution dropped -"; -"--------- rat-eq + subpbl: no_met, NO solution dropped -"; -"--------- rat-eq + subpbl: no_met, NO solution dropped -"; -(*========== inhibit exn 110622 ================================================ - states:=[]; - CalcTree - [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"], - ("RatEq", ["univariate","equation"], ["no_met"]))]; - Iterator 1; - moveActiveRoot 1; - fetchProposedTactic 1; - setNextTactic 1 (Model_Problem ); -autoCalculate 1 (Step 1); fetchProposedTactic 1; -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----* - setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions L"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*) - setNextTactic 1 (Specify_Theory "RatEq"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "RatEq_simplify"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "norm_Rational"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "RatEq_eliminate"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*) - setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial", - "univariate","equation"])); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Model_Problem ); - autoCalculate 1 (Step 1); fetchProposedTactic 1; -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----* - setNextTactic 1 (Add_Given - "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions x_i"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*) - setNextTactic 1 (Specify_Theory "PolyEq"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Specify_Problem ["normalize","polynomial", - "univariate","equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite ("all_left","")); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in")); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - (* __________ for "16 + 12 * x = 0"*) - setNextTactic 1 (Subproblem ("PolyEq", - ["degree_1","polynomial","univariate","equation"])); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Model_Problem ); - autoCalculate 1 (Step 1); fetchProposedTactic 1; -(*-----since Model_Problem + complete_mod_ in case cas of SOME-----* - setNextTactic 1 (Add_Given - "equality (16 + 12 * x = 0)"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions x_i"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; -*-----since Model_Problem + complete_mod_ in case cas of SOME-----*) - setNextTactic 1 (Specify_Theory "PolyEq"); - (*------------- some trials in the problem-hierarchy ---------------*) - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; (* helpless !!!*) - setNextTactic 1 (Refine_Problem ["univariate","equation"]); - - (*------------------------------------------------------------------*) - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify")); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set "polyeq_simplify"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - (*==================================================================*) - setNextTactic 1 Or_to_List; - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Check_elementwise "Assumptions"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Check_Postcond ["degree_1","polynomial", - "univariate","equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Check_Postcond ["normalize","polynomial", - "univariate","equation"]); - autoCalculate 1 (Step 1); fetchProposedTactic 1; -(*========== inhibit exn 2009 ================================================== -*** exception TYPE raised (line 460 of "old_goals.ML"): -*** Type error in application: Incompatible operand type -*** -*** Operator: equality :: bool => una -*** Operand: [((x * 3) = -4)] :: bool list -*** -*** bool => una -*** bool list -*** equality -*** [x * 3 = -4] - - setNextTactic 1 (Check_elementwise "Assumptions"); - autoCalculate 1 (Step 1); fetchProposedTactic 1; - setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]); - val (ptp,_) = get_calc 1; - val (Form t,_,_) = pt_extract ptp; - if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then () - else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO .."; -============ inhibit exn 2009 ================================================*) -============ inhibit exn 110622 ==============================================*) - - -"--------- tryMatchProblem, tryRefineProblem ------------"; -"--------- tryMatchProblem, tryRefineProblem ------------"; -"--------- tryMatchProblem, tryRefineProblem ------------"; -(*{\bf\UC{Having \isac{} Refine the Problem - * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with - * x^^^2 + 4*x + 5 = 2 -see isac.bridge.TestSpecify#testMatchRefine*) - DEconstrCalcTree 1; - CalcTree - [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"], - ("Isac", - ["univariate","equation"], - ["no_met"]))]; - Iterator 1; - moveActiveRoot 1; - - fetchProposedTactic 1; - setNextTactic 1 (Model_Problem ); - (*..this tactic should be done 'tacitly', too !*) - -(* -autoCalculate 1 CompleteCalcHead; -checkContext 1 ([],Pbl) "pbl_equ_univ"; -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]); -*) - - autoCalculate 1 (Step 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)"); - autoCalculate 1 (Step 1); - - "--------- we go into the ProblemBrowser (_NO_ pblID selected) -"; -initContext 1 Pbl_ ([],Pbl); -initContext 1 Met_ ([],Pbl); - - "--------- this match will show some incomplete items: ---------"; -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]); -checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]); - - - fetchProposedTactic 1; - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1); - - fetchProposedTactic 1; - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1); - - "--------- this is a matching model (all items correct): -------"; -checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]); - "--------- this is a NOT matching model (some 'false': ---------"; -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]); - - "--------- find out a matching problem: ------------------------"; - "--------- find out a matching problem (FAILING: no new pbl) ---"; - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]); - - "--------- find out a matching problem (SUCCESSFUL) ------------"; - refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]); - - "--------- tryMatch, tryRefine did not change the calculation -"; - "--------- this is done by on the pbl-browser: ------"; - setNextTactic 1 (Specify_Problem ["normalize","polynomial", - "univariate","equation"]); - autoCalculate 1 (Step 1); -(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",... - and Specify_Theory skipped in comparison to below ---^^^-inserted *) -(*------------vvv-inserted-----------------------------------------------*) - fetchProposedTactic 1; - setNextTactic 1 (Specify_Problem ["normalize","polynomial", - "univariate","equation"]); - autoCalculate 1 (Step 1); - -(*and Specify_Theory skipped by fetchProposedTactic ?!?*) - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); - autoCalculate 1 (Step 1); - - fetchProposedTactic 1; - setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]); -(*========== inhibit exn 110622 ================================================ - vvvvvvvvvvvv - autoCalculate 1 CompleteCalc; - val ((pt,_),_) = get_calc 1; - show_pt pt; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; - -(*------------^^^-inserted-----------------------------------------------*) -(*WN050904 the fetchProposedTactic's below may not have worked like that - before, too, because there was no check*) - fetchProposedTactic 1; - setNextTactic 1 (Specify_Theory "PolyEq"); - autoCalculate 1 (Step 1); - - fetchProposedTactic 1; - setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]); - autoCalculate 1 (Step 1); - - fetchProposedTactic 1; - "--------- now the calc-header is ready for enter 'solving' ----"; - autoCalculate 1 CompleteCalc; - - val ((pt,_),_) = get_calc 1; -rootthy pt; - show_pt pt; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine"; -============ inhibit exn 110622 ==============================================*) - - -"--------- modifyCalcHead, resetCalcHead, modelProblem --"; -"--------- modifyCalcHead, resetCalcHead, modelProblem --"; -"--------- modifyCalcHead, resetCalcHead, modelProblem --"; - states:=[]; - DEconstrCalcTree 1; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - - modifyCalcHead 1 (([],Pbl),(*the position from refFormula*) - "solve (x+1=2, x)",(*the headline*) - [Given ["equality (x+1=2)", "solveFor x"], - Find ["solutions L"](*,Relate []*)], - Pbl, - ("Test", - ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"])); - -val ((Nd (PblObj {env = NONE, - fmz = (fm, tpm), - loc = (SOME scrst_ctxt, NONE), - ctxt, - cell = NONE, - meth, - spec = (thy, - ["sqroot-test", "univariate", "equation", "test"], - ["Test", "squ-equ-test-subpbl1"]), - probl, - branch = TransitiveB, - origin, - ostate = Incomplete, - result}, - []), - ([], Pbl)), - []) = get_calc 1; -(*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*) -if length meth = 0 andalso length probl = 0 (*just some items tested*) then () -else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --"; - -resetCalcHead 1; -modelProblem 1; - -get_calc 1; -val ((Nd (PblObj {env = NONE, - fmz = (fm, tpm), - loc = (SOME scrst_ctxt, NONE), - ctxt, - cell = NONE, - meth, - spec = ("e_domID", ["e_pblID"], ["e_metID"]), - probl, - branch = TransitiveB, - origin, - ostate = Incomplete, - result}, - []), - ([], Pbl)), - []) = get_calc 1; -if length meth = 3 andalso length probl = 3 (*just some items tested*) then () -else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --"; - -"--------- maximum-example, UC: Modeling an example -----"; -"--------- maximum-example, UC: Modeling an example -----"; -"--------- maximum-example, UC: Modeling an example -----"; -(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\} -see isac.bridge.TestModel#testEditItems -*) - val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]", - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]", - "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]", - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", - (*^^^ these are the elements for the root-problem (in variants)*) - (*vvv these are elements required for subproblems*) - "boundVariable a","boundVariable b","boundVariable alpha", - "interval {x::real. 0 <= x & x <= 2*r}", - "interval {x::real. 0 <= x & x <= 2*r}", - "interval {x::real. 0 <= x & x <= pi}", - "errorBound (eps=(0::real))"] - (*specifying is not interesting for this example*) - val spec = ("DiffApp", ["maximum_of","function"], - ["DiffApp","max_by_calculus"]); - (*the empty model with descriptions for user-guidance by Model_Problem*) - val empty_model = [Given ["fixedValues []"], - Find ["maximum", "valuesFor"], - Relate ["relations []"]]; - states:=[]; - DEconstrCalcTree 1; - CalcTree [(elems, spec)]; - Iterator 1; - moveActiveRoot 1; - refFormula 1 (get_pos 1 1); - (*this gives a completely empty model*) - - fetchProposedTactic 1; -(*fill the CalcHead with Descriptions...*) - setNextTactic 1 (Model_Problem ); - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model - !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*) - (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*) - modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*), - "Problem (DiffApp.thy, [maximum_of, function])", - (*the head-form ^^^ is not used for input here*) - [Given ["fixedValues [r=Arbfix]"(*new input*)], - Find ["maximum b"(*new input*), "valuesFor"], - Relate ["relations"]], - (*input (Arbfix will dissappear soon)*) - Pbl (*belongsto*), - e_spec (*no input to the specification*)); - - (*the user does not know, what 'superfluous' for 'maximum b' may mean - and asks what to do next*) - fetchProposedTactic 1; - (*the student follows the advice*) - setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*) - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); - - (*this input completes the model*) - modifyCalcHead 1 (([],Pbl), "not used here", - [Given ["fixedValues [r=Arbfix]"], - Find ["maximum A", "valuesFor [a,b]"(*new input*)], - Relate ["relations [A=a*b, \ - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec); - - (*specification is not interesting an should be skipped by the dialogguide; - !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*) - modifyCalcHead 1 (([],Pbl), "not used here", - [Given ["fixedValues [r=Arbfix]"], - Find ["maximum A", "valuesFor [a,b]"(*new input*)], - Relate ["relations [A=a*b, \ - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, - ("DiffApp", ["e_pblID"], ["e_metID"])); - modifyCalcHead 1 (([],Pbl), "not used here", - [Given ["fixedValues [r=Arbfix]"], - Find ["maximum A", "valuesFor [a,b]"(*new input*)], - Relate ["relations [A=a*b, \ - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, - ("DiffApp", ["maximum_of","function"], - ["e_metID"])); - modifyCalcHead 1 (([],Pbl), "not used here", - [Given ["fixedValues [r=Arbfix]"], - Find ["maximum A", "valuesFor [a,b]"(*new input*)], - Relate ["relations [A=a*b, \ - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, - ("DiffApp", ["maximum_of","function"], - ["DiffApp","max_by_calculus"])); - (*this final calcHead now has STATUS 'complete' !*) - DEconstrCalcTree 1; - -"--------- solve_linear from pbl-hierarchy --------------"; -"--------- solve_linear from pbl-hierarchy --------------"; -"--------- solve_linear from pbl-hierarchy --------------"; - states:=[]; - val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], [])); - CalcTree [(fmz, sp)]; - Iterator 1; moveActiveRoot 1; - refFormula 1 (get_pos 1 1); - modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)", - [Given ["equality (1+-1*2+x=0)", "solveFor x"], - Find ["solutions L"]], - Pbl, - ("Test", ["linear","univariate","equation","test"], - ["Test","solve_linear"])); - autoCalculate 1 CompleteCalc; - refFormula 1 (get_pos 1 1); - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy"; - -"--------- solve_linear as in an algebra system (CAS)----"; -"--------- solve_linear as in an algebra system (CAS)----"; -"--------- solve_linear as in an algebra system (CAS)----"; - states:=[]; - val (fmz, sp) = ([], ("", [], [])); - CalcTree [(fmz, sp)]; - Iterator 1; moveActiveRoot 1; - modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])); - autoCalculate 1 CompleteCalc; - refFormula 1 (get_pos 1 1); - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) - andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then () - else error "FE-interface.sml: diff.behav. in from pbl -hierarchy"; - -"--------- interSteps: on 'miniscript with mini-subpbl' -"; -"--------- interSteps: on 'miniscript with mini-subpbl' -"; -"--------- interSteps: on 'miniscript with mini-subpbl' -"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - val ((pt,_),_) = get_calc 1; - show_pt pt; - - (*UC\label{SOLVE:INFO:intermediate-steps}*) - interSteps 1 ([2],Res); - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*); - val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res)); - getFormulaeFromTo 1 unc gen 1 false; - - (*UC\label{SOLVE:INFO:intermediate-steps}*) - interSteps 1 ([3,2],Res); - val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*); - val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res)); - getFormulaeFromTo 1 unc gen 1 false; - - (*UC\label{SOLVE:INFO:intermediate-steps}*) - interSteps 1 ([3],Res) (*no new steps in subproblems*); - val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res)); - getFormulaeFromTo 1 unc gen 1 false; - - (*UC\label{SOLVE:INFO:intermediate-steps}*) - interSteps 1 ([],Res) (*no new steps in subproblems*); - val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res)); - getFormulaeFromTo 1 unc gen 1 false; - - -"--------- getTactic, fetchApplicableTactics ------------"; -"--------- getTactic, fetchApplicableTactics ------------"; -"--------- getTactic, fetchApplicableTactics ------------"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - val ((pt,_),_) = get_calc 1; - show_pt pt; - - (*UC\label{SOLVE:HIDE:getTactic}*) - getTactic 1 ([],Pbl); - getTactic 1 ([1],Res); - getTactic 1 ([3],Pbl); - getTactic 1 ([3,1],Frm); - getTactic 1 ([3],Res); - getTactic 1 ([],Res); - -(*UC\label{SOLVE:MANUAL:TACTIC:listall}*) - fetchApplicableTactics 1 99999 ([],Pbl); - fetchApplicableTactics 1 99999 ([1],Res); - fetchApplicableTactics 1 99999 ([3],Pbl); - fetchApplicableTactics 1 99999 ([3,1],Res); - fetchApplicableTactics 1 99999 ([3],Res); - fetchApplicableTactics 1 99999 ([],Res); - - -"--------- getAssumptions, getAccumulatedAsms -----------"; -"--------- getAssumptions, getAccumulatedAsms -----------"; -"--------- getAssumptions, getAccumulatedAsms -----------"; -states:=[]; -CalcTree -[(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", - "solveFor x","solutions L"], - ("RatEq",["univariate","equation"],["no_met"]))]; -Iterator 1; moveActiveRoot 1; -autoCalculate 1 CompleteCalc; -val ((pt,_),_) = get_calc 1; -val p = get_pos 1 1; -val (Form f, tac, asms) = pt_extract (pt, p); -if map term2str asms = - ["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", - "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", - "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2", - "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"] -andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then () -else error "TODO compare 2002--2011"; - -(*UC\label{SOLVE:HELP:assumptions}*) -getAssumptions 1 ([3], Res); -getAssumptions 1 ([5], Res); -(*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*) -getAccumulatedAsms 1 ([3], Res); -getAccumulatedAsms 1 ([5], Res); - - -"--------- arbitrary combinations of steps --------------"; -"--------- arbitrary combinations of steps --------------"; -"--------- arbitrary combinations of steps --------------"; - states:=[]; - CalcTree (*start of calculation, return No.1*) - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], - ("Test", - ["linear","univariate","equation","test"], - ["Test","solve_linear"]))]; - Iterator 1; moveActiveRoot 1; - - fetchProposedTactic 1; -(*========== inhibit exn 110628 ================================================ - ERROR get_calc 1 not existent - setNextTactic 1 (Model_Problem ); - autoCalculate 1 (Step 1); - - fetchProposedTactic 1; - fetchProposedTactic 1; - - setNextTactic 1 (Add_Find "solutions L"); - setNextTactic 1 (Add_Find "solutions L"); - - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - - setNextTactic 1 (Specify_Theory "Test"); - fetchProposedTactic 1; - autoCalculate 1 (Step 1); - - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); -(*------------------------- end calc-head*) - - fetchProposedTactic 1; - setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); - autoCalculate 1 (Step 1); - - setNextTactic 1 (Rewrite_Set "Test_simplify"); - fetchProposedTactic 1; - autoCalculate 1 (Step 1); - - autoCalculate 1 CompleteCalc; - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "[x = 1]" andalso p = ([], Res) then () else - error "FE-interface.sml: diff.behav. in combinations of steps"; -============ inhibit exn 11062 ==============================================*) - - -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalcHead; - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - appendFormula 1 "-1 + x = 0"; - (*... returns calcChangedEvent with*) - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res)); - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:enter} right"; - - - -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalcHead; - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - appendFormula 1 "x - 1 = 0"; - val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res)); - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; - (*11 elements !!!*) - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:enter} other"; - - -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalcHead; - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - appendFormula 1 "x = 1"; - (*... returns calcChangedEvent with*) - val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res)); - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; - (*6 elements !!!*) - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); -(*========== inhibit exn 110628 ================================================*) - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2"; -(*============ inhibit exn 110682 ==============================================*) - - -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; -"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalcHead; - autoCalculate 1 (Step 1); - autoCalculate 1 (Step 1); - appendFormula 1 "x - 4711 = 0"; - (*... returns no derivation found *) - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok"; - - -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - moveActiveFormula 1 ([2],Res); - replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*); - (*... returns formula not changed *) - - val ((pt,_),_) = get_calc 1; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1"; - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2"; - -(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*) - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 2; - moveActiveRoot 2; - autoCalculate 2 CompleteCalc; - moveActiveFormula 2 ([2],Res); - replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*); - (*... returns formula not changed *) - - val ((pt,_),_) = get_calc 2; - val p = get_pos 2 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1"; - if map fst (get_interval ([2],Res) ([],Res) 9999 pt) = - [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res), - ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else - error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b"; - -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) - replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*) - (*... returns calcChangedEvent with*) - val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res)); - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; - - val ((pt,_),_) = get_calc 1; - show_pt pt; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1"; -(* for getting the list in whole length ... -print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3; - *) - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = - [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), - ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res), - ([2, 8], Res), ([2, 9], Res), ([2], Res) -(*WN060727 {cutlevup->test_trans} removed: , - ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2"; - - -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; -"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) - replaceFormula 1 "x = 1"; (*<-------------------------------------*) - (*... returns calcChangedEvent with ...*) - val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res)); - getFormulaeFromTo 1 unc gen 99999 (*all levels*) false; - (*9 elements !!!*) - - val ((pt,_),_) = get_calc 1; - show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*) - val (t,_) = get_obj g_result pt [3,2]; term2str t; - if map fst (get_interval ([1],Res) ([],Res) 9999 pt) = - [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), - ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), - ([3,2],Res)] then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1"; - - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "x = 1" andalso p = ([3,2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2"; - - -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; -"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; - states:=[]; - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]))]; - Iterator 1; - moveActiveRoot 1; - autoCalculate 1 CompleteCalc; - moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*) - replaceFormula 1 "x - 4711 = 0"; - (*... returns no derivation found *) - - val ((pt,_),_) = get_calc 1; - show_pt pt; - val p = get_pos 1 1; - val (Form f, tac, asms) = pt_extract (pt, p); - if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else - error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok"; - - *} end -(*=== inhibit exn ?============================================================= -===== inhibit exn ?===========================================================*) - (*========== inhibit exn 110719 ================================================ ============ inhibit exn 110719 ==============================================*)