neuper@37906
|
1 |
(* isac's rewriter
|
neuper@37906
|
2 |
(c) Walther Neuper 2000
|
neuper@37906
|
3 |
|
neuper@37947
|
4 |
use"ProgLang/rewrite.sml";
|
neuper@37906
|
5 |
use"rewrite.sml";
|
neuper@37906
|
6 |
*)
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
exception NO_REWRITE;
|
neuper@37906
|
10 |
exception STOP_REW_SUB; (*WN050820 quick and dirty*)
|
neuper@37906
|
11 |
|
neuper@52101
|
12 |
fun trace i str =
|
neuper@52101
|
13 |
if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()
|
neuper@52101
|
14 |
fun trace1 i str =
|
neuper@52101
|
15 |
if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
|
neuper@52101
|
16 |
|
neuper@52084
|
17 |
(*
|
neuper@52084
|
18 |
Synopsis rewriting (prep for reference manual):
|
neuper@52084
|
19 |
----------------------------------------------
|
neuper@52084
|
20 |
Rewriting uses theorems for transforming terms. However, not all kinds
|
neuper@52084
|
21 |
of such transformations can be done by rewriting. Examples are
|
neuper@52084
|
22 |
calculation with numerals or cancellation of fractions.
|
neuper@52084
|
23 |
|
neuper@52084
|
24 |
Isac tries to present transformations like calculations or cancellation
|
neuper@52084
|
25 |
as simple rewrite steps for the naive user. However, some of such
|
neuper@52084
|
26 |
transformations should be transparent to the user by single-stepping.
|
neuper@52084
|
27 |
For instance, cancellation involves interesting CA algorithms like
|
neuper@52084
|
28 |
GCD of multivariate polynomials.
|
neuper@52084
|
29 |
|
neuper@52084
|
30 |
Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",
|
neuper@52084
|
31 |
the former for steps which are not meant to be inspected by single-stepping
|
neuper@52084
|
32 |
the latter meant for single-stepping and providing respective mechanisms.
|
neuper@52084
|
33 |
|
neuper@52084
|
34 |
(1) Inclusion by "thm Calc" for 1-step execution
|
neuper@52084
|
35 |
TODO
|
neuper@52084
|
36 |
|
neuper@52084
|
37 |
(2) Inclusion by "Rrls" for multi-step execution
|
neuper@52084
|
38 |
TODO
|
neuper@52084
|
39 |
In multi-step execution "reverse rewriting" worked only as passive presentation
|
neuper@52084
|
40 |
without any interaction. So the functions init_state, locate_rule etc are just dummies.
|
neuper@52084
|
41 |
TODO
|
neuper@52084
|
42 |
? multi-step execution did never work.
|
neuper@52084
|
43 |
what worked is "reverse rewriting",
|
neuper@52084
|
44 |
i.e. presentation of intermediate steps *without* interaction
|
neuper@52084
|
45 |
TODO
|
neuper@52084
|
46 |
# type rule and scr | Rfuns
|
neuper@52084
|
47 |
# type rrlsstate = (*state for reverse rewriting*)
|
neuper@52084
|
48 |
# type and rls | Rrls
|
neuper@52084
|
49 |
all in calcelems.sml
|
neuper@52084
|
50 |
TODO
|
neuper@52084
|
51 |
*)
|
neuper@37906
|
52 |
fun rewrite__ thy i bdv tless rls put_asm thm ct =
|
neuper@38022
|
53 |
(let
|
neuper@37906
|
54 |
val (t',asms,lrd,rew) =
|
neuper@37906
|
55 |
rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
|
neuper@37906
|
56 |
(((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
|
neuper@37906
|
57 |
in if rew then SOME (t', distinct asms)
|
neuper@37906
|
58 |
else NONE end)
|
neuper@38022
|
59 |
(* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
|
neuper@37906
|
60 |
and rew_sub thy i bdv tless rls put_asm lrd r t =
|
neuper@41928
|
61 |
((*tracing ("@@@ rew_sub begin: t = "^(term2str t));
|
neuper@41921
|
62 |
tracing ("@@@ rew_sub begin: bdv = "^(PolyML.makestring bdv));
|
neuper@41928
|
63 |
tracing ("@@@ rew_sub begin: r = "^(term2str r));*)
|
neuper@37906
|
64 |
let (* copy from Pure/thm.ML: fun rewritec *)
|
neuper@37906
|
65 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
66 |
o Logic.strip_imp_concl) r;
|
neuper@37906
|
67 |
val r' = Envir.subst_term (Pattern.match thy (lhs, t)
|
neuper@37906
|
68 |
(Vartab.empty, Vartab.empty)) r;
|
neuper@38022
|
69 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
|
neuper@38022
|
70 |
(Logic.count_prems r', [], r'));
|
neuper@37906
|
71 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
72 |
o Logic.strip_imp_concl) r';
|
neuper@38015
|
73 |
(*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)
|
neuper@37906
|
74 |
val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
|
neuper@38015
|
75 |
then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
|
neuper@37976
|
76 |
val (t'',p'') = (*conditional rewriting*)
|
neuper@37906
|
77 |
let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
|
neuper@37906
|
78 |
in if nofalse
|
neuper@37906
|
79 |
then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
|
neuper@38015
|
80 |
then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
|
neuper@37906
|
81 |
" stored: "^(terms2str simpl_p'))
|
neuper@38022
|
82 |
else(); (t',simpl_p')) (* uncond.rew. from above*)
|
neuper@37906
|
83 |
else
|
neuper@37906
|
84 |
(if ! trace_rewrite andalso i < ! depth
|
neuper@38015
|
85 |
then tracing((idt"#"(i+1))^" asms false: "^(terms2str p'))
|
neuper@37906
|
86 |
else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
|
neuper@37906
|
87 |
end
|
neuper@37976
|
88 |
in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
|
neuper@37906
|
89 |
then (if ! trace_rewrite andalso i < ! depth
|
neuper@38015
|
90 |
then tracing((idt"#"i)^" not: \""^
|
neuper@37906
|
91 |
(term2str t)^"\" > \""^
|
neuper@37906
|
92 |
(term2str t')^"\"") else ();
|
neuper@37906
|
93 |
raise NO_REWRITE )
|
neuper@38015
|
94 |
else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^
|
neuper@37906
|
95 |
", p'' ="^(terms2str p'')^", true)");*)
|
neuper@37906
|
96 |
(t'',p'',[],true))
|
neuper@37906
|
97 |
end
|
neuper@37906
|
98 |
) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
|
neuper@38015
|
99 |
((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)
|
neuper@37906
|
100 |
case t of
|
neuper@37906
|
101 |
Const(s,T) => (Const(s,T),[],lrd,false)
|
neuper@37906
|
102 |
| Free(s,T) => (Free(s,T),[],lrd,false)
|
neuper@37906
|
103 |
| Var(n,T) => (Var(n,T),[],lrd,false)
|
neuper@37906
|
104 |
| Bound i => (Bound i,[],lrd,false)
|
neuper@37906
|
105 |
| Abs(s,T,body) =>
|
neuper@37906
|
106 |
let val (t', asms, lrd, rew) =
|
neuper@37906
|
107 |
rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
|
neuper@37906
|
108 |
in (Abs(s,T,t'), asms, [], rew) end
|
neuper@37906
|
109 |
| t1 $ t2 =>
|
neuper@37906
|
110 |
let val (t2', asm2, lrd, rew2) =
|
neuper@37906
|
111 |
rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
|
neuper@37906
|
112 |
in if rew2 then (t1 $ t2', asm2, lrd, true)
|
neuper@37906
|
113 |
else let val (t1', asm1, lrd, rew1) =
|
neuper@37906
|
114 |
rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
|
neuper@37906
|
115 |
in if rew1 then (t1' $ t2, asm1, lrd, true)
|
neuper@37906
|
116 |
else (t1 $ t2,[], lrd, false) end
|
neuper@37906
|
117 |
end)
|
neuper@38022
|
118 |
(* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
|
neuper@37906
|
119 |
and eval__true thy i asms bdv rls =
|
neuper@48760
|
120 |
if asms = [@{term True}] orelse asms = [] then ([], true)
|
neuper@48760
|
121 |
(* this allows to check Rrls with prepat = ([@{term True}], pat) *)
|
neuper@52101
|
122 |
else if asms = [@{term False}] then ([], false) else
|
neuper@52085
|
123 |
let
|
neuper@37906
|
124 |
fun chk indets [] = (indets, true)(*return asms<>True until false*)
|
neuper@52085
|
125 |
| chk indets (a::asms) =
|
neuper@52101
|
126 |
(case rewrite__set_ thy (i + 1) false bdv rls a of
|
neuper@52085
|
127 |
NONE => (chk (indets @ [a]) asms)
|
neuper@52085
|
128 |
| SOME (t, a') =>
|
neuper@52085
|
129 |
if t = @{term True} then (chk (indets @ a') asms)
|
neuper@52085
|
130 |
else if t = @{term False} then ([], false)
|
neuper@52085
|
131 |
(*asm false .. thm not applied ^^^; continue until False vvv*)
|
neuper@52085
|
132 |
else chk (indets @ [t] @ a') asms);
|
neuper@52085
|
133 |
in chk [] asms end
|
neuper@38022
|
134 |
(* rewrite with a rule set, which must not be the empty Erls *)
|
neuper@37906
|
135 |
and rewrite__set_ _ _ __ Erls t =
|
neuper@52101
|
136 |
error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
|
neuper@38036
|
137 |
(* rewrite with a 'reverse rule set' implemented by ML code *)
|
neuper@37906
|
138 |
| rewrite__set_ thy i _ _ (rrls as Rrls _) t =
|
neuper@52101
|
139 |
let
|
neuper@52101
|
140 |
val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
|
neuper@52101
|
141 |
val (t', asm, rew) = app_rev thy (i + 1) rrls t
|
neuper@52101
|
142 |
in if rew then SOME (t', distinct asm) else NONE end
|
neuper@38022
|
143 |
(* rewrite with a rule set containing Thms or Calculations *)
|
neuper@37906
|
144 |
| rewrite__set_ thy i put_asm bdv rls ct =
|
neuper@52101
|
145 |
let
|
neuper@52101
|
146 |
datatype switch = Appl | Noap;
|
neuper@52101
|
147 |
fun rew_once ruls asm ct Noap [] = (ct, asm)
|
neuper@52101
|
148 |
| rew_once ruls asm ct Appl [] =
|
neuper@52101
|
149 |
(case rls of Rls _ => rew_once ruls asm ct Noap ruls
|
neuper@52101
|
150 |
| Seq _ => (ct, asm))
|
neuper@52101
|
151 |
| rew_once ruls asm ct apno (rul::thms) =
|
neuper@52101
|
152 |
case rul of
|
neuper@52101
|
153 |
Thm (thmid, thm) =>
|
neuper@52101
|
154 |
(trace1 i (" try thm: " ^ thmid);
|
neuper@52101
|
155 |
case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
|
neuper@52101
|
156 |
((#erls o rep_rls) rls) put_asm thm ct of
|
neuper@52101
|
157 |
NONE => rew_once ruls asm ct apno thms
|
neuper@52101
|
158 |
| SOME (ct',asm') =>
|
neuper@52101
|
159 |
(trace1 i (" rewrites to: " ^ term2str ct');
|
neuper@52101
|
160 |
rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
|
neuper@52101
|
161 |
| Calc (cc as (op_, _)) =>
|
neuper@52101
|
162 |
let val _= trace1 i (" try calc: " ^ op_ ^ "'")
|
neuper@52101
|
163 |
val ct = uminus_to_string ct
|
neuper@52101
|
164 |
in case get_calculation_ thy cc ct of
|
neuper@52101
|
165 |
NONE => rew_once ruls asm ct apno thms
|
neuper@52101
|
166 |
| SOME (thmid, thm') =>
|
neuper@52101
|
167 |
let
|
neuper@52101
|
168 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
|
neuper@52101
|
169 |
((#erls o rep_rls) rls) put_asm thm' ct;
|
neuper@52101
|
170 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
neuper@52101
|
171 |
string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
|
neuper@52101
|
172 |
val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))
|
neuper@52101
|
173 |
in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
|
neuper@52101
|
174 |
end
|
neuper@52101
|
175 |
| Cal1 (cc as (op_, _)) =>
|
neuper@52101
|
176 |
let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
|
neuper@52101
|
177 |
val ct = uminus_to_string ct
|
neuper@52101
|
178 |
in case get_calculation1_ thy cc ct of
|
neuper@52101
|
179 |
NONE => (ct, asm)
|
neuper@52101
|
180 |
| SOME (thmid, thm') =>
|
neuper@52101
|
181 |
let
|
neuper@52101
|
182 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
|
neuper@52101
|
183 |
((#erls o rep_rls) rls) put_asm thm' ct;
|
neuper@52101
|
184 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
neuper@52101
|
185 |
string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
|
neuper@52101
|
186 |
val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))
|
neuper@52101
|
187 |
in the pairopt end
|
neuper@52101
|
188 |
end
|
neuper@52101
|
189 |
| Rls_ rls' =>
|
neuper@52101
|
190 |
(case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
|
neuper@52101
|
191 |
SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
|
neuper@52101
|
192 |
| NONE => rew_once ruls asm ct apno thms);
|
neuper@52101
|
193 |
val ruls = (#rules o rep_rls) rls;
|
neuper@52101
|
194 |
val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
|
neuper@52101
|
195 |
val (ct', asm') = rew_once ruls [] ct Noap ruls;
|
neuper@52101
|
196 |
in if ct = ct' then NONE else SOME (ct', distinct asm') end
|
neuper@37906
|
197 |
|
neuper@52085
|
198 |
(* apply an Rrls; if not applicable proceed with subterms *)
|
neuper@37906
|
199 |
and app_rev thy i rrls t =
|
neuper@52085
|
200 |
let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
|
neuper@52085
|
201 |
fun chk_prepat thy erls [] t = true
|
neuper@52085
|
202 |
| chk_prepat thy erls prepat t =
|
neuper@52085
|
203 |
let
|
neuper@52085
|
204 |
fun chk (pres, pat) =
|
neuper@52085
|
205 |
(let
|
neuper@52085
|
206 |
val subst: Type.tyenv * Envir.tenv =
|
neuper@52085
|
207 |
Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
|
neuper@52085
|
208 |
in
|
neuper@52085
|
209 |
snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
|
neuper@52085
|
210 |
end) handle _ => false
|
neuper@52085
|
211 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@52085
|
212 |
| scan_ f (pp::pps) =
|
neuper@52085
|
213 |
if f pp then true else scan_ f pps;
|
neuper@52085
|
214 |
in scan_ chk prepat end;
|
neuper@52085
|
215 |
(* apply the normal_form of a rev-set *)
|
neuper@52101
|
216 |
fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
|
neuper@52105
|
217 |
if chk_prepat thy erls prepat t then normal_form t else NONE;
|
neuper@52085
|
218 |
val opt = app_rev' thy rrls t
|
neuper@52085
|
219 |
in
|
neuper@52085
|
220 |
case opt of
|
neuper@52085
|
221 |
SOME (t', asm) => (t', asm, true)
|
neuper@52085
|
222 |
| NONE => app_sub thy i rrls t
|
neuper@52085
|
223 |
end
|
neuper@37906
|
224 |
|
neuper@52085
|
225 |
(* apply an Rrls to subterms *)
|
neuper@37906
|
226 |
and app_sub thy i rrls t =
|
neuper@52085
|
227 |
((*tracing("### app_sub: subterm = "^(term2str t));*)
|
neuper@52085
|
228 |
case t of
|
neuper@52085
|
229 |
Const (s, T) => (Const(s, T), [], false)
|
neuper@52085
|
230 |
| Free (s, T) => (Free(s, T), [], false)
|
neuper@52085
|
231 |
| Var (n, T) => (Var(n, T), [], false)
|
neuper@52085
|
232 |
| Bound i => (Bound i, [], false)
|
neuper@52085
|
233 |
| Abs (s, T, body) =>
|
neuper@37906
|
234 |
let val (t', asm, rew) = app_rev thy i rrls body
|
neuper@37906
|
235 |
in (Abs(s, T, t'), asm, rew) end
|
neuper@52085
|
236 |
| t1 $ t2 =>
|
neuper@52085
|
237 |
let val (t2', asm2, rew2) = app_rev thy i rrls t2
|
neuper@52085
|
238 |
in
|
neuper@52085
|
239 |
if rew2 then (t1 $ t2', asm2, true)
|
neuper@52085
|
240 |
else
|
neuper@52085
|
241 |
let val (t1', asm1, rew1) = app_rev thy i rrls t1
|
neuper@52085
|
242 |
in if rew1 then (t1' $ t2, asm1, true)
|
neuper@52085
|
243 |
else (t1 $ t2, [], false)
|
neuper@52085
|
244 |
end
|
neuper@52085
|
245 |
end);
|
neuper@37906
|
246 |
|
neuper@37906
|
247 |
|
neuper@37906
|
248 |
|
neuper@37906
|
249 |
(*.rewriting without argument [] for rew_ord.*)
|
neuper@37906
|
250 |
(*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
|
neuper@37906
|
251 |
fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
|
neuper@37906
|
252 |
|
neuper@52101
|
253 |
(* rewriting without internal argument [] *)
|
neuper@52101
|
254 |
fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
|
neuper@52101
|
255 |
fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
|
neuper@37906
|
256 |
|
neuper@37906
|
257 |
fun subs'2subst thy (s:subs') =
|
neuper@37906
|
258 |
(((map (apfst (term_of o the o (parse thy))))
|
neuper@37906
|
259 |
o (map (apsnd (term_of o the o (parse thy))))) s):subst;
|
neuper@37906
|
260 |
|
neuper@37906
|
261 |
(*.variants of rewrite.*)
|
neuper@37906
|
262 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
|
neuper@37906
|
263 |
thus the argument put_asm IS NOT NECESSARY -- FIXME*)
|
neuper@37906
|
264 |
(* val (rew_ord,rls,put_asm,thm,ct)=
|
neuper@37906
|
265 |
(e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
|
neuper@37906
|
266 |
*)
|
neuper@37906
|
267 |
fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
|
neuper@37906
|
268 |
(subst:(term * term) list) (thm:thm) (ct:term) =
|
neuper@37906
|
269 |
rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
|
neuper@37906
|
270 |
|
neuper@37906
|
271 |
fun rewrite_set_inst_ (thy:theory)
|
neuper@37906
|
272 |
(put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
|
neuper@37906
|
273 |
(*let
|
neuper@37906
|
274 |
val subst = subs'2subst thy subs';
|
neuper@37906
|
275 |
val subrls = instantiate_rls subs' rls
|
neuper@37906
|
276 |
in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
|
neuper@37906
|
277 |
(*end*);
|
neuper@37906
|
278 |
|
neuper@38025
|
279 |
(* given a list of equalities (lhs = rhs) and a term,
|
neuper@38025
|
280 |
replace all occurrences of lhs in the term with rhs;
|
neuper@38025
|
281 |
thus the order or equalities matters: put variables in lhs first. *)
|
neuper@38025
|
282 |
fun rewrite_terms_ thy ord erls equs t =
|
neuper@42359
|
283 |
let
|
neuper@42359
|
284 |
fun rew_ (t', asm') [] _ = (t', asm')
|
neuper@42359
|
285 |
| rew_ (t', asm') (rules as r::rs) t =
|
neuper@42359
|
286 |
let
|
neuper@42359
|
287 |
val (t'', asm'', lrd, rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
|
neuper@42359
|
288 |
in
|
neuper@42359
|
289 |
if rew
|
neuper@42359
|
290 |
then rew_ (t'', asm' @ asm'') rules t''
|
neuper@42359
|
291 |
else rew_ (t', asm') rs t'
|
neuper@42359
|
292 |
end
|
neuper@42359
|
293 |
val (t'', asm'') = rew_ (e_term, []) equs t
|
neuper@42359
|
294 |
in if t'' = e_term then NONE else SOME (t'', asm'')
|
neuper@42359
|
295 |
end;
|
neuper@37906
|
296 |
|
neuper@37906
|
297 |
(*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
|
neuper@37906
|
298 |
fun calculate_ thy isa_fn ct =
|
neuper@37906
|
299 |
let val ct = uminus_to_string ct
|
neuper@37906
|
300 |
in case get_calculation_ thy isa_fn ct of
|
neuper@37906
|
301 |
NONE => NONE
|
neuper@37906
|
302 |
| SOME (thmID, thm) =>
|
neuper@37906
|
303 |
(let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
|
neuper@37906
|
304 |
in SOME (rew,(thmID, thm)) end)
|
neuper@37906
|
305 |
handle _ => error ("calculate_: "^thmID^" does not rewrite")
|
neuper@37906
|
306 |
end;
|
neuper@37906
|
307 |
(*
|
neuper@37906
|
308 |
> val thy = InsSort.thy;
|
neuper@37906
|
309 |
> val op_ = "le"; (* < *)
|
neuper@37906
|
310 |
> val ct = (the o (parse thy))
|
neuper@37906
|
311 |
"foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
|
neuper@37906
|
312 |
> calculate_ thy op_ ct;
|
neuper@37906
|
313 |
SOME
|
neuper@37906
|
314 |
("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
|
neuper@37906
|
315 |
"(#1 < #3) = True") : (cterm * thm) option *)
|
neuper@37906
|
316 |
|
neuper@52121
|
317 |
fun get_rls_scr rls' = ((#scr o rep_rls o assoc_rls) rls')
|
neuper@52121
|
318 |
handle _ => error ("get_rls_scr: no script for " ^ rls');
|
neuper@37906
|
319 |
|
neuper@37906
|
320 |
(*make_thm added to Pure/thm.ML*)
|
neuper@37906
|
321 |
fun mk_thm thy str =
|
neuper@37906
|
322 |
let val t = (term_of o the o (parse thy)) str
|
neuper@37906
|
323 |
val t' = case t of
|
neuper@37906
|
324 |
Const ("==>",_) $ _ $ _ => t
|
neuper@37906
|
325 |
| _ => Trueprop $ t
|
neuper@37938
|
326 |
in make_thm (cterm_of thy t') end;
|
neuper@37906
|
327 |
(*
|
neuper@37906
|
328 |
val str = "?r ^^^ 2 = ?r * ?r";
|
neuper@37906
|
329 |
val thm = realpow_twoI;
|
neuper@37906
|
330 |
|
neuper@37906
|
331 |
val t1 = (#prop o rep_thm) (num_str thm);
|
neuper@37906
|
332 |
val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
|
neuper@37906
|
333 |
t1 = t2;
|
neuper@37906
|
334 |
val it = true : bool ... !!!
|
neuper@37906
|
335 |
val th1 = (num_str thm);
|
neuper@37906
|
336 |
val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
|
neuper@37906
|
337 |
th1 = th2;
|
neuper@37906
|
338 |
ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
|
neuper@37906
|
339 |
|
neuper@37906
|
340 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
neuper@37906
|
341 |
val str = "k ~= 0 ==> m * k / (n * k) = m / n";
|
neuper@37906
|
342 |
val thm = real_mult_div_cancel2;
|
neuper@37906
|
343 |
|
neuper@37906
|
344 |
val t1 = (#prop o rep_thm) (num_str thm);
|
neuper@37906
|
345 |
val t2 = ((term_of o the o (parse thy)) str);
|
neuper@37906
|
346 |
t1 = t2;
|
neuper@37906
|
347 |
val it = false : bool ... Var .. Free
|
neuper@37906
|
348 |
val th1 = (num_str thm);
|
neuper@37906
|
349 |
val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
|
neuper@37906
|
350 |
th1 = th2;
|
neuper@37906
|
351 |
ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
|
neuper@37906
|
352 |
*)
|
neuper@37906
|
353 |
|
neuper@37906
|
354 |
|
neuper@37906
|
355 |
(*prints subgoal etc.
|
neuper@37906
|
356 |
((goal thy);(topthm()) o ) str; *)
|
neuper@37906
|
357 |
(*assume rejects scheme variables
|
neuper@37938
|
358 |
assume ((cterm_of thy) (Trueprop $
|
neuper@37906
|
359 |
(term_of o the o (parse thy)) str)); *)
|
neuper@37906
|
360 |
|
neuper@37906
|
361 |
|
neuper@37906
|
362 |
(* outcommented 18.11.xx, xx < 02 -------
|
neuper@37906
|
363 |
fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
|
neuper@37906
|
364 |
| rul2rul' (Calc op_) = Calc' op_;
|
neuper@37906
|
365 |
fun rul'2rul thy (Thm'(thmid, ct')) =
|
neuper@37906
|
366 |
Thm (thmid, mk_thm thy ct')
|
neuper@37906
|
367 |
| rul'2rul thy' (Calc' op_) = Calc op_;
|
neuper@37906
|
368 |
|
neuper@37906
|
369 |
|
neuper@37906
|
370 |
fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
|
neuper@37906
|
371 |
Rls'{preconds'= map string_of_cterm preconds,
|
neuper@37906
|
372 |
rew_ord' = fst rew_ord,
|
neuper@37906
|
373 |
rules' = map rul2rul' rules}:rlsdat';
|
neuper@37906
|
374 |
|
neuper@37906
|
375 |
fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
|
neuper@37906
|
376 |
rules'=rules}:rlsdat') =
|
neuper@38041
|
377 |
let val thy = assoc_thy thy';
|
neuper@37906
|
378 |
in Rls{preconds = map (the o (parse thy)) preconds,
|
neuper@37906
|
379 |
rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
|
neuper@37906
|
380 |
rules = map (rul'2rul thy) rules}:rls end;
|
neuper@37906
|
381 |
------- *)
|
neuper@37906
|
382 |
|
neuper@37906
|
383 |
(*.get the theorem associated with the xstring-identifier;
|
neuper@37906
|
384 |
if the identifier starts with "sym_" then swap lhs = rhs around =
|
neuper@37906
|
385 |
(ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
|
neuper@37906
|
386 |
identifiers starting with "#" come from Calc and
|
neuper@37906
|
387 |
get a hand-made theorem (containing numerals only).*)
|
neuper@37906
|
388 |
fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
|
neuper@55487
|
389 |
(case Symbol.explode thmid of
|
neuper@55487
|
390 |
"s"::"y"::"m"::"_"::id =>
|
neuper@55487
|
391 |
if hd id = "#"
|
neuper@55487
|
392 |
then mk_thm thy ct'
|
neuper@55487
|
393 |
else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
|
neuper@55487
|
394 |
| id =>
|
neuper@55487
|
395 |
if hd id = "#"
|
neuper@55487
|
396 |
then mk_thm thy ct'
|
neuper@55487
|
397 |
else (num_str o (Global_Theory.get_thm thy)) thmid
|
neuper@55487
|
398 |
) handle _ =>
|
neuper@55487
|
399 |
error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
|
neuper@40836
|
400 |
(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
|
neuper@37906
|
401 |
val it = "6 = 2 * 3" : thm
|
neuper@37906
|
402 |
|
neuper@40836
|
403 |
> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
|
neuper@37906
|
404 |
val it = "0 + ?z = ?z" : thm
|
neuper@37906
|
405 |
|
neuper@40836
|
406 |
> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
|
neuper@37906
|
407 |
val it = "?t = 0 + ?t" [.] : thm
|
neuper@37906
|
408 |
|
neuper@55487
|
409 |
> assoc_thm' @{theory HOL} ("sym_real_add_zero_left","");
|
neuper@37965
|
410 |
*** Unknown theorem(s) "add_0_left"
|
neuper@37906
|
411 |
*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
|
neuper@37906
|
412 |
uncaught exception ERROR*)
|
neuper@37906
|
413 |
|
neuper@37906
|
414 |
|
neuper@37906
|
415 |
fun parse' (thy:theory') (ct:cterm') =
|
neuper@38041
|
416 |
case parse (assoc_thy thy) ct of
|
neuper@37906
|
417 |
NONE => NONE
|
neuper@37906
|
418 |
| SOME ct => SOME ((term2str (term_of ct)):cterm');
|
neuper@37906
|
419 |
|
neuper@37906
|
420 |
|
neuper@37906
|
421 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
422 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@52121
|
423 |
fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') (put_asm:bool) (thm:thm') (ct:cterm') =
|
neuper@52121
|
424 |
let val thy = assoc_thy thy';
|
neuper@52121
|
425 |
in
|
neuper@52121
|
426 |
case rewrite_ thy ((the o assoc')(!rew_ord',rew_ord))(assoc_rls rls)
|
neuper@52121
|
427 |
put_asm ((assoc_thm' thy) thm) ((term_of o the o (parse thy)) ct) of
|
neuper@52121
|
428 |
NONE => NONE
|
neuper@52121
|
429 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@52121
|
430 |
end;
|
neuper@37906
|
431 |
|
neuper@37906
|
432 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
433 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@52121
|
434 |
fun rewrite_set (thy':theory') (put_asm:bool) (rls:rls') (ct:cterm') =
|
neuper@52121
|
435 |
let val thy = (assoc_thy thy');
|
neuper@52121
|
436 |
in
|
neuper@52121
|
437 |
case rewrite_set_ thy put_asm (assoc_rls rls) ((term_of o the o (parse thy)) ct) of
|
neuper@52121
|
438 |
NONE => NONE
|
neuper@52121
|
439 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@52121
|
440 |
end;
|
neuper@37906
|
441 |
|
neuper@37906
|
442 |
fun eval_listexpr_ thy srls t =
|
neuper@52139
|
443 |
let val rew = rewrite_set_ thy false srls t;
|
neuper@52139
|
444 |
in case rew of SOME (res,_) => res | NONE => t end;
|
neuper@37906
|
445 |
|
neuper@37906
|
446 |
fun get_calculation' (thy:theory') op_ (ct:cterm') =
|
neuper@38041
|
447 |
case get_calculation_ (assoc_thy thy) op_
|
neuper@37906
|
448 |
((uminus_to_string o term_of o the o
|
neuper@38041
|
449 |
(parse (assoc_thy thy))) ct) of
|
neuper@37906
|
450 |
NONE => NONE
|
neuper@37906
|
451 |
| SOME (thmid, thm) =>
|
neuper@37906
|
452 |
SOME ((thmid, string_of_thmI thm):thm');
|
neuper@37906
|
453 |
|
neuper@37906
|
454 |
fun calculate (thy':theory') op_ (ct:cterm') =
|
neuper@38041
|
455 |
let val thy = (assoc_thy thy');
|
neuper@37906
|
456 |
in
|
neuper@37906
|
457 |
case calculate_ thy op_
|
neuper@37906
|
458 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
459 |
NONE => NONE
|
neuper@37906
|
460 |
| SOME (ct,(thmID,thm)) =>
|
neuper@37906
|
461 |
SOME (term2str ct,
|
neuper@37906
|
462 |
(thmID, string_of_thmI thm):thm')
|
neuper@37906
|
463 |
end;
|
neuper@37906
|
464 |
|
neuper@37906
|
465 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
466 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
467 |
fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
|
neuper@37906
|
468 |
(put_asm:bool) subs (thm:thm') (ct:cterm') =
|
neuper@37906
|
469 |
let
|
neuper@38041
|
470 |
val thy = assoc_thy thy';
|
neuper@37906
|
471 |
val thm = assoc_thm' thy thm; (*28.10.02*)
|
neuper@37906
|
472 |
(*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
|
neuper@37906
|
473 |
in
|
neuper@37906
|
474 |
case rewrite_ thy
|
neuper@52121
|
475 |
((the o assoc')(!rew_ord',rew_ord)) (assoc_rls rls)
|
neuper@37906
|
476 |
put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
477 |
NONE => NONE
|
neuper@37906
|
478 |
| SOME (ctm, ctms) =>
|
neuper@37906
|
479 |
SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
|
neuper@37906
|
480 |
end;
|
neuper@37906
|
481 |
|
neuper@37906
|
482 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
483 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
484 |
fun rewrite_set_inst (thy':theory') (put_asm:bool)
|
neuper@37906
|
485 |
subs' (rls:rls') (ct:cterm') =
|
neuper@37906
|
486 |
let
|
neuper@38041
|
487 |
val thy = assoc_thy thy';
|
neuper@37906
|
488 |
val rls = assoc_rls rls
|
neuper@37906
|
489 |
val subst = subs'2subst thy subs'
|
neuper@37906
|
490 |
in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
|
neuper@37906
|
491 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
492 |
NONE => NONE
|
neuper@37906
|
493 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
494 |
end;
|
neuper@37906
|
495 |
|
neuper@37906
|
496 |
|
neuper@37906
|
497 |
(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
|
neuper@41928
|
498 |
fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true
|
neuper@37906
|
499 |
|
neuper@37906
|
500 |
| eval_true' (thy':theory') (rls':rls') (t:term) =
|
neuper@38050
|
501 |
(* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
|
neuper@37906
|
502 |
*)
|
neuper@37906
|
503 |
let val ct' = term2str t;
|
neuper@37906
|
504 |
in case rewrite_set thy' false rls' ct' of
|
neuper@41928
|
505 |
SOME ("HOL.True",_) => true
|
neuper@37906
|
506 |
| _ => false
|
neuper@37906
|
507 |
end;
|
neuper@41928
|
508 |
fun eval_true_ _ _ (Const ("HOL.True",_)) = true
|
neuper@37906
|
509 |
| eval_true_ (thy':theory') rls t =
|
neuper@37906
|
510 |
case rewrite_set_ (assoc_thy thy') false rls t of
|
neuper@41928
|
511 |
SOME (Const ("HOL.True",_),_) => true
|
neuper@37906
|
512 |
| _ => false;
|
neuper@37906
|
513 |
|
neuper@37906
|
514 |
(*
|
neuper@37906
|
515 |
val test_rls =
|
neuper@37906
|
516 |
Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
|
neuper@37906
|
517 |
rules = [Calc ("matches",eval_matches "")
|
neuper@37906
|
518 |
],
|
neuper@48763
|
519 |
scr = Prog ((term_of o the o (parse thy))
|
neuper@37906
|
520 |
"empty_script")
|
neuper@37906
|
521 |
}:rls;
|
neuper@37906
|
522 |
|
neuper@37906
|
523 |
|
neuper@37906
|
524 |
|
neuper@40836
|
525 |
rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls
|
neuper@37906
|
526 |
((the o (parse thy)) "matches (?a = ?b) (x = #0)");
|
neuper@37906
|
527 |
val xxx = (term_of o the o (parse thy))
|
neuper@37906
|
528 |
"matches (?a = ?b) (x = #0)";
|
neuper@37906
|
529 |
eval_matches """" xxx thy;
|
neuper@37906
|
530 |
SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
|
neuper@41924
|
531 |
Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
|
neuper@37906
|
532 |
|
neuper@37906
|
533 |
|
neuper@37906
|
534 |
|
neuper@40836
|
535 |
rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls
|
neuper@37906
|
536 |
((the o (parse thy)) "contains_root (sqrt #0)");
|
neuper@41928
|
537 |
val it = SOME ("HOL.True",[]) : (cterm * cterm list) option
|
neuper@37906
|
538 |
|
neuper@37906
|
539 |
*)
|
neuper@37906
|
540 |
|
neuper@37906
|
541 |
|
neuper@37906
|
542 |
(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
|
neuper@37906
|
543 |
datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
|
neuper@37906
|
544 |
introduced with quick-and-dirty code*)
|
neuper@37906
|
545 |
fun determine dts =
|
neuper@37906
|
546 |
let val false_indet =
|
neuper@37906
|
547 |
filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
|
neuper@37906
|
548 |
val ts = map (#2: det * term -> term) dts
|
neuper@37906
|
549 |
in if nil = false_indet then (TRUE, ts)
|
neuper@37906
|
550 |
else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
|
neuper@37906
|
551 |
false_indet
|
neuper@37906
|
552 |
then (INDET, ts)
|
neuper@37906
|
553 |
else (FALSE, ts) end;
|
neuper@48760
|
554 |
(* val dts = [(INDET,e_term), (FALSE,@{term False}),
|
neuper@48760
|
555 |
(INDET,e_term), (TRUE,@{term True})];
|
neuper@37906
|
556 |
determine dts;
|
neuper@37906
|
557 |
val it =
|
neuper@37906
|
558 |
(FALSE,
|
neuper@41928
|
559 |
[Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),
|
neuper@41928
|
560 |
Const ("HOL.True","bool")]) : det * term list*)
|
neuper@37906
|
561 |
|
neuper@37906
|
562 |
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*)
|
neuper@48760
|
563 |
if cs = [@{term True}] orelse cs = [] then (TRUE, [])
|
neuper@48760
|
564 |
else if cs = [@{term False}] then (FALSE, cs)
|
neuper@37906
|
565 |
else
|
neuper@37906
|
566 |
let fun eval t =
|
neuper@37906
|
567 |
let val taopt = rewrite__set_ thy 1 false [] rls t
|
neuper@37906
|
568 |
in case taopt of
|
neuper@37906
|
569 |
SOME (t,_) =>
|
neuper@48760
|
570 |
if t = @{term True} then (TRUE, t)
|
neuper@48760
|
571 |
else if t = @{term False} then (FALSE, t)
|
neuper@37906
|
572 |
else (INDET, t)
|
neuper@37906
|
573 |
| NONE => (INDET, t) end
|
neuper@37906
|
574 |
in (determine o (map eval)) cs end;
|
neuper@37906
|
575 |
WN.16.5.0-------------------------------------------------------------*)
|