tuned messages;
authorwenzelm
Sun Sep 12 16:06:03 2010 +0200 (2010-09-12)
changeset 392861f8131a7bcb9
parent 39285 85728a4b5620
child 39287 d30be6791038
tuned messages;
tuned comments;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Fri Sep 10 23:11:58 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Sun Sep 12 16:06:03 2010 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  val constrain = Syntax.type_constraint;
     1.5  
     1.6  
     1.7 -(* user parameters *)
     1.8 +(* type inference parameters -- may get instantiated *)
     1.9  
    1.10  fun is_param (x, _: int) = String.isPrefix "?" x;
    1.11  fun param i (x, S) = TVar (("?" ^ x, i), S);
    1.12 @@ -73,7 +73,6 @@
    1.13  
    1.14  (** pretyps and preterms **)
    1.15  
    1.16 -(*parameters may get instantiated, anything else is rigid*)
    1.17  datatype pretyp =
    1.18    PType of string * pretyp list |
    1.19    PTFree of string * sort |
    1.20 @@ -168,7 +167,7 @@
    1.21              SOME U =>
    1.22                let val (pU, idx') = polyT_of U idx
    1.23                in constraint T (PConst (c, pU)) (ps, idx') end
    1.24 -          | NONE => raise TYPE ("No such constant: " ^ quote c, [], []))
    1.25 +          | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []))
    1.26        | pre_of (Var (xi, Type ("_polymorphic_", [T]))) (ps, idx) =
    1.27            let val (pT, idx') = polyT_of T idx
    1.28            in (PVar (xi, pT), (ps, idx')) end
    1.29 @@ -258,7 +257,6 @@
    1.30  
    1.31  fun unify pp tsig =
    1.32    let
    1.33 -
    1.34      (* adjust sorts of parameters *)
    1.35  
    1.36      fun not_of_sort x S' S =
    1.37 @@ -304,13 +302,17 @@
    1.38  
    1.39      (* unification *)
    1.40  
    1.41 +    fun show_tycon (a, Ts) =
    1.42 +      quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT)));
    1.43 +
    1.44      fun unif (T1, T2) (tye_idx as (tye, idx)) =
    1.45        (case (deref tye T1, deref tye T2) of
    1.46          (Param (i, S), T) => assign i T S tye_idx
    1.47        | (T, Param (i, S)) => assign i T S tye_idx
    1.48        | (PType (a, Ts), PType (b, Us)) =>
    1.49            if a <> b then
    1.50 -            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye)
    1.51 +            raise NO_UNIFIER
    1.52 +              ("Clash of types " ^ show_tycon (a, Ts) ^ " and " ^ show_tycon (b, Us), tye)
    1.53            else fold unif (Ts ~~ Us) tye_idx
    1.54        | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye));
    1.55