[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

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
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
89c9edc9	27	val externFlag = ref false
	28	fun allowExterns () = externFlag := true
	29	fun disallowExterns () = externFlag := false
	30
64014a03	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
e680130a	94	\| (TNested (p1, q1), TNested (p2, q2)) =>
2dc33fa4	95	eqPred (p1, p2) andalso eqTy (q1, q2)
e680130a	96
64014a03	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
e680130a	117	\| WrongPred of string * pred * pred
64014a03	118
64014a03	119	fun describe_unification_error t ue =
	120	case ue of
	121	UnifyPred (p1, p2) =>
e680130a	122	(print "Reason: Incompatible contexts.\n";
64014a03	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")
e680130a	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))
64014a03	160
dbd7a7d2	161	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
64014a03	162	case (p1, p2) of
2dc33fa4	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
dbd7a7d2	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)
e680130a	174	\| (_, CPrefix p2) => predImplies (p1All, p2)
dbd7a7d2	175
dbd7a7d2	176	\| (CNot p1, CNot p2) => predImplies (p2, p1)
ff2a424a	177	\| (CRoot, CNot (CConst _, _)) => true
ff2a424a	178	\| (CConst s1, CNot (CConst s2, _)) => s1 <> s2
64014a03	179
dbd7a7d2	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'
2dc33fa4	197	else if predImplies (p1', p2') then
2dc33fa4	198	p1'
dbd7a7d2	199	else
	200	(CAnd (p1', p2'), loc)
	201	end
	202
e680130a	203	fun subPred (p1, p2) =
dbd7a7d2	204	if predImplies (p1, p2) then
	205	()
	206	else
	207	raise (Unify (UnifyPred (p1, p2)))
64014a03	208
e680130a	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
64014a03	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)
2dc33fa4	223	\| TNested (_, t) => occurs u t
64014a03	224	\| TError => false
	225	\| TUnif (_, ref (SOME t)) => occurs u t
	226	\| TUnif (_, u') => u = u'
	227
e680130a	228	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
64014a03	229	case (t1, t2) of
	230	(TBase s1, TBase s2) =>
	231	if s1 = s2 then
	232	()
	233	else
	234	raise Unify (UnifyTyp (t1All, t2All))
e680130a	235	\| (TList t1, TList t2) => subTyp (t1, t2)
64014a03	236	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
e680130a	237	(subTyp (d2, d1);
e680130a	238	subTyp (r1, r2))
64014a03	239
64014a03	240	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
e680130a	241	((subPred (p2, p1);
	242	subRecord subTyp (d2, d1);
	243	subRecord subTyp (r1, r2);
	244	subRecord subTyp (r2, r1))
64014a03	245	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
64014a03	246
e680130a	247	\| (TNested (d1, r1), TNested (d2, r2)) =>
e680130a	248	(subPred (d2, d1);
2dc33fa4	249	subTyp (r1, r2))
e680130a	250
	251	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	252	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
64014a03	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
dbd7a7d2	282	fun whnorm (tAll as (t, loc)) =
	283	case t of
	284	TUnif (_, ref (SOME tAll)) => whnorm tAll
	285	\| _ => tAll
	286
2f68506c	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
4264c8ef	297	fun hasTyp (e, t1, t2) =
2f68506c	298	if (case baseCondition t2 of
	299	NONE => false
	300	\| SOME rule => rule e) then
	301	()
	302	else
	303	subTyp (t1, t2)
4264c8ef	304
51c32b45	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
e680130a	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)
51c32b45	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))
e680130a	339	\| TError => raise Fail "TError in parser-generated type"
	340	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	341	end
	342
d68ab27c	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
64014a03	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
4264c8ef	375	(hasTyp (eAll, t', t);
64014a03	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)
e680130a	395	\| SOME t => checkTyp G t
64014a03	396
add6f172	397	val G' = bindVal G (x, t, NONE)
64014a03	398	val t' = checkExp G' e
	399	in
	400	(TArrow (t, t'), loc)
	401	end
	402	\| EVar x =>
e680130a	403	(case lookupVal G x of
64014a03	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
4264c8ef	415	(hasTyp (func, tf, (TArrow (dom, ran), loc));
4264c8ef	416	hasTyp (arg, ta, dom)
64014a03	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
dbd7a7d2	432
bf9b0bc3	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)
c720772b	438	val t' = whnorm (checkExp G' e)
bf9b0bc3	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
dbd7a7d2	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)
add6f172	462	val G' = bindVal G (x, xt, NONE)
dbd7a7d2	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' =>
e680130a	471	(subTyp (xt', xt)
dbd7a7d2	472	handle Unify ue =>
	473	dte (WrongType ("Retrieved environment variable",
	474	(EVar x, loc),
	475	xt',
	476	xt,
	477	SOME ue));
	478	rt))
e680130a	479	\| (TError, _) => rt
dbd7a7d2	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' =>
d68ab27c	510	((case envVarSetFrom name e1 of
	511	NONE => subTyp (t, t')
	512	\| SOME e => hasTyp (e, t, t'))
dbd7a7d2	513	handle Unify ue =>
	514	dte (WrongType ("Shared environment variable",
	515	(EVar name, loc),
dbd7a7d2	516	t',
d68ab27c	517	t,
dbd7a7d2	518	SOME ue));
	519	d'))
	520	\| SOME t' =>
d68ab27c	521	((case envVarSetFrom name e1 of
	522	NONE => subTyp (t, t')
	523	\| SOME e => hasTyp (e, t, t'))
dbd7a7d2	524	handle Unify ue =>
	525	dte (WrongType ("Shared environment variable",
	526	(EVar name, loc),
dbd7a7d2	527	t',
d68ab27c	528	t,
dbd7a7d2	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
e680130a	538	\| (TError, _) => t2
dbd7a7d2	539	\| _ => (dte (WrongForm ("Action to be sequenced",
	540	"action",
	541	e2,
	542	t2,
	543	NONE));
	544	(TError, loc)))
e680130a	545	\| (TError, _) => t1
dbd7a7d2	546	\| _ => (dte (WrongForm ("Action to be sequenced",
	547	"action",
	548	e1,
	549	t1,
	550	NONE));
	551	(TError, loc))
	552	end
	553
2dc33fa4	554	\| ELocal (e1, e2) =>
dbd7a7d2	555	let
2dc33fa4	556	val t1 = whnorm (checkExp G e1)
2dc33fa4	557	val t2 = whnorm (checkExp G e2)
dbd7a7d2	558	in
2dc33fa4	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' =>
d68ab27c	572	((case envVarSetFrom name e1 of
	573	NONE => subTyp (t', t)
	574	\| SOME e => hasTyp (e, t', t))
2dc33fa4	575	handle Unify ue =>
	576	dte (WrongType ("Shared environment variable",
	577	(EVar name, loc),
2dc33fa4	578	t',
d68ab27c	579	t,
2dc33fa4	580	SOME ue));
	581	d'))
	582	\| SOME t' =>
d68ab27c	583	((case envVarSetFrom name e1 of
	584	NONE => subTyp (t', t)
	585	\| SOME e => hasTyp (e, t', t))
2dc33fa4	586	handle Unify ue =>
	587	dte (WrongType ("Shared environment variable",
	588	(EVar name, loc),
2dc33fa4	589	t',
d68ab27c	590	t,
2dc33fa4	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",
dbd7a7d2	606	"action",
2dc33fa4	607	e1,
2dc33fa4	608	t1,
dbd7a7d2	609	NONE));
	610	(TError, loc))
	611	end
e680130a	612
2dc33fa4	613
e680130a	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
2dc33fa4	620	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
e680130a	621	(case t2 of
	622	(TAction (p, d, r), _) =>
	623	if predImplies (pd, p) then
2dc33fa4	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
e680130a	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)
64014a03	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
e680130a	675	\| TNested _ => tAll
64014a03	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)
e680130a	687	\| TNested _ => false
64014a03	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
e680130a	708	fun checkDecl G (d, _, loc) =
e680130a	709	case d of
89c9edc9	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)
add6f172	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
4264c8ef	731	hasTyp (e, t, to)
add6f172	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
51c32b45	741	\| DContext name => bindContext G name
e680130a	742
51c32b45	743	fun checkFile G tInit (_, ds, eo) =
e680130a	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
4264c8ef	753	hasTyp (e, t, tInit)
e680130a	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
64014a03	762	end