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 &
7 1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
8 10 20 30 40 50 60 70 80 90 100
11 theory Test_Isac imports Isac
15 ("ProgLang/termC.sml")
16 ("ProgLang/calculate.sml")
17 ("ProgLang/rewrite.sml")
18 (*("ProgLang/listg.sml") ("ProgLang/scrtools.sml") ("ProgLang/tools.sml") *)
20 ("Interpret/mstools.sml")
21 ("Interpret/ctree.sml")
22 ("Interpret/ptyps.sml")
23 (*("Interpret/generate.sml")*)
24 ("Interpret/calchead.sml")
25 (*("Interpret/appl.sml")*)
26 ("Interpret/rewtools.sml")
27 (*("Interpret/script.sml")
28 ("Interpret/solve.sml")
29 ("Interpret/inform.sml")*)
30 ("Interpret/mathengine.sml")
32 (*("xmlsrc/mathml.sml")
33 ("xmlsrc/datatypes.sml")
34 ("xmlsrc/pbl-met-hierarchy.sml")
35 ("xmlsrc/thy-hierarchy.sml")*)
36 ("xmlsrc/interface-xml.sml")
38 ("Frontend/messages.sml")
39 ("Frontend/states.sml")
40 ("Frontend/interface.sml")
43 ("Knowledge/delete.sml")
44 ("Knowledge/descript.sml")
45 ("Knowledge/atools.sml")
46 ("Knowledge/simplify.sml")
47 ("Knowledge/poly.sml")
48 ("Knowledge/rational.sml")
49 ("Knowledge/equation.sml")
50 ("Knowledge/root.sml")
51 ("Knowledge/lineq.sml")
52 ("Knowledge/rooteq.sml")
53 ("Knowledge/rateq.sml")
54 ("Knowledge/rootrateq.sml")
55 (*("Knowledge/polyeq.sml")*)
56 ("Knowledge/calculus.sml")
57 ("Knowledge/trig.sml")
58 ("Knowledge/logexp.sml")
59 ("Knowledge/diff.sml")
60 ("Knowledge/integrate.sml")
61 ("Knowledge/eqsystem.sml")
62 ("Knowledge/test.sml")
63 ("Knowledge/polyminus.sml")
64 ("Knowledge/vect.sml")
65 ("Knowledge/diffapp.sml")
66 ("Knowledge/biegelinie.sml")
67 ("Knowledge/algein.sml")
68 ("Knowledge/diophanteq.sml")
69 ("Knowledge/isac.sml")
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 %%%%%%%%%%%%%%%%%%";*}
85 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
87 ("Test", ["sqroot-test","univariate","equation","test"],
88 ["Test","squ-equ-test-subpbl1"]);
89 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS:
102 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
103 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: applicable_in (p,Pbl) pt (Tac id): not at Pbl*)
104 show_pt pt; (*WAS ...(([3], Pbl), solve (-1 + x = 0, x))] OK*)
105 "~~~~~ fun me, args:"; val (_,tac) = nxt;
106 val (pt, p) = case locatetac tac (pt,p) of
107 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
108 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
109 val pIopt = get_pblID (pt,ip);
111 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
112 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
113 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
114 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
115 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
116 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
117 val cpI = if pI = e_pblID then pI' else pI;
118 val cmI = if mI = e_metID then mI' else mI;
119 val {ppc, prls, where_, ...} = get_pbt cpI;
120 val pre = check_preconds "thy 100820" prls where_ probl;
121 val pb = foldl and_ (true, map fst pre);
122 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
123 (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
124 "~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
125 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
126 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
127 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
128 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
129 val cpI = if pI = e_pblID then pI' else pI;
130 val ctxt = get_ctxt pt (p, Pbl);
131 oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)
132 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
133 (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
136 val t = parseNEW ctxt str;
139 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
140 if t = parseNEW ctxt "-1 + x = (0::real)" then ()
142 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
146 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
147 print_depth 999; applicable_in p pt m;
149 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
151 use "Interpret/mstools.sml" (*new 2010*)
152 use "Interpret/ctree.sml" (*!...see(25)*)
153 use "Interpret/ptyps.sml" (* *)
154 (*use "Interpret/generate.sml" new 2011*)
155 use "Interpret/calchead.sml" (*! *)
156 use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
157 use "Interpret/rewtools.sml" (*! *)
158 use "Interpret/script.sml" (*!TODO*)
159 (*use "Interpret/solve.sml" !TODO*)
160 (*use "Interpret/inform.sml" !TODO*)
161 use "Interpret/mathengine.sml" (*!part.*)
162 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
163 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
164 (*use "xmlsrc/mathml.sml" TODO*)
165 (*use "xmlsrc/datatypes.sml" TODO*)
166 (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*)
167 (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*)
168 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
169 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
170 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
171 use "Frontend/messages.sml" (*new 2011*)
172 use "Frontend/states.sml" (*new 2011*)
173 use "Frontend/interface.sml" (*part.*)
174 use "print_exn_G.sml" (*new 2011*)
175 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
176 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
177 use "Knowledge/delete.sml" (*new 2011*)
178 use "Knowledge/descript.sml" (*new 2011*)
179 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*)
180 use "Knowledge/simplify.sml" (*part.*)
181 (*use "Knowledge/poly.sml" 2002*)
182 (*use "Knowledge/rational.sml" part.; diff.emacs--jedit*)
183 (*use "Knowledge/equation.sml" 2002*)
184 (*use "Knowledge/root.sml" 2002*)
185 use "Knowledge/lineq.sml" (*new 2011*)
186 (*use "Knowledge/rooteq.sml" 2002*)
187 (*use "Knowledge/rateq.sml" 2002*)
188 (*use "Knowledge/rootrat.sml" 2002*)
189 (*use "Knowledge/rootrateq.sml" 2002*)
190 (*use "Knowledge/polyeq.sml" 2002*)
191 (*use "Knowledge/rlang.sml" 2002???*)
192 use "Knowledge/calculus.sml" (*new 2011*)
193 (*use "Knowledge/trig.sml" 2002*)
194 (*use "Knowledge/logexp.sml" 2002*)
195 use "Knowledge/diff.sml" (*part.*)
196 (*use "Knowledge/integrate.sml" part. was complete 2009-2
198 (*use "Knowledge/eqsystem.sml" 2002*)
199 use "Knowledge/test.sml" (*new 2011*)
200 use "Knowledge/polyminus.sml" (*part.*)
201 (*use "Knowledge/vect.sml" 2002*)
202 (*use "Knowledge/diffapp.sml" 2002*)
203 (*use "Knowledge/biegelinie.sml" 2002*)
204 (*use "Knowledge/algein.sml" 2002*)
205 use "Knowledge/diophanteq.sml" (*complete*)
206 use "Knowledge/isac.sml" (*part.*)
207 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
208 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
209 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
210 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
214 (*=== inhibit exn ?=============================================================
215 ===== inhibit exn ?===========================================================*)
217 (*========== inhibit exn 110503 ================================================
219 "########### testcode inserted vvv ###########################################";
220 "########### testcode inserted ^^^ ###########################################";
222 ============ inhibit exn 110503 ==============================================*)
224 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
225 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)