4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
7 val e_cterm' = empty_cterm';
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, ...}) =
14 | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
16 | rew_info rls = error ("rew_info called with '"^rls2str rls^"'");
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
22 then let (*val _= tracing("### 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 _= tracing("### from_pblobj_or_detail_thm: metID= "^
27 (metID2str(get_obj g_metID pt p')))
28 val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)
29 in ("OK",thy',rew_ord',erls,(*put_asm*)false)
31 else ((*tracing("### 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)
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)
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);
43 let val (pbl,p',rls') = par_pbl_det pt p
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)
50 SOME isa_fn => ("OK",thy',isa_fn)
51 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
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');
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^"'",
65 (*------------------------------------------------------------------*)
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
71 fun mk_and a b = op_and $ a $ b;
73 (mk_and (Free("a",bool)) (Free("b",bool)));
74 val it = "a & b" : cterm*)
76 fun mk_and [] = @{term True}
79 let fun mk t' (t::[]) = op_and $ t' $ t
80 | mk t' (t::ts) = mk (op_and $ t' $ t) ts
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*)
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, [])
93 | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
94 (e_term, if pred <> Const ("Script.Assumptions",bool)
96 else get_assumptions_ pt (p,Res))
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;
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)
106 else get_assumptions_ pt (p,Res)
109 | mk_set thy _ _ l _ =
110 error ("check_elementwise: no set " ^ term2str l);
111 (*> val consts = str2term "[x=#4]";
112 > val pred = str2term "Assumptions";
113 > val pt = union_asm pt p
114 [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
115 ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
117 > val (sss,ttt) = mk_set thy pt p consts pred;
118 > (term2str sss, term2str ttt);
119 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
121 val consts = str2term "UniversalList";
122 val pred = str2term "Assumptions";
128 (*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
129 (* val (erls,consts,(bdv,pred)) = (erl,ft,vp);
130 val (consts,(bdv,pred)) = (ft,vp);
132 fun check_elementwise thy erls all_results (bdv, asm) =
133 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
135 let val inst_ = map (subst_atomic [sub]) asm
136 in case eval__true thy 1 inst_ [] erls of
137 (asm', true) => ([HOLogic.mk_eq sub], asm')
138 | (_, false) => ([],[])
140 (*val _= tracing("### check_elementwise: res= "^(term2str all_results)^
141 ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
142 val c' = isalist2list all_results
143 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
144 val subs = map (pair bdv) c''
145 in if asm = [] then (all_results, [])
146 else ((apfst ((list2isalist bool) o flat)) o
147 (apsnd flat) o split_list o (map check)) subs end;
149 > val all_results = str2term "[x=a+b,x=b,x=3]";
150 > val bdv = str2term "x";
151 > val asm = str2term "(x ~= a) & (x ~= b)";
153 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
154 > term2str t; tracing(terms2str ts);
155 val it = "[x = a + b, x = b, x = c]" : string
156 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
157 ... with appropriate erls this should be:
158 val it = "[x = a + b, x = c]" : string
159 ["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
160 ////// because b ~= b False*)
165 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
166 \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
167 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
168 val ct' = "HOL.True" : cterm'
170 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
171 \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
172 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
173 val ct' = "HOL.True" : cterm'
176 > val const = (term_of o the o (parse thy)) "(#3::real)";
177 > val pred' = subst_atomic [(bdv,const)] pred;
180 > val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
181 > val bdv = (term_of o the o (parse thy)) "(x::real)";
182 > val pred = (term_of o the o (parse thy))
183 "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
184 > val ttt = check_elementwise thy consts (bdv, pred);
185 > (cterm_of thy) ttt;
186 val it = "[x = #-3, x = #3]" : cterm
188 > val consts = (term_of o the o (parse thy)) "[x = #4]";
189 > val bdv = (term_of o the o (parse thy)) "(x::real)";
190 > val pred = (term_of o the o (parse thy))
191 "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
192 > val ttt = check_elementwise thy consts (bdv,pred);
193 > (cterm_of thy) ttt;
194 val it = "[x = #4]" : cterm
196 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
197 > val bdv = (term_of o the o (parse thy)) "(x::real)";
198 > val pred = (term_of o the o (parse thy))
199 " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
200 > val ttt = check_elementwise thy consts (bdv,pred);
201 > (cterm_of thy) ttt;
202 val it = "[]" : cterm*)
205 (* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)
206 fun split_dummy str =
207 let fun scan s' [] = (implode s', "")
208 | scan s' (s::ss) = if s=" " then (implode s', implode ss)
209 else scan (s'@[s]) ss;
210 in ((scan []) o Symbol.explode) str end;
211 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
212 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
213 > split_dummy "x=-#5//#12";
214 val it = ("x=-#5//#12","") : string * string*)
219 (*.applicability of a tacic wrt. a calc-state (ptree,pos').
220 additionally used by next_tac in the script-interpreter for script-tacs.
221 tests for applicability are so expensive, that results (rewrites!)
222 are kept in the return-value of 'type tac_'.
224 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Appl (Init_Proof' (ct', spec))
226 | applicable_in (p,p_) pt Model_Problem =
227 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
228 then Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
231 val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
232 val {ppc,...} = get_pbt pI'
233 val pbl = init_pbl ppc
234 in Appl (Model_Problem' (pI', pbl, [])) end
236 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
237 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
238 then Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
241 val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
242 val opt = refine_ori oris pI;
245 Appl (Refine_Tacitly' (pI, pblID,
246 e_domID, e_metID, [](*filled in specify*)))
247 | NONE => Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
250 | applicable_in (p,p_) pt (Refine_Problem pI) =
251 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
252 then Notappl ((tac2str (Refine_Problem pI))^
253 " not for pos "^(pos'2str (p,p_)))
255 let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
256 probl=itms, ...}) = get_obj I pt p;
257 val thy = if dI' = e_domID then dI else dI';
258 val rfopt = refine_pbl (assoc_thy thy) pI itms;
260 NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
261 | SOME (rf as (pI',_)) =>
262 (* val SOME (rf as (pI',_)) = rfopt;
265 then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
266 else Appl (Refine_Problem' rf)
269 (*the specify-tacs have cterm' instead term:
270 parse+error here!!!: see appl_add*)
271 | applicable_in (p,p_) pt (Add_Given ct') =
272 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
273 then Notappl ((tac2str (Add_Given ct'))^
274 " not for pos "^(pos'2str (p,p_)))
275 else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
276 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
278 | applicable_in (p,p_) pt (Del_Given ct') =
279 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
280 then Notappl ((tac2str (Del_Given ct'))^
281 " not for pos "^(pos'2str (p,p_)))
282 else Appl (Del_Given' ct')
284 | applicable_in (p,p_) pt (Add_Find ct') =
285 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
286 then Notappl ((tac2str (Add_Find ct'))^
287 " not for pos "^(pos'2str (p,p_)))
288 else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
290 | applicable_in (p,p_) pt (Del_Find ct') =
291 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
292 then Notappl ((tac2str (Del_Find ct'))^
293 " not for pos "^(pos'2str (p,p_)))
294 else Appl (Del_Find' ct')
296 | applicable_in (p,p_) pt (Add_Relation ct') =
297 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
298 then Notappl ((tac2str (Add_Relation ct'))^
299 " not for pos "^(pos'2str (p,p_)))
300 else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
302 | applicable_in (p,p_) pt (Del_Relation ct') =
303 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
304 then Notappl ((tac2str (Del_Relation ct'))^
305 " not for pos "^(pos'2str (p,p_)))
306 else Appl (Del_Relation' ct')
308 | applicable_in (p,p_) pt (Specify_Theory dI) =
309 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
310 then Notappl ((tac2str (Specify_Theory dI))^
311 " not for pos "^(pos'2str (p,p_)))
312 else Appl (Specify_Theory' dI)
313 (* val (p,p_) = p; val Specify_Problem pID = m;
314 val Specify_Problem pID = m;
316 | applicable_in (p,p_) pt (Specify_Problem pID) =
317 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
318 then Notappl ((tac2str (Specify_Problem pID))^
319 " not for pos "^(pos'2str (p,p_)))
321 let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
322 probl=itms, ...}) = get_obj I pt p;
323 val thy = assoc_thy (if dI' = e_domID then dI else dI');
324 val {ppc,where_,prls,...} = get_pbt pID;
325 val pbl = if pI'=e_pblID andalso pI=e_pblID
326 then (false, (init_pbl ppc, []))
327 else match_itms_oris thy itms (ppc,where_,prls) oris;
328 in Appl (Specify_Problem' (pID, pbl)) end
329 (* val Specify_Method mID = nxt; val (p,p_) = p;
331 | applicable_in (p,p_) pt (Specify_Method mID) =
332 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
333 then Notappl ((tac2str (Specify_Method mID))^
334 " not for pos "^(pos'2str (p,p_)))
335 else Appl (Specify_Method' (mID,[(*filled in specify*)],
336 [(*filled in specify*)]))
338 | applicable_in (p,p_) pt (Apply_Method mI) =
339 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
340 then Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))
343 val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;
344 val {where_, ...} = get_pbt pI
345 val pres = map (mk_env probl |> subst_atomic) where_
348 then assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres
350 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
351 and then decide on Notappl/Appl accordingly once more.
352 Implement after all tests are running, since this changes
353 overall system behavior*)
354 in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end
356 | applicable_in (p,p_) pt (Check_Postcond pI) =
357 if member op = [Pbl,Met] p_
358 then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))
359 else Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))
361 (*these are always applicable*)
362 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
363 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
365 | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm')) =
366 if member op = [Pbl, Met] p_
367 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
370 val pp = par_pblobj pt p;
371 val thy' = (get_obj g_domID pt pp): theory';
372 val thy = assoc_thy thy';
373 val {rew_ord' = ro', erls = erls, ...} = get_met (get_obj g_metID pt pp);
374 val (f, p) = case p_ of (*p 12.4.00 unnecessary*)
375 Frm => (get_obj g_form pt p, p)
376 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
377 | _ => error ("applicable_in: call by " ^ pos'2str (p,p_));
380 val subst = subs2subst thy subs;
381 val subs' = subst2subs' subst;
382 in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm' thy thm') f of
384 Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm', f, (f', asm)))
385 | NONE => Notappl ((fst thm')^" not applicable")
387 handle _ => Notappl ("syntax error in "^(subs2str subs))
390 | applicable_in (p,p_) pt (m as Rewrite thm') =
391 if member op = [Pbl,Met] p_
392 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
394 let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
395 val thy = assoc_thy thy';
397 Frm => get_obj g_form pt p
398 | Res => (fst o (get_obj g_result pt)) p
399 | _ => error ("applicable_in Rewrite: call by "^
403 ((*tracing("### applicable_in rls'= "^rls');*)
404 (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
406 case rewrite_ thy (assoc_rew_ord ro)
407 rls' false (assoc_thm' thy thm') f of
408 SOME (f',asm) => Appl (
409 Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
410 | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
414 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
415 if member op = [Pbl,Met] p_
416 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
419 val pp = par_pblobj pt p;
420 val thy' = (get_obj g_domID pt pp):theory';
421 val thy = assoc_thy thy';
422 val {rew_ord'=ro',erls=erls,...} =
423 get_met (get_obj g_metID pt pp);
424 (*val put_asm = true;*)
425 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
426 Frm => (get_obj g_form pt p, p)
427 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
428 | _ => error ("applicable_in: call by "^
430 in case rewrite_ thy (assoc_rew_ord ro') erls
431 (*put_asm*)false (assoc_thm' thy thm') f of
432 SOME (f',asm) => Appl (
433 Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
434 | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
436 | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
437 if member op = [Pbl,Met] p_
438 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
441 val pp = par_pblobj pt p;
442 val thy' = (get_obj g_domID pt pp):theory';
443 val thy = assoc_thy thy';
444 val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
445 val f = case p_ of Frm => get_obj g_form pt p
446 | Res => (fst o (get_obj g_result pt)) p
447 | _ => error ("applicable_in: call by "^
450 let val subst = subs2subst thy subs
451 val subs' = subst2subs' subst
452 in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
453 SOME (f',asm) => Appl (
454 Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
455 | NONE => Notappl (rls^" not applicable") end
456 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
458 | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
459 if member op = [Pbl,Met] p_
460 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
463 val pp = par_pblobj pt p;
464 val thy' = (get_obj g_domID pt pp):theory';
465 val thy = assoc_thy thy';
466 val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
467 get_met (get_obj g_metID pt pp);
468 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
469 Frm => (get_obj g_form pt p, p)
470 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
471 | _ => error ("applicable_in: call by "^
474 let val subst = subs2subst thy subs;
475 val subs' = subst2subs' subst;
476 in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
477 SOME (f',asm) => Appl (
478 Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
479 | NONE => Notappl (rls^" not applicable") end
480 handle _ => Notappl ("syntax error in "^(subs2str subs)) end
482 | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
483 if member op = [Pbl,Met] p_
484 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
487 val pp = par_pblobj pt p;
488 val thy' = (get_obj g_domID pt pp):theory';
489 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
490 Frm => (get_obj g_form pt p, p)
491 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
492 | _ => error ("applicable_in: call by "^
494 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
496 ((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
497 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
499 | NONE => Notappl (rls^" not applicable") end
501 | applicable_in (p,p_) pt (m as Detail_Set rls) =
502 if member op = [Pbl,Met] p_
503 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
505 let val pp = par_pblobj pt p
506 val thy' = (get_obj g_domID pt pp):theory'
508 Frm => get_obj g_form pt p
509 | Res => (fst o (get_obj g_result pt)) p
510 | _ => error ("applicable_in: call by "^
512 in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
514 Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
515 | NONE => Notappl (rls^" not applicable") end
518 | applicable_in p pt (End_Ruleset) =
519 error ("applicable_in: not impl. for "^
520 (tac2str End_Ruleset))
522 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
524 | applicable_in (p,p_) pt (m as Calculate op_) =
525 if member op = [Pbl,Met] p_
526 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
529 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
531 Frm => get_obj g_form pt p
532 | Res => (fst o (get_obj g_result pt)) p
533 in if msg = "OK" then
534 case calculate_ (assoc_thy thy') isa_fn f of
535 SOME (f', (id, thm)) =>
536 Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
537 | NONE => Notappl ("'calculate "^op_^"' not applicable")
541 (*Substitute combines two different kind of "substitution":
542 (1) subst_atomic: for ?a..?z
543 (2) Pattern.match: for solving equational systems
544 (which raises exn for ?a..?z)*)
545 | applicable_in (p,p_) pt (m as Substitute sube) =
546 if member op = [Pbl,Met] p_
547 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
550 val pp = par_pblobj pt p
551 val thy = assoc_thy (get_obj g_domID pt pp)
553 Frm => get_obj g_form pt p
554 | Res => (fst o (get_obj g_result pt)) p
555 val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
556 val subte = sube2subte sube
557 val subst = sube2subst thy sube
558 val ro = assoc_rew_ord rew_ord'
560 if foldl and_ (true, map contains_Var subte)
563 let val f' = subst_atomic subst f
564 in if f = f' then Notappl (sube2str sube^" not applicable")
565 else Appl (Substitute' (ro, erls, subte, f, f'))
569 case rewrite_terms_ thy ro erls subte f of
570 SOME (f', _) => Appl (Substitute' (ro, erls, subte, f, f'))
571 | NONE => Notappl (sube2str sube^" not applicable")
574 | applicable_in p pt (Apply_Assumption cts') =
575 (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts'))))
577 (*'logical' applicability wrt. script in locate: Inconsistent?*)
578 | applicable_in (p,p_) pt (m as Take ct') =
579 if member op = [Pbl,Met] p_
580 then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))
582 let val thy' = get_obj g_domID pt (par_pblobj pt p);
583 in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of
584 SOME ct => Appl (Take' ct)
585 | NONE => Notappl ("syntax error in " ^ ct'))
588 | applicable_in p pt (Take_Inst ct') =
589 error ("applicable_in: not impl. for " ^ tac2str (Take_Inst ct'))
590 | applicable_in p pt (Group (con, ints)) =
591 error ("applicable_in: not impl. for " ^ tac2str (Group (con, ints)))
593 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
594 if member op = [Pbl,Met] p_
595 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
596 case get_obj g_env pt p of
598 Appl (Subproblem' ((domID, pblID, e_metID), [],
599 e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
600 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
601 else (*somewhere later in the script*)
602 Appl (Subproblem' ((domID, pblID, e_metID), [],
603 e_term, [], e_ctxt, subpbl domID pblID))
605 | applicable_in p pt (End_Subproblem) =
606 error ("applicable_in: not impl. for " ^ tac2str End_Subproblem)
607 | applicable_in p pt (CAScmd ct') =
608 error ("applicable_in: not impl. for " ^ tac2str (CAScmd ct'))
609 | applicable_in p pt (Split_And) =
610 error ("applicable_in: not impl. for " ^ tac2str Split_And)
611 | applicable_in p pt (Conclude_And) =
612 error ("applicable_in: not impl. for " ^ tac2str Conclude_And)
613 | applicable_in p pt (Split_Or) =
614 error ("applicable_in: not impl. for " ^ tac2str Split_Or)
615 | applicable_in p pt (Conclude_Or) =
616 error ("applicable_in: not impl. for " ^ tac2str Conclude_Or)
618 | applicable_in (p,p_) pt (Begin_Trans) =
620 val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
621 (*_____ implizit Take in gen*)
622 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
623 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
624 | _ => error ("applicable_in: call by "^
626 val thy' = get_obj g_domID pt (par_pblobj pt p);
627 in (Appl (Begin_Trans' f))
628 handle _ => error ("applicable_in: Begin_Trans finds \
629 \syntaxerror in '"^(term2str f)^"'") end
631 (*TODO: check parent branches*)
632 | applicable_in (p,p_) pt (End_Trans) =
633 let val thy' = get_obj g_domID pt (par_pblobj pt p);
635 then Appl (End_Trans' (get_obj g_result pt p))
636 else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
637 (*TODO: check parent branches*)
639 | applicable_in p pt (Begin_Sequ) =
640 error ("applicable_in: not impl. for " ^ tac2str (Begin_Sequ))
641 | applicable_in p pt (End_Sequ) =
642 error ("applicable_in: not impl. for " ^ tac2str (End_Sequ))
643 | applicable_in p pt (Split_Intersect) =
644 error ("applicable_in: not impl. for " ^ tac2str (Split_Intersect))
645 | applicable_in p pt (End_Intersect) =
646 error ("applicable_in: not impl. for " ^ tac2str (End_Intersect))
648 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
649 if member op = [Pbl,Met] p_
650 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
653 val pp = par_pblobj pt p;
654 val thy' = (get_obj g_domID pt pp):theory';
655 val thy = assoc_thy thy'
656 val metID = (get_obj g_metID pt pp)
657 val {crls,...} = get_met metID
658 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
659 | Res => get_obj g_result pt p;
660 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
662 Const ("List.list.Cons",_) $ _ $ _ =>
663 Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))
664 | Const ("Tools.UniversalList",_) =>
665 Appl (Check_elementwise' (f, pred, (f,asm)))
666 | Const ("List.list.Nil",_) =>
667 Appl (Check_elementwise' (f, pred, (f, asm)))
668 | _ => Notappl ("Check_elementwise not applicable: "^(term2str f)^" should be constants")
671 | applicable_in (p,p_) pt Or_to_List =
672 if member op = [Pbl,Met] p_
673 then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
676 val pp = par_pblobj pt p;
677 val thy' = (get_obj g_domID pt pp):theory';
678 val thy = assoc_thy thy';
680 Frm => get_obj g_form pt p
681 | Res => (fst o (get_obj g_result pt)) p;
682 in (let val ls = or2list f
683 in Appl (Or_to_List' (f, ls)) end)
684 handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
687 | applicable_in p pt (Collect_Trues) =
688 error ("applicable_in: not impl. for "^
689 (tac2str (Collect_Trues)))
691 | applicable_in p pt (Empty_Tac) =
692 Notappl "Empty_Tac is not applicable"
694 | applicable_in (p,p_) pt (Tac id) =
696 val pp = par_pblobj pt p;
697 val thy' = (get_obj g_domID pt pp):theory';
698 val thy = assoc_thy thy';
700 Frm => get_obj g_form pt p
701 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
702 | Res => (fst o (get_obj g_result pt)) p;
704 "subproblem_equation_dummy" =>
706 then Appl (Tac_ (thy, term2str f, id,
707 "subproblem_equation_dummy ("^(term2str f)^")"))
708 else Notappl "applicable only to equations made explicit"
709 | "solve_equation_dummy" =>
710 let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "
712 val (id',f') = split_dummy (term2str f);
713 (*val _= tracing("### applicable_in: f'= "^f');*)
714 (*val _= (term_of o the o (parse thy)) f';*)
715 (*val _= tracing"### applicable_in: solve_equation_dummy";*)
716 in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
717 else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
718 then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
719 else error ("applicable_in: f= " ^ f') end
720 | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
722 | applicable_in p pt End_Proof' = Appl End_Proof''
724 | applicable_in _ _ m =
725 error ("applicable_in called for "^(tac2str m));
728 fun tac2tac_ pt p m =
729 case applicable_in p pt m of
731 | Notappl _ => error ("tac2mstp': fails with"^