reorganise struct. ThmC, part 3 end
1 (* Title: Is a tacitc applicable ?
2 TODO: allocate these functions in appropriate structures
4 (c) due to copyright terms
9 exception PTREE of string
10 datatype appl = Appl of Tactic.T | Notappl of string
11 val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> appl
12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13 val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
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(**) =
26 fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
28 | rew_info (Rule_Set.Seqence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
30 | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
32 | rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
34 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
35 fun from_pblobj_or_detail_thm _ p pt =
37 val (pbl, p', rls') = parent_node pt p
42 val thy' = get_obj g_domID pt p'
43 val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt p')
44 in ("OK", thy', rew_ord', erls, false) end
47 val thy' = get_obj g_domID pt (par_pblobj pt p)
48 val (rew_ord', erls, _) = rew_info rls'
49 in ("OK", thy', rew_ord', erls, false) end
51 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
52 fun from_pblobj_or_detail_calc scrop p pt =
54 val (pbl, p', rls') = parent_node pt p
59 val thy' = get_obj g_domID pt p'
60 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p')
61 val opt = assoc (scr_isa_fns, scrop)
64 SOME isa_fn => ("OK", thy', isa_fn)
65 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn))
69 val thy' = get_obj g_domID pt (par_pblobj pt p);
70 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
72 case assoc (scr_isa_fns, scrop) of
73 SOME isa_fn => ("OK",thy',isa_fn)
74 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn))
78 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
79 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (TermC.empty, [])
80 | mk_set _ pt p (Const ("ListC.UniversalList", _)) pred =
81 (TermC.empty, if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
83 else Ctree.get_assumptions pt (p, Res))
84 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =
86 val (bdv,_) = HOLogic.dest_eq eq;
87 val pred = if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
89 else Ctree.get_assumptions pt (p, Res)
92 error ("check_elementwise: no set " ^ UnparseC.term l);
94 (* check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
95 fun check_elementwise thy erls all_results (bdv, asm) =
96 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
98 let val inst_ = map (subst_atomic [sub]) asm
99 in case Rewrite.eval__true thy 1 inst_ [] erls of
100 (asm', true) => ([HOLogic.mk_eq sub], asm')
101 | (_, false) => ([],[])
103 val c' = TermC.isalist2list all_results
104 val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
105 val subs = map (pair bdv) c''
108 then (all_results, [])
109 else ((apfst ((TermC.list2isalist HOLogic.boolT) o flat)) o (apsnd flat) o split_list o (map check)) subs
112 (* for Tac-dummies in root-equ only: skip str until "("*)
113 fun split_dummy str =
115 fun scan s' [] = (implode s', "")
116 | scan s' (s :: ss) = if s = " " then (implode s', implode ss)
117 else scan (s' @ [s]) ss;
118 in ((scan []) o Symbol.explode) str end;
121 Appl of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
122 | Notappl of string (* tactic is NOT applicable *)
124 (* applicability of a tacic wrt. a calc-state (ctree, pos').
125 additionally used by find_next_step.
126 tests for applicability are so expensive, that results (rewrites!)
127 are kept in the return-value of 'type tac_' *)
128 fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))
129 | applicable_in (p, p_) pt Tactic.Model_Problem =
130 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
131 then Notappl ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
134 val pI' = case get_obj I pt p of
135 PblObj {origin = (_, (_, pI', _),_), ...} => pI'
136 | _ => error "applicable_in Init_Proof: uncovered case get_obj"
137 val {ppc, ...} = Specify.get_pbt pI'
138 val pbl = Generate.init_pbl ppc
139 in Appl (Tactic.Model_Problem' (pI', pbl, [])) end
140 | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) =
141 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
142 then Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
145 val oris = case get_obj I pt p of
146 PblObj {origin = (oris, _, _), ...} => oris
147 | _ => error "applicable_in Refine_Tacitly: uncovered case get_obj"
149 case Specify.refine_ori oris pI of
151 Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.e_domID, Celem.e_metID, [](*filled in specify*)))
152 | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
154 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
155 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
156 then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
159 val (dI, dI', itms) = case get_obj I pt p of
160 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
162 | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
163 val thy = if dI' = ThyC.e_domID then dI else dI';
165 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
166 NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
167 | SOME (rf as (pI', _)) =>
169 then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
170 else Appl (Tactic.Refine_Problem' rf)
172 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
173 | applicable_in (p, p_) pt (Tactic.Add_Given ct') =
174 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
175 then Notappl ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
176 else Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
177 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
178 | applicable_in (p, p_) pt (Tactic.Del_Given ct') =
179 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
180 then Notappl ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
181 else Appl (Tactic.Del_Given' ct')
182 | applicable_in (p, p_) pt (Tactic.Add_Find ct') =
183 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
184 then Notappl ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
185 else Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
186 | applicable_in (p, p_) pt (Tactic.Del_Find ct') =
187 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
188 then Notappl ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
189 else Appl (Tactic.Del_Find' ct')
190 | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =
191 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
192 then Notappl ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
193 else Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
194 | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =
195 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
196 then Notappl ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
197 else Appl (Tactic.Del_Relation' ct')
198 | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =
199 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
200 then Notappl ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
201 else Appl (Tactic.Specify_Theory' dI)
202 | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) =
203 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
204 then Notappl ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
207 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of
208 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
209 => (oris, dI, pI, dI', pI', itms)
210 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
211 val thy = Celem.assoc_thy (if dI' = ThyC.e_domID then dI else dI');
212 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
213 val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
214 then (false, (Generate.init_pbl ppc, []))
215 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
217 Appl (Tactic.Specify_Problem' (pID, pbl))
219 | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =
220 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
221 then Notappl ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
222 else Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
223 | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =
224 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
225 then Notappl ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
228 val (dI, pI, probl, ctxt) = case get_obj I pt p of
229 PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
230 | _ => error "applicable_in Apply_Method: uncovered case get_obj"
231 val {where_, ...} = Specify.get_pbt pI
232 val pres = map (Model.mk_env probl |> subst_atomic) where_
233 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
234 then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
236 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
237 and then decide on Notappl/Appl accordingly once more.
238 Implement after all tests are running, since this changes
239 overall system behavior*)
241 Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
243 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
244 if member op = [Pbl, Met] p_
245 then Notappl ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
246 else Appl (Tactic.Check_Postcond' (pI, TermC.empty))
247 | applicable_in _ _ (Tactic.Take str) = Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
248 | applicable_in _ _ (Tactic.Free_Solve) = Appl (Tactic.Free_Solve') (* always applicable *)
249 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) =
250 if member op = [Pbl, Met] p_
251 then Notappl ((Tactic.input_to_string m)^" not for pos " ^ pos'2str (p, p_))
254 val pp = par_pblobj pt p;
255 val thy' = get_obj g_domID pt pp;
256 val thy = Celem.assoc_thy thy';
257 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
258 val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
259 Frm => (get_obj g_form pt p, p)
260 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
261 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
264 val subst = Selem.subs2subst thy subs;
266 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
268 Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
269 | NONE => Notappl ((fst thm'')^" not applicable")
271 handle _ => Notappl ("syntax error in "^(subs2str subs))
273 | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') =
274 if member op = [Pbl, Met] p_
275 then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
278 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
279 val thy = Celem.assoc_thy thy';
281 Frm => get_obj g_form pt p
282 | Res => (fst o (get_obj g_result pt)) p
283 | _ => error ("applicable_in Rewrite: call by " ^ pos'2str (p, p_));
287 case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
288 SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
289 | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
292 | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) =
293 if member op = [Pbl, Met] p_
294 then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
297 val pp = par_pblobj pt p;
298 val thy' = get_obj g_domID pt pp;
299 val thy = Celem.assoc_thy thy';
300 val f = case p_ of Frm => get_obj g_form pt p
301 | Res => (fst o (get_obj g_result pt)) p
302 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
303 val subst = Selem.subs2subst thy subs
305 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
307 => Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
308 | NONE => Notappl (rls ^ " not applicable")
309 handle _ => Notappl ("syntax error in " ^ subs2str subs)
311 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) =
312 if member op = [Pbl, Met] p_
313 then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
316 val pp = par_pblobj pt p;
317 val thy' = get_obj g_domID pt pp;
318 val thy = Celem.assoc_thy thy';
319 val (f, _) = case p_ of
320 Frm => (get_obj g_form pt p, p)
321 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
322 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
323 val subst = Selem.subs2subst thy subs;
325 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
327 => Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
328 | NONE => Notappl (rls ^ " not applicable")
329 handle _ => Notappl ("syntax error in " ^(subs2str subs))
331 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) =
332 if member op = [Pbl, Met] p_
333 then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
336 val pp = par_pblobj pt p;
337 val thy' = get_obj g_domID pt pp;
338 val (f, _) = case p_ of
339 Frm => (get_obj g_form pt p, p)
340 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
341 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
343 case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
345 => Appl (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
346 | NONE => Notappl (rls ^ " not applicable")
348 | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =
349 if member op = [Pbl, Met] p_
350 then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
353 val pp = par_pblobj pt p
354 val thy' = get_obj g_domID pt pp
356 Frm => get_obj g_form pt p
357 | Res => (fst o (get_obj g_result pt)) p
358 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
360 case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
361 SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
362 | NONE => Notappl (rls^" not applicable")
364 | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
365 | applicable_in (p, p_) pt (m as Tactic.Calculate op_) =
366 if member op = [Pbl, Met] p_
367 then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
370 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
372 Frm => get_obj g_form pt p
373 | Res => (fst o (get_obj g_result pt)) p
374 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
378 case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
380 => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
381 | NONE => Notappl ("'calculate "^op_^"' not applicable")
384 (*Substitute combines two different kind of "substitution":
385 (1) subst_atomic: for ?a..?z
386 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
387 | applicable_in (p, p_) pt (m as Tactic.Substitute sube) =
388 if member op = [Pbl, Met] p_
389 then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
392 val pp = par_pblobj pt p
393 val thy = Celem.assoc_thy (get_obj g_domID pt pp)
395 Frm => get_obj g_form pt p
396 | Res => (fst o (get_obj g_result pt)) p
397 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
398 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
399 val subte = Selem.sube2subte sube
400 val subst = Selem.sube2subst thy sube
401 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
403 if foldl and_ (true, map TermC.contains_Var subte)
405 let val f' = subst_atomic subst f
407 then Notappl (Selem.sube2str sube^" not applicable")
408 else Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
411 case Rewrite.rewrite_terms_ thy ro erls subte f of
412 SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
413 | NONE => Notappl (Selem.sube2str sube ^ " not applicable")
415 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
416 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
417 (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *)
418 | applicable_in _ _ (Tactic.Take_Inst ct') =
419 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct'))
420 | applicable_in (p, p_) _ (m as Tactic.Subproblem (domID, pblID)) =
421 if Pos.on_specification p_
423 Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
424 else (*some fields filled later in LI*)
425 Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
426 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
427 | applicable_in _ _ (Tactic.End_Subproblem) =
428 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
429 | applicable_in _ _ (Tactic.CAScmd ct') =
430 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct'))
431 | applicable_in _ _ (Tactic.Split_And) =
432 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_And)
433 | applicable_in _ _ (Tactic.Conclude_And) =
434 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And)
435 | applicable_in _ _ (Tactic.Split_Or) =
436 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or)
437 | applicable_in _ _ (Tactic.Conclude_Or) =
438 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or)
439 | applicable_in (p, p_) pt (Tactic.Begin_Trans) =
441 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
442 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
443 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
444 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
445 in (Appl (Tactic.Begin_Trans' f))
446 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
448 | applicable_in (p, p_) pt (Tactic.End_Trans) = (*TODO: check parent branches*)
450 then Appl (Tactic.End_Trans' (get_obj g_result pt p))
451 else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
452 | applicable_in _ _ (Tactic.Begin_Sequ) =
453 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
454 | applicable_in _ _ (Tactic.End_Sequ) =
455 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ))
456 | applicable_in _ _ (Tactic.Split_Intersect) =
457 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect))
458 | applicable_in _ _ (Tactic.End_Intersect) =
459 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
460 | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) =
461 if member op = [Pbl, Met] p_
462 then Notappl ((Tactic.input_to_string m) ^ " not for pos " ^ pos'2str (p, p_))
465 val pp = par_pblobj pt p;
466 val thy' = get_obj g_domID pt pp;
467 val thy = Celem.assoc_thy thy'
468 val metID = (get_obj g_metID pt pp)
469 val {crls, ...} = Specify.get_met metID
470 val (f, asm) = case p_ of
471 Frm => (get_obj g_form pt p , [])
472 | Res => get_obj g_result pt p
473 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
474 val vp = (ThyC.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
476 Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
478 | applicable_in (p, p_) pt Tactic.Or_to_List =
479 if member op = [Pbl, Met] p_
480 then Notappl ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
484 Frm => get_obj g_form pt p
485 | Res => (fst o (get_obj g_result pt)) p
486 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
487 in (let val ls = Prog_Expr.or2list f
488 in Appl (Tactic.Or_to_List' (f, ls)) end)
489 handle _ => Notappl ("'Or_to_List' not applicable to " ^ UnparseC.term f)
491 | applicable_in _ _ Tactic.Collect_Trues =
492 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
493 | applicable_in _ _ Tactic.Empty_Tac = Notappl "Empty_Tac is not applicable"
494 | applicable_in (p, p_) pt (Tactic.Tac id) =
496 val pp = par_pblobj pt p;
497 val thy' = get_obj g_domID pt pp;
498 val thy = Celem.assoc_thy thy';
500 Frm => get_obj g_form pt p
501 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
502 | Res => (fst o (get_obj g_result pt)) p
503 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
505 "subproblem_equation_dummy" =>
506 if TermC.is_expliceq f
507 then Appl (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
508 else Notappl "applicable only to equations made explicit"
509 | "solve_equation_dummy" =>
510 let val (id', f') = split_dummy (UnparseC.term f);
512 if id' <> "subproblem_equation_dummy"
513 then Notappl "no subproblem"
514 else if (ThyC.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
515 then Appl (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
516 else error ("applicable_in: f= " ^ f')
518 | _ => Appl (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
520 | applicable_in _ _ Tactic.End_Proof' = Appl Tactic.End_Proof''
521 | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.input_to_string m);
523 fun tac2tac_ pt p m =
524 case applicable_in p pt m of
526 | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);