4 12345678901234567890123456789012345678901234567890123456789012345678901234567890
5 10 20 30 40 50 60 70 80
10 exception PTREE of string
11 val applicable_in : Ctree.pos' -> Ctree.ctree -> Tac.tac -> Chead.appl
12 (* ---- for tests only: made visible in order to remove the warning --------------------------- *)
13 val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tac.tac -> Tac.tac_
14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15 val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
16 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
20 structure Applicable(**): APPLICABLE(**) =
25 fun rew_info (Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
27 | rew_info (Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
29 | rew_info (Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
31 | rew_info rls = error ("rew_info called with '" ^ rls2str rls ^ "'");
33 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
34 fun from_pblobj_or_detail_thm _ p pt =
36 val (pbl, p', rls') = par_pbl_det pt p
41 val thy' = get_obj g_domID pt p'
42 val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt p')
43 in ("OK", thy', rew_ord', erls, false) end
46 val thy' = get_obj g_domID pt (par_pblobj pt p)
47 val (rew_ord', erls, _) = rew_info rls'
48 in ("OK", thy', rew_ord', erls, false) end
50 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
51 fun from_pblobj_or_detail_calc scrop p pt =
53 val (pbl, p', rls') = par_pbl_det pt p
58 val thy' = get_obj g_domID pt p'
59 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p')
60 val opt = assoc (scr_isa_fns, scrop)
63 SOME isa_fn => ("OK", thy', isa_fn)
64 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
68 val thy' = get_obj g_domID pt (par_pblobj pt p);
69 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
71 case assoc (scr_isa_fns, scrop) of
72 SOME isa_fn => ("OK",thy',isa_fn)
73 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn))
77 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
78 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (e_term, [])
79 | mk_set _ pt p (Const ("Tools.UniversalList", _)) pred =
80 (e_term, if pred <> Const ("Script.Assumptions", bool)
82 else get_assumptions_ pt (p, Res))
83 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =
85 val (bdv,_) = HOLogic.dest_eq eq;
86 val pred = if pred <> Const ("Script.Assumptions",bool)
88 else get_assumptions_ pt (p, Res)
91 error ("check_elementwise: no set " ^ term2str l);
93 (* check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
94 fun check_elementwise thy erls all_results (bdv, asm) =
95 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
97 let val inst_ = map (subst_atomic [sub]) asm
98 in case eval__true thy 1 inst_ [] erls of
99 (asm', true) => ([HOLogic.mk_eq sub], asm')
100 | (_, false) => ([],[])
102 val c' = isalist2list all_results
103 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
104 val subs = map (pair bdv) c''
107 then (all_results, [])
108 else ((apfst ((list2isalist bool) o flat)) o (apsnd flat) o split_list o (map check)) subs
111 (* for Tac-dummies in root-equ only: skip str until "("*)
112 fun split_dummy str =
114 fun scan s' [] = (implode s', "")
115 | scan s' (s :: ss) = if s = " " then (implode s', implode ss)
116 else scan (s' @ [s]) ss;
117 in ((scan []) o Symbol.explode) str end;
119 (* applicability of a tacic wrt. a calc-state (ctree,pos').
120 additionally used by next_tac in the script-interpreter for script-tacs.
121 tests for applicability are so expensive, that results (rewrites!)
122 are kept in the return-value of 'type tac_' *)
123 fun applicable_in _ _ (Tac.Init_Proof (ct', spec)) = Chead.Appl (Tac.Init_Proof' (ct', spec))
124 | applicable_in (p, p_) pt Tac.Model_Problem =
125 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
126 then Chead.Notappl ((Tac.tac2str Tac.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
129 val pI' = case get_obj I pt p of
130 PblObj {origin = (_, (_, pI', _),_), ...} => pI'
131 | _ => error "applicable_in Init_Proof: uncovered case get_obj"
132 val {ppc, ...} = Specify.get_pbt pI'
133 val pbl = Generate.init_pbl ppc
134 in Chead.Appl (Tac.Model_Problem' (pI', pbl, [])) end
135 | applicable_in (p, p_) pt (Tac.Refine_Tacitly pI) =
136 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
137 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
140 val oris = case get_obj I pt p of
141 PblObj {origin = (oris, _, _), ...} => oris
142 | _ => error "applicable_in Refine_Tacitly: uncovered case get_obj"
144 case Specify.refine_ori oris pI of
146 Chead.Appl (Tac.Refine_Tacitly' (pI, pblID, e_domID, e_metID, [](*filled in specify*)))
147 | NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Tacitly pI)) ^ " not applicable")
149 | applicable_in (p, p_) pt (Tac.Refine_Problem pI) =
150 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
151 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
154 val (dI, dI', itms) = case get_obj I pt p of
155 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
157 | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
158 val thy = if dI' = e_domID then dI else dI';
160 case Specify.refine_pbl (assoc_thy thy) pI itms of
161 NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable")
162 | SOME (rf as (pI', _)) =>
164 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable")
165 else Chead.Appl (Tac.Refine_Problem' rf)
167 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
168 | applicable_in (p, p_) pt (Tac.Add_Given ct') =
169 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
170 then Chead.Notappl ((Tac.tac2str (Tac.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
171 else Chead.Appl (Tac.Add_Given' (ct', [(*filled in specify_additem*)]))
172 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
173 | applicable_in (p, p_) pt (Tac.Del_Given ct') =
174 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
175 then Chead.Notappl ((Tac.tac2str (Tac.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
176 else Chead.Appl (Tac.Del_Given' ct')
177 | applicable_in (p, p_) pt (Tac.Add_Find ct') =
178 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
179 then Chead.Notappl ((Tac.tac2str (Tac.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
180 else Chead.Appl (Tac.Add_Find' (ct', [(*filled in specify_additem*)]))
181 | applicable_in (p, p_) pt (Tac.Del_Find ct') =
182 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
183 then Chead.Notappl ((Tac.tac2str (Tac.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
184 else Chead.Appl (Tac.Del_Find' ct')
185 | applicable_in (p, p_) pt (Tac.Add_Relation ct') =
186 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
187 then Chead.Notappl ((Tac.tac2str (Tac.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
188 else Chead.Appl (Tac.Add_Relation' (ct', [(*filled in specify_additem*)]))
189 | applicable_in (p, p_) pt (Tac.Del_Relation ct') =
190 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
191 then Chead.Notappl ((Tac.tac2str (Tac.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
192 else Chead.Appl (Tac.Del_Relation' ct')
193 | applicable_in (p, p_) pt (Tac.Specify_Theory dI) =
194 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
195 then Chead.Notappl ((Tac.tac2str (Tac.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
196 else Chead.Appl (Tac.Specify_Theory' dI)
197 | applicable_in (p, p_) pt (Tac.Specify_Problem pID) =
198 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
199 then Chead.Notappl ((Tac.tac2str (Tac.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
202 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of
203 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
204 => (oris, dI, pI, dI', pI', itms)
205 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
206 val thy = assoc_thy (if dI' = e_domID then dI else dI');
207 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
208 val pbl = if pI' = e_pblID andalso pI = e_pblID
209 then (false, (Generate.init_pbl ppc, []))
210 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
212 Chead.Appl (Tac.Specify_Problem' (pID, pbl))
214 | applicable_in (p, p_) pt (Tac.Specify_Method mID) =
215 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
216 then Chead.Notappl ((Tac.tac2str (Tac.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
217 else Chead.Appl (Tac.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
218 | applicable_in (p, p_) pt (Tac.Apply_Method mI) =
219 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
220 then Chead.Notappl ((Tac.tac2str (Tac.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
223 val (dI, pI, probl, ctxt) = case get_obj I pt p of
224 PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
225 | _ => error "applicable_in Apply_Method: uncovered case get_obj"
226 val {where_, ...} = Specify.get_pbt pI
227 val pres = map (mk_env probl |> subst_atomic) where_
228 val ctxt = if is_e_ctxt ctxt
229 then assoc_thy dI |> Proof_Context.init_global |> insert_assumptions pres
231 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
232 and then decide on Chead.Notappl/Appl accordingly once more.
233 Implement after all tests are running, since this changes
234 overall system behavior*)
236 Chead.Appl (Tac.Apply_Method' (mI, NONE, Selem.e_istate (*filled in solve*), ctxt))
238 | applicable_in (p, p_) _ (Tac.Check_Postcond pI) =
239 if member op = [Pbl, Met] p_
240 then Chead.Notappl ((Tac.tac2str (Tac.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
241 else Chead.Appl (Tac.Check_Postcond' (pI, (e_term, [(*fun solve assigns returnvalue of scr*)])))
242 | applicable_in _ _ (Tac.Take str) = Chead.Appl (Tac.Take' (str2term str)) (* always applicable ?*)
243 | applicable_in _ _ (Tac.Free_Solve) = Chead.Appl (Tac.Free_Solve') (* always applicable *)
244 | applicable_in (p, p_) pt (m as Tac.Rewrite_Inst (subs, thm'')) =
245 if member op = [Pbl, Met] p_
246 then Chead.Notappl ((Tac.tac2str m)^" not for pos " ^ pos'2str (p, p_))
249 val pp = par_pblobj pt p;
250 val thy' = (get_obj g_domID pt pp): theory';
251 val thy = assoc_thy thy';
252 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
253 val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
254 Frm => (get_obj g_form pt p, p)
255 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
256 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
259 val subst = Selem.subs2subst thy subs;
261 case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of
263 Chead.Appl (Tac.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
264 | NONE => Chead.Notappl ((fst thm'')^" not applicable")
266 handle _ => Chead.Notappl ("syntax error in "^(subs2str subs))
268 | applicable_in (p, p_) pt (m as Tac.Rewrite thm'') =
269 if member op = [Pbl, Met] p_
270 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p, p_)))
273 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
274 val thy = assoc_thy thy';
276 Frm => get_obj g_form pt p
277 | Res => (fst o (get_obj g_result pt)) p
278 | _ => error ("applicable_in Rewrite: call by " ^ pos'2str (p, p_));
282 case rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of
283 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
284 | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable")
285 else Chead.Notappl msg
287 | applicable_in (p, p_) pt (m as Tac.Rewrite_Asm thm'') =
288 if member op = [Pbl, Met] p_
289 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_)))
292 val pp = par_pblobj pt p;
293 val thy' = (get_obj g_domID pt pp):theory';
294 val thy = assoc_thy thy';
295 val {rew_ord'=ro',erls=erls,...} = Specify.get_met (get_obj g_metID pt pp);
296 val (f, _) = case p_ of
297 Frm => (get_obj g_form pt p, p)
298 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
299 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
301 case rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of
302 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
303 | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end
304 | applicable_in (p, p_) pt (m as Tac.Detail_Set_Inst (subs, rls)) =
305 if member op = [Pbl, Met] p_
306 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p, p_)))
309 val pp = par_pblobj pt p;
310 val thy' = get_obj g_domID pt pp;
311 val thy = assoc_thy thy';
312 val f = case p_ of Frm => get_obj g_form pt p
313 | Res => (fst o (get_obj g_result pt)) p
314 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
315 val subst = Selem.subs2subst thy subs
317 case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
319 => Chead.Appl (Tac.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
320 | NONE => Chead.Notappl (rls ^ " not applicable")
321 handle _ => Chead.Notappl ("syntax error in " ^ subs2str subs)
323 | applicable_in (p, p_) pt (m as Tac.Rewrite_Set_Inst (subs, rls)) =
324 if member op = [Pbl, Met] p_
325 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_)))
328 val pp = par_pblobj pt p;
329 val thy' = get_obj g_domID pt pp;
330 val thy = assoc_thy thy';
331 val (f, _) = case p_ of
332 Frm => (get_obj g_form pt p, p)
333 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
334 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
335 val subst = Selem.subs2subst thy subs;
337 case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
339 => Chead.Appl (Tac.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
340 | NONE => Chead.Notappl (rls ^ " not applicable")
341 handle _ => Chead.Notappl ("syntax error in " ^(subs2str subs))
343 | applicable_in (p, p_) pt (m as Tac.Rewrite_Set rls) =
344 if member op = [Pbl, Met] p_
345 then Chead.Notappl (Tac.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
348 val pp = par_pblobj pt p;
349 val thy' = get_obj g_domID pt pp;
350 val (f, _) = case p_ of
351 Frm => (get_obj g_form pt p, p)
352 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
353 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
355 case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
357 => Chead.Appl (Tac.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
358 | NONE => Chead.Notappl (rls ^ " not applicable")
360 | applicable_in (p, p_) pt (m as Tac.Detail_Set rls) =
361 if member op = [Pbl, Met] p_
362 then Chead.Notappl (Tac.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
365 val pp = par_pblobj pt p
366 val thy' = get_obj g_domID pt pp
368 Frm => get_obj g_form pt p
369 | Res => (fst o (get_obj g_result pt)) p
370 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
372 case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
373 SOME (f',asm) => Chead.Appl (Tac.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
374 | NONE => Chead.Notappl (rls^" not applicable")
376 | applicable_in _ _ Tac.End_Ruleset = error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Ruleset)
377 | applicable_in (p, p_) pt (m as Tac.Calculate op_) =
378 if member op = [Pbl, Met] p_
379 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_)))
382 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
384 Frm => get_obj g_form pt p
385 | Res => (fst o (get_obj g_result pt)) p
386 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
390 case calculate_ (assoc_thy thy') isa_fn f of
392 => Chead.Appl (Tac.Calculate' (thy', op_, f, (f', (id, string_of_thmI thm))))
393 | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable")
394 else Chead.Notappl msg
396 (*Substitute combines two different kind of "substitution":
397 (1) subst_atomic: for ?a..?z
398 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
399 | applicable_in (p, p_) pt (m as Tac.Substitute sube) =
400 if member op = [Pbl, Met] p_
401 then Chead.Notappl (Tac.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
404 val pp = par_pblobj pt p
405 val thy = assoc_thy (get_obj g_domID pt pp)
407 Frm => get_obj g_form pt p
408 | Res => (fst o (get_obj g_result pt)) p
409 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
410 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
411 val subte = Selem.sube2subte sube
412 val subst = Selem.sube2subst thy sube
413 val ro = assoc_rew_ord rew_ord'
415 if foldl and_ (true, map contains_Var subte)
417 let val f' = subst_atomic subst f
419 then Chead.Notappl (Selem.sube2str sube^" not applicable")
420 else Chead.Appl (Tac.Substitute' (ro, erls, subte, f, f'))
423 case rewrite_terms_ thy ro erls subte f of
424 SOME (f', _) => Chead.Appl (Tac.Substitute' (ro, erls, subte, f, f'))
425 | NONE => Chead.Notappl (Selem.sube2str sube ^ " not applicable")
427 | applicable_in _ _ (Tac.Apply_Assumption cts') =
428 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Apply_Assumption cts'))
429 (* 'logical' applicability wrt. script in locate: Inconsistent? *)
430 | applicable_in _ _ (Tac.Take_Inst ct') =
431 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Take_Inst ct'))
432 | applicable_in (p, p_) pt (m as Tac.Subproblem (domID, pblID)) =
433 if member op = [Pbl,Met] p_
434 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
435 case get_obj g_env pt p of
437 Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [],
438 e_term, [], Selem.e_ctxt(*FIXME.WN150511*), subpbl domID pblID))
439 | NONE => Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_)))
440 else (*somewhere later in the script*)
441 Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [],
442 e_term, [], Selem.e_ctxt, subpbl domID pblID))
443 | applicable_in _ _ (Tac.End_Subproblem) =
444 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Subproblem)
445 | applicable_in _ _ (Tac.CAScmd ct') =
446 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.CAScmd ct'))
447 | applicable_in _ _ (Tac.Split_And) =
448 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Split_And)
449 | applicable_in _ _ (Tac.Conclude_And) =
450 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Conclude_And)
451 | applicable_in _ _ (Tac.Split_Or) =
452 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Split_Or)
453 | applicable_in _ _ (Tac.Conclude_Or) =
454 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Conclude_Or)
455 | applicable_in (p, p_) pt (Tac.Begin_Trans) =
457 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
458 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
459 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
460 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
461 in (Chead.Appl (Tac.Begin_Trans' f))
462 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ term2str f ^ "'")
464 | applicable_in (p, p_) pt (Tac.End_Trans) = (*TODO: check parent branches*)
466 then Chead.Appl (Tac.End_Trans' (get_obj g_result pt p))
467 else Chead.Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
468 | applicable_in _ _ (Tac.Begin_Sequ) =
469 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Begin_Sequ))
470 | applicable_in _ _ (Tac.End_Sequ) =
471 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.End_Sequ))
472 | applicable_in _ _ (Tac.Split_Intersect) =
473 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.Split_Intersect))
474 | applicable_in _ _ (Tac.End_Intersect) =
475 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.End_Intersect))
476 | applicable_in (p, p_) pt (m as Tac.Check_elementwise pred) =
477 if member op = [Pbl,Met] p_
478 then Chead.Notappl ((Tac.tac2str m)^" not for pos " ^ pos'2str (p, p_))
481 val pp = par_pblobj pt p;
482 val thy' = (get_obj g_domID pt pp):theory';
483 val thy = assoc_thy thy'
484 val metID = (get_obj g_metID pt pp)
485 val {crls,...} = Specify.get_met metID
486 val (f, asm) = case p_ of
487 Frm => (get_obj g_form pt p , [])
488 | Res => get_obj g_result pt p
489 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
490 val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
492 Const ("List.list.Cons",_) $ _ $ _ =>
493 Chead.Appl (Tac.Check_elementwise' (f, pred, check_elementwise thy crls f vp))
494 | Const ("Tools.UniversalList",_) =>
495 Chead.Appl (Tac.Check_elementwise' (f, pred, (f,asm)))
496 | Const ("List.list.Nil",_) =>
497 Chead.Appl (Tac.Check_elementwise' (f, pred, (f, asm)))
498 | _ => Chead.Notappl ("Check_elementwise not appl.: " ^ term2str f ^ " should be constants")
500 | applicable_in (p, p_) pt Tac.Or_to_List =
501 if member op = [Pbl, Met] p_
502 then Chead.Notappl ((Tac.tac2str Tac.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
506 Frm => get_obj g_form pt p
507 | Res => (fst o (get_obj g_result pt)) p
508 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
509 in (let val ls = or2list f
510 in Chead.Appl (Tac.Or_to_List' (f, ls)) end)
511 handle _ => Chead.Notappl ("'Or_to_List' not applicable to "^(term2str f))
513 | applicable_in _ _ Tac.Collect_Trues =
514 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Collect_Trues)
515 | applicable_in _ _ Tac.Empty_Tac = Chead.Notappl "Empty_Tac is not applicable"
516 | applicable_in (p, p_) pt (Tac.Tac id) =
518 val pp = par_pblobj pt p;
519 val thy' = (get_obj g_domID pt pp):theory';
520 val thy = assoc_thy thy';
522 Frm => get_obj g_form pt p
523 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
524 | Res => (fst o (get_obj g_result pt)) p
525 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
527 "subproblem_equation_dummy" =>
529 then Chead.Appl (Tac.Tac_ (thy, term2str f, id, "subproblem_equation_dummy (" ^ term2str f ^ ")"))
530 else Chead.Notappl "applicable only to equations made explicit"
531 | "solve_equation_dummy" =>
532 let val (id', f') = split_dummy (term2str f);
534 if id' <> "subproblem_equation_dummy"
535 then Chead.Notappl "no subproblem"
536 else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq
537 then Chead.Appl (Tac.Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
538 else error ("applicable_in: f= " ^ f')
540 | _ => Chead.Appl (Tac.Tac_ (thy, term2str f, id, term2str f))
542 | applicable_in _ _ Tac.End_Proof' = Chead.Appl Tac.End_Proof''
543 | applicable_in _ _ m = error ("applicable_in called for " ^ Tac.tac2str m);
545 fun tac2tac_ pt p m =
546 case applicable_in p pt m of
548 | Chead.Notappl _ => error ("tac2mstp': fails with" ^ Tac.tac2str m);