14 |
14 |
15 signature META_SIMPLIFIER = |
15 signature META_SIMPLIFIER = |
16 sig |
16 sig |
17 include BASIC_META_SIMPLIFIER |
17 include BASIC_META_SIMPLIFIER |
18 exception SIMPLIFIER of string * thm |
18 exception SIMPLIFIER of string * thm |
|
19 exception SIMPROC_FAIL of string * exn |
19 type meta_simpset |
20 type meta_simpset |
20 val dest_mss : meta_simpset -> |
21 val dest_mss : meta_simpset -> |
21 {simps: thm list, congs: thm list, procs: (string * cterm list) list} |
22 {simps: thm list, congs: thm list, procs: (string * cterm list) list} |
22 val empty_mss : meta_simpset |
23 val empty_mss : meta_simpset |
23 val clear_mss : meta_simpset -> meta_simpset |
24 val clear_mss : meta_simpset -> meta_simpset |
649 |
651 |
650 fun proc_rews ([]:simproc list) = None |
652 fun proc_rews ([]:simproc list) = None |
651 | proc_rews ({name, proc, lhs, ...} :: ps) = |
653 | proc_rews ({name, proc, lhs, ...} :: ps) = |
652 if Pattern.matches tsigt (term_of lhs, term_of t) then |
654 if Pattern.matches tsigt (term_of lhs, term_of t) then |
653 (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t; |
655 (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t; |
654 case try (fn () => proc signt prems eta_t) () of |
656 case transform_failure (curry SIMPROC_FAIL name) |
655 None => (debug true "EXCEPTION in simproc"; proc_rews ps) |
657 (fn () => proc signt prems eta_t) () of |
656 | Some None => (debug false "FAILED"; proc_rews ps) |
658 None => (debug false "FAILED"; proc_rews ps) |
657 | Some (Some raw_thm) => |
659 | Some raw_thm => |
658 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; |
660 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; |
659 (case rews (mk_procrule raw_thm) of |
661 (case rews (mk_procrule raw_thm) of |
660 None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps) |
662 None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^ |
|
663 " -- does not match") t; proc_rews ps) |
661 | some => some))) |
664 | some => some))) |
662 else proc_rews ps; |
665 else proc_rews ps; |
663 in case eta_t of |
666 in case eta_t of |
664 Abs _ $ _ => Some (transitive eta_thm |
667 Abs _ $ _ => Some (transitive eta_thm |
665 (beta_conversion false eta_t'), skel0) |
668 (beta_conversion false eta_t'), skel0) |