2 (c) Walther Neuper 2000
8 val calculate_: theory -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
9 val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
10 val eval_prog_expr: theory -> Rule_Set.T -> term -> term
11 val eval_true_: theory -> Rule_Set.T -> term -> bool
12 val eval_true: theory -> term list -> Rule_Set.T -> bool
13 val rew_sub: theory -> int -> (term * term) list -> Rule_Def.rew_ord_
14 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
15 val rewrite_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool -> thm ->
16 term -> (term * term list) option
17 val rewrite_inst_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> bool
18 -> (term * term) list -> thm -> term -> (term * term list) option
19 val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
20 val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
21 val rewrite_terms_: theory -> Rule_Def.rew_ord_ -> Rule_Set.T -> term list
22 -> term -> (term * term list) option
24 val trace_on: bool Unsynchronized.ref
25 val depth: int Unsynchronized.ref
26 val lim_deriv: int Unsynchronized.ref
29 val rewrite__: theory -> int -> (term * term) list -> Rule_Def.rew_ord_ ->
30 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
31 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
32 val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
33 val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
34 val trace1: int -> string -> unit
35 val trace_eq1 : int -> string -> Rule_Def.rule_set -> theory -> term -> unit;
36 val trace_eq2 : int -> string -> theory -> term -> term -> unit;
37 val trace_in1 : int -> string -> string -> unit;
38 val trace_in2 : int -> string -> theory -> term -> unit;
39 val trace_in3 : int -> string -> theory -> (term * 'a) option -> unit;
40 val trace_in4 : int -> string -> theory -> term list -> term list -> unit;
41 val trace_in5 : int -> string -> theory -> term list -> unit;
46 structure Rewrite(**): REWRITE(**) =
52 val trace_on = Unsynchronized.ref false;
53 (* depth of recursion in traces of the rewriter, if trace_on:=true *)
54 val depth = Unsynchronized.ref 99999;
55 (* no of rewrites exceeding this int -> NO rewrite *)
56 val lim_deriv = Unsynchronized.ref 100;
59 if ! trace_on andalso i < ! depth then tracing (idt "#" i ^ str) else ()
60 fun trace_eq1 i str rrls thy t =
61 trace i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
62 fun trace_eq2 i str thy t t' =
63 trace i (" " ^ str ^ ": \"" ^
64 UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
67 if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
68 fun trace_in1 i str thmid =
69 trace1 i (" " ^ str ^ ": \"" ^ thmid ^ "\"")
70 fun trace_in2 i str thy t =
71 trace1 i (" " ^ str ^ ": \"" ^ UnparseC.term_in_thy thy t ^ "\"");
72 fun trace_in3 i str thy pairopt =
73 trace1 i (" " ^ str ^ ": " ^ UnparseC.term_in_thy thy ((fst o the) pairopt));
74 fun trace_in4 i str thy ts ts' =
75 if ! trace_on andalso i < ! depth andalso ts <> []
76 then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy ts ^
77 " stored: " ^ UnparseC.terms_in_thy thy ts')
79 fun trace_in5 i str thy p' =
80 if ! trace_on andalso i < ! depth
81 then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_thy thy p')
84 fun rewrite__ thy i bdv tless rls put_asm thm ct =
86 val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
87 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct
88 in if rew then SOME (t', distinct op = asms) else NONE end
89 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
90 and rew_sub thy i bdv tless rls put_asm lrd r t =
92 (** )val _ = @{print}{a = "@ rew_sub: 1 < ?n \<Longrightarrow> NTH ?n..", r = UnparseC.term r};( *TODOO*)
93 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
94 (** )val _ = @{print}{a = "@ rew_sub NO: patterns..", lhs = UnparseC.term lhs, rhs = UnparseC.term rhs};( *TODOO*)
95 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
96 handle Pattern.MATCH => raise NO_REWRITE
97 (** )val _ = @{print}{a = "@ Envir.subst_term: OK gives (3 + - 1)", r' = UnparseC.term r'};( *TODOO*)
98 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
99 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
100 val _ = trace_in2 i "eval asms" thy r';
101 (** )val _ = @{print}{a = "@ eval asms", r' = UnparseC.term r'};( *TODOO*)
102 val (t'', p'') = (*conditional rewriting*)
103 let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
104 (** )val _ = @{print}{a = "@ eval__true asms", simpl_p' = UnparseC.terms simpl_p', nofalse = nofalse};( *TODOO*)
107 then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
108 else (trace_in5 i "asms false" thy p'; raise NO_REWRITE) (* don't go into subtm.of cond*)
111 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
112 then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
113 else (t'', p'', [], true)
115 ) handle NO_REWRITE =>
117 Const(s, T) => (Const(s, T), [], lrd, false)
118 | Free(s, T) => (Free(s, T), [], lrd, false)
119 | Var(n, T) => (Var(n, T), [], lrd, false)
120 | Bound i => (Bound i, [], lrd, false)
122 let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
123 in (Abs(s, T, t'), asms, [], rew) end
125 let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
127 if rew2 then (t1 $ t2', asm2, lrd, true)
129 let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
130 in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
132 and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false*)
133 if asms = [@{term True}] orelse asms = [] then ([], true)
134 else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
135 if asms = [@{term False}] then ([], false)
138 fun chk indets [] = (indets, true) (*return asms<>True until false*)
139 | chk indets (a :: asms) =
140 (case rewrite__set_ thy (i + 1) false bdv rls a of
141 NONE => (chk (indets @ [a]) asms)
143 if t = @{term True} then (chk (indets @ a') asms)
144 else if t = @{term False} then ([], false)
145 (*asm false .. thm not applied ^^^; continue until False vvv*)
146 else chk (indets @ [t] @ a') asms);
148 and rewrite__set_ thy _ _ _ Rule_Set.Empty t = (* rewrite with a rule set*)
149 raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
150 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set'*)
152 val _= trace_eq1 i "rls" rrls thy t;
153 val (t', asm, rew) = app_rev thy (i + 1) rrls t
154 in if rew then SOME (t', distinct op = asm) else NONE end
155 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
157 (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
158 datatype switch = Appl | Noap;
159 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
160 | rew_once ruls asm ct Appl [] =
161 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
162 | Rule_Set.Sequence _ => (ct, asm)
163 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
164 | rew_once ruls asm ct apno (rul :: thms) =
166 Rule.Thm (thmid, thm) =>
167 (trace_in1 i "try thm" thmid;
168 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
169 ((#erls o Rule_Set.rep) rls) put_asm thm ct of
170 NONE => rew_once ruls asm ct apno thms
171 | SOME (ct', asm') =>
172 (trace_in2 i "rewrites to" thy ct';
173 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
174 (* once again try the same rule, e.g. associativity against "()"*)
175 | Rule.Eval (cc as (op_, _)) =>
176 let val _= trace_in1 i "try calc" op_;
177 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
178 in case Eval.adhoc_thm thy cc ct of
179 NONE => rew_once ruls asm ct apno thms
182 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
183 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
184 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
185 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
186 val _ = trace_in3 i "calc. to" thy pairopt;
187 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
189 | Rule.Cal1 (cc as (op_, _)) =>
190 let val _= trace_in1 i "try cal1" op_;
191 val ct = TermC.uminus_to_string ct
192 in case Eval.adhoc_thm1_ thy cc ct of
196 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
197 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
198 val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^
199 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
200 val _ = trace_in3 i "cal1. to" thy pairopt;
204 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
205 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
206 | NONE => rew_once ruls asm ct apno thms)
207 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
208 val ruls = (#rules o Rule_Set.rep) rls;
209 val _ = trace_eq1 i "rls" rls thy ct
210 val (ct', asm') = rew_once ruls [] ct Noap ruls;
211 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end
212 (*-------------------------------------------------------------*)
213 and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms*)
214 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
215 fun chk_prepat _ _ [] _ = true
216 | chk_prepat thy erls prepat t =
218 fun chk (pres, pat) =
220 val subst: Type.tyenv * Envir.tenv =
221 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
223 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
224 end) handle Pattern.MATCH => false
225 fun scan_ _ [] = false
226 | scan_ f (pp :: pps) =
227 if f pp then true else scan_ f pps;
228 in scan_ chk prepat end;
229 (* apply the normal_form of a rev-set *)
230 fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
231 if chk_prepat thy erls prepat t then normal_form t else NONE
232 | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
233 val opt = app_rev' thy rrls t
236 SOME (t', asm) => (t', asm, true)
237 | NONE => app_sub thy i rrls t
239 and app_sub thy i rrls t = (* apply an Rrls to subterms*)
241 Const (s, T) => (Const(s, T), [], false)
242 | Free (s, T) => (Free(s, T), [], false)
243 | Var (n, T) => (Var(n, T), [], false)
244 | Bound i => (Bound i, [], false)
245 | Abs (s, T, body) =>
246 let val (t', asm, rew) = app_rev thy i rrls body
247 in (Abs(s, T, t'), asm, rew) end
249 let val (t2', asm2, rew2) = app_rev thy i rrls t2
251 if rew2 then (t1 $ t2', asm2, true)
253 let val (t1', asm1, rew1) = app_rev thy i rrls t1
254 in if rew1 then (t1' $ t2, asm1, true)
255 else (t1 $ t2, [], false)
259 (* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
260 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
262 (* rewriting without internal argument [] *)
263 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
264 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
266 (* variants of rewrite; TODO del. put_asm *)
267 fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
268 rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
269 fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
271 (* given a list of equalities (lhs = rhs) and a term,
272 replace all occurrences of lhs in the term with rhs;
273 thus the order or equalities matters: put variables in lhs first. *)
274 fun rewrite_terms_ thy ord erls equs t =
276 fun rew_ (t', asm') [] _ = (t', asm')
277 | rew_ (t', asm') (rules as r::rs) t =
279 val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
282 then rew_ (t'', asm' @ asm'') rules t''
283 else rew_ (t', asm') rs t'
285 val (t'', asm'') = rew_ (TermC.empty, []) equs t
286 in if t'' = TermC.empty then NONE else SOME (t'', asm'')
289 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
290 fun calculate_ thy isa_fn ct =
291 let val ct = TermC.uminus_to_string ct
292 in case Eval.adhoc_thm thy isa_fn ct of
294 | SOME (thmID, thm) =>
295 (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
297 | NONE => raise ERROR ""
298 in SOME (rew, (thmID, thm)) end)
299 handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite")
302 fun eval_prog_expr thy srls t =
303 let val rew = rewrite_set_ thy false srls t;
304 in case rew of SOME (res,_) => res | NONE => t end;
306 fun eval_true_ _ _ (Const ("HOL.True",_)) = true
307 | eval_true_ thy rls t =
308 case rewrite_set_ thy false rls t of
309 SOME (Const ("HOL.True",_),_) => true