--- a/src/HOL/Tools/case_translation.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML Wed Jul 17 21:48:21 2013 +0200
@@ -366,7 +366,12 @@
fun make_case ctxt config used x clauses =
let
fun string_of_clause (pat, rhs) =
- Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
+ (case try (fn () => (* FIXME may crash!? *)
+ Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs)) ()
+ of
+ SOME s => s
+ | NONE => Markup.markup Markup.intensify "<malformed>");
+
val _ = map (no_repeat_vars ctxt o fst) clauses;
val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
val rangeT =
@@ -384,9 +389,11 @@
(case subtract (op =) tags (map (snd o snd) rows) of
[] => ()
| is =>
- (case config of Error => case_error | Warning => warning | Quiet => fn _ => ())
- ("The following clauses are redundant (covered by preceding clauses):\n" ^
- cat_lines (map (string_of_clause o nth clauses) is)));
+ if config = Quiet then ()
+ else
+ (if config = Error then case_error else warning (*FIXME lack of syntactic context!?*))
+ ("The following clauses are redundant (covered by preceding clauses):\n" ^
+ cat_lines (map (string_of_clause o nth clauses) is)));
in
case_tm
end;
--- a/src/Pure/Isar/attrib.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Jul 17 21:48:21 2013 +0200
@@ -252,8 +252,6 @@
local
-val strict_eq_thm = op = o pairself Thm.rep_thm;
-
fun apply_att src (context, th) =
let
val src1 = Args.assignable src;
@@ -275,7 +273,7 @@
(case decls of
[] => [(th, [src'])]
| (th2, srcs2) :: rest =>
- if strict_eq_thm (th, th2)
+ if Thm.eq_thm_strict (th, th2)
then ((th2, src' :: srcs2) :: rest)
else (th, [src']) :: (th2, srcs2) :: rest);
in ((th, NONE), (decls', context')) end
@@ -308,7 +306,7 @@
|>> flat;
val decls' = rev (map (apsnd rev) decls);
val facts' =
- if eq_list (eq_fst strict_eq_thm) (decls', fact') then
+ if eq_list (eq_fst Thm.eq_thm_strict) (decls', fact') then
[((b, []), map2 (fn (th, atts1) => fn (_, atts2) => (th, atts1 @ atts2)) decls' fact')]
else if null decls' then [((b, []), fact')]
else [(empty_binding, decls'), ((b, []), fact')];
--- a/src/Pure/Isar/runtime.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/Isar/runtime.ML Wed Jul 17 21:48:21 2013 +0200
@@ -50,8 +50,15 @@
local
-fun if_context NONE _ _ = []
- | if_context (SOME ctxt) f xs = map (f ctxt) xs;
+fun robust f x =
+ (case try f x of
+ SOME s => s
+ | NONE => Markup.markup Markup.intensify "<malformed>");
+
+fun robust2 f x y = robust (fn () => f x y) ();
+
+fun robust_context NONE _ _ = []
+ | robust_context (SOME ctxt) f xs = map (robust2 f ctxt) xs;
fun identify exn =
let
@@ -96,22 +103,22 @@
| ERROR msg => msg
| Fail msg => raised exn "Fail" [msg]
| THEORY (msg, thys) =>
- raised exn "THEORY" (msg :: map Context.str_of_thy thys)
+ raised exn "THEORY" (msg :: map (robust Context.str_of_thy) thys)
| Ast.AST (msg, asts) =>
- raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
+ raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
| TYPE (msg, Ts, ts) =>
raised exn "TYPE" (msg ::
- (if_context context Syntax.string_of_typ Ts @
- if_context context Syntax.string_of_term ts))
+ (robust_context context Syntax.string_of_typ Ts @
+ robust_context context Syntax.string_of_term ts))
| TERM (msg, ts) =>
- raised exn "TERM" (msg :: if_context context Syntax.string_of_term ts)
+ raised exn "TERM" (msg :: robust_context context Syntax.string_of_term ts)
| CTERM (msg, cts) =>
raised exn "CTERM"
- (msg :: if_context context Syntax.string_of_term (map term_of cts))
+ (msg :: robust_context context Syntax.string_of_term (map term_of cts))
| THM (msg, i, thms) =>
raised exn ("THM " ^ string_of_int i)
- (msg :: if_context context Display.string_of_thm thms)
- | _ => raised exn (Pretty.string_of (pretty_exn exn)) []);
+ (msg :: robust_context context Display.string_of_thm thms)
+ | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
in [((i, msg), id)] end)
and sorted_msgs context exn =
sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
--- a/src/Pure/Syntax/type_annotation.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/Syntax/type_annotation.ML Wed Jul 17 21:48:21 2013 +0200
@@ -51,12 +51,12 @@
fun fastype_of Ts (t $ u) =
(case dest_fun false (fastype_of Ts t) of
SOME T => T
- | NONE => raise TERM ("fasfastype_of: expected function type", [t $ u]))
+ | NONE => raise TERM ("fastype_of: expected function type", [t $ u]))
| fastype_of _ (Const (_, T)) = T
| fastype_of _ (Free (_, T)) = T
| fastype_of _ (Var (_, T)) = T
| fastype_of Ts (Bound i) =
- (nth Ts i handle General.Subscript => raise TERM ("fasfastype_of: Bound", [Bound i]))
+ (nth Ts i handle General.Subscript => raise TERM ("fastype_of: Bound", [Bound i]))
| fastype_of Ts (Abs (_, T, u)) = T --> fastype_of (T :: Ts) u;
end;
--- a/src/Pure/System/command_line.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/System/command_line.ML Wed Jul 17 21:48:21 2013 +0200
@@ -17,7 +17,11 @@
uninterruptible (fn restore_attributes => fn () =>
let val rc =
restore_attributes body () handle exn =>
- (Output.error_msg (ML_Compiler.exn_message exn); if Exn.is_interrupt exn then 130 else 1);
+ let
+ val _ =
+ Output.error_msg (ML_Compiler.exn_message exn)
+ handle _ => Output.error_msg "Exception raised, but failed to print details!";
+ in if Exn.is_interrupt exn then 130 else 1 end;
in if rc = 0 then () else exit rc end) ();
fun tool0 body = tool (fn () => (body (); 0));
--- a/src/Pure/context.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/context.ML Wed Jul 17 21:48:21 2013 +0200
@@ -495,7 +495,7 @@
fun raw_transfer thy' (Proof.Context (data, thy_ref)) =
let
val thy = deref thy_ref;
- val _ = subthy (thy, thy') orelse error "transfer proof context: not a super theory";
+ val _ = subthy (thy, thy') orelse error "Cannot transfer proof context: not a super theory";
val _ = check_thy thy;
val data' = init_new_data data thy';
val thy_ref' = check_thy thy';
@@ -518,9 +518,9 @@
in k end;
fun get k dest prf =
- dest (case Datatab.lookup (data_of_proof prf) k of
+ (case Datatab.lookup (data_of_proof prf) k of
SOME x => x
- | NONE => invoke_init k (Proof_Context.theory_of prf)); (*adhoc value*)
+ | NONE => invoke_init k (Proof_Context.theory_of prf)) |> dest; (*adhoc value for old theories*)
fun put k mk x = map_prf (Datatab.update (k, mk x));
--- a/src/Pure/more_thm.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Pure/more_thm.ML Wed Jul 17 21:48:21 2013 +0200
@@ -39,6 +39,7 @@
val eq_thm: thm * thm -> bool
val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
+ val eq_thm_strict: thm * thm -> bool
val equiv_thm: thm * thm -> bool
val class_triv: theory -> class -> thm
val of_sort: ctyp * sort -> thm list
@@ -192,6 +193,11 @@
val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
+fun eq_thm_strict ths =
+ eq_thm_thy ths andalso eq_thm ths andalso
+ let val (rep1, rep2) = pairself Thm.rep_thm ths
+ in #maxidx rep1 = #maxidx rep2 andalso #tags rep1 = #tags rep2 end;
+
(* pattern equivalence *)
--- a/src/Tools/adhoc_overloading.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML Wed Jul 17 21:48:21 2013 +0200
@@ -32,10 +32,18 @@
fun not_overloaded_error oconst =
error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
-fun unresolved_overloading_error ctxt (c, T) t reason =
- error ("Unresolved overloading of " ^ quote c ^ " :: " ^
- quote (Syntax.string_of_typ ctxt T) ^ " in " ^
- quote (Syntax.string_of_term ctxt t) ^ " (" ^ reason ^ ")");
+fun unresolved_overloading_error ctxt (c, T) t instances =
+ let val ctxt' = Config.put show_variants true ctxt
+ in
+ cat_lines (
+ "Unresolved overloading of constant" ::
+ quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) ::
+ "in term " ::
+ quote (Syntax.string_of_term ctxt' t) ::
+ (if null instances then "no instances" else "multiple instances:") ::
+ map (Syntax.string_of_term ctxt') instances)
+ |> error
+ end;
(* generic data *)
@@ -137,10 +145,13 @@
handle Type.TUNIFY => NONE
end;
+fun get_instances ctxt (c, T) =
+ Same.function (get_variants ctxt) c
+ |> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T);
+
fun insert_variants_same ctxt t (Const (c, T)) =
- (case map_filter (unifiable_with (Proof_Context.theory_of ctxt) T)
- (Same.function (get_variants ctxt) c) of
- [] => unresolved_overloading_error ctxt (c, T) t "no instances"
+ (case get_instances ctxt (c, T) of
+ [] => unresolved_overloading_error ctxt (c, T) t []
| [variant] => variant
| _ => raise Same.SAME)
| insert_variants_same _ _ _ = raise Same.SAME;
@@ -173,7 +184,7 @@
fun check_unresolved t =
(case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of
[] => ()
- | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t "multiple instances");
+ | ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_instances ctxt (c, T)));
val _ = map check_unresolved ts;
in NONE end;
--- a/src/Tools/induct.ML Wed Jul 17 13:34:21 2013 +0200
+++ b/src/Tools/induct.ML Wed Jul 17 21:48:21 2013 +0200
@@ -162,8 +162,7 @@
| SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
val rearrange_eqs_simproc =
- Simplifier.simproc_global
- (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"]
+ Simplifier.simproc_global Pure.thy "rearrange_eqs" ["all t"]
(fn ctxt => fn t => mk_swap_rrule ctxt (cterm_of (Proof_Context.theory_of ctxt) t));