--- a/src/Pure/Isar/class.ML Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Pure/Isar/class.ML Mon Apr 18 12:04:21 2011 +0200
@@ -450,15 +450,16 @@
(((primary_constraints, []), (((improve, subst), false), unchecks)), false))
end;
-fun resort_terms pp algebra consts constraints ts =
+fun resort_terms ctxt algebra consts constraints ts =
let
- fun matchings (Const (c_ty as (c, _))) = (case constraints c
- of NONE => I
- | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
- (Consts.typargs consts c_ty) sorts)
- | matchings _ = I
+ fun matchings (Const (c_ty as (c, _))) =
+ (case constraints c of
+ NONE => I
+ | SOME sorts =>
+ fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
+ | matchings _ = I;
val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
- handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
+ handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
val inst = map_type_tvar
(fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
@@ -535,7 +536,7 @@
val improve_constraints = AList.lookup (op =)
(map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
fun resort_check ts ctxt =
- (case resort_terms (Context.pretty ctxt) algebra consts improve_constraints ts of
+ (case resort_terms ctxt algebra consts improve_constraints ts of
NONE => NONE
| SOME ts' => SOME (ts', ctxt));
val lookup_inst_param = AxClass.lookup_inst_param consts params;
@@ -560,7 +561,8 @@
notes = Generic_Target.notes
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+ (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+ Generic_Target.theory_abbrev prmode ((b, mx), t)),
declaration = K Generic_Target.theory_declaration,
syntax_declaration = K Generic_Target.theory_declaration,
pretty = pretty,
--- a/src/Pure/sorts.ML Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Pure/sorts.ML Mon Apr 18 12:04:21 2011 +0200
@@ -48,7 +48,7 @@
val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
-> algebra -> (sort -> sort) * algebra
type class_error
- val class_error: Context.pretty -> class_error -> string
+ val class_error: Proof.context -> class_error -> string
exception CLASS_ERROR of class_error
val mg_domain: algebra -> string -> sort -> sort list (*exception CLASS_ERROR*)
val meet_sort: algebra -> typ * sort
@@ -335,14 +335,13 @@
No_Arity of string * class |
No_Subsort of sort * sort;
-fun class_error pp (No_Classrel (c1, c2)) =
- "No class relation " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2]
- | class_error pp (No_Arity (a, c)) =
- "No type arity " ^ Syntax.string_of_arity (Syntax.init_pretty pp) (a, [], [c])
- | class_error pp (No_Subsort (S1, S2)) =
+fun class_error ctxt (No_Classrel (c1, c2)) =
+ "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
+ | class_error ctxt (No_Arity (a, c)) =
+ "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
+ | class_error ctxt (No_Subsort (S1, S2)) =
"Cannot derive subsort relation " ^
- Syntax.string_of_sort (Syntax.init_pretty pp) S1 ^ " < " ^
- Syntax.string_of_sort (Syntax.init_pretty pp) S2;
+ Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
exception CLASS_ERROR of class_error;
--- a/src/Pure/type.ML Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Pure/type.ML Mon Apr 18 12:04:21 2011 +0200
@@ -310,7 +310,7 @@
fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
| arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
- handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+ handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
--- a/src/Tools/Code/code_thingol.ML Mon Apr 18 11:44:39 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Apr 18 12:04:21 2011 +0200
@@ -574,18 +574,25 @@
fun translation_error thy permissive some_thm msg sub_msg =
if permissive
then raise PERMISSIVE ()
- else let
- val err_thm = case some_thm
- of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
- | NONE => "";
- in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+ else
+ let
+ val err_thm =
+ (case some_thm of
+ SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
+ | NONE => "");
+ in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
fun not_wellsorted thy permissive some_thm ty sort e =
let
- val err_class = Sorts.class_error (Context.pretty_global thy) e;
- val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
- ^ Syntax.string_of_sort_global thy sort;
- in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
+ val ctxt = Syntax.init_pretty_global thy;
+ val err_class = Sorts.class_error ctxt e;
+ val err_typ =
+ "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+ Syntax.string_of_sort_global thy sort;
+ in
+ translation_error thy permissive some_thm "Wellsortedness error"
+ (err_typ ^ "\n" ^ err_class)
+ end;
(* translation *)