neuper@37906
|
1 |
(* isac's rewriter
|
neuper@37906
|
2 |
(c) Walther Neuper 2000
|
neuper@37906
|
3 |
*)
|
neuper@37906
|
4 |
|
wneuper@59380
|
5 |
signature REWRITE =
|
walther@59901
|
6 |
sig
|
walther@60269
|
7 |
exception NO_REWRITE
|
Walther@60539
|
8 |
val calculate_: Proof.context -> string * Eval.ml_fun -> term -> (term * (string * thm)) option
|
Walther@60500
|
9 |
val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool
|
Walther@60500
|
10 |
val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term
|
Walther@60500
|
11 |
val eval_true_: Proof.context -> Rule_Set.T -> term -> bool
|
Walther@60500
|
12 |
val eval_true: Proof.context -> term list -> Rule_Set.T -> bool
|
Walther@60509
|
13 |
val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function
|
walther@59901
|
14 |
-> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
|
Walther@60509
|
15 |
val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm ->
|
walther@59901
|
16 |
term -> (term * term list) option
|
Walther@60509
|
17 |
val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool
|
Walther@60477
|
18 |
-> Subst.T -> thm -> term -> (term * term list) option
|
Walther@60500
|
19 |
val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option
|
Walther@60500
|
20 |
val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
|
Walther@60509
|
21 |
val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list
|
walther@59901
|
22 |
-> term -> (term * term list) option
|
Walther@60592
|
23 |
(*from isac_test for Minisubpbl*)
|
Walther@60509
|
24 |
val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function ->
|
walther@59901
|
25 |
Rule_Set.T -> bool -> thm -> term -> (term * term list) option
|
Walther@60500
|
26 |
val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option
|
Walther@60592
|
27 |
val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit;
|
Walther@60592
|
28 |
|
Walther@60592
|
29 |
\<^isac_test>\<open>
|
Walther@60500
|
30 |
val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
|
Walther@60500
|
31 |
val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool
|
Walther@60500
|
32 |
val trace1: Proof.context -> int -> string -> unit
|
Walther@60500
|
33 |
val trace_eq2 : Proof.context -> int -> string -> term -> term -> unit;
|
Walther@60500
|
34 |
val trace_in1 : Proof.context -> int -> string -> string -> unit;
|
Walther@60500
|
35 |
val trace_in2 : Proof.context -> int -> string -> term -> unit;
|
Walther@60500
|
36 |
val trace_in3 : Proof.context -> int -> string -> (term * 'a) option -> unit;
|
Walther@60500
|
37 |
val trace_in4 : Proof.context -> int -> string -> term list -> term list -> unit;
|
Walther@60500
|
38 |
val trace_in5 : Proof.context -> int -> string -> term list -> unit;
|
wenzelm@60223
|
39 |
\<close>
|
walther@59901
|
40 |
end
|
wneuper@59380
|
41 |
|
Walther@60574
|
42 |
(*
|
Walther@60574
|
43 |
Must be global for re-use in other structs.
|
Walther@60574
|
44 |
|
Walther@60574
|
45 |
DOES NOT WORK IN me, etc: in Test_Code.init_calc @{context} --
|
Walther@60574
|
46 |
@{context} is overwritten by ctxt derived from Formalisation.
|
Walther@60574
|
47 |
THUS USE WITH DIRECT rewrite_, etc.
|
Walther@60574
|
48 |
*)
|
Walther@60500
|
49 |
val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
|
Walther@60501
|
50 |
(* no of rewrites exceeding this int -> NO_REWRITE *)
|
Walther@60501
|
51 |
val rewrite_limit = Attrib.setup_config_int \<^binding>\<open>rewrite_limit\<close> (K 100);
|
Walther@60501
|
52 |
|
wneuper@59380
|
53 |
(**)
|
wneuper@59380
|
54 |
structure Rewrite(**): REWRITE(**) =
|
wneuper@59380
|
55 |
struct
|
wneuper@59380
|
56 |
(**)
|
neuper@37906
|
57 |
|
neuper@37906
|
58 |
exception NO_REWRITE;
|
neuper@37906
|
59 |
|
Walther@60507
|
60 |
(* depth of recursion in traces of the rewriter, if trace_on = true *)
|
Walther@60501
|
61 |
val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);
|
walther@59901
|
62 |
|
Walther@60500
|
63 |
fun trace ctxt i str =
|
Walther@60501
|
64 |
if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
|
Walther@60501
|
65 |
then tracing (idt "#" i ^ str) else ()
|
Walther@60500
|
66 |
fun trace_eq1 ctxt i str rrls t =
|
Walther@60500
|
67 |
trace ctxt i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_ctxt ctxt t)
|
Walther@60500
|
68 |
fun trace_eq2 ctxt i str t t' =
|
Walther@60500
|
69 |
trace ctxt i (" " ^ str ^ ": \"" ^
|
Walther@60500
|
70 |
UnparseC.term_in_ctxt ctxt t ^ "\" > \"" ^ UnparseC.term_in_ctxt ctxt t' ^ "\"");
|
Walther@60500
|
71 |
fun trace1 ctxt i str =
|
Walther@60501
|
72 |
if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
|
Walther@60501
|
73 |
then tracing (idt "#" (i + 1) ^ str) else ()
|
Walther@60500
|
74 |
fun trace_in1 ctxt i str thmid =
|
Walther@60500
|
75 |
trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
|
Walther@60500
|
76 |
fun trace_in2 ctxt i str t =
|
Walther@60500
|
77 |
trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"");
|
Walther@60500
|
78 |
fun trace_in3 ctxt i str pairopt =
|
Walther@60500
|
79 |
trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));
|
Walther@60500
|
80 |
fun trace_in4 ctxt i str ts ts' =
|
Walther@60501
|
81 |
if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth andalso ts <> []
|
Walther@60500
|
82 |
then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt ts ^
|
Walther@60500
|
83 |
" stored: " ^ UnparseC.terms_in_ctxt ctxt ts')
|
walther@60262
|
84 |
else ();
|
Walther@60500
|
85 |
fun trace_in5 ctxt i str p' =
|
Walther@60501
|
86 |
if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth
|
Walther@60500
|
87 |
then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt p')
|
walther@60262
|
88 |
else();
|
Walther@60500
|
89 |
fun msg call ctxt op_ thmC t =
|
walther@60390
|
90 |
call ^ ": \n" ^
|
Walther@60592
|
91 |
"Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm_PIDE ctxt thmC) ^ ")\n" ^
|
Walther@60500
|
92 |
"but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";
|
neuper@52101
|
93 |
|
Walther@60500
|
94 |
fun rewrite__ ctxt i bdv tless rls put_asm thm ct =
|
wneuper@59381
|
95 |
let
|
Walther@60500
|
96 |
val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
|
wenzelm@60203
|
97 |
(TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
|
walther@60017
|
98 |
in if rew then SOME (t', distinct op = asms) else NONE end
|
walther@60262
|
99 |
(* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
|
Walther@60500
|
100 |
and rew_sub ctxt i bdv tless rls put_asm lrd r t =
|
neuper@38022
|
101 |
(let
|
wneuper@59381
|
102 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
|
Walther@60500
|
103 |
val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt)
|
Walther@60500
|
104 |
(lhs, t) (Vartab.empty, Vartab.empty)) r)
|
walther@60262
|
105 |
handle Pattern.MATCH => raise NO_REWRITE
|
wneuper@59381
|
106 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
wneuper@59381
|
107 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
Walther@60500
|
108 |
val _ = trace_in2 ctxt i "eval asms" r';
|
walther@60262
|
109 |
val (t'', p'') = (*conditional rewriting*)
|
Walther@60500
|
110 |
let val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls
|
wneuper@59381
|
111 |
in
|
wneuper@59381
|
112 |
if nofalse
|
Walther@60500
|
113 |
then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)
|
Walther@60500
|
114 |
else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
|
walther@60324
|
115 |
end
|
walther@60262
|
116 |
in
|
Walther@60594
|
117 |
if TermC.perm lhs rhs andalso not (tless ctxt bdv (t', t)) (*ordered rewriting*)
|
Walther@60500
|
118 |
then (trace_eq2 ctxt i "not >" t t'; raise NO_REWRITE)
|
walther@60262
|
119 |
else (t'', p'', [], true)
|
walther@60262
|
120 |
end
|
walther@60262
|
121 |
) handle NO_REWRITE =>
|
walther@60262
|
122 |
(case t of
|
walther@60262
|
123 |
Const(s, T) => (Const(s, T), [], lrd, false)
|
walther@60262
|
124 |
| Free(s, T) => (Free(s, T), [], lrd, false)
|
walther@60262
|
125 |
| Var(n, T) => (Var(n, T), [], lrd, false)
|
walther@60262
|
126 |
| Bound i => (Bound i, [], lrd, false)
|
walther@60262
|
127 |
| Abs(s, T, body) =>
|
Walther@60500
|
128 |
let val (t', asms, _ (*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.D]) r body
|
walther@60262
|
129 |
in (Abs(s, T, t'), asms, [], rew) end
|
walther@60262
|
130 |
| t1 $ t2 =>
|
Walther@60500
|
131 |
let val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
|
walther@60262
|
132 |
in
|
walther@60262
|
133 |
if rew2 then (t1 $ t2', asm2, lrd, true)
|
walther@60262
|
134 |
else
|
Walther@60500
|
135 |
let val (t1', asm1, lrd, rew1) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
|
walther@60262
|
136 |
in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
|
walther@60262
|
137 |
end)
|
Walther@60500
|
138 |
and eval__true ctxt i asms bdv rls = (* rewrite asumptions until one evaluates to false*)
|
neuper@48760
|
139 |
if asms = [@{term True}] orelse asms = [] then ([], true)
|
wneuper@59381
|
140 |
else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
|
wneuper@59381
|
141 |
if asms = [@{term False}] then ([], false)
|
wneuper@59381
|
142 |
else
|
wneuper@59381
|
143 |
let
|
wneuper@59381
|
144 |
fun chk indets [] = (indets, true) (*return asms<>True until false*)
|
wneuper@59381
|
145 |
| chk indets (a :: asms) =
|
Walther@60500
|
146 |
(case rewrite__set_ ctxt (i + 1) false bdv rls a of
|
wneuper@59381
|
147 |
NONE => (chk (indets @ [a]) asms)
|
wneuper@59381
|
148 |
| SOME (t, a') =>
|
wneuper@59381
|
149 |
if t = @{term True} then (chk (indets @ a') asms)
|
wneuper@59381
|
150 |
else if t = @{term False} then ([], false)
|
wneuper@59381
|
151 |
(*asm false .. thm not applied ^^^; continue until False vvv*)
|
wneuper@59381
|
152 |
else chk (indets @ [t] @ a') asms);
|
wneuper@59381
|
153 |
in chk [] asms end
|
Walther@60500
|
154 |
and rewrite__set_ ctxt (*1*)_ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
|
Walther@60500
|
155 |
raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_ctxt ctxt t ^ "'")
|
Walther@60500
|
156 |
| rewrite__set_ (*2*)ctxt i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
|
neuper@52101
|
157 |
let
|
Walther@60500
|
158 |
val _= trace_eq1 ctxt i "rls" rrls t;
|
Walther@60500
|
159 |
val (t', asm, rew) = app_rev ctxt (i + 1) rrls t
|
walther@60017
|
160 |
in if rew then SOME (t', distinct op = asm) else NONE end
|
Walther@60500
|
161 |
| rewrite__set_ (*3*)ctxt i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
|
neuper@52101
|
162 |
let
|
Walther@60500
|
163 |
(* attention with cp to test/..: unbound ctxt, i, bdv, rls; TODO1803? pull out to rewrite__*)
|
neuper@52101
|
164 |
datatype switch = Appl | Noap;
|
walther@60389
|
165 |
fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
|
walther@60389
|
166 |
| rew_once (*2*)ruls asm ct Appl [] =
|
walther@59851
|
167 |
(case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
|
walther@59878
|
168 |
| Rule_Set.Sequence _ => (ct, asm)
|
walther@59867
|
169 |
| rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
|
walther@60389
|
170 |
| rew_once (*3*)ruls asm ct apno (rul :: thms) =
|
neuper@52101
|
171 |
case rul of
|
wneuper@59416
|
172 |
Rule.Thm (thmid, thm) =>
|
Walther@60500
|
173 |
(trace_in1 ctxt i "try thm" thmid;
|
Walther@60500
|
174 |
case rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
|
Walther@60586
|
175 |
((#asm_rls o Rule_Set.rep) rls) put_asm thm ct of
|
neuper@52101
|
176 |
NONE => rew_once ruls asm ct apno thms
|
wneuper@59381
|
177 |
| SOME (ct', asm') =>
|
Walther@60500
|
178 |
(trace_in2 ctxt i "rewrites to" ct';
|
wneuper@59399
|
179 |
rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
|
Walther@60596
|
180 |
(* once again try the same rule, in particular commutative/associative +,* *)
|
Walther@60500
|
181 |
| Rule.Eval (cc as (op_, _)) =>
|
Walther@60500
|
182 |
let val _ = trace_in1 ctxt i "try calc" op_;
|
Walther@60519
|
183 |
in case Eval.adhoc_thm ctxt cc ct of
|
neuper@52101
|
184 |
NONE => rew_once ruls asm ct apno thms
|
wneuper@59381
|
185 |
| SOME (_, thm') =>
|
neuper@52101
|
186 |
let
|
Walther@60500
|
187 |
val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
|
Walther@60586
|
188 |
((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
|
Walther@60500
|
189 |
val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct)
|
Walther@60500
|
190 |
val _ = trace_in3 ctxt i "calc. to" pairopt;
|
neuper@52101
|
191 |
in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
|
neuper@52101
|
192 |
end
|
wneuper@59416
|
193 |
| Rule.Cal1 (cc as (op_, _)) =>
|
Walther@60500
|
194 |
let val _ = trace_in1 ctxt i "try cal1" op_;
|
Walther@60519
|
195 |
in case Eval.adhoc_thm1_ ctxt cc ct of
|
neuper@52101
|
196 |
NONE => (ct, asm)
|
wneuper@59381
|
197 |
| SOME (_, thm') =>
|
neuper@52101
|
198 |
let
|
Walther@60500
|
199 |
val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
|
Walther@60586
|
200 |
((#asm_rls o Rule_Set.rep) rls) put_asm thm' ct;
|
walther@59962
|
201 |
val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
|
Walther@60592
|
202 |
ThmC.string_of_thm_PIDE ctxt thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")
|
Walther@60500
|
203 |
val _ = trace_in3 ctxt i "cal1. to" pairopt;
|
neuper@52101
|
204 |
in the pairopt end
|
neuper@52101
|
205 |
end
|
wneuper@59416
|
206 |
| Rule.Rls_ rls' =>
|
Walther@60500
|
207 |
(case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of
|
neuper@52101
|
208 |
SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
|
wneuper@59381
|
209 |
| NONE => rew_once ruls asm ct apno thms)
|
walther@59867
|
210 |
| r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
|
walther@59852
|
211 |
val ruls = (#rules o Rule_Set.rep) rls;
|
Walther@60500
|
212 |
val _ = trace_eq1 ctxt i "rls" rls ct
|
neuper@52101
|
213 |
val (ct', asm') = rew_once ruls [] ct Noap ruls;
|
walther@60017
|
214 |
in if ct = ct' then NONE else SOME (ct', distinct op = asm') end
|
Walther@60500
|
215 |
and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
|
neuper@52085
|
216 |
let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
|
wneuper@59381
|
217 |
fun chk_prepat _ _ [] _ = true
|
Walther@60586
|
218 |
| chk_prepat ctxt asm_rls prepat t =
|
neuper@52085
|
219 |
let
|
neuper@52085
|
220 |
fun chk (pres, pat) =
|
neuper@52085
|
221 |
(let
|
neuper@52085
|
222 |
val subst: Type.tyenv * Envir.tenv =
|
Walther@60500
|
223 |
Pattern.match (Proof_Context.theory_of ctxt) (pat, t) (Vartab.empty, Vartab.empty)
|
neuper@52085
|
224 |
in
|
Walther@60586
|
225 |
snd (eval__true ctxt (i + 1) (map (Envir.subst_term subst) pres) [] asm_rls)
|
walther@60267
|
226 |
end) handle Pattern.MATCH => false
|
wneuper@59381
|
227 |
fun scan_ _ [] = false
|
wneuper@59398
|
228 |
| scan_ f (pp :: pps) =
|
neuper@52085
|
229 |
if f pp then true else scan_ f pps;
|
neuper@52085
|
230 |
in scan_ chk prepat end;
|
neuper@52085
|
231 |
(* apply the normal_form of a rev-set *)
|
Walther@60586
|
232 |
fun app_rev' ctxt (Rule_Set.Rrls {asm_rls, prepat, program = Rule.Rfuns {normal_form, ...}, ...}) t =
|
Walther@60586
|
233 |
if chk_prepat ctxt asm_rls prepat t then normal_form t else NONE
|
walther@59867
|
234 |
| app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
|
Walther@60500
|
235 |
val opt = app_rev' ctxt rrls t
|
neuper@52085
|
236 |
in
|
neuper@52085
|
237 |
case opt of
|
neuper@52085
|
238 |
SOME (t', asm) => (t', asm, true)
|
Walther@60500
|
239 |
| NONE => app_sub ctxt i rrls t
|
neuper@52085
|
240 |
end
|
Walther@60500
|
241 |
and app_sub ctxt i rrls t = (* apply an Rrls to subterms*)
|
neuper@52085
|
242 |
case t of
|
neuper@52085
|
243 |
Const (s, T) => (Const(s, T), [], false)
|
neuper@52085
|
244 |
| Free (s, T) => (Free(s, T), [], false)
|
neuper@52085
|
245 |
| Var (n, T) => (Var(n, T), [], false)
|
neuper@52085
|
246 |
| Bound i => (Bound i, [], false)
|
neuper@52085
|
247 |
| Abs (s, T, body) =>
|
Walther@60500
|
248 |
let val (t', asm, rew) = app_rev ctxt i rrls body
|
neuper@37906
|
249 |
in (Abs(s, T, t'), asm, rew) end
|
neuper@52085
|
250 |
| t1 $ t2 =>
|
Walther@60500
|
251 |
let val (t2', asm2, rew2) = app_rev ctxt i rrls t2
|
neuper@52085
|
252 |
in
|
neuper@52085
|
253 |
if rew2 then (t1 $ t2', asm2, true)
|
neuper@52085
|
254 |
else
|
Walther@60500
|
255 |
let val (t1', asm1, rew1) = app_rev ctxt i rrls t1
|
neuper@52085
|
256 |
in if rew1 then (t1' $ t2, asm1, true)
|
neuper@52085
|
257 |
else (t1 $ t2, [], false)
|
neuper@52085
|
258 |
end
|
wneuper@59381
|
259 |
end;
|
neuper@37906
|
260 |
|
walther@60324
|
261 |
(* rewriting without argument [] for rew_ord *)
|
neuper@37906
|
262 |
fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
|
neuper@37906
|
263 |
|
walther@60324
|
264 |
(* rewriting without internal arguments 1, [] *)
|
Walther@60592
|
265 |
fun rewrite_ ctxt rew_ord asm_rls bool thm term = rewrite__ ctxt 1 [] rew_ord asm_rls bool thm term;
|
Walther@60592
|
266 |
fun rewrite_set_ ctxt bool rls term = rewrite__set_ ctxt 1 bool [] rls term;
|
neuper@37906
|
267 |
|
wneuper@59381
|
268 |
(* variants of rewrite; TODO del. put_asm *)
|
Walther@60609
|
269 |
fun rewrite_inst_ ctxt rew_ord rls put_asm subst thm ct =
|
Walther@60609
|
270 |
rewrite__ ctxt 1 subst rew_ord rls put_asm thm ct;
|
Walther@60609
|
271 |
fun rewrite_set_inst_ ctxt put_asm subst rls ct = rewrite__set_ ctxt 1 put_asm subst rls ct;
|
neuper@37906
|
272 |
|
neuper@38025
|
273 |
(* given a list of equalities (lhs = rhs) and a term,
|
neuper@38025
|
274 |
replace all occurrences of lhs in the term with rhs;
|
neuper@38025
|
275 |
thus the order or equalities matters: put variables in lhs first. *)
|
Walther@60609
|
276 |
fun rewrite_terms_ ctxt ord asm_rls equs t =
|
neuper@42359
|
277 |
let
|
neuper@42359
|
278 |
fun rew_ (t', asm') [] _ = (t', asm')
|
neuper@42359
|
279 |
| rew_ (t', asm') (rules as r::rs) t =
|
neuper@42359
|
280 |
let
|
Walther@60609
|
281 |
val (t'', asm'', _(*lrd*), rew) = rew_sub ctxt 1 [] ord asm_rls false [] (HOLogic.Trueprop $ r) t
|
neuper@42359
|
282 |
in
|
neuper@42359
|
283 |
if rew
|
neuper@42359
|
284 |
then rew_ (t'', asm' @ asm'') rules t''
|
neuper@42359
|
285 |
else rew_ (t', asm') rs t'
|
neuper@42359
|
286 |
end
|
walther@59861
|
287 |
val (t'', asm'') = rew_ (TermC.empty, []) equs t
|
walther@59861
|
288 |
in if t'' = TermC.empty then NONE else SOME (t'', asm'')
|
neuper@42359
|
289 |
end;
|
neuper@37906
|
290 |
|
wneuper@59381
|
291 |
(* search ct for adjacent numerals and calculate them by operator isa_fn *)
|
Walther@60609
|
292 |
fun calculate_ ctxt (isa_fn as (id, _(*eval_fn*))) t =
|
Walther@60519
|
293 |
case Eval.adhoc_thm ctxt isa_fn t of
|
walther@60337
|
294 |
NONE => NONE
|
walther@60337
|
295 |
| SOME (thmID, thm) =>
|
Walther@60509
|
296 |
(let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of
|
walther@60337
|
297 |
SOME (rew, _) => rew
|
Walther@60500
|
298 |
| NONE => raise ERROR (msg "calculate_" ctxt id thm t)
|
walther@60337
|
299 |
in SOME (rew, (thmID, thm)) end)
|
walther@60337
|
300 |
handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");
|
neuper@37906
|
301 |
|
Walther@60609
|
302 |
fun eval_prog_expr ctxt prog_rls t =
|
Walther@60609
|
303 |
let val rew = rewrite_set_ ctxt false prog_rls t;
|
neuper@52139
|
304 |
in case rew of SOME (res,_) => res | NONE => t end;
|
neuper@37906
|
305 |
|
wenzelm@60309
|
306 |
fun eval_true_ _ _ (Const (\<^const_name>\<open>True\<close>,_)) = true
|
Walther@60609
|
307 |
| eval_true_ ctxt rls t =
|
Walther@60609
|
308 |
case rewrite_set_ ctxt false rls t of
|
Walther@60609
|
309 |
SOME (Const (\<^const_name>\<open>True\<close>, _), _) => true
|
neuper@37906
|
310 |
| _ => false;
|
neuper@37906
|
311 |
|
walther@60262
|
312 |
end
|