[hcoop/domtool2.git] / 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 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
      | 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
27d9de59 AC	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.
dac62e84	17	*)
27d9de59 AC	18
	19	(* Domtool configuration language type checking *)
	20
	21	structure Tycheck :> TYCHECK = struct
	22
492c1cff	23	open Ast Print Env
27d9de59 AC	24
	25	structure SM = StringMap
	26
27d9de59 AC	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
234b917a	90	\| (TNested (p1, q1), TNested (p2, q2)) =>
1a4e5a6c	91	eqPred (p1, p2) andalso eqTy (q1, q2)
234b917a	92
27d9de59 AC	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
234b917a	113	\| WrongPred of string * pred * pred
27d9de59	114
27d9de59 AC	115	fun describe_unification_error t ue =
	116	case ue of
	117	UnifyPred (p1, p2) =>
234b917a	118	(print "Reason: Incompatible contexts.\n";
27d9de59 AC	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")
234b917a AC	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))
27d9de59	156
db427c67	157	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
27d9de59	158	case (p1, p2) of
1a4e5a6c AC	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
db427c67 AC	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)
234b917a	170	\| (_, CPrefix p2) => predImplies (p1All, p2)
db427c67 AC	171
db427c67 AC	172	\| (CNot p1, CNot p2) => predImplies (p2, p1)
27d9de59	173
db427c67 AC	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'
1a4e5a6c AC	191	else if predImplies (p1', p2') then
1a4e5a6c AC	192	p1'
db427c67 AC	193	else
	194	(CAnd (p1', p2'), loc)
	195	end
	196
234b917a	197	fun subPred (p1, p2) =
db427c67 AC	198	if predImplies (p1, p2) then
	199	()
	200	else
	201	raise (Unify (UnifyPred (p1, p2)))
27d9de59	202
234b917a AC	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
27d9de59 AC	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)
1a4e5a6c	217	\| TNested (_, t) => occurs u t
27d9de59 AC	218	\| TError => false
	219	\| TUnif (_, ref (SOME t)) => occurs u t
	220	\| TUnif (_, u') => u = u'
	221
234b917a	222	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
27d9de59 AC	223	case (t1, t2) of
	224	(TBase s1, TBase s2) =>
	225	if s1 = s2 then
	226	()
	227	else
	228	raise Unify (UnifyTyp (t1All, t2All))
234b917a	229	\| (TList t1, TList t2) => subTyp (t1, t2)
27d9de59	230	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
234b917a AC	231	(subTyp (d2, d1);
234b917a AC	232	subTyp (r1, r2))
27d9de59 AC	233
27d9de59 AC	234	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
234b917a AC	235	((subPred (p2, p1);
	236	subRecord subTyp (d2, d1);
	237	subRecord subTyp (r1, r2);
	238	subRecord subTyp (r2, r1))
27d9de59 AC	239	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
27d9de59 AC	240
234b917a AC	241	\| (TNested (d1, r1), TNested (d2, r2)) =>
234b917a AC	242	(subPred (d2, d1);
1a4e5a6c	243	subTyp (r1, r2))
234b917a AC	244
	245	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	246	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
27d9de59 AC	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
db427c67 AC	276	fun whnorm (tAll as (t, loc)) =
	277	case t of
	278	TUnif (_, ref (SOME tAll)) => whnorm tAll
	279	\| _ => tAll
	280
629a34f6 AC	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
6be996d4	291	fun hasTyp (e, t1, t2) =
629a34f6 AC	292	if (case baseCondition t2 of
	293	NONE => false
	294	\| SOME rule => rule e) then
	295	()
	296	else
	297	subTyp (t1, t2)
6be996d4	298
095de39e AC	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
234b917a AC	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)
095de39e AC	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))
234b917a AC	333	\| TError => raise Fail "TError in parser-generated type"
	334	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	335	end
	336
27d9de59 AC	337	fun checkExp G (eAll as (e, loc)) =
	338	let
	339	val dte = describe_type_error loc
	340	in
	341	case e of
	342	EInt _ => (TBase "int", loc)
	343	\| EString _ => (TBase "string", loc)
	344	\| EList es =>
	345	let
	346	val t = (newUnif (), loc)
	347	in
	348	foldl (fn (e', ret) =>
	349	let
	350	val t' = checkExp G e'
	351	in
6be996d4	352	(hasTyp (eAll, t', t);
27d9de59 AC	353	if isError t' then
	354	(TList (TError, loc), loc)
	355	else
	356	ret)
	357	handle Unify ue =>
	358	(dte (WrongType ("List element",
	359	e',
	360	t',
	361	t,
	362	SOME ue));
	363	(TError, loc))
	364	end) (TList t, loc) es
	365	end
	366
	367	\| ELam (x, to, e) =>
	368	let
	369	val t =
	370	case to of
	371	NONE => (newUnif (), loc)
234b917a	372	\| SOME t => checkTyp G t
27d9de59	373
492c1cff	374	val G' = bindVal G (x, t, NONE)
27d9de59 AC	375	val t' = checkExp G' e
	376	in
	377	(TArrow (t, t'), loc)
	378	end
	379	\| EVar x =>
234b917a	380	(case lookupVal G x of
27d9de59 AC	381	NONE => (dte (UnboundVariable x);
	382	(TError, loc))
	383	\| SOME t => t)
	384	\| EApp (func, arg) =>
	385	let
	386	val dom = (newUnif (), loc)
	387	val ran = (newUnif (), loc)
	388
	389	val tf = checkExp G func
	390	val ta = checkExp G arg
	391	in
6be996d4 AC	392	(hasTyp (func, tf, (TArrow (dom, ran), loc));
6be996d4 AC	393	hasTyp (arg, ta, dom)
27d9de59 AC	394	handle Unify ue =>
	395	dte (WrongType ("Function argument",
	396	arg,
	397	ta,
	398	dom,
	399	SOME ue));
	400	ran)
	401	handle Unify ue =>
	402	(dte (WrongForm ("Function to be applied",
	403	"function",
	404	func,
	405	tf,
	406	SOME ue));
	407	(TError, loc))
	408	end
db427c67 AC	409
	410	\| ESet (evar, e) =>
	411	let
	412	val t = checkExp G e
	413	in
	414	(TAction ((CPrefix (CRoot, loc), loc),
	415	SM.empty,
	416	SM.insert (SM.empty, evar, t)),
	417	loc)
	418	end
	419	\| EGet (x, evar, rest) =>
	420	let
	421	val xt = (newUnif (), loc)
492c1cff	422	val G' = bindVal G (x, xt, NONE)
db427c67 AC	423
	424	val rt = whnorm (checkExp G' rest)
	425	in
	426	case rt of
	427	(TAction (p, d, r), _) =>
	428	(case SM.find (d, evar) of
	429	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	430	\| SOME xt' =>
234b917a	431	(subTyp (xt', xt)
db427c67 AC	432	handle Unify ue =>
	433	dte (WrongType ("Retrieved environment variable",
	434	(EVar x, loc),
	435	xt',
	436	xt,
	437	SOME ue));
	438	rt))
234b917a	439	\| (TError, _) => rt
db427c67 AC	440	\| _ => (dte (WrongForm ("Body of environment variable read",
	441	"action",
	442	rest,
	443	rt,
	444	NONE));
	445	(TError, loc))
	446	end
	447
	448	\| ESeq [] => raise Fail "Empty ESeq"
	449	\| ESeq [e1] => checkExp G e1
	450	\| ESeq (e1 :: rest) =>
	451	let
	452	val e2 = (ESeq rest, loc)
	453
	454	val t1 = whnorm (checkExp G e1)
	455	val t2 = whnorm (checkExp G e2)
	456	in
	457	case t1 of
	458	(TAction (p1, d1, r1), _) =>
	459	(case t2 of
	460	(TAction (p2, d2, r2), _) =>
	461	let
	462	val p' = predSimpl (CAnd (p1, p2), loc)
	463
	464	val d' = SM.foldli (fn (name, t, d') =>
	465	case SM.find (r1, name) of
	466	NONE =>
	467	(case SM.find (d', name) of
	468	NONE => SM.insert (d', name, t)
	469	\| SOME t' =>
234b917a	470	(subTyp (t, t')
db427c67 AC	471	handle Unify ue =>
	472	dte (WrongType ("Shared environment variable",
	473	(EVar name, loc),
	474	t,
	475	t',
	476	SOME ue));
	477	d'))
	478	\| SOME t' =>
234b917a	479	(subTyp (t, t')
db427c67 AC	480	handle Unify ue =>
	481	dte (WrongType ("Shared environment variable",
	482	(EVar name, loc),
	483	t,
	484	t',
	485	SOME ue));
	486	d'))
	487	d1 d2
	488
	489	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	490	r1 r2
	491	in
	492	(TAction (p', d', r'), loc)
	493	end
234b917a	494	\| (TError, _) => t2
db427c67 AC	495	\| _ => (dte (WrongForm ("Action to be sequenced",
	496	"action",
	497	e2,
	498	t2,
	499	NONE));
	500	(TError, loc)))
234b917a	501	\| (TError, _) => t1
db427c67 AC	502	\| _ => (dte (WrongForm ("Action to be sequenced",
	503	"action",
	504	e1,
	505	t1,
	506	NONE));
	507	(TError, loc))
	508	end
	509
1a4e5a6c	510	\| ELocal (e1, e2) =>
db427c67	511	let
1a4e5a6c AC	512	val t1 = whnorm (checkExp G e1)
1a4e5a6c AC	513	val t2 = whnorm (checkExp G e2)
db427c67	514	in
1a4e5a6c AC	515	case t1 of
	516	(TAction (p1, d1, r1), _) =>
	517	(case t2 of
	518	(TAction (p2, d2, r2), _) =>
	519	let
	520	val p' = predSimpl (CAnd (p1, p2), loc)
	521
	522	val d' = SM.foldli (fn (name, t, d') =>
	523	case SM.find (r1, name) of
	524	NONE =>
	525	(case SM.find (d', name) of
	526	NONE => SM.insert (d', name, t)
	527	\| SOME t' =>
	528	(subTyp (t, t')
	529	handle Unify ue =>
	530	dte (WrongType ("Shared environment variable",
	531	(EVar name, loc),
	532	t,
	533	t',
	534	SOME ue));
	535	d'))
	536	\| SOME t' =>
	537	(subTyp (t, t')
	538	handle Unify ue =>
	539	dte (WrongType ("Shared environment variable",
	540	(EVar name, loc),
	541	t,
	542	t',
	543	SOME ue));
	544	d'))
	545	d1 d2
	546	in
	547	(TAction (p', d', r2), loc)
	548	end
	549	\| (TError, _) => t2
	550	\| _ => (dte (WrongForm ("Action to be sequenced",
	551	"action",
	552	e2,
	553	t2,
	554	NONE));
	555	(TError, loc)))
	556	\| (TError, _) => t1
	557	\| _ => (dte (WrongForm ("Action to be sequenced",
db427c67	558	"action",
1a4e5a6c AC	559	e1,
1a4e5a6c AC	560	t1,
db427c67 AC	561	NONE));
	562	(TError, loc))
	563	end
234b917a	564
1a4e5a6c	565
234b917a AC	566	\| EWith (e1, e2) =>
	567	let
	568	val t1 = whnorm (checkExp G e1)
	569	val t2 = whnorm (checkExp G e2)
	570	in
	571	case t1 of
1a4e5a6c	572	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a AC	573	(case t2 of
	574	(TAction (p, d, r), _) =>
	575	if predImplies (pd, p) then
1a4e5a6c AC	576	let
	577	val combineRecs =
	578	SM.unionWithi (fn (name, t1, t2) =>
	579	(subTyp (t1, t2)
	580	handle Unify ue =>
	581	dte (WrongType ("Environment variable",
	582	(EVar name, loc),
	583	t1,
	584	t2,
	585	SOME ue));
	586	t2))
	587	in
	588	(TAction (pr, combineRecs (d, d1),
	589	combineRecs (r, r1)), loc)
	590	end
234b917a AC	591	else
	592	(dte (WrongPred ("nested action",
	593	pd,
	594	p));
	595	(TError, loc))
	596	\| (TError, _) => t2
	597	\| _ =>
	598	(dte (WrongForm ("Body of nested action",
	599	"action",
	600	e2,
	601	t2,
	602	NONE));
	603	(TError, loc)))
	604	\| (TError, _) => t1
	605	\| _ =>
	606	(dte (WrongForm ("Container of nested action",
	607	"action",
	608	e1,
	609	t1,
	610	NONE));
	611	(TError, loc))
	612	end
	613
	614	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	615	SM.empty, SM.empty), loc)
27d9de59 AC	616	end
	617
	618	exception Ununif
	619
	620	fun ununif (tAll as (t, loc)) =
	621	case t of
	622	TBase _ => tAll
	623	\| TList t => (TList (ununif t), loc)
	624	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	625	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	626	\| TUnif (_, ref (SOME t)) => ununif t
234b917a	627	\| TNested _ => tAll
27d9de59 AC	628	\| TError => tAll
	629
	630	\| TUnif (_, ref NONE) => raise Ununif
	631
	632	fun hasError (t, _) =
	633	case t of
	634	TBase _ => false
	635	\| TList t => hasError t
	636	\| TArrow (d, r) => hasError d orelse hasError r
	637	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	638	orelse List.exists hasError (SM.listItems r)
234b917a	639	\| TNested _ => false
27d9de59 AC	640	\| TError => false
	641	\| TUnif (_, ref (SOME t)) => hasError t
	642	\| TUnif (_, ref NONE) => false
	643
	644
	645	fun checkUnit G (eAll as (_, loc)) =
	646	let
	647	val _ = resetUnif ()
	648	val t = checkExp G eAll
	649	in
	650	if hasError t then
	651	t
	652	else
	653	ununif t
	654	handle Ununif =>
	655	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
	656	printd (p_typ t);
	657	t)
	658	end
	659
234b917a AC	660	fun checkDecl G (d, _, loc) =
	661	case d of
	662	DExternType name => bindType G name
492c1cff AC	663	\| DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
	664	\| DVal (name, to, e) =>
	665	let
	666	val to =
	667	case to of
	668	NONE => (newUnif (), loc)
	669	\| SOME to => checkTyp G to
	670
	671	val t = checkExp G e
	672	in
6be996d4	673	hasTyp (e, t, to)
492c1cff AC	674	handle Unify ue =>
	675	describe_type_error loc
	676	(WrongType ("Bound value",
	677	e,
	678	t,
	679	to,
	680	SOME ue));
	681	bindVal G (name, to, SOME e)
	682	end
095de39e	683	\| DContext name => bindContext G name
234b917a	684
095de39e	685	fun checkFile G tInit (_, ds, eo) =
234b917a AC	686	let
	687	val G' = foldl (fn (d, G) => checkDecl G d) G ds
	688	in
	689	case eo of
	690	NONE => ()
	691	\| SOME (e as (_, loc)) =>
	692	let
	693	val t = checkExp G' e
	694	in
6be996d4	695	hasTyp (e, t, tInit)
234b917a AC	696	handle Unify ue =>
	697	(ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
	698	preface ("Actual:", p_typ t);
	699	preface ("Needed:", p_typ tInit))
	700	end;
	701	G'
	702	end
	703
27d9de59	704	end