[hcoop/domtool2.git] / src / tycheck.sml

(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006-2007, Adam Chlipala
 * Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
 *
 * 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
      | DEnv (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 ("Dynamically bound value",
							    e,
							    t,
							    to,
							    SOME ue));
	    bindInitialDynEnvVal G (name, to, 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 (prog as (_, ds, eo)) =
    let
	val G' = foldl (fn (d, G) => checkDecl G d) G ds

	fun tInitial prog env =
	    (* This should likely only take the dynamic env as an argument *)
	    let
		fun allSets (e, _) =
		    case e of
			ESkip => true
		      | ESet _ => true
		      | ESeq es => List.all allSets es
		      | _ => false

		val dmy = ErrorMsg.dummyLoc

		fun bodyType (_, _, SOME e) =
		    if allSets e then
			(CPrefix (CRoot, dmy), dmy)
		    else
			(CRoot, dmy)
		  | bodyType _ = (CRoot, dmy)
	    in
		(TAction (bodyType prog,
			  Env.initialDynEnvTypes env,
			  StringMap.empty),
		 dmy)
	    end

    in
	case eo of
	    NONE => ()
	  | SOME (e as (_, loc)) =>
	    let
		val t = checkExp G' e
		val tInit = tInitial prog G'
	    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
e140629f	3	* Copyright (c) 2014 Clinton Ebadi <clinton@unknownlamer.org>
27d9de59 AC	4	*
	5	* This program is free software; you can redistribute it and/or
	6	* modify it under the terms of the GNU General Public License
	7	* as published by the Free Software Foundation; either version 2
	8	* of the License, or (at your option) any later version.
	9	*
	10	* This program is distributed in the hope that it will be useful,
	11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	13	* GNU General Public License for more details.
	14	*
	15	* You should have received a copy of the GNU General Public License
	16	* along with this program; if not, write to the Free Software
	17	* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
dac62e84	18	*)
27d9de59 AC	19
	20	(* Domtool configuration language type checking *)
	21
	22	structure Tycheck :> TYCHECK = struct
	23
492c1cff	24	open Ast Print Env
27d9de59 AC	25
	26	structure SM = StringMap
	27
b3159a70 AC	28	val externFlag = ref false
	29	fun allowExterns () = externFlag := true
	30	fun disallowExterns () = externFlag := false
	31
27d9de59 AC	32	local
	33	val unifCount = ref 0
	34	in
	35	fun resetUnif () = unifCount := 0
	36
	37	fun newUnif () =
	38	let
	39	val c = !unifCount
	40	val name =
	41	if c < 26 then
	42	str (chr (ord #"A" + c))
	43	else
	44	"UNIF" ^ Int.toString (c - 26)
	45	in
	46	unifCount := c + 1;
	47	TUnif (name, ref NONE)
	48	end
	49	end
	50
27d9de59	51
db427c67	52	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
27d9de59	53	case (p1, p2) of
1a4e5a6c AC	54	(_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
	55	\| (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
	56
	57	\| (_, CPrefix (CRoot, _)) => true
db427c67 AC	58	\| (CNot (CPrefix (CRoot, _), _), _) => true
	59
	60	\| (CRoot, CRoot) => true
	61
	62	\| (CConst s1, CConst s2) => s1 = s2
	63
	64	\| (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
234b917a	65	\| (_, CPrefix p2) => predImplies (p1All, p2)
db427c67 AC	66
db427c67 AC	67	\| (CNot p1, CNot p2) => predImplies (p2, p1)
2882ee37 AC	68	\| (CRoot, CNot (CConst _, _)) => true
2882ee37 AC	69	\| (CConst s1, CNot (CConst s2, _)) => s1 <> s2
27d9de59	70
db427c67 AC	71	\| _ => false
	72
	73	fun predSimpl (pAll as (p, loc)) =
	74	case p of
	75	CRoot => pAll
	76	\| CConst _ => pAll
	77	\| CPrefix p => (CPrefix (predSimpl p), loc)
	78	\| CNot p => (CNot (predSimpl p), loc)
	79	\| CAnd (p1, p2) =>
	80	let
	81	val p1' = predSimpl p1
	82	val p2' = predSimpl p2
	83	in
	84	case p1' of
	85	(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
	86	\| _ => if predImplies (p2', p1') then
	87	p2'
1a4e5a6c AC	88	else if predImplies (p1', p2') then
1a4e5a6c AC	89	p1'
db427c67 AC	90	else
	91	(CAnd (p1', p2'), loc)
	92	end
	93
234b917a	94	fun subPred (p1, p2) =
db427c67 AC	95	if predImplies (p1, p2) then
	96	()
	97	else
	98	raise (Unify (UnifyPred (p1, p2)))
27d9de59	99
234b917a AC	100	fun subRecord f (r1, r2) =
	101	SM.appi (fn (k, v2) =>
	102	case SM.find (r1, k) of
9b7ee2b2	103	NONE => raise Describe.UnequalDomains
234b917a	104	\| SOME v1 => f (v1, v2)) r2
27d9de59 AC	105
	106	fun occurs u (t, _) =
	107	case t of
	108	TBase _ => false
	109	\| TList t => occurs u t
	110	\| TArrow (d, r) => occurs u d orelse occurs u r
	111	\| TAction (_, d, r) =>
	112	List.exists (occurs u) (SM.listItems d)
	113	orelse List.exists (occurs u) (SM.listItems r)
1a4e5a6c	114	\| TNested (_, t) => occurs u t
27d9de59 AC	115	\| TError => false
	116	\| TUnif (_, ref (SOME t)) => occurs u t
	117	\| TUnif (_, u') => u = u'
	118
234b917a	119	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
27d9de59 AC	120	case (t1, t2) of
	121	(TBase s1, TBase s2) =>
	122	if s1 = s2 then
	123	()
	124	else
	125	raise Unify (UnifyTyp (t1All, t2All))
234b917a	126	\| (TList t1, TList t2) => subTyp (t1, t2)
27d9de59	127	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
234b917a AC	128	(subTyp (d2, d1);
234b917a AC	129	subTyp (r1, r2))
27d9de59 AC	130
27d9de59 AC	131	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
234b917a AC	132	((subPred (p2, p1);
	133	subRecord subTyp (d2, d1);
	134	subRecord subTyp (r1, r2);
	135	subRecord subTyp (r2, r1))
27d9de59 AC	136	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
27d9de59 AC	137
234b917a AC	138	\| (TNested (d1, r1), TNested (d2, r2)) =>
234b917a AC	139	(subPred (d2, d1);
1a4e5a6c	140	subTyp (r1, r2))
234b917a AC	141
	142	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	143	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
27d9de59 AC	144
	145	\| (TUnif (_, r1), TUnif (_, r2)) =>
	146	if r1 = r2 then
	147	()
	148	else
	149	r1 := SOME t2All
	150
	151	\| (TUnif (name, r), _) =>
	152	if occurs r t2All then
	153	raise (Unify (UnifyOccurs (name, t2All)))
	154	else
	155	r := SOME t2All
	156
	157	\| (_, TUnif (name, r)) =>
	158	if occurs r t1All then
	159	raise (Unify (UnifyOccurs (name, t1All)))
	160	else
	161	r := SOME t1All
	162
	163	\| (TError, _) => ()
	164	\| (_, TError) => ()
	165
	166	\| _ => raise Unify (UnifyTyp (t1All, t2All))
	167
	168	fun isError t =
	169	case t of
	170	(TError, _) => true
	171	\| _ => false
	172
db427c67 AC	173	fun whnorm (tAll as (t, loc)) =
	174	case t of
	175	TUnif (_, ref (SOME tAll)) => whnorm tAll
	176	\| _ => tAll
	177
629a34f6 AC	178	fun baseCondition t =
	179	case whnorm t of
	180	(TBase name, _) => typeRule name
	181	\| (TList t, _) =>
	182	(case baseCondition t of
	183	NONE => NONE
	184	\| SOME f => SOME (fn (EList ls, _) => List.all f ls
	185	\| _ => false))
	186	\| _ => NONE
	187
4ecbfd4c AC	188	fun simplifyKindOf e =
	189	case e of
	190	(EApp ((EVar s, _), e'), _) =>
	191	(case Env.function s of
	192	NONE => e
	193	\| SOME f =>
	194	case f [e'] of
	195	NONE => e
	196	\| SOME e => e)
	197	\| _ => e
	198
6be996d4	199	fun hasTyp (e, t1, t2) =
629a34f6 AC	200	if (case baseCondition t2 of
629a34f6 AC	201	NONE => false
4ecbfd4c	202	\| SOME rule => rule (simplifyKindOf e)) then
629a34f6 AC	203	()
	204	else
	205	subTyp (t1, t2)
6be996d4	206
095de39e AC	207	fun checkPred G (p, loc) =
	208	let
	209	val err = ErrorMsg.error (SOME loc)
	210	in
	211	case p of
	212	CRoot => ()
	213	\| CConst s =>
	214	if lookupContext G s then
	215	()
	216	else
	217	err ("Unbound context " ^ s)
	218	\| CPrefix p => checkPred G p
	219	\| CNot p => checkPred G p
	220	\| CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
	221	end
	222
234b917a AC	223	fun checkTyp G (tAll as (t, loc)) =
	224	let
	225	val err = ErrorMsg.error (SOME loc)
	226	in
	227	case t of
	228	TBase name =>
	229	if lookupType G name then
	230	tAll
	231	else
	232	(err ("Unbound type name " ^ name);
	233	(TError, loc))
	234	\| TList t => (TList (checkTyp G t), loc)
	235	\| TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
095de39e AC	236	\| TAction (p, d, r) => (checkPred G p;
	237	(TAction (p, SM.map (checkTyp G) d,
	238	SM.map (checkTyp G) r), loc))
	239	\| TNested (p, t) => (checkPred G p;
	240	(TNested (p, checkTyp G t), loc))
234b917a AC	241	\| TError => raise Fail "TError in parser-generated type"
	242	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	243	end
	244
8a7c40fa AC	245	fun envVarSetFrom v (e, _) =
	246	case e of
	247	ESet (v', e) =>
	248	if v = v' then
	249	SOME e
	250	else
	251	NONE
8cbb9632	252	\| EGet (_, _, _, e) => envVarSetFrom v e
8a7c40fa AC	253	\| ESeq es => foldr (fn (e, found) =>
	254	case found of
	255	SOME _ => found
	256	\| NONE => envVarSetFrom v e)
	257	NONE es
	258	\| ELocal (_, e) => envVarSetFrom v e
	259
	260	\| _ => NONE
	261
113d7217	262	val ununify = Describe.ununify
8cbb9632	263
27d9de59 AC	264	fun checkExp G (eAll as (e, loc)) =
27d9de59 AC	265	let
e1b99e23	266	val dte = Describe.describe_type_error loc
27d9de59 AC	267	in
	268	case e of
	269	EInt _ => (TBase "int", loc)
	270	\| EString _ => (TBase "string", loc)
	271	\| EList es =>
	272	let
	273	val t = (newUnif (), loc)
	274	in
	275	foldl (fn (e', ret) =>
	276	let
	277	val t' = checkExp G e'
	278	in
6be996d4	279	(hasTyp (eAll, t', t);
27d9de59 AC	280	if isError t' then
	281	(TList (TError, loc), loc)
	282	else
	283	ret)
	284	handle Unify ue =>
	285	(dte (WrongType ("List element",
	286	e',
	287	t',
	288	t,
	289	SOME ue));
	290	(TError, loc))
	291	end) (TList t, loc) es
	292	end
	293
	294	\| ELam (x, to, e) =>
	295	let
	296	val t =
	297	case to of
	298	NONE => (newUnif (), loc)
234b917a	299	\| SOME t => checkTyp G t
27d9de59	300
492c1cff	301	val G' = bindVal G (x, t, NONE)
27d9de59 AC	302	val t' = checkExp G' e
	303	in
	304	(TArrow (t, t'), loc)
	305	end
	306	\| EVar x =>
234b917a	307	(case lookupVal G x of
27d9de59 AC	308	NONE => (dte (UnboundVariable x);
	309	(TError, loc))
	310	\| SOME t => t)
	311	\| EApp (func, arg) =>
	312	let
	313	val dom = (newUnif (), loc)
	314	val ran = (newUnif (), loc)
	315
	316	val tf = checkExp G func
	317	val ta = checkExp G arg
	318	in
6be996d4 AC	319	(hasTyp (func, tf, (TArrow (dom, ran), loc));
6be996d4 AC	320	hasTyp (arg, ta, dom)
27d9de59 AC	321	handle Unify ue =>
	322	dte (WrongType ("Function argument",
	323	arg,
	324	ta,
	325	dom,
	326	SOME ue));
	327	ran)
	328	handle Unify ue =>
	329	(dte (WrongForm ("Function to be applied",
	330	"function",
	331	func,
	332	tf,
	333	SOME ue));
	334	(TError, loc))
	335	end
db427c67	336
6bb366c5 AC	337	\| EALam (x, p, e) =>
	338	let
	339	val p' = checkPred G p
	340
	341	val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
cdb376d4	342	val t' = whnorm (checkExp G' e)
6bb366c5 AC	343	in
	344	case t' of
	345	(TAction _, _) => (TNested (p, t'), loc)
	346	\| _ => (dte (WrongForm ("Body of nested configuration 'fn'",
	347	"action",
	348	e,
	349	t',
	350	NONE));
	351	(TError, loc))
	352	end
	353
db427c67 AC	354	\| ESet (evar, e) =>
	355	let
	356	val t = checkExp G e
	357	in
	358	(TAction ((CPrefix (CRoot, loc), loc),
	359	SM.empty,
	360	SM.insert (SM.empty, evar, t)),
	361	loc)
	362	end
8cbb9632	363	\| EGet (x, topt, evar, rest) =>
db427c67 AC	364	let
db427c67 AC	365	val xt = (newUnif (), loc)
492c1cff	366	val G' = bindVal G (x, xt, NONE)
db427c67 AC	367
	368	val rt = whnorm (checkExp G' rest)
	369	in
8cbb9632 AC	370	case topt of
	371	NONE => ()
	372	\| SOME t => subTyp (xt, checkTyp G t);
	373
	374	case ununify rt of
db427c67 AC	375	(TAction (p, d, r), _) =>
	376	(case SM.find (d, evar) of
	377	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	378	\| SOME xt' =>
234b917a	379	(subTyp (xt', xt)
db427c67 AC	380	handle Unify ue =>
	381	dte (WrongType ("Retrieved environment variable",
	382	(EVar x, loc),
	383	xt',
	384	xt,
	385	SOME ue));
	386	rt))
234b917a	387	\| (TError, _) => rt
db427c67 AC	388	\| _ => (dte (WrongForm ("Body of environment variable read",
	389	"action",
	390	rest,
	391	rt,
	392	NONE));
	393	(TError, loc))
	394	end
	395
	396	\| ESeq [] => raise Fail "Empty ESeq"
	397	\| ESeq [e1] => checkExp G e1
	398	\| ESeq (e1 :: rest) =>
	399	let
	400	val e2 = (ESeq rest, loc)
	401
	402	val t1 = whnorm (checkExp G e1)
	403	val t2 = whnorm (checkExp G e2)
	404	in
	405	case t1 of
	406	(TAction (p1, d1, r1), _) =>
	407	(case t2 of
	408	(TAction (p2, d2, r2), _) =>
	409	let
	410	val p' = predSimpl (CAnd (p1, p2), loc)
	411
	412	val d' = SM.foldli (fn (name, t, d') =>
	413	case SM.find (r1, name) of
	414	NONE =>
	415	(case SM.find (d', name) of
	416	NONE => SM.insert (d', name, t)
	417	\| SOME t' =>
8a7c40fa AC	418	((case envVarSetFrom name e1 of
	419	NONE => subTyp (t, t')
	420	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	421	handle Unify ue =>
	422	dte (WrongType ("Shared environment variable",
	423	(EVar name, loc),
db427c67	424	t',
8a7c40fa	425	t,
db427c67 AC	426	SOME ue));
	427	d'))
	428	\| SOME t' =>
8a7c40fa AC	429	((case envVarSetFrom name e1 of
	430	NONE => subTyp (t, t')
	431	\| SOME e => hasTyp (e, t, t'))
db427c67 AC	432	handle Unify ue =>
	433	dte (WrongType ("Shared environment variable",
	434	(EVar name, loc),
db427c67	435	t',
8a7c40fa	436	t,
db427c67 AC	437	SOME ue));
	438	d'))
	439	d1 d2
	440
	441	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	442	r1 r2
	443	in
	444	(TAction (p', d', r'), loc)
	445	end
234b917a	446	\| (TError, _) => t2
a7951e95	447	\| _ => (dte (WrongForm ("First action to be sequenced",
db427c67 AC	448	"action",
	449	e2,
	450	t2,
	451	NONE));
	452	(TError, loc)))
234b917a	453	\| (TError, _) => t1
a7951e95	454	\| _ => (dte (WrongForm ("Second action to be sequenced",
db427c67 AC	455	"action",
	456	e1,
	457	t1,
	458	NONE));
	459	(TError, loc))
	460	end
	461
1a4e5a6c	462	\| ELocal (e1, e2) =>
db427c67	463	let
1a4e5a6c AC	464	val t1 = whnorm (checkExp G e1)
1a4e5a6c AC	465	val t2 = whnorm (checkExp G e2)
db427c67	466	in
1a4e5a6c AC	467	case t1 of
	468	(TAction (p1, d1, r1), _) =>
	469	(case t2 of
	470	(TAction (p2, d2, r2), _) =>
	471	let
	472	val p' = predSimpl (CAnd (p1, p2), loc)
	473
	474	val d' = SM.foldli (fn (name, t, d') =>
	475	case SM.find (r1, name) of
	476	NONE =>
	477	(case SM.find (d', name) of
	478	NONE => SM.insert (d', name, t)
	479	\| SOME t' =>
8a7c40fa AC	480	((case envVarSetFrom name e1 of
	481	NONE => subTyp (t', t)
	482	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	483	handle Unify ue =>
	484	dte (WrongType ("Shared environment variable",
	485	(EVar name, loc),
1a4e5a6c	486	t',
8a7c40fa	487	t,
1a4e5a6c AC	488	SOME ue));
	489	d'))
	490	\| SOME t' =>
8a7c40fa AC	491	((case envVarSetFrom name e1 of
	492	NONE => subTyp (t', t)
	493	\| SOME e => hasTyp (e, t', t))
1a4e5a6c AC	494	handle Unify ue =>
	495	dte (WrongType ("Shared environment variable",
	496	(EVar name, loc),
1a4e5a6c	497	t',
8a7c40fa	498	t,
1a4e5a6c AC	499	SOME ue));
	500	d'))
	501	d1 d2
	502	in
	503	(TAction (p', d', r2), loc)
	504	end
	505	\| (TError, _) => t2
a7951e95	506	\| _ => (dte (WrongForm ("Body of local settings",
1a4e5a6c AC	507	"action",
	508	e2,
	509	t2,
	510	NONE));
	511	(TError, loc)))
	512	\| (TError, _) => t1
a7951e95	513	\| _ => (dte (WrongForm ("Local settings",
db427c67	514	"action",
1a4e5a6c AC	515	e1,
1a4e5a6c AC	516	t1,
db427c67 AC	517	NONE));
	518	(TError, loc))
	519	end
234b917a	520
1a4e5a6c	521
234b917a AC	522	\| EWith (e1, e2) =>
	523	let
	524	val t1 = whnorm (checkExp G e1)
	525	val t2 = whnorm (checkExp G e2)
	526	in
	527	case t1 of
1a4e5a6c	528	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a AC	529	(case t2 of
	530	(TAction (p, d, r), _) =>
	531	if predImplies (pd, p) then
1a4e5a6c AC	532	let
	533	val combineRecs =
	534	SM.unionWithi (fn (name, t1, t2) =>
	535	(subTyp (t1, t2)
	536	handle Unify ue =>
	537	dte (WrongType ("Environment variable",
	538	(EVar name, loc),
	539	t1,
	540	t2,
	541	SOME ue));
	542	t2))
	543	in
	544	(TAction (pr, combineRecs (d, d1),
	545	combineRecs (r, r1)), loc)
	546	end
234b917a AC	547	else
	548	(dte (WrongPred ("nested action",
	549	pd,
	550	p));
	551	(TError, loc))
	552	\| (TError, _) => t2
	553	\| _ =>
	554	(dte (WrongForm ("Body of nested action",
	555	"action",
	556	e2,
	557	t2,
	558	NONE));
	559	(TError, loc)))
	560	\| (TError, _) => t1
	561	\| _ =>
	562	(dte (WrongForm ("Container of nested action",
	563	"action",
	564	e1,
	565	t1,
	566	NONE));
	567	(TError, loc))
	568	end
	569
	570	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	571	SM.empty, SM.empty), loc)
75d4c2d6 AC	572
	573	\| EIf (e1, e2, e3) =>
	574	let
75d4c2d6 AC	575	val t1 = checkExp G e1
	576	val t2 = checkExp G e2
	577	val t3 = checkExp G e3
	578	val bool = (TBase "bool", loc)
	579	in
	580	(subTyp (t1, bool))
	581	handle Unify ue =>
a356587a	582	dte (WrongType ("\"if\" test",
75d4c2d6 AC	583	e1,
	584	t1,
	585	bool,
	586	SOME ue));
a356587a AC	587	(subTyp (t2, t3); t3)
	588	handle Unify _ =>
	589	((subTyp (t3, t2); t2)
	590	handle Unify ue =>
	591	(dte (WrongType ("\"else\" case",
	592	eAll,
	593	t3,
	594	t2,
	595	SOME ue));
	596	(TError, loc)))
75d4c2d6	597	end
27d9de59 AC	598	end
	599
	600	exception Ununif
	601
	602	fun ununif (tAll as (t, loc)) =
	603	case t of
	604	TBase _ => tAll
	605	\| TList t => (TList (ununif t), loc)
	606	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	607	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	608	\| TUnif (_, ref (SOME t)) => ununif t
234b917a	609	\| TNested _ => tAll
27d9de59 AC	610	\| TError => tAll
	611
	612	\| TUnif (_, ref NONE) => raise Ununif
	613
	614	fun hasError (t, _) =
	615	case t of
	616	TBase _ => false
	617	\| TList t => hasError t
	618	\| TArrow (d, r) => hasError d orelse hasError r
	619	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	620	orelse List.exists hasError (SM.listItems r)
234b917a	621	\| TNested _ => false
27d9de59 AC	622	\| TError => false
	623	\| TUnif (_, ref (SOME t)) => hasError t
	624	\| TUnif (_, ref NONE) => false
	625
	626
	627	fun checkUnit G (eAll as (_, loc)) =
	628	let
	629	val _ = resetUnif ()
	630	val t = checkExp G eAll
	631	in
	632	if hasError t then
	633	t
	634	else
	635	ununif t
	636	handle Ununif =>
	637	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
9b7ee2b2	638	output (p_typ t);
27d9de59 AC	639	t)
	640	end
	641
234b917a AC	642	fun checkDecl G (d, _, loc) =
234b917a AC	643	case d of
b3159a70 AC	644	DExternType name =>
	645	if !externFlag then
	646	bindType G name
	647	else
	648	(ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
	649	G)
	650	\| DExternVal (name, t) =>
	651	if !externFlag then
	652	bindVal G (name, checkTyp G t, NONE)
	653	else
	654	(ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
	655	G)
492c1cff AC	656	\| DVal (name, to, e) =>
	657	let
	658	val to =
	659	case to of
	660	NONE => (newUnif (), loc)
	661	\| SOME to => checkTyp G to
	662
	663	val t = checkExp G e
	664	in
6be996d4	665	hasTyp (e, t, to)
492c1cff	666	handle Unify ue =>
e1b99e23 AC	667	Describe.describe_type_error loc
	668	(WrongType ("Bound value",
	669	e,
	670	t,
	671	to,
	672	SOME ue));
492c1cff AC	673	bindVal G (name, to, SOME e)
492c1cff AC	674	end
e140629f CE	675	\| DEnv (name, to, e) =>
	676	let
	677	val to =
	678	case to of
	679	NONE => (newUnif (), loc)
	680	\| SOME to => checkTyp G to
	681
	682	val t = checkExp G e
	683	in
	684	hasTyp (e, t, to)
	685	handle Unify ue =>
	686	Describe.describe_type_error loc
	687	(WrongType ("Dynamically bound value",
	688	e,
	689	t,
	690	to,
	691	SOME ue));
	692	bindInitialDynEnvVal G (name, to, e)
	693	end
095de39e	694	\| DContext name => bindContext G name
234b917a	695
f8fd0d2a AC	696	fun printActionDiffs {have, need} =
	697	case (ununif have, ununif need) of
	698	((TAction (p1, in1, out1), loc), (TAction (p2, in2, out2), _)) =>
	699	let
	700	fun checkPreds () =
	701	if predImplies (p1, p2) then
	702	()
	703	else
	704	(ErrorMsg.error (SOME loc) "Files provides the wrong kind of configuration.";
	705	preface ("Have:", p_pred p1);
	706	preface ("Need:", p_pred p2))
	707
	708	fun checkIn () =
	709	SM.appi (fn (name, t) =>
	710	case SM.find (in2, name) of
	711	NONE => (ErrorMsg.error (SOME loc) "An unavailable environment variable is used.";
	712	print ("Name: " ^ name ^ "\n");
	713	preface ("Type:", p_typ t))
	714	\| SOME t' =>
	715	subTyp (t', t)
	716	handle Unify _ =>
	717	(ErrorMsg.error (SOME loc) "Wrong type for environment variable.";
	718	print (" Name: " ^ name ^ "\n");
	719	preface (" Has type:", p_typ t');
	720	preface ("Used with type:", p_typ t)))
	721	in1
	722
	723	fun checkOut () =
	724	SM.appi (fn (name, t) =>
	725	case SM.find (out1, name) of
	726	NONE => (ErrorMsg.error (SOME loc) "Missing an output environment variable.";
	727	print ("Name: " ^ name ^ "\n");
	728	preface ("Type:", p_typ t))
	729	\| SOME t' =>
	730	subTyp (t', t)
	731	handle Unify _ =>
	732	(ErrorMsg.error (SOME loc) "Wrong type for output environment variable.";
	733	print (" Name: " ^ name ^ "\n");
	734	preface (" Has type:", p_typ t');
	735	preface ("Need type:", p_typ t)))
	736	out2
	737	in
	738	checkPreds ();
	739	checkIn ();
	740	checkOut ();
	741	true
	742	end
	743
	744	\| _ => false
	745
e140629f	746	fun checkFile G (prog as (_, ds, eo)) =
234b917a AC	747	let
234b917a AC	748	val G' = foldl (fn (d, G) => checkDecl G d) G ds
e140629f CE	749
	750	fun tInitial prog env =
	751	(* This should likely only take the dynamic env as an argument *)
	752	let
	753	fun allSets (e, _) =
	754	case e of
	755	ESkip => true
	756	\| ESet _ => true
	757	\| ESeq es => List.all allSets es
	758	\| _ => false
	759
	760	val dmy = ErrorMsg.dummyLoc
	761
	762	fun bodyType (_, _, SOME e) =
	763	if allSets e then
	764	(CPrefix (CRoot, dmy), dmy)
	765	else
	766	(CRoot, dmy)
	767	\| bodyType _ = (CRoot, dmy)
	768	in
	769	(TAction (bodyType prog,
	770	Env.initialDynEnvTypes env,
	771	StringMap.empty),
	772	dmy)
	773	end
	774
234b917a AC	775	in
	776	case eo of
	777	NONE => ()
	778	\| SOME (e as (_, loc)) =>
	779	let
	780	val t = checkExp G' e
e140629f	781	val tInit = tInitial prog G'
234b917a	782	in
6be996d4	783	hasTyp (e, t, tInit)
f8fd0d2a AC	784	handle Unify _ =>
	785	if printActionDiffs {have = t, need = tInit} then
	786	()
	787	else
	788	ErrorMsg.error (SOME loc) "File ends in something that isn't a directive."
234b917a AC	789	end;
	790	G'
	791	end
	792
27d9de59	793	end