exception SIMPROC_FAIL: solid error reporting of simprocs;
authorwenzelm
Thu Aug 08 23:51:24 2002 +0200 (2002-08-08)
changeset 1348654464ea94d6f
parent 13485 acf39e924091
child 13487 1291c6375c29
exception SIMPROC_FAIL: solid error reporting of simprocs;
src/Pure/Isar/toplevel.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 08 23:50:23 2002 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 08 23:51:24 2002 +0200
     1.3 @@ -383,6 +383,8 @@
     1.4    | exn_message (ProofContext.CONTEXT (msg, _)) = msg
     1.5    | exn_message (Proof.STATE (msg, _)) = msg
     1.6    | exn_message (ProofHistory.FAIL msg) = msg
     1.7 +  | exn_message (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
     1.8 +      fail_message "simproc" ((name, Position.none), exn)
     1.9    | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info
    1.10    | exn_message (Method.METHOD_FAIL info) = fail_message "method" info
    1.11    | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info
     2.1 --- a/src/Pure/meta_simplifier.ML	Thu Aug 08 23:50:23 2002 +0200
     2.2 +++ b/src/Pure/meta_simplifier.ML	Thu Aug 08 23:51:24 2002 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4  sig
     2.5    include BASIC_META_SIMPLIFIER
     2.6    exception SIMPLIFIER of string * thm
     2.7 +  exception SIMPROC_FAIL of string * exn
     2.8    type meta_simpset
     2.9    val dest_mss          : meta_simpset ->
    2.10      {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    2.11 @@ -63,6 +64,7 @@
    2.12  (** diagnostics **)
    2.13  
    2.14  exception SIMPLIFIER of string * thm;
    2.15 +exception SIMPROC_FAIL of string * exn;
    2.16  
    2.17  val simp_depth = ref 0;
    2.18  
    2.19 @@ -651,13 +653,14 @@
    2.20        | proc_rews ({name, proc, lhs, ...} :: ps) =
    2.21            if Pattern.matches tsigt (term_of lhs, term_of t) then
    2.22              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
    2.23 -             case try (fn () => proc signt prems eta_t) () of
    2.24 -               None => (debug true "EXCEPTION in simproc"; proc_rews ps)
    2.25 -             | Some None => (debug false "FAILED"; proc_rews ps)
    2.26 -             | Some (Some raw_thm) =>
    2.27 +             case transform_failure (curry SIMPROC_FAIL name)
    2.28 +                 (fn () => proc signt prems eta_t) () of
    2.29 +               None => (debug false "FAILED"; proc_rews ps)
    2.30 +             | Some raw_thm =>
    2.31                   (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
    2.32                    (case rews (mk_procrule raw_thm) of
    2.33 -                    None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
    2.34 +                    None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^
    2.35 +                      " -- does not match") t; proc_rews ps)
    2.36                    | some => some)))
    2.37            else proc_rews ps;
    2.38    in case eta_t of