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 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 baseCondition t =
    case whnorm t of
	(TBase name, _) => typeRule name
      | (TList t, _) =>
	(case baseCondition t of
	     NONE => NONE
	   | SOME f => SOME (fn (EList ls, _) => List.all f ls
			      | _ => false))
      | _ => NONE

fun hasTyp (e, t1, t2) =
    if (case baseCondition t2 of
	    NONE => false
	  | SOME rule => rule e) then
	()
    else
	subTyp (t1, t2)

fun checkPred G (p, loc) =
    let
	val err = ErrorMsg.error (SOME loc)
    in
	case p of
	    CRoot => ()
	  | CConst s =>
	    if lookupContext G s then
		()
	    else
		err ("Unbound context " ^ s)
	  | CPrefix p => checkPred G p
	  | CNot p => checkPred G p
	  | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
    end

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) => (checkPred G p;
				  (TAction (p, SM.map (checkTyp G) d,
					    SM.map (checkTyp G) r), loc))
	  | TNested (p, t) => (checkPred G p;
			       (TNested (p, checkTyp G t), loc))
	  | TError => raise Fail "TError in parser-generated type"
	  | TUnif _ => raise Fail "TUnif in parser-generated type"
    end

fun envVarSetFrom v (e, _) =
    case e of
	ESet (v', e) =>
	if v = v' then
	    SOME e
	else
	    NONE
      | EGet (_, _, e) => envVarSetFrom v e
      | ESeq es => foldr (fn (e, found) =>
			     case found of
				 SOME _ => found
			       | NONE => envVarSetFrom v e)
			 NONE es
      | ELocal (_, e) => envVarSetFrom v e

      | _ => NONE

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' =>
							     ((case envVarSetFrom name e1 of
								   NONE => subTyp (t, t')
								 | SOME e => hasTyp (e, t, t'))
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t',
										     t,
										     SOME ue));
							      d'))
						      | SOME t' =>
							((case envVarSetFrom name e1 of
								   NONE => subTyp (t, t')
								 | SOME e => hasTyp (e, 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' =>
							     ((case envVarSetFrom name e1 of
								   NONE => subTyp (t', t)
								 | SOME e => hasTyp (e, t', t))
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t',
										     t,
										     SOME ue));
							      d'))
						      | SOME t' =>
							((case envVarSetFrom name e1 of
								   NONE => subTyp (t', t)
								 | SOME e => hasTyp (e, 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
      | DContext name => bindContext G name

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 describe_unification_error t ue =
	116	case ue of
	117	UnifyPred (p1, p2) =>
	118	(print "Reason: Incompatible contexts.\n";
	119	preface ("Have:", p_pred p1);
	120	preface ("Need:", p_pred p2))
	121	\| UnifyTyp (t1, t2) =>
	122	if eqTy (t, t1) then
	123	()
	124	else
	125	(print "Reason: Incompatible types.\n";
	126	preface ("Have:", p_typ t1);
	127	preface ("Need:", p_typ t2))
	128	\| UnifyOccurs (name, t') =>
	129	if eqTy (t, t') then
	130	()
	131	else
	132	(print "Reason: Occurs check failed for ";
	133	print name;
	134	print " in:\n";
	135	printd (p_typ t))
	136
	137	fun describe_type_error loc te =
	138	case te of
	139	WrongType (place, e, t1, t2, ueo) =>
	140	(ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
	141	preface (" Expression:", p_exp e);
	142	preface ("Actual type:", p_typ t1);
	143	preface ("Needed type:", p_typ t2);
	144	Option.app (describe_unification_error t1) ueo)
	145	\| WrongForm (place, form, e, t, ueo) =>
	146	(ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
	147	preface ("Expression:", p_exp e);
	148	preface (" Type:", p_typ t);
	149	Option.app (describe_unification_error t) ueo)
	150	\| UnboundVariable name =>
	151	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
	152	\| WrongPred (place, p1, p2) =>
	153	(ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
	154	preface ("Have:", p_pred p1);
	155	preface ("Need:", p_pred p2))
	156
	157	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
	158	case (p1, p2) of
	159	(_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
	160	\| (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
	161
	162	\| (_, CPrefix (CRoot, _)) => true
	163	\| (CNot (CPrefix (CRoot, _), _), _) => true
	164
	165	\| (CRoot, CRoot) => true
	166
	167	\| (CConst s1, CConst s2) => s1 = s2
	168
	169	\| (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
	170	\| (_, CPrefix p2) => predImplies (p1All, p2)
	171
	172	\| (CNot p1, CNot p2) => predImplies (p2, p1)
	173
	174	\| _ => false
	175
	176	fun predSimpl (pAll as (p, loc)) =
	177	case p of
	178	CRoot => pAll
	179	\| CConst _ => pAll
	180	\| CPrefix p => (CPrefix (predSimpl p), loc)
	181	\| CNot p => (CNot (predSimpl p), loc)
	182	\| CAnd (p1, p2) =>
	183	let
	184	val p1' = predSimpl p1
	185	val p2' = predSimpl p2
	186	in
	187	case p1' of
	188	(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
	189	\| _ => if predImplies (p2', p1') then
	190	p2'
	191	else if predImplies (p1', p2') then
	192	p1'
	193	else
	194	(CAnd (p1', p2'), loc)
	195	end
	196
	197	fun subPred (p1, p2) =
	198	if predImplies (p1, p2) then
	199	()
	200	else
	201	raise (Unify (UnifyPred (p1, p2)))
	202
	203	fun subRecord f (r1, r2) =
	204	SM.appi (fn (k, v2) =>
	205	case SM.find (r1, k) of
	206	NONE => raise UnequalDomains
	207	\| SOME v1 => f (v1, v2)) r2
	208
	209	fun occurs u (t, _) =
	210	case t of
	211	TBase _ => false
	212	\| TList t => occurs u t
	213	\| TArrow (d, r) => occurs u d orelse occurs u r
	214	\| TAction (_, d, r) =>
	215	List.exists (occurs u) (SM.listItems d)
	216	orelse List.exists (occurs u) (SM.listItems r)
	217	\| TNested (_, t) => occurs u t
	218	\| TError => false
	219	\| TUnif (_, ref (SOME t)) => occurs u t
	220	\| TUnif (_, u') => u = u'
	221
	222	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
	223	case (t1, t2) of
	224	(TBase s1, TBase s2) =>
	225	if s1 = s2 then
	226	()
	227	else
	228	raise Unify (UnifyTyp (t1All, t2All))
	229	\| (TList t1, TList t2) => subTyp (t1, t2)
	230	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
	231	(subTyp (d2, d1);
	232	subTyp (r1, r2))
	233
	234	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	235	((subPred (p2, p1);
	236	subRecord subTyp (d2, d1);
	237	subRecord subTyp (r1, r2);
	238	subRecord subTyp (r2, r1))
	239	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
	240
	241	\| (TNested (d1, r1), TNested (d2, r2)) =>
	242	(subPred (d2, d1);
	243	subTyp (r1, r2))
	244
	245	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	246	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
	247
	248	\| (TUnif (_, r1), TUnif (_, r2)) =>
	249	if r1 = r2 then
	250	()
	251	else
	252	r1 := SOME t2All
	253
	254	\| (TUnif (name, r), _) =>
	255	if occurs r t2All then
	256	raise (Unify (UnifyOccurs (name, t2All)))
	257	else
	258	r := SOME t2All
	259
	260	\| (_, TUnif (name, r)) =>
	261	if occurs r t1All then
	262	raise (Unify (UnifyOccurs (name, t1All)))
	263	else
	264	r := SOME t1All
	265
	266	\| (TError, _) => ()
	267	\| (_, TError) => ()
	268
	269	\| _ => raise Unify (UnifyTyp (t1All, t2All))
	270
	271	fun isError t =
	272	case t of
	273	(TError, _) => true
	274	\| _ => false
	275
	276	fun whnorm (tAll as (t, loc)) =
	277	case t of
	278	TUnif (_, ref (SOME tAll)) => whnorm tAll
	279	\| _ => tAll
	280
	281	fun baseCondition t =
	282	case whnorm t of
	283	(TBase name, _) => typeRule name
	284	\| (TList t, _) =>
	285	(case baseCondition t of
	286	NONE => NONE
	287	\| SOME f => SOME (fn (EList ls, _) => List.all f ls
	288	\| _ => false))
	289	\| _ => NONE
	290
	291	fun hasTyp (e, t1, t2) =
	292	if (case baseCondition t2 of
	293	NONE => false
	294	\| SOME rule => rule e) then
	295	()
	296	else
	297	subTyp (t1, t2)
	298
	299	fun checkPred G (p, loc) =
	300	let
	301	val err = ErrorMsg.error (SOME loc)
	302	in
	303	case p of
	304	CRoot => ()
	305	\| CConst s =>
	306	if lookupContext G s then
	307	()
	308	else
	309	err ("Unbound context " ^ s)
	310	\| CPrefix p => checkPred G p
	311	\| CNot p => checkPred G p
	312	\| CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
	313	end
	314
	315	fun checkTyp G (tAll as (t, loc)) =
	316	let
	317	val err = ErrorMsg.error (SOME loc)
	318	in
	319	case t of
	320	TBase name =>
	321	if lookupType G name then
	322	tAll
	323	else
	324	(err ("Unbound type name " ^ name);
	325	(TError, loc))
	326	\| TList t => (TList (checkTyp G t), loc)
	327	\| TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
	328	\| TAction (p, d, r) => (checkPred G p;
	329	(TAction (p, SM.map (checkTyp G) d,
	330	SM.map (checkTyp G) r), loc))
	331	\| TNested (p, t) => (checkPred G p;
	332	(TNested (p, checkTyp G t), loc))
	333	\| TError => raise Fail "TError in parser-generated type"
	334	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	335	end
	336
	337	fun envVarSetFrom v (e, _) =
	338	case e of
	339	ESet (v', e) =>
	340	if v = v' then
	341	SOME e
	342	else
	343	NONE
	344	\| EGet (_, _, e) => envVarSetFrom v e
	345	\| ESeq es => foldr (fn (e, found) =>
	346	case found of
	347	SOME _ => found
	348	\| NONE => envVarSetFrom v e)
	349	NONE es
	350	\| ELocal (_, e) => envVarSetFrom v e
	351
	352	\| _ => NONE
	353
	354	fun checkExp G (eAll as (e, loc)) =
	355	let
	356	val dte = describe_type_error loc
	357	in
	358	case e of
	359	EInt _ => (TBase "int", loc)
	360	\| EString _ => (TBase "string", loc)
	361	\| EList es =>
	362	let
	363	val t = (newUnif (), loc)
	364	in
	365	foldl (fn (e', ret) =>
	366	let
	367	val t' = checkExp G e'
	368	in
	369	(hasTyp (eAll, t', t);
	370	if isError t' then
	371	(TList (TError, loc), loc)
	372	else
	373	ret)
	374	handle Unify ue =>
	375	(dte (WrongType ("List element",
	376	e',
	377	t',
	378	t,
	379	SOME ue));
	380	(TError, loc))
	381	end) (TList t, loc) es
	382	end
	383
	384	\| ELam (x, to, e) =>
	385	let
	386	val t =
	387	case to of
	388	NONE => (newUnif (), loc)
	389	\| SOME t => checkTyp G t
	390
	391	val G' = bindVal G (x, t, NONE)
	392	val t' = checkExp G' e
	393	in
	394	(TArrow (t, t'), loc)
	395	end
	396	\| EVar x =>
	397	(case lookupVal G x of
	398	NONE => (dte (UnboundVariable x);
	399	(TError, loc))
	400	\| SOME t => t)
	401	\| EApp (func, arg) =>
	402	let
	403	val dom = (newUnif (), loc)
	404	val ran = (newUnif (), loc)
	405
	406	val tf = checkExp G func
	407	val ta = checkExp G arg
	408	in
	409	(hasTyp (func, tf, (TArrow (dom, ran), loc));
	410	hasTyp (arg, ta, dom)
	411	handle Unify ue =>
	412	dte (WrongType ("Function argument",
	413	arg,
	414	ta,
	415	dom,
	416	SOME ue));
	417	ran)
	418	handle Unify ue =>
	419	(dte (WrongForm ("Function to be applied",
	420	"function",
	421	func,
	422	tf,
	423	SOME ue));
	424	(TError, loc))
	425	end
	426
	427	\| ESet (evar, e) =>
	428	let
	429	val t = checkExp G e
	430	in
	431	(TAction ((CPrefix (CRoot, loc), loc),
	432	SM.empty,
	433	SM.insert (SM.empty, evar, t)),
	434	loc)
	435	end
	436	\| EGet (x, evar, rest) =>
	437	let
	438	val xt = (newUnif (), loc)
	439	val G' = bindVal G (x, xt, NONE)
	440
	441	val rt = whnorm (checkExp G' rest)
	442	in
	443	case rt of
	444	(TAction (p, d, r), _) =>
	445	(case SM.find (d, evar) of
	446	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	447	\| SOME xt' =>
	448	(subTyp (xt', xt)
	449	handle Unify ue =>
	450	dte (WrongType ("Retrieved environment variable",
	451	(EVar x, loc),
	452	xt',
	453	xt,
	454	SOME ue));
	455	rt))
	456	\| (TError, _) => rt
	457	\| _ => (dte (WrongForm ("Body of environment variable read",
	458	"action",
	459	rest,
	460	rt,
	461	NONE));
	462	(TError, loc))
	463	end
	464
	465	\| ESeq [] => raise Fail "Empty ESeq"
	466	\| ESeq [e1] => checkExp G e1
	467	\| ESeq (e1 :: rest) =>
	468	let
	469	val e2 = (ESeq rest, loc)
	470
	471	val t1 = whnorm (checkExp G e1)
	472	val t2 = whnorm (checkExp G e2)
	473	in
	474	case t1 of
	475	(TAction (p1, d1, r1), _) =>
	476	(case t2 of
	477	(TAction (p2, d2, r2), _) =>
	478	let
	479	val p' = predSimpl (CAnd (p1, p2), loc)
	480
	481	val d' = SM.foldli (fn (name, t, d') =>
	482	case SM.find (r1, name) of
	483	NONE =>
	484	(case SM.find (d', name) of
	485	NONE => SM.insert (d', name, t)
	486	\| SOME t' =>
	487	((case envVarSetFrom name e1 of
	488	NONE => subTyp (t, t')
	489	\| SOME e => hasTyp (e, t, t'))
	490	handle Unify ue =>
	491	dte (WrongType ("Shared environment variable",
	492	(EVar name, loc),
	493	t',
	494	t,
	495	SOME ue));
	496	d'))
	497	\| SOME t' =>
	498	((case envVarSetFrom name e1 of
	499	NONE => subTyp (t, t')
	500	\| SOME e => hasTyp (e, t, t'))
	501	handle Unify ue =>
	502	dte (WrongType ("Shared environment variable",
	503	(EVar name, loc),
	504	t',
	505	t,
	506	SOME ue));
	507	d'))
	508	d1 d2
	509
	510	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	511	r1 r2
	512	in
	513	(TAction (p', d', r'), loc)
	514	end
	515	\| (TError, _) => t2
	516	\| _ => (dte (WrongForm ("Action to be sequenced",
	517	"action",
	518	e2,
	519	t2,
	520	NONE));
	521	(TError, loc)))
	522	\| (TError, _) => t1
	523	\| _ => (dte (WrongForm ("Action to be sequenced",
	524	"action",
	525	e1,
	526	t1,
	527	NONE));
	528	(TError, loc))
	529	end
	530
	531	\| ELocal (e1, e2) =>
	532	let
	533	val t1 = whnorm (checkExp G e1)
	534	val t2 = whnorm (checkExp G e2)
	535	in
	536	case t1 of
	537	(TAction (p1, d1, r1), _) =>
	538	(case t2 of
	539	(TAction (p2, d2, r2), _) =>
	540	let
	541	val p' = predSimpl (CAnd (p1, p2), loc)
	542
	543	val d' = SM.foldli (fn (name, t, d') =>
	544	case SM.find (r1, name) of
	545	NONE =>
	546	(case SM.find (d', name) of
	547	NONE => SM.insert (d', name, t)
	548	\| SOME t' =>
	549	((case envVarSetFrom name e1 of
	550	NONE => subTyp (t', t)
	551	\| SOME e => hasTyp (e, t', t))
	552	handle Unify ue =>
	553	dte (WrongType ("Shared environment variable",
	554	(EVar name, loc),
	555	t',
	556	t,
	557	SOME ue));
	558	d'))
	559	\| SOME t' =>
	560	((case envVarSetFrom name e1 of
	561	NONE => subTyp (t', t)
	562	\| SOME e => hasTyp (e, t', t))
	563	handle Unify ue =>
	564	dte (WrongType ("Shared environment variable",
	565	(EVar name, loc),
	566	t',
	567	t,
	568	SOME ue));
	569	d'))
	570	d1 d2
	571	in
	572	(TAction (p', d', r2), loc)
	573	end
	574	\| (TError, _) => t2
	575	\| _ => (dte (WrongForm ("Action to be sequenced",
	576	"action",
	577	e2,
	578	t2,
	579	NONE));
	580	(TError, loc)))
	581	\| (TError, _) => t1
	582	\| _ => (dte (WrongForm ("Action to be sequenced",
	583	"action",
	584	e1,
	585	t1,
	586	NONE));
	587	(TError, loc))
	588	end
	589
	590
	591	\| EWith (e1, e2) =>
	592	let
	593	val t1 = whnorm (checkExp G e1)
	594	val t2 = whnorm (checkExp G e2)
	595	in
	596	case t1 of
	597	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
	598	(case t2 of
	599	(TAction (p, d, r), _) =>
	600	if predImplies (pd, p) then
	601	let
	602	val combineRecs =
	603	SM.unionWithi (fn (name, t1, t2) =>
	604	(subTyp (t1, t2)
	605	handle Unify ue =>
	606	dte (WrongType ("Environment variable",
	607	(EVar name, loc),
	608	t1,
	609	t2,
	610	SOME ue));
	611	t2))
	612	in
	613	(TAction (pr, combineRecs (d, d1),
	614	combineRecs (r, r1)), loc)
	615	end
	616	else
	617	(dte (WrongPred ("nested action",
	618	pd,
	619	p));
	620	(TError, loc))
	621	\| (TError, _) => t2
	622	\| _ =>
	623	(dte (WrongForm ("Body of nested action",
	624	"action",
	625	e2,
	626	t2,
	627	NONE));
	628	(TError, loc)))
	629	\| (TError, _) => t1
	630	\| _ =>
	631	(dte (WrongForm ("Container of nested action",
	632	"action",
	633	e1,
	634	t1,
	635	NONE));
	636	(TError, loc))
	637	end
	638
	639	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	640	SM.empty, SM.empty), loc)
	641	end
	642
	643	exception Ununif
	644
	645	fun ununif (tAll as (t, loc)) =
	646	case t of
	647	TBase _ => tAll
	648	\| TList t => (TList (ununif t), loc)
	649	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	650	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	651	\| TUnif (_, ref (SOME t)) => ununif t
	652	\| TNested _ => tAll
	653	\| TError => tAll
	654
	655	\| TUnif (_, ref NONE) => raise Ununif
	656
	657	fun hasError (t, _) =
	658	case t of
	659	TBase _ => false
	660	\| TList t => hasError t
	661	\| TArrow (d, r) => hasError d orelse hasError r
	662	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	663	orelse List.exists hasError (SM.listItems r)
	664	\| TNested _ => false
	665	\| TError => false
	666	\| TUnif (_, ref (SOME t)) => hasError t
	667	\| TUnif (_, ref NONE) => false
	668
	669
	670	fun checkUnit G (eAll as (_, loc)) =
	671	let
	672	val _ = resetUnif ()
	673	val t = checkExp G eAll
	674	in
	675	if hasError t then
	676	t
	677	else
	678	ununif t
	679	handle Ununif =>
	680	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
	681	printd (p_typ t);
	682	t)
	683	end
	684
	685	fun checkDecl G (d, _, loc) =
	686	case d of
	687	DExternType name => bindType G name
	688	\| DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
	689	\| DVal (name, to, e) =>
	690	let
	691	val to =
	692	case to of
	693	NONE => (newUnif (), loc)
	694	\| SOME to => checkTyp G to
	695
	696	val t = checkExp G e
	697	in
	698	hasTyp (e, t, to)
	699	handle Unify ue =>
	700	describe_type_error loc
	701	(WrongType ("Bound value",
	702	e,
	703	t,
	704	to,
	705	SOME ue));
	706	bindVal G (name, to, SOME e)
	707	end
	708	\| DContext name => bindContext G name
	709
	710	fun checkFile G tInit (_, ds, eo) =
	711	let
	712	val G' = foldl (fn (d, G) => checkDecl G d) G ds
	713	in
	714	case eo of
	715	NONE => ()
	716	\| SOME (e as (_, loc)) =>
	717	let
	718	val t = checkExp G' e
	719	in
	720	hasTyp (e, t, tInit)
	721	handle Unify ue =>
	722	(ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
	723	preface ("Actual:", p_typ t);
	724	preface ("Needed:", p_typ tInit))
	725	end;
	726	G'
	727	end
	728
	729	end