[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

val externFlag = ref false
fun allowExterns () = externFlag := true
fun disallowExterns () = externFlag := false

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)
      | (CRoot, CNot (CConst _, _)) => true
      | (CConst s1, CNot (CConst s2, _)) => s1 <> s2

      | _ => 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

	  | EALam (x, p, e) =>
	    let
		val p' = checkPred G p

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