src/tycheck.sml

(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006, Adam Chlipala
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
 *)

(* Domtool configuration language type checking *)

structure Tycheck :> TYCHECK = struct

open Ast Print Env

structure SM = StringMap

local
    val unifCount = ref 0
in
fun resetUnif () = unifCount := 0

fun newUnif () =
    let
	val c = !unifCount
	val name =
	    if c < 26 then
		str (chr (ord #"A" + c))
	    else
		"UNIF" ^ Int.toString (c - 26)
    in
	unifCount := c + 1;
	TUnif (name, ref NONE)
    end
end

exception UnequalDomains

fun eqRecord f (r1, r2) =
    (SM.appi (fn (k, v1) =>
		 case SM.find (r2, k) of
		     NONE => raise UnequalDomains
		   | SOME v2 =>
		     if f (v1, v2) then
			 ()
		     else
			 raise UnequalDomains) r1;
     SM.appi (fn (k, v2) =>
		 case SM.find (r1, k) of
		     NONE => raise UnequalDomains
		   | SOME v1 =>
		     if f (v1, v2) then
			 ()
		     else
			 raise UnequalDomains) r2;
     true)
    handle UnequalDomains => false

fun eqPred ((p1, _), (p2, _)) =
    case (p1, p2) of
	(CRoot, CRoot) => true
      | (CConst s1, CConst s2) => s1 = s2
      | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
      | (CNot p1, CNot p2) => eqPred (p1, p2)
      | (CAnd (p1, q1), CAnd (p2, q2)) =>
	eqPred (p1, p2) andalso eqPred (q1, q2)

      | _ => false

fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
    case (t1, t2) of
	(TBase s1, TBase s2) => s1 = s2
      | (TList t1, TList t2) => eqTy (t1, t2)
      | (TArrow (d1, r1), TArrow (d2, r2)) =>
	eqTy (d1, d2) andalso eqTy (r1, r2)

      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
	andalso eqRecord eqTy (r1, r2)

      | (TNested (p1, q1), TNested (p2, q2)) =>
	eqPred (p1, p2) andalso eqTy (q1, q2)

      | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
      | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)

      | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2

      | (TError, TError) => true

      | _ => 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 preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
					[PD.string s, PD.space 1, d]))

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)
      | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)

      | (_, CPrefix (CRoot, _)) => true
      | (CNot (CPrefix (CRoot, _), _), _) => true

      | (CRoot, CRoot) => true

      | (CConst s1, CConst s2) => s1 = s2

      | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
      | (_, CPrefix p2) => predImplies (p1All, p2)

      | (CNot p1, CNot p2) => predImplies (p2, p1)

      | _ => false

fun predSimpl (pAll as (p, loc)) =
    case p of
	CRoot => pAll
      | CConst _ => pAll
      | CPrefix p => (CPrefix (predSimpl p), loc)
      | CNot p => (CNot (predSimpl p), loc)
      | CAnd (p1, p2) =>
	let
	    val p1' = predSimpl p1
	    val p2' = predSimpl p2
	in
	    case p1' of
		(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
	      | _ => if predImplies (p2', p1') then
			 p2'
		     else if predImplies (p1', p2') then
			 p1'
		     else
			 (CAnd (p1', p2'), loc)
	end

fun subPred (p1, p2) =
    if predImplies (p1, p2) then
	()
    else
	raise (Unify (UnifyPred (p1, p2)))

fun subRecord f (r1, r2) =
    SM.appi (fn (k, v2) =>
		case SM.find (r1, k) of
		    NONE => raise UnequalDomains
		  | SOME v1 => f (v1, v2)) r2

fun occurs u (t, _) =
    case t of
	TBase _ => false
      | TList t => occurs u t
      | TArrow (d, r) => occurs u d orelse occurs u r
      | TAction (_, d, r) =>
	List.exists (occurs u) (SM.listItems d)
	orelse List.exists (occurs u) (SM.listItems r)
      | TNested (_, t) => occurs u t
      | TError => false
      | TUnif (_, ref (SOME t)) => occurs u t
      | TUnif (_, u') => u = u'

fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
    case (t1, t2) of
	(TBase s1, TBase s2) =>
	if s1 = s2 then
	    ()
	else
	    raise Unify (UnifyTyp (t1All, t2All))
      | (TList t1, TList t2) => subTyp (t1, t2)
      | (TArrow (d1, r1), TArrow (d2, r2)) =>
	(subTyp (d2, d1);
	 subTyp (r1, r2))

      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	((subPred (p2, p1);
	  subRecord subTyp (d2, d1);
	  subRecord subTyp (r1, r2);
	  subRecord subTyp (r2, r1))
	 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))

      | (TNested (d1, r1), TNested (d2, r2)) =>
	(subPred (d2, d1);
	 subTyp (r1, r2))

      | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
      | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)

      | (TUnif (_, r1), TUnif (_, r2)) =>
	if r1 = r2 then
	    ()
	else
	    r1 := SOME t2All

      | (TUnif (name, r), _) =>
	if occurs r t2All then
	    raise (Unify (UnifyOccurs (name, t2All)))
	else
	    r := SOME t2All

      | (_, TUnif (name, r)) =>
	if occurs r t1All then
	    raise (Unify (UnifyOccurs (name, t1All)))
	else
	    r := SOME t1All

      | (TError, _) => ()
      | (_, TError) => ()

      | _ => raise Unify (UnifyTyp (t1All, t2All))

fun isError t =
    case t of
	(TError, _) => true
      | _ => false

fun whnorm (tAll as (t, loc)) =
    case t of
	TUnif (_, ref (SOME tAll)) => whnorm tAll
      | _ => tAll

fun hasTyp (e, t1, t2) =
    case whnorm t2 of
	(TBase name, _) =>
	(case typeRule name of
	     NONE => subTyp (t1, t2)
	   | SOME rule =>
	     if rule e then
		 ()
	     else
		 subTyp (t1, t2))
      | _ => subTyp (t1, t2)

fun checkTyp G (tAll as (t, loc)) =
    let
	val err = ErrorMsg.error (SOME loc)
    in
	case t of
	    TBase name =>
	    if lookupType G name then
		tAll
	    else
		(err ("Unbound type name " ^ name);
		 (TError, loc))
	  | TList t => (TList (checkTyp G t), loc)
	  | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
	  | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
					   SM.map (checkTyp G) r), loc)
	  | TNested (p, t) => (TNested (p, checkTyp G t), loc)
	  | TError => raise Fail "TError in parser-generated type"
	  | TUnif _ => raise Fail "TUnif in parser-generated type"
    end

fun checkExp G (eAll as (e, loc)) =
    let
	val dte = describe_type_error loc
    in
	case e of
	    EInt _ => (TBase "int", loc)
	  | EString _ => (TBase "string", loc)
	  | EList es =>
	    let
		val t = (newUnif (), loc)
	    in
		foldl (fn (e', ret) =>
			  let
			      val t' = checkExp G e'
			  in
			      (hasTyp (eAll, t', t);
			       if isError t' then
				   (TList (TError, loc), loc)
			       else
				   ret)
			      handle Unify ue =>
				     (dte (WrongType ("List element",
						      e',
						      t',
						      t,
						      SOME ue));
				      (TError, loc))
			  end) (TList t, loc) es
	    end

	  | ELam (x, to, e) =>
	    let
		val t =
		    case to of
			NONE => (newUnif (), loc)
		      | SOME t => checkTyp G t

		val G' = bindVal G (x, t, NONE)
		val t' = checkExp G' e
	    in
		(TArrow (t, t'), loc)
	    end
	  | EVar x =>
	    (case lookupVal G x of
		 NONE => (dte (UnboundVariable x);
			  (TError, loc))
	       | SOME t => t)
	  | EApp (func, arg) =>
	    let
		val dom = (newUnif (), loc)
		val ran = (newUnif (), loc)

		val tf = checkExp G func
		val ta = checkExp G arg
	    in
		(hasTyp (func, tf, (TArrow (dom, ran), loc));
		 hasTyp (arg, ta, dom)
		 handle Unify ue =>
			dte (WrongType ("Function argument",
					arg,
					ta,
					dom,
					SOME ue));
		 ran)
		handle Unify ue =>
		       (dte (WrongForm ("Function to be applied",
					"function",
					func,
					tf,
					SOME ue));
			(TError, loc))
	    end

	  | ESet (evar, e) =>
	    let
		val t = checkExp G e
	    in
		(TAction ((CPrefix (CRoot, loc), loc),
			  SM.empty,
			  SM.insert (SM.empty, evar, t)),
		 loc)
	    end
	  | EGet (x, evar, rest) =>
	    let
		val xt = (newUnif (), loc)
		val G' = bindVal G (x, xt, NONE)

		val rt = whnorm (checkExp G' rest)
	    in
		case rt of
		    (TAction (p, d, r), _) =>
		    (case SM.find (d, evar) of
			 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
		       | SOME xt' =>
			 (subTyp (xt', xt)
				handle Unify ue =>
				       dte (WrongType ("Retrieved environment variable",
						       (EVar x, loc),
						       xt',
						       xt,
						       SOME ue));
			  rt))
		  | (TError, _) => rt
		  | _ => (dte (WrongForm ("Body of environment variable read",
					  "action",
					  rest,
					  rt,
					  NONE));
			  (TError, loc))
	    end

	  | ESeq [] => raise Fail "Empty ESeq"
	  | ESeq [e1] => checkExp G e1
	  | ESeq (e1 :: rest) =>
	    let
		val e2 = (ESeq rest, loc)

		val t1 = whnorm (checkExp G e1)
		val t2 = whnorm (checkExp G e2)
	    in
		case t1 of
		    (TAction (p1, d1, r1), _) =>
		    (case t2 of
			 (TAction (p2, d2, r2), _) =>
			 let
			     val p' = predSimpl (CAnd (p1, p2), loc)

			     val d' = SM.foldli (fn (name, t, d') =>
						    case SM.find (r1, name) of
							NONE =>
							(case SM.find (d', name) of
							     NONE => SM.insert (d', name, t)
							   | SOME t' =>
							     (subTyp (t, t')
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t,
										     t',
										     SOME ue));
							      d'))
						      | SOME t' =>
							(subTyp (t, t')
							 handle Unify ue =>
								dte (WrongType ("Shared environment variable",
										(EVar name, loc),
										t,
										t',
										SOME ue));
							 d'))
						d1 d2

			     val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
						r1 r2
			 in
			     (TAction (p', d', r'), loc)
			 end
		       | (TError, _) => t2
		       | _ => (dte (WrongForm ("Action to be sequenced",
					       "action",
					       e2,
					       t2,
					       NONE));
			       (TError, loc)))
		  | (TError, _) => t1
		  | _ => (dte (WrongForm ("Action to be sequenced",
					  "action",
					  e1,
					  t1,
					  NONE));
			  (TError, loc))
	    end

	  | ELocal (e1, e2) =>
	    let
		val t1 = whnorm (checkExp G e1)
		val t2 = whnorm (checkExp G e2)
	    in
		case t1 of
		    (TAction (p1, d1, r1), _) =>
		    (case t2 of
			 (TAction (p2, d2, r2), _) =>
			 let
			     val p' = predSimpl (CAnd (p1, p2), loc)

			     val d' = SM.foldli (fn (name, t, d') =>
						    case SM.find (r1, name) of
							NONE =>
							(case SM.find (d', name) of
							     NONE => SM.insert (d', name, t)
							   | SOME t' =>
							     (subTyp (t, t')
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t,
										     t',
										     SOME ue));
							      d'))
						      | SOME t' =>
							(subTyp (t, t')
							 handle Unify ue =>
								dte (WrongType ("Shared environment variable",
										(EVar name, loc),
										t,
										t',
										SOME ue));
							 d'))
						d1 d2
			 in
			     (TAction (p', d', r2), loc)
			 end
		       | (TError, _) => t2
		       | _ => (dte (WrongForm ("Action to be sequenced",
					       "action",
					       e2,
					       t2,
					       NONE));
			       (TError, loc)))
		  | (TError, _) => t1
		  | _ => (dte (WrongForm ("Action to be sequenced",
					  "action",
					  e1,
					  t1,
					  NONE));
			  (TError, loc))
	    end


	  | EWith (e1, e2) =>
	    let
		val t1 = whnorm (checkExp G e1)
		val t2 = whnorm (checkExp G e2)
	    in
		case t1 of
		    (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
		    (case t2 of
			 (TAction (p, d, r), _) =>
			 if predImplies (pd, p) then
			     let
				 val combineRecs =
				     SM.unionWithi (fn (name, t1, t2) =>
						       (subTyp (t1, t2)
							handle Unify ue =>
							       dte (WrongType ("Environment variable",
									       (EVar name, loc),
									       t1,
									       t2,
									       SOME ue));
							t2))
			     in
				 (TAction (pr, combineRecs (d, d1),
					   combineRecs (r, r1)), loc)
			     end
			 else
			     (dte (WrongPred ("nested action",
					      pd,
					      p));
			      (TError, loc))
		       | (TError, _) => t2
		       | _ =>
			 (dte (WrongForm ("Body of nested action",
					  "action",
					  e2,
					  t2,
					  NONE));
			  (TError, loc)))
		  | (TError, _) => t1
		  | _ =>
		    (dte (WrongForm ("Container of nested action",
				     "action",
				     e1,
				     t1,
				     NONE));
		     (TError, loc))
	    end

	  | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
			       SM.empty, SM.empty), loc)
    end

exception Ununif

fun ununif (tAll as (t, loc)) =
    case t of
	TBase _ => tAll
      | TList t => (TList (ununif t), loc)
      | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
      | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
      | TUnif (_, ref (SOME t)) => ununif t
      | TNested _ => tAll
      | TError => tAll

      | TUnif (_, ref NONE) => raise Ununif

fun hasError (t, _) =
    case t of
	TBase _ => false
      | TList t => hasError t
      | TArrow (d, r) => hasError d orelse hasError r
      | TAction (p, d, r) => List.exists hasError (SM.listItems d)
			     orelse List.exists hasError (SM.listItems r)
      | TNested _ => false
      | TError => false
      | TUnif (_, ref (SOME t)) => hasError t
      | TUnif (_, ref NONE) => false


fun checkUnit G (eAll as (_, loc)) =
    let
	val _ = resetUnif ()
	val t = checkExp G eAll
    in
	if hasError t then
	    t
	else
	    ununif t
	    handle Ununif =>
		   (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
		    printd (p_typ t);
		    t)
    end

fun checkDecl G (d, _, loc) =
    case d of
	DExternType name => bindType G name
      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
      | DVal (name, to, e) =>
	let
	    val to =
		case to of
		    NONE => (newUnif (), loc)
		  | SOME to => checkTyp G to

	    val t = checkExp G e
	in
	    hasTyp (e, t, to)
	    handle Unify ue =>
		   describe_type_error loc
				       (WrongType ("Bound value",
						   e,
						   t,
						   to,
						   SOME ue));
	    bindVal G (name, to, SOME e)
	end

fun checkFile G tInit (ds, eo) =
    let
	val G' = foldl (fn (d, G) => checkDecl G d) G ds
    in
	case eo of
	    NONE => ()
	  | SOME (e as (_, loc)) =>
	    let
		val t = checkExp G' e
	    in
		hasTyp (e, t, tInit)
		handle Unify ue =>
		       (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
			preface ("Actual:", p_typ t);
			preface ("Needed:", p_typ tInit))
	    end;
	G'
    end

end
Commit	Line	Data
	1	(* HCoop Domtool (http://hcoop.sourceforge.net/)
	2	* Copyright (c) 2006, Adam Chlipala
	3	*
	4	* This program is free software; you can redistribute it and/or
	5	* modify it under the terms of the GNU General Public License
	6	* as published by the Free Software Foundation; either version 2
	7	* of the License, or (at your option) any later version.
	8	*
	9	* This program is distributed in the hope that it will be useful,
	10	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	11	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	12	* GNU General Public License for more details.
	13	*
	14	* You should have received a copy of the GNU General Public License
	15	* along with this program; if not, write to the Free Software
	16	* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
	17	*)
	18
	19	(* Domtool configuration language type checking *)
	20
	21	structure Tycheck :> TYCHECK = struct
	22
	23	open Ast Print Env
	24
	25	structure SM = StringMap
	26
	27	local
	28	val unifCount = ref 0
	29	in
	30	fun resetUnif () = unifCount := 0
	31
	32	fun newUnif () =
	33	let
	34	val c = !unifCount
	35	val name =
	36	if c < 26 then
	37	str (chr (ord #"A" + c))
	38	else
	39	"UNIF" ^ Int.toString (c - 26)
	40	in
	41	unifCount := c + 1;
	42	TUnif (name, ref NONE)
	43	end
	44	end
	45
	46	exception UnequalDomains
	47
	48	fun eqRecord f (r1, r2) =
	49	(SM.appi (fn (k, v1) =>
	50	case SM.find (r2, k) of
	51	NONE => raise UnequalDomains
	52	\| SOME v2 =>
	53	if f (v1, v2) then
	54	()
	55	else
	56	raise UnequalDomains) r1;
	57	SM.appi (fn (k, v2) =>
	58	case SM.find (r1, k) of
	59	NONE => raise UnequalDomains
	60	\| SOME v1 =>
	61	if f (v1, v2) then
	62	()
	63	else
	64	raise UnequalDomains) r2;
	65	true)
	66	handle UnequalDomains => false
	67
	68	fun eqPred ((p1, _), (p2, _)) =
	69	case (p1, p2) of
	70	(CRoot, CRoot) => true
	71	\| (CConst s1, CConst s2) => s1 = s2
	72	\| (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
	73	\| (CNot p1, CNot p2) => eqPred (p1, p2)
	74	\| (CAnd (p1, q1), CAnd (p2, q2)) =>
	75	eqPred (p1, p2) andalso eqPred (q1, q2)
	76
	77	\| _ => false
	78
	79	fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
	80	case (t1, t2) of
	81	(TBase s1, TBase s2) => s1 = s2
	82	\| (TList t1, TList t2) => eqTy (t1, t2)
	83	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
	84	eqTy (d1, d2) andalso eqTy (r1, r2)
	85
	86	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	87	eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
	88	andalso eqRecord eqTy (r1, r2)
	89
	90	\| (TNested (p1, q1), TNested (p2, q2)) =>
	91	eqPred (p1, p2) andalso eqTy (q1, q2)
	92
	93	\| (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
	94	\| (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
	95
	96	\| (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
	97
	98	\| (TError, TError) => true
	99
	100	\| _ => false
	101
	102	datatype unification_error =
	103	UnifyPred of pred * pred
	104	\| UnifyTyp of typ * typ
	105	\| UnifyOccurs of string * typ
	106
	107	exception Unify of unification_error
	108
	109	datatype type_error =
	110	WrongType of string * exp * typ * typ * unification_error option
	111	\| WrongForm of string * string * exp * typ * unification_error option
	112	\| UnboundVariable of string
	113	\| WrongPred of string * pred * pred
	114
	115	fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
	116	[PD.string s, PD.space 1, d]))
	117
	118	fun describe_unification_error t ue =
	119	case ue of
	120	UnifyPred (p1, p2) =>
	121	(print "Reason: Incompatible contexts.\n";
	122	preface ("Have:", p_pred p1);
	123	preface ("Need:", p_pred p2))
	124	\| UnifyTyp (t1, t2) =>
	125	if eqTy (t, t1) then
	126	()
	127	else
	128	(print "Reason: Incompatible types.\n";
	129	preface ("Have:", p_typ t1);
	130	preface ("Need:", p_typ t2))
	131	\| UnifyOccurs (name, t') =>
	132	if eqTy (t, t') then
	133	()
	134	else
	135	(print "Reason: Occurs check failed for ";
	136	print name;
	137	print " in:\n";
	138	printd (p_typ t))
	139
	140	fun describe_type_error loc te =
	141	case te of
	142	WrongType (place, e, t1, t2, ueo) =>
	143	(ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
	144	preface (" Expression:", p_exp e);
	145	preface ("Actual type:", p_typ t1);
	146	preface ("Needed type:", p_typ t2);
	147	Option.app (describe_unification_error t1) ueo)
	148	\| WrongForm (place, form, e, t, ueo) =>
	149	(ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
	150	preface ("Expression:", p_exp e);
	151	preface (" Type:", p_typ t);
	152	Option.app (describe_unification_error t) ueo)
	153	\| UnboundVariable name =>
	154	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
	155	\| WrongPred (place, p1, p2) =>
	156	(ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
	157	preface ("Have:", p_pred p1);
	158	preface ("Need:", p_pred p2))
	159
	160	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
	161	case (p1, p2) of
	162	(_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
	163	\| (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
	164
	165	\| (_, CPrefix (CRoot, _)) => true
	166	\| (CNot (CPrefix (CRoot, _), _), _) => true
	167
	168	\| (CRoot, CRoot) => true
	169
	170	\| (CConst s1, CConst s2) => s1 = s2
	171
	172	\| (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
	173	\| (_, CPrefix p2) => predImplies (p1All, p2)
	174
	175	\| (CNot p1, CNot p2) => predImplies (p2, p1)
	176
	177	\| _ => false
	178
	179	fun predSimpl (pAll as (p, loc)) =
	180	case p of
	181	CRoot => pAll
	182	\| CConst _ => pAll
	183	\| CPrefix p => (CPrefix (predSimpl p), loc)
	184	\| CNot p => (CNot (predSimpl p), loc)
	185	\| CAnd (p1, p2) =>
	186	let
	187	val p1' = predSimpl p1
	188	val p2' = predSimpl p2
	189	in
	190	case p1' of
	191	(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
	192	\| _ => if predImplies (p2', p1') then
	193	p2'
	194	else if predImplies (p1', p2') then
	195	p1'
	196	else
	197	(CAnd (p1', p2'), loc)
	198	end
	199
	200	fun subPred (p1, p2) =
	201	if predImplies (p1, p2) then
	202	()
	203	else
	204	raise (Unify (UnifyPred (p1, p2)))
	205
	206	fun subRecord f (r1, r2) =
	207	SM.appi (fn (k, v2) =>
	208	case SM.find (r1, k) of
	209	NONE => raise UnequalDomains
	210	\| SOME v1 => f (v1, v2)) r2
	211
	212	fun occurs u (t, _) =
	213	case t of
	214	TBase _ => false
	215	\| TList t => occurs u t
	216	\| TArrow (d, r) => occurs u d orelse occurs u r
	217	\| TAction (_, d, r) =>
	218	List.exists (occurs u) (SM.listItems d)
	219	orelse List.exists (occurs u) (SM.listItems r)
	220	\| TNested (_, t) => occurs u t
	221	\| TError => false
	222	\| TUnif (_, ref (SOME t)) => occurs u t
	223	\| TUnif (_, u') => u = u'
	224
	225	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
	226	case (t1, t2) of
	227	(TBase s1, TBase s2) =>
	228	if s1 = s2 then
	229	()
	230	else
	231	raise Unify (UnifyTyp (t1All, t2All))
	232	\| (TList t1, TList t2) => subTyp (t1, t2)
	233	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
	234	(subTyp (d2, d1);
	235	subTyp (r1, r2))
	236
	237	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	238	((subPred (p2, p1);
	239	subRecord subTyp (d2, d1);
	240	subRecord subTyp (r1, r2);
	241	subRecord subTyp (r2, r1))
	242	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
	243
	244	\| (TNested (d1, r1), TNested (d2, r2)) =>
	245	(subPred (d2, d1);
	246	subTyp (r1, r2))
	247
	248	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	249	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
	250
	251	\| (TUnif (_, r1), TUnif (_, r2)) =>
	252	if r1 = r2 then
	253	()
	254	else
	255	r1 := SOME t2All
	256
	257	\| (TUnif (name, r), _) =>
	258	if occurs r t2All then
	259	raise (Unify (UnifyOccurs (name, t2All)))
	260	else
	261	r := SOME t2All
	262
	263	\| (_, TUnif (name, r)) =>
	264	if occurs r t1All then
	265	raise (Unify (UnifyOccurs (name, t1All)))
	266	else
	267	r := SOME t1All
	268
	269	\| (TError, _) => ()
	270	\| (_, TError) => ()
	271
	272	\| _ => raise Unify (UnifyTyp (t1All, t2All))
	273
	274	fun isError t =
	275	case t of
	276	(TError, _) => true
	277	\| _ => false
	278
	279	fun whnorm (tAll as (t, loc)) =
	280	case t of
	281	TUnif (_, ref (SOME tAll)) => whnorm tAll
	282	\| _ => tAll
	283
	284	fun hasTyp (e, t1, t2) =
	285	case whnorm t2 of
	286	(TBase name, _) =>
	287	(case typeRule name of
	288	NONE => subTyp (t1, t2)
	289	\| SOME rule =>
	290	if rule e then
	291	()
	292	else
	293	subTyp (t1, t2))
	294	\| _ => subTyp (t1, t2)
	295
	296	fun checkTyp G (tAll as (t, loc)) =
	297	let
	298	val err = ErrorMsg.error (SOME loc)
	299	in
	300	case t of
	301	TBase name =>
	302	if lookupType G name then
	303	tAll
	304	else
	305	(err ("Unbound type name " ^ name);
	306	(TError, loc))
	307	\| TList t => (TList (checkTyp G t), loc)
	308	\| TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
	309	\| TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
	310	SM.map (checkTyp G) r), loc)
	311	\| TNested (p, t) => (TNested (p, checkTyp G t), loc)
	312	\| TError => raise Fail "TError in parser-generated type"
	313	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	314	end
	315
	316	fun checkExp G (eAll as (e, loc)) =
	317	let
	318	val dte = describe_type_error loc
	319	in
	320	case e of
	321	EInt _ => (TBase "int", loc)
	322	\| EString _ => (TBase "string", loc)
	323	\| EList es =>
	324	let
	325	val t = (newUnif (), loc)
	326	in
	327	foldl (fn (e', ret) =>
	328	let
	329	val t' = checkExp G e'
	330	in
	331	(hasTyp (eAll, t', t);
	332	if isError t' then
	333	(TList (TError, loc), loc)
	334	else
	335	ret)
	336	handle Unify ue =>
	337	(dte (WrongType ("List element",
	338	e',
	339	t',
	340	t,
	341	SOME ue));
	342	(TError, loc))
	343	end) (TList t, loc) es
	344	end
	345
	346	\| ELam (x, to, e) =>
	347	let
	348	val t =
	349	case to of
	350	NONE => (newUnif (), loc)
	351	\| SOME t => checkTyp G t
	352
	353	val G' = bindVal G (x, t, NONE)
	354	val t' = checkExp G' e
	355	in
	356	(TArrow (t, t'), loc)
	357	end
	358	\| EVar x =>
	359	(case lookupVal G x of
	360	NONE => (dte (UnboundVariable x);
	361	(TError, loc))
	362	\| SOME t => t)
	363	\| EApp (func, arg) =>
	364	let
	365	val dom = (newUnif (), loc)
	366	val ran = (newUnif (), loc)
	367
	368	val tf = checkExp G func
	369	val ta = checkExp G arg
	370	in
	371	(hasTyp (func, tf, (TArrow (dom, ran), loc));
	372	hasTyp (arg, ta, dom)
	373	handle Unify ue =>
	374	dte (WrongType ("Function argument",
	375	arg,
	376	ta,
	377	dom,
	378	SOME ue));
	379	ran)
	380	handle Unify ue =>
	381	(dte (WrongForm ("Function to be applied",
	382	"function",
	383	func,
	384	tf,
	385	SOME ue));
	386	(TError, loc))
	387	end
	388
	389	\| ESet (evar, e) =>
	390	let
	391	val t = checkExp G e
	392	in
	393	(TAction ((CPrefix (CRoot, loc), loc),
	394	SM.empty,
	395	SM.insert (SM.empty, evar, t)),
	396	loc)
	397	end
	398	\| EGet (x, evar, rest) =>
	399	let
	400	val xt = (newUnif (), loc)
	401	val G' = bindVal G (x, xt, NONE)
	402
	403	val rt = whnorm (checkExp G' rest)
	404	in
	405	case rt of
	406	(TAction (p, d, r), _) =>
	407	(case SM.find (d, evar) of
	408	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	409	\| SOME xt' =>
	410	(subTyp (xt', xt)
	411	handle Unify ue =>
	412	dte (WrongType ("Retrieved environment variable",
	413	(EVar x, loc),
	414	xt',
	415	xt,
	416	SOME ue));
	417	rt))
	418	\| (TError, _) => rt
	419	\| _ => (dte (WrongForm ("Body of environment variable read",
	420	"action",
	421	rest,
	422	rt,
	423	NONE));
	424	(TError, loc))
	425	end
	426
	427	\| ESeq [] => raise Fail "Empty ESeq"
	428	\| ESeq [e1] => checkExp G e1
	429	\| ESeq (e1 :: rest) =>
	430	let
	431	val e2 = (ESeq rest, loc)
	432
	433	val t1 = whnorm (checkExp G e1)
	434	val t2 = whnorm (checkExp G e2)
	435	in
	436	case t1 of
	437	(TAction (p1, d1, r1), _) =>
	438	(case t2 of
	439	(TAction (p2, d2, r2), _) =>
	440	let
	441	val p' = predSimpl (CAnd (p1, p2), loc)
	442
	443	val d' = SM.foldli (fn (name, t, d') =>
	444	case SM.find (r1, name) of
	445	NONE =>
	446	(case SM.find (d', name) of
	447	NONE => SM.insert (d', name, t)
	448	\| SOME t' =>
	449	(subTyp (t, t')
	450	handle Unify ue =>
	451	dte (WrongType ("Shared environment variable",
	452	(EVar name, loc),
	453	t,
	454	t',
	455	SOME ue));
	456	d'))
	457	\| SOME t' =>
	458	(subTyp (t, t')
	459	handle Unify ue =>
	460	dte (WrongType ("Shared environment variable",
	461	(EVar name, loc),
	462	t,
	463	t',
	464	SOME ue));
	465	d'))
	466	d1 d2
	467
	468	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	469	r1 r2
	470	in
	471	(TAction (p', d', r'), loc)
	472	end
	473	\| (TError, _) => t2
	474	\| _ => (dte (WrongForm ("Action to be sequenced",
	475	"action",
	476	e2,
	477	t2,
	478	NONE));
	479	(TError, loc)))
	480	\| (TError, _) => t1
	481	\| _ => (dte (WrongForm ("Action to be sequenced",
	482	"action",
	483	e1,
	484	t1,
	485	NONE));
	486	(TError, loc))
	487	end
	488
	489	\| ELocal (e1, e2) =>
	490	let
	491	val t1 = whnorm (checkExp G e1)
	492	val t2 = whnorm (checkExp G e2)
	493	in
	494	case t1 of
	495	(TAction (p1, d1, r1), _) =>
	496	(case t2 of
	497	(TAction (p2, d2, r2), _) =>
	498	let
	499	val p' = predSimpl (CAnd (p1, p2), loc)
	500
	501	val d' = SM.foldli (fn (name, t, d') =>
	502	case SM.find (r1, name) of
	503	NONE =>
	504	(case SM.find (d', name) of
	505	NONE => SM.insert (d', name, t)
	506	\| SOME t' =>
	507	(subTyp (t, t')
	508	handle Unify ue =>
	509	dte (WrongType ("Shared environment variable",
	510	(EVar name, loc),
	511	t,
	512	t',
	513	SOME ue));
	514	d'))
	515	\| SOME t' =>
	516	(subTyp (t, t')
	517	handle Unify ue =>
	518	dte (WrongType ("Shared environment variable",
	519	(EVar name, loc),
	520	t,
	521	t',
	522	SOME ue));
	523	d'))
	524	d1 d2
	525	in
	526	(TAction (p', d', r2), loc)
	527	end
	528	\| (TError, _) => t2
	529	\| _ => (dte (WrongForm ("Action to be sequenced",
	530	"action",
	531	e2,
	532	t2,
	533	NONE));
	534	(TError, loc)))
	535	\| (TError, _) => t1
	536	\| _ => (dte (WrongForm ("Action to be sequenced",
	537	"action",
	538	e1,
	539	t1,
	540	NONE));
	541	(TError, loc))
	542	end
	543
	544
	545	\| EWith (e1, e2) =>
	546	let
	547	val t1 = whnorm (checkExp G e1)
	548	val t2 = whnorm (checkExp G e2)
	549	in
	550	case t1 of
	551	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
	552	(case t2 of
	553	(TAction (p, d, r), _) =>
	554	if predImplies (pd, p) then
	555	let
	556	val combineRecs =
	557	SM.unionWithi (fn (name, t1, t2) =>
	558	(subTyp (t1, t2)
	559	handle Unify ue =>
	560	dte (WrongType ("Environment variable",
	561	(EVar name, loc),
	562	t1,
	563	t2,
	564	SOME ue));
	565	t2))
	566	in
	567	(TAction (pr, combineRecs (d, d1),
	568	combineRecs (r, r1)), loc)
	569	end
	570	else
	571	(dte (WrongPred ("nested action",
	572	pd,
	573	p));
	574	(TError, loc))
	575	\| (TError, _) => t2
	576	\| _ =>
	577	(dte (WrongForm ("Body of nested action",
	578	"action",
	579	e2,
	580	t2,
	581	NONE));
	582	(TError, loc)))
	583	\| (TError, _) => t1
	584	\| _ =>
	585	(dte (WrongForm ("Container of nested action",
	586	"action",
	587	e1,
	588	t1,
	589	NONE));
	590	(TError, loc))
	591	end
	592
	593	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	594	SM.empty, SM.empty), loc)
	595	end
	596
	597	exception Ununif
	598
	599	fun ununif (tAll as (t, loc)) =
	600	case t of
	601	TBase _ => tAll
	602	\| TList t => (TList (ununif t), loc)
	603	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	604	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	605	\| TUnif (_, ref (SOME t)) => ununif t
	606	\| TNested _ => tAll
	607	\| TError => tAll
	608
	609	\| TUnif (_, ref NONE) => raise Ununif
	610
	611	fun hasError (t, _) =
	612	case t of
	613	TBase _ => false
	614	\| TList t => hasError t
	615	\| TArrow (d, r) => hasError d orelse hasError r
	616	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	617	orelse List.exists hasError (SM.listItems r)
	618	\| TNested _ => false
	619	\| TError => false
	620	\| TUnif (_, ref (SOME t)) => hasError t
	621	\| TUnif (_, ref NONE) => false
	622
	623
	624	fun checkUnit G (eAll as (_, loc)) =
	625	let
	626	val _ = resetUnif ()
	627	val t = checkExp G eAll
	628	in
	629	if hasError t then
	630	t
	631	else
	632	ununif t
	633	handle Ununif =>
	634	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
	635	printd (p_typ t);
	636	t)
	637	end
	638
	639	fun checkDecl G (d, _, loc) =
	640	case d of
	641	DExternType name => bindType G name
	642	\| DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
	643	\| DVal (name, to, e) =>
	644	let
	645	val to =
	646	case to of
	647	NONE => (newUnif (), loc)
	648	\| SOME to => checkTyp G to
	649
	650	val t = checkExp G e
	651	in
	652	hasTyp (e, t, to)
	653	handle Unify ue =>
	654	describe_type_error loc
	655	(WrongType ("Bound value",
	656	e,
	657	t,
	658	to,
	659	SOME ue));
	660	bindVal G (name, to, SOME e)
	661	end
	662
	663	fun checkFile G tInit (ds, eo) =
	664	let
	665	val G' = foldl (fn (d, G) => checkDecl G d) G ds
	666	in
	667	case eo of
	668	NONE => ()
	669	\| SOME (e as (_, loc)) =>
	670	let
	671	val t = checkExp G' e
	672	in
	673	hasTyp (e, t, tInit)
	674	handle Unify ue =>
	675	(ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
	676	preface ("Actual:", p_typ t);
	677	preface ("Needed:", p_typ tInit))
	678	end;
	679	G'
	680	end
	681
	682	end