make Test_Isac.thy run in jEdit; intermed.
jEdit behaves differently from emacs in file dependencies.
Test_Isac.thy runs in emacs now.
For jEdit different uses seem appropriate; done in next step.
1.1 --- a/src/Tools/isac/Build_Isac.thy Sat Mar 19 15:18:10 2011 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Mar 23 17:20:39 2011 +0100
1.3 @@ -30,7 +30,7 @@
1.4 "use_thy ProgLang/Tools"
1.5 "use_thy ProgLang/Script"
1.6 use "ProgLang/scrtools.sml"
1.7 -*) "ProgLang/Language"
1.8 +*) "ProgLang/ProgLang"
1.9
1.10 (* use "Interpret/mstools.sml"
1.11 use "Interpret/ctree.sml"
1.12 @@ -74,7 +74,7 @@
1.13
1.14 ML {* check_guhs_unique := false; *}
1.15 ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
1.16 -
1.17 +ML {* @{theory "Isac"} *}
1.18 end
1.19
1.20 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
2.1 --- a/src/Tools/isac/Build_Test_Isac.thy Sat Mar 19 15:18:10 2011 +0100
2.2 +++ b/src/Tools/isac/Build_Test_Isac.thy Wed Mar 23 17:20:39 2011 +0100
2.3 @@ -16,7 +16,7 @@
2.4 header {* Loading the isac mathengine *}
2.5
2.6 theory Build_Test_Isac
2.7 -imports Complex_Main "ProgLang/Language" "Knowledge/Isac" "Test_Isac"
2.8 +imports Complex_Main "ProgLang/ProgLang" "Knowledge/Isac" "Test_Isac"
2.9 begin
2.10
2.11 use_thy "Build_Isac"
3.1 --- a/src/Tools/isac/Interpret/Interpret.thy Sat Mar 19 15:18:10 2011 +0100
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Mar 23 17:20:39 2011 +0100
3.3 @@ -3,7 +3,7 @@
3.4 (c) due to copyright terms
3.5 *)
3.6
3.7 -theory Interpret imports Language
3.8 +theory Interpret imports ProgLang
3.9 uses ("mstools.sml") ("ctree.sml") ("ptyps.sml") ("generate.sml")
3.10 ("calchead.sml") ("appl.sml") ("rewtools.sml") ("script.sml")
3.11 ("solve.sml") ("inform.sml") ("mathengine.sml")
4.1 --- a/src/Tools/isac/Knowledge/Delete.thy Sat Mar 19 15:18:10 2011 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Wed Mar 23 17:20:39 2011 +0100
4.3 @@ -3,7 +3,7 @@
4.4 (c) due to copyright terms
4.5 *)
4.6
4.7 -theory Delete imports "../ProgLang/Language" begin
4.8 +theory Delete imports "../ProgLang/ProgLang" begin
4.9
4.10 axioms (* theorems which are available only with long names,
4.11 which can not yet be handled in isac's scripts *)
5.1 --- a/src/Tools/isac/ProgLang/Language.thy Sat Mar 19 15:18:10 2011 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,12 +0,0 @@
5.4 -(* Title: collect all defitions for the program language
5.5 - Author: Walther Neuper 100831
5.6 - (c) due to copyright terms
5.7 - *)
5.8 -
5.9 -theory Language imports Script
5.10 - uses ("../ProgLang/scrtools.sml")
5.11 -begin
5.12 -
5.13 -use "../ProgLang/scrtools.sml"
5.14 -
5.15 -end
5.16 \ No newline at end of file
6.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sat Mar 19 15:18:10 2011 +0100
6.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Mar 23 17:20:39 2011 +0100
6.3 @@ -4,9 +4,10 @@
6.4 *)
6.5
6.6 theory ListC imports Complex_Main
6.7 -uses ("../library.sml")("../calcelems.sml")
6.8 -("termC.sml")("calculate.sml")
6.9 -("rewrite.sml")
6.10 +uses ("../library.sml")
6.11 + ("../calcelems.sml")
6.12 + ("termC.sml")("calculate.sml")
6.13 + ("rewrite.sml")
6.14 begin
6.15 use "../library.sml" (*indent,...*)
6.16 use "../calcelems.sml" (*str_of_type, Thm,...*)
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Wed Mar 23 17:20:39 2011 +0100
7.3 @@ -0,0 +1,12 @@
7.4 +(* Title: collect all defitions for the program language
7.5 + Author: Walther Neuper 100831
7.6 + (c) due to copyright terms
7.7 + *)
7.8 +
7.9 +theory ProgLang imports Script
7.10 + uses ("../ProgLang/scrtools.sml")
7.11 +begin
7.12 +
7.13 +use "../ProgLang/scrtools.sml"
7.14 +
7.15 +end
7.16 \ No newline at end of file
8.1 --- a/src/Tools/isac/Test_Isac.thy Sat Mar 19 15:18:10 2011 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,205 +0,0 @@
8.4 -(* Title: Run_Tests on isac
8.5 - Author: Walther Neuper 100808
8.6 - (c) due to copyright terms
8.7 -
8.8 -$ cd /usr/local/isabisac/src/Tools/isac
8.9 -$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
8.10 -$ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy &
8.11 -
8.12 -RESTART emacs after having created a new Isac heap with
8.13 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
8.14 -
8.15 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
8.16 - 10 20 30 40 50 60 70 80
8.17 -Keep this width during test; otherwise \n would be inserted into string-
8.18 -representation of terms and thus break some tests.
8.19 -*)
8.20 -
8.21 -theory Test_Isac imports "Knowledge/Isac" begin
8.22 -
8.23 -ML{* writeln "**** run the tests **************************************" *}
8.24 -ML {* Toplevel.debug := true; *}
8.25 -ML {*
8.26 -(*
8.27 -cd "systest";
8.28 -(*+ check kbtest/diffapp.sml for additional items in met-model*)
8.29 - use"root-equ.sml";
8.30 - use"script.sml";
8.31 - (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
8.32 - use"scriptnew.sml";
8.33 - use"subp-rooteq.sml";
8.34 - use"tacis.sml";
8.35 - use"interface-xml.sml";
8.36 - (* use"testdaten.sml"; no update after dropping 'errorBound'*)
8.37 - cd "../..";
8.38 -*)
8.39 -*}
8.40 -ML{* writeln "**** run systests complete ******************************" *}
8.41 -
8.42 -use"../../../test/Tools/isac/calcelems.sml" (*complete*)
8.43 -
8.44 -(*
8.45 -cd"smltest/Scripts";
8.46 -*)
8.47 -use"../../../test/Tools/isac/ProgLang/termC.sml" (*part.*)
8.48 -ML {*print_depth 9*}
8.49 -use"../../../test/Tools/isac/ProgLang/calculate.sml" (*part.*)
8.50 -
8.51 -ML {*store_met*}
8.52 -
8.53 -use"../../../test/Tools/isac/ProgLang/rewrite.sml" (*GOON*)
8.54 -(*
8.55 - use"listg.sml";
8.56 - use"scrtools.sml";
8.57 - use"tools.sml";
8.58 - cd "../..";
8.59 -cd"smltest/ME";
8.60 -*)
8.61 -use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*)
8.62 -use "../../../test/Tools/isac/Interpret/ctree.sml" (*part.*)
8.63 -use "../../../test/Tools/isac/Interpret/ptyps.sml" (*TODO*)
8.64 -use "../../../test/Tools/isac/Interpret/calchead.sml" (**)
8.65 -use "../../../test/Tools/isac/Interpret/rewtools.sml" (**)
8.66 -(*
8.67 - use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
8.68 - use"inform.sml";
8.69 -*)
8.70 -ML {*print_depth 5*}
8.71 -use "../../../test/Tools/isac/Interpret/mathengine.sml" (*part.+110310*)
8.72 -ML {**}
8.73 -(*
8.74 - use"me.sml";
8.75 - cd "../..";
8.76 -cd"smltest/xmlsrc";
8.77 - use"datatypes.sml";
8.78 - use"pbl-met-hierarchy.sml";
8.79 -use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml" (**)
8.80 -*)
8.81 -
8.82 -use"../../../test/Tools/isac/Frontend/interface.sml" (**)
8.83 -(*
8.84 - cd "../..";
8.85 -*)
8.86 -ML{* writeln "**** run tests on math-engine complete ******************" *}
8.87 -(*
8.88 -cd"smltest/IsacKnowledge"; ---below the order as in theory Isac---
8.89 - use"atools.sml";
8.90 - use"termorder.sml";
8.91 -*)
8.92 -use"../../../test/Tools/isac/Knowledge/simplify.sml" (*part.*)
8.93 -(*
8.94 - use"poly.sml"
8.95 -*)
8.96 -use"../../../test/Tools/isac/Knowledge/rational.sml" (*part.*)
8.97 -(*
8.98 - use"equation.sml";
8.99 - use"root.sml";
8.100 -*)
8.101 -ML {*
8.102 - t';
8.103 -*}
8.104 -
8.105 -ML {*
8.106 -e186a;
8.107 -str2term "x ~= 0";
8.108 -*}
8.109 -
8.110 -use "../../../test/Tools/isac/Knowledge/inssort.sml" (*part.*)
8.111 -ML {*
8.112 -(*
8.113 - (*use"inssort.sml"; problems with recdef in Isabelle2002*)
8.114 - use"rooteq.sml";
8.115 - use"rateq.sml";
8.116 - use"rootrateq.sml";
8.117 -
8.118 - use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
8.119 - ? also check others without check 'diff.behav.'*);
8.120 - use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
8.121 - for simplification search MG
8.122 - erls: 98a(1) 104a(1) 104a(2) 68a *);
8.123 - use"wn.sml";
8.124 - use"trig.sml";
8.125 - use"logexp.sml";
8.126 -*)
8.127 -*}
8.128 -ML {*print_depth 5*}
8.129 -use "../../../test/Tools/isac/Knowledge/diff.sml" (* +110310*)
8.130 -use "../../../test/Tools/isac/Knowledge/integrate.sml" (*complete--110310*)
8.131 -(*
8.132 - use"eqsystem.sml";
8.133 -*)
8.134 -ML {*print_depth 5*}
8.135 -use "../../../test/Tools/isac/Knowledge/polyminus.sml" (* part. *)
8.136 -(*
8.137 - use"vect.sml";
8.138 - use"diffapp.sml";
8.139 - use"biegelinie.sml";
8.140 - use"algein.sml";
8.141 -*)
8.142 -use "../../../test/Tools/isac/Knowledge/diophanteq.sml" (**)
8.143 -ML {*
8.144 -print_depth 999;
8.145 -nxt;
8.146 -*}
8.147 -use "../../../test/Tools/isac/Knowledge/isac.sml" (**)
8.148 -
8.149 -ML {*print_depth 999*}
8.150 -ML {*map Context.theory_name isabthys*}
8.151 -ML {*print_depth 5*}
8.152 -
8.153 -(*
8.154 - cd "../..";
8.155 -*)
8.156 -(* TODO
8.157 -use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
8.158 -:
8.159 -*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
8.160 -*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language"
8.161 -
8.162 -use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
8.163 -*)
8.164 -use "../../../test/Pure/library.sml" (**)
8.165 -use_thy "../../../test/Pure/General/Basics"
8.166 -
8.167 -use_thy "../../../test/Pure/Isar/Test_Parse_Term" (*part.*)
8.168 -use_thy "../../../test/Pure/Isar/Test_Parsers"
8.169 -
8.170 -ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}
8.171 -(*
8.172 -val path = "/home/neuper/proto3/testsml2xml/";
8.173 -pbl_hierarchy2file (path ^ "pbl/");
8.174 -pbls2file (path ^ "pbl/");
8.175 -met_hierarchy2file (path ^ "met/");
8.176 -mets2file (path ^ "met/");
8.177 -thy_hierarchy2file (path ^ "thy/");
8.178 -thes2file (path ^ "thy/");
8.179 -cd"sml";
8.180 -*)
8.181 -ML{* writeln "**** tested creation of xmldata *************************" *}
8.182 -
8.183 -ML{*states:=[];
8.184 - writeln "=========================================================";
8.185 -
8.186 - writeln "**** run systests complete ***************** re-organize!";
8.187 - writeln "**** run tests on math-engine complete ******************";
8.188 - writeln "**** run tests on IsacKnowledge complete ****************";
8.189 - writeln "**** build isac kernel + run tests complete *************";
8.190 - writeln "**** tested creation of xmldata *************************";
8.191 -*}
8.192 -
8.193 -end
8.194 -
8.195 -(*=== inhibit exn ?=============================================================
8.196 -===== inhibit exn ?===========================================================*)
8.197 -
8.198 -
8.199 -(*========== inhibit exn WN110319 ==============================================
8.200 -
8.201 -"########### testcode inserted vvv ###########################################";
8.202 -"########### testcode inserted ^^^ ###########################################";
8.203 -
8.204 -============ inhibit exn WN110319 ============================================*)
8.205 -
8.206 -
8.207 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
8.208 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
9.1 --- a/src/Tools/isac/Test_Some.thy Sat Mar 19 15:18:10 2011 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,40 +0,0 @@
9.4 -(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
9.5 - Author: Walther Neuper 101001
9.6 - (c) copyright due to lincense terms.
9.7 -
9.8 -$ cd /usr/local/isabisac/test/Tools/isac
9.9 -$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
9.10 -*)
9.11 -
9.12 -theory Test_Some imports Isac begin
9.13 -(*..................................########..................................*)
9.14 -
9.15 -ML{* writeln "**** run the test ***************************************" *}
9.16 -
9.17 -ML {*
9.18 -fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
9.19 -(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t;
9.20 -(*..............................................########......................*)
9.21 -*}
9.22 -
9.23 -ML {*parseNEW*}
9.24 -
9.25 -use"../../../test/Tools/isac/Interpret/mstools.sml";
9.26 -
9.27 -end
9.28 -
9.29 -
9.30 -(*=== inhibit exn ?=============================================================
9.31 -===== inhibit exn ?===========================================================*)
9.32 -
9.33 -
9.34 -(*========== inhibit exn 110317 ================================================
9.35 -
9.36 -"########### testcode inserted vvv ###########################################";
9.37 -"########### testcode inserted ^^^ ###########################################";
9.38 -
9.39 -============ inhibit exn 110317 ==============================================*)
9.40 -
9.41 -
9.42 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
9.43 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/test/Tools/isac/Frontend/Frontend.thy Wed Mar 23 17:20:39 2011 +0100
10.3 @@ -0,0 +1,21 @@
10.4 +(* Title: collect all defitions for the Frontend
10.5 + Author: Walther Neuper 110226
10.6 + (c) due to copyright terms
10.7 + *)
10.8 +
10.9 +theory Frontend imports Isac
10.10 + uses ("messages.sml")
10.11 + ("states.sml")
10.12 + ("interface.sml")
10.13 + ("../print_exn_G.sml")
10.14 +begin
10.15 +(*???
10.16 + ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
10.17 + use "messages.sml"
10.18 + use "states.sml"
10.19 + use "interface.sml"
10.20 +
10.21 + use "../print_exn_G.sml"
10.22 + ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
10.23 +*)
10.24 +end
10.25 \ No newline at end of file
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/test/Tools/isac/Frontend/Frontend_jedit.thy Wed Mar 23 17:20:39 2011 +0100
11.3 @@ -0,0 +1,19 @@
11.4 +(* Title: collect all defitions for the Frontend
11.5 + Author: Walther Neuper 110226
11.6 + (c) due to copyright terms
11.7 + *)
11.8 +
11.9 +theory Frontend_jedit imports Isac
11.10 + uses ("messages.sml")
11.11 + ("states.sml")
11.12 + ("interface.sml")
11.13 + ("../print_exn_G.sml")
11.14 +begin
11.15 + ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
11.16 + use "messages.sml" (*new 2011*)
11.17 + use "states.sml" (*new 2011*)
11.18 + use "interface.sml" (*part.*)
11.19 +
11.20 + use "../print_exn_G.sml" (*new 2011*)
11.21 + ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
11.22 +end
11.23 \ No newline at end of file
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/test/Tools/isac/Frontend/messages.sml Wed Mar 23 17:20:39 2011 +0100
12.3 @@ -0,0 +1,4 @@
12.4 +(* Title: test/../messages.sml
12.5 + Author: Walther Neuper 110320
12.6 + (c) copyright due to lincense terms.
12.7 +*)
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/Frontend/states.sml Wed Mar 23 17:20:39 2011 +0100
13.3 @@ -0,0 +1,4 @@
13.4 +(* Title: test/../states.sml
13.5 + Author: Walther Neuper 110320
13.6 + (c) copyright due to lincense terms.
13.7 +*)
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/test/Tools/isac/Interpret/Interpret.thy Wed Mar 23 17:20:39 2011 +0100
14.3 @@ -0,0 +1,34 @@
14.4 +(* Title: collect all defitions for the Lucas-Interpreter
14.5 + Author: Walther Neuper 110226
14.6 + (c) due to copyright terms
14.7 + *)
14.8 +
14.9 +theory Interpret imports Isac
14.10 +uses ("mstools.sml")
14.11 + ("ctree.sml")
14.12 + ("ptyps.sml")
14.13 + ("generate.sml")
14.14 + ("calchead.sml")
14.15 + ("appl.sml")
14.16 + ("rewtools.sml")
14.17 + ("script.sml")
14.18 + ("solve.sml")
14.19 + ("inform.sml")
14.20 + ("mathengine.sml")
14.21 +begin
14.22 +(*???*)
14.23 + ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
14.24 + use "mstools.sml"
14.25 +(*use "ctree.sml" *)
14.26 + use "ptyps.sml"
14.27 +(*use "generate.sml" *)
14.28 + use "calchead.sml"
14.29 +(*use "appl.sml" *)
14.30 + use "rewtools.sml"
14.31 +(*use "script.sml" *)
14.32 +(*use "solve.sml" *)
14.33 +(*use "inform.sml" *)
14.34 + use "mathengine.sml"
14.35 + ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
14.36 +(**)
14.37 +end
14.38 \ No newline at end of file
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/test/Tools/isac/Interpret/Interpret_jedit.thy Wed Mar 23 17:20:39 2011 +0100
15.3 @@ -0,0 +1,32 @@
15.4 +(* Title: collect all defitions for the Lucas-Interpreter
15.5 + Author: Walther Neuper 110226
15.6 + (c) due to copyright terms
15.7 + *)
15.8 +
15.9 +theory Interpret_jedit imports Isac
15.10 +uses ("mstools.sml")
15.11 + ("ctree.sml")
15.12 + ("ptyps.sml")
15.13 + ("generate.sml")
15.14 + ("calchead.sml")
15.15 + ("appl.sml")
15.16 + ("rewtools.sml")
15.17 + ("script.sml")
15.18 + ("solve.sml")
15.19 + ("inform.sml")
15.20 + ("mathengine.sml")
15.21 +begin
15.22 + ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
15.23 + use "mstools.sml"
15.24 +(*use "ctree.sml" *)
15.25 + use "ptyps.sml"
15.26 +(*use "generate.sml" *)
15.27 + use "calchead.sml"
15.28 +(*use "appl.sml" *)
15.29 + use "rewtools.sml"
15.30 +(*use "script.sml" *)
15.31 +(*use "solve.sml" *)
15.32 +(*use "inform.sml" *)
15.33 + use "mathengine.sml"
15.34 + ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
15.35 +end
15.36 \ No newline at end of file
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/test/Tools/isac/Interpret/appl.sml Wed Mar 23 17:20:39 2011 +0100
16.3 @@ -0,0 +1,4 @@
16.4 +(* Title: test/../appl.sml
16.5 + Author: Walther Neuper 110320
16.6 + (c) copyright due to lincense terms.
16.7 +*)
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/test/Tools/isac/Interpret/generate.sml Wed Mar 23 17:20:39 2011 +0100
17.3 @@ -0,0 +1,4 @@
17.4 +(* Title: test/../generate.sml
17.5 + Author: Walther Neuper 110320
17.6 + (c) copyright due to lincense terms.
17.7 +*)
18.1 --- a/test/Tools/isac/Interpret/mathengine.sml Sat Mar 19 15:18:10 2011 +0100
18.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Wed Mar 23 17:20:39 2011 +0100
18.3 @@ -132,9 +132,9 @@
18.4 "----- appendFormula TODO: first repair error";
18.5 val cs = ((pt,p),[]);
18.6 val ("ok", cs' as (_,_,(pt,p))) = step p cs;
18.7 - val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2"; val encode = I;
18.8 + val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
18.9 (*
18.10 - val ("no derivation found", (_,_,(pt, p))) = inform cs' (encode ifo);
18.11 + val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
18.12 here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
18.13 *)
18.14
19.1 --- a/test/Tools/isac/Knowledge/Isac.thy Sat Mar 19 15:18:10 2011 +0100
19.2 +++ b/test/Tools/isac/Knowledge/Isac.thy Wed Mar 23 17:20:39 2011 +0100
19.3 @@ -6,7 +6,12 @@
19.4 10 20 30 40 50 60 70 80
19.5 *)
19.6
19.7 -theory Isac imports Complex_Main (*TODO Build_Isac*) begin
19.8 +(*WN110319 theory Isac imports Complex_Main (*TODO Build_Isac*) begin*)
19.9 +theory isac imports Isac
19.10 +imports "Frontend/Frontend"
19.11 + PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*) DiophantEq Test
19.12 +begin
19.13 +
19.14
19.15 text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;
19.16 the leading parts of longnames can be dropped with some exceptions. *}
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/test/Tools/isac/Knowledge/Knowledge.thy Wed Mar 23 17:20:39 2011 +0100
20.3 @@ -0,0 +1,44 @@
20.4 +theory Knowledge imports Isac "../../../../test/Tools/isac/Knowledge/Isac"
20.5 +uses
20.6 + ("delete.sml") ("descript.sml") ("atools.sml")
20.7 + ("simplify.sml") ("poly.sml") ("rational.sml") ("equation.sml") ("root.sml")
20.8 + ("lineq.sml") ("rooteq.sml") ("rateq.sml") ("rootrateq.sml") (*"polyeq.sml"*)
20.9 +
20.10 + ("calculus.sml") ("trig.sml") ("logexp.sml") ("diff.sml") ("integrate.sml")
20.11 + ("eqsystem.sml") ("test.sml") ("polyminus.sml") ("vect.sml") ("diffapp.sml")
20.12 + ("biegelinie.sml") ("algein.sml") ("diophanteq.sml") ("isac.sml")
20.13 +
20.14 +begin
20.15 +
20.16 + ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
20.17 + use "delete.sml" (*new 2011*)
20.18 + use "descript.sml" (*new 2011*)
20.19 + use "atools.sml" (*2002, added termorder.sml 2011*)
20.20 + use "simplify.sml" (*part.*)
20.21 + use "poly.sml" (*2002*)
20.22 + use "rational.sml" (*part.*)
20.23 + use "equation.sml" (*2002*)
20.24 + use "root.sml" (*2002*)
20.25 + use "lineq.sml" (*new 2011*)
20.26 + use "rooteq.sml" (*2002*)
20.27 + use "rateq.sml" (*2002*)
20.28 + use "rootrateq.sml" (*2002*)
20.29 +(*use "polyeq.sml" (*2002*) WN110323 error with comments*)
20.30 + use "calculus.sml" (*new 2011*)
20.31 + use "trig.sml" (*2002*)
20.32 + use "logexp.sml" (*2002*)
20.33 + use "diff.sml" (*part.*)
20.34 + use "integrate.sml" (*part. was complete 2009-2*)
20.35 + use "eqsystem.sml" (*2002*)
20.36 + use "test.sml" (*new 2011*)
20.37 + use "polyminus.sml" (*part.*)
20.38 + use "vect.sml" (*2002*)
20.39 + use "diffapp.sml" (*2002*)
20.40 + use "biegelinie.sml" (*2002*)
20.41 + use "algein.sml" (*2002*)
20.42 + use "diophanteq.sml" (*complete*)
20.43 + use "isac.sml" (*part.*)
20.44 + ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
20.45 +
20.46 +end
20.47 +
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/test/Tools/isac/Knowledge/Knowledge_jedit.thy Wed Mar 23 17:20:39 2011 +0100
21.3 @@ -0,0 +1,43 @@
21.4 +theory Knowledge_jedit imports Isac "../../../../test/Tools/isac/Knowledge/Isac"
21.5 +uses
21.6 + ("delete.sml") ("descript.sml") ("atools.sml")
21.7 + ("simplify.sml") ("poly.sml") ("rational.sml") ("equation.sml") ("root.sml")
21.8 + ("lineq.sml") ("rooteq.sml") ("rateq.sml") ("rootrat.sml") ("rootrateq.sml")
21.9 + ("polyeq.sml")
21.10 + ("calculus.sml") ("trig.sml") ("logexp.sml") ("diff.sml") ("integrate.sml")
21.11 + ("eqsystem.sml") ("test.sml") ("polyminus.sml") ("vect.sml") ("diffapp.sml")
21.12 + ("biegelinie.sml") ("algein.sml") ("diophanteq.sml") ("isac.sml")
21.13 +
21.14 +begin
21.15 + ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
21.16 + use "delete.sml"
21.17 + use "descript.sml"
21.18 +(*use "atools.sml" *)
21.19 + use "simplify.sml"
21.20 +(*use "poly.sml" *)
21.21 + use "rational.sml"
21.22 +(*use "equation.sml" *)
21.23 +(*use "root.sml" *)
21.24 + use "lineq.sml"
21.25 +(*use "rooteq.sml" *)
21.26 +(*use "rateq.sml" *)
21.27 +(*use "rootrat.sml" *)
21.28 +(*use "rootrateq.sml" *)
21.29 +(*use "polyeq.sml" *)
21.30 + use "calculus.sml"
21.31 +(*use "trig.sml" *)
21.32 +(*use "logexp.sml" *)
21.33 + use "diff.sml"
21.34 + use "integrate.sml"
21.35 +(*use "eqsystem.sml" *)
21.36 + use "test.sml"
21.37 + use "polyminus.sml"
21.38 +(*use "vect.sml" *)
21.39 +(*use "diffapp.sml" *)
21.40 +(*use "biegelinie.sml" *)
21.41 +(*use "algein.sml" *)
21.42 + use "diophanteq.sml"
21.43 + use "isac.sml"
21.44 + ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
21.45 +end
21.46 +
22.1 --- a/test/Tools/isac/Knowledge/algein.sml Sat Mar 19 15:18:10 2011 +0100
22.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Mar 23 17:20:39 2011 +0100
22.3 @@ -5,7 +5,6 @@
22.4 use"../smltest/IsacKnowledge/algein.sml";
22.5 use"algein.sml";
22.6 *)
22.7 -val thy = AlgEin.thy;
22.8
22.9 "-----------------------------------------------------------------";
22.10 "table of contents -----------------------------------------------";
22.11 @@ -18,6 +17,8 @@
22.12 "-----------------------------------------------------------------";
22.13 "-----------------------------------------------------------------";
22.14
22.15 +(*=== inhibit exn ?=============================================================
22.16 +val thy = AlgEin.thy;
22.17
22.18
22.19 (* use"../smltest/IsacKnowledge/algein.sml";
22.20 @@ -156,3 +157,4 @@
22.21 (* use"../smltest/IsacKnowledge/algein.sml";
22.22 *)
22.23
22.24 +===== inhibit exn ?===========================================================*)
23.1 --- a/test/Tools/isac/Knowledge/atools.sml Sat Mar 19 15:18:10 2011 +0100
23.2 +++ b/test/Tools/isac/Knowledge/atools.sml Wed Mar 23 17:20:39 2011 +0100
23.3 @@ -7,16 +7,18 @@
23.4 use"atools.sml";
23.5 *)
23.6
23.7 -"-----------------------------------------------------------------";
23.8 -"table of contents -----------------------------------------------";
23.9 -"-----------------------------------------------------------------";
23.10 -"----------- occurs_in -------------------------------------------";
23.11 -"----------- argument_of -----------------------------------------";
23.12 -"----------- sameFunId -------------------------------------------";
23.13 -"----------- filter_sameFunId ------------------------------------";
23.14 -"----------- boollist2sum ----------------------------------------";
23.15 -"-----------------------------------------------------------------";
23.16 +"--------------------------------------------------------";
23.17 +"table of contents --------------------------------------";
23.18 +"--------------------------------------------------------";
23.19 +"----------- occurs_in ----------------------------------";
23.20 +"----------- argument_of --------------------------------";
23.21 +"----------- sameFunId ----------------------------------";
23.22 +"----------- filter_sameFunId ---------------------------";
23.23 +"----------- boollist2sum -------------------------------";
23.24 +"----------- termorder (<-- termorder.sml) --------------";
23.25 +"--------------------------------------------------------";
23.26
23.27 +(*=== inhibit exn ?=============================================================
23.28
23.29 val thy = Atools.thy;
23.30
23.31 @@ -126,6 +128,199 @@
23.32 trace_rewrite:=false;
23.33
23.34
23.35 -(* use"IsacKnowledge/Atools.ML";
23.36 - use"../smltest/IsacKnowledge/atools.sml";
23.37 - *)
23.38 \ No newline at end of file
23.39 +"----------- termorder (<-- termorder.sml) --------------";
23.40 +"----------- termorder (<-- termorder.sml) --------------";
23.41 +"----------- termorder (<-- termorder.sml) --------------";
23.42 + (* tests on rewrite orders
23.43 + author Matthias Goldgruber 2003
23.44 +
23.45 + WN0509 do not use this file anymore, since orders require thy:
23.46 + do tests in the smltest/IsacKnowledge/file.sml
23.47 + where file.ML defines the respective order !
23.48 +
23.49 +use"../smltest/IsacKnowledge/termorder.sml";
23.50 +*)
23.51 +
23.52 +
23.53 + (*MK die ersten Tests*)
23.54 + val substa = [(e_term, (term_of o the o (parse thy)) "a")];
23.55 + val substb = [(e_term, (term_of o the o (parse thy)) "b")];
23.56 + val substx = [(e_term, (term_of o the o (parse thy)) "x")];
23.57 +
23.58 + val x1 = (term_of o the o (parse thy)) "a + b + x";
23.59 + val x2 = (term_of o the o (parse thy)) "a + x + b";
23.60 + val x3 = (term_of o the o (parse thy)) "a + x + b";
23.61 + val x4 = (term_of o the o (parse thy)) "x + a + b";
23.62 +
23.63 +if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
23.64 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
23.65 +
23.66 +if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
23.67 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
23.68 +
23.69 +if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
23.70 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
23.71 +
23.72 + val aa = (term_of o the o (parse thy)) "-1 * a * x";
23.73 + val bb = (term_of o the o (parse thy)) "x^^^3";
23.74 + ord_make_polynomial_in true thy substx (aa, bb);
23.75 + true; (* => LESS *)
23.76 +
23.77 + val aa = (term_of o the o (parse thy)) "-1 * a * x";
23.78 + val bb = (term_of o the o (parse thy)) "x^^^3";
23.79 + ord_make_polynomial_in true thy substa (aa, bb);
23.80 + false; (* => GREATER *)
23.81 +
23.82 + (*und nach dem Re-engineering der Termorders in den 'rulesets'
23.83 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
23.84 + val bdv= (term_of o the o (parse thy)) "bdv";
23.85 + val x = (term_of o the o (parse thy)) "x";
23.86 + val a = (term_of o the o (parse thy)) "a";
23.87 + val b = (term_of o the o (parse thy)) "b";
23.88 + val SOME (t',_) =
23.89 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
23.90 +if term2str t' = "b + x + a" then ()
23.91 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
23.92 +
23.93 + val NONE =
23.94 + rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
23.95 + term2str t';
23.96 + "a + x + b";
23.97 +
23.98 + val SOME (t',_) =
23.99 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
23.100 +if term2str t' = "a + b + x" then ()
23.101 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
23.102 +
23.103 +
23.104 +
23.105 + val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
23.106 + val ppp = (term_of o the o (parse thy)) ppp';
23.107 + val SOME (t',_) =
23.108 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
23.109 +(*MG 2003...
23.110 + term2str t';
23.111 + "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
23.112 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
23.113 +else error "termorder.sml diff.behav ord_make_polynomial_in #14";
23.114 +
23.115 + val SOME (t',_) =
23.116 + rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
23.117 +(*MG 2003...
23.118 + "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
23.119 +if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
23.120 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
23.121 +
23.122 + val ttt' = "(3*x + 5)/18";
23.123 + val ttt = (term_of o the o (parse thy)) ttt';
23.124 + val SOME (uuu,_) =
23.125 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
23.126 +if term2str uuu = "(5 + 3 * x) / 18" then ()
23.127 +else error "termorder.sml diff.behav ord_make_polynomial_in #16";
23.128 +
23.129 + val SOME (uuu,_) =
23.130 + rewrite_set_ thy false make_polynomial ttt;
23.131 +if term2str uuu = "(5 + 3 * x) / 18" then ()
23.132 +else error "termorder.sml diff.behav ord_make_polynomial_in #16";
23.133 +
23.134 +
23.135 +
23.136 +
23.137 +(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
23.138 +
23.139 + (*Aufgabe zum Einstieg in die Arbeit...*)
23.140 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
23.141 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
23.142 + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
23.143 + term2str t;
23.144 + "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
23.145 + val SOME (t,_) =
23.146 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
23.147 + term2str t;
23.148 + "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
23.149 +(* bei Verwendung von "size_of-term" nach MG :*)
23.150 +(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
23.151 +
23.152 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
23.153 + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
23.154 + term2str t;
23.155 + "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
23.156 +(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
23.157 +
23.158 + val SOME (t,_) =
23.159 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
23.160 + term2str t;
23.161 + "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
23.162 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
23.163 + "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
23.164 +
23.165 + (*das rewriting l"asst sich beobachten mit
23.166 + trace_rewrite:=true;
23.167 + *)
23.168 +
23.169 +
23.170 +
23.171 +"------15.11.02 --------------------------";
23.172 + val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
23.173 + val bdv = (term_of o the o (parse thy)) "bdv";
23.174 + val a = (term_of o the o (parse thy)) "a";
23.175 +
23.176 + trace_rewrite:=true;
23.177 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
23.178 + val SOME (t,_) =
23.179 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
23.180 + term2str t;
23.181 + val SOME (t,_) =
23.182 + rewrite_set_ thy false discard_parentheses t;
23.183 + term2str t;
23.184 +"1 + b * x + x * a";
23.185 +
23.186 + val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
23.187 + val SOME (t,_) =
23.188 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
23.189 + term2str t;
23.190 + val SOME (t,_) =
23.191 + rewrite_set_ thy false discard_parentheses t;
23.192 + term2str t;
23.193 +"1 + (x + b * x) * a + a ^^^ 2";
23.194 +
23.195 + val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
23.196 + val SOME (t,_) =
23.197 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
23.198 + term2str t;
23.199 + val SOME (t,_) =
23.200 + rewrite_set_ thy false discard_parentheses t;
23.201 + term2str t;
23.202 +"1 + b * a + (7 + x) * a ^^^ 2";
23.203 +
23.204 +(* MG2003
23.205 + Atools.thy grundlegende Algebra
23.206 + Poly.thy Polynome
23.207 + Rational.thy Br"uche
23.208 + Root.thy Wurzeln
23.209 + RootRat.thy Wurzen + Br"uche
23.210 + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
23.211 +
23.212 + cd"knowledge";
23.213 + remove_thy"Termorder";
23.214 + use_thy"Isac";
23.215 +
23.216 + get_thm Termorder.thy "bdv_n_collect";
23.217 + get_thm (theory "Isac") "bdv_n_collect";
23.218 +
23.219 +*)
23.220 + val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
23.221 + val SOME (t,_) =
23.222 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
23.223 + term2str t;
23.224 + val SOME (t,_) =
23.225 + rewrite_set_ thy false discard_parentheses t;
23.226 + term2str t;
23.227 +"(7 + x) * a ^^^ 2";
23.228 +
23.229 + val t = (term_of o the o (parse Termorder.thy)) "Pi";
23.230 +
23.231 + val t = (term_of o the o (parseold thy)) "7";
23.232 +
23.233 +----------------------------------------------------------------------*)
23.234 +===== inhibit exn ?===========================================================*)
24.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Sat Mar 19 15:18:10 2011 +0100
24.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Mar 23 17:20:39 2011 +0100
24.3 @@ -5,7 +5,6 @@
24.4 use"../smltest/IsacKnowledge/biegelinie.sml";
24.5 use"biegelinie.sml";
24.6 *)
24.7 -val thy = Biegelinie.thy;
24.8
24.9 "-----------------------------------------------------------------";
24.10 "table of contents -----------------------------------------------";
24.11 @@ -26,6 +25,8 @@
24.12 "-----------------------------------------------------------------";
24.13 "-----------------------------------------------------------------";
24.14
24.15 +(*=== inhibit exn ?=============================================================
24.16 +val thy = Biegelinie.thy;
24.17
24.18 "----------- the rules -------------------------------------------";
24.19 "----------- the rules -------------------------------------------";
24.20 @@ -1038,3 +1039,5 @@
24.21 (*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
24.22
24.23 "----- functions comming from:";
24.24 +
24.25 +===== inhibit exn ?===========================================================*)
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/test/Tools/isac/Knowledge/calculus.sml Wed Mar 23 17:20:39 2011 +0100
25.3 @@ -0,0 +1,4 @@
25.4 +(* Title: test/../calculus.sml
25.5 + Author: Walther Neuper 110320
25.6 + (c) copyright due to lincense terms.
25.7 +*)
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/test/Tools/isac/Knowledge/delete.sml Wed Mar 23 17:20:39 2011 +0100
26.3 @@ -0,0 +1,4 @@
26.4 +(* Title: test/../delete.sml
26.5 + Author: Walther Neuper 110320
26.6 + (c) copyright due to lincense terms.
26.7 +*)
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/test/Tools/isac/Knowledge/descript.sml Wed Mar 23 17:20:39 2011 +0100
27.3 @@ -0,0 +1,4 @@
27.4 +(* Title: test/../descript.sml
27.5 + Author: Walther Neuper 110320
27.6 + (c) copyright due to lincense terms.
27.7 +*)
28.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Sat Mar 19 15:18:10 2011 +0100
28.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Mar 23 17:20:39 2011 +0100
28.3 @@ -20,6 +20,7 @@
28.4 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
28.5
28.6
28.7 +(*=== inhibit exn ?=============================================================
28.8
28.9
28.10
28.11 @@ -750,3 +751,4 @@
28.12
28.13
28.14
28.15 +===== inhibit exn ?===========================================================*)
29.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Sat Mar 19 15:18:10 2011 +0100
29.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Mar 23 17:20:39 2011 +0100
29.3 @@ -6,7 +6,6 @@
29.4 use"../smltest/IsacKnowledge/eqsystem.sml";
29.5 use"eqsystem.sml";
29.6 *)
29.7 -val thy = EqSystem.thy;
29.8
29.9 "-----------------------------------------------------------------";
29.10 "table of contents -----------------------------------------------";
29.11 @@ -31,6 +30,8 @@
29.12 "-----------------------------------------------------------------";
29.13 "-----------------------------------------------------------------";
29.14
29.15 +(*=== inhibit exn ?=============================================================
29.16 +val thy = EqSystem.thy;
29.17
29.18 "----------- occur_exactly_in ------------------------------------";
29.19 "----------- occur_exactly_in ------------------------------------";
29.20 @@ -1443,3 +1444,4 @@
29.21 use"../smltest/IsacKnowledge/eqsystem.sml";
29.22 use"eqsystem.sml";
29.23 *)
29.24 +===== inhibit exn ?===========================================================*)
30.1 --- a/test/Tools/isac/Knowledge/equation.sml Sat Mar 19 15:18:10 2011 +0100
30.2 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Mar 23 17:20:39 2011 +0100
30.3 @@ -1,12 +1,7 @@
30.4 (* tests on the equation solver
30.5 - author: Walther Neuper
30.6 - 070703
30.7 + author: Walther Neuper 070703
30.8 (c) due to copyright terms
30.9 -
30.10 -use"../smltest/IsacKnowledge/equation.sml";
30.11 -use"equation.sml";
30.12 *)
30.13 -val thy = (theory "Isac");
30.14
30.15 "-----------------------------------------------------------------";
30.16 "table of contents -----------------------------------------------";
30.17 @@ -16,6 +11,8 @@
30.18 "-----------------------------------------------------------------";
30.19 "-----------------------------------------------------------------";
30.20
30.21 +(*=== inhibit exn ?=============================================================
30.22 +val thy = (theory "Isac");
30.23
30.24 "----------- CAS input -------------------------------------------";
30.25 "----------- CAS input -------------------------------------------";
30.26 @@ -31,3 +28,4 @@
30.27 show_pt pt;
30.28 if p = ([], Res) andalso term2str res = "[x = 1]" then ()
30.29 else error "equation.sml behav.changed for CAS solve (x+1=2, x))";
30.30 +===== inhibit exn ?===========================================================*)
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/test/Tools/isac/Knowledge/lineq.sml Wed Mar 23 17:20:39 2011 +0100
31.3 @@ -0,0 +1,4 @@
31.4 +(* Title: test/../lineq.sml
31.5 + Author: Walther Neuper 110320
31.6 + (c) copyright due to lincense terms.
31.7 +*)
32.1 --- a/test/Tools/isac/Knowledge/logexp.sml Sat Mar 19 15:18:10 2011 +0100
32.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed Mar 23 17:20:39 2011 +0100
32.3 @@ -3,7 +3,6 @@
32.4 use"../smltest/IsacKnowledge/logexp.sml";
32.5 *)
32.6
32.7 -val thy = LogExp.thy;
32.8 "-----------------------------------------------------------------";
32.9 "table of contents -----------------------------------------------";
32.10 "-----------------------------------------------------------------";
32.11 @@ -12,6 +11,8 @@
32.12 "-----------------------------------------------------------------";
32.13 "-----------------------------------------------------------------";
32.14
32.15 +(*=== inhibit exn ?=============================================================
32.16 +val thy = LogExp.thy;
32.17
32.18 "----------- setup presentation innsbruck ------------------------";
32.19 "----------- setup presentation innsbruck ------------------------";
32.20 @@ -59,3 +60,4 @@
32.21 show_pt pt;
32.22
32.23 *-------------------------------------------------------------------*)
32.24 +===== inhibit exn ?===========================================================*)
33.1 --- a/test/Tools/isac/Knowledge/poly.sml Sat Mar 19 15:18:10 2011 +0100
33.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Mar 23 17:20:39 2011 +0100
33.3 @@ -29,6 +29,7 @@
33.4 "--------------------------------------------------------";
33.5 "--------------------------------------------------------";
33.6
33.7 +(*=== inhibit exn ?=============================================================
33.8
33.9 "-------- check is'_polyexp is_polyexp ------------------";
33.10 "-------- check is'_polyexp is_polyexp ------------------";
33.11 @@ -557,4 +558,5 @@
33.12 val t1 = str2term "2 * b + (3 * a + 3 * b)";
33.13 val t2 = str2term "3 * a + (2 * b + 3 * b)";
33.14
33.15 +===== inhibit exn ============================================================*)
33.16 ===== inhibit exn ?===========================================================*)
34.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Sat Mar 19 15:18:10 2011 +0100
34.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Mar 23 17:20:39 2011 +0100
34.3 @@ -28,6 +28,8 @@
34.4 "-----------------------------------------------------------------";
34.5 "-----------------------------------------------------------------";
34.6
34.7 +(*=== inhibit exn ?=============================================================
34.8 +
34.9 val c = [];
34.10
34.11 "----------- tests on predicates in problems ---------------------";
34.12 @@ -1176,3 +1178,4 @@
34.13 val ((pt,p),_) = get_calc 1; show_pt pt;
34.14
34.15 interSteps 1 ([1],Res) (*no Rewrite_Set...*);
34.16 +===== inhibit exn ?===========================================================*)
35.1 --- a/test/Tools/isac/Knowledge/rateq.sml Sat Mar 19 15:18:10 2011 +0100
35.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Mar 23 17:20:39 2011 +0100
35.3 @@ -11,6 +11,8 @@
35.4 "---------(1/x=5) ---------------------";
35.5 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
35.6
35.7 +(*=== inhibit exn ?=============================================================
35.8 +
35.9 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
35.10 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
35.11 val result = term2str t_;
35.12 @@ -143,3 +145,5 @@
35.13 else error "rateq.sml: new behaviour: [x = -2, x = 10]";
35.14
35.15 "----------- rateq.sml end--------";
35.16 +
35.17 +===== inhibit exn ?===========================================================*)
36.1 --- a/test/Tools/isac/Knowledge/root.sml Sat Mar 19 15:18:10 2011 +0100
36.2 +++ b/test/Tools/isac/Knowledge/root.sml Wed Mar 23 17:20:39 2011 +0100
36.3 @@ -1,5 +1,15 @@
36.4 -(* testexamples for Root, radicals
36.5 - *)
36.6 +(* Title: testexamples for Root, radicals
36.7 + Author: Walther Neuper
36.8 + (c) due to copyright terms
36.9 + *)
36.10 +"--------------------------------------------------------";
36.11 +"table of contents --------------------------------------";
36.12 +"--------------------------------------------------------";
36.13 +"----------- TODO ---------------------------------------";
36.14 +"--------------------------------------------------------";
36.15 +"--------------------------------------------------------";
36.16 +
36.17 +(*=== inhibit exn ?=============================================================
36.18
36.19 val thy = Root.thy;
36.20
36.21 @@ -13,3 +23,4 @@
36.22 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
36.23 term2str t';
36.24 if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1";
36.25 +===== inhibit exn ?===========================================================*)
37.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Sat Mar 19 15:18:10 2011 +0100
37.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Mar 23 17:20:39 2011 +0100
37.3 @@ -14,6 +14,9 @@
37.4 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
37.5 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
37.6 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
37.7 +"--------------------------------------------------------";
37.8 +
37.9 +(*=== inhibit exn ?=============================================================
37.10
37.11 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
37.12 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
37.13 @@ -468,3 +471,4 @@
37.14 "----------- rooteq.sml end--------";
37.15
37.16
37.17 +===== inhibit exn ?===========================================================*)
38.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Sat Mar 19 15:18:10 2011 +0100
38.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Mar 23 17:20:39 2011 +0100
38.3 @@ -2,11 +2,15 @@
38.4 use"rootrateq.sml";
38.5 *)
38.6
38.7 +
38.8 +"--------------------- tests on predicates -------------------------------";
38.9 +"--------------------- tests on predicates -------------------------------";
38.10 +"--------------------- tests on predicates -------------------------------";
38.11 +
38.12 +(*=== inhibit exn ?=============================================================
38.13 +
38.14 val thy = (theory "Isac");
38.15
38.16 -"--------------------- tests on predicates -------------------------------";
38.17 -"--------------------- tests on predicates -------------------------------";
38.18 -"--------------------- tests on predicates -------------------------------";
38.19 (*
38.20 Compiler.Control.Print.printDepth:=5; (*4 default*)
38.21 trace_rewrite:=true;
38.22 @@ -227,3 +231,4 @@
38.23 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
38.24 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
38.25 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
38.26 +===== inhibit exn ?===========================================================*)
39.1 --- a/test/Tools/isac/Knowledge/termorder.sml Sat Mar 19 15:18:10 2011 +0100
39.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
39.3 @@ -1,192 +0,0 @@
39.4 - (* tests on rewrite orders
39.5 - author Matthias Goldgruber 2003
39.6 -
39.7 - WN0509 do not use this file anymore, since orders require thy:
39.8 - do tests in the smltest/IsacKnowledge/file.sml
39.9 - where file.ML defines the respective order !
39.10 -
39.11 -use"../smltest/IsacKnowledge/termorder.sml";
39.12 -*)
39.13 -
39.14 -
39.15 - (*MK die ersten Tests*)
39.16 - val substa = [(e_term, (term_of o the o (parse thy)) "a")];
39.17 - val substb = [(e_term, (term_of o the o (parse thy)) "b")];
39.18 - val substx = [(e_term, (term_of o the o (parse thy)) "x")];
39.19 -
39.20 - val x1 = (term_of o the o (parse thy)) "a + b + x";
39.21 - val x2 = (term_of o the o (parse thy)) "a + x + b";
39.22 - val x3 = (term_of o the o (parse thy)) "a + x + b";
39.23 - val x4 = (term_of o the o (parse thy)) "x + a + b";
39.24 -
39.25 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
39.26 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
39.27 -
39.28 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
39.29 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
39.30 -
39.31 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
39.32 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
39.33 -
39.34 - val aa = (term_of o the o (parse thy)) "-1 * a * x";
39.35 - val bb = (term_of o the o (parse thy)) "x^^^3";
39.36 - ord_make_polynomial_in true thy substx (aa, bb);
39.37 - true; (* => LESS *)
39.38 -
39.39 - val aa = (term_of o the o (parse thy)) "-1 * a * x";
39.40 - val bb = (term_of o the o (parse thy)) "x^^^3";
39.41 - ord_make_polynomial_in true thy substa (aa, bb);
39.42 - false; (* => GREATER *)
39.43 -
39.44 - (*und nach dem Re-engineering der Termorders in den 'rulesets'
39.45 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
39.46 - val bdv= (term_of o the o (parse thy)) "bdv";
39.47 - val x = (term_of o the o (parse thy)) "x";
39.48 - val a = (term_of o the o (parse thy)) "a";
39.49 - val b = (term_of o the o (parse thy)) "b";
39.50 - val SOME (t',_) =
39.51 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
39.52 -if term2str t' = "b + x + a" then ()
39.53 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
39.54 -
39.55 - val NONE =
39.56 - rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
39.57 - term2str t';
39.58 - "a + x + b";
39.59 -
39.60 - val SOME (t',_) =
39.61 - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
39.62 -if term2str t' = "a + b + x" then ()
39.63 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
39.64 -
39.65 -
39.66 -
39.67 - val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
39.68 - val ppp = (term_of o the o (parse thy)) ppp';
39.69 - val SOME (t',_) =
39.70 - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
39.71 -(*MG 2003...
39.72 - term2str t';
39.73 - "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
39.74 -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
39.75 -else error "termorder.sml diff.behav ord_make_polynomial_in #14";
39.76 -
39.77 - val SOME (t',_) =
39.78 - rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
39.79 -(*MG 2003...
39.80 - "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
39.81 -if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
39.82 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
39.83 -
39.84 - val ttt' = "(3*x + 5)/18";
39.85 - val ttt = (term_of o the o (parse thy)) ttt';
39.86 - val SOME (uuu,_) =
39.87 - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
39.88 -if term2str uuu = "(5 + 3 * x) / 18" then ()
39.89 -else error "termorder.sml diff.behav ord_make_polynomial_in #16";
39.90 -
39.91 - val SOME (uuu,_) =
39.92 - rewrite_set_ thy false make_polynomial ttt;
39.93 -if term2str uuu = "(5 + 3 * x) / 18" then ()
39.94 -else error "termorder.sml diff.behav ord_make_polynomial_in #16";
39.95 -
39.96 -
39.97 -
39.98 -
39.99 -(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
39.100 -
39.101 - (*Aufgabe zum Einstieg in die Arbeit...*)
39.102 - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
39.103 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
39.104 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
39.105 - term2str t;
39.106 - "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
39.107 - val SOME (t,_) =
39.108 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
39.109 - term2str t;
39.110 - "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
39.111 -(* bei Verwendung von "size_of-term" nach MG :*)
39.112 -(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
39.113 -
39.114 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
39.115 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
39.116 - term2str t;
39.117 - "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
39.118 -(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
39.119 -
39.120 - val SOME (t,_) =
39.121 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
39.122 - term2str t;
39.123 - "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
39.124 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
39.125 - "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
39.126 -
39.127 - (*das rewriting l"asst sich beobachten mit
39.128 - trace_rewrite:=true;
39.129 - *)
39.130 -
39.131 -
39.132 -
39.133 -"------15.11.02 --------------------------";
39.134 - val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
39.135 - val bdv = (term_of o the o (parse thy)) "bdv";
39.136 - val a = (term_of o the o (parse thy)) "a";
39.137 -
39.138 - trace_rewrite:=true;
39.139 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
39.140 - val SOME (t,_) =
39.141 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
39.142 - term2str t;
39.143 - val SOME (t,_) =
39.144 - rewrite_set_ thy false discard_parentheses t;
39.145 - term2str t;
39.146 -"1 + b * x + x * a";
39.147 -
39.148 - val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
39.149 - val SOME (t,_) =
39.150 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
39.151 - term2str t;
39.152 - val SOME (t,_) =
39.153 - rewrite_set_ thy false discard_parentheses t;
39.154 - term2str t;
39.155 -"1 + (x + b * x) * a + a ^^^ 2";
39.156 -
39.157 - val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
39.158 - val SOME (t,_) =
39.159 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
39.160 - term2str t;
39.161 - val SOME (t,_) =
39.162 - rewrite_set_ thy false discard_parentheses t;
39.163 - term2str t;
39.164 -"1 + b * a + (7 + x) * a ^^^ 2";
39.165 -
39.166 -(* MG2003
39.167 - Atools.thy grundlegende Algebra
39.168 - Poly.thy Polynome
39.169 - Rational.thy Br"uche
39.170 - Root.thy Wurzeln
39.171 - RootRat.thy Wurzen + Br"uche
39.172 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
39.173 -
39.174 - cd"knowledge";
39.175 - remove_thy"Termorder";
39.176 - use_thy"Isac";
39.177 -
39.178 - get_thm Termorder.thy "bdv_n_collect";
39.179 - get_thm (theory "Isac") "bdv_n_collect";
39.180 -
39.181 -*)
39.182 - val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
39.183 - val SOME (t,_) =
39.184 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
39.185 - term2str t;
39.186 - val SOME (t,_) =
39.187 - rewrite_set_ thy false discard_parentheses t;
39.188 - term2str t;
39.189 -"(7 + x) * a ^^^ 2";
39.190 -
39.191 - val t = (term_of o the o (parse Termorder.thy)) "Pi";
39.192 -
39.193 - val t = (term_of o the o (parseold thy)) "7";
39.194 -
39.195 -----------------------------------------------------------------------*)
40.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
40.2 +++ b/test/Tools/isac/Knowledge/test.sml Wed Mar 23 17:20:39 2011 +0100
40.3 @@ -0,0 +1,4 @@
40.4 +(* Title: test/../test.sml
40.5 + Author: Walther Neuper 110320
40.6 + (c) copyright due to lincense terms.
40.7 +*)
41.1 --- a/test/Tools/isac/Knowledge/trig.sml Sat Mar 19 15:18:10 2011 +0100
41.2 +++ b/test/Tools/isac/Knowledge/trig.sml Wed Mar 23 17:20:39 2011 +0100
41.3 @@ -1,2 +1,7 @@
41.4 (* testexamples for Trig, trigonometry
41.5 - *)
41.6 \ No newline at end of file
41.7 + *)
41.8 +"--------------------------------------------------------";
41.9 +"table of contents --------------------------------------";
41.10 +"--------------------------------------------------------";
41.11 +"----------- TODO ---------------------------------------";
41.12 +"--------------------------------------------------------";
42.1 --- a/test/Tools/isac/Knowledge/vect.sml Sat Mar 19 15:18:10 2011 +0100
42.2 +++ b/test/Tools/isac/Knowledge/vect.sml Wed Mar 23 17:20:39 2011 +0100
42.3 @@ -1,2 +1,7 @@
42.4 (* testexamples for Vect, vector spaces
42.5 - *)
42.6 \ No newline at end of file
42.7 + *)
42.8 +"--------------------------------------------------------";
42.9 +"table of contents --------------------------------------";
42.10 +"--------------------------------------------------------";
42.11 +"----------- TODO ---------------------------------------";
42.12 +"--------------------------------------------------------";
43.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
43.2 +++ b/test/Tools/isac/ProgLang/ProgLang.thy Wed Mar 23 17:20:39 2011 +0100
43.3 @@ -0,0 +1,26 @@
43.4 +(* Title: collect all defitions for the program language
43.5 + Author: Walther Neuper 100831
43.6 + (c) due to copyright terms
43.7 + *)
43.8 +
43.9 +theory ProgLang imports Isac
43.10 +uses ("../library.sml")
43.11 + ("../calcelems.sml")
43.12 + ("scrtools.sml")
43.13 + ("termC.sml")
43.14 + ("calculate.sml")
43.15 + ("rewrite.sml")
43.16 +begin
43.17 +(*???
43.18 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
43.19 + use "../library.sml"
43.20 + use "../calcelems.sml"
43.21 + use "termC.sml"
43.22 + use "calculate.sml"
43.23 + use "rewrite.sml"
43.24 +(*use "listg.sml" *)
43.25 +(*use "scrtools.sml" *)
43.26 +(*use"tools.sml" *)
43.27 + ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
43.28 +*)
43.29 +end
43.30 \ No newline at end of file
44.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
44.2 +++ b/test/Tools/isac/ProgLang/ProgLang_jedit.thy Wed Mar 23 17:20:39 2011 +0100
44.3 @@ -0,0 +1,26 @@
44.4 +(* Title: collect all defitions for the program language
44.5 + Author: Walther Neuper 100831
44.6 + (c) due to copyright terms
44.7 + *)
44.8 +
44.9 +theory ProgLang_jedit imports Isac
44.10 +uses ("../library.sml")
44.11 + ("../calcelems.sml")
44.12 + ("termC.sml")
44.13 + ("calculate.sml")
44.14 + ("rewrite.sml")
44.15 + (*"listg.sml"*)
44.16 + (*"scrtools.sml"*)
44.17 + (*"tools.sml"*)
44.18 +begin
44.19 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
44.20 + use "../library.sml"
44.21 + use "../calcelems.sml"
44.22 + use "termC.sml"
44.23 + use "calculate.sml"
44.24 +(*use "rewrite.sml" *)
44.25 +(*use "listg.sml" *)
44.26 +(*use "scrtools.sml" *)
44.27 +(*use"tools.sml" *)
44.28 + ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
44.29 +end
44.30 \ No newline at end of file
45.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Sat Mar 19 15:18:10 2011 +0100
45.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Wed Mar 23 17:20:39 2011 +0100
45.3 @@ -23,6 +23,7 @@
45.4 "--------------------------------------------------------";
45.5 "--------------------------------------------------------";
45.6
45.7 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
45.8
45.9 "----------- assemble rewrite ---------------------------";
45.10 "----------- assemble rewrite ---------------------------";
45.11 @@ -54,7 +55,6 @@
45.12 (*lookup in isabelle?trace?response...*)
45.13 writeln(Syntax.string_of_term ctxt rew);
45.14 writeln(Syntax.string_of_term ctxt RHS);
45.15 -
45.16 "===== rewriting: prep insertion into rew_sub";
45.17 val thy = @{theory Complex_Main};
45.18 val ctxt = @{context};
45.19 @@ -504,7 +504,6 @@
45.20 scan_ chk prepat;
45.21 tracing "=== poly.sml: scan_ chk prepat end";
45.22
45.23 -
45.24 "----- chk ---";
45.25 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
45.26 val [(pres, pat)] = prepat;
45.27 @@ -524,5 +523,4 @@
45.28 ([], true) => ()
45.29 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
45.30
45.31 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
45.32 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
46.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
46.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Mar 23 17:20:39 2011 +0100
46.3 @@ -0,0 +1,126 @@
46.4 +(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
46.5 + Author: Walther Neuper 101001
46.6 + (c) copyright due to lincense terms.
46.7 +
46.8 +$ cd /usr/local/isabisac/test/Tools/isac
46.9 +$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
46.10 +*)
46.11 +
46.12 +theory Test_Isac imports Isac
46.13 + "ProgLang/ProgLang"
46.14 + "Interpret/Interpret"
46.15 + "xmlsrc/xmlsrc"
46.16 + "Frontend/Frontend"
46.17 + "Knowledge/Knowledge"
46.18 +begin
46.19 +(* cd "systest";
46.20 + (*+ check kbtest/diffapp.sml for additional items in met-model*)
46.21 + use"root-equ.sml";
46.22 + use"script.sml";
46.23 + (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
46.24 + use"scriptnew.sml";
46.25 + use"subp-rooteq.sml";
46.26 + use"tacis.sml";
46.27 + use"interface-xml.sml";
46.28 + (* use"testdaten.sml"; no update after dropping 'errorBound'*)
46.29 + cd "../..";
46.30 +*)
46.31 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
46.32 + use "library.sml" (*new 2011*)
46.33 + use "calcelems.sml" (*complete*)
46.34 + use "ProgLang/termC.sml" (*part.*)
46.35 + use "ProgLang/calculate.sml" (*part.*)
46.36 + use "ProgLang/rewrite.sml" (*part.*)
46.37 +(*use "ProgLang/listg.sml" 2002*)
46.38 +(*use "ProgLang/scrtools.sml" 2002*)
46.39 +(*use "ProgLang/tools.sml" 2002*)
46.40 + ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
46.41 +
46.42 +(*??? "ProgLang/ProgLang"*)
46.43 +
46.44 + ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
46.45 + use "Interpret/mstools.sml" (*empty*)
46.46 +(*use "Interpret/ctree.sml" TODO*)
46.47 + use "Interpret/ptyps.sml" (* *)
46.48 +(*use "Interpret/generate.sml" new 2011*)
46.49 + use "Interpret/calchead.sml" (* *)
46.50 +(*use "Interpret/appl.sml" new 2011*)
46.51 + use "Interpret/rewtools.sml" (* *)
46.52 +(*use "Interpret/script.sml" TODO*)
46.53 +(*use "Interpret/solve.sml" TODO*)
46.54 +(*use "Interpret/inform.sml" TODO*)
46.55 + use "Interpret/mathengine.sml"(*part.*)
46.56 + ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
46.57 +
46.58 +(*??? "Interpret/Interpret"*)
46.59 +
46.60 + ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
46.61 +(*use "xmlsrc/mathml.sml" TODO*)
46.62 +(*use "xmlsrc/datatypes.sml" TODO*)
46.63 +(*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
46.64 +(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
46.65 + use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
46.66 + ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
46.67 +
46.68 +(*??? "xmlsrc/xmlsrc"*)
46.69 +
46.70 + ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
46.71 + use "Frontend/messages.sml" (*new 2011*)
46.72 + use "Frontend/states.sml" (*new 2011*)
46.73 + use "Frontend/interface.sml" (*part.*)
46.74 +
46.75 + use "print_exn_G.sml" (*new 2011*)
46.76 + ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
46.77 +
46.78 +(*??? "Frontend/Frontend"*)
46.79 +
46.80 + ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
46.81 + use "Knowledge/delete.sml" (*new 2011*)
46.82 + use "Knowledge/descript.sml" (*new 2011*)
46.83 +(*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
46.84 + use "Knowledge/simplify.sml" (*part.*)
46.85 +(*use "Knowledge/poly.sml" 2002*)
46.86 + use "Knowledge/rational.sml" (*part.*)
46.87 +(*use "Knowledge/equation.sml" 2002*)
46.88 +(*use "Knowledge/root.sml" 2002*)
46.89 + use "Knowledge/lineq.sml" (*new 2011*)
46.90 +(*use "Knowledge/rooteq.sml" 2002*)
46.91 +(*use "Knowledge/rateq.sml" 2002*)
46.92 +(*use "Knowledge/rootrat.sml" 2002*)
46.93 +(*use "Knowledge/rootrateq.sml" 2002*)
46.94 +(*use "Knowledge/polyeq.sml" 2002*)
46.95 + use "Knowledge/calculus.sml" (*new 2011*)
46.96 +(*use "Knowledge/trig.sml" 2002*)
46.97 +(*use "Knowledge/logexp.sml" 2002*)
46.98 + use "Knowledge/diff.sml" (*part.*)
46.99 + use "Knowledge/integrate.sml" (*part. was complete 2009-2*)
46.100 +(*use "Knowledge/eqsystem.sml" 2002*)
46.101 + use "Knowledge/test.sml" (*new 2011*)
46.102 + use "Knowledge/polyminus.sml" (*part.*)
46.103 +(*use "Knowledge/vect.sml" 2002*)
46.104 +(*use "Knowledge/diffapp.sml" 2002*)
46.105 +(*use "Knowledge/biegelinie.sml" 2002*)
46.106 +(*use "Knowledge/algein.sml" 2002*)
46.107 + use "Knowledge/diophanteq.sml" (*complete*)
46.108 + use "Knowledge/isac.sml" (*part.*)
46.109 + ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
46.110 +
46.111 +(*??? "Knowledge/Knowledge"*)
46.112 +
46.113 +end
46.114 +
46.115 +
46.116 +(*=== inhibit exn ?=============================================================
46.117 +===== inhibit exn ?===========================================================*)
46.118 +
46.119 +
46.120 +(*========== inhibit exn 110317 ================================================
46.121 +
46.122 +"########### testcode inserted vvv ###########################################";
46.123 +"########### testcode inserted ^^^ ###########################################";
46.124 +
46.125 +============ inhibit exn 110317 ==============================================*)
46.126 +
46.127 +
46.128 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
46.129 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
47.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
47.2 +++ b/test/Tools/isac/Test_Isac_jedit.thy Wed Mar 23 17:20:39 2011 +0100
47.3 @@ -0,0 +1,45 @@
47.4 +(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
47.5 + Author: Walther Neuper 101001
47.6 + (c) copyright due to lincense terms.
47.7 +
47.8 +$ cd /usr/local/isabisac/test/Tools/isac
47.9 +$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
47.10 +*)
47.11 +
47.12 +theory Test_Isac_jedit imports Isac
47.13 +uses ( "library.sml")
47.14 + ( "calcelems.sml")
47.15 + ("ProgLang/termC.sml")
47.16 + ("ProgLang/calculate.sml")
47.17 + ("ProgLang/rewrite.sml")
47.18 + ("ProgLang/listg.sml")
47.19 + ("ProgLang/scrtools.sml")
47.20 + ("ProgLang/tools.sml")
47.21 +
47.22 +begin
47.23 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
47.24 + use "library.sml" (*new 2011*)
47.25 + use "calcelems.sml" (*complete*)
47.26 + use "ProgLang/termC.sml" (*part.*)
47.27 + use "ProgLang/calculate.sml" (*part.*)
47.28 + use "ProgLang/rewrite.sml" (*part.*)
47.29 +
47.30 + ML {*"%%%%%%%%%%%%%%%%% all test finished successfully %%%%%%%";*}
47.31 +
47.32 +end
47.33 +
47.34 +
47.35 +(*=== inhibit exn ?=============================================================
47.36 +===== inhibit exn ?===========================================================*)
47.37 +
47.38 +
47.39 +(*========== inhibit exn 110317 ================================================
47.40 +
47.41 +"########### testcode inserted vvv ###########################################";
47.42 +"########### testcode inserted ^^^ ###########################################";
47.43 +
47.44 +============ inhibit exn 110317 ==============================================*)
47.45 +
47.46 +
47.47 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
47.48 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
48.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
48.2 +++ b/test/Tools/isac/Test_Some.thy Wed Mar 23 17:20:39 2011 +0100
48.3 @@ -0,0 +1,50 @@
48.4 +(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
48.5 + Author: Walther Neuper 101001
48.6 + (c) copyright due to lincense terms.
48.7 +
48.8 +$ cd /usr/local/isabisac/test/Tools/isac
48.9 +$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
48.10 +*)
48.11 +
48.12 +theory Test_Some imports Isac begin
48.13 +(*..................................########..................................*)
48.14 +
48.15 +ML {*
48.16 +parse;
48.17 +parseNEW;
48.18 +update_loc';
48.19 +*}
48.20 +
48.21 +
48.22 +ML{* writeln "**** run the test ***************************************" *}
48.23 +
48.24 +ML {*
48.25 +fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
48.26 +(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t;
48.27 +(*..............................................########......................*)
48.28 +*}
48.29 +
48.30 +ML {*pos'2str;
48.31 +
48.32 +
48.33 +*}
48.34 +
48.35 +use"../../../test/Tools/isac/Interpret/mstools.sml"
48.36 +
48.37 +end
48.38 +
48.39 +
48.40 +(*=== inhibit exn ?=============================================================
48.41 +===== inhibit exn ?===========================================================*)
48.42 +
48.43 +
48.44 +(*========== inhibit exn 110317 ================================================
48.45 +
48.46 +"########### testcode inserted vvv ###########################################";
48.47 +"########### testcode inserted ^^^ ###########################################";
48.48 +
48.49 +============ inhibit exn 110317 ==============================================*)
48.50 +
48.51 +
48.52 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
48.53 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
49.1 --- a/test/Tools/isac/library.sml Sat Mar 19 15:18:10 2011 +0100
49.2 +++ b/test/Tools/isac/library.sml Wed Mar 23 17:20:39 2011 +0100
49.3 @@ -1,4 +1,9 @@
49.4 -{*
49.5 +Toplevel.debug := true;
49.6 +
49.7 +fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
49.8 +(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t;
49.9 +(*..............................................########......................*)
49.10 +
49.11 "--- Pure/General/ord_list.ML";
49.12 union;
49.13 union (op =) [1,2,3] [3,4,5];
49.14 @@ -9,4 +14,4 @@
49.15 merge;
49.16 merge (op =) ([1,2,3], [3,4,5]);
49.17 (*val it = [4, 5, 1, 2, 3] : int list*)
49.18 -*}
49.19 +
50.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
50.2 +++ b/test/Tools/isac/print_exn_G.sml Wed Mar 23 17:20:39 2011 +0100
50.3 @@ -0,0 +1,4 @@
50.4 +(* Title: test/../print_exn_G.sml
50.5 + Author: Walther Neuper 110320
50.6 + (c) copyright due to lincense terms.
50.7 +*)
51.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
51.2 +++ b/test/Tools/isac/xmlsrc/interface-xml.sml Wed Mar 23 17:20:39 2011 +0100
51.3 @@ -0,0 +1,4 @@
51.4 +(* Title: test/../interface-xml.sml
51.5 + Author: Walther Neuper 110320
51.6 + (c) copyright due to lincense terms.
51.7 +*)
52.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
52.2 +++ b/test/Tools/isac/xmlsrc/xmlsrc.thy Wed Mar 23 17:20:39 2011 +0100
52.3 @@ -0,0 +1,22 @@
52.4 +(* Title: collect all defitions for xml generation
52.5 + Author: Walther Neuper 110226
52.6 + (c) due to copyright terms
52.7 +*)
52.8 +
52.9 +theory xmlsrc imports Isac
52.10 + uses ("mathml.sml")
52.11 + ("datatypes.sml")
52.12 + ("pbl-met-hierarchy.sml")
52.13 + ("thy-hierarchy.sml")
52.14 + ("interface-xml.sml")
52.15 +begin
52.16 +(*???
52.17 + ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
52.18 +(*use "xmlsrc/mathml.sml" *)
52.19 +(*use "xmlsrc/datatypes.sml" *)
52.20 +(*use "xmlsrc/pbl-met-hierarchy.sml" *)
52.21 +(*use "xmlsrc/thy-hierarchy.sml" *)
52.22 + use "xmlsrc/interface-xml.sml"
52.23 + ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
52.24 +*)
52.25 +end
52.26 \ No newline at end of file
53.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
53.2 +++ b/test/Tools/isac/xmlsrc/xmlsrc_jedit.thy Wed Mar 23 17:20:39 2011 +0100
53.3 @@ -0,0 +1,20 @@
53.4 +(* Title: collect all defitions for xml generation
53.5 + Author: Walther Neuper 110226
53.6 + (c) due to copyright terms
53.7 +*)
53.8 +
53.9 +theory xmlsrc_jedit imports Isac
53.10 + uses ("mathml.sml")
53.11 + ("datatypes.sml")
53.12 + ("pbl-met-hierarchy.sml")
53.13 + ("thy-hierarchy.sml")
53.14 + ("interface-xml.sml")
53.15 +begin
53.16 + ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
53.17 +(*use "xmlsrc/mathml.sml" *)
53.18 +(*use "xmlsrc/datatypes.sml" *)
53.19 +(*use "xmlsrc/pbl-met-hierarchy.sml" *)
53.20 +(*use "xmlsrc/thy-hierarchy.sml" *)
53.21 + use "xmlsrc/interface-xml.sml"
53.22 + ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
53.23 +end
53.24 \ No newline at end of file