[hcoop/zz_old/domtool2-proto.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
	    

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 Describe.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 simplifyKindOf e =
    case e of
	(EApp ((EVar s, _), e'), _) =>
	(case Env.function s of
	     NONE => e
	   | SOME f =>
	     case f [e'] of
		 NONE => e
	       | SOME e => e)
      | _ => e

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