117 fun scan s' [] = (implode s', "") |
115 fun scan s' [] = (implode s', "") |
118 | scan s' (s :: ss) = if s = " " then (implode s', implode ss) |
116 | scan s' (s :: ss) = if s = " " then (implode s', implode ss) |
119 else scan (s' @ [s]) ss; |
117 else scan (s' @ [s]) ss; |
120 in ((scan []) o Symbol.explode) str end; |
118 in ((scan []) o Symbol.explode) str end; |
121 |
119 |
122 (* applicability of a tacic wrt. a calc-state (ctree, pos'). |
|
123 additionally used by find_next_step. |
|
124 tests for applicability are so expensive, that results (rewrites!) |
|
125 are kept in the return-value of 'type tac_' *) |
|
126 fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Applicable.Yes (Tactic.Init_Proof' (ct', spec)) |
|
127 | applicable_in (p, p_) pt Tactic.Model_Problem = |
|
128 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then |
|
129 Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
130 else |
|
131 let |
|
132 val pI' = case Ctree.get_obj I pt p of |
|
133 Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI' |
|
134 | _ => error "applicable_in Init_Proof: uncovered case Ctree.get_obj" |
|
135 val {ppc, ...} = Specify.get_pbt pI' |
|
136 val pbl = Generate.init_pbl ppc |
|
137 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end |
|
138 | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) = |
|
139 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
140 then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
141 else |
|
142 let |
|
143 val oris = case Ctree.get_obj I pt p of |
|
144 Ctree.PblObj {origin = (oris, _, _), ...} => oris |
|
145 | _ => error "applicable_in Refine_Tacitly: uncovered case Ctree.get_obj" |
|
146 in |
|
147 case Specify.refine_ori oris pI of |
|
148 SOME pblID => |
|
149 Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*))) |
|
150 | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable") |
|
151 end |
|
152 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) = |
|
153 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
154 then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_))) |
|
155 else |
|
156 let |
|
157 val (dI, dI', itms) = case Ctree.get_obj I pt p of |
|
158 Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...} |
|
159 => (dI, dI', itms) |
|
160 | _ => error "applicable_in Refine_Problem: uncovered case Ctree.get_obj" |
|
161 val thy = if dI' = ThyC.id_empty then dI else dI'; |
|
162 in |
|
163 case Specify.refine_pbl (ThyC.get_theory thy) pI itms of |
|
164 NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable") |
|
165 | SOME (rf as (pI', _)) => |
|
166 if pI' = pI |
|
167 then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable") |
|
168 else Applicable.Yes (Tactic.Refine_Problem' rf) |
|
169 end |
|
170 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*) |
|
171 | applicable_in (p, p_) pt (Tactic.Add_Given ct') = |
|
172 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
173 then Applicable.No ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
174 else Applicable.Yes (Tactic.Add_Given' (ct', [(*filled in specify_additem*)])) |
|
175 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*) |
|
176 | applicable_in (p, p_) pt (Tactic.Del_Given ct') = |
|
177 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
178 then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
179 else Applicable.Yes (Tactic.Del_Given' ct') |
|
180 | applicable_in (p, p_) pt (Tactic.Add_Find ct') = |
|
181 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
182 then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
183 else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)])) |
|
184 | applicable_in (p, p_) pt (Tactic.Del_Find ct') = |
|
185 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
186 then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
187 else Applicable.Yes (Tactic.Del_Find' ct') |
|
188 | applicable_in (p, p_) pt (Tactic.Add_Relation ct') = |
|
189 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
190 then Applicable.No ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
191 else Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)])) |
|
192 | applicable_in (p, p_) pt (Tactic.Del_Relation ct') = |
|
193 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
194 then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
195 else Applicable.Yes (Tactic.Del_Relation' ct') |
|
196 | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) = |
|
197 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
198 then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
199 else Applicable.Yes (Tactic.Specify_Theory' dI) |
|
200 | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) = |
|
201 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
202 then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
203 else |
|
204 let |
|
205 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of |
|
206 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...} |
|
207 => (oris, dI, pI, dI', pI', itms) |
|
208 | _ => error "applicable_in Specify_Problem: uncovered case Ctree.get_obj" |
|
209 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI'); |
|
210 val {ppc, where_, prls, ...} = Specify.get_pbt pID; |
|
211 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty |
|
212 then (false, (Generate.init_pbl ppc, [])) |
|
213 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris; |
|
214 in |
|
215 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl)) |
|
216 end |
|
217 | applicable_in (p, p_) pt (Tactic.Specify_Method mID) = |
|
218 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
219 then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
220 else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)])) |
|
221 | applicable_in (p, p_) pt (Tactic.Apply_Method mI) = |
|
222 if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res |
|
223 then Applicable.No ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
224 else |
|
225 let |
|
226 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of |
|
227 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) |
|
228 | _ => error "applicable_in Apply_Method: uncovered case Ctree.get_obj" |
|
229 val {where_, ...} = Specify.get_pbt pI |
|
230 val pres = map (Model.mk_env probl |> subst_atomic) where_ |
|
231 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*) |
|
232 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres |
|
233 else ctxt |
|
234 (*TODO.WN110416 here do evalprecond according to fun check_preconds' |
|
235 and then decide on Applicable.No/Applicable.Yes accordingly once more. |
|
236 Implement after all tests are running, since this changes |
|
237 overall system behavior*) |
|
238 in |
|
239 Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt)) |
|
240 end |
|
241 (*required for corner cases, e.g. test setup in inssort.sml*) |
|
242 | applicable_in pos _ Tactic.Empty_Tac = Applicable.No "Empty_Tac is not applicable" |
|
243 | applicable_in pos _ m = |
|
244 raise ERROR ("applicable_in called for " ^ Tactic.input_to_string m ^ " at" ^ Pos.pos'2str pos); |
|
245 (*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------* ) |
|
246 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) = |
|
247 if member op = [Pos.Pbl, Pos.Met] p_ |
|
248 then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
249 else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty)) |
|
250 | applicable_in _ _ (Tactic.Take str) = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*) |
|
251 | applicable_in _ _ (Tactic.Free_Solve) = Applicable.Yes (Tactic.Free_Solve') (* always applicable *) |
|
252 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) = |
|
253 if member op = [Pos.Pbl, Pos.Met] p_ |
|
254 then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_)) |
|
255 else |
|
256 let |
|
257 val pp = Ctree.par_pblobj pt p; |
|
258 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
259 val thy = ThyC.get_theory thy'; |
|
260 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp); |
|
261 val (f, _) = case p_ of (*p 12.4.00 unnecessary*) |
|
262 Frm => (Ctree.get_obj Ctree.g_form pt p, p) |
|
263 | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) |
|
264 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
265 in |
|
266 let |
|
267 val subst = Subst.T_from_input thy subs; |
|
268 in |
|
269 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of |
|
270 SOME (f',asm) => |
|
271 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) |
|
272 | NONE => Applicable.No ((fst thm'')^" not applicable") |
|
273 end |
|
274 handle _ => Applicable.No ("syntax error in "^(subs2str subs)) |
|
275 end |
|
276 | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') = |
|
277 if member op = [Pos.Pbl, Pos.Met] p_ |
|
278 then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_))) |
|
279 else |
|
280 let |
|
281 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt; |
|
282 val thy = ThyC.get_theory thy'; |
|
283 val f = case p_ of |
|
284 Frm => Ctree.get_obj Ctree.g_form pt p |
|
285 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
286 | _ => error ("applicable_in Rewrite: call by " ^ Pos.pos'2str (p, p_)); |
|
287 in |
|
288 if msg = "OK" |
|
289 then |
|
290 case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of |
|
291 SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm))) |
|
292 | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable") |
|
293 else Applicable.No msg |
|
294 end |
|
295 | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) = |
|
296 if member op = [Pos.Pbl, Pos.Met] p_ |
|
297 then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_))) |
|
298 else |
|
299 let |
|
300 val pp = Ctree.par_pblobj pt p; |
|
301 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
302 val thy = ThyC.get_theory thy'; |
|
303 val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p |
|
304 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
305 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
306 val subst = Subst.T_from_input thy subs |
|
307 in |
|
308 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of |
|
309 SOME (f', asm) |
|
310 => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) |
|
311 | NONE => Applicable.No (rls ^ " not applicable") |
|
312 handle _ => Applicable.No ("syntax error in " ^ subs2str subs) |
|
313 end |
|
314 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) = |
|
315 if member op = [Pos.Pbl, Pos.Met] p_ |
|
316 then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_))) |
|
317 else |
|
318 let |
|
319 val pp = Ctree.par_pblobj pt p; |
|
320 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
321 val thy = ThyC.get_theory thy'; |
|
322 val (f, _) = case p_ of |
|
323 Frm => (Ctree.get_obj Ctree.g_form pt p, p) |
|
324 | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) |
|
325 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
326 val subst = Subst.T_from_input thy subs; |
|
327 in |
|
328 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of |
|
329 SOME (f',asm) |
|
330 => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm))) |
|
331 | NONE => Applicable.No (rls ^ " not applicable") |
|
332 handle _ => Applicable.No ("syntax error in " ^(subs2str subs)) |
|
333 end |
|
334 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) = |
|
335 if member op = [Pos.Pbl, Pos.Met] p_ |
|
336 then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
337 else |
|
338 let |
|
339 val pp = Ctree.par_pblobj pt p; |
|
340 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
341 val (f, _) = case p_ of |
|
342 Frm => (Ctree.get_obj Ctree.g_form pt p, p) |
|
343 | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p) |
|
344 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
345 in |
|
346 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of |
|
347 SOME (f', asm) |
|
348 => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
|
349 | NONE => Applicable.No (rls ^ " not applicable") |
|
350 end |
|
351 | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) = |
|
352 if member op = [Pos.Pbl, Pos.Met] p_ |
|
353 then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
354 else |
|
355 let |
|
356 val pp = Ctree.par_pblobj pt p |
|
357 val thy' = Ctree.get_obj Ctree.g_domID pt pp |
|
358 val f = case p_ of |
|
359 Frm => Ctree.get_obj Ctree.g_form pt p |
|
360 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
361 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
362 in |
|
363 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of |
|
364 SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
|
365 | NONE => Applicable.No (rls^" not applicable") |
|
366 end |
|
367 | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset) |
|
368 | applicable_in (p, p_) pt (m as Tactic.Calculate op_) = |
|
369 if member op = [Pos.Pbl, Pos.Met] p_ |
|
370 then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_))) |
|
371 else |
|
372 let |
|
373 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt; |
|
374 val f = case p_ of |
|
375 Frm => Ctree.get_obj Ctree.g_form pt p |
|
376 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
377 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
378 in |
|
379 if msg = "OK" |
|
380 then |
|
381 case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of |
|
382 SOME (f', (id, thm)) |
|
383 => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm)))) |
|
384 | NONE => Applicable.No ("'calculate "^op_^"' not applicable") |
|
385 else Applicable.No msg |
|
386 end |
|
387 (*Substitute combines two different kind of "substitution": |
|
388 (1) subst_atomic: for ?a..?z |
|
389 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*) |
|
390 | applicable_in (p, p_) pt (m as Tactic.Substitute sube) = |
|
391 if member op = [Pos.Pbl, Pos.Met] p_ |
|
392 then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
393 else |
|
394 let |
|
395 val pp = Ctree.par_pblobj pt p |
|
396 val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp) |
|
397 val f = case p_ of |
|
398 Frm => Ctree.get_obj Ctree.g_form pt p |
|
399 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
400 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
401 val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) |
|
402 val subte = Subst.input_to_terms sube |
|
403 val subst = Subst.T_from_string_eqs thy sube |
|
404 val ro = Rewrite_Ord.assoc_rew_ord rew_ord' |
|
405 in |
|
406 if foldl and_ (true, map TermC.contains_Var subte) |
|
407 then (*1*) |
|
408 let val f' = subst_atomic subst f |
|
409 in if f = f' |
|
410 then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") |
|
411 else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) |
|
412 end |
|
413 else (*2*) |
|
414 case Rewrite.rewrite_terms_ thy ro erls subte f of |
|
415 SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f')) |
|
416 | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable") |
|
417 end |
|
418 | applicable_in _ _ (Tactic.Apply_Assumption cts') = |
|
419 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts')) |
|
420 (* 'logical' applicability wrt. script in locate_input_tactic: Inconsistent? *) |
|
421 | applicable_in _ _ (Tactic.Take_Inst ct') = |
|
422 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Take_Inst ct')) |
|
423 | applicable_in (p, p_) _ (m as Tactic.Subproblem (domID, pblID)) = |
|
424 if Pos.on_specification p_ |
|
425 then |
|
426 Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
427 else (*some fields filled later in LI*) |
|
428 Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [], |
|
429 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID)) |
|
430 | applicable_in _ _ (Tactic.End_Subproblem) = |
|
431 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem) |
|
432 | applicable_in _ _ (Tactic.CAScmd ct') = |
|
433 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.CAScmd ct')) |
|
434 | applicable_in _ _ (Tactic.Split_And) = |
|
435 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_And) |
|
436 | applicable_in _ _ (Tactic.Conclude_And) = |
|
437 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_And) |
|
438 | applicable_in _ _ (Tactic.Split_Or) = |
|
439 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Split_Or) |
|
440 | applicable_in _ _ (Tactic.Conclude_Or) = |
|
441 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Conclude_Or) |
|
442 | applicable_in (p, p_) pt (Tactic.Begin_Trans) = |
|
443 let |
|
444 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*) |
|
445 Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p) |
|
446 | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p) |
|
447 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
448 in (Applicable.Yes (Tactic.Begin_Trans' f)) |
|
449 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'") |
|
450 end |
|
451 | applicable_in (p, p_) pt (Tactic.End_Trans) = (*TODO: check parent branches*) |
|
452 if p_ = Pos.Res |
|
453 then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p)) |
|
454 else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence" |
|
455 | applicable_in _ _ (Tactic.Begin_Sequ) = |
|
456 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ)) |
|
457 | applicable_in _ _ (Tactic.End_Sequ) = |
|
458 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Sequ)) |
|
459 | applicable_in _ _ (Tactic.Split_Intersect) = |
|
460 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Split_Intersect)) |
|
461 | applicable_in _ _ (Tactic.End_Intersect) = |
|
462 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect)) |
|
463 | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) = |
|
464 if member op = [Pos.Pbl, Pos.Met] p_ |
|
465 then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_)) |
|
466 else |
|
467 let |
|
468 val pp = Ctree.par_pblobj pt p; |
|
469 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
470 val thy = ThyC.get_theory thy' |
|
471 val metID = (Ctree.get_obj Ctree.g_metID pt pp) |
|
472 val {crls, ...} = Specify.get_met metID |
|
473 val (f, asm) = case p_ of |
|
474 Frm => (Ctree.get_obj Ctree.g_form pt p , []) |
|
475 | Pos.Res => Ctree.get_obj Ctree.g_result pt p |
|
476 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
477 val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f; |
|
478 in |
|
479 Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm))) |
|
480 end |
|
481 | applicable_in (p, p_) pt Tactic.Or_to_List = |
|
482 if member op = [Pos.Pbl, Pos.Met] p_ |
|
483 then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_))) |
|
484 else |
|
485 let |
|
486 val f = case p_ of |
|
487 Frm => Ctree.get_obj Ctree.g_form pt p |
|
488 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
489 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
490 in (let val ls = Prog_Expr.or2list f |
|
491 in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end) |
|
492 handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f) |
|
493 end |
|
494 | applicable_in _ _ Tactic.Collect_Trues = |
|
495 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues) |
|
496 | applicable_in _ _ Tactic.Empty_Tac = Applicable.No "Empty_Tac is not applicable" |
|
497 | applicable_in (p, p_) pt (Tactic.Tac id) = |
|
498 let |
|
499 val pp = Ctree.par_pblobj pt p; |
|
500 val thy' = Ctree.get_obj Ctree.g_domID pt pp; |
|
501 val thy = ThyC.get_theory thy'; |
|
502 val f = case p_ of |
|
503 Frm => Ctree.get_obj Ctree.g_form pt p |
|
504 | Pos.Pbl => error "applicable_in (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl" |
|
505 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
506 | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_)); |
|
507 in case id of |
|
508 "subproblem_equation_dummy" => |
|
509 if TermC.is_expliceq f |
|
510 then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")")) |
|
511 else Applicable.No "applicable only to equations made explicit" |
|
512 | "solve_equation_dummy" => |
|
513 let val (id', f') = split_dummy (UnparseC.term f); |
|
514 in |
|
515 if id' <> "subproblem_equation_dummy" |
|
516 then Applicable.No "no subproblem" |
|
517 else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq |
|
518 then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]")) |
|
519 else error ("applicable_in: f= " ^ f') |
|
520 end |
|
521 | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f)) |
|
522 end |
|
523 | applicable_in _ _ Tactic.End_Proof' = Applicable.Yes Tactic.End_Proof'' |
|
524 | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.input_to_string m); |
|
525 ( *-----^^^^^- solve ---------------------------------------------------------------------------*) |
|
526 |
|
527 fun tac2tac_ pt p m = |
|
528 case applicable_in p pt m of |
|
529 Applicable.Yes m' => m' |
|
530 | Applicable.No _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m); |
|
531 |
|
532 (**)end(**); |
120 (**)end(**); |