intermed. ctxt ..: interrupted -- make x+1=2 go through first
fun step: does strange distinction ...
is_none (get_obj g_env pt (fst p))
(*^^^^^^^^: Apply_Method without init_form*)
... which is affected by SOME (_, ctxt) in env.
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/Isabelle/bin/isabelle jedit -l Isac Test_Isac.thy &
7 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
8 10 20 30 40 50 60 70 80 90 100
11 theory Test_Isac imports
13 "Knowledge/Rational_Test"
19 ("ProgLang/termC.sml")
20 ("ProgLang/calculate.sml")
21 ("ProgLang/rewrite.sml")
22 (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
24 ("Interpret/mstools.sml")
25 ("Interpret/ctree.sml")
26 ("Interpret/ptyps.sml")
27 (*("Interpret/generate.sml")*)
28 ("Interpret/calchead.sml")
29 (*("Interpret/appl.sml")*)
30 ("Interpret/rewtools.sml")
31 (*("Interpret/script.sml")
32 ("Interpret/solve.sml")
33 ("Interpret/inform.sml")*)
34 ("Interpret/mathengine.sml")
36 (*("xmlsrc/mathml.sml")
37 ("xmlsrc/datatypes.sml")
38 ("xmlsrc/pbl-met-hierarchy.sml")
39 ("xmlsrc/thy-hierarchy.sml")*)
40 ("xmlsrc/interface-xml.sml")
42 ("Frontend/messages.sml")
43 ("Frontend/states.sml")
44 ("Frontend/interface.sml")
47 ("Knowledge/delete.sml")
48 ("Knowledge/descript.sml")
49 ("Knowledge/atools.sml")
50 ("Knowledge/simplify.sml")
51 ("Knowledge/poly.sml")
52 ("Knowledge/rational.sml")
53 ("Knowledge/equation.sml")
54 ("Knowledge/root.sml")
55 ("Knowledge/lineq.sml")
56 ("Knowledge/rooteq.sml")
57 ("Knowledge/rateq.sml")
58 ("Knowledge/rootrateq.sml")
59 (*("Knowledge/polyeq.sml")*)
60 ("Knowledge/calculus.sml")
61 ("Knowledge/trig.sml")
62 ("Knowledge/logexp.sml")
63 ("Knowledge/diff.sml")
64 ("Knowledge/integrate.sml")
65 ("Knowledge/eqsystem.sml")
66 ("Knowledge/test.sml")
67 ("Knowledge/polyminus.sml")
68 ("Knowledge/vect.sml")
69 ("Knowledge/diffapp.sml")
70 ("Knowledge/biegelinie.sml")
71 ("Knowledge/algein.sml")
72 ("Knowledge/diophanteq.sml")
73 ("Knowledge/isac.sml")
77 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
78 use "library.sml" (*new 2011*)
79 use "calcelems.sml" (*complete*)
80 use "ProgLang/termC.sml" (*part.*)
81 use "ProgLang/calculate.sml" (*part.*)
82 use "ProgLang/rewrite.sml" (*part.*)
83 (*use "ProgLang/listg.sml" 2002*)
84 (*use "ProgLang/scrtools.sml" 2002*)
85 (*use "ProgLang/tools.sml" 2002*)
86 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
87 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
91 use "Interpret/mstools.sml" (*new 2010*)
94 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
96 ("Test", ["sqroot-test","univariate","equation","test"],
97 ["Test","squ-equ-test-subpbl1"]);
98 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
99 "~~~~~ fun me, args:"; val (_,tac) = nxt;
100 val ("ok", (_, _, (pt, p))) = locatetac tac (pt,p);
101 "~~~~~ fun step, args:"; val (ip as (_,p_), ptp as (pt,p), tacis) = (p, (pt, e_pos'), []);
104 val pIopt = get_pblID (pt,ip);
105 ip = ([],Res) (*false*);
107 member op = [Pbl,Met] p_
108 andalso is_none (get_obj g_env pt (fst p))
115 step p ((pt, e_pos'),[]);
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 use "Interpret/ctree.sml" (*!...see(25)*)
129 use "Interpret/ptyps.sml" (* *)
130 (*use "Interpret/generate.sml" new 2011*)
131 use "Interpret/calchead.sml" (*! *)
132 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
133 use "Interpret/rewtools.sml" (*! *)
134 use "Interpret/script.sml" (*!TODO*)
135 (*use "Interpret/solve.sml" !TODO*)
136 (*use "Interpret/inform.sml" !TODO*)
137 use "Interpret/mathengine.sml" (*!part.*)
138 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
139 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
140 (*use "xmlsrc/mathml.sml" TODO*)
141 (*use "xmlsrc/datatypes.sml" TODO*)
142 (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
143 (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
144 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
145 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
146 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
147 use "Frontend/messages.sml" (*new 2011*)
148 use "Frontend/states.sml" (*new 2011*)
149 use "Frontend/interface.sml" (*part.*)
150 use "print_exn_G.sml" (*new 2011*)
151 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
152 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
153 use "Knowledge/delete.sml" (*new 2011*)
154 use "Knowledge/descript.sml" (*new 2011*)
155 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
156 use "Knowledge/simplify.sml" (*part.*)
157 (*use "Knowledge/poly.sml" 2002*)
158 (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
159 (*use "Knowledge/equation.sml" 2002*)
160 (*use "Knowledge/root.sml" 2002*)
161 use "Knowledge/lineq.sml" (*new 2011*)
162 (*use "Knowledge/rooteq.sml" 2002*)
163 (*use "Knowledge/rateq.sml" 2002*)
164 (*use "Knowledge/rootrat.sml" 2002*)
165 (*use "Knowledge/rootrateq.sml" 2002*)
166 (*use "Knowledge/polyeq.sml" 2002*)
167 (*use "Knowledge/rlang.sml" 2002???*)
168 use "Knowledge/calculus.sml" (*new 2011*)
169 (*use "Knowledge/trig.sml" 2002*)
170 (*use "Knowledge/logexp.sml" 2002*)
171 use "Knowledge/diff.sml" (*part.*)
172 (*use "Knowledge/integrate.sml" part. was complete 2009-2
174 (*use "Knowledge/eqsystem.sml" 2002*)
175 use "Knowledge/test.sml" (*new 2011*)
176 use "Knowledge/polyminus.sml" (*part.*)
177 (*use "Knowledge/vect.sml" 2002*)
178 (*use "Knowledge/diffapp.sml" 2002*)
179 (*use "Knowledge/biegelinie.sml" 2002*)
180 (*use "Knowledge/algein.sml" 2002*)
181 use "Knowledge/diophanteq.sml" (*complete*)
182 use "Knowledge/isac.sml" (*part.*)
183 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
184 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
185 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
186 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
190 (*=== inhibit exn ?=============================================================
191 ===== inhibit exn ?===========================================================*)
193 (*========== inhibit exn 110503 ================================================
195 "########### testcode inserted vvv ###########################################";
196 "########### testcode inserted ^^^ ###########################################";
198 ============ inhibit exn 110503 ==============================================*)
200 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
201 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)