src/Pure/sign.ML
changeset 1393 73b6b003c6ca
parent 1241 bfc93c86f0a1
child 1414 036e072b215a
     1.1 --- a/src/Pure/sign.ML	Fri Dec 08 10:35:48 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Dec 08 10:36:36 1995 +0100
     1.3 @@ -40,6 +40,7 @@
     1.4      val certify_typ: sg -> typ -> typ
     1.5      val certify_term: sg -> term -> term * typ * int
     1.6      val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.7 +    val exn_type_msg: sg -> string * typ list * term list -> string
     1.8      val infer_types: sg -> (indexname -> typ option) ->
     1.9        (indexname -> sort option) -> string list -> bool
    1.10        -> term list * typ -> int * term * (indexname * typ) list
    1.11 @@ -262,26 +263,34 @@
    1.12    end;
    1.13  
    1.14  
    1.15 +(*Package error messages from type checking*)
    1.16 +fun exn_type_msg sg (msg, Ts, ts) =
    1.17 +    let val show_typ = string_of_typ sg
    1.18 +	val show_term = string_of_term sg
    1.19 +	fun term_err [] = ""
    1.20 +	  | term_err [t] = "\nInvolving this term:\n" ^ show_term t
    1.21 +	  | term_err ts =
    1.22 +	    "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.23 +    in  "\nType checking error: " ^ msg ^ "\n" ^
    1.24 +	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
    1.25 +    end; 
    1.26 +
    1.27 +
    1.28  
    1.29  (** infer_types **)         (*exception ERROR*)
    1.30  
    1.31 +(*ts is the list of alternative parses; only one is hoped to be type-correct.
    1.32 +  T is the expected type for the correct term.
    1.33 +  Other standard arguments:
    1.34 +    types is a partial map from indexnames to types (constrains Free, Var).
    1.35 +    sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
    1.36 +    used is the list of already used type variables.
    1.37 +    If freeze then internal TVars are turned into TFrees, else TVars.*)
    1.38  fun infer_types sg types sorts used freeze (ts, T) =
    1.39    let
    1.40      val Sg {tsig, ...} = sg;
    1.41 -    val show_typ = string_of_typ sg;
    1.42 -    val show_term = string_of_term sg;
    1.43  
    1.44 -    fun term_err [] = ""
    1.45 -      | term_err [t] = "\nInvolving this term:\n" ^ show_term t
    1.46 -      | term_err ts =
    1.47 -          "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.48 -
    1.49 -    fun exn_type_msg (msg, Ts, ts) =
    1.50 -	"\nType checking error: " ^ msg ^ "\n" ^
    1.51 -	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
    1.52 -
    1.53 -    val T' = certify_typ sg T
    1.54 -             handle TYPE arg => error (exn_type_msg arg);
    1.55 +    val T' = certify_typ sg T handle TYPE arg => error (exn_type_msg sg arg);
    1.56  
    1.57      val ct = const_type sg;
    1.58  
    1.59 @@ -298,7 +307,8 @@
    1.60                      | Ambigs of term list;
    1.61  
    1.62      fun process_term(res,(t,i)) =
    1.63 -       let val (u,tye) = Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    1.64 +       let val ([u],tye) = 
    1.65 +	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
    1.66         in case res of
    1.67              One(_,t0,_) => Ambigs([u,t0])
    1.68            | Errs _ => One(i,u,tye)
    1.69 @@ -314,12 +324,12 @@
    1.70              \It helps (speed!) if you disambiguate your grammar or your input."
    1.71            else ();
    1.72            res)
    1.73 -     | Errs(errs) => (warn(); error(cat_lines(map exn_type_msg errs)))
    1.74 +     | Errs(errs) => (warn(); error(cat_lines(map (exn_type_msg sg) errs)))
    1.75       | Ambigs(us) =>
    1.76           (warn();
    1.77            let val old_show_brackets = !show_brackets
    1.78                val dummy = show_brackets := true;
    1.79 -              val errs = cat_lines(map show_term us)
    1.80 +              val errs = cat_lines(map (string_of_term sg) us)
    1.81            in show_brackets := old_show_brackets;
    1.82               error("Error: More than one term is type correct:\n" ^ errs)
    1.83            end)