intermed. context integration
- prep_ori works with parseNEW
- unused thy function parameters removed
- thy parameter replaced by ctxt where useful
- appl_add adjusted and cleaned up - still uses parse due to error
- seek_oridts cleaned up
- split_dts cleaned up
1 (* Title: All tests on isac; observe outcommented
2 Author: Walther Neuper 101001
3 (c) copyright due to lincense terms.
5 $ cd /usr/local/isabisac/test/Tools/isac
6 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
9 theory Test_Isac imports Isac
13 ("ProgLang/termC.sml")
14 ("ProgLang/calculate.sml")
15 ("ProgLang/rewrite.sml")
16 (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
18 ("Interpret/mstools.sml")
19 ("Interpret/ctree.sml")
20 ("Interpret/ptyps.sml")
21 (*("Interpret/generate.sml")*)
22 ("Interpret/calchead.sml")
23 (*("Interpret/appl.sml")*)
24 ("Interpret/rewtools.sml")
25 (*("Interpret/script.sml")
26 ("Interpret/solve.sml")
27 ("Interpret/inform.sml")*)
28 ("Interpret/mathengine.sml")
30 (*("xmlsrc/mathml.sml")
31 ("xmlsrc/datatypes.sml")
32 ("xmlsrc/pbl-met-hierarchy.sml")
33 ("xmlsrc/thy-hierarchy.sml")*)
34 ("xmlsrc/interface-xml.sml")
36 ("Frontend/messages.sml")
37 ("Frontend/states.sml")
38 ("Frontend/interface.sml")
41 ("Knowledge/delete.sml")
42 ("Knowledge/descript.sml")
43 ("Knowledge/atools.sml")
44 ("Knowledge/simplify.sml")
45 ("Knowledge/poly.sml")
46 ("Knowledge/rational.sml")
47 ("Knowledge/equation.sml")
48 ("Knowledge/root.sml")
49 ("Knowledge/lineq.sml")
50 ("Knowledge/rooteq.sml")
51 ("Knowledge/rateq.sml")
52 ("Knowledge/rootrateq.sml")
53 (*("Knowledge/polyeq.sml")*)
54 ("Knowledge/calculus.sml")
55 ("Knowledge/trig.sml")
56 ("Knowledge/logexp.sml")
57 ("Knowledge/diff.sml")
58 ("Knowledge/integrate.sml")
59 ("Knowledge/eqsystem.sml")
60 ("Knowledge/test.sml")
61 ("Knowledge/polyminus.sml")
62 ("Knowledge/vect.sml")
63 ("Knowledge/diffapp.sml")
64 ("Knowledge/biegelinie.sml")
65 ("Knowledge/algein.sml")
66 ("Knowledge/diophanteq.sml")
67 ("Knowledge/isac.sml")
72 ML {*print_depth 100*}
73 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
74 use "library.sml" (*new 2011*)
75 use "calcelems.sml" (*complete*)
76 use "ProgLang/termC.sml" (*part.*)
77 use "ProgLang/calculate.sml" (*part.*)
78 use "ProgLang/rewrite.sml" (*part.*)
79 (*use "ProgLang/listg.sml" 2002*)
80 (*use "ProgLang/scrtools.sml" 2002*)
81 (*use "ProgLang/tools.sml" 2002*)
82 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
83 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
84 use "Interpret/mstools.sml" (*empty*)
85 use "Interpret/ctree.sml"
86 use "Interpret/ptyps.sml" (* *)
87 (*use "Interpret/generate.sml" new 2011*)
88 use "Interpret/calchead.sml" (* *)
89 (*use "Interpret/appl.sml" new 2011*)
90 use "Interpret/rewtools.sml" (* *)
91 (*use "Interpret/script.sml" TODO*)
92 (*use "Interpret/solve.sml" TODO*)
93 (*use "Interpret/inform.sml" TODO*)
94 use "Interpret/mathengine.sml"(*part.*)
95 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
96 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
97 (*use "xmlsrc/mathml.sml" TODO*)
98 (*use "xmlsrc/datatypes.sml" TODO*)
99 (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
100 (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
101 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
102 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
103 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
104 use "Frontend/messages.sml" (*new 2011*)
105 use "Frontend/states.sml" (*new 2011*)
106 use "Frontend/interface.sml" (*part.*)
107 use "print_exn_G.sml" (*new 2011*)
108 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
109 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
110 use "Knowledge/delete.sml" (*new 2011*)
111 use "Knowledge/descript.sml" (*new 2011*)
112 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
113 use "Knowledge/simplify.sml" (*part.*)
114 (*use "Knowledge/poly.sml" 2002*)
115 (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
116 (*use "Knowledge/equation.sml" 2002*)
117 (*use "Knowledge/root.sml" 2002*)
118 use "Knowledge/lineq.sml" (*new 2011*)
119 (*use "Knowledge/rooteq.sml" 2002*)
120 (*use "Knowledge/rateq.sml" 2002*)
121 (*use "Knowledge/rootrat.sml" 2002*)
122 (*use "Knowledge/rootrateq.sml" 2002*)
123 (*use "Knowledge/polyeq.sml" 2002*)
124 use "Knowledge/calculus.sml" (*new 2011*)
125 (*use "Knowledge/trig.sml" 2002*)
126 (*use "Knowledge/logexp.sml" 2002*)
127 use "Knowledge/diff.sml" (*part.*)
128 (*use "Knowledge/integrate.sml" part. was complete 2009-2
130 (*use "Knowledge/eqsystem.sml" 2002*)
131 use "Knowledge/test.sml" (*new 2011*)
132 use "Knowledge/polyminus.sml" (*part.*)
133 (*use "Knowledge/vect.sml" 2002*)
134 (*use "Knowledge/diffapp.sml" 2002*)
135 (*use "Knowledge/biegelinie.sml" 2002*)
136 (*use "Knowledge/algein.sml" 2002*)
137 use "Knowledge/diophanteq.sml" (*complete*)
138 use "Knowledge/isac.sml" (*part.*)
139 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
140 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
141 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
142 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
146 (*=== inhibit exn ?=============================================================
147 ===== inhibit exn ?===========================================================*)
149 (*========== inhibit exn 110323 ================================================
151 "########### testcode inserted vvv ###########################################";
152 "########### testcode inserted ^^^ ###########################################";
154 ============ inhibit exn 110323 ==============================================*)
156 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
157 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)