equal
deleted
inserted
replaced
171 (trace_in2 ctxt i "rewrites to" ct'; |
171 (trace_in2 ctxt i "rewrites to" ct'; |
172 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) |
172 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms))) |
173 (* once again try the same rule, e.g. associativity against "()"*) |
173 (* once again try the same rule, e.g. associativity against "()"*) |
174 | Rule.Eval (cc as (op_, _)) => |
174 | Rule.Eval (cc as (op_, _)) => |
175 let val _ = trace_in1 ctxt i "try calc" op_; |
175 let val _ = trace_in1 ctxt i "try calc" op_; |
176 in case Eval.adhoc_thm (Proof_Context.theory_of ctxt) cc ct of |
176 in case Eval.adhoc_thm ctxt cc ct of |
177 NONE => rew_once ruls asm ct apno thms |
177 NONE => rew_once ruls asm ct apno thms |
178 | SOME (_, thm') => |
178 | SOME (_, thm') => |
179 let |
179 let |
180 val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
180 val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
181 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
181 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
183 val _ = trace_in3 ctxt i "calc. to" pairopt; |
183 val _ = trace_in3 ctxt i "calc. to" pairopt; |
184 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end |
184 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end |
185 end |
185 end |
186 | Rule.Cal1 (cc as (op_, _)) => |
186 | Rule.Cal1 (cc as (op_, _)) => |
187 let val _ = trace_in1 ctxt i "try cal1" op_; |
187 let val _ = trace_in1 ctxt i "try cal1" op_; |
188 in case Eval.adhoc_thm1_ (Proof_Context.theory_of ctxt) cc ct of |
188 in case Eval.adhoc_thm1_ ctxt cc ct of |
189 NONE => (ct, asm) |
189 NONE => (ct, asm) |
190 | SOME (_, thm') => |
190 | SOME (_, thm') => |
191 let |
191 let |
192 val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
192 val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls) |
193 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
193 ((#erls o Rule_Set.rep) rls) put_asm thm' ct; |
203 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\""); |
203 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\""); |
204 val ruls = (#rules o Rule_Set.rep) rls; |
204 val ruls = (#rules o Rule_Set.rep) rls; |
205 val _ = trace_eq1 ctxt i "rls" rls ct |
205 val _ = trace_eq1 ctxt i "rls" rls ct |
206 val (ct', asm') = rew_once ruls [] ct Noap ruls; |
206 val (ct', asm') = rew_once ruls [] ct Noap ruls; |
207 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end |
207 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end |
208 (*--vvv and app_sub are type correct-----------------------------------------------------------*) |
|
209 and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*) |
208 and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*) |
210 let (* check a (precond, pattern) of a rev-set; stops with 1st true *) |
209 let (* check a (precond, pattern) of a rev-set; stops with 1st true *) |
211 fun chk_prepat _ _ [] _ = true |
210 fun chk_prepat _ _ [] _ = true |
212 | chk_prepat ctxt erls prepat t = |
211 | chk_prepat ctxt erls prepat t = |
213 let |
212 let |
282 in if t'' = TermC.empty then NONE else SOME (t'', asm'') |
281 in if t'' = TermC.empty then NONE else SOME (t'', asm'') |
283 end; |
282 end; |
284 |
283 |
285 (* search ct for adjacent numerals and calculate them by operator isa_fn *) |
284 (* search ct for adjacent numerals and calculate them by operator isa_fn *) |
286 fun calculate_ ctxt (isa_fn as (id, eval_fn)) t = |
285 fun calculate_ ctxt (isa_fn as (id, eval_fn)) t = |
287 case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of |
286 case Eval.adhoc_thm ctxt isa_fn t of |
288 NONE => NONE |
287 NONE => NONE |
289 | SOME (thmID, thm) => |
288 | SOME (thmID, thm) => |
290 (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of |
289 (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of |
291 SOME (rew, _) => rew |
290 SOME (rew, _) => rew |
292 | NONE => raise ERROR (msg "calculate_" ctxt id thm t) |
291 | NONE => raise ERROR (msg "calculate_" ctxt id thm t) |