[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
	    

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
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
27d9de59	50
db427c67	51	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
27d9de59	52	case (p1, p2) of
1a4e5a6c AC	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
db427c67 AC	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)
234b917a	64	\| (_, CPrefix p2) => predImplies (p1All, p2)
db427c67 AC	65
db427c67 AC	66	\| (CNot p1, CNot p2) => predImplies (p2, p1)
2882ee37 AC	67	\| (CRoot, CNot (CConst _, _)) => true
2882ee37 AC	68	\| (CConst s1, CNot (CConst s2, _)) => s1 <> s2
27d9de59	69
db427c67 AC	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'
1a4e5a6c AC	87	else if predImplies (p1', p2') then
1a4e5a6c AC	88	p1'
db427c67 AC	89	else
	90	(CAnd (p1', p2'), loc)
	91	end
	92
234b917a	93	fun subPred (p1, p2) =
db427c67 AC	94	if predImplies (p1, p2) then
	95	()
	96	else
	97	raise (Unify (UnifyPred (p1, p2)))
27d9de59	98
234b917a AC	99	fun subRecord f (r1, r2) =
	100	SM.appi (fn (k, v2) =>
	101	case SM.find (r1, k) of
9b7ee2b2	102	NONE => raise Describe.UnequalDomains
234b917a	103	\| SOME v1 => f (v1, v2)) r2
27d9de59 AC	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)
1a4e5a6c	113	\| TNested (_, t) => occurs u t
27d9de59 AC	114	\| TError => false
	115	\| TUnif (_, ref (SOME t)) => occurs u t
	116	\| TUnif (_, u') => u = u'
	117
234b917a	118	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
27d9de59 AC	119	case (t1, t2) of
	120	(TBase s1, TBase s2) =>
	121	if s1 = s2 then
	122	()
	123	else
	124	raise Unify (UnifyTyp (t1All, t2All))
234b917a	125	\| (TList t1, TList t2) => subTyp (t1, t2)
27d9de59	126	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
234b917a AC	127	(subTyp (d2, d1);
234b917a AC	128	subTyp (r1, r2))
27d9de59 AC	129
27d9de59 AC	130	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
234b917a AC	131	((subPred (p2, p1);
	132	subRecord subTyp (d2, d1);
	133	subRecord subTyp (r1, r2);
	134	subRecord subTyp (r2, r1))
27d9de59 AC	135	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
27d9de59 AC	136
234b917a AC	137	\| (TNested (d1, r1), TNested (d2, r2)) =>
234b917a AC	138	(subPred (d2, d1);
1a4e5a6c	139	subTyp (r1, r2))
234b917a AC	140
	141	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	142	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
27d9de59 AC	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
db427c67 AC	172	fun whnorm (tAll as (t, loc)) =
	173	case t of
	174	TUnif (_, ref (SOME tAll)) => whnorm tAll
	175	\| _ => tAll
	176
629a34f6 AC	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
4ecbfd4c AC	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
6be996d4	198	fun hasTyp (e, t1, t2) =
629a34f6 AC	199	if (case baseCondition t2 of
629a34f6 AC	200	NONE => false
4ecbfd4c	201	\| SOME rule => rule (simplifyKindOf e)) then
629a34f6 AC	202	()
	203	else
	204	subTyp (t1, t2)
6be996d4	205
095de39e AC	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
234b917a AC	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)
095de39e AC	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))
234b917a AC	240	\| TError => raise Fail "TError in parser-generated type"
	241	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	242	end
	243
8a7c40fa AC	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
27d9de59 AC	261	fun checkExp G (eAll as (e, loc)) =
27d9de59 AC	262	let
e1b99e23	263	val dte = Describe.describe_type_error loc
27d9de59 AC	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
6be996d4	276	(hasTyp (eAll, t', t);
27d9de59 AC	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)
234b917a	296	\| SOME t => checkTyp G t
27d9de59	297
492c1cff	298	val G' = bindVal G (x, t, NONE)
27d9de59 AC	299	val t' = checkExp G' e
	300	in
	301	(TArrow (t, t'), loc)
	302	end
	303	\| EVar x =>
234b917a	304	(case lookupVal G x of
27d9de59 AC	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
6be996d4 AC	316	(hasTyp (func, tf, (TArrow (dom, ran), loc));
6be996d4 AC	317	hasTyp (arg, ta, dom)
27d9de59 AC	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
db427c67	333
6bb366c5 AC	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)
cdb376d4	339	val t' = whnorm (checkExp G' e)
6bb366c5 AC	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
db427c67 AC	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)
492c1cff	363	val G' = bindVal G (x, xt, NONE)
db427c67 AC	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' =>
234b917a	372	(subTyp (xt', xt)
db427c67 AC	373	handle Unify ue =>
	374	dte (WrongType ("Retrieved environment variable",
	375	(EVar x, loc),
	376	xt',
	377	xt,
	378	SOME ue));
	379	rt))
234b917a	380	\| (TError, _) => rt
db427c67 AC	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' =>
8a7c40fa AC	411	((case envVarSetFrom name e1 of
	412	NONE => subTyp (t, t')
	413	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	414	handle Unify ue =>
	415	dte (WrongType ("Shared environment variable",
	416	(EVar name, loc),
db427c67	417	t',
8a7c40fa	418	t,
db427c67 AC	419	SOME ue));
	420	d'))
	421	\| SOME t' =>
8a7c40fa AC	422	((case envVarSetFrom name e1 of
	423	NONE => subTyp (t, t')
	424	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	425	handle Unify ue =>
	426	dte (WrongType ("Shared environment variable",
	427	(EVar name, loc),
db427c67	428	t',
8a7c40fa	429	t,
db427c67 AC	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
234b917a	439	\| (TError, _) => t2
db427c67 AC	440	\| _ => (dte (WrongForm ("Action to be sequenced",
	441	"action",
	442	e2,
	443	t2,
	444	NONE));
	445	(TError, loc)))
234b917a	446	\| (TError, _) => t1
db427c67 AC	447	\| _ => (dte (WrongForm ("Action to be sequenced",
	448	"action",
	449	e1,
	450	t1,
	451	NONE));
	452	(TError, loc))
	453	end
	454
1a4e5a6c	455	\| ELocal (e1, e2) =>
db427c67	456	let
1a4e5a6c AC	457	val t1 = whnorm (checkExp G e1)
1a4e5a6c AC	458	val t2 = whnorm (checkExp G e2)
db427c67	459	in
1a4e5a6c AC	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' =>
8a7c40fa AC	473	((case envVarSetFrom name e1 of
	474	NONE => subTyp (t', t)
	475	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	476	handle Unify ue =>
	477	dte (WrongType ("Shared environment variable",
	478	(EVar name, loc),
1a4e5a6c	479	t',
8a7c40fa	480	t,
1a4e5a6c AC	481	SOME ue));
	482	d'))
	483	\| SOME t' =>
8a7c40fa AC	484	((case envVarSetFrom name e1 of
	485	NONE => subTyp (t', t)
	486	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	487	handle Unify ue =>
	488	dte (WrongType ("Shared environment variable",
	489	(EVar name, loc),
1a4e5a6c	490	t',
8a7c40fa	491	t,
1a4e5a6c AC	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",
db427c67	507	"action",
1a4e5a6c AC	508	e1,
1a4e5a6c AC	509	t1,
db427c67 AC	510	NONE));
	511	(TError, loc))
	512	end
234b917a	513
1a4e5a6c	514
234b917a AC	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
1a4e5a6c	521	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a AC	522	(case t2 of
	523	(TAction (p, d, r), _) =>
	524	if predImplies (pd, p) then
1a4e5a6c AC	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
234b917a AC	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)
27d9de59 AC	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
234b917a	576	\| TNested _ => tAll
27d9de59 AC	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)
234b917a	588	\| TNested _ => false
27d9de59 AC	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:";
9b7ee2b2	605	output (p_typ t);
27d9de59 AC	606	t)
	607	end
	608
234b917a AC	609	fun checkDecl G (d, _, loc) =
234b917a AC	610	case d of
b3159a70 AC	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)
492c1cff AC	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
6be996d4	632	hasTyp (e, t, to)
492c1cff	633	handle Unify ue =>
e1b99e23 AC	634	Describe.describe_type_error loc
	635	(WrongType ("Bound value",
	636	e,
	637	t,
	638	to,
	639	SOME ue));
492c1cff AC	640	bindVal G (name, to, SOME e)
492c1cff AC	641	end
095de39e	642	\| DContext name => bindContext G name
234b917a	643
095de39e	644	fun checkFile G tInit (_, ds, eo) =
234b917a AC	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
6be996d4	654	hasTyp (e, t, tInit)
234b917a AC	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
27d9de59	663	end