1 (* use"ME/appl.sml"; |
|
2 use"appl.sml"; |
|
3 |
|
4 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
5 10 20 30 40 50 60 70 80 |
|
6 *) |
|
7 val e_cterm' = empty_cterm'; |
|
8 |
|
9 |
|
10 fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = |
|
11 (rew_ord':rew_ord',erls,ca) |
|
12 | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = |
|
13 (rew_ord',erls,ca) |
|
14 | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = |
|
15 (rew_ord',erls, ca) |
|
16 | rew_info rls = raise error ("rew_info called with '"^rls2str rls^"'"); |
|
17 |
|
18 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*) |
|
19 fun from_pblobj_or_detail_thm thm' p pt = |
|
20 let val (pbl,p',rls') = par_pbl_det pt p |
|
21 in if pbl |
|
22 then let (*val _= writeln("### from_pblobj_or_detail_thm: pbl=true")*) |
|
23 val thy' = get_obj g_domID pt p' |
|
24 val {rew_ord',erls,(*asm_thm,*)...} = |
|
25 get_met (get_obj g_metID pt p') |
|
26 (*val _= writeln("### from_pblobj_or_detail_thm: metID= "^ |
|
27 (metID2str(get_obj g_metID pt p'))) |
|
28 val _= writeln("### from_pblobj_or_detail_thm: erls= "^erls)*) |
|
29 in ("OK",thy',rew_ord',erls,(*put_asm*)false) |
|
30 end |
|
31 else ((*writeln("### from_pblobj_or_detail_thm: pbl=false");*) |
|
32 (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!! |
|
33 NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false) |
|
34 | SOME rls =>*) |
|
35 let val thy' = get_obj g_domID pt (par_pblobj pt p) |
|
36 val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls' |
|
37 in ("OK",thy',rew_ord',erls,false) end) |
|
38 end; |
|
39 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*) |
|
40 fun from_pblobj_or_detail_calc scrop p pt = |
|
41 (* val (scrop, p, pt) = (op_, p, pt); |
|
42 *) |
|
43 let val (pbl,p',rls') = par_pbl_det pt p |
|
44 in if pbl |
|
45 then let val thy' = get_obj g_domID pt p' |
|
46 val {calc = scr_isa_fns,...} = |
|
47 get_met (get_obj g_metID pt p') |
|
48 val opt = assoc (scr_isa_fns, scrop) |
|
49 in case opt of |
|
50 SOME isa_fn => ("OK",thy',isa_fn) |
|
51 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'", |
|
52 "",("",e_evalfn)) end |
|
53 else (*case assoc(!ruleset', rls') of |
|
54 NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn)) |
|
55 | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*) |
|
56 (* val SOME rls = assoc(!ruleset', rls'); |
|
57 *) |
|
58 let val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
59 val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
|
60 in case assoc (scr_isa_fns, scrop) of |
|
61 SOME isa_fn => ("OK",thy',isa_fn) |
|
62 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'", |
|
63 "",("",e_evalfn)) end |
|
64 end; |
|
65 (*------------------------------------------------------------------*) |
|
66 |
|
67 val op_and = Const ("op &", [bool, bool] ---> bool); |
|
68 (*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool)); |
|
69 val it = "a & b" : cterm |
|
70 *) |
|
71 fun mk_and a b = op_and $ a $ b; |
|
72 (*> (cterm_of thy) |
|
73 (mk_and (Free("a",bool)) (Free("b",bool))); |
|
74 val it = "a & b" : cterm*) |
|
75 |
|
76 fun mk_and [] = HOLogic.true_const |
|
77 | mk_and (t::[]) = t |
|
78 | mk_and (t::ts) = |
|
79 let fun mk t' (t::[]) = op_and $ t' $ t |
|
80 | mk t' (t::ts) = mk (op_and $ t' $ t) ts |
|
81 in mk t ts end; |
|
82 (*> val pred = map (term_of o the o (parse thy)) |
|
83 ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"]; |
|
84 > (cterm_of thy) (mk_and pred); |
|
85 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*) |
|
86 |
|
87 |
|
88 |
|
89 |
|
90 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
|
91 fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, []) |
|
92 |
|
93 | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred = |
|
94 (e_term, if pred <> Const ("Script.Assumptions",bool) |
|
95 then [pred] |
|
96 else (map fst) (get_assumptions_ pt (p,Res))) |
|
97 |
|
98 (* val pred = (term_of o the o (parse thy)) pred; |
|
99 val consts as Const ("List.list.Cons",_) $ eq $ _ = ft; |
|
100 mk_set thy pt p consts pred; |
|
101 *) |
|
102 | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred = |
|
103 let val (bdv,_) = HOLogic.dest_eq eq; |
|
104 val pred = if pred <> Const ("Script.Assumptions",bool) |
|
105 then [pred] |
|
106 else (map fst) (get_assumptions_ pt (p,Res)) |
|
107 in (bdv, pred) end |
|
108 |
|
109 | mk_set thy _ _ l _ = |
|
110 raise error ("check_elementwise: no set "^ |
|
111 (Syntax.string_of_term (thy2ctxt thy) l)); |
|
112 (*> val consts = str2term "[x=#4]"; |
|
113 > val pred = str2term "Assumptions"; |
|
114 > val pt = union_asm pt p |
|
115 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]), |
|
116 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; |
|
117 > val p = []; |
|
118 > val (sss,ttt) = mk_set thy pt p consts pred; |
|
119 > (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt); |
|
120 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... |
|
121 |
|
122 val consts = str2term "UniversalList"; |
|
123 val pred = str2term "Assumptions"; |
|
124 |
|
125 *) |
|
126 |
|
127 |
|
128 |
|
129 (*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*) |
|
130 (* val (erls,consts,(bdv,pred)) = (erl,ft,vp); |
|
131 val (consts,(bdv,pred)) = (ft,vp); |
|
132 *) |
|
133 fun check_elementwise thy erls all_results (bdv, asm) = |
|
134 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*) |
|
135 fun check sub = |
|
136 let val inst_ = map (subst_atomic [sub]) asm |
|
137 in case eval__true thy 1 inst_ [] erls of |
|
138 (asm', true) => ([HOLogic.mk_eq sub], asm') |
|
139 | (_, false) => ([],[]) |
|
140 end; |
|
141 (*val _= writeln("### check_elementwise: res= "^(term2str all_results)^ |
|
142 ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*) |
|
143 val c' = isalist2list all_results |
|
144 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*) |
|
145 val subs = map (pair bdv) c'' |
|
146 in if asm = [] then (all_results, []) |
|
147 else ((apfst ((list2isalist bool) o flat)) o |
|
148 (apsnd flat) o split_list o (map check)) subs end; |
|
149 (* 20.5.03 |
|
150 > val all_results = str2term "[x=a+b,x=b,x=3]"; |
|
151 > val bdv = str2term "x"; |
|
152 > val asm = str2term "(x ~= a) & (x ~= b)"; |
|
153 > val erls = e_rls; |
|
154 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm); |
|
155 > term2str t; writeln(terms2str ts); |
|
156 val it = "[x = a + b, x = b, x = c]" : string |
|
157 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"] |
|
158 ... with appropriate erls this should be: |
|
159 val it = "[x = a + b, x = c]" : string |
|
160 ["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"] |
|
161 ////// because b ~= b False*) |
|
162 |
|
163 |
|
164 |
|
165 (*before 5.03----- |
|
166 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\ |
|
167 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4"; |
|
168 > val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct; |
|
169 val ct' = "True" : cterm' |
|
170 |
|
171 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\ |
|
172 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4"; |
|
173 > val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct; |
|
174 val ct' = "True" : cterm' |
|
175 |
|
176 |
|
177 > val const = (term_of o the o (parse thy)) "(#3::real)"; |
|
178 > val pred' = subst_atomic [(bdv,const)] pred; |
|
179 |
|
180 |
|
181 > val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]"; |
|
182 > val bdv = (term_of o the o (parse thy)) "(x::real)"; |
|
183 > val pred = (term_of o the o (parse thy)) |
|
184 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4"; |
|
185 > val ttt = check_elementwise thy consts (bdv, pred); |
|
186 > (cterm_of thy) ttt; |
|
187 val it = "[x = #-3, x = #3]" : cterm |
|
188 |
|
189 > val consts = (term_of o the o (parse thy)) "[x = #4]"; |
|
190 > val bdv = (term_of o the o (parse thy)) "(x::real)"; |
|
191 > val pred = (term_of o the o (parse thy)) |
|
192 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x"; |
|
193 > val ttt = check_elementwise thy consts (bdv,pred); |
|
194 > (cterm_of thy) ttt; |
|
195 val it = "[x = #4]" : cterm |
|
196 |
|
197 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]"; |
|
198 > val bdv = (term_of o the o (parse thy)) "(x::real)"; |
|
199 > val pred = (term_of o the o (parse thy)) |
|
200 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x"; |
|
201 > val ttt = check_elementwise thy consts (bdv,pred); |
|
202 > (cterm_of thy) ttt; |
|
203 val it = "[]" : cterm*) |
|
204 |
|
205 |
|
206 (* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*) |
|
207 fun split_dummy str = |
|
208 let fun scan s' [] = (implode s', "") |
|
209 | scan s' (s::ss) = if s=" " then (implode s', implode ss) |
|
210 else scan (s'@[s]) ss; |
|
211 in ((scan []) o explode) str end; |
|
212 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)"; |
|
213 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string |
|
214 > split_dummy "x=-#5//#12"; |
|
215 val it = ("x=-#5//#12","") : string * string*) |
|
216 |
|
217 |
|
218 |
|
219 |
|
220 (*.applicability of a tacic wrt. a calc-state (ptree,pos'). |
|
221 additionally used by next_tac in the script-interpreter for sequence-tacs. |
|
222 tests for applicability are so expensive, that results (rewrites!) |
|
223 are kept in the return-value of 'type tac_'. |
|
224 .*) |
|
225 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = |
|
226 Appl (Init_Proof' (ct', spec)) |
|
227 |
|
228 | applicable_in (p,p_) pt Model_Problem = |
|
229 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
230 then Notappl ((tac2str Model_Problem)^ |
|
231 " not for pos "^(pos'2str (p,p_))) |
|
232 else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p |
|
233 val {ppc,...} = get_pbt pI' |
|
234 val pbl = init_pbl ppc |
|
235 in Appl (Model_Problem' (pI', pbl, [])) end |
|
236 (* val Refine_Tacitly pI = m; |
|
237 *) |
|
238 | applicable_in (p,p_) pt (Refine_Tacitly pI) = |
|
239 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
240 then Notappl ((tac2str (Refine_Tacitly pI))^ |
|
241 " not for pos "^(pos'2str (p,p_))) |
|
242 else (* val Refine_Tacitly pI = m; |
|
243 *) |
|
244 let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p; |
|
245 val opt = refine_ori oris pI; |
|
246 in case opt of |
|
247 SOME pblID => |
|
248 Appl (Refine_Tacitly' (pI, pblID, |
|
249 e_domID, e_metID, [](*filled in specify*))) |
|
250 | NONE => Notappl ((tac2str (Refine_Tacitly pI))^ |
|
251 " not applicable") end |
|
252 (* val (p,p_) = ip; |
|
253 val Refine_Problem pI = m; |
|
254 *) |
|
255 | applicable_in (p,p_) pt (Refine_Problem pI) = |
|
256 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
257 then Notappl ((tac2str (Refine_Problem pI))^ |
|
258 " not for pos "^(pos'2str (p,p_))) |
|
259 else |
|
260 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), |
|
261 probl=itms, ...}) = get_obj I pt p; |
|
262 val thy = if dI' = e_domID then dI else dI'; |
|
263 val rfopt = refine_pbl (assoc_thy thy) pI itms; |
|
264 in case rfopt of |
|
265 NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable") |
|
266 | SOME (rf as (pI',_)) => |
|
267 (* val SOME (rf as (pI',_)) = rfopt; |
|
268 *) |
|
269 if pI' = pI |
|
270 then Notappl ((tac2str (Refine_Problem pI))^" not applicable") |
|
271 else Appl (Refine_Problem' rf) |
|
272 end |
|
273 |
|
274 (*the specify-tacs have cterm' instead term: |
|
275 parse+error here!!!: see appl_add*) |
|
276 | applicable_in (p,p_) pt (Add_Given ct') = |
|
277 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
278 then Notappl ((tac2str (Add_Given ct'))^ |
|
279 " not for pos "^(pos'2str (p,p_))) |
|
280 else Appl (Add_Given' (ct', [(*filled in specify_additem*)])) |
|
281 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*) |
|
282 |
|
283 | applicable_in (p,p_) pt (Del_Given ct') = |
|
284 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
285 then Notappl ((tac2str (Del_Given ct'))^ |
|
286 " not for pos "^(pos'2str (p,p_))) |
|
287 else Appl (Del_Given' ct') |
|
288 |
|
289 | applicable_in (p,p_) pt (Add_Find ct') = |
|
290 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
291 then Notappl ((tac2str (Add_Find ct'))^ |
|
292 " not for pos "^(pos'2str (p,p_))) |
|
293 else Appl (Add_Find' (ct', [(*filled in specify_additem*)])) |
|
294 |
|
295 | applicable_in (p,p_) pt (Del_Find ct') = |
|
296 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
297 then Notappl ((tac2str (Del_Find ct'))^ |
|
298 " not for pos "^(pos'2str (p,p_))) |
|
299 else Appl (Del_Find' ct') |
|
300 |
|
301 | applicable_in (p,p_) pt (Add_Relation ct') = |
|
302 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
303 then Notappl ((tac2str (Add_Relation ct'))^ |
|
304 " not for pos "^(pos'2str (p,p_))) |
|
305 else Appl (Add_Relation' (ct', [(*filled in specify_additem*)])) |
|
306 |
|
307 | applicable_in (p,p_) pt (Del_Relation ct') = |
|
308 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
309 then Notappl ((tac2str (Del_Relation ct'))^ |
|
310 " not for pos "^(pos'2str (p,p_))) |
|
311 else Appl (Del_Relation' ct') |
|
312 |
|
313 | applicable_in (p,p_) pt (Specify_Theory dI) = |
|
314 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
315 then Notappl ((tac2str (Specify_Theory dI))^ |
|
316 " not for pos "^(pos'2str (p,p_))) |
|
317 else Appl (Specify_Theory' dI) |
|
318 (* val (p,p_) = p; val Specify_Problem pID = m; |
|
319 val Specify_Problem pID = m; |
|
320 *) |
|
321 | applicable_in (p,p_) pt (Specify_Problem pID) = |
|
322 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
323 then Notappl ((tac2str (Specify_Problem pID))^ |
|
324 " not for pos "^(pos'2str (p,p_))) |
|
325 else |
|
326 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_), |
|
327 probl=itms, ...}) = get_obj I pt p; |
|
328 val thy = assoc_thy (if dI' = e_domID then dI else dI'); |
|
329 val {ppc,where_,prls,...} = get_pbt pID; |
|
330 val pbl = if pI'=e_pblID andalso pI=e_pblID |
|
331 then (false, (init_pbl ppc, [])) |
|
332 else match_itms_oris thy itms (ppc,where_,prls) oris; |
|
333 in Appl (Specify_Problem' (pID, pbl)) end |
|
334 (* val Specify_Method mID = nxt; val (p,p_) = p; |
|
335 *) |
|
336 | applicable_in (p,p_) pt (Specify_Method mID) = |
|
337 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
338 then Notappl ((tac2str (Specify_Method mID))^ |
|
339 " not for pos "^(pos'2str (p,p_))) |
|
340 else Appl (Specify_Method' (mID,[(*filled in specify*)], |
|
341 [(*filled in specify*)])) |
|
342 |
|
343 | applicable_in (p,p_) pt (Apply_Method mI) = |
|
344 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
|
345 then Notappl ((tac2str (Apply_Method mI))^ |
|
346 " not for pos "^(pos'2str (p,p_))) |
|
347 else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*))) |
|
348 |
|
349 | applicable_in (p,p_) pt (Check_Postcond pI) = |
|
350 if member op = [Pbl,Met] p_ |
|
351 then Notappl ((tac2str (Check_Postcond pI))^ |
|
352 " not for pos "^(pos'2str (p,p_))) |
|
353 else Appl (Check_Postcond' |
|
354 (pI,(e_term,[(*asm in solve*)]))) |
|
355 (* in solve -"- ^^^^^^ gets returnvalue of scr*) |
|
356 |
|
357 (*these are always applicable*) |
|
358 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str)) |
|
359 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve') |
|
360 |
|
361 (* val m as Rewrite_Inst (subs, thm') = m; |
|
362 *) |
|
363 | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) = |
|
364 if member op = [Pbl,Met] p_ |
|
365 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
366 else |
|
367 let |
|
368 val pp = par_pblobj pt p; |
|
369 val thy' = (get_obj g_domID pt pp):theory'; |
|
370 val thy = assoc_thy thy'; |
|
371 val {rew_ord'=ro',erls=erls,...} = |
|
372 get_met (get_obj g_metID pt pp); |
|
373 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
|
374 Frm => (get_obj g_form pt p, p) |
|
375 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
|
376 | _ => raise error ("applicable_in: call by "^ |
|
377 (pos'2str (p,p_))); |
|
378 in |
|
379 let val subst = subs2subst thy subs; |
|
380 val subs' = subst2subs' subst; |
|
381 in case rewrite_inst_ thy (assoc_rew_ord ro') erls |
|
382 (*put_asm*)false subst (assoc_thm' thy thm') f of |
|
383 SOME (f',asm) => Appl ( |
|
384 Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm', |
|
385 (*term_of o the o (parse (assoc_thy thy'))*) f, |
|
386 (*(term_of o the o (parse (assoc_thy thy'))*) (f', |
|
387 (*map (term_of o the o (parse (assoc_thy thy')))*) asm))) |
|
388 | NONE => Notappl ((fst thm')^" not applicable") end |
|
389 handle _ => Notappl ("syntax error in "^(subs2str subs)) end |
|
390 |
|
391 (* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m); |
|
392 val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac); |
|
393 *) |
|
394 | applicable_in (p,p_) pt (m as Rewrite thm') = |
|
395 if member op = [Pbl,Met] p_ |
|
396 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
397 else |
|
398 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt; |
|
399 val thy = assoc_thy thy'; |
|
400 val f = case p_ of |
|
401 Frm => get_obj g_form pt p |
|
402 | Res => (fst o (get_obj g_result pt)) p |
|
403 | _ => raise error ("applicable_in Rewrite: call by "^ |
|
404 (pos'2str (p,p_))); |
|
405 in if msg = "OK" |
|
406 then |
|
407 ((*writeln("### applicable_in rls'= "^rls');*) |
|
408 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f; |
|
409 *) |
|
410 case rewrite_ thy (assoc_rew_ord ro) |
|
411 rls' false (assoc_thm' thy thm') f of |
|
412 SOME (f',asm) => Appl ( |
|
413 Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm))) |
|
414 | NONE => Notappl ("'"^(fst thm')^"' not applicable") ) |
|
415 else Notappl msg |
|
416 end |
|
417 |
|
418 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') = |
|
419 if member op = [Pbl,Met] p_ |
|
420 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
421 else |
|
422 let |
|
423 val pp = par_pblobj pt p; |
|
424 val thy' = (get_obj g_domID pt pp):theory'; |
|
425 val thy = assoc_thy thy'; |
|
426 val {rew_ord'=ro',erls=erls,...} = |
|
427 get_met (get_obj g_metID pt pp); |
|
428 (*val put_asm = true;*) |
|
429 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
|
430 Frm => (get_obj g_form pt p, p) |
|
431 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
|
432 | _ => raise error ("applicable_in: call by "^ |
|
433 (pos'2str (p,p_))); |
|
434 in case rewrite_ thy (assoc_rew_ord ro') erls |
|
435 (*put_asm*)false (assoc_thm' thy thm') f of |
|
436 SOME (f',asm) => Appl ( |
|
437 Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm))) |
|
438 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end |
|
439 |
|
440 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) = |
|
441 if member op = [Pbl,Met] p_ |
|
442 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
443 else |
|
444 let |
|
445 val pp = par_pblobj pt p; |
|
446 val thy' = (get_obj g_domID pt pp):theory'; |
|
447 val thy = assoc_thy thy'; |
|
448 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp); |
|
449 val f = case p_ of Frm => get_obj g_form pt p |
|
450 | Res => (fst o (get_obj g_result pt)) p |
|
451 | _ => raise error ("applicable_in: call by "^ |
|
452 (pos'2str (p,p_))); |
|
453 in |
|
454 let val subst = subs2subst thy subs |
|
455 val subs' = subst2subs' subst |
|
456 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of |
|
457 SOME (f',asm) => Appl ( |
|
458 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm))) |
|
459 | NONE => Notappl (rls^" not applicable") end |
|
460 handle _ => Notappl ("syntax error in "^(subs2str subs)) end |
|
461 |
|
462 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) = |
|
463 if member op = [Pbl,Met] p_ |
|
464 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
465 else |
|
466 let |
|
467 val pp = par_pblobj pt p; |
|
468 val thy' = (get_obj g_domID pt pp):theory'; |
|
469 val thy = assoc_thy thy'; |
|
470 val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} = |
|
471 get_met (get_obj g_metID pt pp); |
|
472 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
|
473 Frm => (get_obj g_form pt p, p) |
|
474 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
|
475 | _ => raise error ("applicable_in: call by "^ |
|
476 (pos'2str (p,p_))); |
|
477 in |
|
478 let val subst = subs2subst thy subs; |
|
479 val subs' = subst2subs' subst; |
|
480 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of |
|
481 SOME (f',asm) => Appl ( |
|
482 Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm))) |
|
483 | NONE => Notappl (rls^" not applicable") end |
|
484 handle _ => Notappl ("syntax error in "^(subs2str subs)) end |
|
485 |
|
486 | applicable_in (p,p_) pt (m as Rewrite_Set rls) = |
|
487 if member op = [Pbl,Met] p_ |
|
488 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
489 else |
|
490 let |
|
491 val pp = par_pblobj pt p; |
|
492 val thy' = (get_obj g_domID pt pp):theory'; |
|
493 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
|
494 Frm => (get_obj g_form pt p, p) |
|
495 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
|
496 | _ => raise error ("applicable_in: call by "^ |
|
497 (pos'2str (p,p_))); |
|
498 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of |
|
499 SOME (f',asm) => |
|
500 ((*writeln("#.# applicable_in Rewrite_Set,2f'= "^f');*) |
|
501 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm))) |
|
502 ) |
|
503 | NONE => Notappl (rls^" not applicable") end |
|
504 |
|
505 | applicable_in (p,p_) pt (m as Detail_Set rls) = |
|
506 if member op = [Pbl,Met] p_ |
|
507 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
508 else |
|
509 let val pp = par_pblobj pt p |
|
510 val thy' = (get_obj g_domID pt pp):theory' |
|
511 val f = case p_ of |
|
512 Frm => get_obj g_form pt p |
|
513 | Res => (fst o (get_obj g_result pt)) p |
|
514 | _ => raise error ("applicable_in: call by "^ |
|
515 (pos'2str (p,p_))); |
|
516 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of |
|
517 SOME (f',asm) => |
|
518 Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm))) |
|
519 | NONE => Notappl (rls^" not applicable") end |
|
520 |
|
521 |
|
522 | applicable_in p pt (End_Ruleset) = |
|
523 raise error ("applicable_in: not impl. for "^ |
|
524 (tac2str End_Ruleset)) |
|
525 |
|
526 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m); |
|
527 *) |
|
528 | applicable_in (p,p_) pt (m as Calculate op_) = |
|
529 if member op = [Pbl,Met] p_ |
|
530 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
531 else |
|
532 let |
|
533 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt; |
|
534 val f = case p_ of |
|
535 Frm => get_obj g_form pt p |
|
536 | Res => (fst o (get_obj g_result pt)) p |
|
537 in if msg = "OK" then |
|
538 case calculate_ (assoc_thy thy') isa_fn f of |
|
539 SOME (f', (id, thm)) => |
|
540 Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm)))) |
|
541 | NONE => Notappl ("'calculate "^op_^"' not applicable") |
|
542 else Notappl msg |
|
543 end |
|
544 |
|
545 (*Substitute combines two different kind of "substitution": |
|
546 (1) subst_atomic: for ?a..?z |
|
547 (2) Pattern.match: for solving equational systems |
|
548 (which raises exn for ?a..?z)*) |
|
549 | applicable_in (p,p_) pt (m as Substitute sube) = |
|
550 if member op = [Pbl,Met] p_ |
|
551 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
552 else let val pp = par_pblobj pt p |
|
553 val thy = assoc_thy (get_obj g_domID pt pp) |
|
554 val f = case p_ of |
|
555 Frm => get_obj g_form pt p |
|
556 | Res => (fst o (get_obj g_result pt)) p |
|
557 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp) |
|
558 val subte = sube2subte sube |
|
559 val subst = sube2subst thy sube |
|
560 in if foldl and_ (true, map contains_Var subte) |
|
561 (*1*) |
|
562 then let val f' = subst_atomic subst f |
|
563 in if f = f' then Notappl (sube2str sube^" not applicable") |
|
564 else Appl (Substitute' (subte, f, f')) |
|
565 end |
|
566 (*2*) |
|
567 else case rewrite_terms_ thy (assoc_rew_ord rew_ord') |
|
568 erls subte f of |
|
569 SOME (f', _) => Appl (Substitute' (subte, f, f')) |
|
570 | NONE => Notappl (sube2str sube^" not applicable") |
|
571 end |
|
572 (*-------WN08114 interrupted with error in polyminus.sml "11 = 11" |
|
573 | applicable_in (p,p_) pt (m as Substitute sube) = |
|
574 if member op = [Pbl,Met] p_ |
|
575 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
576 else let val pp = par_pblobj pt p |
|
577 val thy = assoc_thy (get_obj g_domID pt pp) |
|
578 val f = case p_ of |
|
579 Frm => get_obj g_form pt p |
|
580 | Res => (fst o (get_obj g_result pt)) p |
|
581 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp) |
|
582 val subte = sube2subte sube |
|
583 in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of |
|
584 SOME (f', _) => Appl (Substitute' (subte, f, f')) |
|
585 | NONE => Notappl (sube2str sube^" not applicable") |
|
586 end |
|
587 ------------------*) |
|
588 |
|
589 | applicable_in p pt (Apply_Assumption cts') = |
|
590 (raise error ("applicable_in: not impl. for "^ |
|
591 (tac2str (Apply_Assumption cts')))) |
|
592 |
|
593 (*'logical' applicability wrt. script in locate: Inconsistent?*) |
|
594 | applicable_in (p,p_) pt (m as Take ct') = |
|
595 if member op = [Pbl,Met] p_ |
|
596 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
597 else |
|
598 let val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
599 in (case parse (assoc_thy thy') ct' of |
|
600 SOME ct => Appl (Take' (term_of ct)) |
|
601 | NONE => Notappl ("syntax error in "^ct')) |
|
602 end |
|
603 |
|
604 | applicable_in p pt (Take_Inst ct') = |
|
605 raise error ("applicable_in: not impl. for "^ |
|
606 (tac2str (Take_Inst ct'))) |
|
607 |
|
608 | applicable_in p pt (Group (con, ints)) = |
|
609 raise error ("applicable_in: not impl. for "^ |
|
610 (tac2str (Group (con, ints)))) |
|
611 |
|
612 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) = |
|
613 if member op = [Pbl,Met] p_ |
|
614 then (*maybe Apply_Method has already been done*) |
|
615 case get_obj g_env pt p of |
|
616 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [], |
|
617 e_term, [], subpbl domID pblID)) |
|
618 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
619 else (*somewhere later in the script*) |
|
620 Appl (Subproblem' ((domID, pblID, e_metID), [], |
|
621 e_term, [], subpbl domID pblID)) |
|
622 |
|
623 | applicable_in p pt (End_Subproblem) = |
|
624 raise error ("applicable_in: not impl. for "^ |
|
625 (tac2str (End_Subproblem))) |
|
626 |
|
627 | applicable_in p pt (CAScmd ct') = |
|
628 raise error ("applicable_in: not impl. for "^ |
|
629 (tac2str (CAScmd ct'))) |
|
630 |
|
631 | applicable_in p pt (Split_And) = |
|
632 raise error ("applicable_in: not impl. for "^ |
|
633 (tac2str (Split_And))) |
|
634 | applicable_in p pt (Conclude_And) = |
|
635 raise error ("applicable_in: not impl. for "^ |
|
636 (tac2str (Conclude_And))) |
|
637 | applicable_in p pt (Split_Or) = |
|
638 raise error ("applicable_in: not impl. for "^ |
|
639 (tac2str (Split_Or))) |
|
640 | applicable_in p pt (Conclude_Or) = |
|
641 raise error ("applicable_in: not impl. for "^ |
|
642 (tac2str (Conclude_Or))) |
|
643 |
|
644 | applicable_in (p,p_) pt (Begin_Trans) = |
|
645 let |
|
646 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
|
647 (*_____ implizit Take in gen*) |
|
648 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p) |
|
649 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p) |
|
650 | _ => raise error ("applicable_in: call by "^ |
|
651 (pos'2str (p,p_))); |
|
652 val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
653 in (Appl (Begin_Trans' f)) |
|
654 handle _ => raise error ("applicable_in: Begin_Trans finds \ |
|
655 \syntaxerror in '"^(term2str f)^"'") end |
|
656 |
|
657 (*TODO: check parent branches*) |
|
658 | applicable_in (p,p_) pt (End_Trans) = |
|
659 let val thy' = get_obj g_domID pt (par_pblobj pt p); |
|
660 in if p_ = Res |
|
661 then Appl (End_Trans' (get_obj g_result pt p)) |
|
662 else Notappl "'End_Trans' is not applicable at \ |
|
663 \the beginning of a transitive sequence" |
|
664 (*TODO: check parent branches*) |
|
665 end |
|
666 |
|
667 | applicable_in p pt (Begin_Sequ) = |
|
668 raise error ("applicable_in: not impl. for "^ |
|
669 (tac2str (Begin_Sequ))) |
|
670 | applicable_in p pt (End_Sequ) = |
|
671 raise error ("applicable_in: not impl. for "^ |
|
672 (tac2str (End_Sequ))) |
|
673 | applicable_in p pt (Split_Intersect) = |
|
674 raise error ("applicable_in: not impl. for "^ |
|
675 (tac2str (Split_Intersect))) |
|
676 | applicable_in p pt (End_Intersect) = |
|
677 raise error ("applicable_in: not impl. for "^ |
|
678 (tac2str (End_Intersect))) |
|
679 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it; |
|
680 val (vvv,ppp) = vp; |
|
681 |
|
682 val Check_elementwise pred = m; |
|
683 |
|
684 val ((p,p_), Check_elementwise pred) = (p, m); |
|
685 *) |
|
686 | applicable_in (p,p_) pt (m as Check_elementwise pred) = |
|
687 if member op = [Pbl,Met] p_ |
|
688 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
|
689 else |
|
690 let |
|
691 val pp = par_pblobj pt p; |
|
692 val thy' = (get_obj g_domID pt pp):theory'; |
|
693 val thy = assoc_thy thy' |
|
694 val metID = (get_obj g_metID pt pp) |
|
695 val {crls,...} = get_met metID |
|
696 (*val _=writeln("### applicable_in Check_elementwise: crls= "^crls) |
|
697 val _=writeln("### applicable_in Check_elementwise: pred= "^pred)*) |
|
698 (*val erl = the (assoc'(!ruleset',crls))*) |
|
699 val (f,asm) = case p_ of |
|
700 Frm => (get_obj g_form pt p , []) |
|
701 | Res => get_obj g_result pt p; |
|
702 (*val _= writeln("### applicable_in Check_elementwise: f= "^f);*) |
|
703 val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred); |
|
704 (*val (v,p)=vp;val _=writeln("### applicable_in Check_elementwise: vp= "^ |
|
705 pair2str(term2str v,term2str p))*) |
|
706 in case f of |
|
707 Const ("List.list.Cons",_) $ _ $ _ => |
|
708 Appl (Check_elementwise' |
|
709 (f, pred, |
|
710 ((*writeln("### applicable_in Check_elementwise: --> "^ |
|
711 (res2str (check_elementwise thy crls f vp)));*) |
|
712 check_elementwise thy crls f vp))) |
|
713 | Const ("Tools.UniversalList",_) => |
|
714 Appl (Check_elementwise' (f, pred, (f,asm))) |
|
715 | Const ("List.list.Nil",_) => |
|
716 (*Notappl "not applicable to empty list" 3.6.03*) |
|
717 Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*)))) |
|
718 | _ => Notappl ("not applicable: "^(term2str f)^" should be constants") |
|
719 end |
|
720 |
|
721 | applicable_in (p,p_) pt Or_to_List = |
|
722 if member op = [Pbl,Met] p_ |
|
723 then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_))) |
|
724 else |
|
725 let |
|
726 val pp = par_pblobj pt p; |
|
727 val thy' = (get_obj g_domID pt pp):theory'; |
|
728 val thy = assoc_thy thy'; |
|
729 val f = case p_ of |
|
730 Frm => get_obj g_form pt p |
|
731 | Res => (fst o (get_obj g_result pt)) p; |
|
732 in (let val ls = or2list f |
|
733 in Appl (Or_to_List' (f, ls)) end) |
|
734 handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f)) |
|
735 end |
|
736 |
|
737 | applicable_in p pt (Collect_Trues) = |
|
738 raise error ("applicable_in: not impl. for "^ |
|
739 (tac2str (Collect_Trues))) |
|
740 |
|
741 | applicable_in p pt (Empty_Tac) = |
|
742 Notappl "Empty_Tac is not applicable" |
|
743 |
|
744 | applicable_in (p,p_) pt (Tac id) = |
|
745 let |
|
746 val pp = par_pblobj pt p; |
|
747 val thy' = (get_obj g_domID pt pp):theory'; |
|
748 val thy = assoc_thy thy'; |
|
749 val f = case p_ of |
|
750 Frm => get_obj g_form pt p |
|
751 | Res => (fst o (get_obj g_result pt)) p; |
|
752 in case id of |
|
753 "subproblem_equation_dummy" => |
|
754 if is_expliceq f |
|
755 then Appl (Tac_ (thy, term2str f, id, |
|
756 "subproblem_equation_dummy ("^(term2str f)^")")) |
|
757 else Notappl "applicable only to equations made explicit" |
|
758 | "solve_equation_dummy" => |
|
759 let (*val _= writeln("### applicable_in: solve_equation_dummy: f= " |
|
760 ^f);*) |
|
761 val (id',f') = split_dummy (term2str f); |
|
762 (*val _= writeln("### applicable_in: f'= "^f');*) |
|
763 (*val _= (term_of o the o (parse thy)) f';*) |
|
764 (*val _= writeln"### applicable_in: solve_equation_dummy";*) |
|
765 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem" |
|
766 else if is_expliceq ((term_of o the o (parse thy)) f') |
|
767 then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]")) |
|
768 else error ("applicable_in: f= " ^ f') end |
|
769 | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end |
|
770 |
|
771 | applicable_in p pt End_Proof' = Appl End_Proof'' |
|
772 |
|
773 | applicable_in _ _ m = |
|
774 raise error ("applicable_in called for "^(tac2str m)); |
|
775 |
|
776 (*WN060614 unused*) |
|
777 fun tac2tac_ pt p m = |
|
778 case applicable_in p pt m of |
|
779 Appl (m') => m' |
|
780 | Notappl _ => raise error ("tac2mstp': fails with"^ |
|
781 (tac2str m)); |
|
782 |
|