common Type.appl_error, which also covers explicit constraints;
authorwenzelm
Sun Sep 12 19:55:45 2010 +0200 (2010-09-12)
changeset 3928992b50c8bb67b
parent 39288 f1ae2493d93f
child 39290 44e4d8dfd6bf
common Type.appl_error, which also covers explicit constraints;
src/Pure/sign.ML
src/Pure/type.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/sign.ML	Sun Sep 12 19:04:02 2010 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Sep 12 19:55:45 2010 +0200
     1.3 @@ -265,12 +265,12 @@
     1.4  
     1.5  fun type_check pp tm =
     1.6    let
     1.7 -    fun err_appl why bs t T u U =
     1.8 +    fun err_appl bs t T u U =
     1.9        let
    1.10          val xs = map Free bs;           (*we do not rename here*)
    1.11          val t' = subst_bounds (xs, t);
    1.12          val u' = subst_bounds (xs, u);
    1.13 -        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
    1.14 +        val msg = Type.appl_error pp t' T u' U;
    1.15        in raise TYPE (msg, [T, U], [t', u']) end;
    1.16  
    1.17      fun typ_of (_, Const (_, T)) = T
    1.18 @@ -283,8 +283,8 @@
    1.19            let val T = typ_of (bs, t) and U = typ_of (bs, u) in
    1.20              (case T of
    1.21                Type ("fun", [T1, T2]) =>
    1.22 -                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
    1.23 -            | _ => err_appl "Operator not of function type" bs t T u U)
    1.24 +                if T1 = U then T2 else err_appl bs t T u U
    1.25 +            | _ => err_appl bs t T u U)
    1.26            end;
    1.27    in typ_of ([], tm) end;
    1.28  
     2.1 --- a/src/Pure/type.ML	Sun Sep 12 19:04:02 2010 +0200
     2.2 +++ b/src/Pure/type.ML	Sun Sep 12 19:55:45 2010 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  sig
     2.5    (*constraints*)
     2.6    val constraint: typ -> term -> term
     2.7 +  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
     2.8    (*type signatures and certified types*)
     2.9    datatype decl =
    2.10      LogicalType of int |
    2.11 @@ -104,6 +105,28 @@
    2.12    if T = dummyT then t
    2.13    else Const ("_type_constraint_", T --> T) $ t;
    2.14  
    2.15 +fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
    2.16 +      cat_lines
    2.17 +       ["Failed to meet type constraint:", "",
    2.18 +        Pretty.string_of (Pretty.block
    2.19 +         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
    2.20 +          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
    2.21 +        Pretty.string_of (Pretty.block
    2.22 +         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
    2.23 +  | appl_error pp t T u U =
    2.24 +      cat_lines
    2.25 +       ["Type error in application: " ^
    2.26 +          (case T of
    2.27 +            Type ("fun", _) => "incompatible operand type"
    2.28 +          | _ => "operator not of function type"),
    2.29 +        "",
    2.30 +        Pretty.string_of (Pretty.block
    2.31 +          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
    2.32 +            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
    2.33 +        Pretty.string_of (Pretty.block
    2.34 +          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
    2.35 +            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
    2.36 +
    2.37  
    2.38  
    2.39  (** type signatures and certified types **)
     3.1 --- a/src/Pure/type_infer.ML	Sun Sep 12 19:04:02 2010 +0200
     3.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 19:55:45 2010 +0200
     3.3 @@ -13,7 +13,6 @@
     3.4    val paramify_vars: typ -> typ
     3.5    val paramify_dummies: typ -> int -> typ * int
     3.6    val fixate_params: Name.context -> term list -> term list
     3.7 -  val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
     3.8    val infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
     3.9      (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
    3.10      term list -> term list
    3.11 @@ -318,29 +317,12 @@
    3.12  
    3.13  (** type inference **)
    3.14  
    3.15 -(* appl_error *)
    3.16 -
    3.17 -fun appl_error pp why t T u U =
    3.18 - ["Type error in application: " ^ why,
    3.19 -  "",
    3.20 -  Pretty.string_of (Pretty.block
    3.21 -    [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
    3.22 -      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
    3.23 -  Pretty.string_of (Pretty.block
    3.24 -    [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
    3.25 -      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
    3.26 -  ""];
    3.27 -
    3.28 -
    3.29  (* infer *)
    3.30  
    3.31  fun infer pp tsig =
    3.32    let
    3.33      (* errors *)
    3.34  
    3.35 -    fun unif_failed msg =
    3.36 -      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
    3.37 -
    3.38      fun prep_output tye bs ts Ts =
    3.39        let
    3.40          val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
    3.41 @@ -353,27 +335,21 @@
    3.42      fun err_loose i =
    3.43        raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
    3.44  
    3.45 +    fun unif_failed msg =
    3.46 +      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
    3.47 +
    3.48      fun err_appl msg tye bs t T u U =
    3.49        let
    3.50          val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U];
    3.51 -        val why =
    3.52 -          (case T' of
    3.53 -            Type ("fun", _) => "Incompatible operand type"
    3.54 -          | _ => "Operator not of function type");
    3.55 -        val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
    3.56 +        val text = unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n";
    3.57        in raise TYPE (text, [T', U'], [t', u']) end;
    3.58  
    3.59      fun err_constraint msg tye bs t T U =
    3.60        let
    3.61          val ([t'], [T', U']) = prep_output tye bs [t] [T, U];
    3.62 -        val text = cat_lines
    3.63 -         [unif_failed msg,
    3.64 -          "Cannot meet type constraint:", "",
    3.65 -          Pretty.string_of (Pretty.block
    3.66 -           [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
    3.67 -            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
    3.68 -          Pretty.string_of (Pretty.block
    3.69 -           [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
    3.70 +        val text =
    3.71 +          unif_failed msg ^
    3.72 +            Type.appl_error pp (Const ("_type_constraint_", U' --> U')) (U' --> U') t' T' ^ "\n";
    3.73        in raise TYPE (text, [T', U'], [t']) end;
    3.74  
    3.75