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

(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006, 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

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
	    
exception UnequalDomains
	  
fun eqRecord f (r1, r2) =
    (SM.appi (fn (k, v1) =>
		 case SM.find (r2, k) of
		     NONE => raise UnequalDomains
		   | SOME v2 =>
		     if f (v1, v2) then
			 ()
		     else
			 raise UnequalDomains) r1;
     SM.appi (fn (k, v2) =>
		 case SM.find (r1, k) of
		     NONE => raise UnequalDomains
		   | SOME v1 =>
		     if f (v1, v2) then
			 ()
		     else
			 raise UnequalDomains) r2;
     true)
    handle UnequalDomains => false

fun eqPred ((p1, _), (p2, _)) =
    case (p1, p2) of
	(CRoot, CRoot) => true
      | (CConst s1, CConst s2) => s1 = s2
      | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
      | (CNot p1, CNot p2) => eqPred (p1, p2)
      | (CAnd (p1, q1), CAnd (p2, q2)) =>
	eqPred (p1, p2) andalso eqPred (q1, q2)

      | _ => false

fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
    case (t1, t2) of
	(TBase s1, TBase s2) => s1 = s2
      | (TList t1, TList t2) => eqTy (t1, t2)
      | (TArrow (d1, r1), TArrow (d2, r2)) =>
	eqTy (d1, d2) andalso eqTy (r1, r2)

      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
	andalso eqRecord eqTy (r1, r2)

      | (TNested (p1, q1), TNested (p2, q2)) =>
	eqPred (p1, p2) andalso eqTy (q1, q2)

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

      | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2

      | (TError, TError) => true

      | _ => false

datatype unification_error =
	 UnifyPred of pred * pred
       | UnifyTyp of typ * typ
       | UnifyOccurs of string * typ

exception Unify of unification_error

datatype type_error =
	 WrongType of string * exp * typ * typ * unification_error option
       | WrongForm of string * string * exp * typ * unification_error option
       | UnboundVariable of string
       | WrongPred of string * pred * pred

fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
					[PD.string s, PD.space 1, d]))

fun describe_unification_error t ue =
    case ue of
	UnifyPred (p1, p2) =>
	(print "Reason: Incompatible contexts.\n";
	 preface ("Have:", p_pred p1);
	 preface ("Need:", p_pred p2))
      | UnifyTyp (t1, t2) =>
	if eqTy (t, t1) then
	    ()
	else
	    (print "Reason: Incompatible types.\n";
	     preface ("Have:", p_typ t1);
	     preface ("Need:", p_typ t2))
      | UnifyOccurs (name, t') =>
	if eqTy (t, t') then
	    ()
	else
	    (print "Reason: Occurs check failed for ";
	     print name;
	     print " in:\n";
	     printd (p_typ t))

fun describe_type_error loc te =
    case te of
	WrongType (place, e, t1, t2, ueo) =>
	(ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
	 preface (" Expression:", p_exp e);
	 preface ("Actual type:", p_typ t1);
	 preface ("Needed type:", p_typ t2);
	 Option.app (describe_unification_error t1) ueo)
      |	WrongForm (place, form, e, t, ueo) =>
	(ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
	 preface ("Expression:", p_exp e);
	 preface ("      Type:", p_typ t);
	 Option.app (describe_unification_error t) ueo)
      | UnboundVariable name =>
	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
      |	WrongPred (place, p1, p2) =>
	(ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
	 preface ("Have:", p_pred p1);
	 preface ("Need:", p_pred p2))

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)

      | _ => 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 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 hasTyp (e, t1, t2) =
    case whnorm t2 of
	(TBase name, _) =>
	(case typeRule name of
	     NONE => subTyp (t1, t2)
	   | SOME rule =>
	     if rule e then
		 ()
	     else
		 subTyp (t1, t2))
      | _ => subTyp (t1, t2)

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) => (TAction (p, SM.map (checkTyp G) d,
					   SM.map (checkTyp G) r), loc)
	  | TNested (p, t) => (TNested (p, checkTyp G t), loc)
	  | TError => raise Fail "TError in parser-generated type"
	  | TUnif _ => raise Fail "TUnif in parser-generated type"
    end

fun checkExp G (eAll as (e, loc)) =
    let
	val dte = 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

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

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

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

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

			     val d' = SM.foldli (fn (name, t, d') =>
						    case SM.find (r1, name) of
							NONE =>
							(case SM.find (d', name) of
							     NONE => SM.insert (d', name, t)
							   | SOME t' =>
							     (subTyp (t, t')
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t,
										     t',
										     SOME ue));
							      d'))
						      | SOME t' =>
							(subTyp (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' =>
							     (subTyp (t, t')
							      handle Unify ue =>
								     dte (WrongType ("Shared environment variable",
										     (EVar name, loc),
										     t,
										     t',
										     SOME ue));
							      d'))
						      | SOME t' =>
							(subTyp (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:";
		    printd (p_typ t);
		    t)
    end

fun checkDecl G (d, _, loc) =
    case d of
	DExternType name => bindType G name
      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
      | 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_type_error loc
				       (WrongType ("Bound value",
						   e,
						   t,
						   to,
						   SOME ue));
	    bindVal G (name, to, SOME e)
	end

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/)
	2	* Copyright (c) 2006, Adam Chlipala
	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.
	17	*)
	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
64014a03	27	local
	28	val unifCount = ref 0
	29	in
	30	fun resetUnif () = unifCount := 0
	31
	32	fun newUnif () =
	33	let
	34	val c = !unifCount
	35	val name =
	36	if c < 26 then
	37	str (chr (ord #"A" + c))
	38	else
	39	"UNIF" ^ Int.toString (c - 26)
	40	in
	41	unifCount := c + 1;
	42	TUnif (name, ref NONE)
	43	end
	44	end
	45
	46	exception UnequalDomains
	47
	48	fun eqRecord f (r1, r2) =
	49	(SM.appi (fn (k, v1) =>
	50	case SM.find (r2, k) of
	51	NONE => raise UnequalDomains
	52	\| SOME v2 =>
	53	if f (v1, v2) then
	54	()
	55	else
	56	raise UnequalDomains) r1;
	57	SM.appi (fn (k, v2) =>
	58	case SM.find (r1, k) of
	59	NONE => raise UnequalDomains
	60	\| SOME v1 =>
	61	if f (v1, v2) then
	62	()
	63	else
	64	raise UnequalDomains) r2;
	65	true)
	66	handle UnequalDomains => false
	67
	68	fun eqPred ((p1, _), (p2, _)) =
	69	case (p1, p2) of
	70	(CRoot, CRoot) => true
	71	\| (CConst s1, CConst s2) => s1 = s2
	72	\| (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
	73	\| (CNot p1, CNot p2) => eqPred (p1, p2)
	74	\| (CAnd (p1, q1), CAnd (p2, q2)) =>
	75	eqPred (p1, p2) andalso eqPred (q1, q2)
	76
	77	\| _ => false
	78
	79	fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
	80	case (t1, t2) of
	81	(TBase s1, TBase s2) => s1 = s2
	82	\| (TList t1, TList t2) => eqTy (t1, t2)
	83	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
	84	eqTy (d1, d2) andalso eqTy (r1, r2)
	85
	86	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	87	eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
	88	andalso eqRecord eqTy (r1, r2)
	89
e680130a	90	\| (TNested (p1, q1), TNested (p2, q2)) =>
2dc33fa4	91	eqPred (p1, p2) andalso eqTy (q1, q2)
e680130a	92
64014a03	93	\| (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
	94	\| (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
	95
	96	\| (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
	97
	98	\| (TError, TError) => true
	99
	100	\| _ => false
	101
	102	datatype unification_error =
	103	UnifyPred of pred * pred
	104	\| UnifyTyp of typ * typ
	105	\| UnifyOccurs of string * typ
	106
	107	exception Unify of unification_error
	108
	109	datatype type_error =
	110	WrongType of string * exp * typ * typ * unification_error option
	111	\| WrongForm of string * string * exp * typ * unification_error option
	112	\| UnboundVariable of string
e680130a	113	\| WrongPred of string * pred * pred
64014a03	114
	115	fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
	116	[PD.string s, PD.space 1, d]))
	117
	118	fun describe_unification_error t ue =
	119	case ue of
	120	UnifyPred (p1, p2) =>
e680130a	121	(print "Reason: Incompatible contexts.\n";
64014a03	122	preface ("Have:", p_pred p1);
	123	preface ("Need:", p_pred p2))
	124	\| UnifyTyp (t1, t2) =>
	125	if eqTy (t, t1) then
	126	()
	127	else
	128	(print "Reason: Incompatible types.\n";
	129	preface ("Have:", p_typ t1);
	130	preface ("Need:", p_typ t2))
	131	\| UnifyOccurs (name, t') =>
	132	if eqTy (t, t') then
	133	()
	134	else
	135	(print "Reason: Occurs check failed for ";
	136	print name;
	137	print " in:\n";
	138	printd (p_typ t))
	139
	140	fun describe_type_error loc te =
	141	case te of
	142	WrongType (place, e, t1, t2, ueo) =>
	143	(ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
	144	preface (" Expression:", p_exp e);
	145	preface ("Actual type:", p_typ t1);
	146	preface ("Needed type:", p_typ t2);
	147	Option.app (describe_unification_error t1) ueo)
	148	\| WrongForm (place, form, e, t, ueo) =>
	149	(ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
	150	preface ("Expression:", p_exp e);
	151	preface (" Type:", p_typ t);
	152	Option.app (describe_unification_error t) ueo)
	153	\| UnboundVariable name =>
	154	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
e680130a	155	\| WrongPred (place, p1, p2) =>
	156	(ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
	157	preface ("Have:", p_pred p1);
	158	preface ("Need:", p_pred p2))
64014a03	159
dbd7a7d2	160	fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
64014a03	161	case (p1, p2) of
2dc33fa4	162	(_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
	163	\| (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
	164
	165	\| (_, CPrefix (CRoot, _)) => true
dbd7a7d2	166	\| (CNot (CPrefix (CRoot, _), _), _) => true
	167
	168	\| (CRoot, CRoot) => true
	169
	170	\| (CConst s1, CConst s2) => s1 = s2
	171
	172	\| (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
e680130a	173	\| (_, CPrefix p2) => predImplies (p1All, p2)
dbd7a7d2	174
dbd7a7d2	175	\| (CNot p1, CNot p2) => predImplies (p2, p1)
64014a03	176
dbd7a7d2	177	\| _ => false
	178
	179	fun predSimpl (pAll as (p, loc)) =
	180	case p of
	181	CRoot => pAll
	182	\| CConst _ => pAll
	183	\| CPrefix p => (CPrefix (predSimpl p), loc)
	184	\| CNot p => (CNot (predSimpl p), loc)
	185	\| CAnd (p1, p2) =>
	186	let
	187	val p1' = predSimpl p1
	188	val p2' = predSimpl p2
	189	in
	190	case p1' of
	191	(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
	192	\| _ => if predImplies (p2', p1') then
	193	p2'
2dc33fa4	194	else if predImplies (p1', p2') then
2dc33fa4	195	p1'
dbd7a7d2	196	else
	197	(CAnd (p1', p2'), loc)
	198	end
	199
e680130a	200	fun subPred (p1, p2) =
dbd7a7d2	201	if predImplies (p1, p2) then
	202	()
	203	else
	204	raise (Unify (UnifyPred (p1, p2)))
64014a03	205
e680130a	206	fun subRecord f (r1, r2) =
	207	SM.appi (fn (k, v2) =>
	208	case SM.find (r1, k) of
	209	NONE => raise UnequalDomains
	210	\| SOME v1 => f (v1, v2)) r2
64014a03	211
	212	fun occurs u (t, _) =
	213	case t of
	214	TBase _ => false
	215	\| TList t => occurs u t
	216	\| TArrow (d, r) => occurs u d orelse occurs u r
	217	\| TAction (_, d, r) =>
	218	List.exists (occurs u) (SM.listItems d)
	219	orelse List.exists (occurs u) (SM.listItems r)
2dc33fa4	220	\| TNested (_, t) => occurs u t
64014a03	221	\| TError => false
	222	\| TUnif (_, ref (SOME t)) => occurs u t
	223	\| TUnif (_, u') => u = u'
	224
e680130a	225	fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
64014a03	226	case (t1, t2) of
	227	(TBase s1, TBase s2) =>
	228	if s1 = s2 then
	229	()
	230	else
	231	raise Unify (UnifyTyp (t1All, t2All))
e680130a	232	\| (TList t1, TList t2) => subTyp (t1, t2)
64014a03	233	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
e680130a	234	(subTyp (d2, d1);
e680130a	235	subTyp (r1, r2))
64014a03	236
64014a03	237	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
e680130a	238	((subPred (p2, p1);
	239	subRecord subTyp (d2, d1);
	240	subRecord subTyp (r1, r2);
	241	subRecord subTyp (r2, r1))
64014a03	242	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
64014a03	243
e680130a	244	\| (TNested (d1, r1), TNested (d2, r2)) =>
e680130a	245	(subPred (d2, d1);
2dc33fa4	246	subTyp (r1, r2))
e680130a	247
	248	\| (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
	249	\| (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
64014a03	250
	251	\| (TUnif (_, r1), TUnif (_, r2)) =>
	252	if r1 = r2 then
	253	()
	254	else
	255	r1 := SOME t2All
	256
	257	\| (TUnif (name, r), _) =>
	258	if occurs r t2All then
	259	raise (Unify (UnifyOccurs (name, t2All)))
	260	else
	261	r := SOME t2All
	262
	263	\| (_, TUnif (name, r)) =>
	264	if occurs r t1All then
	265	raise (Unify (UnifyOccurs (name, t1All)))
	266	else
	267	r := SOME t1All
	268
	269	\| (TError, _) => ()
	270	\| (_, TError) => ()
	271
	272	\| _ => raise Unify (UnifyTyp (t1All, t2All))
	273
	274	fun isError t =
	275	case t of
	276	(TError, _) => true
	277	\| _ => false
	278
dbd7a7d2	279	fun whnorm (tAll as (t, loc)) =
	280	case t of
	281	TUnif (_, ref (SOME tAll)) => whnorm tAll
	282	\| _ => tAll
	283
4264c8ef	284	fun hasTyp (e, t1, t2) =
	285	case whnorm t2 of
	286	(TBase name, _) =>
	287	(case typeRule name of
	288	NONE => subTyp (t1, t2)
	289	\| SOME rule =>
	290	if rule e then
	291	()
	292	else
	293	subTyp (t1, t2))
	294	\| _ => subTyp (t1, t2)
	295
e680130a	296	fun checkTyp G (tAll as (t, loc)) =
	297	let
	298	val err = ErrorMsg.error (SOME loc)
	299	in
	300	case t of
	301	TBase name =>
	302	if lookupType G name then
	303	tAll
	304	else
	305	(err ("Unbound type name " ^ name);
	306	(TError, loc))
	307	\| TList t => (TList (checkTyp G t), loc)
	308	\| TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
	309	\| TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
	310	SM.map (checkTyp G) r), loc)
2dc33fa4	311	\| TNested (p, t) => (TNested (p, checkTyp G t), loc)
e680130a	312	\| TError => raise Fail "TError in parser-generated type"
	313	\| TUnif _ => raise Fail "TUnif in parser-generated type"
	314	end
	315
64014a03	316	fun checkExp G (eAll as (e, loc)) =
	317	let
	318	val dte = describe_type_error loc
	319	in
	320	case e of
	321	EInt _ => (TBase "int", loc)
	322	\| EString _ => (TBase "string", loc)
	323	\| EList es =>
	324	let
	325	val t = (newUnif (), loc)
	326	in
	327	foldl (fn (e', ret) =>
	328	let
	329	val t' = checkExp G e'
	330	in
4264c8ef	331	(hasTyp (eAll, t', t);
64014a03	332	if isError t' then
	333	(TList (TError, loc), loc)
	334	else
	335	ret)
	336	handle Unify ue =>
	337	(dte (WrongType ("List element",
	338	e',
	339	t',
	340	t,
	341	SOME ue));
	342	(TError, loc))
	343	end) (TList t, loc) es
	344	end
	345
	346	\| ELam (x, to, e) =>
	347	let
	348	val t =
	349	case to of
	350	NONE => (newUnif (), loc)
e680130a	351	\| SOME t => checkTyp G t
64014a03	352
add6f172	353	val G' = bindVal G (x, t, NONE)
64014a03	354	val t' = checkExp G' e
	355	in
	356	(TArrow (t, t'), loc)
	357	end
	358	\| EVar x =>
e680130a	359	(case lookupVal G x of
64014a03	360	NONE => (dte (UnboundVariable x);
	361	(TError, loc))
	362	\| SOME t => t)
	363	\| EApp (func, arg) =>
	364	let
	365	val dom = (newUnif (), loc)
	366	val ran = (newUnif (), loc)
	367
	368	val tf = checkExp G func
	369	val ta = checkExp G arg
	370	in
4264c8ef	371	(hasTyp (func, tf, (TArrow (dom, ran), loc));
4264c8ef	372	hasTyp (arg, ta, dom)
64014a03	373	handle Unify ue =>
	374	dte (WrongType ("Function argument",
	375	arg,
	376	ta,
	377	dom,
	378	SOME ue));
	379	ran)
	380	handle Unify ue =>
	381	(dte (WrongForm ("Function to be applied",
	382	"function",
	383	func,
	384	tf,
	385	SOME ue));
	386	(TError, loc))
	387	end
dbd7a7d2	388
	389	\| ESet (evar, e) =>
	390	let
	391	val t = checkExp G e
	392	in
	393	(TAction ((CPrefix (CRoot, loc), loc),
	394	SM.empty,
	395	SM.insert (SM.empty, evar, t)),
	396	loc)
	397	end
	398	\| EGet (x, evar, rest) =>
	399	let
	400	val xt = (newUnif (), loc)
add6f172	401	val G' = bindVal G (x, xt, NONE)
dbd7a7d2	402
	403	val rt = whnorm (checkExp G' rest)
	404	in
	405	case rt of
	406	(TAction (p, d, r), _) =>
	407	(case SM.find (d, evar) of
	408	NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
	409	\| SOME xt' =>
e680130a	410	(subTyp (xt', xt)
dbd7a7d2	411	handle Unify ue =>
	412	dte (WrongType ("Retrieved environment variable",
	413	(EVar x, loc),
	414	xt',
	415	xt,
	416	SOME ue));
	417	rt))
e680130a	418	\| (TError, _) => rt
dbd7a7d2	419	\| _ => (dte (WrongForm ("Body of environment variable read",
	420	"action",
	421	rest,
	422	rt,
	423	NONE));
	424	(TError, loc))
	425	end
	426
	427	\| ESeq [] => raise Fail "Empty ESeq"
	428	\| ESeq [e1] => checkExp G e1
	429	\| ESeq (e1 :: rest) =>
	430	let
	431	val e2 = (ESeq rest, loc)
	432
	433	val t1 = whnorm (checkExp G e1)
	434	val t2 = whnorm (checkExp G e2)
	435	in
	436	case t1 of
	437	(TAction (p1, d1, r1), _) =>
	438	(case t2 of
	439	(TAction (p2, d2, r2), _) =>
	440	let
	441	val p' = predSimpl (CAnd (p1, p2), loc)
	442
	443	val d' = SM.foldli (fn (name, t, d') =>
	444	case SM.find (r1, name) of
	445	NONE =>
	446	(case SM.find (d', name) of
	447	NONE => SM.insert (d', name, t)
	448	\| SOME t' =>
e680130a	449	(subTyp (t, t')
dbd7a7d2	450	handle Unify ue =>
	451	dte (WrongType ("Shared environment variable",
	452	(EVar name, loc),
	453	t,
	454	t',
	455	SOME ue));
	456	d'))
	457	\| SOME t' =>
e680130a	458	(subTyp (t, t')
dbd7a7d2	459	handle Unify ue =>
	460	dte (WrongType ("Shared environment variable",
	461	(EVar name, loc),
	462	t,
	463	t',
	464	SOME ue));
	465	d'))
	466	d1 d2
	467
	468	val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
	469	r1 r2
	470	in
	471	(TAction (p', d', r'), loc)
	472	end
e680130a	473	\| (TError, _) => t2
dbd7a7d2	474	\| _ => (dte (WrongForm ("Action to be sequenced",
	475	"action",
	476	e2,
	477	t2,
	478	NONE));
	479	(TError, loc)))
e680130a	480	\| (TError, _) => t1
dbd7a7d2	481	\| _ => (dte (WrongForm ("Action to be sequenced",
	482	"action",
	483	e1,
	484	t1,
	485	NONE));
	486	(TError, loc))
	487	end
	488
2dc33fa4	489	\| ELocal (e1, e2) =>
dbd7a7d2	490	let
2dc33fa4	491	val t1 = whnorm (checkExp G e1)
2dc33fa4	492	val t2 = whnorm (checkExp G e2)
dbd7a7d2	493	in
2dc33fa4	494	case t1 of
	495	(TAction (p1, d1, r1), _) =>
	496	(case t2 of
	497	(TAction (p2, d2, r2), _) =>
	498	let
	499	val p' = predSimpl (CAnd (p1, p2), loc)
	500
	501	val d' = SM.foldli (fn (name, t, d') =>
	502	case SM.find (r1, name) of
	503	NONE =>
	504	(case SM.find (d', name) of
	505	NONE => SM.insert (d', name, t)
	506	\| SOME t' =>
	507	(subTyp (t, t')
	508	handle Unify ue =>
	509	dte (WrongType ("Shared environment variable",
	510	(EVar name, loc),
	511	t,
	512	t',
	513	SOME ue));
	514	d'))
	515	\| SOME t' =>
	516	(subTyp (t, t')
	517	handle Unify ue =>
	518	dte (WrongType ("Shared environment variable",
	519	(EVar name, loc),
	520	t,
	521	t',
	522	SOME ue));
	523	d'))
	524	d1 d2
	525	in
	526	(TAction (p', d', r2), loc)
	527	end
	528	\| (TError, _) => t2
	529	\| _ => (dte (WrongForm ("Action to be sequenced",
	530	"action",
	531	e2,
	532	t2,
	533	NONE));
	534	(TError, loc)))
	535	\| (TError, _) => t1
	536	\| _ => (dte (WrongForm ("Action to be sequenced",
dbd7a7d2	537	"action",
2dc33fa4	538	e1,
2dc33fa4	539	t1,
dbd7a7d2	540	NONE));
	541	(TError, loc))
	542	end
e680130a	543
2dc33fa4	544
e680130a	545	\| EWith (e1, e2) =>
	546	let
	547	val t1 = whnorm (checkExp G e1)
	548	val t2 = whnorm (checkExp G e2)
	549	in
	550	case t1 of
2dc33fa4	551	(TNested (pd, (TAction (pr, d1, r1), _)), _) =>
e680130a	552	(case t2 of
	553	(TAction (p, d, r), _) =>
	554	if predImplies (pd, p) then
2dc33fa4	555	let
	556	val combineRecs =
	557	SM.unionWithi (fn (name, t1, t2) =>
	558	(subTyp (t1, t2)
	559	handle Unify ue =>
	560	dte (WrongType ("Environment variable",
	561	(EVar name, loc),
	562	t1,
	563	t2,
	564	SOME ue));
	565	t2))
	566	in
	567	(TAction (pr, combineRecs (d, d1),
	568	combineRecs (r, r1)), loc)
	569	end
e680130a	570	else
	571	(dte (WrongPred ("nested action",
	572	pd,
	573	p));
	574	(TError, loc))
	575	\| (TError, _) => t2
	576	\| _ =>
	577	(dte (WrongForm ("Body of nested action",
	578	"action",
	579	e2,
	580	t2,
	581	NONE));
	582	(TError, loc)))
	583	\| (TError, _) => t1
	584	\| _ =>
	585	(dte (WrongForm ("Container of nested action",
	586	"action",
	587	e1,
	588	t1,
	589	NONE));
	590	(TError, loc))
	591	end
	592
	593	\| ESkip => (TAction ((CPrefix (CRoot, loc), loc),
	594	SM.empty, SM.empty), loc)
64014a03	595	end
	596
	597	exception Ununif
	598
	599	fun ununif (tAll as (t, loc)) =
	600	case t of
	601	TBase _ => tAll
	602	\| TList t => (TList (ununif t), loc)
	603	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	604	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	605	\| TUnif (_, ref (SOME t)) => ununif t
e680130a	606	\| TNested _ => tAll
64014a03	607	\| TError => tAll
	608
	609	\| TUnif (_, ref NONE) => raise Ununif
	610
	611	fun hasError (t, _) =
	612	case t of
	613	TBase _ => false
	614	\| TList t => hasError t
	615	\| TArrow (d, r) => hasError d orelse hasError r
	616	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	617	orelse List.exists hasError (SM.listItems r)
e680130a	618	\| TNested _ => false
64014a03	619	\| TError => false
	620	\| TUnif (_, ref (SOME t)) => hasError t
	621	\| TUnif (_, ref NONE) => false
	622
	623
	624	fun checkUnit G (eAll as (_, loc)) =
	625	let
	626	val _ = resetUnif ()
	627	val t = checkExp G eAll
	628	in
	629	if hasError t then
	630	t
	631	else
	632	ununif t
	633	handle Ununif =>
	634	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
	635	printd (p_typ t);
	636	t)
	637	end
	638
e680130a	639	fun checkDecl G (d, _, loc) =
	640	case d of
	641	DExternType name => bindType G name
add6f172	642	\| DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
	643	\| DVal (name, to, e) =>
	644	let
	645	val to =
	646	case to of
	647	NONE => (newUnif (), loc)
	648	\| SOME to => checkTyp G to
	649
	650	val t = checkExp G e
	651	in
4264c8ef	652	hasTyp (e, t, to)
add6f172	653	handle Unify ue =>
	654	describe_type_error loc
	655	(WrongType ("Bound value",
	656	e,
	657	t,
	658	to,
	659	SOME ue));
	660	bindVal G (name, to, SOME e)
	661	end
e680130a	662
	663	fun checkFile G tInit (ds, eo) =
	664	let
	665	val G' = foldl (fn (d, G) => checkDecl G d) G ds
	666	in
	667	case eo of
	668	NONE => ()
	669	\| SOME (e as (_, loc)) =>
	670	let
	671	val t = checkExp G' e
	672	in
4264c8ef	673	hasTyp (e, t, tInit)
e680130a	674	handle Unify ue =>
	675	(ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
	676	preface ("Actual:", p_typ t);
	677	preface ("Needed:", p_typ tInit))
	678	end;
	679	G'
	680	end
	681
64014a03	682	end