1.1 --- a/src/Tools/isac/Frontend/interface.sml Tue Jul 19 13:12:37 2011 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Tue Jul 19 14:01:27 2011 +0200
1.3 @@ -52,6 +52,9 @@
1.4 val setNextTactic : calcID -> tac -> unit
1.5 val setProblem : calcID -> pblID -> unit
1.6 val setTheory : calcID -> thyID -> unit
1.7 +(*------------ for tests*)
1.8 +val encode: cterm' -> cterm'
1.9 +val encode_fmz: fmz -> fmz
1.10 end
1.11
1.12
2.1 --- a/test/Tools/isac/Frontend/interface.sml Tue Jul 19 13:12:37 2011 +0200
2.2 +++ b/test/Tools/isac/Frontend/interface.sml Tue Jul 19 14:01:27 2011 +0200
2.3 @@ -470,14 +470,13 @@
2.4 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
2.5 states:=[];
2.6 CalcTree
2.7 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
2.8 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.9 ("Test",
2.10 ["linear","univariate","equation","test"],
2.11 ["Test","solve_linear"]))];
2.12 Iterator 1;
2.13 moveActiveRoot 1;
2.14 autoCalculate 1 CompleteModel;
2.15 -(*========== inhibit exn 110718 ================================================
2.16 refFormula 1 (get_pos 1 1);
2.17
2.18 setProblem 1 ["linear","univariate","equation","test"];
2.19 @@ -506,7 +505,7 @@
2.20 val (Form f, tac, asms) = pt_extract (pt, p);
2.21 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
2.22 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
2.23 -============ inhibit exn 110718 ==============================================*)
2.24 +
2.25
2.26 "--------- setContext..Thy ------------------------------";
2.27 "--------- setContext..Thy ------------------------------";
2.28 @@ -983,7 +982,7 @@
2.29 Iterator 1; moveActiveRoot 1;
2.30 refFormula 1 (get_pos 1 1);
2.31 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",
2.32 - [Given ["equality (1+-1*2+x=0)", "solveFor x"],
2.33 + [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
2.34 Find ["solutions L"]],
2.35 Pbl,
2.36 ("Test", ["linear","univariate","equation","test"],
2.37 @@ -1113,7 +1112,7 @@
2.38 "--------- arbitrary combinations of steps --------------";
2.39 states:=[];
2.40 CalcTree (*start of calculation, return No.1*)
2.41 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
2.42 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.43 ("Test",
2.44 ["linear","univariate","equation","test"],
2.45 ["Test","solve_linear"]))];
3.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 13:12:37 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/ctree.sml Tue Jul 19 14:01:27 2011 +0200
3.3 @@ -583,7 +583,7 @@
3.4 "-------------- move_dn: Frm -> Res ------------------------------";
3.5 (*states := [];
3.6 CalcTree (*start of calculation, return No.1*)
3.7 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
3.8 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
3.9 ("Test",
3.10 ["linear","univariate","equation","test"],
3.11 ["Test","solve_linear"]))];
4.1 --- a/test/Tools/isac/Interpret/me.sml Tue Jul 19 13:12:37 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/me.sml Tue Jul 19 14:01:27 2011 +0200
4.3 @@ -337,7 +337,7 @@
4.4 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
4.5 val c = [];
4.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST
4.7 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
4.8 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
4.9 ("Test",
4.10 ["linear","univariate","equation","test"],
4.11 ["Test","solve_linear"]))];
4.12 @@ -373,7 +373,7 @@
4.13 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
4.14 states:=[];
4.15 CalcTree (*start of calculation, return No.1*)
4.16 - [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
4.17 + [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
4.18 ("Test",
4.19 ["linear","univariate","equation","test"],
4.20 ["Test","solve_linear"]))];
5.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Jul 19 13:12:37 2011 +0200
5.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Jul 19 14:01:27 2011 +0200
5.3 @@ -417,7 +417,7 @@
5.4 "----- initContext -----";
5.5 states:=[];
5.6 CalcTree
5.7 - [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
5.8 + [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
5.9 ("Test",
5.10 ["linear","univariate","equation","test"],
5.11 ["Test","solve_linear"]))];
5.12 @@ -441,7 +441,7 @@
5.13 "----- checkContext -----";
5.14 states:=[];
5.15 CalcTree
5.16 - [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
5.17 + [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
5.18 ("Test",
5.19 ["linear","univariate","equation","test"],
5.20 ["Test","solve_linear"]))];
6.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Tue Jul 19 13:12:37 2011 +0200
6.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Tue Jul 19 14:01:27 2011 +0200
6.3 @@ -139,7 +139,7 @@
6.4 "---------------- solve_linear as rootpbl -----------------";
6.5 "---------------- solve_linear as rootpbl -----------------";
6.6 "---------------- solve_linear as rootpbl -----------------";
6.7 -val fmz = ["equality (1+-1*2+x=0)",
6.8 +val fmz = ["equality (1+-1*2+x=(0::real))",
6.9 "solveFor x","solutions L"];
6.10 val (dI',pI',mI') =
6.11 ("Test",["linear","univariate","equation","test"],
7.1 --- a/test/Tools/isac/Test_Some.thy Tue Jul 19 13:12:37 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Tue Jul 19 14:01:27 2011 +0200
7.3 @@ -7,27 +7,19 @@
7.4
7.5 ML{* writeln "**** run the test ***************************************" *}
7.6
7.7 -use"../../../test/Tools/isac/Knowledge/integrate.sml"
7.8 +use"../../../test/Tools/isac/Frontend/interface.sml"
7.9
7.10 ML{*
7.11 -
7.12 -
7.13 *}
7.14 -
7.15 ML{*
7.16
7.17 *}
7.18 ML{*
7.19 -p
7.20 -*}
7.21 -ML{*
7.22
7.23 *}
7.24 end
7.25
7.26
7.27 -
7.28 -
7.29 (*========== inhibit exn 110719 ================================================
7.30 ============ inhibit exn 110719 ==============================================*)
7.31