Unified treatment of type error msgs.
authornipkow
Fri Oct 09 15:28:04 1998 +0200 (1998-10-09)
changeset 5635b7d6b7f66131
parent 5634 7f61a83d4a01
child 5636 dd8f30780fa9
Unified treatment of type error msgs.
src/Pure/sign.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/sign.ML	Fri Oct 09 14:36:48 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Oct 09 15:28:04 1998 +0200
     1.3 @@ -602,15 +602,7 @@
     1.4          val xs = map Free bs;		(*we do not rename here*)
     1.5          val t' = subst_bounds (xs, t);
     1.6          val u' = subst_bounds (xs, u);
     1.7 -        val text = cat_lines
     1.8 -         ["Type error in application: " ^ why,
     1.9 -          "",
    1.10 -          Pretty.string_of
    1.11 -           (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
    1.12 -                          Pretty.str " ::", Pretty.brk 1, prT T]),
    1.13 -          Pretty.string_of
    1.14 -           (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.15 -                          Pretty.str " ::", Pretty.brk 1, prT U]), ""];
    1.16 +        val text = cat_lines(TypeInfer.appl_error prt prT why t' T u' U);
    1.17        in raise TYPE (text, [T, U], [t', u']) end;
    1.18  
    1.19      fun typ_of (_, Const (_, T)) = T
     2.1 --- a/src/Pure/type_infer.ML	Fri Oct 09 14:36:48 1998 +0200
     2.2 +++ b/src/Pure/type_infer.ML	Fri Oct 09 15:28:04 1998 +0200
     2.3 @@ -11,6 +11,8 @@
     2.4      -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
     2.5      -> string list -> bool -> (indexname -> bool) -> term list -> typ list
     2.6      -> term list * typ list * (indexname * typ) list
     2.7 +  val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T)
     2.8 +    -> string -> term -> typ -> term -> typ -> string list
     2.9  end;
    2.10  
    2.11  structure TypeInfer: TYPE_INFER =
    2.12 @@ -295,6 +297,17 @@
    2.13  
    2.14  (** type inference **)
    2.15  
    2.16 +fun appl_error prt prT why t T u U =
    2.17 +  ["Type error in application: " ^ why,
    2.18 +   "",
    2.19 +   Pretty.string_of
    2.20 +    (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t,
    2.21 +                   Pretty.str " ::", Pretty.brk 1, prT T]),
    2.22 +   Pretty.string_of
    2.23 +     (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u,
    2.24 +                    Pretty.str " ::", Pretty.brk 1, prT U]),
    2.25 +   ""];
    2.26 +
    2.27  (* infer *)                                     (*DESTRUCTIVE*)
    2.28  
    2.29  fun infer prt prT classrel arities =
    2.30 @@ -304,8 +317,6 @@
    2.31      fun unif_failed msg =
    2.32        "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
    2.33  
    2.34 -    val str_of = Pretty.string_of;
    2.35 -
    2.36      fun prep_output bs ts Ts =
    2.37        let
    2.38          val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
    2.39 @@ -325,14 +336,8 @@
    2.40            (case T' of
    2.41              Type ("fun", _) => "Incompatible operand type."
    2.42            | _ => "Operator not of function type.");
    2.43 -        val text = cat_lines
    2.44 -         [unif_failed msg,
    2.45 -          "Type error in application: " ^ why,
    2.46 -          "",
    2.47 -          str_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
    2.48 -            Pretty.str " ::", Pretty.brk 1, prT T']),
    2.49 -          str_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    2.50 -            Pretty.str " ::", Pretty.brk 1, prT U']), ""];
    2.51 +        val text = unif_failed msg ^
    2.52 +                   cat_lines (appl_error prt prT why t' T' u' U');
    2.53        in raise TYPE (text, [T', U'], [t', u']) end;
    2.54  
    2.55      fun err_constraint msg bs t T U =
    2.56 @@ -340,11 +345,12 @@
    2.57          val ([t'], [T', U']) = prep_output bs [t] [T, U];
    2.58          val text = cat_lines
    2.59           [unif_failed msg,
    2.60 -          "Cannot meet type constraint:",
    2.61 -          "",
    2.62 -          str_of (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
    2.63 -            Pretty.str " ::", Pretty.brk 1, prT T']),
    2.64 -          str_of (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
    2.65 +          "Cannot meet type constraint:", "",
    2.66 +          Pretty.string_of
    2.67 +           (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
    2.68 +                          Pretty.str " ::", Pretty.brk 1, prT T']),
    2.69 +          Pretty.string_of
    2.70 +           (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
    2.71        in raise TYPE (text, [T', U'], [t']) end;
    2.72  
    2.73