1 (* isac's rewriter |
|
2 (c) Walther Neuper 2000 |
|
3 |
|
4 use"Scripts/rewrite.sml"; |
|
5 use"rewrite.sml"; |
|
6 *) |
|
7 |
|
8 |
|
9 exception NO_REWRITE; |
|
10 exception STOP_REW_SUB; (*WN050820 quick and dirty*) |
|
11 |
|
12 (*17.6.00: rewrite by going down the term with rew_sub*) |
|
13 (* val (thy, i, bdv, tless, rls, put_asm, thm, ct) = |
|
14 (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term); |
|
15 *) |
|
16 fun rewrite__ thy i bdv tless rls put_asm thm ct = |
|
17 ((*writeln ("@@@ r..te__ begin: t = "^(term2str ct));*) |
|
18 let |
|
19 val (t',asms,lrd,rew) = |
|
20 rew_sub thy i bdv tless rls put_asm [(*root of the term*)] |
|
21 (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct; |
|
22 in if rew then SOME (t', distinct asms) |
|
23 else NONE end) |
|
24 (* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct); |
|
25 val t1 = (#prop o rep_thm) thm; |
|
26 val t2 = norm t1; |
|
27 val t3 = inst_bdv bdv t2; |
|
28 |
|
29 val thm4 = read_instantiate [("bdv","x")] thm; |
|
30 val t4 = (norm o #prop o rep_thm) thm4; |
|
31 *) |
|
32 (* val (thy, i, bdv, tless, rls, put_asm, r, t) = |
|
33 (thy, i,bdv, tless, rls, put_asm, |
|
34 (((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct); |
|
35 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
|
36 (thy, 1, [], ord, erls,false, [], r, t); |
|
37 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
|
38 (thy, i, bdv, tless, rls, put_asm, [], |
|
39 ((inst_bdv bdv) o norm o #prop o rep_thm) thm, ct); |
|
40 *) |
|
41 and rew_sub thy i bdv tless rls put_asm lrd r t = |
|
42 ((*writeln ("@@@ rew_sub begin: t = "^(term2str t));*) |
|
43 let (* copy from Pure/thm.ML: fun rewritec *) |
|
44 (*val (lhs,rhs) = (dest_equals' o strip_trueprop |
|
45 o Logic.strip_imp_concl) r; |
|
46 val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t); |
|
47 val r' = ren_inst (insts, r, lhs, t); |
|
48 val p' = map strip_trueprop (Logic.strip_imp_prems r'); |
|
49 val t' = (snd o dest_equals' o strip_trueprop |
|
50 o Logic.strip_imp_concl) r';*) |
|
51 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop |
|
52 o Logic.strip_imp_concl) r; |
|
53 val r' = Envir.subst_term (Pattern.match thy (lhs, t) |
|
54 (Vartab.empty, Vartab.empty)) r; |
|
55 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r'); |
|
56 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop |
|
57 o Logic.strip_imp_concl) r'; |
|
58 (*val _= writeln("@@@ rew_sub match: t'= "^(term2str t'));*) |
|
59 val _= if ! trace_rewrite andalso i < ! depth andalso p' <> [] |
|
60 then writeln((idt"#"(i+1))^" eval asms: "^(term2str r')) else(); |
|
61 val (t'',p'') = (*conditional rewriting*) |
|
62 let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls |
|
63 in if nofalse |
|
64 then (if ! trace_rewrite andalso i < ! depth andalso p' <> [] |
|
65 then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^ |
|
66 " stored: "^(terms2str simpl_p')) |
|
67 else(); (t',simpl_p')) (* + uncond.rew. *) |
|
68 else |
|
69 (if ! trace_rewrite andalso i < ! depth |
|
70 then writeln((idt"#"(i+1))^" asms false: "^(terms2str p')) |
|
71 else(); raise STOP_REW_SUB (*dont go into subterms of cond*)) |
|
72 end |
|
73 in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*) |
|
74 then (if ! trace_rewrite andalso i < ! depth |
|
75 then writeln((idt"#"i)^" not: \""^ |
|
76 (term2str t)^"\" > \""^ |
|
77 (term2str t')^"\"") else (); |
|
78 raise NO_REWRITE ) |
|
79 else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^ |
|
80 ", p'' ="^(terms2str p'')^", true)");*) |
|
81 (t'',p'',[],true)) |
|
82 end |
|
83 ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) => |
|
84 ((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*) |
|
85 case t of |
|
86 Const(s,T) => (Const(s,T),[],lrd,false) |
|
87 | Free(s,T) => (Free(s,T),[],lrd,false) |
|
88 | Var(n,T) => (Var(n,T),[],lrd,false) |
|
89 | Bound i => (Bound i,[],lrd,false) |
|
90 | Abs(s,T,body) => |
|
91 let val (t', asms, lrd, rew) = |
|
92 rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body |
|
93 in (Abs(s,T,t'), asms, [], rew) end |
|
94 | t1 $ t2 => |
|
95 let val (t2', asm2, lrd, rew2) = |
|
96 rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2 |
|
97 in if rew2 then (t1 $ t2', asm2, lrd, true) |
|
98 else let val (t1', asm1, lrd, rew1) = |
|
99 rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1 |
|
100 in if rew1 then (t1' $ t2, asm1, lrd, true) |
|
101 else (t1 $ t2,[], lrd, false) end |
|
102 end) |
|
103 (* val (cprems',rls)=([pre],prls); |
|
104 rewrite__set_ thy i false rls pre; |
|
105 *) |
|
106 and eval__true thy i asms bdv rls = |
|
107 (* val (thy, i, asms, bdv, rls) = (thy, (i+1), p', bdv, rls); |
|
108 *) |
|
109 if asms = [HOLogic.true_const] orelse asms = [] |
|
110 then ([], true) else if asms = [HOLogic.false_const] then ([], false) |
|
111 else let |
|
112 fun chk indets [] = (indets, true)(*return asms<>True until false*) |
|
113 | chk indets (a::asms) = |
|
114 (* val (indets, (a::asms)) = ([], asms); |
|
115 *) |
|
116 (case rewrite__set_ thy (i+1) false bdv rls a of |
|
117 NONE => (chk (indets @ [a]) asms) |
|
118 | SOME (t, a') => |
|
119 if t = HOLogic.true_const |
|
120 then (chk (indets @ a') asms) |
|
121 else if t = HOLogic.false_const then ([], false) |
|
122 (*asm false .. thm not applied ^^^; continue until False vvv*) |
|
123 else (chk (indets @ [t] @ a') asms)); |
|
124 in chk [] asms end |
|
125 |
|
126 and rewrite__set_ _ _ __ Erls t = |
|
127 raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'") |
|
128 | rewrite__set_ thy i _ _ (rrls as Rrls _) t = |
|
129 let val _= if ! trace_rewrite andalso i < ! depth |
|
130 then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^ |
|
131 (term2str t)) else () |
|
132 val (t', asm, rew) = app_rev thy (i+1) rrls t |
|
133 in if rew then SOME (t', distinct asm) |
|
134 else NONE end |
|
135 | rewrite__set_ thy i put_asm bdv rls ct = |
|
136 (* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term); |
|
137 *) |
|
138 let |
|
139 datatype switch = Appl | Noap; |
|
140 fun rew_once ruls asm ct Noap [] = (ct,asm) |
|
141 | rew_once ruls asm ct Appl [] = |
|
142 (case rls of Rls _ => rew_once ruls asm ct Noap ruls |
|
143 | Seq _ => (ct,asm)) |
|
144 | rew_once ruls asm ct apno (rul::thms) = |
|
145 (* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls); |
|
146 val Thm (thmid, thm) = rul; |
|
147 *) |
|
148 case rul of |
|
149 Thm (thmid, thm) => |
|
150 (if !trace_rewrite andalso i < ! depth |
|
151 then writeln((idt"#"(i+1))^" try thm: "^thmid) else (); |
|
152 case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
|
153 ((#erls o rep_rls) rls) put_asm thm ct of |
|
154 NONE => rew_once ruls asm ct apno thms |
|
155 | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth |
|
156 then writeln((idt"="(i+1))^" rewrites to: "^ |
|
157 (term2str ct')) else (); |
|
158 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms))) |
|
159 | Calc (cc as (op_,_)) => |
|
160 (let val _= if !trace_rewrite andalso i < ! depth then |
|
161 writeln((idt"#"(i+1))^" try calc: "^op_^"'") else (); |
|
162 val ct = uminus_to_string ct |
|
163 in case get_calculation_ thy cc ct of |
|
164 NONE => ((*writeln "@@@ rewrite__set_: get_calculation_-> NONE";*) |
|
165 rew_once ruls asm ct apno thms) |
|
166 | SOME (thmid, thm') => |
|
167 let |
|
168 val pairopt = |
|
169 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
|
170 ((#erls o rep_rls) rls) put_asm thm' ct; |
|
171 val _ = if pairopt <> NONE then () |
|
172 else raise error("rewrite_set_, rewrite_ \""^ |
|
173 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
|
174 val _ = if ! trace_rewrite andalso i < ! depth |
|
175 then writeln((idt"="(i+1))^" calc. to: "^ |
|
176 (term2str ((fst o the) pairopt))) |
|
177 else() |
|
178 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end |
|
179 end) |
|
180 (* use"Scripts/rewrite.sml"; |
|
181 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
182 | Cal1 (cc as (op_,_)) => |
|
183 (let val _= if !trace_rewrite andalso i < ! depth then |
|
184 writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else (); |
|
185 val ct = uminus_to_string ct |
|
186 in case get_calculation1_ thy cc ct of |
|
187 NONE => (ct, asm) |
|
188 | SOME (thmid, thm') => |
|
189 let |
|
190 val pairopt = |
|
191 rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) |
|
192 ((#erls o rep_rls) rls) put_asm thm' ct; |
|
193 val _ = if pairopt <> NONE then () |
|
194 else raise error("rewrite_set_, rewrite_ \""^ |
|
195 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") |
|
196 val _ = if ! trace_rewrite andalso i < ! depth |
|
197 then writeln((idt"="(i+1))^" cal1. to: "^ |
|
198 (term2str ((fst o the) pairopt))) |
|
199 else() |
|
200 in the pairopt end |
|
201 end) |
|
202 (*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
203 | Rls_ rls' => |
|
204 (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of |
|
205 SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms |
|
206 | NONE => rew_once ruls asm ct apno thms); |
|
207 |
|
208 val ruls = (#rules o rep_rls) rls; |
|
209 val _= if ! trace_rewrite andalso i < ! depth |
|
210 then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^ |
|
211 (term2str ct)) else () |
|
212 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
|
213 in if ct = ct' then NONE else SOME (ct', distinct asm') end |
|
214 |
|
215 and app_rev thy i rrls t = |
|
216 let (*.check a (precond, pattern) of a rev-set; stops with 1st true.*) |
|
217 fun chk_prepat thy erls [] t = true |
|
218 | chk_prepat thy erls prepat t = |
|
219 let fun chk (pres, pat) = |
|
220 (let val subst: Type.tyenv * Envir.tenv = |
|
221 Pattern.match thy (pat, t) |
|
222 (Vartab.empty, Vartab.empty) |
|
223 in snd (eval__true thy (i+1) |
|
224 (map (Envir.subst_term subst) pres) |
|
225 [] erls) |
|
226 end) |
|
227 handle _ => false |
|
228 fun scan_ f [] = false (*scan_ NEVER called by []*) |
|
229 | scan_ f (pp::pps) = if f pp then true |
|
230 else scan_ f pps; |
|
231 in scan_ chk prepat end; |
|
232 |
|
233 (*.apply the normal_form of a rev-set.*) |
|
234 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t = |
|
235 if chk_prepat thy erls prepat t |
|
236 then ((*writeln("### app_rev': t = "^(term2str t));*) |
|
237 normal_form t) |
|
238 else NONE; |
|
239 |
|
240 val opt = app_rev' thy rrls t |
|
241 in case opt of |
|
242 SOME (t', asm) => (t', asm, true) |
|
243 | NONE => app_sub thy i rrls t |
|
244 end |
|
245 and app_sub thy i rrls t = |
|
246 ((*writeln("### app_sub: subterm = "^(term2str t));*) |
|
247 case t of |
|
248 Const (s, T) => (Const(s, T), [], false) |
|
249 | Free (s, T) => (Free(s, T), [], false) |
|
250 | Var (n, T) => (Var(n, T), [], false) |
|
251 | Bound i => (Bound i, [], false) |
|
252 | Abs (s, T, body) => |
|
253 let val (t', asm, rew) = app_rev thy i rrls body |
|
254 in (Abs(s, T, t'), asm, rew) end |
|
255 | t1 $ t2 => |
|
256 let val (t2', asm2, rew2) = app_rev thy i rrls t2 |
|
257 in if rew2 then (t1 $ t2', asm2, true) |
|
258 else let val (t1', asm1, rew1) = app_rev thy i rrls t1 |
|
259 in if rew1 then (t1' $ t2, asm1, true) |
|
260 else (t1 $ t2, [], false) end |
|
261 end); |
|
262 |
|
263 |
|
264 |
|
265 (*.rewriting without argument [] for rew_ord.*) |
|
266 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*) |
|
267 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls; |
|
268 |
|
269 |
|
270 (*.rewriting without internal argument [] for rew_ord.*) |
|
271 (* val (thy, rew_ord, erls, bool, thm, term) = |
|
272 (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f); |
|
273 val (thy, rew_ord, erls, bool, thm, term) = |
|
274 (thy, rew_ord, erls, false, thm, t''); |
|
275 *) |
|
276 fun rewrite_ thy rew_ord erls bool thm term = |
|
277 rewrite__ thy 1 [] rew_ord erls bool thm term; |
|
278 fun rewrite_set_ thy bool rls term = |
|
279 (* val (thy, bool, rls, term) = (thy, false, srls, t); |
|
280 *) |
|
281 rewrite__set_ thy 1 bool [] rls term; |
|
282 |
|
283 |
|
284 fun subs'2subst thy (s:subs') = |
|
285 (((map (apfst (term_of o the o (parse thy)))) |
|
286 o (map (apsnd (term_of o the o (parse thy))))) s):subst; |
|
287 |
|
288 (*.variants of rewrite.*) |
|
289 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, |
|
290 thus the argument put_asm IS NOT NECESSARY -- FIXME*) |
|
291 (* val (rew_ord,rls,put_asm,thm,ct)= |
|
292 (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t); |
|
293 *) |
|
294 fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool) |
|
295 (subst:(term * term) list) (thm:thm) (ct:term) = |
|
296 rewrite__ thy 1 subst rew_ord rls put_asm thm ct; |
|
297 |
|
298 fun rewrite_set_inst_ (thy:theory) |
|
299 (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) = |
|
300 (*let |
|
301 val subst = subs'2subst thy subs'; |
|
302 val subrls = instantiate_rls subs' rls |
|
303 in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct |
|
304 (*end*); |
|
305 |
|
306 (* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t); |
|
307 *) |
|
308 (*.rewrite using a list of terms.*) |
|
309 fun rewrite_terms_ thy ord erls subte t = |
|
310 let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^ |
|
311 term_detail2str (hd subte)^ |
|
312 "### rewrite_terms_ t= '"^term2str t^"' ..."^ |
|
313 term_detail2str t);*) |
|
314 fun rew_ (t', asm') [] _ = (t', asm') |
|
315 (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t); |
|
316 2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t''); |
|
317 rew_ (t', asm') (r::rs) t; |
|
318 *) |
|
319 | rew_ (t', asm') (rules as r::rs) t = |
|
320 let val _ = writeln("rew_ "^term2str t); |
|
321 val (t'', asm'', lrd, rew) = |
|
322 rew_sub thy 1 [] ord erls false [] r t |
|
323 in if rew |
|
324 then (writeln("true rew_ "^term2str t''); |
|
325 rew_ (t'', asm' @ asm'') rules t'') |
|
326 else (writeln("false rew_ "^term2str t''); |
|
327 rew_ (t', asm') rs t') |
|
328 end |
|
329 val (t'', asm'') = rew_ (e_term, []) subte t |
|
330 in if t'' = e_term |
|
331 then NONE else SOME (t'', asm'') |
|
332 end; |
|
333 |
|
334 |
|
335 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*) |
|
336 fun calculate_ thy isa_fn ct = |
|
337 let val ct = uminus_to_string ct |
|
338 in case get_calculation_ thy isa_fn ct of |
|
339 NONE => NONE |
|
340 | SOME (thmID, thm) => |
|
341 (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct |
|
342 in SOME (rew,(thmID, thm)) end) |
|
343 handle _ => error ("calculate_: "^thmID^" does not rewrite") |
|
344 end; |
|
345 (* |
|
346 > val thy = InsSort.thy; |
|
347 > val op_ = "le"; (* < *) |
|
348 > val ct = (the o (parse thy)) |
|
349 "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"; |
|
350 > calculate_ thy op_ ct; |
|
351 SOME |
|
352 ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])", |
|
353 "(#1 < #3) = True") : (cterm * thm) option *) |
|
354 |
|
355 |
|
356 (* for test-printouts: |
|
357 val _ = writeln("in rew_sub : "^( Syntax.string_of_term (thy2ctxt thy) t)) |
|
358 val _ = writeln("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems'))) |
|
359 *) |
|
360 |
|
361 |
|
362 |
|
363 |
|
364 |
|
365 |
|
366 fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs')) |
|
367 handle _ => raise error ("get_rls_scr: no script for "^rs'); |
|
368 |
|
369 |
|
370 (*make_thm added to Pure/thm.ML*) |
|
371 fun mk_thm thy str = |
|
372 let val t = (term_of o the o (parse thy)) str |
|
373 val t' = case t of |
|
374 Const ("==>",_) $ _ $ _ => t |
|
375 | _ => Trueprop $ t |
|
376 in make_thm (cterm_of thy t') end; |
|
377 (* |
|
378 val str = "?r ^^^ 2 = ?r * ?r"; |
|
379 val thm = realpow_twoI; |
|
380 |
|
381 val t1 = (#prop o rep_thm) (num_str thm); |
|
382 val t2 = Trueprop $ ((term_of o the o (parse thy)) str); |
|
383 t1 = t2; |
|
384 val it = true : bool ... !!! |
|
385 val th1 = (num_str thm); |
|
386 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e; |
|
387 th1 = th2; |
|
388 ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?! |
|
389 |
|
390 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
391 val str = "k ~= 0 ==> m * k / (n * k) = m / n"; |
|
392 val thm = real_mult_div_cancel2; |
|
393 |
|
394 val t1 = (#prop o rep_thm) (num_str thm); |
|
395 val t2 = ((term_of o the o (parse thy)) str); |
|
396 t1 = t2; |
|
397 val it = false : bool ... Var .. Free |
|
398 val th1 = (num_str thm); |
|
399 val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e; |
|
400 th1 = th2; |
|
401 ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?! |
|
402 *) |
|
403 |
|
404 |
|
405 (*prints subgoal etc. |
|
406 ((goal thy);(topthm()) o ) str; *) |
|
407 (*assume rejects scheme variables |
|
408 assume ((cterm_of thy) (Trueprop $ |
|
409 (term_of o the o (parse thy)) str)); *) |
|
410 |
|
411 |
|
412 (* outcommented 18.11.xx, xx < 02 ------- |
|
413 fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm) |
|
414 | rul2rul' (Calc op_) = Calc' op_; |
|
415 fun rul'2rul thy (Thm'(thmid, ct')) = |
|
416 Thm (thmid, mk_thm thy ct') |
|
417 | rul'2rul thy' (Calc' op_) = Calc op_; |
|
418 |
|
419 |
|
420 fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) = |
|
421 Rls'{preconds'= map string_of_cterm preconds, |
|
422 rew_ord' = fst rew_ord, |
|
423 rules' = map rul2rul' rules}:rlsdat'; |
|
424 |
|
425 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord, |
|
426 rules'=rules}:rlsdat') = |
|
427 let val thy = the (assoc' (theory',thy')) |
|
428 in Rls{preconds = map (the o (parse thy)) preconds, |
|
429 rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))), |
|
430 rules = map (rul'2rul thy) rules}:rls end; |
|
431 ------- *) |
|
432 |
|
433 (*.get the theorem associated with the xstring-identifier; |
|
434 if the identifier starts with "sym_" then swap lhs = rhs around = |
|
435 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI); |
|
436 identifiers starting with "#" come from Calc and |
|
437 get a hand-made theorem (containing numerals only).*) |
|
438 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') = |
|
439 (case explode thmid of |
|
440 "s"::"y"::"m"::"_"::id => |
|
441 if hd id = "#" |
|
442 then mk_thm thy ct' |
|
443 else ((num_str o (PureThy.get_thm thy)) (implode id)) RS sym |
|
444 | id => |
|
445 if hd id = "#" |
|
446 then mk_thm thy ct' |
|
447 else (num_str o (PureThy.get_thm thy)) thmid |
|
448 ) handle _ => |
|
449 raise error ("assoc_thm': '"^thmid^"' not in '"^ |
|
450 (theory2domID thy)^"' (and parents)"); |
|
451 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3"); |
|
452 val it = "6 = 2 * 3" : thm |
|
453 |
|
454 > assoc_thm' Isac.thy ("real_add_zero_left",""); |
|
455 val it = "0 + ?z = ?z" : thm |
|
456 |
|
457 > assoc_thm' Isac.thy ("sym_real_add_zero_left",""); |
|
458 val it = "?t = 0 + ?t" [.] : thm |
|
459 |
|
460 > assoc_thm' HOL.thy ("sym_real_add_zero_left",""); |
|
461 *** Unknown theorem(s) "real_add_zero_left" |
|
462 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents) |
|
463 uncaught exception ERROR*) |
|
464 |
|
465 |
|
466 fun parse' (thy:theory') (ct:cterm') = |
|
467 case parse ((the o assoc')(!theory',thy)) ct of |
|
468 NONE => NONE |
|
469 | SOME ct => SOME ((term2str (term_of ct)):cterm'); |
|
470 |
|
471 |
|
472 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
|
473 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
|
474 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') |
|
475 (put_asm:bool) (thm:thm') (ct:cterm') = |
|
476 (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f); |
|
477 *) |
|
478 let val thy = (the o assoc')(!theory',thy'); |
|
479 in |
|
480 case rewrite_ thy |
|
481 ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls)) |
|
482 put_asm ((assoc_thm' thy) thm) |
|
483 ((term_of o the o (parse thy)) ct) of |
|
484 NONE => NONE |
|
485 | SOME (t, ts) => SOME (term2str t, terms2str ts) |
|
486 end; |
|
487 |
|
488 (* |
|
489 val thy = "RatArith.thy"; |
|
490 val rew_ord = "dummy_ord"; |
|
491 > val rls = "eval_rls"; |
|
492 val put_asm = true; |
|
493 val thm = ("square_equation_left",""); |
|
494 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)"; |
|
495 |
|
496 val Zthy = ((the o assoc')(!theory',thy)); |
|
497 val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord)); |
|
498 val Zrls = ((the o assoc')(!ruleset',rls)); |
|
499 val Zput_asm = put_asm; |
|
500 val Zthm = ((the o (assoc'_thm' thy)) thm); |
|
501 val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct); |
|
502 |
|
503 rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct; |
|
504 |
|
505 use"Isa99/interface_ME_ISA.sml"; |
|
506 *) |
|
507 |
|
508 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
|
509 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
|
510 fun rewrite_set (thy':theory') (put_asm:bool) |
|
511 (rls:rls') (ct:cterm') = |
|
512 let val thy = (the o assoc')(!theory',thy'); |
|
513 in |
|
514 case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls)) |
|
515 ((term_of o the o (parse thy)) ct) of |
|
516 NONE => NONE |
|
517 | SOME (t, ts) => SOME (term2str t, terms2str ts) |
|
518 end; |
|
519 |
|
520 (*evaluate list-expressions |
|
521 should work on term, and stand in Isa99/rewrite-parse.sml, |
|
522 but there list_rls <- eval_binop is not yet defined*) |
|
523 (*fun eval_listexpr' ct = |
|
524 let val rew = rewrite_set "ListG.thy" false "list_rls" ct; |
|
525 in case rew of |
|
526 SOME (res,_) => res |
|
527 | NONE => ct end;-----------------30.9.02---*) |
|
528 fun eval_listexpr_ thy srls t = |
|
529 (* val (thy, srls, t) = |
|
530 ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t)); |
|
531 *) |
|
532 let val rew = rewrite_set_ thy false srls t; |
|
533 in case rew of |
|
534 SOME (res,_) => res |
|
535 | NONE => t end; |
|
536 |
|
537 |
|
538 fun get_calculation' (thy:theory') op_ (ct:cterm') = |
|
539 case get_calculation_ ((the o assoc')(!theory',thy)) op_ |
|
540 ((uminus_to_string o term_of o the o |
|
541 (parse ((the o assoc')(!theory',thy)))) ct) of |
|
542 NONE => NONE |
|
543 | SOME (thmid, thm) => |
|
544 SOME ((thmid, string_of_thmI thm):thm'); |
|
545 |
|
546 fun calculate (thy':theory') op_ (ct:cterm') = |
|
547 let val thy = (the o assoc')(!theory',thy'); |
|
548 in |
|
549 case calculate_ thy op_ |
|
550 ((term_of o the o (parse thy)) ct) of |
|
551 NONE => NONE |
|
552 | SOME (ct,(thmID,thm)) => |
|
553 SOME (term2str ct, |
|
554 (thmID, string_of_thmI thm):thm') |
|
555 end; |
|
556 (* |
|
557 fun instantiate'' thy' subs ((thmid,ct'):thm') = |
|
558 let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*) |
|
559 in (thmid_, (string_of_thmI o (read_instantiate subs)) |
|
560 ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end; |
|
561 |
|
562 fun instantiate_rls' thy' subs (rls:rls') = |
|
563 rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat'; |
|
564 |
|
565 ... problem with these functions: |
|
566 > val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)"; |
|
567 val thm = "(bdv + a = b) = (bdv = b - a)" : thm |
|
568 > show_types:=true; thm; |
|
569 val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm |
|
570 ... and this doesn't match because of too general typing (?!) |
|
571 and read_insitantiate doesn't instantiate the types (?!) |
|
572 === solutions: |
|
573 (1) hard-coded type-instantiation ("'a", "RatArith.rat") |
|
574 (2) instantiate', instantiate ... no help by isabelle-users@ !!! |
|
575 === conclusion: |
|
576 rewrite_inst, rewrite_set_inst circumvent the problem, |
|
577 according functions out-commented with 'instantiate'' |
|
578 *) |
|
579 |
|
580 (* instantiate'' |
|
581 fun instantiate'' thy' subs ((thmid,ct'):thm') = |
|
582 let |
|
583 val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*) |
|
584 val thy = (the o assoc')(!theory',thy'); |
|
585 val typs = map (#T o rep_cterm o the o (parse thy)) |
|
586 ((snd o split_list) subs); |
|
587 val ctyps = map |
|
588 ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy)) |
|
589 ((snd o split_list) subs); |
|
590 |
|
591 > val thy' = "RatArith.thy"; |
|
592 > val subs = [("bdv","x::rat"),("zzz","z::nat")]; |
|
593 > (the o (parse ((the o assoc')(!theory',thy')))) "x::rat"; |
|
594 > (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy')))); |
|
595 |
|
596 > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o |
|
597 (parse ((the o assoc')(!theory',thy')))) "x::rat"; |
|
598 > val bdv = (the o (parse thy)) "bdv"; |
|
599 > val x = (the o (parse thy)) "x"; |
|
600 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add) |
|
601 handle e => print_exn e; |
|
602 uncaught exception THM |
|
603 raised at: thm.ML:1085.18-1085.69 |
|
604 thm.ML:1092.34 |
|
605 goals.ML:536.61 |
|
606 |
|
607 > val bdv = (the o (parse thy)) "bdv::nat"; |
|
608 > val x = (the o (parse thy)) "x::nat"; |
|
609 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add) |
|
610 handle e => print_exn e; |
|
611 uncaught exception THM |
|
612 raised at: thm.ML:1085.18-1085.69 |
|
613 thm.ML:1092.34 |
|
614 goals.ML:536.61 |
|
615 |
|
616 > (instantiate' [SOME ctyp] [] isolate_bdv_add) |
|
617 handle e => print_exn e; |
|
618 uncaught exception TYPE |
|
619 raised at: drule.ML:613.13-615.44 |
|
620 goals.ML:536.61 |
|
621 |
|
622 > val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat"; |
|
623 *) |
|
624 |
|
625 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
|
626 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
|
627 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls') |
|
628 (put_asm:bool) subs (thm:thm') (ct:cterm') = |
|
629 let |
|
630 val thy = (the o assoc')(!theory',thy'); |
|
631 val thm = assoc_thm' thy thm; (*28.10.02*) |
|
632 (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*) |
|
633 in |
|
634 case rewrite_ thy |
|
635 ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls)) |
|
636 put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of |
|
637 NONE => NONE |
|
638 | SOME (ctm, ctms) => |
|
639 SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list) |
|
640 end; |
|
641 |
|
642 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst |
|
643 thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*) |
|
644 fun rewrite_set_inst (thy':theory') (put_asm:bool) |
|
645 subs' (rls:rls') (ct:cterm') = |
|
646 let |
|
647 val thy = (the o assoc')(!theory',thy'); |
|
648 val rls = assoc_rls rls |
|
649 val subst = subs'2subst thy subs' |
|
650 (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*) |
|
651 in case rewrite_set_inst_ thy put_asm subst (*sub*)rls |
|
652 ((term_of o the o (parse thy)) ct) of |
|
653 NONE => NONE |
|
654 | SOME (t, ts) => SOME (term2str t, terms2str ts) |
|
655 end; |
|
656 |
|
657 |
|
658 (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *) |
|
659 fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true |
|
660 |
|
661 | eval_true' (thy':theory') (rls':rls') (t:term) = |
|
662 (* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres'; |
|
663 *) |
|
664 let val ct' = term2str t; |
|
665 in case rewrite_set thy' false rls' ct' of |
|
666 SOME ("True",_) => true |
|
667 | _ => false |
|
668 end; |
|
669 fun eval_true_ _ _ (Const ("True",_)) = true |
|
670 | eval_true_ (thy':theory') rls t = |
|
671 case rewrite_set_ (assoc_thy thy') false rls t of |
|
672 SOME (Const ("True",_),_) => true |
|
673 | _ => false; |
|
674 |
|
675 (* |
|
676 val test_rls = |
|
677 Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right), |
|
678 rules = [Calc ("matches",eval_matches "") |
|
679 ], |
|
680 scr = Script ((term_of o the o (parse thy)) |
|
681 "empty_script") |
|
682 }:rls; |
|
683 |
|
684 |
|
685 |
|
686 rewrite_set_ Isac.thy eval_rls false test_rls |
|
687 ((the o (parse thy)) "matches (?a = ?b) (x = #0)"); |
|
688 val xxx = (term_of o the o (parse thy)) |
|
689 "matches (?a = ?b) (x = #0)"; |
|
690 eval_matches """" xxx thy; |
|
691 SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True", |
|
692 Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#))) |
|
693 |
|
694 |
|
695 |
|
696 rewrite_set_ Isac.thy eval_rls false eval_rls |
|
697 ((the o (parse thy)) "contains_root (sqrt #0)"); |
|
698 val it = SOME ("True",[]) : (cterm * cterm list) option |
|
699 |
|
700 *) |
|
701 |
|
702 |
|
703 (*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise |
|
704 datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03 |
|
705 introduced with quick-and-dirty code*) |
|
706 fun determine dts = |
|
707 let val false_indet = |
|
708 filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts |
|
709 val ts = map (#2: det * term -> term) dts |
|
710 in if nil = false_indet then (TRUE, ts) |
|
711 else if nil = filter ((curry op= FALSE) o (#1:det * term -> det)) |
|
712 false_indet |
|
713 then (INDET, ts) |
|
714 else (FALSE, ts) end; |
|
715 (* val dts = [(INDET,e_term), (FALSE,HOLogic.false_const), |
|
716 (INDET,e_term), (TRUE,HOLogic.true_const)]; |
|
717 determine dts; |
|
718 val it = |
|
719 (FALSE, |
|
720 [Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"), |
|
721 Const ("True","bool")]) : det * term list*) |
|
722 |
|
723 fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*) |
|
724 if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, []) |
|
725 else if cs = [HOLogic.false_const] then (FALSE, cs) |
|
726 else |
|
727 let fun eval t = |
|
728 let val taopt = rewrite__set_ thy 1 false [] rls t |
|
729 in case taopt of |
|
730 SOME (t,_) => |
|
731 if t = HOLogic.true_const then (TRUE, t) |
|
732 else if t = HOLogic.false_const then (FALSE, t) |
|
733 else (INDET, t) |
|
734 | NONE => (INDET, t) end |
|
735 in (determine o (map eval)) cs end; |
|
736 WN.16.5.0-------------------------------------------------------------*) |
|