1 (* Title: tests for Interpret/mstools.sml
2 Author: Walther Neuper 100930, Mathias Lehnfeld
3 (c) copyright due to lincense terms.
5 "-----------------------------------------------------------------------------------------------";
6 "table of contents -----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------------------------";
8 "----------- go through Model_Problem until nxt_tac --------------------------------------------";
9 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
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 "--------------------------------------------------------";
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"];
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 ================================================*)
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 Step.by_tactic tac (pt,p) of
51 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml Step.by_tactic";
52 "~~~~~ fun Step.do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
53 val pIopt = get_pblID (pt,ip);
55 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
56 Library.member op = [Pbl,Met] 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 = Problem.id_empty 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 Step_Specify.by_tactic_input, 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 = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
73 val cpI = if pI = Problem.id_empty then pI' else pI;
74 val ctxt = get_ctxt pt (p, Pbl);
75 "~~~~~ fun add_single, 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=" ^ UnparseC.term t);
80 val ots = (Library.distinct op = o flat o (map #5)) (ori:O_Model.T);
81 val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
82 val (d, ts) = Input_Descript.split t;
83 "~~~~~ fun Input_Descript.split, args:"; val (t as d $ arg) = t;
84 (*if Input_Descript.is_a d then () else error "TODO";*)
85 if Input_Descript.is_a d then () else error "TODO";
86 "----- these were the errors (call hierarchy from bottom up)";
87 I_Model.check_single ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
88 Err "[error] add_single: is_known: identifiers [equality] not in example"*)
89 nxt_specif_additem "#Given" ct ptp;(*WAS
90 Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
91 Step_Specify.by_tactic_input tac ptp;(*WAS
92 Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
93 nxt_specify_ (pt,ip); (*WAS
94 Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
95 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS
96 Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
97 ========== inhibit exn AK110725 ================================================*)
99 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
100 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
101 "----------- fun Input_Descript.join -- fun Input_Descript.split -------------------------------";
102 (*val t = str2term "maximum A";
103 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
104 val it = "maximum A" : cterm
105 > val t = str2term "fixedValues [r=Arbfix]";
106 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
107 "fixedValues [r = Arbfix]"
108 > val t = str2term "valuesFor [a]";
109 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
111 > val t = str2term "valuesFor [a,b]";
112 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
114 > val t = str2term "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]";
115 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join 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) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
120 > val t = str2term "interval {x::real. 0 <= x & x <= 2*r}";
121 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
122 "interval {x. 0 <= x & x <= 2 * r}"
124 > val t = str2term "equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))";
125 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
126 "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"
127 > val t = str2term "solveFor x";
128 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
130 > val t = str2term "errorBound (eps=0)";
131 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
132 "errorBound (eps = 0)"
133 > val t = str2term "solutions L";
134 > val (d,ts) = Input_Descript.split thy t; Input_Descript.join thy (d,ts);
138 > val t = (Thm.term_of o the o (parse thy)) "testdscforlist [#1]";
139 > val (d,ts) = Input_Descript.split t;
140 > Input_Descript.join thy (d,ts);
141 val it = "testdscforlist [#1]" : cterm
143 > val t = (Thm.term_of o the o (parse thy)) "(A::real)";
144 > val (d,ts) = Input_Descript.split 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) = Input_Descript.split 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) = Input_Descript.split t;
153 val ts = [Free ("#1","'a"),Free ("#2","'a")] : NOT WANTED
155 "----------- type penv -------------------------------------------------------------------------";
156 "----------- type penv -------------------------------------------------------------------------";
157 "----------- type penv -------------------------------------------------------------------------";
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";
167 val penv = [(e_,[ev]),(v_,[vv]),(r_,[rv2,rv2])]: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
174 "----------- fun untouched ---------------------------------------------------------------------";
175 "----------- fun untouched ---------------------------------------------------------------------";
176 "----------- fun untouched ---------------------------------------------------------------------";
179 > untouched [I_Model.single_empty];
181 > untouched [I_Model.single_empty, (1,[],false,"I_Model.single_empty",Syn "I_Model.single_empty")];
182 val it = false : bool*)
183 "----------- fun pbl_ids -----------------------------------------------------------------------";
184 "----------- fun pbl_ids -----------------------------------------------------------------------";
185 "----------- fun pbl_ids -----------------------------------------------------------------------";
187 val t as t1 $ t2 = str2term "antiDerivativeName M_b";
190 val t = (Thm.term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
191 val (d,argl) = strip_comb t;
192 Input_Descript.is_a d; (*see Input_Descript.split*)
197 [Const ("List.list.Cons","[bool, bool List.list] => bool List.list") $
198 (Const # $ Free # $ Const (#,#)) $ Const ("List.list.Nil","bool List..
200 val (dsc,vl) = (Input_Descript.split 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
204 val (dsc,id) = (split_did o Thm.term_of o the o (parse thy)) "solveFor v_";
206 val it = [Free ("x","RealDef.real")] : term list
208 val (dsc,vl) = (Input_Descript.split 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_";
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 ----------------------------------------------------------------------";
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
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 ^.........!!!!
234 "----------- fun upd ---------------------------------------------------------------------------";
235 "----------- fun upd ---------------------------------------------------------------------------";
236 "----------- fun upd ---------------------------------------------------------------------------";
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*)
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;
254 val eargs = flat eargs;
255 val (vs, dsc, id, vl) = hd eargs;
256 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
258 val (vs, dsc, id, vl) = hd (tl eargs);
259 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
261 val (vs, dsc, id, vl) = hd (tl (tl eargs));
262 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
264 val (vs, dsc, id, vl) = hd (tl (tl (tl eargs)));
265 val envv = upds_envv thy envv [(vs, dsc, id, vl)];
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"),[# $ # $ (# $ #)])]),
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"),[# $ # $ (# $ #)])]),
277 [(Free ("fix_","bool List.list"),[Const (#,#),Free (#,#)]),
278 (Free ("m_","bool"),[Free (#,#)]),
279 (Free ("vs_","bool List.list"),[# $ # $ Const #])])] : envv *)
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";
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";
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";
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";
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";
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";