1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/Minisubpbl/000-comments.sml	Thu May 12 10:00:06 2011 +0200
     1.3 @@ -0,0 +1,19 @@
     1.4 +(* Title:  000-comments.sml
     1.5 +   Author: Walther Neuper 1105
     1.6 +   (c) copyright due to lincense terms.
     1.7 +*)
     1.8 +
     1.9 +(* The tests in this directory use one specific example exclusively.
    1.10 +  The example uses data specifically defined in Test.thy exclusively.
    1.11 +  The example covers the essential features of isac's mathengine.
    1.12 +  Each test is kept in a separate file.
    1.13 +  The order of the files reflects the sequence of work done by the mathengine.
    1.14 +  Testruns showing errors on files indicate roughly the points of failure.
    1.15 +
    1.16 +  The sequence is diveded into the following groups:
    1.17 +  100: initialisation of the rootproblem and specify phase
    1.18 +  200: start and execute the method of the rootproblem
    1.19 +  300: initialisation of a subproblem from script and specify phase
    1.20 +  400: start and execute the method of the subproblem
    1.21 +  500: check postconditions of subproblem and rootproblem
    1.22 +*)

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml	Thu May 12 10:00:06 2011 +0200
     2.3 @@ -0,0 +1,11 @@
     2.4 +(* Title:  100-init-rootpbl.sml
     2.5 +   Author: Walther Neuper 1105
     2.6 +   (c) copyright due to lincense terms.
     2.7 +*)
     2.8 +
     2.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    2.10 +val (dI',pI',mI') =
    2.11 +  ("Test", ["sqroot-test","univariate","equation","test"],
    2.12 +   ["Test","squ-equ-test-subpbl1"]);
    2.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    2.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml	Thu May 12 10:00:06 2011 +0200
     3.3 @@ -0,0 +1,18 @@
     3.4 +(* Title:  200-start-method.sml
     3.5 +   Author: Walther Neuper 1105
     3.6 +   (c) copyright due to lincense terms.
     3.7 +*)
     3.8 +
     3.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    3.10 +val (dI',pI',mI') =
    3.11 +  ("Test", ["sqroot-test","univariate","equation","test"],
    3.12 +   ["Test","squ-equ-test-subpbl1"]);
    3.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    3.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.15 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.16 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml	Thu May 12 10:00:06 2011 +0200
     4.3 @@ -0,0 +1,20 @@
     4.4 +(* Title:  300-init-subpbl.sml
     4.5 +   Author: Walther Neuper 1105
     4.6 +   (c) copyright due to lincense terms.
     4.7 +*)
     4.8 +
     4.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    4.10 +val (dI',pI',mI') =
    4.11 +  ("Test", ["sqroot-test","univariate","equation","test"],
    4.12 +   ["Test","squ-equ-test-subpbl1"]);
    4.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    4.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    4.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.22 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.23 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Thu May 12 10:00:06 2011 +0200
     5.3 @@ -0,0 +1,30 @@
     5.4 +(* Title:  400-start-meth-subpbl.sml
     5.5 +   Author: Walther Neuper 1105
     5.6 +   (c) copyright due to lincense terms.
     5.7 +*)
     5.8 +
     5.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    5.10 +val (dI',pI',mI') =
    5.11 +  ("Test", ["sqroot-test","univariate","equation","test"],
    5.12 +   ["Test","squ-equ-test-subpbl1"]);
    5.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    5.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    5.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.22 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.23 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
    5.24 +(*
    5.25 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    5.33 +*)

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/test/Tools/isac/Minisubpbl/500-postcond.sml	Thu May 12 10:00:06 2011 +0200
     6.3 @@ -0,0 +1,30 @@
     6.4 +(* Title:  500-postcond.sml
     6.5 +   Author: Walther Neuper 1105
     6.6 +   (c) copyright due to lincense terms.
     6.7 +*)
     6.8 +
     6.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    6.10 +val (dI',pI',mI') =
    6.11 +  ("Test", ["sqroot-test","univariate","equation","test"],
    6.12 +   ["Test","squ-equ-test-subpbl1"]);
    6.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    6.14 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    6.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.22 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.23 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem"*)
    6.24 +(*
    6.25 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    6.33 +*)

     7.1 --- a/test/Tools/isac/Test_Isac.thy	Thu May 12 08:26:02 2011 +0200
     7.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu May 12 10:00:06 2011 +0200
     7.3 @@ -21,6 +21,13 @@
     7.4    ("ProgLang/rewrite.sml")
     7.5  (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
     7.6  
     7.7 +  ("Minisubpbl/000-comments.sml")
     7.8 +  ("Minisubpbl/100-init-rootpbl.sml")
     7.9 +  ("Minisubpbl/200-start-method.sml")
    7.10 +  ("Minisubpbl/300-init-subpbl.sml")
    7.11 +  ("Minisubpbl/400-start-meth-subpbl.sml")
    7.12 +  ("Minisubpbl/500-postcond.sml")
    7.13 +
    7.14    ("Interpret/mstools.sml") 
    7.15    ("Interpret/ctree.sml")
    7.16    ("Interpret/ptyps.sml") 
    7.17 @@ -84,6 +91,14 @@
    7.18  (*use "ProgLang/scrtools.sml"         2002*)
    7.19  (*use "ProgLang/tools.sml"            2002*)
    7.20    ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
    7.21 +  use "Minisubpbl/000-comments.sml"
    7.22 +  use "Minisubpbl/100-init-rootpbl.sml"
    7.23 +  use "Minisubpbl/200-start-method.sml"
    7.24 +  use "Minisubpbl/300-init-subpbl.sml"
    7.25 +  use "Minisubpbl/400-start-meth-subpbl.sml"
    7.26 +  use "Minisubpbl/500-postcond.sml"
    7.27 +  ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
    7.28 +  ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
    7.29    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    7.30    use "Interpret/mstools.sml"       (*new 2010*)
    7.31