[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 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
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
8a7c40fa AC	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
27d9de59 AC	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
6be996d4	369	(hasTyp (eAll, t', t);
27d9de59 AC	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)
234b917a	389	\| SOME t => checkTyp G t
27d9de59	390
492c1cff	391	val G' = bindVal G (x, t, NONE)
27d9de59 AC	392	val t' = checkExp G' e
	393	in
	394	(TArrow (t, t'), loc)
	395	end
	396	\| EVar x =>
234b917a	397	(case lookupVal G x of
27d9de59 AC	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
6be996d4 AC	409	(hasTyp (func, tf, (TArrow (dom, ran), loc));
6be996d4 AC	410	hasTyp (arg, ta, dom)
27d9de59 AC	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
db427c67 AC	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)
492c1cff	439	val G' = bindVal G (x, xt, NONE)
db427c67 AC	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' =>
234b917a	448	(subTyp (xt', xt)
db427c67 AC	449	handle Unify ue =>
	450	dte (WrongType ("Retrieved environment variable",
	451	(EVar x, loc),
	452	xt',
	453	xt,
	454	SOME ue));
	455	rt))
234b917a	456	\| (TError, _) => rt
db427c67 AC	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' =>
8a7c40fa AC	487	((case envVarSetFrom name e1 of
	488	NONE => subTyp (t, t')
	489	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	490	handle Unify ue =>
	491	dte (WrongType ("Shared environment variable",
	492	(EVar name, loc),
db427c67	493	t',
8a7c40fa	494	t,
db427c67 AC	495	SOME ue));
	496	d'))
	497	\| SOME t' =>
8a7c40fa AC	498	((case envVarSetFrom name e1 of
	499	NONE => subTyp (t, t')
	500	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	501	handle Unify ue =>
	502	dte (WrongType ("Shared environment variable",
	503	(EVar name, loc),
db427c67	504	t',
8a7c40fa	505	t,
db427c67 AC	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
234b917a	515	\| (TError, _) => t2
db427c67 AC	516	\| _ => (dte (WrongForm ("Action to be sequenced",
	517	"action",
	518	e2,
	519	t2,
	520	NONE));
	521	(TError, loc)))
234b917a	522	\| (TError, _) => t1
db427c67 AC	523	\| _ => (dte (WrongForm ("Action to be sequenced",
	524	"action",
	525	e1,
	526	t1,
	527	NONE));
	528	(TError, loc))
	529	end
	530
1a4e5a6c	531	\| ELocal (e1, e2) =>
db427c67	532	let
1a4e5a6c AC	533	val t1 = whnorm (checkExp G e1)
1a4e5a6c AC	534	val t2 = whnorm (checkExp G e2)
db427c67	535	in
1a4e5a6c AC	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' =>
8a7c40fa AC	549	((case envVarSetFrom name e1 of
	550	NONE => subTyp (t', t)
	551	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	552	handle Unify ue =>
	553	dte (WrongType ("Shared environment variable",
	554	(EVar name, loc),
1a4e5a6c	555	t',
8a7c40fa	556	t,
1a4e5a6c AC	557	SOME ue));
	558	d'))
	559	\| SOME t' =>
8a7c40fa AC	560	((case envVarSetFrom name e1 of
	561	NONE => subTyp (t', t)
	562	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	563	handle Unify ue =>
	564	dte (WrongType ("Shared environment variable",
	565	(EVar name, loc),
1a4e5a6c	566	t',
8a7c40fa	567	t,
1a4e5a6c AC	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",
db427c67	583	"action",
1a4e5a6c AC	584	e1,
1a4e5a6c AC	585	t1,
db427c67 AC	586	NONE));
	587	(TError, loc))
	588	end
234b917a	589
1a4e5a6c	590
234b917a AC	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
1a4e5a6c	597	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a AC	598	(case t2 of
	599	(TAction (p, d, r), _) =>
	600	if predImplies (pd, p) then
1a4e5a6c AC	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
234b917a AC	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)
27d9de59 AC	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
234b917a	652	\| TNested _ => tAll
27d9de59 AC	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)
234b917a	664	\| TNested _ => false
27d9de59 AC	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
234b917a AC	685	fun checkDecl G (d, _, loc) =
	686	case d of
	687	DExternType name => bindType G name
492c1cff AC	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
6be996d4	698	hasTyp (e, t, to)
492c1cff AC	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
095de39e	708	\| DContext name => bindContext G name
234b917a	709
095de39e	710	fun checkFile G tInit (_, ds, eo) =
234b917a AC	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
6be996d4	720	hasTyp (e, t, tInit)
234b917a AC	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
27d9de59	729	end