[hcoop/domtool2.git] / src / tycheck.sml

(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006-2007, 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

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