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 |
*)
|
neuper@37906
|
7 |
val e_cterm' = empty_cterm';
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
|
neuper@37906
|
11 |
(rew_ord':rew_ord',erls,ca)
|
neuper@37906
|
12 |
| rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
|
neuper@37906
|
13 |
(rew_ord',erls,ca)
|
neuper@37906
|
14 |
| rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
|
neuper@37906
|
15 |
(rew_ord',erls, ca)
|
neuper@38031
|
16 |
| rew_info rls = error ("rew_info called with '"^rls2str rls^"'");
|
neuper@37906
|
17 |
|
neuper@37906
|
18 |
(*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
|
neuper@37906
|
19 |
fun from_pblobj_or_detail_thm thm' p pt =
|
neuper@37906
|
20 |
let val (pbl,p',rls') = par_pbl_det pt p
|
neuper@37906
|
21 |
in if pbl
|
neuper@38015
|
22 |
then let (*val _= tracing("### from_pblobj_or_detail_thm: pbl=true")*)
|
neuper@37906
|
23 |
val thy' = get_obj g_domID pt p'
|
neuper@37906
|
24 |
val {rew_ord',erls,(*asm_thm,*)...} =
|
neuper@37906
|
25 |
get_met (get_obj g_metID pt p')
|
neuper@38015
|
26 |
(*val _= tracing("### from_pblobj_or_detail_thm: metID= "^
|
neuper@37906
|
27 |
(metID2str(get_obj g_metID pt p')))
|
neuper@38015
|
28 |
val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)
|
neuper@37906
|
29 |
in ("OK",thy',rew_ord',erls,(*put_asm*)false)
|
neuper@37906
|
30 |
end
|
neuper@38015
|
31 |
else ((*tracing("### from_pblobj_or_detail_thm: pbl=false");*)
|
neuper@37906
|
32 |
(*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!!
|
neuper@37926
|
33 |
NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
|
neuper@37926
|
34 |
| SOME rls =>*)
|
neuper@37906
|
35 |
let val thy' = get_obj g_domID pt (par_pblobj pt p)
|
neuper@37906
|
36 |
val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'
|
neuper@37930
|
37 |
in ("OK",thy',rew_ord',erls,false) end)
|
neuper@37906
|
38 |
end;
|
neuper@37906
|
39 |
(*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
|
neuper@37906
|
40 |
fun from_pblobj_or_detail_calc scrop p pt =
|
neuper@37906
|
41 |
(* val (scrop, p, pt) = (op_, p, pt);
|
neuper@37906
|
42 |
*)
|
neuper@37906
|
43 |
let val (pbl,p',rls') = par_pbl_det pt p
|
neuper@37906
|
44 |
in if pbl
|
neuper@37906
|
45 |
then let val thy' = get_obj g_domID pt p'
|
neuper@37906
|
46 |
val {calc = scr_isa_fns,...} =
|
neuper@37906
|
47 |
get_met (get_obj g_metID pt p')
|
neuper@37906
|
48 |
val opt = assoc (scr_isa_fns, scrop)
|
neuper@37906
|
49 |
in case opt of
|
neuper@37926
|
50 |
SOME isa_fn => ("OK",thy',isa_fn)
|
neuper@37926
|
51 |
| NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
|
neuper@37906
|
52 |
"",("",e_evalfn)) end
|
neuper@37906
|
53 |
else (*case assoc(!ruleset', rls') of
|
neuper@37926
|
54 |
NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
|
neuper@37926
|
55 |
| SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
|
neuper@37926
|
56 |
(* val SOME rls = assoc(!ruleset', rls');
|
neuper@37906
|
57 |
*)
|
neuper@37906
|
58 |
let val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@37906
|
59 |
val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
|
neuper@37906
|
60 |
in case assoc (scr_isa_fns, scrop) of
|
neuper@37926
|
61 |
SOME isa_fn => ("OK",thy',isa_fn)
|
neuper@37926
|
62 |
| NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
|
neuper@37906
|
63 |
"",("",e_evalfn)) end
|
neuper@37906
|
64 |
end;
|
neuper@37906
|
65 |
(*------------------------------------------------------------------*)
|
neuper@37906
|
66 |
|
neuper@37906
|
67 |
val op_and = Const ("op &", [bool, bool] ---> bool);
|
neuper@37938
|
68 |
(*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
|
neuper@37906
|
69 |
val it = "a & b" : cterm
|
neuper@37906
|
70 |
*)
|
neuper@37906
|
71 |
fun mk_and a b = op_and $ a $ b;
|
neuper@37938
|
72 |
(*> (cterm_of thy)
|
neuper@37906
|
73 |
(mk_and (Free("a",bool)) (Free("b",bool)));
|
neuper@37906
|
74 |
val it = "a & b" : cterm*)
|
neuper@37906
|
75 |
|
neuper@37906
|
76 |
fun mk_and [] = HOLogic.true_const
|
neuper@37906
|
77 |
| mk_and (t::[]) = t
|
neuper@37906
|
78 |
| mk_and (t::ts) =
|
neuper@37906
|
79 |
let fun mk t' (t::[]) = op_and $ t' $ t
|
neuper@37906
|
80 |
| mk t' (t::ts) = mk (op_and $ t' $ t) ts
|
neuper@37906
|
81 |
in mk t ts end;
|
neuper@37906
|
82 |
(*> val pred = map (term_of o the o (parse thy))
|
neuper@37906
|
83 |
["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
|
neuper@37938
|
84 |
> (cterm_of thy) (mk_and pred);
|
neuper@37906
|
85 |
val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
|
neuper@37906
|
86 |
|
neuper@37906
|
87 |
|
neuper@37906
|
88 |
|
neuper@37906
|
89 |
|
neuper@37906
|
90 |
(*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
|
neuper@37906
|
91 |
fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, [])
|
neuper@37906
|
92 |
|
neuper@37906
|
93 |
| mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
|
neuper@37906
|
94 |
(e_term, if pred <> Const ("Script.Assumptions",bool)
|
neuper@37906
|
95 |
then [pred]
|
neuper@37906
|
96 |
else (map fst) (get_assumptions_ pt (p,Res)))
|
neuper@37906
|
97 |
|
neuper@37906
|
98 |
(* val pred = (term_of o the o (parse thy)) pred;
|
neuper@37906
|
99 |
val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
|
neuper@37906
|
100 |
mk_set thy pt p consts pred;
|
neuper@37906
|
101 |
*)
|
neuper@37906
|
102 |
| mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred =
|
neuper@37906
|
103 |
let val (bdv,_) = HOLogic.dest_eq eq;
|
neuper@37906
|
104 |
val pred = if pred <> Const ("Script.Assumptions",bool)
|
neuper@37906
|
105 |
then [pred]
|
neuper@37906
|
106 |
else (map fst) (get_assumptions_ pt (p,Res))
|
neuper@37906
|
107 |
in (bdv, pred) end
|
neuper@37906
|
108 |
|
neuper@37906
|
109 |
| mk_set thy _ _ l _ =
|
neuper@38053
|
110 |
error ("check_elementwise: no set " ^ term2str l);
|
neuper@37906
|
111 |
(*> val consts = str2term "[x=#4]";
|
neuper@37906
|
112 |
> val pred = str2term "Assumptions";
|
neuper@37906
|
113 |
> val pt = union_asm pt p
|
neuper@37906
|
114 |
[("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
|
neuper@37906
|
115 |
("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
|
neuper@37906
|
116 |
> val p = [];
|
neuper@37906
|
117 |
> val (sss,ttt) = mk_set thy pt p consts pred;
|
neuper@38053
|
118 |
> (term2str sss, term2str ttt);
|
neuper@37906
|
119 |
val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
|
neuper@37906
|
120 |
|
neuper@37906
|
121 |
val consts = str2term "UniversalList";
|
neuper@37906
|
122 |
val pred = str2term "Assumptions";
|
neuper@37906
|
123 |
|
neuper@37906
|
124 |
*)
|
neuper@37906
|
125 |
|
neuper@37906
|
126 |
|
neuper@37906
|
127 |
|
neuper@37906
|
128 |
(*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
|
neuper@37906
|
129 |
(* val (erls,consts,(bdv,pred)) = (erl,ft,vp);
|
neuper@37906
|
130 |
val (consts,(bdv,pred)) = (ft,vp);
|
neuper@37906
|
131 |
*)
|
neuper@37906
|
132 |
fun check_elementwise thy erls all_results (bdv, asm) =
|
neuper@37906
|
133 |
let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
|
neuper@37906
|
134 |
fun check sub =
|
neuper@37906
|
135 |
let val inst_ = map (subst_atomic [sub]) asm
|
neuper@37906
|
136 |
in case eval__true thy 1 inst_ [] erls of
|
neuper@37906
|
137 |
(asm', true) => ([HOLogic.mk_eq sub], asm')
|
neuper@37906
|
138 |
| (_, false) => ([],[])
|
neuper@37906
|
139 |
end;
|
neuper@38015
|
140 |
(*val _= tracing("### check_elementwise: res= "^(term2str all_results)^
|
neuper@37906
|
141 |
", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
|
neuper@37906
|
142 |
val c' = isalist2list all_results
|
neuper@37906
|
143 |
val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
|
neuper@37906
|
144 |
val subs = map (pair bdv) c''
|
neuper@37906
|
145 |
in if asm = [] then (all_results, [])
|
neuper@37906
|
146 |
else ((apfst ((list2isalist bool) o flat)) o
|
neuper@37906
|
147 |
(apsnd flat) o split_list o (map check)) subs end;
|
neuper@37906
|
148 |
(* 20.5.03
|
neuper@37906
|
149 |
> val all_results = str2term "[x=a+b,x=b,x=3]";
|
neuper@37906
|
150 |
> val bdv = str2term "x";
|
neuper@37906
|
151 |
> val asm = str2term "(x ~= a) & (x ~= b)";
|
neuper@37906
|
152 |
> val erls = e_rls;
|
neuper@37906
|
153 |
> val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
|
neuper@38015
|
154 |
> term2str t; tracing(terms2str ts);
|
neuper@37906
|
155 |
val it = "[x = a + b, x = b, x = c]" : string
|
neuper@37906
|
156 |
["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
|
neuper@37906
|
157 |
... with appropriate erls this should be:
|
neuper@37906
|
158 |
val it = "[x = a + b, x = c]" : string
|
neuper@37906
|
159 |
["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
|
neuper@37906
|
160 |
////// because b ~= b False*)
|
neuper@37906
|
161 |
|
neuper@37906
|
162 |
|
neuper@37906
|
163 |
|
neuper@37906
|
164 |
(*before 5.03-----
|
neuper@37906
|
165 |
> val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
|
neuper@37906
|
166 |
\ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
|
neuper@38050
|
167 |
> val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
|
neuper@37906
|
168 |
val ct' = "True" : cterm'
|
neuper@37906
|
169 |
|
neuper@37906
|
170 |
> val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
|
neuper@37906
|
171 |
\ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
|
neuper@38050
|
172 |
> val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
|
neuper@37906
|
173 |
val ct' = "True" : cterm'
|
neuper@37906
|
174 |
|
neuper@37906
|
175 |
|
neuper@37906
|
176 |
> val const = (term_of o the o (parse thy)) "(#3::real)";
|
neuper@37906
|
177 |
> val pred' = subst_atomic [(bdv,const)] pred;
|
neuper@37906
|
178 |
|
neuper@37906
|
179 |
|
neuper@37906
|
180 |
> val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
|
neuper@37906
|
181 |
> val bdv = (term_of o the o (parse thy)) "(x::real)";
|
neuper@37906
|
182 |
> val pred = (term_of o the o (parse thy))
|
neuper@37906
|
183 |
"((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
|
neuper@37906
|
184 |
> val ttt = check_elementwise thy consts (bdv, pred);
|
neuper@37938
|
185 |
> (cterm_of thy) ttt;
|
neuper@37906
|
186 |
val it = "[x = #-3, x = #3]" : cterm
|
neuper@37906
|
187 |
|
neuper@37906
|
188 |
> val consts = (term_of o the o (parse thy)) "[x = #4]";
|
neuper@37906
|
189 |
> val bdv = (term_of o the o (parse thy)) "(x::real)";
|
neuper@37906
|
190 |
> val pred = (term_of o the o (parse thy))
|
neuper@37906
|
191 |
"#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
|
neuper@37906
|
192 |
> val ttt = check_elementwise thy consts (bdv,pred);
|
neuper@37938
|
193 |
> (cterm_of thy) ttt;
|
neuper@37906
|
194 |
val it = "[x = #4]" : cterm
|
neuper@37906
|
195 |
|
neuper@37906
|
196 |
> val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
|
neuper@37906
|
197 |
> val bdv = (term_of o the o (parse thy)) "(x::real)";
|
neuper@37906
|
198 |
> val pred = (term_of o the o (parse thy))
|
neuper@37906
|
199 |
" #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
|
neuper@37906
|
200 |
> val ttt = check_elementwise thy consts (bdv,pred);
|
neuper@37938
|
201 |
> (cterm_of thy) ttt;
|
neuper@37906
|
202 |
val it = "[]" : cterm*)
|
neuper@37906
|
203 |
|
neuper@37906
|
204 |
|
neuper@37906
|
205 |
(* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)
|
neuper@37906
|
206 |
fun split_dummy str =
|
neuper@37906
|
207 |
let fun scan s' [] = (implode s', "")
|
neuper@37906
|
208 |
| scan s' (s::ss) = if s=" " then (implode s', implode ss)
|
neuper@37906
|
209 |
else scan (s'@[s]) ss;
|
neuper@37906
|
210 |
in ((scan []) o explode) str end;
|
neuper@37906
|
211 |
(* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
|
neuper@37906
|
212 |
val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
|
neuper@37906
|
213 |
> split_dummy "x=-#5//#12";
|
neuper@37906
|
214 |
val it = ("x=-#5//#12","") : string * string*)
|
neuper@37906
|
215 |
|
neuper@37906
|
216 |
|
neuper@37906
|
217 |
|
neuper@37906
|
218 |
|
neuper@37906
|
219 |
(*.applicability of a tacic wrt. a calc-state (ptree,pos').
|
neuper@37906
|
220 |
additionally used by next_tac in the script-interpreter for sequence-tacs.
|
neuper@37906
|
221 |
tests for applicability are so expensive, that results (rewrites!)
|
neuper@37906
|
222 |
are kept in the return-value of 'type tac_'.
|
neuper@37906
|
223 |
.*)
|
neuper@37906
|
224 |
fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
|
neuper@37906
|
225 |
Appl (Init_Proof' (ct', spec))
|
neuper@37906
|
226 |
|
neuper@37906
|
227 |
| applicable_in (p,p_) pt Model_Problem =
|
neuper@37906
|
228 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
229 |
then Notappl ((tac2str Model_Problem)^
|
neuper@37906
|
230 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
231 |
else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
|
neuper@37906
|
232 |
val {ppc,...} = get_pbt pI'
|
neuper@37906
|
233 |
val pbl = init_pbl ppc
|
neuper@37906
|
234 |
in Appl (Model_Problem' (pI', pbl, [])) end
|
neuper@37906
|
235 |
(* val Refine_Tacitly pI = m;
|
neuper@37906
|
236 |
*)
|
neuper@37906
|
237 |
| applicable_in (p,p_) pt (Refine_Tacitly pI) =
|
neuper@37906
|
238 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
239 |
then Notappl ((tac2str (Refine_Tacitly pI))^
|
neuper@37906
|
240 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
241 |
else (* val Refine_Tacitly pI = m;
|
neuper@37906
|
242 |
*)
|
neuper@37906
|
243 |
let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
|
neuper@37906
|
244 |
val opt = refine_ori oris pI;
|
neuper@37906
|
245 |
in case opt of
|
neuper@37926
|
246 |
SOME pblID =>
|
neuper@37906
|
247 |
Appl (Refine_Tacitly' (pI, pblID,
|
neuper@37906
|
248 |
e_domID, e_metID, [](*filled in specify*)))
|
neuper@37926
|
249 |
| NONE => Notappl ((tac2str (Refine_Tacitly pI))^
|
neuper@37906
|
250 |
" not applicable") end
|
neuper@37906
|
251 |
(* val (p,p_) = ip;
|
neuper@37906
|
252 |
val Refine_Problem pI = m;
|
neuper@37906
|
253 |
*)
|
neuper@37906
|
254 |
| applicable_in (p,p_) pt (Refine_Problem pI) =
|
neuper@37906
|
255 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
256 |
then Notappl ((tac2str (Refine_Problem pI))^
|
neuper@37906
|
257 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
258 |
else
|
neuper@37906
|
259 |
let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
|
neuper@37906
|
260 |
probl=itms, ...}) = get_obj I pt p;
|
neuper@37906
|
261 |
val thy = if dI' = e_domID then dI else dI';
|
neuper@37906
|
262 |
val rfopt = refine_pbl (assoc_thy thy) pI itms;
|
neuper@37906
|
263 |
in case rfopt of
|
neuper@37926
|
264 |
NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
|
neuper@37926
|
265 |
| SOME (rf as (pI',_)) =>
|
neuper@37926
|
266 |
(* val SOME (rf as (pI',_)) = rfopt;
|
neuper@37906
|
267 |
*)
|
neuper@37906
|
268 |
if pI' = pI
|
neuper@37906
|
269 |
then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
|
neuper@37906
|
270 |
else Appl (Refine_Problem' rf)
|
neuper@37906
|
271 |
end
|
neuper@37906
|
272 |
|
neuper@37906
|
273 |
(*the specify-tacs have cterm' instead term:
|
neuper@37906
|
274 |
parse+error here!!!: see appl_add*)
|
neuper@37906
|
275 |
| applicable_in (p,p_) pt (Add_Given ct') =
|
neuper@37906
|
276 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
277 |
then Notappl ((tac2str (Add_Given ct'))^
|
neuper@37906
|
278 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
279 |
else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
|
neuper@37906
|
280 |
(*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
|
neuper@37906
|
281 |
|
neuper@37906
|
282 |
| applicable_in (p,p_) pt (Del_Given ct') =
|
neuper@37906
|
283 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
284 |
then Notappl ((tac2str (Del_Given ct'))^
|
neuper@37906
|
285 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
286 |
else Appl (Del_Given' ct')
|
neuper@37906
|
287 |
|
neuper@37906
|
288 |
| applicable_in (p,p_) pt (Add_Find ct') =
|
neuper@37906
|
289 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
290 |
then Notappl ((tac2str (Add_Find ct'))^
|
neuper@37906
|
291 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
292 |
else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
|
neuper@37906
|
293 |
|
neuper@37906
|
294 |
| applicable_in (p,p_) pt (Del_Find ct') =
|
neuper@37906
|
295 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
296 |
then Notappl ((tac2str (Del_Find ct'))^
|
neuper@37906
|
297 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
298 |
else Appl (Del_Find' ct')
|
neuper@37906
|
299 |
|
neuper@37906
|
300 |
| applicable_in (p,p_) pt (Add_Relation ct') =
|
neuper@37906
|
301 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
302 |
then Notappl ((tac2str (Add_Relation ct'))^
|
neuper@37906
|
303 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
304 |
else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
|
neuper@37906
|
305 |
|
neuper@37906
|
306 |
| applicable_in (p,p_) pt (Del_Relation ct') =
|
neuper@37906
|
307 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
308 |
then Notappl ((tac2str (Del_Relation ct'))^
|
neuper@37906
|
309 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
310 |
else Appl (Del_Relation' ct')
|
neuper@37906
|
311 |
|
neuper@37906
|
312 |
| applicable_in (p,p_) pt (Specify_Theory dI) =
|
neuper@37906
|
313 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
314 |
then Notappl ((tac2str (Specify_Theory dI))^
|
neuper@37906
|
315 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
316 |
else Appl (Specify_Theory' dI)
|
neuper@37906
|
317 |
(* val (p,p_) = p; val Specify_Problem pID = m;
|
neuper@37906
|
318 |
val Specify_Problem pID = m;
|
neuper@37906
|
319 |
*)
|
neuper@37906
|
320 |
| applicable_in (p,p_) pt (Specify_Problem pID) =
|
neuper@37906
|
321 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
322 |
then Notappl ((tac2str (Specify_Problem pID))^
|
neuper@37906
|
323 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
324 |
else
|
neuper@37906
|
325 |
let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
|
neuper@37906
|
326 |
probl=itms, ...}) = get_obj I pt p;
|
neuper@37906
|
327 |
val thy = assoc_thy (if dI' = e_domID then dI else dI');
|
neuper@37906
|
328 |
val {ppc,where_,prls,...} = get_pbt pID;
|
neuper@37906
|
329 |
val pbl = if pI'=e_pblID andalso pI=e_pblID
|
neuper@37906
|
330 |
then (false, (init_pbl ppc, []))
|
neuper@37906
|
331 |
else match_itms_oris thy itms (ppc,where_,prls) oris;
|
neuper@37906
|
332 |
in Appl (Specify_Problem' (pID, pbl)) end
|
neuper@37906
|
333 |
(* val Specify_Method mID = nxt; val (p,p_) = p;
|
neuper@37906
|
334 |
*)
|
neuper@37906
|
335 |
| applicable_in (p,p_) pt (Specify_Method mID) =
|
neuper@37906
|
336 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
337 |
then Notappl ((tac2str (Specify_Method mID))^
|
neuper@37906
|
338 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
339 |
else Appl (Specify_Method' (mID,[(*filled in specify*)],
|
neuper@37906
|
340 |
[(*filled in specify*)]))
|
neuper@37906
|
341 |
|
neuper@37906
|
342 |
| applicable_in (p,p_) pt (Apply_Method mI) =
|
neuper@37906
|
343 |
if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
|
neuper@37906
|
344 |
then Notappl ((tac2str (Apply_Method mI))^
|
neuper@37906
|
345 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37926
|
346 |
else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
|
neuper@37906
|
347 |
|
neuper@37906
|
348 |
| applicable_in (p,p_) pt (Check_Postcond pI) =
|
neuper@37935
|
349 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
350 |
then Notappl ((tac2str (Check_Postcond pI))^
|
neuper@37906
|
351 |
" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
352 |
else Appl (Check_Postcond'
|
neuper@37906
|
353 |
(pI,(e_term,[(*asm in solve*)])))
|
neuper@37906
|
354 |
(* in solve -"- ^^^^^^ gets returnvalue of scr*)
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
(*these are always applicable*)
|
neuper@37906
|
357 |
| applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
|
neuper@37906
|
358 |
| applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
|
neuper@37906
|
359 |
|
neuper@37906
|
360 |
(* val m as Rewrite_Inst (subs, thm') = m;
|
neuper@37906
|
361 |
*)
|
neuper@37906
|
362 |
| applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
|
neuper@37935
|
363 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
364 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
365 |
else
|
neuper@37906
|
366 |
let
|
neuper@37906
|
367 |
val pp = par_pblobj pt p;
|
neuper@37906
|
368 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
369 |
val thy = assoc_thy thy';
|
neuper@37930
|
370 |
val {rew_ord'=ro',erls=erls,...} =
|
neuper@37906
|
371 |
get_met (get_obj g_metID pt pp);
|
neuper@37906
|
372 |
val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
|
neuper@37906
|
373 |
Frm => (get_obj g_form pt p, p)
|
neuper@37906
|
374 |
| Res => ((fst o (get_obj g_result pt)) p, lev_on p)
|
neuper@38031
|
375 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
376 |
(pos'2str (p,p_)));
|
neuper@37906
|
377 |
in
|
neuper@37906
|
378 |
let val subst = subs2subst thy subs;
|
neuper@37906
|
379 |
val subs' = subst2subs' subst;
|
neuper@37906
|
380 |
in case rewrite_inst_ thy (assoc_rew_ord ro') erls
|
neuper@37906
|
381 |
(*put_asm*)false subst (assoc_thm' thy thm') f of
|
neuper@37926
|
382 |
SOME (f',asm) => Appl (
|
neuper@37906
|
383 |
Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',
|
neuper@37906
|
384 |
(*term_of o the o (parse (assoc_thy thy'))*) f,
|
neuper@37906
|
385 |
(*(term_of o the o (parse (assoc_thy thy'))*) (f',
|
neuper@37906
|
386 |
(*map (term_of o the o (parse (assoc_thy thy')))*) asm)))
|
neuper@37926
|
387 |
| NONE => Notappl ((fst thm')^" not applicable") end
|
neuper@37906
|
388 |
handle _ => Notappl ("syntax error in "^(subs2str subs)) end
|
neuper@37906
|
389 |
|
neuper@37906
|
390 |
(* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);
|
neuper@37906
|
391 |
val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
|
neuper@37906
|
392 |
*)
|
neuper@37906
|
393 |
| applicable_in (p,p_) pt (m as Rewrite thm') =
|
neuper@37935
|
394 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
395 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
396 |
else
|
neuper@37906
|
397 |
let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
|
neuper@37906
|
398 |
val thy = assoc_thy thy';
|
neuper@37906
|
399 |
val f = case p_ of
|
neuper@37906
|
400 |
Frm => get_obj g_form pt p
|
neuper@37906
|
401 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@38031
|
402 |
| _ => error ("applicable_in Rewrite: call by "^
|
neuper@37906
|
403 |
(pos'2str (p,p_)));
|
neuper@37906
|
404 |
in if msg = "OK"
|
neuper@37906
|
405 |
then
|
neuper@38015
|
406 |
((*tracing("### applicable_in rls'= "^rls');*)
|
neuper@37926
|
407 |
(* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
|
neuper@37906
|
408 |
*)
|
neuper@37906
|
409 |
case rewrite_ thy (assoc_rew_ord ro)
|
neuper@37906
|
410 |
rls' false (assoc_thm' thy thm') f of
|
neuper@37926
|
411 |
SOME (f',asm) => Appl (
|
neuper@37906
|
412 |
Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
|
neuper@37926
|
413 |
| NONE => Notappl ("'"^(fst thm')^"' not applicable") )
|
neuper@37906
|
414 |
else Notappl msg
|
neuper@37906
|
415 |
end
|
neuper@37906
|
416 |
|
neuper@37906
|
417 |
| applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
|
neuper@37935
|
418 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
419 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
420 |
else
|
neuper@37906
|
421 |
let
|
neuper@37906
|
422 |
val pp = par_pblobj pt p;
|
neuper@37906
|
423 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
424 |
val thy = assoc_thy thy';
|
neuper@37906
|
425 |
val {rew_ord'=ro',erls=erls,...} =
|
neuper@37906
|
426 |
get_met (get_obj g_metID pt pp);
|
neuper@37906
|
427 |
(*val put_asm = true;*)
|
neuper@37906
|
428 |
val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
|
neuper@37906
|
429 |
Frm => (get_obj g_form pt p, p)
|
neuper@37906
|
430 |
| Res => ((fst o (get_obj g_result pt)) p, lev_on p)
|
neuper@38031
|
431 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
432 |
(pos'2str (p,p_)));
|
neuper@37906
|
433 |
in case rewrite_ thy (assoc_rew_ord ro') erls
|
neuper@37906
|
434 |
(*put_asm*)false (assoc_thm' thy thm') f of
|
neuper@37926
|
435 |
SOME (f',asm) => Appl (
|
neuper@37906
|
436 |
Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
|
neuper@37926
|
437 |
| NONE => Notappl ("'"^(fst thm')^"' not applicable") end
|
neuper@37906
|
438 |
|
neuper@37906
|
439 |
| applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
|
neuper@37935
|
440 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
441 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
442 |
else
|
neuper@37906
|
443 |
let
|
neuper@37906
|
444 |
val pp = par_pblobj pt p;
|
neuper@37906
|
445 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
446 |
val thy = assoc_thy thy';
|
neuper@37906
|
447 |
val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
|
neuper@37906
|
448 |
val f = case p_ of Frm => get_obj g_form pt p
|
neuper@37906
|
449 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@38031
|
450 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
451 |
(pos'2str (p,p_)));
|
neuper@37906
|
452 |
in
|
neuper@37906
|
453 |
let val subst = subs2subst thy subs
|
neuper@37906
|
454 |
val subs' = subst2subs' subst
|
neuper@37906
|
455 |
in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
|
neuper@37926
|
456 |
SOME (f',asm) => Appl (
|
neuper@37906
|
457 |
Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
|
neuper@37926
|
458 |
| NONE => Notappl (rls^" not applicable") end
|
neuper@37906
|
459 |
handle _ => Notappl ("syntax error in "^(subs2str subs)) end
|
neuper@37906
|
460 |
|
neuper@37906
|
461 |
| applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
|
neuper@37935
|
462 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
463 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
464 |
else
|
neuper@37906
|
465 |
let
|
neuper@37906
|
466 |
val pp = par_pblobj pt p;
|
neuper@37906
|
467 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
468 |
val thy = assoc_thy thy';
|
neuper@37906
|
469 |
val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
|
neuper@37906
|
470 |
get_met (get_obj g_metID pt pp);
|
neuper@37906
|
471 |
val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
|
neuper@37906
|
472 |
Frm => (get_obj g_form pt p, p)
|
neuper@37906
|
473 |
| Res => ((fst o (get_obj g_result pt)) p, lev_on p)
|
neuper@38031
|
474 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
475 |
(pos'2str (p,p_)));
|
neuper@37906
|
476 |
in
|
neuper@37906
|
477 |
let val subst = subs2subst thy subs;
|
neuper@37906
|
478 |
val subs' = subst2subs' subst;
|
neuper@37906
|
479 |
in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
|
neuper@37926
|
480 |
SOME (f',asm) => Appl (
|
neuper@37906
|
481 |
Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
|
neuper@37926
|
482 |
| NONE => Notappl (rls^" not applicable") end
|
neuper@37906
|
483 |
handle _ => Notappl ("syntax error in "^(subs2str subs)) end
|
neuper@37906
|
484 |
|
neuper@37906
|
485 |
| applicable_in (p,p_) pt (m as Rewrite_Set rls) =
|
neuper@37935
|
486 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
487 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
488 |
else
|
neuper@37906
|
489 |
let
|
neuper@37906
|
490 |
val pp = par_pblobj pt p;
|
neuper@37906
|
491 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
492 |
val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
|
neuper@37906
|
493 |
Frm => (get_obj g_form pt p, p)
|
neuper@37906
|
494 |
| Res => ((fst o (get_obj g_result pt)) p, lev_on p)
|
neuper@38031
|
495 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
496 |
(pos'2str (p,p_)));
|
neuper@37930
|
497 |
in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
|
neuper@37926
|
498 |
SOME (f',asm) =>
|
neuper@38015
|
499 |
((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)
|
neuper@37906
|
500 |
Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
|
neuper@37906
|
501 |
)
|
neuper@37926
|
502 |
| NONE => Notappl (rls^" not applicable") end
|
neuper@37906
|
503 |
|
neuper@37906
|
504 |
| applicable_in (p,p_) pt (m as Detail_Set rls) =
|
neuper@37935
|
505 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
506 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
507 |
else
|
neuper@37906
|
508 |
let val pp = par_pblobj pt p
|
neuper@37906
|
509 |
val thy' = (get_obj g_domID pt pp):theory'
|
neuper@37906
|
510 |
val f = case p_ of
|
neuper@37906
|
511 |
Frm => get_obj g_form pt p
|
neuper@37906
|
512 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@38031
|
513 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
514 |
(pos'2str (p,p_)));
|
neuper@37906
|
515 |
in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
|
neuper@37926
|
516 |
SOME (f',asm) =>
|
neuper@37906
|
517 |
Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
|
neuper@37926
|
518 |
| NONE => Notappl (rls^" not applicable") end
|
neuper@37906
|
519 |
|
neuper@37906
|
520 |
|
neuper@37906
|
521 |
| applicable_in p pt (End_Ruleset) =
|
neuper@38031
|
522 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
523 |
(tac2str End_Ruleset))
|
neuper@37906
|
524 |
|
neuper@37906
|
525 |
(* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
|
neuper@37906
|
526 |
*)
|
neuper@37906
|
527 |
| applicable_in (p,p_) pt (m as Calculate op_) =
|
neuper@37935
|
528 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
529 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
530 |
else
|
neuper@37906
|
531 |
let
|
neuper@37906
|
532 |
val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
|
neuper@37906
|
533 |
val f = case p_ of
|
neuper@37906
|
534 |
Frm => get_obj g_form pt p
|
neuper@37906
|
535 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@37906
|
536 |
in if msg = "OK" then
|
neuper@37906
|
537 |
case calculate_ (assoc_thy thy') isa_fn f of
|
neuper@37926
|
538 |
SOME (f', (id, thm)) =>
|
neuper@37906
|
539 |
Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
|
neuper@37926
|
540 |
| NONE => Notappl ("'calculate "^op_^"' not applicable")
|
neuper@37906
|
541 |
else Notappl msg
|
neuper@37906
|
542 |
end
|
neuper@37906
|
543 |
|
neuper@37906
|
544 |
(*Substitute combines two different kind of "substitution":
|
neuper@37906
|
545 |
(1) subst_atomic: for ?a..?z
|
neuper@37906
|
546 |
(2) Pattern.match: for solving equational systems
|
neuper@37906
|
547 |
(which raises exn for ?a..?z)*)
|
neuper@37906
|
548 |
| applicable_in (p,p_) pt (m as Substitute sube) =
|
neuper@37935
|
549 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
550 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
551 |
else let val pp = par_pblobj pt p
|
neuper@37906
|
552 |
val thy = assoc_thy (get_obj g_domID pt pp)
|
neuper@37906
|
553 |
val f = case p_ of
|
neuper@37906
|
554 |
Frm => get_obj g_form pt p
|
neuper@37906
|
555 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@37906
|
556 |
val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
|
neuper@37906
|
557 |
val subte = sube2subte sube
|
neuper@37906
|
558 |
val subst = sube2subst thy sube
|
neuper@37906
|
559 |
in if foldl and_ (true, map contains_Var subte)
|
neuper@37906
|
560 |
(*1*)
|
neuper@37906
|
561 |
then let val f' = subst_atomic subst f
|
neuper@37906
|
562 |
in if f = f' then Notappl (sube2str sube^" not applicable")
|
neuper@37906
|
563 |
else Appl (Substitute' (subte, f, f'))
|
neuper@37906
|
564 |
end
|
neuper@37906
|
565 |
(*2*)
|
neuper@37906
|
566 |
else case rewrite_terms_ thy (assoc_rew_ord rew_ord')
|
neuper@37906
|
567 |
erls subte f of
|
neuper@37926
|
568 |
SOME (f', _) => Appl (Substitute' (subte, f, f'))
|
neuper@37926
|
569 |
| NONE => Notappl (sube2str sube^" not applicable")
|
neuper@37906
|
570 |
end
|
neuper@37906
|
571 |
(*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
|
neuper@37906
|
572 |
| applicable_in (p,p_) pt (m as Substitute sube) =
|
neuper@37935
|
573 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
574 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
575 |
else let val pp = par_pblobj pt p
|
neuper@37906
|
576 |
val thy = assoc_thy (get_obj g_domID pt pp)
|
neuper@37906
|
577 |
val f = case p_ of
|
neuper@37906
|
578 |
Frm => get_obj g_form pt p
|
neuper@37906
|
579 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@37906
|
580 |
val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
|
neuper@37906
|
581 |
val subte = sube2subte sube
|
neuper@37906
|
582 |
in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
|
neuper@37926
|
583 |
SOME (f', _) => Appl (Substitute' (subte, f, f'))
|
neuper@37926
|
584 |
| NONE => Notappl (sube2str sube^" not applicable")
|
neuper@37906
|
585 |
end
|
neuper@37906
|
586 |
------------------*)
|
neuper@37906
|
587 |
|
neuper@37906
|
588 |
| applicable_in p pt (Apply_Assumption cts') =
|
neuper@38031
|
589 |
(error ("applicable_in: not impl. for "^
|
neuper@37906
|
590 |
(tac2str (Apply_Assumption cts'))))
|
neuper@37906
|
591 |
|
neuper@37906
|
592 |
(*'logical' applicability wrt. script in locate: Inconsistent?*)
|
neuper@37906
|
593 |
| applicable_in (p,p_) pt (m as Take ct') =
|
neuper@37935
|
594 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
595 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
596 |
else
|
neuper@37906
|
597 |
let val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@37906
|
598 |
in (case parse (assoc_thy thy') ct' of
|
neuper@37926
|
599 |
SOME ct => Appl (Take' (term_of ct))
|
neuper@37926
|
600 |
| NONE => Notappl ("syntax error in "^ct'))
|
neuper@37906
|
601 |
end
|
neuper@37906
|
602 |
|
neuper@37906
|
603 |
| applicable_in p pt (Take_Inst ct') =
|
neuper@38031
|
604 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
605 |
(tac2str (Take_Inst ct')))
|
neuper@37906
|
606 |
|
neuper@37906
|
607 |
| applicable_in p pt (Group (con, ints)) =
|
neuper@38031
|
608 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
609 |
(tac2str (Group (con, ints))))
|
neuper@37906
|
610 |
|
neuper@37906
|
611 |
| applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
|
neuper@37935
|
612 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
613 |
then (*maybe Apply_Method has already been done*)
|
neuper@37906
|
614 |
case get_obj g_env pt p of
|
neuper@37926
|
615 |
SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
|
neuper@37906
|
616 |
e_term, [], subpbl domID pblID))
|
neuper@37926
|
617 |
| NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
618 |
else (*somewhere later in the script*)
|
neuper@37906
|
619 |
Appl (Subproblem' ((domID, pblID, e_metID), [],
|
neuper@37906
|
620 |
e_term, [], subpbl domID pblID))
|
neuper@37906
|
621 |
|
neuper@37906
|
622 |
| applicable_in p pt (End_Subproblem) =
|
neuper@38031
|
623 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
624 |
(tac2str (End_Subproblem)))
|
neuper@37906
|
625 |
|
neuper@37906
|
626 |
| applicable_in p pt (CAScmd ct') =
|
neuper@38031
|
627 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
628 |
(tac2str (CAScmd ct')))
|
neuper@37906
|
629 |
|
neuper@37906
|
630 |
| applicable_in p pt (Split_And) =
|
neuper@38031
|
631 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
632 |
(tac2str (Split_And)))
|
neuper@37906
|
633 |
| applicable_in p pt (Conclude_And) =
|
neuper@38031
|
634 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
635 |
(tac2str (Conclude_And)))
|
neuper@37906
|
636 |
| applicable_in p pt (Split_Or) =
|
neuper@38031
|
637 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
638 |
(tac2str (Split_Or)))
|
neuper@37906
|
639 |
| applicable_in p pt (Conclude_Or) =
|
neuper@38031
|
640 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
641 |
(tac2str (Conclude_Or)))
|
neuper@37906
|
642 |
|
neuper@37906
|
643 |
| applicable_in (p,p_) pt (Begin_Trans) =
|
neuper@37906
|
644 |
let
|
neuper@37906
|
645 |
val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
|
neuper@37906
|
646 |
(*_____ implizit Take in gen*)
|
neuper@37906
|
647 |
Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
|
neuper@37906
|
648 |
| Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
|
neuper@38031
|
649 |
| _ => error ("applicable_in: call by "^
|
neuper@37906
|
650 |
(pos'2str (p,p_)));
|
neuper@37906
|
651 |
val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@37906
|
652 |
in (Appl (Begin_Trans' f))
|
neuper@38031
|
653 |
handle _ => error ("applicable_in: Begin_Trans finds \
|
neuper@37906
|
654 |
\syntaxerror in '"^(term2str f)^"'") end
|
neuper@37906
|
655 |
|
neuper@37906
|
656 |
(*TODO: check parent branches*)
|
neuper@37906
|
657 |
| applicable_in (p,p_) pt (End_Trans) =
|
neuper@37906
|
658 |
let val thy' = get_obj g_domID pt (par_pblobj pt p);
|
neuper@37906
|
659 |
in if p_ = Res
|
neuper@37906
|
660 |
then Appl (End_Trans' (get_obj g_result pt p))
|
neuper@37906
|
661 |
else Notappl "'End_Trans' is not applicable at \
|
neuper@37906
|
662 |
\the beginning of a transitive sequence"
|
neuper@37906
|
663 |
(*TODO: check parent branches*)
|
neuper@37906
|
664 |
end
|
neuper@37906
|
665 |
|
neuper@37906
|
666 |
| applicable_in p pt (Begin_Sequ) =
|
neuper@38031
|
667 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
668 |
(tac2str (Begin_Sequ)))
|
neuper@37906
|
669 |
| applicable_in p pt (End_Sequ) =
|
neuper@38031
|
670 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
671 |
(tac2str (End_Sequ)))
|
neuper@37906
|
672 |
| applicable_in p pt (Split_Intersect) =
|
neuper@38031
|
673 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
674 |
(tac2str (Split_Intersect)))
|
neuper@37906
|
675 |
| applicable_in p pt (End_Intersect) =
|
neuper@38031
|
676 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
677 |
(tac2str (End_Intersect)))
|
neuper@37906
|
678 |
(* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
|
neuper@37906
|
679 |
val (vvv,ppp) = vp;
|
neuper@37906
|
680 |
|
neuper@37906
|
681 |
val Check_elementwise pred = m;
|
neuper@37906
|
682 |
|
neuper@37906
|
683 |
val ((p,p_), Check_elementwise pred) = (p, m);
|
neuper@37906
|
684 |
*)
|
neuper@37906
|
685 |
| applicable_in (p,p_) pt (m as Check_elementwise pred) =
|
neuper@37935
|
686 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
687 |
then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
688 |
else
|
neuper@37906
|
689 |
let
|
neuper@37906
|
690 |
val pp = par_pblobj pt p;
|
neuper@37906
|
691 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
692 |
val thy = assoc_thy thy'
|
neuper@37906
|
693 |
val metID = (get_obj g_metID pt pp)
|
neuper@37906
|
694 |
val {crls,...} = get_met metID
|
neuper@38015
|
695 |
(*val _=tracing("### applicable_in Check_elementwise: crls= "^crls)
|
neuper@38015
|
696 |
val _=tracing("### applicable_in Check_elementwise: pred= "^pred)*)
|
neuper@37906
|
697 |
(*val erl = the (assoc'(!ruleset',crls))*)
|
neuper@37906
|
698 |
val (f,asm) = case p_ of
|
neuper@37906
|
699 |
Frm => (get_obj g_form pt p , [])
|
neuper@37906
|
700 |
| Res => get_obj g_result pt p;
|
neuper@38015
|
701 |
(*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)
|
neuper@37906
|
702 |
val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
|
neuper@38015
|
703 |
(*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^
|
neuper@37906
|
704 |
pair2str(term2str v,term2str p))*)
|
neuper@37906
|
705 |
in case f of
|
neuper@37906
|
706 |
Const ("List.list.Cons",_) $ _ $ _ =>
|
neuper@37906
|
707 |
Appl (Check_elementwise'
|
neuper@37906
|
708 |
(f, pred,
|
neuper@38015
|
709 |
((*tracing("### applicable_in Check_elementwise: --> "^
|
neuper@37906
|
710 |
(res2str (check_elementwise thy crls f vp)));*)
|
neuper@37906
|
711 |
check_elementwise thy crls f vp)))
|
neuper@37906
|
712 |
| Const ("Tools.UniversalList",_) =>
|
neuper@37906
|
713 |
Appl (Check_elementwise' (f, pred, (f,asm)))
|
neuper@37906
|
714 |
| Const ("List.list.Nil",_) =>
|
neuper@37906
|
715 |
(*Notappl "not applicable to empty list" 3.6.03*)
|
neuper@37906
|
716 |
Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))
|
neuper@37906
|
717 |
| _ => Notappl ("not applicable: "^(term2str f)^" should be constants")
|
neuper@37906
|
718 |
end
|
neuper@37906
|
719 |
|
neuper@37906
|
720 |
| applicable_in (p,p_) pt Or_to_List =
|
neuper@37935
|
721 |
if member op = [Pbl,Met] p_
|
neuper@37906
|
722 |
then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
|
neuper@37906
|
723 |
else
|
neuper@37906
|
724 |
let
|
neuper@37906
|
725 |
val pp = par_pblobj pt p;
|
neuper@37906
|
726 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
727 |
val thy = assoc_thy thy';
|
neuper@37906
|
728 |
val f = case p_ of
|
neuper@37906
|
729 |
Frm => get_obj g_form pt p
|
neuper@37906
|
730 |
| Res => (fst o (get_obj g_result pt)) p;
|
neuper@37906
|
731 |
in (let val ls = or2list f
|
neuper@37906
|
732 |
in Appl (Or_to_List' (f, ls)) end)
|
neuper@37906
|
733 |
handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
|
neuper@37906
|
734 |
end
|
neuper@37906
|
735 |
|
neuper@37906
|
736 |
| applicable_in p pt (Collect_Trues) =
|
neuper@38031
|
737 |
error ("applicable_in: not impl. for "^
|
neuper@37906
|
738 |
(tac2str (Collect_Trues)))
|
neuper@37906
|
739 |
|
neuper@37906
|
740 |
| applicable_in p pt (Empty_Tac) =
|
neuper@37906
|
741 |
Notappl "Empty_Tac is not applicable"
|
neuper@37906
|
742 |
|
neuper@37906
|
743 |
| applicable_in (p,p_) pt (Tac id) =
|
neuper@37906
|
744 |
let
|
neuper@37906
|
745 |
val pp = par_pblobj pt p;
|
neuper@37906
|
746 |
val thy' = (get_obj g_domID pt pp):theory';
|
neuper@37906
|
747 |
val thy = assoc_thy thy';
|
neuper@37906
|
748 |
val f = case p_ of
|
neuper@37906
|
749 |
Frm => get_obj g_form pt p
|
neuper@37906
|
750 |
| Res => (fst o (get_obj g_result pt)) p;
|
neuper@37906
|
751 |
in case id of
|
neuper@37906
|
752 |
"subproblem_equation_dummy" =>
|
neuper@37906
|
753 |
if is_expliceq f
|
neuper@37906
|
754 |
then Appl (Tac_ (thy, term2str f, id,
|
neuper@37906
|
755 |
"subproblem_equation_dummy ("^(term2str f)^")"))
|
neuper@37906
|
756 |
else Notappl "applicable only to equations made explicit"
|
neuper@37906
|
757 |
| "solve_equation_dummy" =>
|
neuper@38015
|
758 |
let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "
|
neuper@37906
|
759 |
^f);*)
|
neuper@37906
|
760 |
val (id',f') = split_dummy (term2str f);
|
neuper@38015
|
761 |
(*val _= tracing("### applicable_in: f'= "^f');*)
|
neuper@37906
|
762 |
(*val _= (term_of o the o (parse thy)) f';*)
|
neuper@38015
|
763 |
(*val _= tracing"### applicable_in: solve_equation_dummy";*)
|
neuper@37906
|
764 |
in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
|
neuper@37906
|
765 |
else if is_expliceq ((term_of o the o (parse thy)) f')
|
neuper@37906
|
766 |
then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
|
neuper@37906
|
767 |
else error ("applicable_in: f= " ^ f') end
|
neuper@37906
|
768 |
| _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
|
neuper@37906
|
769 |
|
neuper@37906
|
770 |
| applicable_in p pt End_Proof' = Appl End_Proof''
|
neuper@37906
|
771 |
|
neuper@37906
|
772 |
| applicable_in _ _ m =
|
neuper@38031
|
773 |
error ("applicable_in called for "^(tac2str m));
|
neuper@37906
|
774 |
|
neuper@37906
|
775 |
(*WN060614 unused*)
|
neuper@37906
|
776 |
fun tac2tac_ pt p m =
|
neuper@37906
|
777 |
case applicable_in p pt m of
|
neuper@37906
|
778 |
Appl (m') => m'
|
neuper@38031
|
779 |
| Notappl _ => error ("tac2mstp': fails with"^
|
neuper@37906
|
780 |
(tac2str m));
|
neuper@37906
|
781 |
|