|
1 (* Title: tests for Interpret/mstools.sml |
|
2 Author: Walther Neuper 100930, Mathias Lehnfeld |
|
3 (c) copyright due to lincense terms. |
|
4 *) |
|
5 "-----------------------------------------------------------------------------------------------"; |
|
6 "table of contents -----------------------------------------------------------------------------"; |
|
7 "-----------------------------------------------------------------------------------------------"; |
|
8 "----------- go through Model_Problem until nxt_tac --------------------------------------------"; |
|
9 "----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; |
|
10 "----------- type penv -------------------------------------------------------------------------"; |
|
11 "----------- fun untouched ---------------------------------------------------------------------"; |
|
12 "----------- fun pbl_ids -----------------------------------------------------------------------"; |
|
13 "----------- fun upd_penv ----------------------------------------------------------------------"; |
|
14 "----------- fun upd ---------------------------------------------------------------------------"; |
|
15 "----------- fun upds_envv ---------------------------------------------------------------------"; |
|
16 "----------- fun common_subthy -----------------------------------------------------------------"; |
|
17 "--------------------------------------------------------"; |
|
18 "--------------------------------------------------------"; |
|
19 "--------------------------------------------------------"; |
|
20 "--------------------------------------------------------"; |
|
21 |
|
22 |
|
23 "----------- go through Model_Problem until nxt_tac --------------------------------------------"; |
|
24 "----------- go through Model_Problem until nxt_tac --------------------------------------------"; |
|
25 "----------- go through Model_Problem until nxt_tac --------------------------------------------"; |
|
26 (*FIXME.WN110511 delete this test? (goes through "Model_Problem until nxt_tac)*) |
|
27 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; |
|
28 val (dI',pI',mI') = |
|
29 ("Test", ["sqroot-test","univariate","equation","test"], |
|
30 ["Test","squ-equ-test-subpbl1"]); |
|
31 (*========== inhibit exn AK110725 ================================================ |
|
32 (* ERROR: same as above, see lines 120- 123 *) |
|
33 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
34 ========== inhibit exn AK110725 ================================================*) |
|
35 |
|
36 (*========== inhibit exn AK110725 ================================================ |
|
37 (* ERROR: p, nxt, pt not declared due to above error *) |
|
38 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
43 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
47 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*) |
|
48 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*) |
|
49 "~~~~~ fun me, args:"; val (_,tac) = nxt; |
|
50 val (pt, p) = case locatetac tac (pt,p) of |
|
51 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; |
|
52 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
|
53 val pIopt = get_pblID (pt,ip); |
|
54 tacis; (*= []*) |
|
55 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*) |
|
56 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*) |
|
57 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip); |
|
58 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), |
|
59 probl,spec=(dI,pI,mI),...}) = get_obj I pt p; |
|
60 just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*) |
|
61 val cpI = if pI = e_pblID then pI' else pI; |
|
62 val cmI = if mI = e_metID then mI' else mI; |
|
63 val {ppc, prls, where_, ...} = get_pbt cpI; |
|
64 val pre = check_preconds "thy 100820" prls where_ probl; |
|
65 val pb = foldl and_ (true, map fst pre); |
|
66 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) |
|
67 (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*) |
|
68 "~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp); |
|
69 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp); |
|
70 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_), |
|
71 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p; |
|
72 val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; |
|
73 val cpI = if pI = e_pblID then pI' else pI; |
|
74 val ctxt = get_ctxt pt (p, Pbl); |
|
75 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct); |
|
76 val SOME t = parseNEW ctxt str; |
|
77 is_known ctxt sel oris t; |
|
78 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t); |
|
79 val _ = tracing ("RM is_known: t=" ^ term2str t); |
|
80 val ots = (distinct o flat o (map #5)) (ori:ori list); |
|
81 val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots; |
|
82 val (d, ts) = split_dts t; |
|
83 "~~~~~ fun split_dts, args:"; val (t as d $ arg) = t; |
|
84 (*if is_dsc d then () else error "TODO";*) |
|
85 if is_dsc d then () else error "TODO"; |
|
86 "----- these were the errors (call hierarchy from bottom up)"; |
|
87 appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS |
|
88 Err "[error] appl_add: is_known: identifiers [equality] not in example"*) |
|
89 nxt_specif_additem "#Given" ct ptp;(*WAS |
|
90 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
|
91 nxt_specif tac ptp;(*WAS |
|
92 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
|
93 nxt_specify_ (pt,ip); (*WAS |
|
94 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
|
95 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS |
|
96 Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) |
|
97 ========== inhibit exn AK110725 ================================================*) |
|
98 |
|
99 "----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; |
|
100 "----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; |
|
101 "----------- fun comp_dts -- fun split_dts -----------------------------------------------------"; |
|
102 (*val t = str2term "maximum A"; |
|
103 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
104 val it = "maximum A" : cterm |
|
105 > val t = str2term "fixedValues [r=Arbfix]"; |
|
106 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
107 "fixedValues [r = Arbfix]" |
|
108 > val t = str2term "valuesFor [a]"; |
|
109 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
110 "valuesFor [a]" |
|
111 > val t = str2term "valuesFor [a,b]"; |
|
112 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
113 "valuesFor [a, b]" |
|
114 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"; |
|
115 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
116 relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]" |
|
117 > val t = str2term "boundVariable a"; |
|
118 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
119 "boundVariable a" |
|
120 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}"; |
|
121 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
122 "interval {x. 0 <= x & x <= 2 * r}" |
|
123 |
|
124 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))"; |
|
125 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
126 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))" |
|
127 > val t = str2term "solveFor x"; |
|
128 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
129 "solveFor x" |
|
130 > val t = str2term "errorBound (eps=0)"; |
|
131 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
132 "errorBound (eps = 0)" |
|
133 > val t = str2term "solutions L"; |
|
134 > val (d,ts) = split_dts thy t; comp_dts thy (d,ts); |
|
135 "solutions L" |
|
136 |
|
137 before 6.5.03: |
|
138 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]"; |
|
139 > val (d,ts) = split_dts t; |
|
140 > comp_dts thy (d,ts); |
|
141 val it = "testdscforlist [#1]" : cterm |
|
142 |
|
143 > val t = (Thm.term_of o the o (parse thy)) "(A::real)"; |
|
144 > val (d,ts) = split_dts t; |
|
145 val d = Const ("empty","empty") : term |
|
146 val ts = [Free ("A","RealDef.real")] : term list |
|
147 > val t = (Thm.term_of o the o (parse thy)) "[R=(R::real)]"; |
|
148 > val (d,ts) = split_dts t; |
|
149 val d = Const ("empty","empty") : term |
|
150 val ts = [Const # $ Free # $ Free (#,#)] : term list |
|
151 > val t = (Thm.term_of o the o (parse thy)) "[#1,#2]"; |
|
152 > val (d,ts) = split_dts t; |
|
153 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED |
|
154 *) |
|
155 "----------- type penv -------------------------------------------------------------------------"; |
|
156 "----------- type penv -------------------------------------------------------------------------"; |
|
157 "----------- type penv -------------------------------------------------------------------------"; |
|
158 (* |
|
159 val e_ = (Thm.term_of o the o (parse thy)) "e_::bool"; |
|
160 val ev = (Thm.term_of o the o (parse thy)) "#4 + #3 * x^^^#2 = #0"; |
|
161 val v_ = (Thm.term_of o the o (parse thy)) "v_"; |
|
162 val vv = (Thm.term_of o the o (parse thy)) "x"; |
|
163 val r_ = (Thm.term_of o the o (parse thy)) "err_::bool"; |
|
164 val rv1 = (Thm.term_of o the o (parse thy)) "#0"; |
|
165 val rv2 = (Thm.term_of o the o (parse thy)) "eps"; |
|
166 |
|
167 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]:penv; |
|
168 map getval penv; |
|
169 [(Free ("e_","bool"), |
|
170 Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#0","RealDef.real")), |
|
171 (Free ("v_","RealDef.real"),Free ("x","RealDef.real")), |
|
172 (Free ("err_","bool"),Free ("#0","RealDef.real"))] : (term * term) list |
|
173 *) |
|
174 "----------- fun untouched ---------------------------------------------------------------------"; |
|
175 "----------- fun untouched ---------------------------------------------------------------------"; |
|
176 "----------- fun untouched ---------------------------------------------------------------------"; |
|
177 (*> untouched []; |
|
178 val it = true : bool |
|
179 > untouched [e_itm]; |
|
180 val it = true : bool |
|
181 > untouched [e_itm, (1,[],false,"e_itm",Syn "e_itm")]; |
|
182 val it = false : bool*) |
|
183 "----------- fun pbl_ids -----------------------------------------------------------------------"; |
|
184 "----------- fun pbl_ids -----------------------------------------------------------------------"; |
|
185 "----------- fun pbl_ids -----------------------------------------------------------------------"; |
|
186 (* |
|
187 val t as t1 $ t2 = str2term "antiDerivativeName M_b"; |
|
188 pbl_ids ctxt t1 t2; |
|
189 |
|
190 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]"; |
|
191 val (d,argl) = strip_comb t; |
|
192 is_dsc d; (*see split_dts*) |
|
193 dest_list (d,argl); |
|
194 val (_ $ v) = t; |
|
195 is_list v; |
|
196 pbl_ids ctxt d v; |
|
197 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $ |
|
198 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List.. |
|
199 |
|
200 val (dsc,vl) = (split_dts o Thm.term_of o the o (parse thy)) "solveFor x"; |
|
201 val dsc = Const ("Input_Descript.solveFor","RealDef.real => Tools.una") : term |
|
202 val vl = Free ("x","RealDef.real") : term |
|
203 |
|
204 val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_"; |
|
205 pbl_ids ctxt dsc vl; |
|
206 val it = [Free ("x","RealDef.real")] : term list |
|
207 |
|
208 val (dsc,vl) = (split_dts o Thm.term_of o the o(parse thy)) |
|
209 "errorBound (eps=#0)"; |
|
210 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy)) "errorBound err_"; |
|
211 pbl_ids ctxt dsc vl; |
|
212 val it = [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")] : term list *) |
|
213 "----------- fun upd_penv ----------------------------------------------------------------------"; |
|
214 "----------- fun upd_penv ----------------------------------------------------------------------"; |
|
215 "----------- fun upd_penv ----------------------------------------------------------------------"; |
|
216 (* |
|
217 val penv = []; |
|
218 val (dsc,vl) = (split_did o Thm.term_of o the o (parse thy)) "solveFor x"; |
|
219 val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_"; |
|
220 val penv = upd_penv thy penv dsc (id, vl); |
|
221 [(Free ("v_","RealDef.real"), |
|
222 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")])] |
|
223 : (term * term list) list |
|
224 |
|
225 val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"errorBound (eps=#0)"; |
|
226 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"errorBound err_"; |
|
227 upd_penv thy penv dsc (id, vl); |
|
228 [(Free ("v_","RealDef.real"), |
|
229 [Const (#,#) $ Free (#,#) $ Free ("#0","RealDef.real")]), |
|
230 (Free ("err_","bool"), |
|
231 [Free ("#0","RealDef.real"),Free ("eps","RealDef.real")])] |
|
232 : (term * term list) list ^.........!!!! |
|
233 *) |
|
234 "----------- fun upd ---------------------------------------------------------------------------"; |
|
235 "----------- fun upd ---------------------------------------------------------------------------"; |
|
236 "----------- fun upd ---------------------------------------------------------------------------"; |
|
237 (* |
|
238 val i = 2; |
|
239 val envv = [(1,[]:penv),(2,[]:penv),(3,[]:penv)]:envv; |
|
240 val (dsc,vl) = (split_did o Thm.term_of o the o(parse thy))"boundVariable b"; |
|
241 val (dsc,id) = (split_did o Thm.term_of o the o(parse thy))"boundVariable v_"; |
|
242 upd thy envv dsc (id, vl) i; |
|
243 val it = (2,[(Free ("v_","RealDef.real"),[Free ("b","RealDef.real")])]) |
|
244 : int * (term * term list) list*) |
|
245 |
|
246 "----------- fun upds_envv ---------------------------------------------------------------------"; |
|
247 "----------- fun upds_envv ---------------------------------------------------------------------"; |
|
248 "----------- fun upds_envv ---------------------------------------------------------------------"; |
|
249 (* eval test-maximum.sml until Specify_Method ... |
|
250 val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt []; |
|
251 val met = (#ppc o get_met) mI; |
|
252 |
|
253 val envv = []; |
|
254 val eargs = flat eargs; |
|
255 val (vs, dsc, id, vl) = hd eargs; |
|
256 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
257 |
|
258 val (vs, dsc, id, vl) = hd (tl eargs); |
|
259 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
260 |
|
261 val (vs, dsc, id, vl) = hd (tl (tl eargs)); |
|
262 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
263 |
|
264 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs))); |
|
265 val envv = upds_envv thy envv [(vs, dsc, id, vl)]; |
|
266 [(1, |
|
267 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
268 (Free ("m_","bool"),[Free (#,#)]), |
|
269 (Free ("vs_","bool List.list"),[# $ # $ Const #]), |
|
270 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
271 (2, |
|
272 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
273 (Free ("m_","bool"),[Free (#,#)]), |
|
274 (Free ("vs_","bool List.list"),[# $ # $ Const #]), |
|
275 (Free ("rs_","bool List.list"),[# $ # $ (# $ #)])]), |
|
276 (3, |
|
277 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]), |
|
278 (Free ("m_","bool"),[Free (#,#)]), |
|
279 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *) |
|
280 |
|
281 "----------- fun common_subthy -----------------------------------------------------------------"; |
|
282 "----------- fun common_subthy -----------------------------------------------------------------"; |
|
283 "----------- fun common_subthy -----------------------------------------------------------------"; |
|
284 val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Inverse_Z_Transform}); |
|
285 if Context.theory_name (common_subthy (thy1, thy2)) = "Inverse_Z_Transform" |
|
286 then () else error "common_subthy 1"; |
|
287 |
|
288 val (thy1, thy2) = (@{theory Inverse_Z_Transform}, @{theory Partial_Fractions});(* Isac.Inverse_Z_Transform *) |
|
289 if Context.theory_name (common_subthy (thy1, thy2)) = "Inverse_Z_Transform" |
|
290 then () else error "common_subthy 2"; |
|
291 |
|
292 val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory PolyEq}); |
|
293 if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 3"; |
|
294 |
|
295 val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac_Knowledge}); |
|
296 if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 4"; |
|
297 |
|
298 val (thy1, thy2) = (@{theory PolyEq}, @{theory Partial_Fractions}); |
|
299 if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 5"; |
|
300 |
|
301 val (thy1, thy2) = (@{theory Isac_Knowledge}, @{theory Partial_Fractions}); |
|
302 if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 6"; |