src/Pure/type_infer.ML
changeset 39289 92b50c8bb67b
parent 39288 f1ae2493d93f
child 39290 44e4d8dfd6bf
     1.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 19:04:02 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 19:55:45 2010 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4    val paramify_vars: typ -> typ
     1.5    val paramify_dummies: typ -> int -> typ * int
     1.6    val fixate_params: Name.context -> term list -> term list
     1.7 -  val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
     1.8    val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     1.9      (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
    1.10      term list -> term list
    1.11 @@ -318,29 +317,12 @@
    1.12  
    1.13  (** type inference **)
    1.14  
    1.15 -(* appl_error *)
    1.16 -
    1.17 -fun appl_error pp why t T u U =
    1.18 - ["Type error in application: " ^ why,
    1.19 -  "",
    1.20 -  Pretty.string_of (Pretty.block
    1.21 -    [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
    1.22 -      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
    1.23 -  Pretty.string_of (Pretty.block
    1.24 -    [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
    1.25 -      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
    1.26 -  ""];
    1.27 -
    1.28 -
    1.29  (* infer *)
    1.30  
    1.31  fun infer pp tsig =
    1.32    let
    1.33      (* errors *)
    1.34  
    1.35 -    fun unif_failed msg =
    1.36 -      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
    1.37 -
    1.38      fun prep_output tye bs ts Ts =
    1.39        let
    1.40          val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
    1.41 @@ -353,27 +335,21 @@
    1.42      fun err_loose i =
    1.43        raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
    1.44  
    1.45 +    fun unif_failed msg =
    1.46 +      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
    1.47 +
    1.48      fun err_appl msg tye bs t T u U =
    1.49        let
    1.50          val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
    1.51 -        val why =
    1.52 -          (case T' of
    1.53 -            Type ("fun", _) => "Incompatible operand type"
    1.54 -          | _ => "Operator not of function type");
    1.55 -        val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
    1.56 +        val text = unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n";
    1.57        in raise TYPE (text, [T', U'], [t', u']) end;
    1.58  
    1.59      fun err_constraint msg tye bs t T U =
    1.60        let
    1.61          val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
    1.62 -        val text = cat_lines
    1.63 -         [unif_failed msg,
    1.64 -          "Cannot meet type constraint:", "",
    1.65 -          Pretty.string_of (Pretty.block
    1.66 -           [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
    1.67 -            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
    1.68 -          Pretty.string_of (Pretty.block
    1.69 -           [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
    1.70 +        val text =
    1.71 +          unif_failed msg ^
    1.72 +            Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n";
    1.73        in raise TYPE (text, [T', U'], [t']) end;
    1.74  
    1.75