simplified Sorts.class_error: plain Proof.context;
authorwenzelm
Mon Apr 18 12:04:21 2011 +0200 (2011-04-18)
changeset 42385b46b47775cbe
parent 42384 6b8e28b52ae3
child 42386 50ea65e84d98
simplified Sorts.class_error: plain Proof.context;
tuned;
src/Pure/Isar/class.ML
src/Pure/sorts.ML
src/Pure/type.ML
src/Tools/Code/code_thingol.ML
     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 *)