[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

val ununify = Describe.ununify

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 ("First action to be sequenced",
					       "action",
					       e2,
					       t2,
					       NONE));
			       (TError, loc)))
		  | (TError, _) => t1
		  | _ => (dte (WrongForm ("Second 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 ("Body of local settings",
					       "action",
					       e2,
					       t2,
					       NONE));
			       (TError, loc)))
		  | (TError, _) => t1
		  | _ => (dte (WrongForm ("Local settings",
					  "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)

	  | EIf (e1, e2, e3) =>
	    let
		val t1 = checkExp G e1
		val t2 = checkExp G e2
		val t3 = checkExp G e3
		val bool = (TBase "bool", loc)
	    in
		(subTyp (t1, bool))
		handle Unify ue =>
		       dte (WrongType ("\"if\" test",
				       e1,
				       t1,
				       bool,
				       SOME ue));
		(subTyp (t2, t3); t3)
		       handle Unify _ =>
			      ((subTyp (t3, t2); t2)
			       handle Unify ue =>
				      (dte (WrongType ("\"else\" case",
						       eAll,
						       t3,
						       t2,
						       SOME ue));
				       (TError, loc)))
	    end
    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 printActionDiffs {have, need} =
    case (ununif have, ununif need) of
	((TAction (p1, in1, out1), loc), (TAction (p2, in2, out2), _)) =>
	let
	    fun checkPreds () =
		if predImplies (p1, p2) then
		    ()
		else
		    (ErrorMsg.error (SOME loc) "Files provides the wrong kind of configuration.";
		     preface ("Have:", p_pred p1);
		     preface ("Need:", p_pred p2))

	    fun checkIn () =
		SM.appi (fn (name, t) =>
			    case SM.find (in2, name) of
				NONE => (ErrorMsg.error (SOME loc) "An unavailable environment variable is used.";
					 print ("Name: " ^ name ^ "\n");
					 preface ("Type:", p_typ t))
			      | SOME t' =>
				subTyp (t', t)
				handle Unify _ =>
				       (ErrorMsg.error (SOME loc) "Wrong type for environment variable.";
					print ("          Name: " ^ name ^ "\n");
					preface ("      Has type:", p_typ t');
					preface ("Used with type:", p_typ t)))
			in1
			
	    fun checkOut () =
		SM.appi (fn (name, t) =>
			    case SM.find (out1, name) of
				NONE => (ErrorMsg.error (SOME loc) "Missing an output environment variable.";
					 print ("Name: " ^ name ^ "\n");
					 preface ("Type:", p_typ t))
			      | SOME t' =>
				subTyp (t', t)
				handle Unify _ =>
				       (ErrorMsg.error (SOME loc) "Wrong type for output environment variable.";
					print ("     Name: " ^ name ^ "\n");
					preface (" Has type:", p_typ t');
					preface ("Need type:", p_typ t)))
			out2
	in
	    checkPreds ();
	    checkIn ();
	    checkOut ();
	    true
	end
	
      | _ => false

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