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