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@37906
|
317 |
fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
|
neuper@38031
|
318 |
handle _ => error ("get_rls_scr: no script for "^rs');
|
neuper@37906
|
319 |
|
neuper@37906
|
320 |
|
neuper@37906
|
321 |
(*make_thm added to Pure/thm.ML*)
|
neuper@37906
|
322 |
fun mk_thm thy str =
|
neuper@37906
|
323 |
let val t = (term_of o the o (parse thy)) str
|
neuper@37906
|
324 |
val t' = case t of
|
neuper@37906
|
325 |
Const ("==>",_) $ _ $ _ => t
|
neuper@37906
|
326 |
| _ => Trueprop $ t
|
neuper@37938
|
327 |
in make_thm (cterm_of thy t') end;
|
neuper@37906
|
328 |
(*
|
neuper@37906
|
329 |
val str = "?r ^^^ 2 = ?r * ?r";
|
neuper@37906
|
330 |
val thm = realpow_twoI;
|
neuper@37906
|
331 |
|
neuper@37906
|
332 |
val t1 = (#prop o rep_thm) (num_str thm);
|
neuper@37906
|
333 |
val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
|
neuper@37906
|
334 |
t1 = t2;
|
neuper@37906
|
335 |
val it = true : bool ... !!!
|
neuper@37906
|
336 |
val th1 = (num_str thm);
|
neuper@37906
|
337 |
val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
|
neuper@37906
|
338 |
th1 = th2;
|
neuper@37906
|
339 |
ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
|
neuper@37906
|
340 |
|
neuper@37906
|
341 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
neuper@37906
|
342 |
val str = "k ~= 0 ==> m * k / (n * k) = m / n";
|
neuper@37906
|
343 |
val thm = real_mult_div_cancel2;
|
neuper@37906
|
344 |
|
neuper@37906
|
345 |
val t1 = (#prop o rep_thm) (num_str thm);
|
neuper@37906
|
346 |
val t2 = ((term_of o the o (parse thy)) str);
|
neuper@37906
|
347 |
t1 = t2;
|
neuper@37906
|
348 |
val it = false : bool ... Var .. Free
|
neuper@37906
|
349 |
val th1 = (num_str thm);
|
neuper@37906
|
350 |
val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
|
neuper@37906
|
351 |
th1 = th2;
|
neuper@37906
|
352 |
ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
|
neuper@37906
|
353 |
*)
|
neuper@37906
|
354 |
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
(*prints subgoal etc.
|
neuper@37906
|
357 |
((goal thy);(topthm()) o ) str; *)
|
neuper@37906
|
358 |
(*assume rejects scheme variables
|
neuper@37938
|
359 |
assume ((cterm_of thy) (Trueprop $
|
neuper@37906
|
360 |
(term_of o the o (parse thy)) str)); *)
|
neuper@37906
|
361 |
|
neuper@37906
|
362 |
|
neuper@37906
|
363 |
(* outcommented 18.11.xx, xx < 02 -------
|
neuper@37906
|
364 |
fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
|
neuper@37906
|
365 |
| rul2rul' (Calc op_) = Calc' op_;
|
neuper@37906
|
366 |
fun rul'2rul thy (Thm'(thmid, ct')) =
|
neuper@37906
|
367 |
Thm (thmid, mk_thm thy ct')
|
neuper@37906
|
368 |
| rul'2rul thy' (Calc' op_) = Calc op_;
|
neuper@37906
|
369 |
|
neuper@37906
|
370 |
|
neuper@37906
|
371 |
fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
|
neuper@37906
|
372 |
Rls'{preconds'= map string_of_cterm preconds,
|
neuper@37906
|
373 |
rew_ord' = fst rew_ord,
|
neuper@37906
|
374 |
rules' = map rul2rul' rules}:rlsdat';
|
neuper@37906
|
375 |
|
neuper@37906
|
376 |
fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
|
neuper@37906
|
377 |
rules'=rules}:rlsdat') =
|
neuper@38041
|
378 |
let val thy = assoc_thy thy';
|
neuper@37906
|
379 |
in Rls{preconds = map (the o (parse thy)) preconds,
|
neuper@37906
|
380 |
rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
|
neuper@37906
|
381 |
rules = map (rul'2rul thy) rules}:rls end;
|
neuper@37906
|
382 |
------- *)
|
neuper@37906
|
383 |
|
neuper@37906
|
384 |
(*.get the theorem associated with the xstring-identifier;
|
neuper@37906
|
385 |
if the identifier starts with "sym_" then swap lhs = rhs around =
|
neuper@37906
|
386 |
(ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
|
neuper@37906
|
387 |
identifiers starting with "#" come from Calc and
|
neuper@37906
|
388 |
get a hand-made theorem (containing numerals only).*)
|
neuper@37906
|
389 |
fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
|
neuper@40836
|
390 |
(case Symbol.explode thmid of
|
neuper@37906
|
391 |
"s"::"y"::"m"::"_"::id =>
|
neuper@37906
|
392 |
if hd id = "#"
|
neuper@37906
|
393 |
then mk_thm thy ct'
|
neuper@41899
|
394 |
else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
|
neuper@37906
|
395 |
| id =>
|
neuper@37906
|
396 |
if hd id = "#"
|
neuper@37906
|
397 |
then mk_thm thy ct'
|
neuper@41899
|
398 |
else (num_str o (Global_Theory.get_thm thy)) thmid
|
neuper@37906
|
399 |
) handle _ =>
|
neuper@38031
|
400 |
error ("assoc_thm': '"^thmid^"' not in '"^
|
neuper@37906
|
401 |
(theory2domID thy)^"' (and parents)");
|
neuper@40836
|
402 |
(*> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_#mult_2_3","6 = 2 * 3");
|
neuper@37906
|
403 |
val it = "6 = 2 * 3" : thm
|
neuper@37906
|
404 |
|
neuper@40836
|
405 |
> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");
|
neuper@37906
|
406 |
val it = "0 + ?z = ?z" : thm
|
neuper@37906
|
407 |
|
neuper@40836
|
408 |
> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");
|
neuper@37906
|
409 |
val it = "?t = 0 + ?t" [.] : thm
|
neuper@37906
|
410 |
|
neuper@37906
|
411 |
> assoc_thm' HOL.thy ("sym_real_add_zero_left","");
|
neuper@37965
|
412 |
*** Unknown theorem(s) "add_0_left"
|
neuper@37906
|
413 |
*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
|
neuper@37906
|
414 |
uncaught exception ERROR*)
|
neuper@37906
|
415 |
|
neuper@37906
|
416 |
|
neuper@37906
|
417 |
fun parse' (thy:theory') (ct:cterm') =
|
neuper@38041
|
418 |
case parse (assoc_thy thy) ct of
|
neuper@37906
|
419 |
NONE => NONE
|
neuper@37906
|
420 |
| SOME ct => SOME ((term2str (term_of ct)):cterm');
|
neuper@37906
|
421 |
|
neuper@37906
|
422 |
|
neuper@37906
|
423 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
424 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
425 |
fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
|
neuper@37906
|
426 |
(put_asm:bool) (thm:thm') (ct:cterm') =
|
neuper@37906
|
427 |
(* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);
|
neuper@37906
|
428 |
*)
|
neuper@38041
|
429 |
let val thy = assoc_thy thy';
|
neuper@37906
|
430 |
in
|
neuper@37906
|
431 |
case rewrite_ thy
|
neuper@37906
|
432 |
((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))
|
neuper@37906
|
433 |
put_asm ((assoc_thm' thy) thm)
|
neuper@37906
|
434 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
435 |
NONE => NONE
|
neuper@37906
|
436 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
437 |
end;
|
neuper@37906
|
438 |
|
neuper@37906
|
439 |
(*
|
neuper@38058
|
440 |
val thy = "RatArith";
|
neuper@37906
|
441 |
val rew_ord = "dummy_ord";
|
neuper@37906
|
442 |
> val rls = "eval_rls";
|
neuper@37906
|
443 |
val put_asm = true;
|
neuper@37906
|
444 |
val thm = ("square_equation_left","");
|
neuper@37906
|
445 |
val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
|
neuper@37906
|
446 |
|
neuper@38041
|
447 |
val Zthy = assoc_thy thy;
|
neuper@37906
|
448 |
val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
|
neuper@37906
|
449 |
val Zrls = ((the o assoc')(!ruleset',rls));
|
neuper@37906
|
450 |
val Zput_asm = put_asm;
|
neuper@37906
|
451 |
val Zthm = ((the o (assoc'_thm' thy)) thm);
|
neuper@38041
|
452 |
val Zct = ((the o (parse (assoc_thy thy))) ct);
|
neuper@37906
|
453 |
|
neuper@37906
|
454 |
rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
|
neuper@37906
|
455 |
|
neuper@37906
|
456 |
use"Isa99/interface_ME_ISA.sml";
|
neuper@37906
|
457 |
*)
|
neuper@37906
|
458 |
|
neuper@37906
|
459 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
460 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
461 |
fun rewrite_set (thy':theory') (put_asm:bool)
|
neuper@37906
|
462 |
(rls:rls') (ct:cterm') =
|
neuper@38041
|
463 |
let val thy = (assoc_thy thy');
|
neuper@37906
|
464 |
in
|
neuper@37906
|
465 |
case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))
|
neuper@37906
|
466 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
467 |
NONE => NONE
|
neuper@37906
|
468 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
469 |
end;
|
neuper@37906
|
470 |
|
neuper@37906
|
471 |
(*evaluate list-expressions
|
neuper@37906
|
472 |
should work on term, and stand in Isa99/rewrite-parse.sml,
|
neuper@37906
|
473 |
but there list_rls <- eval_binop is not yet defined*)
|
neuper@37906
|
474 |
(*fun eval_listexpr' ct =
|
neuper@38058
|
475 |
let val rew = rewrite_set "ListC" false "list_rls" ct;
|
neuper@37906
|
476 |
in case rew of
|
neuper@37906
|
477 |
SOME (res,_) => res
|
neuper@37906
|
478 |
| NONE => ct end;-----------------30.9.02---*)
|
neuper@37906
|
479 |
fun eval_listexpr_ thy srls t =
|
neuper@37906
|
480 |
(* val (thy, srls, t) =
|
neuper@37906
|
481 |
((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
|
neuper@37906
|
482 |
*)
|
neuper@37906
|
483 |
let val rew = rewrite_set_ thy false srls t;
|
neuper@37906
|
484 |
in case rew of
|
neuper@37906
|
485 |
SOME (res,_) => res
|
neuper@37906
|
486 |
| NONE => t end;
|
neuper@37906
|
487 |
|
neuper@37906
|
488 |
|
neuper@37906
|
489 |
fun get_calculation' (thy:theory') op_ (ct:cterm') =
|
neuper@38041
|
490 |
case get_calculation_ (assoc_thy thy) op_
|
neuper@37906
|
491 |
((uminus_to_string o term_of o the o
|
neuper@38041
|
492 |
(parse (assoc_thy thy))) ct) of
|
neuper@37906
|
493 |
NONE => NONE
|
neuper@37906
|
494 |
| SOME (thmid, thm) =>
|
neuper@37906
|
495 |
SOME ((thmid, string_of_thmI thm):thm');
|
neuper@37906
|
496 |
|
neuper@37906
|
497 |
fun calculate (thy':theory') op_ (ct:cterm') =
|
neuper@38041
|
498 |
let val thy = (assoc_thy thy');
|
neuper@37906
|
499 |
in
|
neuper@37906
|
500 |
case calculate_ thy op_
|
neuper@37906
|
501 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
502 |
NONE => NONE
|
neuper@37906
|
503 |
| SOME (ct,(thmID,thm)) =>
|
neuper@37906
|
504 |
SOME (term2str ct,
|
neuper@37906
|
505 |
(thmID, string_of_thmI thm):thm')
|
neuper@37906
|
506 |
end;
|
neuper@37906
|
507 |
(*
|
neuper@37906
|
508 |
fun instantiate'' thy' subs ((thmid,ct'):thm') =
|
neuper@40836
|
509 |
let val thmid_ = implode ("#"::(Symbol.explode thmid)) (*see type thm'*)
|
neuper@37906
|
510 |
in (thmid_, (string_of_thmI o (read_instantiate subs))
|
neuper@37906
|
511 |
((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
|
neuper@37906
|
512 |
|
neuper@37906
|
513 |
fun instantiate_rls' thy' subs (rls:rls') =
|
neuper@37906
|
514 |
rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
|
neuper@37906
|
515 |
|
neuper@37906
|
516 |
... problem with these functions:
|
neuper@37906
|
517 |
> val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
|
neuper@37906
|
518 |
val thm = "(bdv + a = b) = (bdv = b - a)" : thm
|
neuper@37906
|
519 |
> show_types:=true; thm;
|
neuper@37906
|
520 |
val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
|
neuper@37906
|
521 |
... and this doesn't match because of too general typing (?!)
|
neuper@37906
|
522 |
and read_insitantiate doesn't instantiate the types (?!)
|
neuper@37906
|
523 |
=== solutions:
|
neuper@37906
|
524 |
(1) hard-coded type-instantiation ("'a", "RatArith.rat")
|
neuper@37906
|
525 |
(2) instantiate', instantiate ... no help by isabelle-users@ !!!
|
neuper@37906
|
526 |
=== conclusion:
|
neuper@37906
|
527 |
rewrite_inst, rewrite_set_inst circumvent the problem,
|
neuper@37906
|
528 |
according functions out-commented with 'instantiate''
|
neuper@37906
|
529 |
*)
|
neuper@37906
|
530 |
|
neuper@37906
|
531 |
(* instantiate''
|
neuper@37906
|
532 |
fun instantiate'' thy' subs ((thmid,ct'):thm') =
|
neuper@37906
|
533 |
let
|
neuper@40836
|
534 |
val thmid_ = implode ("#"::(Symbol.explode thmid)); (*see type thm'*)
|
neuper@38041
|
535 |
val thy = assoc_thy thy';
|
neuper@37906
|
536 |
val typs = map (#T o rep_cterm o the o (parse thy))
|
neuper@37906
|
537 |
((snd o split_list) subs);
|
neuper@37906
|
538 |
val ctyps = map
|
neuper@37906
|
539 |
((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
|
neuper@37906
|
540 |
((snd o split_list) subs);
|
neuper@37906
|
541 |
|
neuper@38058
|
542 |
> val thy' = "RatArith";
|
neuper@37906
|
543 |
> val subs = [("bdv","x::rat"),("zzz","z::nat")];
|
neuper@38041
|
544 |
> (the o (parse (assoc_thy thy'))) "x::rat";
|
neuper@38041
|
545 |
> (#T o rep_cterm o the o (parse (assoc_thy thy')));
|
neuper@37906
|
546 |
|
neuper@37906
|
547 |
> val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
|
neuper@38041
|
548 |
(parse (assoc_thy thy'))) "x::rat";
|
neuper@37906
|
549 |
> val bdv = (the o (parse thy)) "bdv";
|
neuper@37906
|
550 |
> val x = (the o (parse thy)) "x";
|
neuper@37906
|
551 |
> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
|
neuper@37906
|
552 |
handle e => print_exn e;
|
neuper@37906
|
553 |
uncaught exception THM
|
neuper@37906
|
554 |
raised at: thm.ML:1085.18-1085.69
|
neuper@37906
|
555 |
thm.ML:1092.34
|
neuper@37906
|
556 |
goals.ML:536.61
|
neuper@37906
|
557 |
|
neuper@37906
|
558 |
> val bdv = (the o (parse thy)) "bdv::nat";
|
neuper@37906
|
559 |
> val x = (the o (parse thy)) "x::nat";
|
neuper@37906
|
560 |
> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
|
neuper@37906
|
561 |
handle e => print_exn e;
|
neuper@37906
|
562 |
uncaught exception THM
|
neuper@37906
|
563 |
raised at: thm.ML:1085.18-1085.69
|
neuper@37906
|
564 |
thm.ML:1092.34
|
neuper@37906
|
565 |
goals.ML:536.61
|
neuper@37906
|
566 |
|
neuper@37906
|
567 |
> (instantiate' [SOME ctyp] [] isolate_bdv_add)
|
neuper@37906
|
568 |
handle e => print_exn e;
|
neuper@37906
|
569 |
uncaught exception TYPE
|
neuper@37906
|
570 |
raised at: drule.ML:613.13-615.44
|
neuper@37906
|
571 |
goals.ML:536.61
|
neuper@37906
|
572 |
|
neuper@37906
|
573 |
> val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
|
neuper@37906
|
574 |
*)
|
neuper@37906
|
575 |
|
neuper@37906
|
576 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
577 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
578 |
fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
|
neuper@37906
|
579 |
(put_asm:bool) subs (thm:thm') (ct:cterm') =
|
neuper@37906
|
580 |
let
|
neuper@38041
|
581 |
val thy = assoc_thy thy';
|
neuper@37906
|
582 |
val thm = assoc_thm' thy thm; (*28.10.02*)
|
neuper@37906
|
583 |
(*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
|
neuper@37906
|
584 |
in
|
neuper@37906
|
585 |
case rewrite_ thy
|
neuper@37906
|
586 |
((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls))
|
neuper@37906
|
587 |
put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
588 |
NONE => NONE
|
neuper@37906
|
589 |
| SOME (ctm, ctms) =>
|
neuper@37906
|
590 |
SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
|
neuper@37906
|
591 |
end;
|
neuper@37906
|
592 |
|
neuper@37906
|
593 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
594 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
595 |
fun rewrite_set_inst (thy':theory') (put_asm:bool)
|
neuper@37906
|
596 |
subs' (rls:rls') (ct:cterm') =
|
neuper@37906
|
597 |
let
|
neuper@38041
|
598 |
val thy = assoc_thy thy';
|
neuper@37906
|
599 |
val rls = assoc_rls rls
|
neuper@37906
|
600 |
val subst = subs'2subst thy subs'
|
neuper@37906
|
601 |
(*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
|
neuper@37906
|
602 |
in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
|
neuper@37906
|
603 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
604 |
NONE => NONE
|
neuper@37906
|
605 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
606 |
end;
|
neuper@37906
|
607 |
|
neuper@37906
|
608 |
|
neuper@37906
|
609 |
(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
|
neuper@41928
|
610 |
fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true
|
neuper@37906
|
611 |
|
neuper@37906
|
612 |
| eval_true' (thy':theory') (rls':rls') (t:term) =
|
neuper@38050
|
613 |
(* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
|
neuper@37906
|
614 |
*)
|
neuper@37906
|
615 |
let val ct' = term2str t;
|
neuper@37906
|
616 |
in case rewrite_set thy' false rls' ct' of
|
neuper@41928
|
617 |
SOME ("HOL.True",_) => true
|
neuper@37906
|
618 |
| _ => false
|
neuper@37906
|
619 |
end;
|
neuper@41928
|
620 |
fun eval_true_ _ _ (Const ("HOL.True",_)) = true
|
neuper@37906
|
621 |
| eval_true_ (thy':theory') rls t =
|
neuper@37906
|
622 |
case rewrite_set_ (assoc_thy thy') false rls t of
|
neuper@41928
|
623 |
SOME (Const ("HOL.True",_),_) => true
|
neuper@37906
|
624 |
| _ => false;
|
neuper@37906
|
625 |
|
neuper@37906
|
626 |
(*
|
neuper@37906
|
627 |
val test_rls =
|
neuper@37906
|
628 |
Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
|
neuper@37906
|
629 |
rules = [Calc ("matches",eval_matches "")
|
neuper@37906
|
630 |
],
|
neuper@48763
|
631 |
scr = Prog ((term_of o the o (parse thy))
|
neuper@37906
|
632 |
"empty_script")
|
neuper@37906
|
633 |
}:rls;
|
neuper@37906
|
634 |
|
neuper@37906
|
635 |
|
neuper@37906
|
636 |
|
neuper@40836
|
637 |
rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false test_rls
|
neuper@37906
|
638 |
((the o (parse thy)) "matches (?a = ?b) (x = #0)");
|
neuper@37906
|
639 |
val xxx = (term_of o the o (parse thy))
|
neuper@37906
|
640 |
"matches (?a = ?b) (x = #0)";
|
neuper@37906
|
641 |
eval_matches """" xxx thy;
|
neuper@37906
|
642 |
SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
|
neuper@41924
|
643 |
Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
|
neuper@37906
|
644 |
|
neuper@37906
|
645 |
|
neuper@37906
|
646 |
|
neuper@40836
|
647 |
rewrite_set_ (Thy_Info.get_theory "Isac") eval_rls false eval_rls
|
neuper@37906
|
648 |
((the o (parse thy)) "contains_root (sqrt #0)");
|
neuper@41928
|
649 |
val it = SOME ("HOL.True",[]) : (cterm * cterm list) option
|
neuper@37906
|
650 |
|
neuper@37906
|
651 |
*)
|
neuper@37906
|
652 |
|
neuper@37906
|
653 |
|
neuper@37906
|
654 |
(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
|
neuper@37906
|
655 |
datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
|
neuper@37906
|
656 |
introduced with quick-and-dirty code*)
|
neuper@37906
|
657 |
fun determine dts =
|
neuper@37906
|
658 |
let val false_indet =
|
neuper@37906
|
659 |
filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
|
neuper@37906
|
660 |
val ts = map (#2: det * term -> term) dts
|
neuper@37906
|
661 |
in if nil = false_indet then (TRUE, ts)
|
neuper@37906
|
662 |
else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
|
neuper@37906
|
663 |
false_indet
|
neuper@37906
|
664 |
then (INDET, ts)
|
neuper@37906
|
665 |
else (FALSE, ts) end;
|
neuper@48760
|
666 |
(* val dts = [(INDET,e_term), (FALSE,@{term False}),
|
neuper@48760
|
667 |
(INDET,e_term), (TRUE,@{term True})];
|
neuper@37906
|
668 |
determine dts;
|
neuper@37906
|
669 |
val it =
|
neuper@37906
|
670 |
(FALSE,
|
neuper@41928
|
671 |
[Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),
|
neuper@41928
|
672 |
Const ("HOL.True","bool")]) : det * term list*)
|
neuper@37906
|
673 |
|
neuper@37906
|
674 |
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
|
675 |
if cs = [@{term True}] orelse cs = [] then (TRUE, [])
|
neuper@48760
|
676 |
else if cs = [@{term False}] then (FALSE, cs)
|
neuper@37906
|
677 |
else
|
neuper@37906
|
678 |
let fun eval t =
|
neuper@37906
|
679 |
let val taopt = rewrite__set_ thy 1 false [] rls t
|
neuper@37906
|
680 |
in case taopt of
|
neuper@37906
|
681 |
SOME (t,_) =>
|
neuper@48760
|
682 |
if t = @{term True} then (TRUE, t)
|
neuper@48760
|
683 |
else if t = @{term False} then (FALSE, t)
|
neuper@37906
|
684 |
else (INDET, t)
|
neuper@37906
|
685 |
| NONE => (INDET, t) end
|
neuper@37906
|
686 |
in (determine o (map eval)) cs end;
|
neuper@37906
|
687 |
WN.16.5.0-------------------------------------------------------------*)
|