intermed. context introduction to specification phase
1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Apr 04 11:05:07 2011 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 06 18:01:02 2011 +0200
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 Mon Apr 04 11:05:07 2011 +0200
2.2 +++ b/src/Tools/isac/Build_Test_Isac.thy Wed Apr 06 18:01:02 2011 +0200
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 Mon Apr 04 11:05:07 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Apr 06 18:01:02 2011 +0200
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/Interpret/calchead.sml Mon Apr 04 11:05:07 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed Apr 06 18:01:02 2011 +0200
4.3 @@ -276,7 +276,7 @@
4.4
4.5 (*.to an input (d,ts) find the according ori and insert the ts.*)
4.6 (*WN.11.03: + dont take first inter<>[]*)
4.7 -fun seek_oridts ctxt sel (d,ts) [] =
4.8 +(*fun seek_oridts ctxt sel (d,ts) [] =
4.9 ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
4.10 (comp_dts (d,ts))) ^
4.11 "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
4.12 @@ -286,6 +286,21 @@
4.13 then ("",
4.14 (id,vat,sel,d, inter op = ts ts'):ori,
4.15 ts')
4.16 + else seek_oridts ctxt sel (d,ts) oris;*)
4.17 +
4.18 +fun seek_oridts ctxt sel (d,ts) [] =
4.19 + ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
4.20 + (comp_dts (d,ts))) ^
4.21 + "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
4.22 + [])
4.23 + | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
4.24 + if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
4.25 + then if sel = sel'
4.26 + then ("",
4.27 + (id,vat,sel,d, inter op = ts ts'):ori,
4.28 + ts')
4.29 + else ((Print_Mode.setmp [] (Syntax.string_of_term ctxt) (comp_dts (d,ts)))
4.30 + ^ " not for " ^ sel, e_ori_, [])
4.31 else seek_oridts ctxt sel (d,ts) oris;
4.32
4.33 (*.to an input (_,ts) find the according ori and insert the ts.*)
5.1 --- a/src/Tools/isac/Knowledge/Delete.thy Mon Apr 04 11:05:07 2011 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Wed Apr 06 18:01:02 2011 +0200
5.3 @@ -3,7 +3,7 @@
5.4 (c) due to copyright terms
5.5 *)
5.6
5.7 -theory Delete imports "../ProgLang/Language" begin
5.8 +theory Delete imports "../ProgLang/ProgLang" begin
5.9
5.10 axioms (* theorems which are available only with long names,
5.11 which can not yet be handled in isac's scripts *)
6.1 --- a/src/Tools/isac/ProgLang/Language.thy Mon Apr 04 11:05:07 2011 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,12 +0,0 @@
6.4 -(* Title: collect all defitions for the program language
6.5 - Author: Walther Neuper 100831
6.6 - (c) due to copyright terms
6.7 - *)
6.8 -
6.9 -theory Language imports Script
6.10 - uses ("../ProgLang/scrtools.sml")
6.11 -begin
6.12 -
6.13 -use "../ProgLang/scrtools.sml"
6.14 -
6.15 -end
6.16 \ No newline at end of file
7.1 --- a/src/Tools/isac/ProgLang/ListC.thy Mon Apr 04 11:05:07 2011 +0200
7.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Wed Apr 06 18:01:02 2011 +0200
7.3 @@ -4,9 +4,10 @@
7.4 *)
7.5
7.6 theory ListC imports Complex_Main
7.7 -uses ("../library.sml")("../calcelems.sml")
7.8 -("termC.sml")("calculate.sml")
7.9 -("rewrite.sml")
7.10 +uses ("../library.sml")
7.11 + ("../calcelems.sml")
7.12 + ("termC.sml")("calculate.sml")
7.13 + ("rewrite.sml")
7.14 begin
7.15 use "../library.sml" (*indent,...*)
7.16 use "../calcelems.sml" (*str_of_type, Thm,...*)
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Wed Apr 06 18:01:02 2011 +0200
8.3 @@ -0,0 +1,12 @@
8.4 +(* Title: collect all defitions for the program language
8.5 + Author: Walther Neuper 100831
8.6 + (c) due to copyright terms
8.7 + *)
8.8 +
8.9 +theory ProgLang imports Script
8.10 + uses ("../ProgLang/scrtools.sml")
8.11 +begin
8.12 +
8.13 +use "../ProgLang/scrtools.sml"
8.14 +
8.15 +end
8.16 \ No newline at end of file
9.1 --- a/src/Tools/isac/Test_Isac.thy Mon Apr 04 11:05:07 2011 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,207 +0,0 @@
9.4 -(* Title: Run_Tests on isac
9.5 - Author: Walther Neuper 100808
9.6 - (c) due to copyright terms
9.7 -
9.8 -$ cd /usr/local/isabisac/src/Tools/isac
9.9 -$ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
9.10 -$ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy &
9.11 -
9.12 -RESTART emacs after having created a new Isac heap with
9.13 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
9.14 -
9.15 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
9.16 - 10 20 30 40 50 60 70 80
9.17 -Keep this width during test; otherwise \n would be inserted into string-
9.18 -representation of terms and thus break some tests.
9.19 -*)
9.20 -
9.21 -theory Test_Isac imports
9.22 - "Knowledge/Isac"
9.23 - "../../../test/Pure/General/Basics"
9.24 - "../../../test/Pure/Isar/Test_Parse_Term" (*part.*)
9.25 - "../../../test/Pure/Isar/Test_Parsers"
9.26 -begin
9.27 -
9.28 -ML{* writeln "**** run the tests **************************************" *}
9.29 -ML {* Toplevel.debug := true; *}
9.30 -ML {*
9.31 -(*
9.32 -cd "systest";
9.33 -(*+ check kbtest/diffapp.sml for additional items in met-model*)
9.34 - use"root-equ.sml";
9.35 - use"script.sml";
9.36 - (* use"script_if.sml"; WN03 missing: is_rootequation_in*)
9.37 - use"scriptnew.sml";
9.38 - use"subp-rooteq.sml";
9.39 - use"tacis.sml";
9.40 - use"interface-xml.sml";
9.41 - (* use"testdaten.sml"; no update after dropping 'errorBound'*)
9.42 - cd "../..";
9.43 -*)
9.44 -*}
9.45 -ML{* writeln "**** run systests complete ******************************" *}
9.46 -
9.47 -use"../../../test/Tools/isac/calcelems.sml" (*complete*)
9.48 -
9.49 -(*
9.50 -cd"smltest/Scripts";
9.51 -*)
9.52 -use"../../../test/Tools/isac/ProgLang/termC.sml" (*part.*)
9.53 -ML {*print_depth 90*}
9.54 -use"../../../test/Tools/isac/ProgLang/calculate.sml" (*part.*)
9.55 -
9.56 -ML {*store_met*}
9.57 -
9.58 -use"../../../test/Tools/isac/ProgLang/rewrite.sml" (*GOON*)
9.59 -(*
9.60 - use"listg.sml";
9.61 - use"scrtools.sml";
9.62 - use"tools.sml";
9.63 - cd "../..";
9.64 -cd"smltest/ME";
9.65 -*)
9.66 -
9.67 -use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*)
9.68 -use "../../../test/Tools/isac/Interpret/ctree.sml" (*part.*)
9.69 -use "../../../test/Tools/isac/Interpret/ptyps.sml" (*TODO*)
9.70 -use "../../../test/Tools/isac/Interpret/calchead.sml" (**)
9.71 -use "../../../test/Tools/isac/Interpret/rewtools.sml" (**)
9.72 -(*
9.73 - use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
9.74 - use"inform.sml";
9.75 -*)
9.76 -ML {*print_depth 300*}
9.77 -use "../../../test/Tools/isac/Interpret/mathengine.sml" (*part.+110310*)
9.78 -ML {**}
9.79 -(*
9.80 - use"me.sml";
9.81 - cd "../..";
9.82 -cd"smltest/xmlsrc";
9.83 - use"datatypes.sml";
9.84 - use"pbl-met-hierarchy.sml";
9.85 -use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml" (**)
9.86 -*)
9.87 -
9.88 -use"../../../test/Tools/isac/Frontend/interface.sml" (**)
9.89 -(*
9.90 - cd "../..";
9.91 -*)
9.92 -ML{* writeln "**** run tests on math-engine complete ******************" *}
9.93 -(*
9.94 -cd"smltest/IsacKnowledge"; ---below the order as in theory Isac---
9.95 - use"atools.sml";
9.96 - use"termorder.sml";
9.97 -*)
9.98 -use"../../../test/Tools/isac/Knowledge/simplify.sml" (*part.*)
9.99 -(*
9.100 - use"poly.sml"
9.101 -*)
9.102 -use"../../../test/Tools/isac/Knowledge/rational.sml" (*part.*)
9.103 -(*
9.104 - use"equation.sml";
9.105 - use"root.sml";
9.106 -*)
9.107 -ML {*
9.108 - t';
9.109 -*}
9.110 -
9.111 -ML {*
9.112 -e186a;
9.113 -str2term "x ~= 0";
9.114 -*}
9.115 -
9.116 -use "../../../test/Tools/isac/Knowledge/inssort.sml" (*part.*)
9.117 -ML {*
9.118 -(*
9.119 - (*use"inssort.sml"; problems with recdef in Isabelle2002*)
9.120 - use"rooteq.sml";
9.121 - use"rateq.sml";
9.122 - use"rootrateq.sml";
9.123 -
9.124 - use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
9.125 - ? also check others without check 'diff.behav.'*);
9.126 - use"rlang.sml"; (*WN.12.6.03: for TODOs search 'writeln',
9.127 - for simplification search MG
9.128 - erls: 98a(1) 104a(1) 104a(2) 68a *);
9.129 - use"wn.sml";
9.130 - use"trig.sml";
9.131 - use"logexp.sml";
9.132 -*)
9.133 -*}
9.134 -ML {*print_depth 5*}
9.135 -use "../../../test/Tools/isac/Knowledge/diff.sml" (* +110310*)
9.136 -use "../../../test/Tools/isac/Knowledge/integrate.sml" (*complete--110310*)
9.137 -(*
9.138 - use"eqsystem.sml";
9.139 -*)
9.140 -ML {*print_depth 5*}
9.141 -use "../../../test/Tools/isac/Knowledge/polyminus.sml" (* part. *)
9.142 -(*
9.143 - use"vect.sml";
9.144 - use"diffapp.sml";
9.145 - use"biegelinie.sml";
9.146 - use"algein.sml";
9.147 -*)
9.148 -use "../../../test/Tools/isac/Knowledge/diophanteq.sml" (**)
9.149 -ML {*
9.150 -print_depth 999;
9.151 -nxt;
9.152 -*}
9.153 -use "../../../test/Tools/isac/Knowledge/isac.sml" (**)
9.154 -
9.155 -ML {*print_depth 999*}
9.156 -ML {*map Context.theory_name isabthys*}
9.157 -ML {*print_depth 5*}
9.158 -
9.159 -(*
9.160 - cd "../..";
9.161 -*)
9.162 -(* TODO
9.163 -use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
9.164 -:
9.165 -*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
9.166 -*** Theory loader: the error(s) above occurred while examining Thy_Info.get_theory "Foo_Language"
9.167 -
9.168 -use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
9.169 -*)
9.170 -use "../../../test/Pure/library.sml" (**)
9.171 -
9.172 -ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}
9.173 -(*
9.174 -val path = "/home/neuper/proto3/testsml2xml/";
9.175 -pbl_hierarchy2file (path ^ "pbl/");
9.176 -pbls2file (path ^ "pbl/");
9.177 -met_hierarchy2file (path ^ "met/");
9.178 -mets2file (path ^ "met/");
9.179 -thy_hierarchy2file (path ^ "thy/");
9.180 -thes2file (path ^ "thy/");
9.181 -cd"sml";
9.182 -*)
9.183 -ML{* writeln "**** tested creation of xmldata *************************" *}
9.184 -
9.185 -ML{*states:=[];
9.186 - writeln "=========================================================";
9.187 -
9.188 - writeln "**** run systests complete ***************** re-organize!";
9.189 - writeln "**** run tests on math-engine complete ******************";
9.190 - writeln "**** run tests on IsacKnowledge complete ****************";
9.191 - writeln "**** build isac kernel + run tests complete *************";
9.192 - writeln "**** tested creation of xmldata *************************";
9.193 -*}
9.194 -
9.195 -end
9.196 -
9.197 -(*=== inhibit exn ?=============================================================
9.198 -===== inhibit exn ?===========================================================*)
9.199 -
9.200 -
9.201 -(*========== inhibit exn WN110319 ==============================================
9.202 -
9.203 -"########### testcode inserted vvv ###########################################";
9.204 -"########### testcode inserted ^^^ ###########################################";
9.205 -
9.206 -============ inhibit exn WN110319 ============================================*)
9.207 -
9.208 -
9.209 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
9.210 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
10.1 --- a/src/Tools/isac/Test_Some.thy Mon Apr 04 11:05:07 2011 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,39 +0,0 @@
10.4 -(* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS'
10.5 - Author: Walther Neuper 101001
10.6 - (c) copyright due to lincense terms.
10.7 -
10.8 -$ cd /usr/local/isabisac/test/Tools/isac
10.9 -$ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy &
10.10 -*)
10.11 -
10.12 -theory Test_Some imports Isac begin
10.13 -(*..................................########..................................*)
10.14 -
10.15 -ML{* writeln "**** run the test ***************************************" *}
10.16 -
10.17 -ML {*
10.18 -fun term2st t = Print_Mode.setmp [] (Syntax.string_of_term
10.19 -(ProofContext.init_global (Thy_Info.get_theory "Rational"))) t;
10.20 -(*..............................................########......................*)
10.21 -*}
10.22 -
10.23 -use "../../../test/Tools/isac/ProgLang/calculate.sml";
10.24 -use "../../../test/Tools/isac/Interpret/mathengine.sml";
10.25 -
10.26 -end
10.27 -
10.28 -
10.29 -(*=== inhibit exn ?=============================================================
10.30 -===== inhibit exn ?===========================================================*)
10.31 -
10.32 -
10.33 -(*========== inhibit exn 110317 ================================================
10.34 -
10.35 -"########### testcode inserted vvv ###########################################";
10.36 -"########### testcode inserted ^^^ ###########################################";
10.37 -
10.38 -============ inhibit exn 110317 ==============================================*)
10.39 -
10.40 -
10.41 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.42 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/Build_Test.thy Wed Apr 06 18:01:02 2011 +0200
11.3 @@ -0,0 +1,25 @@
11.4 +(* Title: test/../test-depend/Build_Test.thy
11.5 + Author: Walther Neuper 110320
11.6 + (c) copyright due to lincense terms.
11.7 +*)
11.8 +
11.9 +header {* file dependencies according to Test_Isac.thy *}
11.10 +
11.11 +theory Build_Test
11.12 +imports Main "testdir1/testdir1" "testdirm/testdirm"
11.13 +begin
11.14 +
11.15 + text {* jedit and emacs treat file dependencies differently.
11.16 + The files in test-depend/ mimic Test_Isac.thy.
11.17 + Tests are independent by all importing Main.
11.18 + We have this directory/file structure:
11.19 + testdir1/testdir1.thy collects all testfiles in testdir1
11.20 + testfile-1-1.sml
11.21 + testfile-1-n.sml
11.22 + testdirm/testdirm.thy collects all testfiles in testdirm
11.23 + testfile-m-1.sml
11.24 + testfile-m-n.sml
11.25 + *}
11.26 + ML {*"=== test-depend/Build_test.thy =================="*}
11.27 +
11.28 +end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testdir1.thy Wed Apr 06 18:01:02 2011 +0200
12.3 @@ -0,0 +1,18 @@
12.4 +(* Title: test/../test-depend/testdir1.thy
12.5 + Author: Walther Neuper 110320
12.6 + (c) copyright due to lincense terms.
12.7 +*)
12.8 +
12.9 +header {* collect all testfiles in directory testdir1/ *}
12.10 +
12.11 +theory testdir1
12.12 +imports Main
12.13 +uses ("testfile-1-1.sml")("testfile-1-n.sml")
12.14 +begin
12.15 +
12.16 + ML {*"===== test-depend/testdir1/testdir1.thy ========="*}
12.17 + use "testfile-1-1.sml"
12.18 + use "testfile-1-n.sml"
12.19 +
12.20 +end
12.21 +
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testfile-1-1.sml Wed Apr 06 18:01:02 2011 +0200
13.3 @@ -0,0 +1,8 @@
13.4 +(* Title: test/../test-depend/testdir1/testfile-1-1.sml
13.5 + Author: Walther Neuper 110320
13.6 + (c) copyright due to lincense terms.
13.7 +*)
13.8 +
13.9 +"======= test-depend/testdir1/testfile-1-1.sml ===";
13.10 +"========= content testfile-1-1.sml ==============";
13.11 +
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdir1/testfile-1-n.sml Wed Apr 06 18:01:02 2011 +0200
14.3 @@ -0,0 +1,8 @@
14.4 +(* Title: test/../test-depend/testdir1/testfile-1-n.sml
14.5 + Author: Walther Neuper 110320
14.6 + (c) copyright due to lincense terms.
14.7 +*)
14.8 +
14.9 +"======= test-depend/testdir1/testfile-1-n.sml ===";
14.10 +"========= content testfile-1-n.sml ==============";
14.11 +
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testdirm.thy Wed Apr 06 18:01:02 2011 +0200
15.3 @@ -0,0 +1,18 @@
15.4 +(* Title: test/../test-depend/testdirm/testdirm.thy
15.5 + Author: Walther Neuper 110320
15.6 + (c) copyright due to lincense terms.
15.7 +*)
15.8 +
15.9 +header {* collect all testfiles in directory testdirm/ *}
15.10 +
15.11 +theory testdirm
15.12 +imports Main
15.13 +uses ("testfile-m-1.sml")("testfile-m-n.sml")
15.14 +begin
15.15 +
15.16 + ML {*"===== test-depend/testdir1/testdir1.thy ========="*}
15.17 + use "testfile-m-1.sml"
15.18 + use "testfile-m-n.sml"
15.19 +
15.20 +end
15.21 +
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testfile-m-1.sml Wed Apr 06 18:01:02 2011 +0200
16.3 @@ -0,0 +1,8 @@
16.4 +(* Title: test/../test-depend/testdir1/testfile-m-1.sml
16.5 + Author: Walther Neuper 110320
16.6 + (c) copyright due to lincense terms.
16.7 +*)
16.8 +
16.9 +"======= test-depend/testdirm/testfile-m-1.sml ===";
16.10 +"========= content testfile-m-1.sml ==============";
16.11 +
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/test/Tools/isac/ADDTESTS/test-depend/testdirm/testfile-m-n.sml Wed Apr 06 18:01:02 2011 +0200
17.3 @@ -0,0 +1,8 @@
17.4 +(* Title: test/../test-depend/testdir1/testfile-m-n.sml
17.5 + Author: Walther Neuper 110320
17.6 + (c) copyright due to lincense terms.
17.7 +*)
17.8 +
17.9 +"======= test-depend/testdirm/testfile-m-n.sml ===";
17.10 +"========= content testfile-m-n.sml ==============";
17.11 +
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/test/Tools/isac/Frontend/messages.sml Wed Apr 06 18:01:02 2011 +0200
18.3 @@ -0,0 +1,4 @@
18.4 +(* Title: test/../messages.sml
18.5 + Author: Walther Neuper 110320
18.6 + (c) copyright due to lincense terms.
18.7 +*)
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/test/Tools/isac/Frontend/states.sml Wed Apr 06 18:01:02 2011 +0200
19.3 @@ -0,0 +1,4 @@
19.4 +(* Title: test/../states.sml
19.5 + Author: Walther Neuper 110320
19.6 + (c) copyright due to lincense terms.
19.7 +*)
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/test/Tools/isac/Interpret/appl.sml Wed Apr 06 18:01:02 2011 +0200
20.3 @@ -0,0 +1,4 @@
20.4 +(* Title: test/../appl.sml
20.5 + Author: Walther Neuper 110320
20.6 + (c) copyright due to lincense terms.
20.7 +*)
21.1 --- a/test/Tools/isac/Interpret/ctree.sml Mon Apr 04 11:05:07 2011 +0200
21.2 +++ b/test/Tools/isac/Interpret/ctree.sml Wed Apr 06 18:01:02 2011 +0200
21.3 @@ -64,17 +64,17 @@
21.4 "this build should be detailed each time a test fails later \
21.5 \i.e. all the tests should be caught here first \
21.6 \and linked with a reference to the respective test environment";
21.7 -val fmz = ["equality (x+1=(2::int))",
21.8 - "solveFor (x::int)","solutions L"];
21.9 +val fmz = ["equality (x + 1 = (2::int))",
21.10 + "solveFor x","solutions L"];
21.11 val (dI',pI',mI') =
21.12 ("Test",["sqroot-test","univariate","equation","test"],
21.13 ["Test","squ-equ-test-subpbl1"]);
21.14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
21.15 -val (p,_,f,(nxt,tacx),_,pt) = me nxt p [1] pt;
21.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (* error happens here *)
21.17 (* nxt = Add_Given "equality (x + 1 = 2)"
21.18 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
21.19 *)
21.20 -val (p,_,f,nxt,_,pt) = me (nxt,tacx) p [1] pt;
21.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
21.22 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
21.23 *)
21.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/test/Tools/isac/Interpret/generate.sml Wed Apr 06 18:01:02 2011 +0200
22.3 @@ -0,0 +1,4 @@
22.4 +(* Title: test/../generate.sml
22.5 + Author: Walther Neuper 110320
22.6 + (c) copyright due to lincense terms.
22.7 +*)
23.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Apr 04 11:05:07 2011 +0200
23.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Wed Apr 06 18:01:02 2011 +0200
23.3 @@ -132,9 +132,9 @@
23.4 "----- appendFormula TODO: first repair error";
23.5 val cs = ((pt,p),[]);
23.6 val ("ok", cs' as (_,_,(pt,p))) = step p cs;
23.7 - val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2"; val encode = I;
23.8 + val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
23.9 (*
23.10 - val ("no derivation found", (_,_,(pt, p))) = inform cs' (encode ifo);
23.11 + val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
23.12 here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
23.13 *)
23.14
24.1 --- a/test/Tools/isac/Knowledge/Isac.thy Mon Apr 04 11:05:07 2011 +0200
24.2 +++ b/test/Tools/isac/Knowledge/Isac.thy Wed Apr 06 18:01:02 2011 +0200
24.3 @@ -6,7 +6,12 @@
24.4 10 20 30 40 50 60 70 80
24.5 *)
24.6
24.7 -theory Isac imports Complex_Main (*TODO Build_Isac*) begin
24.8 +(*WN110319 theory Isac imports Complex_Main (*TODO Build_Isac*) begin*)
24.9 +theory isac imports Isac
24.10 +imports "Frontend/Frontend"
24.11 + PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*) DiophantEq Test
24.12 +begin
24.13 +
24.14
24.15 text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;
24.16 the leading parts of longnames can be dropped with some exceptions. *}
25.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Apr 04 11:05:07 2011 +0200
25.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Apr 06 18:01:02 2011 +0200
25.3 @@ -5,7 +5,6 @@
25.4 use"../smltest/IsacKnowledge/algein.sml";
25.5 use"algein.sml";
25.6 *)
25.7 -val thy = AlgEin.thy;
25.8
25.9 "-----------------------------------------------------------------";
25.10 "table of contents -----------------------------------------------";
25.11 @@ -18,6 +17,8 @@
25.12 "-----------------------------------------------------------------";
25.13 "-----------------------------------------------------------------";
25.14
25.15 +(*=== inhibit exn ?=============================================================
25.16 +val thy = AlgEin.thy;
25.17
25.18
25.19 (* use"../smltest/IsacKnowledge/algein.sml";
25.20 @@ -156,3 +157,4 @@
25.21 (* use"../smltest/IsacKnowledge/algein.sml";
25.22 *)
25.23
25.24 +===== inhibit exn ?===========================================================*)
26.1 --- a/test/Tools/isac/Knowledge/atools.sml Mon Apr 04 11:05:07 2011 +0200
26.2 +++ b/test/Tools/isac/Knowledge/atools.sml Wed Apr 06 18:01:02 2011 +0200
26.3 @@ -7,16 +7,18 @@
26.4 use"atools.sml";
26.5 *)
26.6
26.7 -"-----------------------------------------------------------------";
26.8 -"table of contents -----------------------------------------------";
26.9 -"-----------------------------------------------------------------";
26.10 -"----------- occurs_in -------------------------------------------";
26.11 -"----------- argument_of -----------------------------------------";
26.12 -"----------- sameFunId -------------------------------------------";
26.13 -"----------- filter_sameFunId ------------------------------------";
26.14 -"----------- boollist2sum ----------------------------------------";
26.15 -"-----------------------------------------------------------------";
26.16 +"--------------------------------------------------------";
26.17 +"table of contents --------------------------------------";
26.18 +"--------------------------------------------------------";
26.19 +"----------- occurs_in ----------------------------------";
26.20 +"----------- argument_of --------------------------------";
26.21 +"----------- sameFunId ----------------------------------";
26.22 +"----------- filter_sameFunId ---------------------------";
26.23 +"----------- boollist2sum -------------------------------";
26.24 +"----------- termorder (<-- termorder.sml) --------------";
26.25 +"--------------------------------------------------------";
26.26
26.27 +(*=== inhibit exn ?=============================================================
26.28
26.29 val thy = Atools.thy;
26.30
26.31 @@ -126,6 +128,199 @@
26.32 trace_rewrite:=false;
26.33
26.34
26.35 -(* use"IsacKnowledge/Atools.ML";
26.36 - use"../smltest/IsacKnowledge/atools.sml";
26.37 - *)
26.38 \ No newline at end of file
26.39 +"----------- termorder (<-- termorder.sml) --------------";
26.40 +"----------- termorder (<-- termorder.sml) --------------";
26.41 +"----------- termorder (<-- termorder.sml) --------------";
26.42 + (* tests on rewrite orders
26.43 + author Matthias Goldgruber 2003
26.44 +
26.45 + WN0509 do not use this file anymore, since orders require thy:
26.46 + do tests in the smltest/IsacKnowledge/file.sml
26.47 + where file.ML defines the respective order !
26.48 +
26.49 +use"../smltest/IsacKnowledge/termorder.sml";
26.50 +*)
26.51 +
26.52 +
26.53 + (*MK die ersten Tests*)
26.54 + val substa = [(e_term, (term_of o the o (parse thy)) "a")];
26.55 + val substb = [(e_term, (term_of o the o (parse thy)) "b")];
26.56 + val substx = [(e_term, (term_of o the o (parse thy)) "x")];
26.57 +
26.58 + val x1 = (term_of o the o (parse thy)) "a + b + x";
26.59 + val x2 = (term_of o the o (parse thy)) "a + x + b";
26.60 + val x3 = (term_of o the o (parse thy)) "a + x + b";
26.61 + val x4 = (term_of o the o (parse thy)) "x + a + b";
26.62 +
26.63 +if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
26.64 +else error "termorder.sml diff.behav ord_make_polynomial_in #1";
26.65 +
26.66 +if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
26.67 +else error "termorder.sml diff.behav ord_make_polynomial_in #2";
26.68 +
26.69 +if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
26.70 +else error "termorder.sml diff.behav ord_make_polynomial_in #3";
26.71 +
26.72 + val aa = (term_of o the o (parse thy)) "-1 * a * x";
26.73 + val bb = (term_of o the o (parse thy)) "x^^^3";
26.74 + ord_make_polynomial_in true thy substx (aa, bb);
26.75 + true; (* => LESS *)
26.76 +
26.77 + val aa = (term_of o the o (parse thy)) "-1 * a * x";
26.78 + val bb = (term_of o the o (parse thy)) "x^^^3";
26.79 + ord_make_polynomial_in true thy substa (aa, bb);
26.80 + false; (* => GREATER *)
26.81 +
26.82 + (*und nach dem Re-engineering der Termorders in den 'rulesets'
26.83 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
26.84 + val bdv= (term_of o the o (parse thy)) "bdv";
26.85 + val x = (term_of o the o (parse thy)) "x";
26.86 + val a = (term_of o the o (parse thy)) "a";
26.87 + val b = (term_of o the o (parse thy)) "b";
26.88 + val SOME (t',_) =
26.89 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
26.90 +if term2str t' = "b + x + a" then ()
26.91 +else error "termorder.sml diff.behav ord_make_polynomial_in #11";
26.92 +
26.93 + val NONE =
26.94 + rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
26.95 + term2str t';
26.96 + "a + x + b";
26.97 +
26.98 + val SOME (t',_) =
26.99 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
26.100 +if term2str t' = "a + b + x" then ()
26.101 +else error "termorder.sml diff.behav ord_make_polynomial_in #13";
26.102 +
26.103 +
26.104 +
26.105 + val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
26.106 + val ppp = (term_of o the o (parse thy)) ppp';
26.107 + val SOME (t',_) =
26.108 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
26.109 +(*MG 2003...
26.110 + term2str t';
26.111 + "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
26.112 +if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
26.113 +else error "termorder.sml diff.behav ord_make_polynomial_in #14";
26.114 +
26.115 + val SOME (t',_) =
26.116 + rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
26.117 +(*MG 2003...
26.118 + "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
26.119 +if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
26.120 +else error "termorder.sml diff.behav ord_make_polynomial_in #15";
26.121 +
26.122 + val ttt' = "(3*x + 5)/18";
26.123 + val ttt = (term_of o the o (parse thy)) ttt';
26.124 + val SOME (uuu,_) =
26.125 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
26.126 +if term2str uuu = "(5 + 3 * x) / 18" then ()
26.127 +else error "termorder.sml diff.behav ord_make_polynomial_in #16";
26.128 +
26.129 + val SOME (uuu,_) =
26.130 + rewrite_set_ thy false make_polynomial ttt;
26.131 +if term2str uuu = "(5 + 3 * x) / 18" then ()
26.132 +else error "termorder.sml diff.behav ord_make_polynomial_in #16";
26.133 +
26.134 +
26.135 +
26.136 +
26.137 +(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
26.138 +
26.139 + (*Aufgabe zum Einstieg in die Arbeit...*)
26.140 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
26.141 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
26.142 + val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
26.143 + term2str t;
26.144 + "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
26.145 + val SOME (t,_) =
26.146 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
26.147 + term2str t;
26.148 + "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
26.149 +(* bei Verwendung von "size_of-term" nach MG :*)
26.150 +(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
26.151 +
26.152 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
26.153 + val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
26.154 + term2str t;
26.155 + "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
26.156 +(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
26.157 +
26.158 + val SOME (t,_) =
26.159 + rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
26.160 + term2str t;
26.161 + "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
26.162 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
26.163 + "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
26.164 +
26.165 + (*das rewriting l"asst sich beobachten mit
26.166 + trace_rewrite:=true;
26.167 + *)
26.168 +
26.169 +
26.170 +
26.171 +"------15.11.02 --------------------------";
26.172 + val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
26.173 + val bdv = (term_of o the o (parse thy)) "bdv";
26.174 + val a = (term_of o the o (parse thy)) "a";
26.175 +
26.176 + trace_rewrite:=true;
26.177 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
26.178 + val SOME (t,_) =
26.179 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.180 + term2str t;
26.181 + val SOME (t,_) =
26.182 + rewrite_set_ thy false discard_parentheses t;
26.183 + term2str t;
26.184 +"1 + b * x + x * a";
26.185 +
26.186 + val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
26.187 + val SOME (t,_) =
26.188 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.189 + term2str t;
26.190 + val SOME (t,_) =
26.191 + rewrite_set_ thy false discard_parentheses t;
26.192 + term2str t;
26.193 +"1 + (x + b * x) * a + a ^^^ 2";
26.194 +
26.195 + val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
26.196 + val SOME (t,_) =
26.197 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.198 + term2str t;
26.199 + val SOME (t,_) =
26.200 + rewrite_set_ thy false discard_parentheses t;
26.201 + term2str t;
26.202 +"1 + b * a + (7 + x) * a ^^^ 2";
26.203 +
26.204 +(* MG2003
26.205 + Atools.thy grundlegende Algebra
26.206 + Poly.thy Polynome
26.207 + Rational.thy Br"uche
26.208 + Root.thy Wurzeln
26.209 + RootRat.thy Wurzen + Br"uche
26.210 + Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
26.211 +
26.212 + cd"knowledge";
26.213 + remove_thy"Termorder";
26.214 + use_thy"Isac";
26.215 +
26.216 + get_thm Termorder.thy "bdv_n_collect";
26.217 + get_thm (theory "Isac") "bdv_n_collect";
26.218 +
26.219 +*)
26.220 + val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
26.221 + val SOME (t,_) =
26.222 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
26.223 + term2str t;
26.224 + val SOME (t,_) =
26.225 + rewrite_set_ thy false discard_parentheses t;
26.226 + term2str t;
26.227 +"(7 + x) * a ^^^ 2";
26.228 +
26.229 + val t = (term_of o the o (parse Termorder.thy)) "Pi";
26.230 +
26.231 + val t = (term_of o the o (parseold thy)) "7";
26.232 +
26.233 +----------------------------------------------------------------------*)
26.234 +===== inhibit exn ?===========================================================*)
27.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Mon Apr 04 11:05:07 2011 +0200
27.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Apr 06 18:01:02 2011 +0200
27.3 @@ -5,7 +5,6 @@
27.4 use"../smltest/IsacKnowledge/biegelinie.sml";
27.5 use"biegelinie.sml";
27.6 *)
27.7 -val thy = Biegelinie.thy;
27.8
27.9 "-----------------------------------------------------------------";
27.10 "table of contents -----------------------------------------------";
27.11 @@ -26,6 +25,8 @@
27.12 "-----------------------------------------------------------------";
27.13 "-----------------------------------------------------------------";
27.14
27.15 +(*=== inhibit exn ?=============================================================
27.16 +val thy = Biegelinie.thy;
27.17
27.18 "----------- the rules -------------------------------------------";
27.19 "----------- the rules -------------------------------------------";
27.20 @@ -1038,3 +1039,5 @@
27.21 (*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
27.22
27.23 "----- functions comming from:";
27.24 +
27.25 +===== inhibit exn ?===========================================================*)
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/test/Tools/isac/Knowledge/calculus.sml Wed Apr 06 18:01:02 2011 +0200
28.3 @@ -0,0 +1,4 @@
28.4 +(* Title: test/../calculus.sml
28.5 + Author: Walther Neuper 110320
28.6 + (c) copyright due to lincense terms.
28.7 +*)
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/test/Tools/isac/Knowledge/delete.sml Wed Apr 06 18:01:02 2011 +0200
29.3 @@ -0,0 +1,4 @@
29.4 +(* Title: test/../delete.sml
29.5 + Author: Walther Neuper 110320
29.6 + (c) copyright due to lincense terms.
29.7 +*)
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/test/Tools/isac/Knowledge/descript.sml Wed Apr 06 18:01:02 2011 +0200
30.3 @@ -0,0 +1,4 @@
30.4 +(* Title: test/../descript.sml
30.5 + Author: Walther Neuper 110320
30.6 + (c) copyright due to lincense terms.
30.7 +*)
31.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Mon Apr 04 11:05:07 2011 +0200
31.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 06 18:01:02 2011 +0200
31.3 @@ -20,6 +20,7 @@
31.4 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
31.5
31.6
31.7 +(*=== inhibit exn ?=============================================================
31.8
31.9
31.10
31.11 @@ -750,3 +751,4 @@
31.12
31.13
31.14
31.15 +===== inhibit exn ?===========================================================*)
32.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Apr 04 11:05:07 2011 +0200
32.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 06 18:01:02 2011 +0200
32.3 @@ -6,7 +6,6 @@
32.4 use"../smltest/IsacKnowledge/eqsystem.sml";
32.5 use"eqsystem.sml";
32.6 *)
32.7 -val thy = EqSystem.thy;
32.8
32.9 "-----------------------------------------------------------------";
32.10 "table of contents -----------------------------------------------";
32.11 @@ -31,6 +30,8 @@
32.12 "-----------------------------------------------------------------";
32.13 "-----------------------------------------------------------------";
32.14
32.15 +(*=== inhibit exn ?=============================================================
32.16 +val thy = EqSystem.thy;
32.17
32.18 "----------- occur_exactly_in ------------------------------------";
32.19 "----------- occur_exactly_in ------------------------------------";
32.20 @@ -1443,3 +1444,4 @@
32.21 use"../smltest/IsacKnowledge/eqsystem.sml";
32.22 use"eqsystem.sml";
32.23 *)
32.24 +===== inhibit exn ?===========================================================*)
33.1 --- a/test/Tools/isac/Knowledge/equation.sml Mon Apr 04 11:05:07 2011 +0200
33.2 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Apr 06 18:01:02 2011 +0200
33.3 @@ -1,12 +1,7 @@
33.4 (* tests on the equation solver
33.5 - author: Walther Neuper
33.6 - 070703
33.7 + author: Walther Neuper 070703
33.8 (c) due to copyright terms
33.9 -
33.10 -use"../smltest/IsacKnowledge/equation.sml";
33.11 -use"equation.sml";
33.12 *)
33.13 -val thy = (theory "Isac");
33.14
33.15 "-----------------------------------------------------------------";
33.16 "table of contents -----------------------------------------------";
33.17 @@ -16,6 +11,8 @@
33.18 "-----------------------------------------------------------------";
33.19 "-----------------------------------------------------------------";
33.20
33.21 +(*=== inhibit exn ?=============================================================
33.22 +val thy = (theory "Isac");
33.23
33.24 "----------- CAS input -------------------------------------------";
33.25 "----------- CAS input -------------------------------------------";
33.26 @@ -31,3 +28,4 @@
33.27 show_pt pt;
33.28 if p = ([], Res) andalso term2str res = "[x = 1]" then ()
33.29 else error "equation.sml behav.changed for CAS solve (x+1=2, x))";
33.30 +===== inhibit exn ?===========================================================*)
34.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
34.2 +++ b/test/Tools/isac/Knowledge/lineq.sml Wed Apr 06 18:01:02 2011 +0200
34.3 @@ -0,0 +1,4 @@
34.4 +(* Title: test/../lineq.sml
34.5 + Author: Walther Neuper 110320
34.6 + (c) copyright due to lincense terms.
34.7 +*)
35.1 --- a/test/Tools/isac/Knowledge/logexp.sml Mon Apr 04 11:05:07 2011 +0200
35.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed Apr 06 18:01:02 2011 +0200
35.3 @@ -3,7 +3,6 @@
35.4 use"../smltest/IsacKnowledge/logexp.sml";
35.5 *)
35.6
35.7 -val thy = LogExp.thy;
35.8 "-----------------------------------------------------------------";
35.9 "table of contents -----------------------------------------------";
35.10 "-----------------------------------------------------------------";
35.11 @@ -12,6 +11,8 @@
35.12 "-----------------------------------------------------------------";
35.13 "-----------------------------------------------------------------";
35.14
35.15 +(*=== inhibit exn ?=============================================================
35.16 +val thy = LogExp.thy;
35.17
35.18 "----------- setup presentation innsbruck ------------------------";
35.19 "----------- setup presentation innsbruck ------------------------";
35.20 @@ -59,3 +60,4 @@
35.21 show_pt pt;
35.22
35.23 *-------------------------------------------------------------------*)
35.24 +===== inhibit exn ?===========================================================*)
36.1 --- a/test/Tools/isac/Knowledge/poly.sml Mon Apr 04 11:05:07 2011 +0200
36.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Apr 06 18:01:02 2011 +0200
36.3 @@ -29,6 +29,7 @@
36.4 "--------------------------------------------------------";
36.5 "--------------------------------------------------------";
36.6
36.7 +(*=== inhibit exn ?=============================================================
36.8
36.9 "-------- check is'_polyexp is_polyexp ------------------";
36.10 "-------- check is'_polyexp is_polyexp ------------------";
36.11 @@ -557,4 +558,5 @@
36.12 val t1 = str2term "2 * b + (3 * a + 3 * b)";
36.13 val t2 = str2term "3 * a + (2 * b + 3 * b)";
36.14
36.15 +===== inhibit exn ============================================================*)
36.16 ===== inhibit exn ?===========================================================*)
37.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Mon Apr 04 11:05:07 2011 +0200
37.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Apr 06 18:01:02 2011 +0200
37.3 @@ -28,6 +28,8 @@
37.4 "-----------------------------------------------------------------";
37.5 "-----------------------------------------------------------------";
37.6
37.7 +(*=== inhibit exn ?=============================================================
37.8 +
37.9 val c = [];
37.10
37.11 "----------- tests on predicates in problems ---------------------";
37.12 @@ -1176,3 +1178,4 @@
37.13 val ((pt,p),_) = get_calc 1; show_pt pt;
37.14
37.15 interSteps 1 ([1],Res) (*no Rewrite_Set...*);
37.16 +===== inhibit exn ?===========================================================*)
38.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Apr 04 11:05:07 2011 +0200
38.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Apr 06 18:01:02 2011 +0200
38.3 @@ -11,6 +11,8 @@
38.4 "---------(1/x=5) ---------------------";
38.5 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
38.6
38.7 +(*=== inhibit exn ?=============================================================
38.8 +
38.9 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
38.10 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
38.11 val result = term2str t_;
38.12 @@ -143,3 +145,5 @@
38.13 else error "rateq.sml: new behaviour: [x = -2, x = 10]";
38.14
38.15 "----------- rateq.sml end--------";
38.16 +
38.17 +===== inhibit exn ?===========================================================*)
39.1 --- a/test/Tools/isac/Knowledge/root.sml Mon Apr 04 11:05:07 2011 +0200
39.2 +++ b/test/Tools/isac/Knowledge/root.sml Wed Apr 06 18:01:02 2011 +0200
39.3 @@ -1,5 +1,15 @@
39.4 -(* testexamples for Root, radicals
39.5 - *)
39.6 +(* Title: testexamples for Root, radicals
39.7 + Author: Walther Neuper
39.8 + (c) due to copyright terms
39.9 + *)
39.10 +"--------------------------------------------------------";
39.11 +"table of contents --------------------------------------";
39.12 +"--------------------------------------------------------";
39.13 +"----------- TODO ---------------------------------------";
39.14 +"--------------------------------------------------------";
39.15 +"--------------------------------------------------------";
39.16 +
39.17 +(*=== inhibit exn ?=============================================================
39.18
39.19 val thy = Root.thy;
39.20
39.21 @@ -13,3 +23,4 @@
39.22 val SOME (t',_) = rewrite_set_ thy false Root_erls t;
39.23 term2str t';
39.24 if term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1";
39.25 +===== inhibit exn ?===========================================================*)
40.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Mon Apr 04 11:05:07 2011 +0200
40.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Apr 06 18:01:02 2011 +0200
40.3 @@ -14,6 +14,9 @@
40.4 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
40.5 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
40.6 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
40.7 +"--------------------------------------------------------";
40.8 +
40.9 +(*=== inhibit exn ?=============================================================
40.10
40.11 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
40.12 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
40.13 @@ -468,3 +471,4 @@
40.14 "----------- rooteq.sml end--------";
40.15
40.16
40.17 +===== inhibit exn ?===========================================================*)
41.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Apr 04 11:05:07 2011 +0200
41.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Apr 06 18:01:02 2011 +0200
41.3 @@ -2,11 +2,15 @@
41.4 use"rootrateq.sml";
41.5 *)
41.6
41.7 +
41.8 +"--------------------- tests on predicates -------------------------------";
41.9 +"--------------------- tests on predicates -------------------------------";
41.10 +"--------------------- tests on predicates -------------------------------";
41.11 +
41.12 +(*=== inhibit exn ?=============================================================
41.13 +
41.14 val thy = (theory "Isac");
41.15
41.16 -"--------------------- tests on predicates -------------------------------";
41.17 -"--------------------- tests on predicates -------------------------------";
41.18 -"--------------------- tests on predicates -------------------------------";
41.19 (*
41.20 Compiler.Control.Print.printDepth:=5; (*4 default*)
41.21 trace_rewrite:=true;
41.22 @@ -227,3 +231,4 @@
41.23 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
41.24 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
41.25 | _ => error "rootrateq.sml: diff.behav. in 3/(1+sqrt(x))= 1 -> [x = 4]";
41.26 +===== inhibit exn ?===========================================================*)
42.1 --- a/test/Tools/isac/Knowledge/termorder.sml Mon Apr 04 11:05:07 2011 +0200
42.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
42.3 @@ -1,192 +0,0 @@
42.4 - (* tests on rewrite orders
42.5 - author Matthias Goldgruber 2003
42.6 -
42.7 - WN0509 do not use this file anymore, since orders require thy:
42.8 - do tests in the smltest/IsacKnowledge/file.sml
42.9 - where file.ML defines the respective order !
42.10 -
42.11 -use"../smltest/IsacKnowledge/termorder.sml";
42.12 -*)
42.13 -
42.14 -
42.15 - (*MK die ersten Tests*)
42.16 - val substa = [(e_term, (term_of o the o (parse thy)) "a")];
42.17 - val substb = [(e_term, (term_of o the o (parse thy)) "b")];
42.18 - val substx = [(e_term, (term_of o the o (parse thy)) "x")];
42.19 -
42.20 - val x1 = (term_of o the o (parse thy)) "a + b + x";
42.21 - val x2 = (term_of o the o (parse thy)) "a + x + b";
42.22 - val x3 = (term_of o the o (parse thy)) "a + x + b";
42.23 - val x4 = (term_of o the o (parse thy)) "x + a + b";
42.24 -
42.25 -if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()
42.26 -else error "termorder.sml diff.behav ord_make_polynomial_in #1";
42.27 -
42.28 -if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()
42.29 -else error "termorder.sml diff.behav ord_make_polynomial_in #2";
42.30 -
42.31 -if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()
42.32 -else error "termorder.sml diff.behav ord_make_polynomial_in #3";
42.33 -
42.34 - val aa = (term_of o the o (parse thy)) "-1 * a * x";
42.35 - val bb = (term_of o the o (parse thy)) "x^^^3";
42.36 - ord_make_polynomial_in true thy substx (aa, bb);
42.37 - true; (* => LESS *)
42.38 -
42.39 - val aa = (term_of o the o (parse thy)) "-1 * a * x";
42.40 - val bb = (term_of o the o (parse thy)) "x^^^3";
42.41 - ord_make_polynomial_in true thy substa (aa, bb);
42.42 - false; (* => GREATER *)
42.43 -
42.44 - (*und nach dem Re-engineering der Termorders in den 'rulesets'
42.45 - kannst Du die 'gr"osste' Variable frei w"ahlen: *)
42.46 - val bdv= (term_of o the o (parse thy)) "bdv";
42.47 - val x = (term_of o the o (parse thy)) "x";
42.48 - val a = (term_of o the o (parse thy)) "a";
42.49 - val b = (term_of o the o (parse thy)) "b";
42.50 - val SOME (t',_) =
42.51 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
42.52 -if term2str t' = "b + x + a" then ()
42.53 -else error "termorder.sml diff.behav ord_make_polynomial_in #11";
42.54 -
42.55 - val NONE =
42.56 - rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
42.57 - term2str t';
42.58 - "a + x + b";
42.59 -
42.60 - val SOME (t',_) =
42.61 - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
42.62 -if term2str t' = "a + b + x" then ()
42.63 -else error "termorder.sml diff.behav ord_make_polynomial_in #13";
42.64 -
42.65 -
42.66 -
42.67 - val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
42.68 - val ppp = (term_of o the o (parse thy)) ppp';
42.69 - val SOME (t',_) =
42.70 - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
42.71 -(*MG 2003...
42.72 - term2str t';
42.73 - "(-6) + (-5 * x + (-15 * x ^^^ 2))";*)
42.74 -if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
42.75 -else error "termorder.sml diff.behav ord_make_polynomial_in #14";
42.76 -
42.77 - val SOME (t',_) =
42.78 - rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';
42.79 -(*MG 2003...
42.80 - "(-6) + (-5 * x + (-15) * x ^^^ 2)";*)
42.81 -if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()
42.82 -else error "termorder.sml diff.behav ord_make_polynomial_in #15";
42.83 -
42.84 - val ttt' = "(3*x + 5)/18";
42.85 - val ttt = (term_of o the o (parse thy)) ttt';
42.86 - val SOME (uuu,_) =
42.87 - rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
42.88 -if term2str uuu = "(5 + 3 * x) / 18" then ()
42.89 -else error "termorder.sml diff.behav ord_make_polynomial_in #16";
42.90 -
42.91 - val SOME (uuu,_) =
42.92 - rewrite_set_ thy false make_polynomial ttt;
42.93 -if term2str uuu = "(5 + 3 * x) / 18" then ()
42.94 -else error "termorder.sml diff.behav ord_make_polynomial_in #16";
42.95 -
42.96 -
42.97 -
42.98 -
42.99 -(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
42.100 -
42.101 - (*Aufgabe zum Einstieg in die Arbeit...*)
42.102 - val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
42.103 - (*ein 'ruleset' aus Poly.ML wird angewandt...*)
42.104 - val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;
42.105 - term2str t;
42.106 - "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
42.107 - val SOME (t,_) =
42.108 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
42.109 - term2str t;
42.110 - "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
42.111 -(* bei Verwendung von "size_of-term" nach MG :*)
42.112 -(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
42.113 -
42.114 - (*wir holen 'a' wieder aus der Klammerung heraus...*)
42.115 - val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;
42.116 - term2str t;
42.117 - "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
42.118 -(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
42.119 -
42.120 - val SOME (t,_) =
42.121 - rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;
42.122 - term2str t;
42.123 - "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
42.124 - (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
42.125 - "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
42.126 -
42.127 - (*das rewriting l"asst sich beobachten mit
42.128 - trace_rewrite:=true;
42.129 - *)
42.130 -
42.131 -
42.132 -
42.133 -"------15.11.02 --------------------------";
42.134 - val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
42.135 - val bdv = (term_of o the o (parse thy)) "bdv";
42.136 - val a = (term_of o the o (parse thy)) "a";
42.137 -
42.138 - trace_rewrite:=true;
42.139 - (* Anwenden einer Regelmenge aus Termorder.ML: *)
42.140 - val SOME (t,_) =
42.141 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
42.142 - term2str t;
42.143 - val SOME (t,_) =
42.144 - rewrite_set_ thy false discard_parentheses t;
42.145 - term2str t;
42.146 -"1 + b * x + x * a";
42.147 -
42.148 - val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
42.149 - val SOME (t,_) =
42.150 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
42.151 - term2str t;
42.152 - val SOME (t,_) =
42.153 - rewrite_set_ thy false discard_parentheses t;
42.154 - term2str t;
42.155 -"1 + (x + b * x) * a + a ^^^ 2";
42.156 -
42.157 - val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
42.158 - val SOME (t,_) =
42.159 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
42.160 - term2str t;
42.161 - val SOME (t,_) =
42.162 - rewrite_set_ thy false discard_parentheses t;
42.163 - term2str t;
42.164 -"1 + b * a + (7 + x) * a ^^^ 2";
42.165 -
42.166 -(* MG2003
42.167 - Atools.thy grundlegende Algebra
42.168 - Poly.thy Polynome
42.169 - Rational.thy Br"uche
42.170 - Root.thy Wurzeln
42.171 - RootRat.thy Wurzen + Br"uche
42.172 - Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
42.173 -
42.174 - cd"knowledge";
42.175 - remove_thy"Termorder";
42.176 - use_thy"Isac";
42.177 -
42.178 - get_thm Termorder.thy "bdv_n_collect";
42.179 - get_thm (theory "Isac") "bdv_n_collect";
42.180 -
42.181 -*)
42.182 - val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
42.183 - val SOME (t,_) =
42.184 - rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
42.185 - term2str t;
42.186 - val SOME (t,_) =
42.187 - rewrite_set_ thy false discard_parentheses t;
42.188 - term2str t;
42.189 -"(7 + x) * a ^^^ 2";
42.190 -
42.191 - val t = (term_of o the o (parse Termorder.thy)) "Pi";
42.192 -
42.193 - val t = (term_of o the o (parseold thy)) "7";
42.194 -
42.195 -----------------------------------------------------------------------*)
43.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
43.2 +++ b/test/Tools/isac/Knowledge/test.sml Wed Apr 06 18:01:02 2011 +0200
43.3 @@ -0,0 +1,4 @@
43.4 +(* Title: test/../test.sml
43.5 + Author: Walther Neuper 110320
43.6 + (c) copyright due to lincense terms.
43.7 +*)
44.1 --- a/test/Tools/isac/Knowledge/trig.sml Mon Apr 04 11:05:07 2011 +0200
44.2 +++ b/test/Tools/isac/Knowledge/trig.sml Wed Apr 06 18:01:02 2011 +0200
44.3 @@ -1,2 +1,7 @@
44.4 (* testexamples for Trig, trigonometry
44.5 - *)
44.6 \ No newline at end of file
44.7 + *)
44.8 +"--------------------------------------------------------";
44.9 +"table of contents --------------------------------------";
44.10 +"--------------------------------------------------------";
44.11 +"----------- TODO ---------------------------------------";
44.12 +"--------------------------------------------------------";
45.1 --- a/test/Tools/isac/Knowledge/vect.sml Mon Apr 04 11:05:07 2011 +0200
45.2 +++ b/test/Tools/isac/Knowledge/vect.sml Wed Apr 06 18:01:02 2011 +0200
45.3 @@ -1,2 +1,7 @@
45.4 (* testexamples for Vect, vector spaces
45.5 - *)
45.6 \ No newline at end of file
45.7 + *)
45.8 +"--------------------------------------------------------";
45.9 +"table of contents --------------------------------------";
45.10 +"--------------------------------------------------------";
45.11 +"----------- TODO ---------------------------------------";
45.12 +"--------------------------------------------------------";
46.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Apr 04 11:05:07 2011 +0200
46.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Wed Apr 06 18:01:02 2011 +0200
46.3 @@ -23,6 +23,7 @@
46.4 "--------------------------------------------------------";
46.5 "--------------------------------------------------------";
46.6
46.7 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
46.8
46.9 "----------- assemble rewrite ---------------------------";
46.10 "----------- assemble rewrite ---------------------------";
46.11 @@ -54,7 +55,6 @@
46.12 (*lookup in isabelle?trace?response...*)
46.13 writeln(Syntax.string_of_term ctxt rew);
46.14 writeln(Syntax.string_of_term ctxt RHS);
46.15 -
46.16 "===== rewriting: prep insertion into rew_sub";
46.17 val thy = @{theory Complex_Main};
46.18 val ctxt = @{context};
46.19 @@ -504,7 +504,6 @@
46.20 scan_ chk prepat;
46.21 tracing "=== poly.sml: scan_ chk prepat end";
46.22
46.23 -
46.24 "----- chk ---";
46.25 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
46.26 val [(pres, pat)] = prepat;
46.27 @@ -524,5 +523,4 @@
46.28 ([], true) => ()
46.29 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
46.30
46.31 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
46.32 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
47.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
47.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 06 18:01:02 2011 +0200
47.3 @@ -0,0 +1,157 @@
47.4 +(* Title: All tests on isac; observe outcommented
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 -l Isac Test_Isac.thy &
47.10 +*)
47.11 +
47.12 +theory Test_Isac imports Isac
47.13 +uses
47.14 + ( "library.sml")
47.15 + ( "calcelems.sml")
47.16 + ("ProgLang/termC.sml")
47.17 + ("ProgLang/calculate.sml")
47.18 + ("ProgLang/rewrite.sml")
47.19 +(*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
47.20 +
47.21 + ("Interpret/mstools.sml")
47.22 +(*("Interpret/ctree.sml")*)
47.23 + ("Interpret/ptyps.sml")
47.24 +(*("Interpret/generate.sml")*)
47.25 + ("Interpret/calchead.sml")
47.26 +(*("Interpret/appl.sml")*)
47.27 + ("Interpret/rewtools.sml")
47.28 +(*("Interpret/script.sml")
47.29 + ("Interpret/solve.sml")
47.30 + ("Interpret/inform.sml")*)
47.31 + ("Interpret/mathengine.sml")
47.32 +
47.33 +(*("xmlsrc/mathml.sml")
47.34 + ("xmlsrc/datatypes.sml")
47.35 + ("xmlsrc/pbl-met-hierarchy.sml")
47.36 + ("xmlsrc/thy-hierarchy.sml")*)
47.37 + ("xmlsrc/interface-xml.sml")
47.38 +
47.39 + ("Frontend/messages.sml")
47.40 + ("Frontend/states.sml")
47.41 + ("Frontend/interface.sml")
47.42 + ("print_exn_G.sml")
47.43 +
47.44 + ("Knowledge/delete.sml")
47.45 + ("Knowledge/descript.sml")
47.46 + ("Knowledge/atools.sml")
47.47 + ("Knowledge/simplify.sml")
47.48 + ("Knowledge/poly.sml")
47.49 + ("Knowledge/rational.sml")
47.50 + ("Knowledge/equation.sml")
47.51 + ("Knowledge/root.sml")
47.52 + ("Knowledge/lineq.sml")
47.53 + ("Knowledge/rooteq.sml")
47.54 + ("Knowledge/rateq.sml")
47.55 + ("Knowledge/rootrateq.sml")
47.56 +(*("Knowledge/polyeq.sml")*)
47.57 + ("Knowledge/calculus.sml")
47.58 + ("Knowledge/trig.sml")
47.59 + ("Knowledge/logexp.sml")
47.60 + ("Knowledge/diff.sml")
47.61 + ("Knowledge/integrate.sml")
47.62 + ("Knowledge/eqsystem.sml")
47.63 + ("Knowledge/test.sml")
47.64 + ("Knowledge/polyminus.sml")
47.65 + ("Knowledge/vect.sml")
47.66 + ("Knowledge/diffapp.sml")
47.67 + ("Knowledge/biegelinie.sml")
47.68 + ("Knowledge/algein.sml")
47.69 + ("Knowledge/diophanteq.sml")
47.70 + ("Knowledge/isac.sml")
47.71 +
47.72 +
47.73 +begin
47.74 +
47.75 + ML {*print_depth 100*}
47.76 + ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
47.77 + use "library.sml" (*new 2011*)
47.78 + use "calcelems.sml" (*complete*)
47.79 + use "ProgLang/termC.sml" (*part.*)
47.80 + use "ProgLang/calculate.sml" (*part.*)
47.81 + use "ProgLang/rewrite.sml" (*part.*)
47.82 +(*use "ProgLang/listg.sml" 2002*)
47.83 +(*use "ProgLang/scrtools.sml" 2002*)
47.84 +(*use "ProgLang/tools.sml" 2002*)
47.85 + ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
47.86 + ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
47.87 + use "Interpret/mstools.sml" (*empty*)
47.88 +(*use "Interpret/ctree.sml" TODO*)
47.89 + use "Interpret/ptyps.sml" (* *)
47.90 +(*use "Interpret/generate.sml" new 2011*)
47.91 + use "Interpret/calchead.sml" (* *)
47.92 +(*use "Interpret/appl.sml" new 2011*)
47.93 + use "Interpret/rewtools.sml" (* *)
47.94 +(*use "Interpret/script.sml" TODO*)
47.95 +(*use "Interpret/solve.sml" TODO*)
47.96 +(*use "Interpret/inform.sml" TODO*)
47.97 + use "Interpret/mathengine.sml"(*part.*)
47.98 + ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
47.99 + ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
47.100 +(*use "xmlsrc/mathml.sml" TODO*)
47.101 +(*use "xmlsrc/datatypes.sml" TODO*)
47.102 +(*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
47.103 +(*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
47.104 + use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
47.105 + ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
47.106 + ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
47.107 + use "Frontend/messages.sml" (*new 2011*)
47.108 + use "Frontend/states.sml" (*new 2011*)
47.109 + use "Frontend/interface.sml" (*part.*)
47.110 + use "print_exn_G.sml" (*new 2011*)
47.111 + ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
47.112 + ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
47.113 + use "Knowledge/delete.sml" (*new 2011*)
47.114 + use "Knowledge/descript.sml" (*new 2011*)
47.115 +(*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
47.116 + use "Knowledge/simplify.sml" (*part.*)
47.117 +(*use "Knowledge/poly.sml" 2002*)
47.118 +(*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
47.119 +(*use "Knowledge/equation.sml" 2002*)
47.120 +(*use "Knowledge/root.sml" 2002*)
47.121 + use "Knowledge/lineq.sml" (*new 2011*)
47.122 +(*use "Knowledge/rooteq.sml" 2002*)
47.123 +(*use "Knowledge/rateq.sml" 2002*)
47.124 +(*use "Knowledge/rootrat.sml" 2002*)
47.125 +(*use "Knowledge/rootrateq.sml" 2002*)
47.126 +(*use "Knowledge/polyeq.sml" 2002*)
47.127 + use "Knowledge/calculus.sml" (*new 2011*)
47.128 +(*use "Knowledge/trig.sml" 2002*)
47.129 +(*use "Knowledge/logexp.sml" 2002*)
47.130 + use "Knowledge/diff.sml" (*part.*)
47.131 +(*use "Knowledge/integrate.sml" part. was complete 2009-2
47.132 + diff.emacs--jedit*)
47.133 +(*use "Knowledge/eqsystem.sml" 2002*)
47.134 + use "Knowledge/test.sml" (*new 2011*)
47.135 + use "Knowledge/polyminus.sml" (*part.*)
47.136 +(*use "Knowledge/vect.sml" 2002*)
47.137 +(*use "Knowledge/diffapp.sml" 2002*)
47.138 +(*use "Knowledge/biegelinie.sml" 2002*)
47.139 +(*use "Knowledge/algein.sml" 2002*)
47.140 + use "Knowledge/diophanteq.sml" (*complete*)
47.141 + use "Knowledge/isac.sml" (*part.*)
47.142 + ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
47.143 + ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
47.144 + ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
47.145 + ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
47.146 +
47.147 +end
47.148 +
47.149 +(*=== inhibit exn ?=============================================================
47.150 +===== inhibit exn ?===========================================================*)
47.151 +
47.152 +(*========== inhibit exn 110323 ================================================
47.153 +
47.154 +"########### testcode inserted vvv ###########################################";
47.155 +"########### testcode inserted ^^^ ###########################################";
47.156 +
47.157 +============ inhibit exn 110323 ==============================================*)
47.158 +
47.159 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
47.160 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
48.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
48.2 +++ b/test/Tools/isac/Test_Some.thy Wed Apr 06 18:01:02 2011 +0200
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 Mon Apr 04 11:05:07 2011 +0200
49.2 +++ b/test/Tools/isac/library.sml Wed Apr 06 18:01:02 2011 +0200
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 Apr 06 18:01:02 2011 +0200
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 Apr 06 18:01:02 2011 +0200
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 +*)