[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 hasTyp (e, t1, t2) =
    if (case baseCondition t2 of
	    NONE => false
	  | SOME rule => rule e) then
	()
    else
	subTyp (t1, t2)

fun checkPred G (p, loc) =
    let
	val err = ErrorMsg.error (SOME loc)
    in
	case p of
	    CRoot => ()
	  | CConst s =>
	    if lookupContext G s then
		()
	    else
		err ("Unbound context " ^ s)
	  | CPrefix p => checkPred G p
	  | CNot p => checkPred G p
	  | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
    end

fun checkTyp G (tAll as (t, loc)) =
    let
	val err = ErrorMsg.error (SOME loc)
    in
	case t of
	    TBase name =>
	    if lookupType G name then
		tAll
	    else
		(err ("Unbound type name " ^ name);
		 (TError, loc))
	  | TList t => (TList (checkTyp G t), loc)
	  | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
	  | TAction (p, d, r) => (checkPred G p;
				  (TAction (p, SM.map (checkTyp G) d,
					    SM.map (checkTyp G) r), loc))
	  | TNested (p, t) => (checkPred G p;
			       (TNested (p, checkTyp G t), loc))
	  | TError => raise Fail "TError in parser-generated type"
	  | TUnif _ => raise Fail "TUnif in parser-generated type"
    end

fun envVarSetFrom v (e, _) =
    case e of
	ESet (v', e) =>
	if v = v' then
	    SOME e
	else
	    NONE
      | EGet (_, _, e) => envVarSetFrom v e
      | ESeq es => foldr (fn (e, found) =>
			     case found of
				 SOME _ => found
			       | NONE => envVarSetFrom v e)
			 NONE es
      | ELocal (_, e) => envVarSetFrom v e

      | _ => NONE

fun checkExp G (eAll as (e, loc)) =
    let
	val dte = Describe.describe_type_error loc
    in
	case e of
	    EInt _ => (TBase "int", loc)
	  | EString _ => (TBase "string", loc)
	  | EList es =>
	    let
		val t = (newUnif (), loc)
	    in
		foldl (fn (e', ret) =>
			  let
			      val t' = checkExp G e'
			  in
			      (hasTyp (eAll, t', t);
			       if isError t' then
				   (TList (TError, loc), loc)
			       else
				   ret)
			      handle Unify ue =>
				     (dte (WrongType ("List element",
						      e',
						      t',
						      t,
						      SOME ue));
				      (TError, loc))
			  end) (TList t, loc) es
	    end

	  | ELam (x, to, e) =>
	    let
		val t =
		    case to of
			NONE => (newUnif (), loc)
		      | SOME t => checkTyp G t

		val G' = bindVal G (x, t, NONE)
		val t' = checkExp G' e
	    in
		(TArrow (t, t'), loc)
	    end
	  | EVar x =>
	    (case lookupVal G x of
		 NONE => (dte (UnboundVariable x);
			  (TError, loc))
	       | SOME t => t)
	  | EApp (func, arg) =>
	    let
		val dom = (newUnif (), loc)
		val ran = (newUnif (), loc)

		val tf = checkExp G func
		val ta = checkExp G arg
	    in
		(hasTyp (func, tf, (TArrow (dom, ran), loc));
		 hasTyp (arg, ta, dom)
		 handle Unify ue =>
			dte (WrongType ("Function argument",
					arg,
					ta,
					dom,
					SOME ue));
		 ran)
		handle Unify ue =>
		       (dte (WrongForm ("Function to be applied",
					"function",
					func,
					tf,
					SOME ue));
			(TError, loc))
	    end

	  | EALam (x, p, e) =>
	    let
		val p' = checkPred G p

		val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
		val t' = whnorm (checkExp G' e)
	    in
		case t' of
		    (TAction _, _) => (TNested (p, t'), loc)
		  | _ => (dte (WrongForm ("Body of nested configuration 'fn'",
					  "action",
					  e,
					  t',
					  NONE));
			  (TError, loc))
	    end

	  | ESet (evar, e) =>
	    let
		val t = checkExp G e
	    in
		(TAction ((CPrefix (CRoot, loc), loc),
			  SM.empty,
			  SM.insert (SM.empty, evar, t)),
		 loc)
	    end
	  | EGet (x, evar, rest) =>
	    let
		val xt = (newUnif (), loc)
		val G' = bindVal G (x, xt, NONE)

		val rt = whnorm (checkExp G' rest)
	    in
		case rt of
		    (TAction (p, d, r), _) =>
		    (case SM.find (d, evar) of
			 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
		       | SOME xt' =>
			 (subTyp (xt', xt)
				handle Unify ue =>
				       dte (WrongType ("Retrieved environment variable",
						       (EVar x, loc),
						       xt',
						       xt,
						       SOME ue));
			  rt))
		  | (TError, _) => rt
		  | _ => (dte (WrongForm ("Body of environment variable read",
					  "action",
					  rest,
					  rt,
					  NONE));
			  (TError, loc))
	    end

	  | ESeq [] => raise Fail "Empty ESeq"
	  | ESeq [e1] => checkExp G e1
	  | ESeq (e1 :: rest) =>
	    let
		val e2 = (ESeq rest, loc)

		val t1 = whnorm (checkExp G e1)
		val t2 = whnorm (checkExp G e2)
	    in
		case t1 of
		    (TAction (p1, d1, r1), _) =>
		    (case t2 of
			 (TAction (p2, d2, r2), _) =>
			 let
			     val p' = predSimpl (CAnd (p1, p2), loc)

			     val d' = SM.foldli (fn (name, t, d') =>
						    case SM.find (r1, name) of
							NONE =>
							(case SM.find (d', name) of
							     NONE => SM.insert (d', name, t)
							   | SOME t' =>
							     ((case envVarSetFrom name e1 of
								   NONE => subTyp (t, t')
								 | SOME e => hasTyp (e, t, t'))
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t',
										     t,
										     SOME ue));
							      d'))
						      | SOME t' =>
							((case envVarSetFrom name e1 of
								   NONE => subTyp (t, t')
								 | SOME e => hasTyp (e, t, t'))
							 handle Unify ue =>
								dte (WrongType ("Shared environment variable",
										(EVar name, loc),
										t',
										t,
										SOME ue));
							 d'))
						d1 d2

			     val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
						r1 r2
			 in
			     (TAction (p', d', r'), loc)
			 end
		       | (TError, _) => t2
		       | _ => (dte (WrongForm ("Action to be sequenced",
					       "action",
					       e2,
					       t2,
					       NONE));
			       (TError, loc)))
		  | (TError, _) => t1
		  | _ => (dte (WrongForm ("Action to be sequenced",
					  "action",
					  e1,
					  t1,
					  NONE));
			  (TError, loc))
	    end

	  | ELocal (e1, e2) =>
	    let
		val t1 = whnorm (checkExp G e1)
		val t2 = whnorm (checkExp G e2)
	    in
		case t1 of
		    (TAction (p1, d1, r1), _) =>
		    (case t2 of
			 (TAction (p2, d2, r2), _) =>
			 let
			     val p' = predSimpl (CAnd (p1, p2), loc)

			     val d' = SM.foldli (fn (name, t, d') =>
						    case SM.find (r1, name) of
							NONE =>
							(case SM.find (d', name) of
							     NONE => SM.insert (d', name, t)
							   | SOME t' =>
							     ((case envVarSetFrom name e1 of
								   NONE => subTyp (t', t)
								 | SOME e => hasTyp (e, t', t))
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t',
										     t,
										     SOME ue));
							      d'))
						      | SOME t' =>
							((case envVarSetFrom name e1 of
								   NONE => subTyp (t', t)
								 | SOME e => hasTyp (e, t', t))
							 handle Unify ue =>
								dte (WrongType ("Shared environment variable",
										(EVar name, loc),
										t',
										t,
										SOME ue));
							 d'))
						d1 d2
			 in
			     (TAction (p', d', r2), loc)
			 end
		       | (TError, _) => t2
		       | _ => (dte (WrongForm ("Action to be sequenced",
					       "action",
					       e2,
					       t2,
					       NONE));
			       (TError, loc)))
		  | (TError, _) => t1
		  | _ => (dte (WrongForm ("Action to be sequenced",
					  "action",
					  e1,
					  t1,
					  NONE));
			  (TError, loc))
	    end


	  | EWith (e1, e2) =>
	    let
		val t1 = whnorm (checkExp G e1)
		val t2 = whnorm (checkExp G e2)
	    in
		case t1 of
		    (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
		    (case t2 of
			 (TAction (p, d, r), _) =>
			 if predImplies (pd, p) then
			     let
				 val combineRecs =
				     SM.unionWithi (fn (name, t1, t2) =>
						       (subTyp (t1, t2)
							handle Unify ue =>
							       dte (WrongType ("Environment variable",
									       (EVar name, loc),
									       t1,
									       t2,
									       SOME ue));
							t2))
			     in
				 (TAction (pr, combineRecs (d, d1),
					   combineRecs (r, r1)), loc)
			     end
			 else
			     (dte (WrongPred ("nested action",
					      pd,
					      p));
			      (TError, loc))
		       | (TError, _) => t2
		       | _ =>
			 (dte (WrongForm ("Body of nested action",
					  "action",
					  e2,
					  t2,
					  NONE));
			  (TError, loc)))
		  | (TError, _) => t1
		  | _ =>
		    (dte (WrongForm ("Container of nested action",
				     "action",
				     e1,
				     t1,
				     NONE));
		     (TError, loc))
	    end

	  | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
			       SM.empty, SM.empty), loc)
    end

exception Ununif

fun ununif (tAll as (t, loc)) =
    case t of
	TBase _ => tAll
      | TList t => (TList (ununif t), loc)
      | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
      | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
      | TUnif (_, ref (SOME t)) => ununif t
      | TNested _ => tAll
      | TError => tAll

      | TUnif (_, ref NONE) => raise Ununif

fun hasError (t, _) =
    case t of
	TBase _ => false
      | TList t => hasError t
      | TArrow (d, r) => hasError d orelse hasError r
      | TAction (p, d, r) => List.exists hasError (SM.listItems d)
			     orelse List.exists hasError (SM.listItems r)
      | TNested _ => false
      | TError => false
      | TUnif (_, ref (SOME t)) => hasError t
      | TUnif (_, ref NONE) => false


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