X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/blobdiff_plain/8c57a89d75cc1d4fd050bd3767f9c881b1766c4a..e1b99e23f8d30efc7842ee006e0ff3ef0347b7df:/src/tycheck.sml

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 007a0fe..6f62a6c 100644
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -1,5 +1,5 @@
 (* HCoop Domtool (http://hcoop.sourceforge.net/)
- * Copyright (c) 2006, Adam Chlipala
+ * Copyright (c) 2006-2007, Adam Chlipala
  *
  * This program is free software; you can redistribute it and/or
  * modify it under the terms of the GNU General Public License
@@ -103,61 +103,6 @@ fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
 
       | _ => false
 
-datatype unification_error =
-	 UnifyPred of pred * pred
-       | UnifyTyp of typ * typ
-       | UnifyOccurs of string * typ
-
-exception Unify of unification_error
-
-datatype type_error =
-	 WrongType of string * exp * typ * typ * unification_error option
-       | WrongForm of string * string * exp * typ * unification_error option
-       | UnboundVariable of string
-       | WrongPred of string * pred * pred
-
-fun describe_unification_error t ue =
-    case ue of
-	UnifyPred (p1, p2) =>
-	(print "Reason: Incompatible contexts.\n";
-	 preface ("Have:", p_pred p1);
-	 preface ("Need:", p_pred p2))
-      | UnifyTyp (t1, t2) =>
-	if eqTy (t, t1) then
-	    ()
-	else
-	    (print "Reason: Incompatible types.\n";
-	     preface ("Have:", p_typ t1);
-	     preface ("Need:", p_typ t2))
-      | UnifyOccurs (name, t') =>
-	if eqTy (t, t') then
-	    ()
-	else
-	    (print "Reason: Occurs check failed for ";
-	     print name;
-	     print " in:\n";
-	     printd (p_typ t))
-
-fun describe_type_error loc te =
-    case te of
-	WrongType (place, e, t1, t2, ueo) =>
-	(ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
-	 preface (" Expression:", p_exp e);
-	 preface ("Actual type:", p_typ t1);
-	 preface ("Needed type:", p_typ t2);
-	 Option.app (describe_unification_error t1) ueo)
-      |	WrongForm (place, form, e, t, ueo) =>
-	(ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
-	 preface ("Expression:", p_exp e);
-	 preface ("      Type:", p_typ t);
-	 Option.app (describe_unification_error t) ueo)
-      | UnboundVariable name =>
-	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
-      |	WrongPred (place, p1, p2) =>
-	(ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
-	 preface ("Have:", p_pred p1);
-	 preface ("Need:", p_pred p2))
-
 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
     case (p1, p2) of
 	(_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
@@ -359,7 +304,7 @@ fun envVarSetFrom v (e, _) =
 
 fun checkExp G (eAll as (e, loc)) =
     let
-	val dte = describe_type_error loc
+	val dte = Describe.describe_type_error loc
     in
 	case e of
 	    EInt _ => (TBase "int", loc)
@@ -730,12 +675,12 @@ fun checkDecl G (d, _, loc) =
 	in
 	    hasTyp (e, t, to)
 	    handle Unify ue =>
-		   describe_type_error loc
-				       (WrongType ("Bound value",
-						   e,
-						   t,
-						   to,
-						   SOME ue));
+		   Describe.describe_type_error loc
+						(WrongType ("Bound value",
+							    e,
+							    t,
+							    to,
+							    SOME ue));
 	    bindVal G (name, to, SOME e)
 	end
       | DContext name => bindContext G name