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