diff -r cd7854f2636d -r 02a9b2540eb7 src/Tools/isac/Test_Isac.thy --- a/src/Tools/isac/Test_Isac.thy Tue Sep 28 13:30:29 2010 +0200 +++ b/src/Tools/isac/Test_Isac.thy Fri Oct 01 10:23:38 2010 +0200 @@ -9,7 +9,7 @@ 10 20 30 40 50 60 70 80 *) -theory Test_Isac imports Isac begin +theory Test_Isac imports "Knowledge/Isac" begin ML{* writeln "**** run the tests **************************************" *}; ML {* Toplevel.debug := true; *} @@ -31,18 +31,21 @@ cd"smltest/Scripts"; *) use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*) - use"../../../test/Tools/isac/ProgLang/calculate.sml"; (*part.*) -use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*part.*) +ML {*print_depth 999;*} +use"../../../test/Tools/isac/ProgLang/rewrite.sml"; (*GOON*) (* use"listg.sml"; use"scrtools.sml"; use"tools.sml"; cd "../.."; cd"smltest/ME"; - use"ctree.sml"; *) +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"; @@ -63,36 +66,45 @@ *) ML{* writeln "**** run tests on math-engine complete ******************" *}; (* -cd"smltest/IsacKnowledge"; +cd"smltest/IsacKnowledge"; ---below the order as in theoryy Isac--- use"atools.sml"; - use"complex.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.*) +(* + use"rational.sml" + 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"diffapp.sml"; *) use "../../../test/Tools/isac/Knowledge/integrate.sml"; (*part.*) (* - use"equation.sml"; - (*use"inssort.sml"; problems with recdef in Isabelle2002*) - use"logexp.sml"; -*) -use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*) -(* + use"eqsystem.sml"; use"polyminus.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"rateq.sml"; - use"rational.sml" (*TODO add_fractions_p throws overflow-exn WN*); - use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln', - for simplification search MG - erls: 98a(1) 104a(1) 104a(2) 68a *); - use"root.sml"; - use"rooteq.sml"; - use"rootrateq.sml"; - use"termorder.sml"; - use"trig.sml"; use"vect.sml"; - use"wn.sml"; - use"eqsystem.sml"; + use"diffapp.sml"; use"biegelinie.sml"; use"algein.sml"; cd "../..";