(* Title Run_Tests on isac

$ cd /usr/local/isabisac/test/Tools/isac

$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &

$ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy &

RESTART emacs after having created a new Isac heap.

was sml/RTEST-root.sml in isac-2002

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

theory Test_Isac imports "Knowledge/Isac" begin

ML{* writeln "**** run the tests **************************************" *};

ML {* Toplevel.debug := true; *}

(* 

cd "systest";

(*+ check kbtest/diffapp.sml for additional items in met-model*)

       	use"root-equ.sml"; 

       	use"script.sml";   

	(* use"script_if.sml"; WN03 missing: is_rootequation_in*)

       	use"scriptnew.sml";     

       	use"subp-rooteq.sml";   

	use"tacis.sml";

	use"interface-xml.sml";

	(* use"testdaten.sml"; no update after dropping 'errorBound'*)    

 	cd "../..";

*)

ML{* writeln "**** run systests complete ******************************" *};

(*

cd"smltest/Scripts";

*)

use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)

use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)

ML {*print_depth 5;*}

use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)

(*

	use"listg.sml";

 	use"scrtools.sml";

 	use"tools.sml";

 	cd "../.."; 

cd"smltest/ME";

*)

use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)

(*      use"ctree.sml";

*)

use "../../../test/Tools/isac/Interpret/ptyps.sml";   (*TODO*)

use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)

(*

       	use"calchead.sml"; 

 	use"rewtools.sml";

        use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);

        use"inform.sml";

	use"me.sml";

       	use"ptyps.sml"; 

 	cd "../.."; 

cd"smltest/xmlsrc";

 	use"datatypes.sml";        

       	use"pbl-met-hierarchy.sml"; 

       	use"thy-hierarchy.sml"; 

 	cd "../.."; 

cd"smltest/FE-interface";

       	use"interface.sml";

 	cd "../..";

*)

ML{* writeln "**** run tests on math-engine complete ******************" *};

(*

cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---

        use"atools.sml";

 	use"termorder.sml";

*)

ML {*

val t = str2term "(x^^^2 * x) is_multUnordered";

val pat = parse_patt (theory "Isac") "?p is_multUnordered";

*}

ML {*

val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);

Envir.subst_term subst (*pres?*);

*}

use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)

ML {*

the o (parse thy);

((parse thy)) "9 = 3 ^^^ 2";

(the o (parse thy)) "9 = 3 ^^^ 2";

(term_of o the o (parse thy)) "9 = 3 ^^^ 2";

Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2";

cterm_of (theory "Isac") (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2");

(make_thm o (cterm_of (theory "Isac")))

  (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2");

*}

ML {*

str2term "1 < (2 :: real)";

*}

use"../../../test/Tools/isac/Knowledge/rational.sml"

ML {*111*}

(*

	use"equation.sml";

 	use"root.sml";

	(*use"inssort.sml"; problems with recdef in Isabelle2002*)

 	use"rooteq.sml";

 	use"rateq.sml";

 	use"rootrateq.sml";

 	use"polyeq.sml";  (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN

 			     ? also check others without check 'diff.behav.'*);

 	use"rlang.sml";    (*WN.12.6.03: for TODOs search 'writeln', 

 			     for simplification search MG 

 		 erls:       98a(1) 104a(1) 104a(2) 68a *);

	use"wn.sml";

 	use"trig.sml";

 	use"logexp.sml";

 	use"diff.sml";

*)

use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)

(*

	use"eqsystem.sml";

*)

use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (*part.*)

(*

 	use"vect.sml";  

 	use"diffapp.sml";

	use"biegelinie.sml";

	use"algein.sml";

 	cd "../..";

*)

(* TODO

use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"

*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"

*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"

use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"

*)

use_thy "../../../test/Pure/Isar/Test_Parse_Term"

use_thy "../../../test/Pure/Isar/Test_Parsers"

ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};

(*

val path = "/home/neuper/proto3/testsml2xml/"; 

pbl_hierarchy2file (path ^ "pbl/");

pbls2file          (path ^ "pbl/");

met_hierarchy2file (path ^ "met/");

mets2file          (path ^ "met/");

thy_hierarchy2file (path ^ "thy/");

thes2file          (path ^ "thy/");

cd"sml";

*)

ML{* writeln "**** tested creation of xmldata *************************" *};

ML{*states:=[];

     writeln "=========================================================";

     writeln "**** run systests complete ***************** re-organize!";

     writeln "**** run tests on math-engine complete ******************";

     writeln "**** run tests on IsacKnowledge complete ****************";

     writeln "**** build isac kernel + run tests complete *************";

     writeln "**** tested creation of xmldata *************************";

*}

end