[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 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 baseCondition t =
    case whnorm t of
	(TBase name, _) => typeRule name
      | (TList t, _) =>
	(case baseCondition t of
	     NONE => NONE
	   | SOME f => SOME (fn (EList ls, _) => List.all f ls
			      | _ => false))
      | _ => NONE

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

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