[hcoop/zz_old/domtool2-proto.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
64014a03	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.
ae3a5b8c	17	*)
64014a03	18
	19	(* Domtool configuration language type checking *)
	20
	21	structure Tycheck :> TYCHECK = struct
	22
add6f172	23	open Ast Print Env
64014a03	24
	25	structure SM = StringMap
	26
64014a03	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
e680130a	90	\| (TNested (p1, q1), TNested (p2, q2)) =>
2dc33fa4	91	eqPred (p1, p2) andalso eqTy (q1, q2)
e680130a	92
64014a03	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
e680130a	113	\| WrongPred of string * pred * pred
64014a03	114
64014a03	115	fun describe_unification_error t ue =
	116	case ue of
	117	UnifyPred (p1, p2) =>
e680130a	118	(print "Reason: Incompatible contexts.\n";
64014a03	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")
e680130a	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))
64014a03	156
dbd7a7d2	157	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
64014a03	158	case (p1, p2) of
2dc33fa4	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
dbd7a7d2	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)
e680130a	170	\| (_, CPrefix p2) => predImplies (p1All, p2)
dbd7a7d2	171
dbd7a7d2	172	\| (CNot p1, CNot p2) => predImplies (p2, p1)
64014a03	173
dbd7a7d2	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'
2dc33fa4	191	else if predImplies (p1', p2') then
2dc33fa4	192	p1'
dbd7a7d2	193	else
	194	(CAnd (p1', p2'), loc)
	195	end
	196
e680130a	197	fun subPred (p1, p2) =
dbd7a7d2	198	if predImplies (p1, p2) then
	199	()
	200	else
	201	raise (Unify (UnifyPred (p1, p2)))
64014a03	202
e680130a	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
64014a03	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)
2dc33fa4	217	\| TNested (_, t) => occurs u t
64014a03	218	\| TError => false
	219	\| TUnif (_, ref (SOME t)) => occurs u t
	220	\| TUnif (_, u') => u = u'
	221
e680130a	222	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
64014a03	223	case (t1, t2) of
	224	(TBase s1, TBase s2) =>
	225	if s1 = s2 then
	226	()
	227	else
	228	raise Unify (UnifyTyp (t1All, t2All))
e680130a	229	\| (TList t1, TList t2) => subTyp (t1, t2)
64014a03	230	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
e680130a	231	(subTyp (d2, d1);
e680130a	232	subTyp (r1, r2))
64014a03	233
64014a03	234	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
e680130a	235	((subPred (p2, p1);
	236	subRecord subTyp (d2, d1);
	237	subRecord subTyp (r1, r2);
	238	subRecord subTyp (r2, r1))
64014a03	239	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
64014a03	240
e680130a	241	\| (TNested (d1, r1), TNested (d2, r2)) =>
e680130a	242	(subPred (d2, d1);
2dc33fa4	243	subTyp (r1, r2))
e680130a	244
	245	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	246	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
64014a03	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
dbd7a7d2	276	fun whnorm (tAll as (t, loc)) =
	277	case t of
	278	TUnif (_, ref (SOME tAll)) => whnorm tAll
	279	\| _ => tAll
	280
2f68506c	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
4264c8ef	291	fun hasTyp (e, t1, t2) =
2f68506c	292	if (case baseCondition t2 of
	293	NONE => false
	294	\| SOME rule => rule e) then
	295	()
	296	else
	297	subTyp (t1, t2)
4264c8ef	298
51c32b45	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
e680130a	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)
51c32b45	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))
e680130a	333	\| TError => raise Fail "TError in parser-generated type"
	334	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	335	end
	336
64014a03	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
4264c8ef	352	(hasTyp (eAll, t', t);
64014a03	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)
e680130a	372	\| SOME t => checkTyp G t
64014a03	373
add6f172	374	val G' = bindVal G (x, t, NONE)
64014a03	375	val t' = checkExp G' e
	376	in
	377	(TArrow (t, t'), loc)
	378	end
	379	\| EVar x =>
e680130a	380	(case lookupVal G x of
64014a03	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
4264c8ef	392	(hasTyp (func, tf, (TArrow (dom, ran), loc));
4264c8ef	393	hasTyp (arg, ta, dom)
64014a03	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
dbd7a7d2	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)
add6f172	422	val G' = bindVal G (x, xt, NONE)
dbd7a7d2	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' =>
e680130a	431	(subTyp (xt', xt)
dbd7a7d2	432	handle Unify ue =>
	433	dte (WrongType ("Retrieved environment variable",
	434	(EVar x, loc),
	435	xt',
	436	xt,
	437	SOME ue));
	438	rt))
e680130a	439	\| (TError, _) => rt
dbd7a7d2	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' =>
e680130a	470	(subTyp (t, t')
dbd7a7d2	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' =>
e680130a	479	(subTyp (t, t')
dbd7a7d2	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
e680130a	494	\| (TError, _) => t2
dbd7a7d2	495	\| _ => (dte (WrongForm ("Action to be sequenced",
	496	"action",
	497	e2,
	498	t2,
	499	NONE));
	500	(TError, loc)))
e680130a	501	\| (TError, _) => t1
dbd7a7d2	502	\| _ => (dte (WrongForm ("Action to be sequenced",
	503	"action",
	504	e1,
	505	t1,
	506	NONE));
	507	(TError, loc))
	508	end
	509
2dc33fa4	510	\| ELocal (e1, e2) =>
dbd7a7d2	511	let
2dc33fa4	512	val t1 = whnorm (checkExp G e1)
2dc33fa4	513	val t2 = whnorm (checkExp G e2)
dbd7a7d2	514	in
2dc33fa4	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",
dbd7a7d2	558	"action",
2dc33fa4	559	e1,
2dc33fa4	560	t1,
dbd7a7d2	561	NONE));
	562	(TError, loc))
	563	end
e680130a	564
2dc33fa4	565
e680130a	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
2dc33fa4	572	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
e680130a	573	(case t2 of
	574	(TAction (p, d, r), _) =>
	575	if predImplies (pd, p) then
2dc33fa4	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
e680130a	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)
64014a03	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
e680130a	627	\| TNested _ => tAll
64014a03	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)
e680130a	639	\| TNested _ => false
64014a03	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
e680130a	660	fun checkDecl G (d, _, loc) =
	661	case d of
	662	DExternType name => bindType G name
add6f172	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
4264c8ef	673	hasTyp (e, t, to)
add6f172	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
51c32b45	683	\| DContext name => bindContext G name
e680130a	684
51c32b45	685	fun checkFile G tInit (_, ds, eo) =
e680130a	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
4264c8ef	695	hasTyp (e, t, tInit)
e680130a	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
64014a03	704	end