[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 ununify (tAll as (t, _)) =
    case t of
	TUnif (_, ref (SOME t)) => ununify t
      | _ => tAll

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, topt, evar, rest) =>
	    let
		val xt = (newUnif (), loc)
		val G' = bindVal G (x, xt, NONE)

		val rt = whnorm (checkExp G' rest)
	    in
		case topt of
		    NONE => ()
		  | SOME t => subTyp (xt, checkTyp G t);

		case ununify 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
8cbb9632	251	\| EGet (_, _, _, e) => envVarSetFrom v e
8a7c40fa AC	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
8cbb9632 AC	261	fun ununify (tAll as (t, _)) =
	262	case t of
	263	TUnif (_, ref (SOME t)) => ununify t
	264	\| _ => tAll
	265
27d9de59 AC	266	fun checkExp G (eAll as (e, loc)) =
27d9de59 AC	267	let
e1b99e23	268	val dte = Describe.describe_type_error loc
27d9de59 AC	269	in
	270	case e of
	271	EInt _ => (TBase "int", loc)
	272	\| EString _ => (TBase "string", loc)
	273	\| EList es =>
	274	let
	275	val t = (newUnif (), loc)
	276	in
	277	foldl (fn (e', ret) =>
	278	let
	279	val t' = checkExp G e'
	280	in
6be996d4	281	(hasTyp (eAll, t', t);
27d9de59 AC	282	if isError t' then
	283	(TList (TError, loc), loc)
	284	else
	285	ret)
	286	handle Unify ue =>
	287	(dte (WrongType ("List element",
	288	e',
	289	t',
	290	t,
	291	SOME ue));
	292	(TError, loc))
	293	end) (TList t, loc) es
	294	end
	295
	296	\| ELam (x, to, e) =>
	297	let
	298	val t =
	299	case to of
	300	NONE => (newUnif (), loc)
234b917a	301	\| SOME t => checkTyp G t
27d9de59	302
492c1cff	303	val G' = bindVal G (x, t, NONE)
27d9de59 AC	304	val t' = checkExp G' e
	305	in
	306	(TArrow (t, t'), loc)
	307	end
	308	\| EVar x =>
234b917a	309	(case lookupVal G x of
27d9de59 AC	310	NONE => (dte (UnboundVariable x);
	311	(TError, loc))
	312	\| SOME t => t)
	313	\| EApp (func, arg) =>
	314	let
	315	val dom = (newUnif (), loc)
	316	val ran = (newUnif (), loc)
	317
	318	val tf = checkExp G func
	319	val ta = checkExp G arg
	320	in
6be996d4 AC	321	(hasTyp (func, tf, (TArrow (dom, ran), loc));
6be996d4 AC	322	hasTyp (arg, ta, dom)
27d9de59 AC	323	handle Unify ue =>
	324	dte (WrongType ("Function argument",
	325	arg,
	326	ta,
	327	dom,
	328	SOME ue));
	329	ran)
	330	handle Unify ue =>
	331	(dte (WrongForm ("Function to be applied",
	332	"function",
	333	func,
	334	tf,
	335	SOME ue));
	336	(TError, loc))
	337	end
db427c67	338
6bb366c5 AC	339	\| EALam (x, p, e) =>
	340	let
	341	val p' = checkPred G p
	342
	343	val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
cdb376d4	344	val t' = whnorm (checkExp G' e)
6bb366c5 AC	345	in
	346	case t' of
	347	(TAction _, _) => (TNested (p, t'), loc)
	348	\| _ => (dte (WrongForm ("Body of nested configuration 'fn'",
	349	"action",
	350	e,
	351	t',
	352	NONE));
	353	(TError, loc))
	354	end
	355
db427c67 AC	356	\| ESet (evar, e) =>
	357	let
	358	val t = checkExp G e
	359	in
	360	(TAction ((CPrefix (CRoot, loc), loc),
	361	SM.empty,
	362	SM.insert (SM.empty, evar, t)),
	363	loc)
	364	end
8cbb9632	365	\| EGet (x, topt, evar, rest) =>
db427c67 AC	366	let
db427c67 AC	367	val xt = (newUnif (), loc)
492c1cff	368	val G' = bindVal G (x, xt, NONE)
db427c67 AC	369
	370	val rt = whnorm (checkExp G' rest)
	371	in
8cbb9632 AC	372	case topt of
	373	NONE => ()
	374	\| SOME t => subTyp (xt, checkTyp G t);
	375
	376	case ununify rt of
db427c67 AC	377	(TAction (p, d, r), _) =>
	378	(case SM.find (d, evar) of
	379	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	380	\| SOME xt' =>
234b917a	381	(subTyp (xt', xt)
db427c67 AC	382	handle Unify ue =>
	383	dte (WrongType ("Retrieved environment variable",
	384	(EVar x, loc),
	385	xt',
	386	xt,
	387	SOME ue));
	388	rt))
234b917a	389	\| (TError, _) => rt
db427c67 AC	390	\| _ => (dte (WrongForm ("Body of environment variable read",
	391	"action",
	392	rest,
	393	rt,
	394	NONE));
	395	(TError, loc))
	396	end
	397
	398	\| ESeq [] => raise Fail "Empty ESeq"
	399	\| ESeq [e1] => checkExp G e1
	400	\| ESeq (e1 :: rest) =>
	401	let
	402	val e2 = (ESeq rest, loc)
	403
	404	val t1 = whnorm (checkExp G e1)
	405	val t2 = whnorm (checkExp G e2)
	406	in
	407	case t1 of
	408	(TAction (p1, d1, r1), _) =>
	409	(case t2 of
	410	(TAction (p2, d2, r2), _) =>
	411	let
	412	val p' = predSimpl (CAnd (p1, p2), loc)
	413
	414	val d' = SM.foldli (fn (name, t, d') =>
	415	case SM.find (r1, name) of
	416	NONE =>
	417	(case SM.find (d', name) of
	418	NONE => SM.insert (d', name, t)
	419	\| SOME t' =>
8a7c40fa AC	420	((case envVarSetFrom name e1 of
	421	NONE => subTyp (t, t')
	422	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	423	handle Unify ue =>
	424	dte (WrongType ("Shared environment variable",
	425	(EVar name, loc),
db427c67	426	t',
8a7c40fa	427	t,
db427c67 AC	428	SOME ue));
	429	d'))
	430	\| SOME t' =>
8a7c40fa AC	431	((case envVarSetFrom name e1 of
	432	NONE => subTyp (t, t')
	433	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	434	handle Unify ue =>
	435	dte (WrongType ("Shared environment variable",
	436	(EVar name, loc),
db427c67	437	t',
8a7c40fa	438	t,
db427c67 AC	439	SOME ue));
	440	d'))
	441	d1 d2
	442
	443	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	444	r1 r2
	445	in
	446	(TAction (p', d', r'), loc)
	447	end
234b917a	448	\| (TError, _) => t2
db427c67 AC	449	\| _ => (dte (WrongForm ("Action to be sequenced",
	450	"action",
	451	e2,
	452	t2,
	453	NONE));
	454	(TError, loc)))
234b917a	455	\| (TError, _) => t1
db427c67 AC	456	\| _ => (dte (WrongForm ("Action to be sequenced",
	457	"action",
	458	e1,
	459	t1,
	460	NONE));
	461	(TError, loc))
	462	end
	463
1a4e5a6c	464	\| ELocal (e1, e2) =>
db427c67	465	let
1a4e5a6c AC	466	val t1 = whnorm (checkExp G e1)
1a4e5a6c AC	467	val t2 = whnorm (checkExp G e2)
db427c67	468	in
1a4e5a6c AC	469	case t1 of
	470	(TAction (p1, d1, r1), _) =>
	471	(case t2 of
	472	(TAction (p2, d2, r2), _) =>
	473	let
	474	val p' = predSimpl (CAnd (p1, p2), loc)
	475
	476	val d' = SM.foldli (fn (name, t, d') =>
	477	case SM.find (r1, name) of
	478	NONE =>
	479	(case SM.find (d', name) of
	480	NONE => SM.insert (d', name, t)
	481	\| SOME t' =>
8a7c40fa AC	482	((case envVarSetFrom name e1 of
	483	NONE => subTyp (t', t)
	484	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	485	handle Unify ue =>
	486	dte (WrongType ("Shared environment variable",
	487	(EVar name, loc),
1a4e5a6c	488	t',
8a7c40fa	489	t,
1a4e5a6c AC	490	SOME ue));
	491	d'))
	492	\| SOME t' =>
8a7c40fa AC	493	((case envVarSetFrom name e1 of
	494	NONE => subTyp (t', t)
	495	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	496	handle Unify ue =>
	497	dte (WrongType ("Shared environment variable",
	498	(EVar name, loc),
1a4e5a6c	499	t',
8a7c40fa	500	t,
1a4e5a6c AC	501	SOME ue));
	502	d'))
	503	d1 d2
	504	in
	505	(TAction (p', d', r2), loc)
	506	end
	507	\| (TError, _) => t2
	508	\| _ => (dte (WrongForm ("Action to be sequenced",
	509	"action",
	510	e2,
	511	t2,
	512	NONE));
	513	(TError, loc)))
	514	\| (TError, _) => t1
	515	\| _ => (dte (WrongForm ("Action to be sequenced",
db427c67	516	"action",
1a4e5a6c AC	517	e1,
1a4e5a6c AC	518	t1,
db427c67 AC	519	NONE));
	520	(TError, loc))
	521	end
234b917a	522
1a4e5a6c	523
234b917a AC	524	\| EWith (e1, e2) =>
	525	let
	526	val t1 = whnorm (checkExp G e1)
	527	val t2 = whnorm (checkExp G e2)
	528	in
	529	case t1 of
1a4e5a6c	530	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a AC	531	(case t2 of
	532	(TAction (p, d, r), _) =>
	533	if predImplies (pd, p) then
1a4e5a6c AC	534	let
	535	val combineRecs =
	536	SM.unionWithi (fn (name, t1, t2) =>
	537	(subTyp (t1, t2)
	538	handle Unify ue =>
	539	dte (WrongType ("Environment variable",
	540	(EVar name, loc),
	541	t1,
	542	t2,
	543	SOME ue));
	544	t2))
	545	in
	546	(TAction (pr, combineRecs (d, d1),
	547	combineRecs (r, r1)), loc)
	548	end
234b917a AC	549	else
	550	(dte (WrongPred ("nested action",
	551	pd,
	552	p));
	553	(TError, loc))
	554	\| (TError, _) => t2
	555	\| _ =>
	556	(dte (WrongForm ("Body of nested action",
	557	"action",
	558	e2,
	559	t2,
	560	NONE));
	561	(TError, loc)))
	562	\| (TError, _) => t1
	563	\| _ =>
	564	(dte (WrongForm ("Container of nested action",
	565	"action",
	566	e1,
	567	t1,
	568	NONE));
	569	(TError, loc))
	570	end
	571
	572	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	573	SM.empty, SM.empty), loc)
27d9de59 AC	574	end
	575
	576	exception Ununif
	577
	578	fun ununif (tAll as (t, loc)) =
	579	case t of
	580	TBase _ => tAll
	581	\| TList t => (TList (ununif t), loc)
	582	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	583	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	584	\| TUnif (_, ref (SOME t)) => ununif t
234b917a	585	\| TNested _ => tAll
27d9de59 AC	586	\| TError => tAll
	587
	588	\| TUnif (_, ref NONE) => raise Ununif
	589
	590	fun hasError (t, _) =
	591	case t of
	592	TBase _ => false
	593	\| TList t => hasError t
	594	\| TArrow (d, r) => hasError d orelse hasError r
	595	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	596	orelse List.exists hasError (SM.listItems r)
234b917a	597	\| TNested _ => false
27d9de59 AC	598	\| TError => false
	599	\| TUnif (_, ref (SOME t)) => hasError t
	600	\| TUnif (_, ref NONE) => false
	601
	602
	603	fun checkUnit G (eAll as (_, loc)) =
	604	let
	605	val _ = resetUnif ()
	606	val t = checkExp G eAll
	607	in
	608	if hasError t then
	609	t
	610	else
	611	ununif t
	612	handle Ununif =>
	613	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
9b7ee2b2	614	output (p_typ t);
27d9de59 AC	615	t)
	616	end
	617
234b917a AC	618	fun checkDecl G (d, _, loc) =
234b917a AC	619	case d of
b3159a70 AC	620	DExternType name =>
	621	if !externFlag then
	622	bindType G name
	623	else
	624	(ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
	625	G)
	626	\| DExternVal (name, t) =>
	627	if !externFlag then
	628	bindVal G (name, checkTyp G t, NONE)
	629	else
	630	(ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
	631	G)
492c1cff AC	632	\| DVal (name, to, e) =>
	633	let
	634	val to =
	635	case to of
	636	NONE => (newUnif (), loc)
	637	\| SOME to => checkTyp G to
	638
	639	val t = checkExp G e
	640	in
6be996d4	641	hasTyp (e, t, to)
492c1cff	642	handle Unify ue =>
e1b99e23 AC	643	Describe.describe_type_error loc
	644	(WrongType ("Bound value",
	645	e,
	646	t,
	647	to,
	648	SOME ue));
492c1cff AC	649	bindVal G (name, to, SOME e)
492c1cff AC	650	end
095de39e	651	\| DContext name => bindContext G name
234b917a	652
095de39e	653	fun checkFile G tInit (_, ds, eo) =
234b917a AC	654	let
	655	val G' = foldl (fn (d, G) => checkDecl G d) G ds
	656	in
	657	case eo of
	658	NONE => ()
	659	\| SOME (e as (_, loc)) =>
	660	let
	661	val t = checkExp G' e
	662	in
6be996d4	663	hasTyp (e, t, tInit)
234b917a AC	664	handle Unify ue =>
	665	(ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
	666	preface ("Actual:", p_typ t);
	667	preface ("Needed:", p_typ tInit))
	668	end;
	669	G'
	670	end
	671
27d9de59	672	end