src/Pure/type_infer.ML
changeset 2979 db6941221197
parent 2957 d35fca99b3be
child 2980 98ad57d99427
     1.1 --- a/src/Pure/type_infer.ML	Thu Apr 17 18:45:43 1997 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Thu Apr 17 18:46:58 1997 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  signature TYPE_INFER =
     1.6  sig
     1.7 -  val infer_types: (string -> typ option) -> Sorts.classrel -> Sorts.arities
     1.8 +  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
     1.9 +    -> (string -> typ option) -> Sorts.classrel -> Sorts.arities
    1.10      -> string list -> bool -> (indexname -> bool) -> term list -> typ list
    1.11      -> term list * typ list * (indexname * typ) list
    1.12  end;
    1.13 @@ -257,7 +258,7 @@
    1.14  
    1.15      fun not_in_sort x S' S =
    1.16        "Type variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not in sort " ^
    1.17 -        Sorts.str_of_sort S;
    1.18 +        Sorts.str_of_sort S ^ ".";
    1.19  
    1.20      fun meet _ [] = ()
    1.21        | meet (Link (r as (ref (Param S')))) S =
    1.22 @@ -298,9 +299,10 @@
    1.23        | unif (Link (ref T)) U = unif T U
    1.24        | unif T (Link (ref U)) = unif T U
    1.25        | unif (PType (a, Ts)) (PType (b, Us)) =
    1.26 -          if a <> b then raise NO_UNIFIER ("Clash of " ^ a ^ ", " ^ b ^ "!")
    1.27 +          if a <> b then
    1.28 +            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".")
    1.29            else seq2 unif Ts Us
    1.30 -      | unif T U = if T = U then () else raise NO_UNIFIER "Unification failed!";
    1.31 +      | unif T U = if T = U then () else raise NO_UNIFIER "";
    1.32  
    1.33    in unif end;
    1.34  
    1.35 @@ -310,26 +312,63 @@
    1.36  
    1.37  (* infer *)                                     (*DESTRUCTIVE*)
    1.38  
    1.39 -fun infer classrel arities =
    1.40 +fun infer prt prT classrel arities =
    1.41    let
    1.42 -    val unif = unify classrel arities;
    1.43 +    (* errors *)
    1.44  
    1.45 -    fun err msg1 msg2 bs ts Ts =
    1.46 +    fun unif_failed msg =
    1.47 +      "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
    1.48 +
    1.49 +    val str_of = Pretty.string_of;
    1.50 +
    1.51 +    fun prep_output bs ts Ts =
    1.52        let
    1.53          val (Ts_bTs', ts') = typs_terms_of [] PTFree "??" (Ts @ map snd bs, ts);
    1.54          val len = length Ts;
    1.55          val Ts' = take (len, Ts_bTs');
    1.56          val xs = map Free (map fst bs ~~ drop (len, Ts_bTs'));
    1.57          val ts'' = map (fn t => subst_bounds (xs, t)) ts';
    1.58 -      in
    1.59 -        raise_type (msg1 ^ " " ^ msg2) Ts' ts''
    1.60 -      end;
    1.61 +      in (ts'', Ts') end;
    1.62 +
    1.63 +    fun err_loose i =
    1.64 +      raise_type ("Loose bound variable: B." ^ string_of_int i) [] [];
    1.65 +
    1.66 +    fun err_appl msg bs t T U_to_V u U =
    1.67 +      let
    1.68 +        val ([t', u'], [T', U_to_V', U']) = prep_output bs [t, u] [T, U_to_V, U];
    1.69 +        val text = cat_lines
    1.70 +         [unif_failed msg,
    1.71 +          "Type error in application:",
    1.72 +          "",
    1.73 +          str_of (Pretty.block [Pretty.str "operator:     ", Pretty.brk 1, prt t',
    1.74 +            Pretty.str " :: ", prT T']),
    1.75 +          str_of (Pretty.block [Pretty.str "expected type:", Pretty.brk 1, prT U_to_V']),
    1.76 +          "",
    1.77 +          str_of (Pretty.block [Pretty.str "operand:      ", Pretty.brk 1, prt u',
    1.78 +            Pretty.str " :: ", prT U']), ""];
    1.79 +      in raise_type text [T', U_to_V', U'] [t', u'] end;
    1.80 +
    1.81 +    fun err_constraint msg bs t T U =
    1.82 +      let
    1.83 +        val ([t'], [T', U']) = prep_output bs [t] [T, U];
    1.84 +        val text = cat_lines
    1.85 +         [unif_failed msg,
    1.86 +          "Cannot meet type constraint:",
    1.87 +          "",
    1.88 +          str_of (Pretty.block [Pretty.str "term:          ", Pretty.brk 1, prt t',
    1.89 +            Pretty.str " :: ", prT T']),
    1.90 +          str_of (Pretty.block [Pretty.str "expected type: ", Pretty.brk 1, prT U']), ""];
    1.91 +      in raise_type text [T', U'] [t'] end;
    1.92 +
    1.93 +
    1.94 +    (* main *)
    1.95 +
    1.96 +    val unif = unify classrel arities;
    1.97  
    1.98      fun inf _ (PConst (_, T)) = T
    1.99        | inf _ (PFree (_, T)) = T
   1.100        | inf _ (PVar (_, T)) = T
   1.101 -      | inf bs (PBound i) = snd (nth_elem (i, bs)
   1.102 -          handle LIST _ => raise_type "Loose bound variable" [] [Bound i])
   1.103 +      | inf bs (PBound i) = snd (nth_elem (i, bs) handle LIST _ => err_loose i)
   1.104        | inf bs (PAbs (x, T, t)) = PType ("fun", [T, inf ((x, T) :: bs) t])
   1.105        | inf bs (PAppl (t, u)) =
   1.106            let
   1.107 @@ -338,12 +377,11 @@
   1.108              val V = mk_param [];
   1.109              val U_to_V = PType ("fun", [U, V]);
   1.110              val _ = unif U_to_V T handle NO_UNIFIER msg =>
   1.111 -              err msg "Bad function application." bs [PAppl (t, u)] [U_to_V, U];
   1.112 +              err_appl msg bs t T U_to_V u U;
   1.113            in V end
   1.114        | inf bs (Constraint (t, U)) =
   1.115            let val T = inf bs t in
   1.116 -            unif T U handle NO_UNIFIER msg =>
   1.117 -              err msg "Cannot meet type constraint." bs [t] [T, U];
   1.118 +            unif T U handle NO_UNIFIER msg => err_constraint msg bs t T U;
   1.119              T
   1.120            end;
   1.121  
   1.122 @@ -352,7 +390,7 @@
   1.123  
   1.124  (* infer_types *)
   1.125  
   1.126 -fun infer_types const_type classrel arities used freeze is_param ts Ts =
   1.127 +fun infer_types prt prT const_type classrel arities used freeze is_param ts Ts =
   1.128    let
   1.129      (*convert to preterms/typs*)
   1.130      val (Tps, Ts') = pretyps_of (K true) ([], Ts);
   1.131 @@ -360,7 +398,7 @@
   1.132  
   1.133      (*run type inference*)
   1.134      val tTs' = ListPair.map Constraint (ts', Ts');
   1.135 -    val _ = seq (fn t => (infer classrel arities t; ())) tTs';
   1.136 +    val _ = seq (fn t => (infer prt prT classrel arities t; ())) tTs';
   1.137  
   1.138      (*collect result unifier*)
   1.139      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)