author wenzelm Mon Apr 18 12:04:21 2011 +0200 (2011-04-18) changeset 42385 b46b47775cbe parent 42384 6b8e28b52ae3 child 42386 50ea65e84d98
simplified Sorts.class_error: plain Proof.context;
tuned;
 src/Pure/Isar/class.ML file | annotate | diff | revisions src/Pure/sorts.ML file | annotate | diff | revisions src/Pure/type.ML file | annotate | diff | revisions src/Tools/Code/code_thingol.ML file | annotate | diff | revisions
```     1.1 --- a/src/Pure/Isar/class.ML	Mon Apr 18 11:44:39 2011 +0200
1.2 +++ b/src/Pure/Isar/class.ML	Mon Apr 18 12:04:21 2011 +0200
1.3 @@ -450,15 +450,16 @@
1.4              (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
1.5    end;
1.6
1.7 -fun resort_terms pp algebra consts constraints ts =
1.8 +fun resort_terms ctxt algebra consts constraints ts =
1.9    let
1.10 -    fun matchings (Const (c_ty as (c, _))) = (case constraints c
1.11 -         of NONE => I
1.12 -          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
1.13 -              (Consts.typargs consts c_ty) sorts)
1.14 -      | matchings _ = I
1.15 +    fun matchings (Const (c_ty as (c, _))) =
1.16 +          (case constraints c of
1.17 +            NONE => I
1.18 +          | SOME sorts =>
1.19 +              fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
1.20 +      | matchings _ = I;
1.21      val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
1.22 -      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
1.23 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
1.24      val inst = map_type_tvar
1.25        (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
1.26    in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
1.27 @@ -535,7 +536,7 @@
1.28      val improve_constraints = AList.lookup (op =)
1.29        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
1.30      fun resort_check ts ctxt =
1.31 -      (case resort_terms (Context.pretty ctxt) algebra consts improve_constraints ts of
1.32 +      (case resort_terms ctxt algebra consts improve_constraints ts of
1.33          NONE => NONE
1.34        | SOME ts' => SOME (ts', ctxt));
1.35      val lookup_inst_param = AxClass.lookup_inst_param consts params;
1.36 @@ -560,7 +561,8 @@
1.37          notes = Generic_Target.notes
1.38            (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
1.39          abbrev = Generic_Target.abbrev
1.40 -          (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
1.41 +          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
1.42 +            Generic_Target.theory_abbrev prmode ((b, mx), t)),
1.43          declaration = K Generic_Target.theory_declaration,
1.44          syntax_declaration = K Generic_Target.theory_declaration,
1.45          pretty = pretty,
```
```     2.1 --- a/src/Pure/sorts.ML	Mon Apr 18 11:44:39 2011 +0200
2.2 +++ b/src/Pure/sorts.ML	Mon Apr 18 12:04:21 2011 +0200
2.3 @@ -48,7 +48,7 @@
2.4    val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
2.5      -> algebra -> (sort -> sort) * algebra
2.6    type class_error
2.7 -  val class_error: Context.pretty -> class_error -> string
2.8 +  val class_error: Proof.context -> class_error -> string
2.9    exception CLASS_ERROR of class_error
2.10    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
2.11    val meet_sort: algebra -> typ * sort
2.12 @@ -335,14 +335,13 @@
2.13    No_Arity of string * class |
2.14    No_Subsort of sort * sort;
2.15
2.16 -fun class_error pp (No_Classrel (c1, c2)) =
2.17 -      "No class relation " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2]
2.18 -  | class_error pp (No_Arity (a, c)) =
2.19 -      "No type arity " ^ Syntax.string_of_arity (Syntax.init_pretty pp) (a, [], [c])
2.20 -  | class_error pp (No_Subsort (S1, S2)) =
2.21 +fun class_error ctxt (No_Classrel (c1, c2)) =
2.22 +      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
2.23 +  | class_error ctxt (No_Arity (a, c)) =
2.24 +      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
2.25 +  | class_error ctxt (No_Subsort (S1, S2)) =
2.26        "Cannot derive subsort relation " ^
2.27 -      Syntax.string_of_sort (Syntax.init_pretty pp) S1 ^ " < " ^
2.28 -      Syntax.string_of_sort (Syntax.init_pretty pp) S2;
2.29 +        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
2.30
2.31  exception CLASS_ERROR of class_error;
2.32
```
```     3.1 --- a/src/Pure/type.ML	Mon Apr 18 11:44:39 2011 +0200
3.2 +++ b/src/Pure/type.ML	Mon Apr 18 12:04:21 2011 +0200
3.3 @@ -310,7 +310,7 @@
3.4
3.5  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
3.6    | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
3.7 -      handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
3.8 +      handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
3.9
3.10
3.11
```
```     4.1 --- a/src/Tools/Code/code_thingol.ML	Mon Apr 18 11:44:39 2011 +0200
4.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 12:04:21 2011 +0200
4.3 @@ -574,18 +574,25 @@
4.4  fun translation_error thy permissive some_thm msg sub_msg =
4.5    if permissive
4.6    then raise PERMISSIVE ()
4.7 -  else let
4.8 -    val err_thm = case some_thm
4.9 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
4.10 -      | NONE => "";
4.11 -  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
4.12 +  else
4.13 +    let
4.14 +      val err_thm =
4.15 +        (case some_thm of
4.16 +          SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
4.17 +        | NONE => "");
4.18 +    in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
4.19
4.20  fun not_wellsorted thy permissive some_thm ty sort e =
4.21    let
4.22 -    val err_class = Sorts.class_error (Context.pretty_global thy) e;
4.23 -    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
4.24 -      ^ Syntax.string_of_sort_global thy sort;
4.25 -  in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
4.26 +    val ctxt = Syntax.init_pretty_global thy;
4.27 +    val err_class = Sorts.class_error ctxt e;
4.28 +    val err_typ =
4.29 +      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
4.30 +        Syntax.string_of_sort_global thy sort;
4.31 +  in
4.32 +    translation_error thy permissive some_thm "Wellsortedness error"
4.33 +      (err_typ ^ "\n" ^ err_class)
4.34 +  end;
4.35
4.36
4.37  (* translation *)
```