19 structure Applicable(**): APPLICABLE(**) = |
19 structure Applicable(**): APPLICABLE(**) = |
20 struct |
20 struct |
21 (**) |
21 (**) |
22 open Ctree |
22 open Ctree |
23 |
23 |
24 fun rew_info (Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
24 fun rew_info (Celem.Rls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
25 (rew_ord', erls, ca) |
25 (rew_ord', erls, ca) |
26 | rew_info (Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
26 | rew_info (Celem.Seq {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
27 (rew_ord', erls, ca) |
27 (rew_ord', erls, ca) |
28 | rew_info (Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
28 | rew_info (Celem.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) = |
29 (rew_ord', erls, ca) |
29 (rew_ord', erls, ca) |
30 | rew_info rls = error ("rew_info called with '" ^ rls2str rls ^ "'"); |
30 | rew_info rls = error ("rew_info called with '" ^ Celem.rls2str rls ^ "'"); |
31 |
31 |
32 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*) |
32 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*) |
33 fun from_pblobj_or_detail_thm _ p pt = |
33 fun from_pblobj_or_detail_thm _ p pt = |
34 let |
34 let |
35 val (pbl, p', rls') = par_pbl_det pt p |
35 val (pbl, p', rls') = par_pbl_det pt p |
58 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p') |
58 val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p') |
59 val opt = assoc (scr_isa_fns, scrop) |
59 val opt = assoc (scr_isa_fns, scrop) |
60 in |
60 in |
61 case opt of |
61 case opt of |
62 SOME isa_fn => ("OK", thy', isa_fn) |
62 SOME isa_fn => ("OK", thy', isa_fn) |
63 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn)) |
63 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Celem.e_evalfn)) |
64 end |
64 end |
65 else |
65 else |
66 let |
66 let |
67 val thy' = get_obj g_domID pt (par_pblobj pt p); |
67 val thy' = get_obj g_domID pt (par_pblobj pt p); |
68 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
68 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) |
69 in |
69 in |
70 case assoc (scr_isa_fns, scrop) of |
70 case assoc (scr_isa_fns, scrop) of |
71 SOME isa_fn => ("OK",thy',isa_fn) |
71 SOME isa_fn => ("OK",thy',isa_fn) |
72 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", e_evalfn)) |
72 | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Celem.e_evalfn)) |
73 end |
73 end |
74 end; |
74 end; |
75 |
75 |
76 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
76 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) |
77 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (e_term, []) |
77 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (Celem.e_term, []) |
78 | mk_set _ pt p (Const ("Tools.UniversalList", _)) pred = |
78 | mk_set _ pt p (Const ("Tools.UniversalList", _)) pred = |
79 (e_term, if pred <> Const ("Script.Assumptions", HOLogic.boolT) |
79 (Celem.e_term, if pred <> Const ("Script.Assumptions", HOLogic.boolT) |
80 then [pred] |
80 then [pred] |
81 else get_assumptions_ pt (p, Res)) |
81 else get_assumptions_ pt (p, Res)) |
82 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred = |
82 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred = |
83 let |
83 let |
84 val (bdv,_) = HOLogic.dest_eq eq; |
84 val (bdv,_) = HOLogic.dest_eq eq; |
85 val pred = if pred <> Const ("Script.Assumptions", HOLogic.boolT) |
85 val pred = if pred <> Const ("Script.Assumptions", HOLogic.boolT) |
86 then [pred] |
86 then [pred] |
87 else get_assumptions_ pt (p, Res) |
87 else get_assumptions_ pt (p, Res) |
88 in (bdv, pred) end |
88 in (bdv, pred) end |
89 | mk_set _ _ _ l _ = |
89 | mk_set _ _ _ l _ = |
90 error ("check_elementwise: no set " ^ term2str l); |
90 error ("check_elementwise: no set " ^ Celem.term2str l); |
91 |
91 |
92 (* check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*) |
92 (* check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*) |
93 fun check_elementwise thy erls all_results (bdv, asm) = |
93 fun check_elementwise thy erls all_results (bdv, asm) = |
94 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*) |
94 let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*) |
95 fun check sub = |
95 fun check sub = |
140 PblObj {origin = (oris, _, _), ...} => oris |
140 PblObj {origin = (oris, _, _), ...} => oris |
141 | _ => error "applicable_in Refine_Tacitly: uncovered case get_obj" |
141 | _ => error "applicable_in Refine_Tacitly: uncovered case get_obj" |
142 in |
142 in |
143 case Specify.refine_ori oris pI of |
143 case Specify.refine_ori oris pI of |
144 SOME pblID => |
144 SOME pblID => |
145 Chead.Appl (Tac.Refine_Tacitly' (pI, pblID, e_domID, e_metID, [](*filled in specify*))) |
145 Chead.Appl (Tac.Refine_Tacitly' (pI, pblID, Celem.e_domID, Celem.e_metID, [](*filled in specify*))) |
146 | NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Tacitly pI)) ^ " not applicable") |
146 | NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Tacitly pI)) ^ " not applicable") |
147 end |
147 end |
148 | applicable_in (p, p_) pt (Tac.Refine_Problem pI) = |
148 | applicable_in (p, p_) pt (Tac.Refine_Problem pI) = |
149 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
149 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res |
150 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_))) |
150 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_))) |
152 let |
152 let |
153 val (dI, dI', itms) = case get_obj I pt p of |
153 val (dI, dI', itms) = case get_obj I pt p of |
154 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...} |
154 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...} |
155 => (dI, dI', itms) |
155 => (dI, dI', itms) |
156 | _ => error "applicable_in Refine_Problem: uncovered case get_obj" |
156 | _ => error "applicable_in Refine_Problem: uncovered case get_obj" |
157 val thy = if dI' = e_domID then dI else dI'; |
157 val thy = if dI' = Celem.e_domID then dI else dI'; |
158 in |
158 in |
159 case Specify.refine_pbl (assoc_thy thy) pI itms of |
159 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of |
160 NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable") |
160 NONE => Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable") |
161 | SOME (rf as (pI', _)) => |
161 | SOME (rf as (pI', _)) => |
162 if pI' = pI |
162 if pI' = pI |
163 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable") |
163 then Chead.Notappl ((Tac.tac2str (Tac.Refine_Problem pI)) ^ " not applicable") |
164 else Chead.Appl (Tac.Refine_Problem' rf) |
164 else Chead.Appl (Tac.Refine_Problem' rf) |
200 let |
200 let |
201 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of |
201 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of |
202 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...} |
202 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...} |
203 => (oris, dI, pI, dI', pI', itms) |
203 => (oris, dI, pI, dI', pI', itms) |
204 | _ => error "applicable_in Specify_Problem: uncovered case get_obj" |
204 | _ => error "applicable_in Specify_Problem: uncovered case get_obj" |
205 val thy = assoc_thy (if dI' = e_domID then dI else dI'); |
205 val thy = Celem.assoc_thy (if dI' = Celem.e_domID then dI else dI'); |
206 val {ppc, where_, prls, ...} = Specify.get_pbt pID; |
206 val {ppc, where_, prls, ...} = Specify.get_pbt pID; |
207 val pbl = if pI' = e_pblID andalso pI = e_pblID |
207 val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID |
208 then (false, (Generate.init_pbl ppc, [])) |
208 then (false, (Generate.init_pbl ppc, [])) |
209 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris; |
209 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris; |
210 in |
210 in |
211 Chead.Appl (Tac.Specify_Problem' (pID, pbl)) |
211 Chead.Appl (Tac.Specify_Problem' (pID, pbl)) |
212 end |
212 end |
223 PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) |
223 PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) |
224 | _ => error "applicable_in Apply_Method: uncovered case get_obj" |
224 | _ => error "applicable_in Apply_Method: uncovered case get_obj" |
225 val {where_, ...} = Specify.get_pbt pI |
225 val {where_, ...} = Specify.get_pbt pI |
226 val pres = map (Model.mk_env probl |> subst_atomic) where_ |
226 val pres = map (Model.mk_env probl |> subst_atomic) where_ |
227 val ctxt = if is_e_ctxt ctxt |
227 val ctxt = if is_e_ctxt ctxt |
228 then assoc_thy dI |> Proof_Context.init_global |> Stool.insert_assumptions pres |
228 then Celem.assoc_thy dI |> Proof_Context.init_global |> Stool.insert_assumptions pres |
229 else ctxt |
229 else ctxt |
230 (*TODO.WN110416 here do evalprecond according to fun check_preconds' |
230 (*TODO.WN110416 here do evalprecond according to fun check_preconds' |
231 and then decide on Chead.Notappl/Appl accordingly once more. |
231 and then decide on Chead.Notappl/Appl accordingly once more. |
232 Implement after all tests are running, since this changes |
232 Implement after all tests are running, since this changes |
233 overall system behavior*) |
233 overall system behavior*) |
235 Chead.Appl (Tac.Apply_Method' (mI, NONE, Selem.e_istate (*filled in solve*), ctxt)) |
235 Chead.Appl (Tac.Apply_Method' (mI, NONE, Selem.e_istate (*filled in solve*), ctxt)) |
236 end |
236 end |
237 | applicable_in (p, p_) _ (Tac.Check_Postcond pI) = |
237 | applicable_in (p, p_) _ (Tac.Check_Postcond pI) = |
238 if member op = [Pbl, Met] p_ |
238 if member op = [Pbl, Met] p_ |
239 then Chead.Notappl ((Tac.tac2str (Tac.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_)) |
239 then Chead.Notappl ((Tac.tac2str (Tac.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_)) |
240 else Chead.Appl (Tac.Check_Postcond' (pI, (e_term, [(*fun solve assigns returnvalue of scr*)]))) |
240 else Chead.Appl (Tac.Check_Postcond' (pI, (Celem.e_term, [(*fun solve assigns returnvalue of scr*)]))) |
241 | applicable_in _ _ (Tac.Take str) = Chead.Appl (Tac.Take' (TermC.str2term str)) (* always applicable ?*) |
241 | applicable_in _ _ (Tac.Take str) = Chead.Appl (Tac.Take' (TermC.str2term str)) (* always applicable ?*) |
242 | applicable_in _ _ (Tac.Free_Solve) = Chead.Appl (Tac.Free_Solve') (* always applicable *) |
242 | applicable_in _ _ (Tac.Free_Solve) = Chead.Appl (Tac.Free_Solve') (* always applicable *) |
243 | applicable_in (p, p_) pt (m as Tac.Rewrite_Inst (subs, thm'')) = |
243 | applicable_in (p, p_) pt (m as Tac.Rewrite_Inst (subs, thm'')) = |
244 if member op = [Pbl, Met] p_ |
244 if member op = [Pbl, Met] p_ |
245 then Chead.Notappl ((Tac.tac2str m)^" not for pos " ^ pos'2str (p, p_)) |
245 then Chead.Notappl ((Tac.tac2str m)^" not for pos " ^ pos'2str (p, p_)) |
246 else |
246 else |
247 let |
247 let |
248 val pp = par_pblobj pt p; |
248 val pp = par_pblobj pt p; |
249 val thy' = (get_obj g_domID pt pp): theory'; |
249 val thy' = get_obj g_domID pt pp; |
250 val thy = assoc_thy thy'; |
250 val thy = Celem.assoc_thy thy'; |
251 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp); |
251 val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp); |
252 val (f, _) = case p_ of (*p 12.4.00 unnecessary*) |
252 val (f, _) = case p_ of (*p 12.4.00 unnecessary*) |
253 Frm => (get_obj g_form pt p, p) |
253 Frm => (get_obj g_form pt p, p) |
254 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
254 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
255 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
255 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
256 in |
256 in |
257 let |
257 let |
258 val subst = Selem.subs2subst thy subs; |
258 val subst = Selem.subs2subst thy subs; |
259 in |
259 in |
260 case Rewrite.rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (snd thm'') f of |
260 case Rewrite.rewrite_inst_ thy (Celem.assoc_rew_ord ro') erls false subst (snd thm'') f of |
261 SOME (f',asm) => |
261 SOME (f',asm) => |
262 Chead.Appl (Tac.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) |
262 Chead.Appl (Tac.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm))) |
263 | NONE => Chead.Notappl ((fst thm'')^" not applicable") |
263 | NONE => Chead.Notappl ((fst thm'')^" not applicable") |
264 end |
264 end |
265 handle _ => Chead.Notappl ("syntax error in "^(subs2str subs)) |
265 handle _ => Chead.Notappl ("syntax error in "^(subs2str subs)) |
268 if member op = [Pbl, Met] p_ |
268 if member op = [Pbl, Met] p_ |
269 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p, p_))) |
269 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p, p_))) |
270 else |
270 else |
271 let |
271 let |
272 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt; |
272 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt; |
273 val thy = assoc_thy thy'; |
273 val thy = Celem.assoc_thy thy'; |
274 val f = case p_ of |
274 val f = case p_ of |
275 Frm => get_obj g_form pt p |
275 Frm => get_obj g_form pt p |
276 | Res => (fst o (get_obj g_result pt)) p |
276 | Res => (fst o (get_obj g_result pt)) p |
277 | _ => error ("applicable_in Rewrite: call by " ^ pos'2str (p, p_)); |
277 | _ => error ("applicable_in Rewrite: call by " ^ pos'2str (p, p_)); |
278 in |
278 in |
279 if msg = "OK" |
279 if msg = "OK" |
280 then |
280 then |
281 case Rewrite.rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of |
281 case Rewrite.rewrite_ thy (Celem.assoc_rew_ord ro) rls' false (snd thm'') f of |
282 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm))) |
282 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm))) |
283 | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable") |
283 | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable") |
284 else Chead.Notappl msg |
284 else Chead.Notappl msg |
285 end |
285 end |
286 | applicable_in (p, p_) pt (m as Tac.Rewrite_Asm thm'') = |
286 | applicable_in (p, p_) pt (m as Tac.Rewrite_Asm thm'') = |
287 if member op = [Pbl, Met] p_ |
287 if member op = [Pbl, Met] p_ |
288 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_))) |
288 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_))) |
289 else |
289 else |
290 let |
290 let |
291 val pp = par_pblobj pt p; |
291 val pp = par_pblobj pt p; |
292 val thy' = (get_obj g_domID pt pp):theory'; |
292 val thy' = get_obj g_domID pt pp; |
293 val thy = assoc_thy thy'; |
293 val thy = Celem.assoc_thy thy'; |
294 val {rew_ord'=ro',erls=erls,...} = Specify.get_met (get_obj g_metID pt pp); |
294 val {rew_ord'=ro',erls=erls,...} = Specify.get_met (get_obj g_metID pt pp); |
295 val (f, _) = case p_ of |
295 val (f, _) = case p_ of |
296 Frm => (get_obj g_form pt p, p) |
296 Frm => (get_obj g_form pt p, p) |
297 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
297 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
298 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
298 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
299 in |
299 in |
300 case Rewrite.rewrite_ thy (assoc_rew_ord ro') erls false (snd thm'') f of |
300 case Rewrite.rewrite_ thy (Celem.assoc_rew_ord ro') erls false (snd thm'') f of |
301 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm))) |
301 SOME (f',asm) => Chead.Appl (Tac.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm))) |
302 | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end |
302 | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end |
303 | applicable_in (p, p_) pt (m as Tac.Detail_Set_Inst (subs, rls)) = |
303 | applicable_in (p, p_) pt (m as Tac.Detail_Set_Inst (subs, rls)) = |
304 if member op = [Pbl, Met] p_ |
304 if member op = [Pbl, Met] p_ |
305 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p, p_))) |
305 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p, p_))) |
306 else |
306 else |
307 let |
307 let |
308 val pp = par_pblobj pt p; |
308 val pp = par_pblobj pt p; |
309 val thy' = get_obj g_domID pt pp; |
309 val thy' = get_obj g_domID pt pp; |
310 val thy = assoc_thy thy'; |
310 val thy = Celem.assoc_thy thy'; |
311 val f = case p_ of Frm => get_obj g_form pt p |
311 val f = case p_ of Frm => get_obj g_form pt p |
312 | Res => (fst o (get_obj g_result pt)) p |
312 | Res => (fst o (get_obj g_result pt)) p |
313 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
313 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
314 val subst = Selem.subs2subst thy subs |
314 val subst = Selem.subs2subst thy subs |
315 in |
315 in |
324 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_))) |
324 then Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_))) |
325 else |
325 else |
326 let |
326 let |
327 val pp = par_pblobj pt p; |
327 val pp = par_pblobj pt p; |
328 val thy' = get_obj g_domID pt pp; |
328 val thy' = get_obj g_domID pt pp; |
329 val thy = assoc_thy thy'; |
329 val thy = Celem.assoc_thy thy'; |
330 val (f, _) = case p_ of |
330 val (f, _) = case p_ of |
331 Frm => (get_obj g_form pt p, p) |
331 Frm => (get_obj g_form pt p, p) |
332 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
332 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
333 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
333 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
334 val subst = Selem.subs2subst thy subs; |
334 val subst = Selem.subs2subst thy subs; |
349 val (f, _) = case p_ of |
349 val (f, _) = case p_ of |
350 Frm => (get_obj g_form pt p, p) |
350 Frm => (get_obj g_form pt p, p) |
351 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
351 | Res => ((fst o (get_obj g_result pt)) p, lev_on p) |
352 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
352 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
353 in |
353 in |
354 case Rewrite.rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of |
354 case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of |
355 SOME (f', asm) |
355 SOME (f', asm) |
356 => Chead.Appl (Tac.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
356 => Chead.Appl (Tac.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
357 | NONE => Chead.Notappl (rls ^ " not applicable") |
357 | NONE => Chead.Notappl (rls ^ " not applicable") |
358 end |
358 end |
359 | applicable_in (p, p_) pt (m as Tac.Detail_Set rls) = |
359 | applicable_in (p, p_) pt (m as Tac.Detail_Set rls) = |
366 val f = case p_ of |
366 val f = case p_ of |
367 Frm => get_obj g_form pt p |
367 Frm => get_obj g_form pt p |
368 | Res => (fst o (get_obj g_result pt)) p |
368 | Res => (fst o (get_obj g_result pt)) p |
369 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
369 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
370 in |
370 in |
371 case Rewrite.rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of |
371 case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of |
372 SOME (f',asm) => Chead.Appl (Tac.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
372 SOME (f',asm) => Chead.Appl (Tac.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm))) |
373 | NONE => Chead.Notappl (rls^" not applicable") |
373 | NONE => Chead.Notappl (rls^" not applicable") |
374 end |
374 end |
375 | applicable_in _ _ Tac.End_Ruleset = error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Ruleset) |
375 | applicable_in _ _ Tac.End_Ruleset = error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Ruleset) |
376 | applicable_in (p, p_) pt (m as Tac.Calculate op_) = |
376 | applicable_in (p, p_) pt (m as Tac.Calculate op_) = |
384 | Res => (fst o (get_obj g_result pt)) p |
384 | Res => (fst o (get_obj g_result pt)) p |
385 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
385 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
386 in |
386 in |
387 if msg = "OK" |
387 if msg = "OK" |
388 then |
388 then |
389 case Rewrite.calculate_ (assoc_thy thy') isa_fn f of |
389 case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of |
390 SOME (f', (id, thm)) |
390 SOME (f', (id, thm)) |
391 => Chead.Appl (Tac.Calculate' (thy', op_, f, (f', (id, string_of_thmI thm)))) |
391 => Chead.Appl (Tac.Calculate' (thy', op_, f, (f', (id, Celem.string_of_thmI thm)))) |
392 | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable") |
392 | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable") |
393 else Chead.Notappl msg |
393 else Chead.Notappl msg |
394 end |
394 end |
395 (*Substitute combines two different kind of "substitution": |
395 (*Substitute combines two different kind of "substitution": |
396 (1) subst_atomic: for ?a..?z |
396 (1) subst_atomic: for ?a..?z |
399 if member op = [Pbl, Met] p_ |
399 if member op = [Pbl, Met] p_ |
400 then Chead.Notappl (Tac.tac2str m ^ " not for pos " ^ pos'2str (p, p_)) |
400 then Chead.Notappl (Tac.tac2str m ^ " not for pos " ^ pos'2str (p, p_)) |
401 else |
401 else |
402 let |
402 let |
403 val pp = par_pblobj pt p |
403 val pp = par_pblobj pt p |
404 val thy = assoc_thy (get_obj g_domID pt pp) |
404 val thy = Celem.assoc_thy (get_obj g_domID pt pp) |
405 val f = case p_ of |
405 val f = case p_ of |
406 Frm => get_obj g_form pt p |
406 Frm => get_obj g_form pt p |
407 | Res => (fst o (get_obj g_result pt)) p |
407 | Res => (fst o (get_obj g_result pt)) p |
408 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
408 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
409 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp) |
409 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp) |
410 val subte = Selem.sube2subte sube |
410 val subte = Selem.sube2subte sube |
411 val subst = Selem.sube2subst thy sube |
411 val subst = Selem.sube2subst thy sube |
412 val ro = assoc_rew_ord rew_ord' |
412 val ro = Celem.assoc_rew_ord rew_ord' |
413 in |
413 in |
414 if foldl and_ (true, map TermC.contains_Var subte) |
414 if foldl and_ (true, map TermC.contains_Var subte) |
415 then (*1*) |
415 then (*1*) |
416 let val f' = subst_atomic subst f |
416 let val f' = subst_atomic subst f |
417 in if f = f' |
417 in if f = f' |
431 | applicable_in (p, p_) pt (m as Tac.Subproblem (domID, pblID)) = |
431 | applicable_in (p, p_) pt (m as Tac.Subproblem (domID, pblID)) = |
432 if member op = [Pbl,Met] p_ |
432 if member op = [Pbl,Met] p_ |
433 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*) |
433 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*) |
434 case get_obj g_env pt p of |
434 case get_obj g_env pt p of |
435 SOME _ => |
435 SOME _ => |
436 Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [], |
436 Chead.Appl (Tac.Subproblem' ((domID, pblID, Celem.e_metID), [], |
437 e_term, [], Selem.e_ctxt(*FIXME.WN150511*), LTool.subpbl domID pblID)) |
437 Celem.e_term, [], Selem.e_ctxt(*FIXME.WN150511*), LTool.subpbl domID pblID)) |
438 | NONE => Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_))) |
438 | NONE => Chead.Notappl ((Tac.tac2str m)^" not for pos "^(pos'2str (p,p_))) |
439 else (*somewhere later in the script*) |
439 else (*somewhere later in the script*) |
440 Chead.Appl (Tac.Subproblem' ((domID, pblID, e_metID), [], |
440 Chead.Appl (Tac.Subproblem' ((domID, pblID, Celem.e_metID), [], |
441 e_term, [], Selem.e_ctxt, LTool.subpbl domID pblID)) |
441 Celem.e_term, [], Selem.e_ctxt, LTool.subpbl domID pblID)) |
442 | applicable_in _ _ (Tac.End_Subproblem) = |
442 | applicable_in _ _ (Tac.End_Subproblem) = |
443 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Subproblem) |
443 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.End_Subproblem) |
444 | applicable_in _ _ (Tac.CAScmd ct') = |
444 | applicable_in _ _ (Tac.CAScmd ct') = |
445 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.CAScmd ct')) |
445 error ("applicable_in: not impl. for " ^ Tac.tac2str (Tac.CAScmd ct')) |
446 | applicable_in _ _ (Tac.Split_And) = |
446 | applicable_in _ _ (Tac.Split_And) = |
456 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*) |
456 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*) |
457 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p) |
457 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p) |
458 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p) |
458 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p) |
459 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
459 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
460 in (Chead.Appl (Tac.Begin_Trans' f)) |
460 in (Chead.Appl (Tac.Begin_Trans' f)) |
461 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ term2str f ^ "'") |
461 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ Celem.term2str f ^ "'") |
462 end |
462 end |
463 | applicable_in (p, p_) pt (Tac.End_Trans) = (*TODO: check parent branches*) |
463 | applicable_in (p, p_) pt (Tac.End_Trans) = (*TODO: check parent branches*) |
464 if p_ = Res |
464 if p_ = Res |
465 then Chead.Appl (Tac.End_Trans' (get_obj g_result pt p)) |
465 then Chead.Appl (Tac.End_Trans' (get_obj g_result pt p)) |
466 else Chead.Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence" |
466 else Chead.Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence" |
476 if member op = [Pbl,Met] p_ |
476 if member op = [Pbl,Met] p_ |
477 then Chead.Notappl ((Tac.tac2str m)^" not for pos " ^ pos'2str (p, p_)) |
477 then Chead.Notappl ((Tac.tac2str m)^" not for pos " ^ pos'2str (p, p_)) |
478 else |
478 else |
479 let |
479 let |
480 val pp = par_pblobj pt p; |
480 val pp = par_pblobj pt p; |
481 val thy' = (get_obj g_domID pt pp):theory'; |
481 val thy' = get_obj g_domID pt pp; |
482 val thy = assoc_thy thy' |
482 val thy = Celem.assoc_thy thy' |
483 val metID = (get_obj g_metID pt pp) |
483 val metID = (get_obj g_metID pt pp) |
484 val {crls,...} = Specify.get_met metID |
484 val {crls,...} = Specify.get_met metID |
485 val (f, asm) = case p_ of |
485 val (f, asm) = case p_ of |
486 Frm => (get_obj g_form pt p , []) |
486 Frm => (get_obj g_form pt p , []) |
487 | Res => get_obj g_result pt p |
487 | Res => get_obj g_result pt p |
488 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
488 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
489 val vp = (thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f; |
489 val vp = (Celem.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f; |
490 in case f of |
490 in case f of |
491 Const ("List.list.Cons",_) $ _ $ _ => |
491 Const ("List.list.Cons",_) $ _ $ _ => |
492 Chead.Appl (Tac.Check_elementwise' (f, pred, check_elementwise thy crls f vp)) |
492 Chead.Appl (Tac.Check_elementwise' (f, pred, check_elementwise thy crls f vp)) |
493 | Const ("Tools.UniversalList",_) => |
493 | Const ("Tools.UniversalList",_) => |
494 Chead.Appl (Tac.Check_elementwise' (f, pred, (f,asm))) |
494 Chead.Appl (Tac.Check_elementwise' (f, pred, (f,asm))) |
495 | Const ("List.list.Nil",_) => |
495 | Const ("List.list.Nil",_) => |
496 Chead.Appl (Tac.Check_elementwise' (f, pred, (f, asm))) |
496 Chead.Appl (Tac.Check_elementwise' (f, pred, (f, asm))) |
497 | _ => Chead.Notappl ("Check_elementwise not appl.: " ^ term2str f ^ " should be constants") |
497 | _ => Chead.Notappl ("Check_elementwise not appl.: " ^ Celem.term2str f ^ " should be constants") |
498 end |
498 end |
499 | applicable_in (p, p_) pt Tac.Or_to_List = |
499 | applicable_in (p, p_) pt Tac.Or_to_List = |
500 if member op = [Pbl, Met] p_ |
500 if member op = [Pbl, Met] p_ |
501 then Chead.Notappl ((Tac.tac2str Tac.Or_to_List)^" not for pos "^(pos'2str (p,p_))) |
501 then Chead.Notappl ((Tac.tac2str Tac.Or_to_List)^" not for pos "^(pos'2str (p,p_))) |
502 else |
502 else |
505 Frm => get_obj g_form pt p |
505 Frm => get_obj g_form pt p |
506 | Res => (fst o (get_obj g_result pt)) p |
506 | Res => (fst o (get_obj g_result pt)) p |
507 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
507 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
508 in (let val ls = or2list f |
508 in (let val ls = or2list f |
509 in Chead.Appl (Tac.Or_to_List' (f, ls)) end) |
509 in Chead.Appl (Tac.Or_to_List' (f, ls)) end) |
510 handle _ => Chead.Notappl ("'Or_to_List' not applicable to "^(term2str f)) |
510 handle _ => Chead.Notappl ("'Or_to_List' not applicable to " ^ Celem.term2str f) |
511 end |
511 end |
512 | applicable_in _ _ Tac.Collect_Trues = |
512 | applicable_in _ _ Tac.Collect_Trues = |
513 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Collect_Trues) |
513 error ("applicable_in: not impl. for " ^ Tac.tac2str Tac.Collect_Trues) |
514 | applicable_in _ _ Tac.Empty_Tac = Chead.Notappl "Empty_Tac is not applicable" |
514 | applicable_in _ _ Tac.Empty_Tac = Chead.Notappl "Empty_Tac is not applicable" |
515 | applicable_in (p, p_) pt (Tac.Tac id) = |
515 | applicable_in (p, p_) pt (Tac.Tac id) = |
516 let |
516 let |
517 val pp = par_pblobj pt p; |
517 val pp = par_pblobj pt p; |
518 val thy' = (get_obj g_domID pt pp):theory'; |
518 val thy' = get_obj g_domID pt pp; |
519 val thy = assoc_thy thy'; |
519 val thy = Celem.assoc_thy thy'; |
520 val f = case p_ of |
520 val f = case p_ of |
521 Frm => get_obj g_form pt p |
521 Frm => get_obj g_form pt p |
522 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl" |
522 | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl" |
523 | Res => (fst o (get_obj g_result pt)) p |
523 | Res => (fst o (get_obj g_result pt)) p |
524 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
524 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_)); |
525 in case id of |
525 in case id of |
526 "subproblem_equation_dummy" => |
526 "subproblem_equation_dummy" => |
527 if TermC.is_expliceq f |
527 if TermC.is_expliceq f |
528 then Chead.Appl (Tac.Tac_ (thy, term2str f, id, "subproblem_equation_dummy (" ^ term2str f ^ ")")) |
528 then Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, "subproblem_equation_dummy (" ^ Celem.term2str f ^ ")")) |
529 else Chead.Notappl "applicable only to equations made explicit" |
529 else Chead.Notappl "applicable only to equations made explicit" |
530 | "solve_equation_dummy" => |
530 | "solve_equation_dummy" => |
531 let val (id', f') = split_dummy (term2str f); |
531 let val (id', f') = split_dummy (Celem.term2str f); |
532 in |
532 in |
533 if id' <> "subproblem_equation_dummy" |
533 if id' <> "subproblem_equation_dummy" |
534 then Chead.Notappl "no subproblem" |
534 then Chead.Notappl "no subproblem" |
535 else if (thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq |
535 else if (Celem.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq |
536 then Chead.Appl (Tac.Tac_ (thy, term2str f, id, "[" ^ f' ^ "]")) |
536 then Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, "[" ^ f' ^ "]")) |
537 else error ("applicable_in: f= " ^ f') |
537 else error ("applicable_in: f= " ^ f') |
538 end |
538 end |
539 | _ => Chead.Appl (Tac.Tac_ (thy, term2str f, id, term2str f)) |
539 | _ => Chead.Appl (Tac.Tac_ (thy, Celem.term2str f, id, Celem.term2str f)) |
540 end |
540 end |
541 | applicable_in _ _ Tac.End_Proof' = Chead.Appl Tac.End_Proof'' |
541 | applicable_in _ _ Tac.End_Proof' = Chead.Appl Tac.End_Proof'' |
542 | applicable_in _ _ m = error ("applicable_in called for " ^ Tac.tac2str m); |
542 | applicable_in _ _ m = error ("applicable_in called for " ^ Tac.tac2str m); |
543 |
543 |
544 fun tac2tac_ pt p m = |
544 fun tac2tac_ pt p m = |