neuper@38024: (* Title Run_Tests on isac
neuper@38024: $ cd /usr/local/isabisac/test/Tools/isac
neuper@38024: $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
neuper@38024: 
neuper@38024: RESTART emacs after having created a new Isac heap.
neuper@38024: was sml/RTEST-root.sml in isac-2002
neuper@38024: 
neuper@38024: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@38024:         10        20        30        40        50        60        70        80
neuper@38024: *)
neuper@38024: 
neuper@38036: theory Test_Isac imports "Knowledge/Isac" begin
neuper@38024: 
neuper@38024: ML{* writeln "**** run the tests **************************************" *};
neuper@38024: ML {* Toplevel.debug := true; *}
neuper@38024: (* 
neuper@38024: cd "systest";
neuper@38024: (*+ check kbtest/diffapp.sml for additional items in met-model*)
neuper@38024:        	use"root-equ.sml"; 
neuper@38024:        	use"script.sml";   
neuper@38024: 	(* use"script_if.sml"; WN03 missing: is_rootequation_in*)
neuper@38024:        	use"scriptnew.sml";     
neuper@38024:        	use"subp-rooteq.sml";   
neuper@38024: 	use"tacis.sml";
neuper@38024: 	use"interface-xml.sml";
neuper@38024: 	(* use"testdaten.sml"; no update after dropping 'errorBound'*)    
neuper@38024:  	cd "../..";
neuper@38024: *)
neuper@38024: ML{* writeln "**** run systests complete ******************************" *};
neuper@38024: (*
neuper@38024: cd"smltest/Scripts";
neuper@38024: *)
neuper@38025: use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
neuper@38025: use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*)
neuper@38032: 
neuper@38036: ML {*print_depth 999;*}
neuper@38036: use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*)
neuper@38024: (*
neuper@38024: 	use"listg.sml";
neuper@38024:  	use"scrtools.sml";
neuper@38024:  	use"tools.sml";
neuper@38024:  	cd "../.."; 
neuper@38024: cd"smltest/ME";
neuper@38024: *)
neuper@38036: use "../../../test/Tools/isac/Interpret/mstools.sml"; (*empty*)
neuper@38036: (*      use"ctree.sml";
neuper@38036: *)
neuper@38036: use "../../../test/Tools/isac/Interpret/ptyps.sml";   (*TODO*)
neuper@38025: use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
neuper@38024: (*
neuper@38024:        	use"calchead.sml"; 
neuper@38024:  	use"rewtools.sml";
neuper@38024:         use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
neuper@38024:         use"inform.sml";
neuper@38024: 	use"me.sml";
neuper@38024:        	use"ptyps.sml"; 
neuper@38024:  	cd "../.."; 
neuper@38024: cd"smltest/xmlsrc";
neuper@38024:  	use"datatypes.sml";        
neuper@38024:        	use"pbl-met-hierarchy.sml"; 
neuper@38024:        	use"thy-hierarchy.sml"; 
neuper@38024:  	cd "../.."; 
neuper@38024: cd"smltest/FE-interface";
neuper@38024:        	use"interface.sml";
neuper@38024:  	cd "../..";
neuper@38024: *)
neuper@38024: ML{* writeln "**** run tests on math-engine complete ******************" *};
neuper@38024: (*
neuper@38036: cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac---
neuper@38024:         use"atools.sml";
neuper@38036:  	use"termorder.sml";
neuper@38036: *)
neuper@38036: 
neuper@38036: ML {*
neuper@38036: val t = str2term "(x^^^2 * x) is_multUnordered";
neuper@38036: val pat = parse_patt (theory "Isac") "?p is_multUnordered";
neuper@38036: *}
neuper@38036: ML {*
neuper@38036: val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
neuper@38036: Envir.subst_term subst (*pres?*);
neuper@38036: *}
neuper@38036: use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
neuper@38036: (*
neuper@38036:  	use"rational.sml"
neuper@38036: 	use"equation.sml";
neuper@38036:  	use"root.sml";
neuper@38036: 	(*use"inssort.sml"; problems with recdef in Isabelle2002*)
neuper@38036:  	use"rooteq.sml";
neuper@38036:  	use"rateq.sml";
neuper@38036:  	use"rootrateq.sml";
neuper@38036: 
neuper@38036:  	use"polyeq.sml";  (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
neuper@38036:  			     ? also check others without check 'diff.behav.'*);
neuper@38036:  	use"rlang.sml";    (*WN.12.6.03: for TODOs search 'writeln', 
neuper@38036:  			     for simplification search MG 
neuper@38036:  		 erls:       98a(1) 104a(1) 104a(2) 68a *);
neuper@38036: 	use"wn.sml";
neuper@38036:  	use"trig.sml";
neuper@38036:  	use"logexp.sml";
neuper@38024:  	use"diff.sml";
neuper@38030: *)
neuper@38030: use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*)
neuper@38030: (*
neuper@38036: 	use"eqsystem.sml";
neuper@38024:  	use"polyminus.sml";
neuper@38024:  	use"vect.sml";  
neuper@38036:  	use"diffapp.sml";
neuper@38024: 	use"biegelinie.sml";
neuper@38024: 	use"algein.sml";
neuper@38024:  	cd "../..";
neuper@38024: *)
neuper@38024: (* TODO
neuper@38024: use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
neuper@38024: 
neuper@38024: *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
neuper@38024: *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
neuper@38024: 
neuper@38024: use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
neuper@38024: *)
neuper@38025: use_thy "../../../test/Pure/Isar/Test_Parse_Term"
neuper@38025: use_thy "../../../test/Pure/Isar/Test_Parsers"
neuper@38024: 
neuper@38024: ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
neuper@38024: (*
neuper@38025: val path = "/home/neuper/proto3/testsml2xml/"; 
neuper@38024: pbl_hierarchy2file (path ^ "pbl/");
neuper@38024: pbls2file          (path ^ "pbl/");
neuper@38024: met_hierarchy2file (path ^ "met/");
neuper@38024: mets2file          (path ^ "met/");
neuper@38024: thy_hierarchy2file (path ^ "thy/");
neuper@38024: thes2file          (path ^ "thy/");
neuper@38024: cd"sml";
neuper@38024: *)
neuper@38024: ML{* writeln "**** tested creation of xmldata *************************" *};
neuper@38024: 
neuper@38024: ML{*states:=[];
neuper@38024:      writeln "=========================================================";
neuper@38024:      
neuper@38024:      writeln "**** run systests complete ***************** re-organize!";
neuper@38024:      writeln "**** run tests on math-engine complete ******************";
neuper@38024:      writeln "**** run tests on IsacKnowledge complete ****************";
neuper@38024:      writeln "**** build isac kernel + run tests complete *************";
neuper@38024:      writeln "**** tested creation of xmldata *************************";
neuper@38024: *}
neuper@38024: 
neuper@38024: end