[hcoop/zz_old/domtool2-proto.git] / src / tycheck.sml

(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006-2007, Adam Chlipala
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
 *)

(* Domtool configuration language type checking *)

structure Tycheck :> TYCHECK = struct

open Ast Print Env

structure SM = StringMap

val externFlag = ref false
fun allowExterns () = externFlag := true
fun disallowExterns () = externFlag := false

local
    val unifCount = ref 0
in
fun resetUnif () = unifCount := 0

fun newUnif () =
    let
	val c = !unifCount
	val name =
	    if c < 26 then
		str (chr (ord #"A" + c))
	    else
		"UNIF" ^ Int.toString (c - 26)
    in
	unifCount := c + 1;
	TUnif (name, ref NONE)
    end
end
	    

fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
    case (p1, p2) of
	(_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
      | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)

      | (_, CPrefix (CRoot, _)) => true
      | (CNot (CPrefix (CRoot, _), _), _) => true

      | (CRoot, CRoot) => true

      | (CConst s1, CConst s2) => s1 = s2

      | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
      | (_, CPrefix p2) => predImplies (p1All, p2)

      | (CNot p1, CNot p2) => predImplies (p2, p1)
      | (CRoot, CNot (CConst _, _)) => true
      | (CConst s1, CNot (CConst s2, _)) => s1 <> s2

      | _ => false

fun predSimpl (pAll as (p, loc)) =
    case p of
	CRoot => pAll
      | CConst _ => pAll
      | CPrefix p => (CPrefix (predSimpl p), loc)
      | CNot p => (CNot (predSimpl p), loc)
      | CAnd (p1, p2) =>
	let
	    val p1' = predSimpl p1
	    val p2' = predSimpl p2
	in
	    case p1' of
		(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
	      | _ => if predImplies (p2', p1') then
			 p2'
		     else if predImplies (p1', p2') then
			 p1'
		     else
			 (CAnd (p1', p2'), loc)
	end
   
fun subPred (p1, p2) =
    if predImplies (p1, p2) then
	()
    else
	raise (Unify (UnifyPred (p1, p2)))

fun subRecord f (r1, r2) =
    SM.appi (fn (k, v2) =>
		case SM.find (r1, k) of
		    NONE => raise Describe.UnequalDomains
		  | SOME v1 => f (v1, v2)) r2

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

fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
    case (t1, t2) of
	(TBase s1, TBase s2) =>
	if s1 = s2 then
	    ()
	else
	    raise Unify (UnifyTyp (t1All, t2All))
      | (TList t1, TList t2) => subTyp (t1, t2)
      | (TArrow (d1, r1), TArrow (d2, r2)) =>
	(subTyp (d2, d1);
	 subTyp (r1, r2))

      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	((subPred (p2, p1);
	  subRecord subTyp (d2, d1);
	  subRecord subTyp (r1, r2);
	  subRecord subTyp (r2, r1))
	 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))

      | (TNested (d1, r1), TNested (d2, r2)) =>
	(subPred (d2, d1);
	 subTyp (r1, r2))

      | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
      | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)

      | (TUnif (_, r1), TUnif (_, r2)) =>
	if r1 = r2 then
	    ()
	else
	    r1 := SOME t2All

      | (TUnif (name, r), _) =>
	if occurs r t2All then
	    raise (Unify (UnifyOccurs (name, t2All)))
	else
	    r := SOME t2All

      | (_, TUnif (name, r)) =>
	if occurs r t1All then
	    raise (Unify (UnifyOccurs (name, t1All)))
	else
	    r := SOME t1All

      | (TError, _) => ()
      | (_, TError) => ()

      | _ => raise Unify (UnifyTyp (t1All, t2All))

fun isError t =
    case t of
	(TError, _) => true
      | _ => false

fun whnorm (tAll as (t, loc)) =
    case t of
	TUnif (_, ref (SOME tAll)) => whnorm tAll
      | _ => tAll

fun baseCondition t =
    case whnorm t of
	(TBase name, _) => typeRule name
      | (TList t, _) =>
	(case baseCondition t of
	     NONE => NONE
	   | SOME f => SOME (fn (EList ls, _) => List.all f ls
			      | _ => false))
      | _ => NONE

fun simplifyKindOf e =
    case e of
	(EApp ((EVar s, _), e'), _) =>
	(case Env.function s of
	     NONE => e
	   | SOME f =>
	     case f [e'] of
		 NONE => e
	       | SOME e => e)
      | _ => e

fun hasTyp (e, t1, t2) =
    if (case baseCondition t2 of
	    NONE => false
	  | SOME rule => rule (simplifyKindOf e)) then
	()
    else
	subTyp (t1, t2)

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

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

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

      | _ => NONE

fun ununify (tAll as (t, _)) =
    case t of
	TUnif (_, ref (SOME t)) => ununify t
      | _ => tAll

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

exception Ununif

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

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

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


fun checkUnit G (eAll as (_, loc)) =
    let
	val _ = resetUnif ()
	val t = checkExp G eAll
    in
	if hasError t then
	    t
	else
	    ununif t
	    handle Ununif =>
		   (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
		    output (p_typ t);
		    t)
    end

fun checkDecl G (d, _, loc) =
    case d of
	DExternType name =>
	if !externFlag then
	    bindType G name
	else
	    (ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
	     G)
      | DExternVal (name, t) =>
	if !externFlag then
	    bindVal G (name, checkTyp G t, NONE)
	else
	    (ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
	     G)
      | DVal (name, to, e) =>
	let
	    val to =
		case to of
		    NONE => (newUnif (), loc)
		  | SOME to => checkTyp G to

	    val t = checkExp G e
	in
	    hasTyp (e, t, to)
	    handle Unify ue =>
		   Describe.describe_type_error loc
						(WrongType ("Bound value",
							    e,
							    t,
							    to,
							    SOME ue));
	    bindVal G (name, to, SOME e)
	end
      | DContext name => bindContext G name

fun checkFile G tInit (_, ds, eo) =
    let
	val G' = foldl (fn (d, G) => checkDecl G d) G ds
    in
	case eo of
	    NONE => ()
	  | SOME (e as (_, loc)) =>
	    let
		val t = checkExp G' e
	    in
		hasTyp (e, t, tInit)
		handle Unify ue =>
		       (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
			preface ("Actual:", p_typ t);
			preface ("Needed:", p_typ tInit))
	    end;
	G'
    end

end
Commit	Line	Data
64014a03	1	(* HCoop Domtool (http://hcoop.sourceforge.net/)
12ad758b	2	* Copyright (c) 2006-2007, Adam Chlipala
64014a03	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.
ae3a5b8c	17	*)
64014a03	18
	19	(* Domtool configuration language type checking *)
	20
	21	structure Tycheck :> TYCHECK = struct
	22
add6f172	23	open Ast Print Env
64014a03	24
	25	structure SM = StringMap
	26
89c9edc9	27	val externFlag = ref false
	28	fun allowExterns () = externFlag := true
	29	fun disallowExterns () = externFlag := false
	30
64014a03	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
64014a03	50
dbd7a7d2	51	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
64014a03	52	case (p1, p2) of
2dc33fa4	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
dbd7a7d2	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)
e680130a	64	\| (_, CPrefix p2) => predImplies (p1All, p2)
dbd7a7d2	65
dbd7a7d2	66	\| (CNot p1, CNot p2) => predImplies (p2, p1)
ff2a424a	67	\| (CRoot, CNot (CConst _, _)) => true
ff2a424a	68	\| (CConst s1, CNot (CConst s2, _)) => s1 <> s2
64014a03	69
dbd7a7d2	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'
2dc33fa4	87	else if predImplies (p1', p2') then
2dc33fa4	88	p1'
dbd7a7d2	89	else
	90	(CAnd (p1', p2'), loc)
	91	end
	92
e680130a	93	fun subPred (p1, p2) =
dbd7a7d2	94	if predImplies (p1, p2) then
	95	()
	96	else
	97	raise (Unify (UnifyPred (p1, p2)))
64014a03	98
e680130a	99	fun subRecord f (r1, r2) =
	100	SM.appi (fn (k, v2) =>
	101	case SM.find (r1, k) of
a4c53cb2	102	NONE => raise Describe.UnequalDomains
e680130a	103	\| SOME v1 => f (v1, v2)) r2
64014a03	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)
2dc33fa4	113	\| TNested (_, t) => occurs u t
64014a03	114	\| TError => false
	115	\| TUnif (_, ref (SOME t)) => occurs u t
	116	\| TUnif (_, u') => u = u'
	117
e680130a	118	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
64014a03	119	case (t1, t2) of
	120	(TBase s1, TBase s2) =>
	121	if s1 = s2 then
	122	()
	123	else
	124	raise Unify (UnifyTyp (t1All, t2All))
e680130a	125	\| (TList t1, TList t2) => subTyp (t1, t2)
64014a03	126	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
e680130a	127	(subTyp (d2, d1);
e680130a	128	subTyp (r1, r2))
64014a03	129
64014a03	130	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
e680130a	131	((subPred (p2, p1);
	132	subRecord subTyp (d2, d1);
	133	subRecord subTyp (r1, r2);
	134	subRecord subTyp (r2, r1))
64014a03	135	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
64014a03	136
e680130a	137	\| (TNested (d1, r1), TNested (d2, r2)) =>
e680130a	138	(subPred (d2, d1);
2dc33fa4	139	subTyp (r1, r2))
e680130a	140
	141	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	142	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
64014a03	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
dbd7a7d2	172	fun whnorm (tAll as (t, loc)) =
	173	case t of
	174	TUnif (_, ref (SOME tAll)) => whnorm tAll
	175	\| _ => tAll
	176
2f68506c	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
a8d3e6c8	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
4264c8ef	198	fun hasTyp (e, t1, t2) =
2f68506c	199	if (case baseCondition t2 of
2f68506c	200	NONE => false
a8d3e6c8	201	\| SOME rule => rule (simplifyKindOf e)) then
2f68506c	202	()
	203	else
	204	subTyp (t1, t2)
4264c8ef	205
51c32b45	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
e680130a	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)
51c32b45	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))
e680130a	240	\| TError => raise Fail "TError in parser-generated type"
	241	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	242	end
	243
d68ab27c	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
28cf1be3	251	\| EGet (_, _, _, e) => envVarSetFrom v e
d68ab27c	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
28cf1be3	261	fun ununify (tAll as (t, _)) =
	262	case t of
	263	TUnif (_, ref (SOME t)) => ununify t
	264	\| _ => tAll
	265
64014a03	266	fun checkExp G (eAll as (e, loc)) =
64014a03	267	let
12ad758b	268	val dte = Describe.describe_type_error loc
64014a03	269	in
	270	case e of
	271	EInt _ => (TBase "int", loc)
	272	\| EString _ => (TBase "string", loc)
	273	\| EList es =>
	274	let
	275	val t = (newUnif (), loc)
	276	in
	277	foldl (fn (e', ret) =>
	278	let
	279	val t' = checkExp G e'
	280	in
4264c8ef	281	(hasTyp (eAll, t', t);
64014a03	282	if isError t' then
	283	(TList (TError, loc), loc)
	284	else
	285	ret)
	286	handle Unify ue =>
	287	(dte (WrongType ("List element",
	288	e',
	289	t',
	290	t,
	291	SOME ue));
	292	(TError, loc))
	293	end) (TList t, loc) es
	294	end
	295
	296	\| ELam (x, to, e) =>
	297	let
	298	val t =
	299	case to of
	300	NONE => (newUnif (), loc)
e680130a	301	\| SOME t => checkTyp G t
64014a03	302
add6f172	303	val G' = bindVal G (x, t, NONE)
64014a03	304	val t' = checkExp G' e
	305	in
	306	(TArrow (t, t'), loc)
	307	end
	308	\| EVar x =>
e680130a	309	(case lookupVal G x of
64014a03	310	NONE => (dte (UnboundVariable x);
	311	(TError, loc))
	312	\| SOME t => t)
	313	\| EApp (func, arg) =>
	314	let
	315	val dom = (newUnif (), loc)
	316	val ran = (newUnif (), loc)
	317
	318	val tf = checkExp G func
	319	val ta = checkExp G arg
	320	in
4264c8ef	321	(hasTyp (func, tf, (TArrow (dom, ran), loc));
4264c8ef	322	hasTyp (arg, ta, dom)
64014a03	323	handle Unify ue =>
	324	dte (WrongType ("Function argument",
	325	arg,
	326	ta,
	327	dom,
	328	SOME ue));
	329	ran)
	330	handle Unify ue =>
	331	(dte (WrongForm ("Function to be applied",
	332	"function",
	333	func,
	334	tf,
	335	SOME ue));
	336	(TError, loc))
	337	end
dbd7a7d2	338
bf9b0bc3	339	\| EALam (x, p, e) =>
	340	let
	341	val p' = checkPred G p
	342
	343	val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
c720772b	344	val t' = whnorm (checkExp G' e)
bf9b0bc3	345	in
	346	case t' of
	347	(TAction _, _) => (TNested (p, t'), loc)
	348	\| _ => (dte (WrongForm ("Body of nested configuration 'fn'",
	349	"action",
	350	e,
	351	t',
	352	NONE));
	353	(TError, loc))
	354	end
	355
dbd7a7d2	356	\| ESet (evar, e) =>
	357	let
	358	val t = checkExp G e
	359	in
	360	(TAction ((CPrefix (CRoot, loc), loc),
	361	SM.empty,
	362	SM.insert (SM.empty, evar, t)),
	363	loc)
	364	end
28cf1be3	365	\| EGet (x, topt, evar, rest) =>
dbd7a7d2	366	let
dbd7a7d2	367	val xt = (newUnif (), loc)
add6f172	368	val G' = bindVal G (x, xt, NONE)
dbd7a7d2	369
	370	val rt = whnorm (checkExp G' rest)
	371	in
28cf1be3	372	case topt of
	373	NONE => ()
	374	\| SOME t => subTyp (xt, checkTyp G t);
	375
	376	case ununify rt of
dbd7a7d2	377	(TAction (p, d, r), _) =>
	378	(case SM.find (d, evar) of
	379	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	380	\| SOME xt' =>
e680130a	381	(subTyp (xt', xt)
dbd7a7d2	382	handle Unify ue =>
	383	dte (WrongType ("Retrieved environment variable",
	384	(EVar x, loc),
	385	xt',
	386	xt,
	387	SOME ue));
	388	rt))
e680130a	389	\| (TError, _) => rt
dbd7a7d2	390	\| _ => (dte (WrongForm ("Body of environment variable read",
	391	"action",
	392	rest,
	393	rt,
	394	NONE));
	395	(TError, loc))
	396	end
	397
	398	\| ESeq [] => raise Fail "Empty ESeq"
	399	\| ESeq [e1] => checkExp G e1
	400	\| ESeq (e1 :: rest) =>
	401	let
	402	val e2 = (ESeq rest, loc)
	403
	404	val t1 = whnorm (checkExp G e1)
	405	val t2 = whnorm (checkExp G e2)
	406	in
	407	case t1 of
	408	(TAction (p1, d1, r1), _) =>
	409	(case t2 of
	410	(TAction (p2, d2, r2), _) =>
	411	let
	412	val p' = predSimpl (CAnd (p1, p2), loc)
	413
	414	val d' = SM.foldli (fn (name, t, d') =>
	415	case SM.find (r1, name) of
	416	NONE =>
	417	(case SM.find (d', name) of
	418	NONE => SM.insert (d', name, t)
	419	\| SOME t' =>
d68ab27c	420	((case envVarSetFrom name e1 of
	421	NONE => subTyp (t, t')
	422	\| SOME e => hasTyp (e, t, t'))
dbd7a7d2	423	handle Unify ue =>
	424	dte (WrongType ("Shared environment variable",
	425	(EVar name, loc),
dbd7a7d2	426	t',
d68ab27c	427	t,
dbd7a7d2	428	SOME ue));
	429	d'))
	430	\| SOME t' =>
d68ab27c	431	((case envVarSetFrom name e1 of
	432	NONE => subTyp (t, t')
	433	\| SOME e => hasTyp (e, t, t'))
dbd7a7d2	434	handle Unify ue =>
	435	dte (WrongType ("Shared environment variable",
	436	(EVar name, loc),
dbd7a7d2	437	t',
d68ab27c	438	t,
dbd7a7d2	439	SOME ue));
	440	d'))
	441	d1 d2
	442
	443	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	444	r1 r2
	445	in
	446	(TAction (p', d', r'), loc)
	447	end
e680130a	448	\| (TError, _) => t2
dbd7a7d2	449	\| _ => (dte (WrongForm ("Action to be sequenced",
	450	"action",
	451	e2,
	452	t2,
	453	NONE));
	454	(TError, loc)))
e680130a	455	\| (TError, _) => t1
dbd7a7d2	456	\| _ => (dte (WrongForm ("Action to be sequenced",
	457	"action",
	458	e1,
	459	t1,
	460	NONE));
	461	(TError, loc))
	462	end
	463
2dc33fa4	464	\| ELocal (e1, e2) =>
dbd7a7d2	465	let
2dc33fa4	466	val t1 = whnorm (checkExp G e1)
2dc33fa4	467	val t2 = whnorm (checkExp G e2)
dbd7a7d2	468	in
2dc33fa4	469	case t1 of
	470	(TAction (p1, d1, r1), _) =>
	471	(case t2 of
	472	(TAction (p2, d2, r2), _) =>
	473	let
	474	val p' = predSimpl (CAnd (p1, p2), loc)
	475
	476	val d' = SM.foldli (fn (name, t, d') =>
	477	case SM.find (r1, name) of
	478	NONE =>
	479	(case SM.find (d', name) of
	480	NONE => SM.insert (d', name, t)
	481	\| SOME t' =>
d68ab27c	482	((case envVarSetFrom name e1 of
	483	NONE => subTyp (t', t)
	484	\| SOME e => hasTyp (e, t', t))
2dc33fa4	485	handle Unify ue =>
	486	dte (WrongType ("Shared environment variable",
	487	(EVar name, loc),
2dc33fa4	488	t',
d68ab27c	489	t,
2dc33fa4	490	SOME ue));
	491	d'))
	492	\| SOME t' =>
d68ab27c	493	((case envVarSetFrom name e1 of
	494	NONE => subTyp (t', t)
	495	\| SOME e => hasTyp (e, t', t))
2dc33fa4	496	handle Unify ue =>
	497	dte (WrongType ("Shared environment variable",
	498	(EVar name, loc),
2dc33fa4	499	t',
d68ab27c	500	t,
2dc33fa4	501	SOME ue));
	502	d'))
	503	d1 d2
	504	in
	505	(TAction (p', d', r2), loc)
	506	end
	507	\| (TError, _) => t2
	508	\| _ => (dte (WrongForm ("Action to be sequenced",
	509	"action",
	510	e2,
	511	t2,
	512	NONE));
	513	(TError, loc)))
	514	\| (TError, _) => t1
	515	\| _ => (dte (WrongForm ("Action to be sequenced",
dbd7a7d2	516	"action",
2dc33fa4	517	e1,
2dc33fa4	518	t1,
dbd7a7d2	519	NONE));
	520	(TError, loc))
	521	end
e680130a	522
2dc33fa4	523
e680130a	524	\| EWith (e1, e2) =>
	525	let
	526	val t1 = whnorm (checkExp G e1)
	527	val t2 = whnorm (checkExp G e2)
	528	in
	529	case t1 of
2dc33fa4	530	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
e680130a	531	(case t2 of
	532	(TAction (p, d, r), _) =>
	533	if predImplies (pd, p) then
2dc33fa4	534	let
	535	val combineRecs =
	536	SM.unionWithi (fn (name, t1, t2) =>
	537	(subTyp (t1, t2)
	538	handle Unify ue =>
	539	dte (WrongType ("Environment variable",
	540	(EVar name, loc),
	541	t1,
	542	t2,
	543	SOME ue));
	544	t2))
	545	in
	546	(TAction (pr, combineRecs (d, d1),
	547	combineRecs (r, r1)), loc)
	548	end
e680130a	549	else
	550	(dte (WrongPred ("nested action",
	551	pd,
	552	p));
	553	(TError, loc))
	554	\| (TError, _) => t2
	555	\| _ =>
	556	(dte (WrongForm ("Body of nested action",
	557	"action",
	558	e2,
	559	t2,
	560	NONE));
	561	(TError, loc)))
	562	\| (TError, _) => t1
	563	\| _ =>
	564	(dte (WrongForm ("Container of nested action",
	565	"action",
	566	e1,
	567	t1,
	568	NONE));
	569	(TError, loc))
	570	end
	571
	572	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	573	SM.empty, SM.empty), loc)
64014a03	574	end
	575
	576	exception Ununif
	577
	578	fun ununif (tAll as (t, loc)) =
	579	case t of
	580	TBase _ => tAll
	581	\| TList t => (TList (ununif t), loc)
	582	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	583	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	584	\| TUnif (_, ref (SOME t)) => ununif t
e680130a	585	\| TNested _ => tAll
64014a03	586	\| TError => tAll
	587
	588	\| TUnif (_, ref NONE) => raise Ununif
	589
	590	fun hasError (t, _) =
	591	case t of
	592	TBase _ => false
	593	\| TList t => hasError t
	594	\| TArrow (d, r) => hasError d orelse hasError r
	595	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	596	orelse List.exists hasError (SM.listItems r)
e680130a	597	\| TNested _ => false
64014a03	598	\| TError => false
	599	\| TUnif (_, ref (SOME t)) => hasError t
	600	\| TUnif (_, ref NONE) => false
	601
	602
	603	fun checkUnit G (eAll as (_, loc)) =
	604	let
	605	val _ = resetUnif ()
	606	val t = checkExp G eAll
	607	in
	608	if hasError t then
	609	t
	610	else
	611	ununif t
	612	handle Ununif =>
	613	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
a4c53cb2	614	output (p_typ t);
64014a03	615	t)
	616	end
	617
e680130a	618	fun checkDecl G (d, _, loc) =
e680130a	619	case d of
89c9edc9	620	DExternType name =>
	621	if !externFlag then
	622	bindType G name
	623	else
	624	(ErrorMsg.error (SOME loc) "'extern type' not allowed in untrusted code";
	625	G)
	626	\| DExternVal (name, t) =>
	627	if !externFlag then
	628	bindVal G (name, checkTyp G t, NONE)
	629	else
	630	(ErrorMsg.error (SOME loc) "'extern val' not allowed in untrusted code";
	631	G)
add6f172	632	\| DVal (name, to, e) =>
	633	let
	634	val to =
	635	case to of
	636	NONE => (newUnif (), loc)
	637	\| SOME to => checkTyp G to
	638
	639	val t = checkExp G e
	640	in
4264c8ef	641	hasTyp (e, t, to)
add6f172	642	handle Unify ue =>
12ad758b	643	Describe.describe_type_error loc
	644	(WrongType ("Bound value",
	645	e,
	646	t,
	647	to,
	648	SOME ue));
add6f172	649	bindVal G (name, to, SOME e)
add6f172	650	end
51c32b45	651	\| DContext name => bindContext G name
e680130a	652
51c32b45	653	fun checkFile G tInit (_, ds, eo) =
e680130a	654	let
	655	val G' = foldl (fn (d, G) => checkDecl G d) G ds
	656	in
	657	case eo of
	658	NONE => ()
	659	\| SOME (e as (_, loc)) =>
	660	let
	661	val t = checkExp G' e
	662	in
4264c8ef	663	hasTyp (e, t, tInit)
e680130a	664	handle Unify ue =>
	665	(ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
	666	preface ("Actual:", p_typ t);
	667	preface ("Needed:", p_typ tInit))
	668	end;
	669	G'
	670	end
	671
64014a03	672	end