certify_term: type_check replaces Term.type_of, providing sensible
authorwenzelm
Mon May 25 21:16:03 1998 +0200 (1998-05-25)
changeset 496127f559b54c57
parent 4960 e07823c1ebff
child 4962 e9217cb15b42
certify_term: type_check replaces Term.type_of, providing sensible
error messages;
eliminated mapfilt_atoms (use Term.foldl_aterms);
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon May 25 21:14:00 1998 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon May 25 21:16:03 1998 +0200
     1.3 @@ -528,8 +528,13 @@
     1.4  
     1.5  (** certify types and terms **)   (*exception TYPE*)
     1.6  
     1.7 +(* certify_typ *)
     1.8 +
     1.9  val certify_typ = Type.cert_typ o tsig_of;
    1.10  
    1.11 +
    1.12 +(* certify_term *)
    1.13 +
    1.14  (*check for duplicate TVars with distinct sorts*)
    1.15  fun nodup_TVars (tvars, T) =
    1.16    (case T of
    1.17 @@ -569,10 +574,43 @@
    1.18            end);
    1.19    in nodups [] [] tm; () end;
    1.20  
    1.21 +(*compute and check type of the term*)
    1.22 +fun type_check sg tm =
    1.23 +  let
    1.24 +    val prt =
    1.25 +      setmp Syntax.show_brackets true
    1.26 +        (setmp long_names true (pretty_term sg));
    1.27 +    val prT = setmp long_names true (pretty_typ sg);
    1.28  
    1.29 -fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
    1.30 -  | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
    1.31 -  | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
    1.32 +    fun err_appl why bs t T u U =
    1.33 +      let
    1.34 +        val xs = map Free bs;		(*we do not rename here*)
    1.35 +        val t' = subst_bounds (xs, t);
    1.36 +        val u' = subst_bounds (xs, u);
    1.37 +        val text = cat_lines
    1.38 +         ["Type error in application: " ^ why,
    1.39 +          "",
    1.40 +          Pretty.string_of (Pretty.block [Pretty.str "Operator:", Pretty.brk 2, prt t',
    1.41 +            Pretty.str " :: ", prT T]),
    1.42 +          Pretty.string_of (Pretty.block [Pretty.str "Operand:", Pretty.brk 3, prt u',
    1.43 +            Pretty.str " :: ", prT U]), ""];
    1.44 +      in raise TYPE (text, [T, U], [t', u']) end;
    1.45 +
    1.46 +    fun typ_of (_, Const (_, T)) = T
    1.47 +      | typ_of (_, Free  (_, T)) = T
    1.48 +      | typ_of (_, Var (_, T)) = T
    1.49 +      | typ_of (bs, Bound i) = snd (nth_elem (i, bs) handle LIST _ =>
    1.50 +          raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
    1.51 +      | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
    1.52 +      | typ_of (bs, t $ u) =
    1.53 +          let val T = typ_of (bs, t) and U = typ_of (bs, u) in
    1.54 +            (case T of
    1.55 +              Type ("fun", [T1, T2]) =>
    1.56 +                if T1 = U then T2 else err_appl "Incompatible operand type." bs t T u U
    1.57 +            | _ => err_appl "Operator not of function type." bs t T u U)
    1.58 +          end;
    1.59 +
    1.60 +  in typ_of ([], tm) end;
    1.61  
    1.62  
    1.63  fun certify_term sg tm =
    1.64 @@ -582,15 +620,15 @@
    1.65  
    1.66      fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T);
    1.67  
    1.68 -    fun atom_err (Const (a, T)) =
    1.69 +    fun atom_err (errs, Const (a, T)) =
    1.70          (case const_type sg a of
    1.71 -          None => Some ("Undeclared constant " ^ show_const a T)
    1.72 +          None => ("Undeclared constant " ^ show_const a T) :: errs
    1.73          | Some U =>
    1.74 -            if Type.typ_instance (tsig, T, U) then None
    1.75 -            else Some ("Illegal type for constant " ^ show_const a T))
    1.76 -      | atom_err (Var ((x, i), _)) =
    1.77 -          if i < 0 then Some ("Negative index for Var " ^ quote x) else None
    1.78 -      | atom_err _ = None;
    1.79 +            if Type.typ_instance (tsig, T, U) then errs
    1.80 +            else ("Illegal type for constant " ^ show_const a T) :: errs)
    1.81 +      | atom_err (errs, Var ((x, i), _)) =
    1.82 +          if i < 0 then ("Negative index for Var " ^ quote x) :: errs else errs
    1.83 +      | atom_err (errs, _) = errs;
    1.84  
    1.85      val norm_tm =
    1.86        (case it_term_types (Type.typ_errors tsig) (tm, []) of
    1.87 @@ -598,8 +636,8 @@
    1.88        | errs => raise TYPE (cat_lines errs, [], [tm]));
    1.89      val _ = nodup_Vars norm_tm;
    1.90    in
    1.91 -    (case mapfilt_atoms atom_err norm_tm of
    1.92 -      [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
    1.93 +    (case foldl_aterms atom_err ([], norm_tm) of
    1.94 +      [] => (norm_tm, type_check sg norm_tm, maxidx_of_term norm_tm)
    1.95      | errs => raise TYPE (cat_lines errs, [], [norm_tm]))
    1.96    end;
    1.97