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

structure SM = StringMap

type env = typ SM.map
val empty = SM.empty

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)

      | (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

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 predicates.\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")

fun unifyPred (p1All as (p1, _), p2All as (p2, _)) =
    case (p1, p2) of
	(CRoot, CRoot) => ()
      | (CConst s1, CConst s2) =>
	if s1 = s2 then
	    ()
	else
	    raise (Unify (UnifyPred (p1All, p2All)))
      | (CPrefix p1, CPrefix p2) => unifyPred (p1, p2)
      | (CNot p1, CNot p2) => unifyPred (p1, p2)
      | (CAnd (p1, q1), CAnd (p2, q2)) =>
	(unifyPred (p1, p2);
	 unifyPred (q1, q2))

      | _ => raise (Unify (UnifyPred (p1All, p2All)))

fun unifyRecord f (r1, r2) =
    (SM.appi (fn (k, v1) =>
		 case SM.find (r2, k) of
		     NONE => raise UnequalDomains
		   | SOME v2 => f (v1, v2)) r1;
     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)
      | TError => false
      | TUnif (_, ref (SOME t)) => occurs u t
      | TUnif (_, u') => u = u'

fun unify (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) => unify (t1, t2)
      | (TArrow (d1, r1), TArrow (d2, r2)) =>
	(unify (d1, d2);
	 unify (r1, r2))

      | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	((unifyPred (p1, p2);
	  unifyRecord unify (d1, d2);
	  unifyRecord unify (r1, r2))
	 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))

      | (TUnif (_, ref (SOME t1)), _) => unify (t1, t2All)
      | (_, TUnif (_, ref (SOME t2))) => unify (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 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
			      (unify (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 => t

		val G' = SM.insert (G, x, t)
		val t' = checkExp G' e
	    in
		(TArrow (t, t'), loc)
	    end
	  | EVar x =>
	    (case SM.find (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
		(unify (tf, (TArrow (dom, ran), loc));
		 unify (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

	  | _ => raise Fail "Not ready for that expression yet!"
    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
      | 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)
      | 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

end
Commit	Line	Data
	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
	23	open Ast Print
	24
	25	structure SM = StringMap
	26
	27	type env = typ SM.map
	28	val empty = SM.empty
	29
	30	local
	31	val unifCount = ref 0
	32	in
	33	fun resetUnif () = unifCount := 0
	34
	35	fun newUnif () =
	36	let
	37	val c = !unifCount
	38	val name =
	39	if c < 26 then
	40	str (chr (ord #"A" + c))
	41	else
	42	"UNIF" ^ Int.toString (c - 26)
	43	in
	44	unifCount := c + 1;
	45	TUnif (name, ref NONE)
	46	end
	47	end
	48
	49	exception UnequalDomains
	50
	51	fun eqRecord f (r1, r2) =
	52	(SM.appi (fn (k, v1) =>
	53	case SM.find (r2, k) of
	54	NONE => raise UnequalDomains
	55	\| SOME v2 =>
	56	if f (v1, v2) then
	57	()
	58	else
	59	raise UnequalDomains) r1;
	60	SM.appi (fn (k, v2) =>
	61	case SM.find (r1, k) of
	62	NONE => raise UnequalDomains
	63	\| SOME v1 =>
	64	if f (v1, v2) then
	65	()
	66	else
	67	raise UnequalDomains) r2;
	68	true)
	69	handle UnequalDomains => false
	70
	71	fun eqPred ((p1, _), (p2, _)) =
	72	case (p1, p2) of
	73	(CRoot, CRoot) => true
	74	\| (CConst s1, CConst s2) => s1 = s2
	75	\| (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
	76	\| (CNot p1, CNot p2) => eqPred (p1, p2)
	77	\| (CAnd (p1, q1), CAnd (p2, q2)) =>
	78	eqPred (p1, p2) andalso eqPred (q1, q2)
	79
	80	\| _ => false
	81
	82	fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
	83	case (t1, t2) of
	84	(TBase s1, TBase s2) => s1 = s2
	85	\| (TList t1, TList t2) => eqTy (t1, t2)
	86	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
	87	eqTy (d1, d2) andalso eqTy (r1, r2)
	88
	89	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	90	eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
	91	andalso eqRecord eqTy (r1, r2)
	92
	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
	113
	114	fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
	115	[PD.string s, PD.space 1, d]))
	116
	117	fun describe_unification_error t ue =
	118	case ue of
	119	UnifyPred (p1, p2) =>
	120	(print "Reason: Incompatible predicates.\n";
	121	preface ("Have:", p_pred p1);
	122	preface ("Need:", p_pred p2))
	123	\| UnifyTyp (t1, t2) =>
	124	if eqTy (t, t1) then
	125	()
	126	else
	127	(print "Reason: Incompatible types.\n";
	128	preface ("Have:", p_typ t1);
	129	preface ("Need:", p_typ t2))
	130	\| UnifyOccurs (name, t') =>
	131	if eqTy (t, t') then
	132	()
	133	else
	134	(print "Reason: Occurs check failed for ";
	135	print name;
	136	print " in:\n";
	137	printd (p_typ t))
	138
	139	fun describe_type_error loc te =
	140	case te of
	141	WrongType (place, e, t1, t2, ueo) =>
	142	(ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
	143	preface (" Expression:", p_exp e);
	144	preface ("Actual type:", p_typ t1);
	145	preface ("Needed type:", p_typ t2);
	146	Option.app (describe_unification_error t1) ueo)
	147	\| WrongForm (place, form, e, t, ueo) =>
	148	(ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
	149	preface ("Expression:", p_exp e);
	150	preface (" Type:", p_typ t);
	151	Option.app (describe_unification_error t) ueo)
	152	\| UnboundVariable name =>
	153	ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
	154
	155	fun unifyPred (p1All as (p1, _), p2All as (p2, _)) =
	156	case (p1, p2) of
	157	(CRoot, CRoot) => ()
	158	\| (CConst s1, CConst s2) =>
	159	if s1 = s2 then
	160	()
	161	else
	162	raise (Unify (UnifyPred (p1All, p2All)))
	163	\| (CPrefix p1, CPrefix p2) => unifyPred (p1, p2)
	164	\| (CNot p1, CNot p2) => unifyPred (p1, p2)
	165	\| (CAnd (p1, q1), CAnd (p2, q2)) =>
	166	(unifyPred (p1, p2);
	167	unifyPred (q1, q2))
	168
	169	\| _ => raise (Unify (UnifyPred (p1All, p2All)))
	170
	171	fun unifyRecord f (r1, r2) =
	172	(SM.appi (fn (k, v1) =>
	173	case SM.find (r2, k) of
	174	NONE => raise UnequalDomains
	175	\| SOME v2 => f (v1, v2)) r1;
	176	SM.appi (fn (k, v2) =>
	177	case SM.find (r1, k) of
	178	NONE => raise UnequalDomains
	179	\| SOME v1 => f (v1, v2)) r2)
	180
	181	fun occurs u (t, _) =
	182	case t of
	183	TBase _ => false
	184	\| TList t => occurs u t
	185	\| TArrow (d, r) => occurs u d orelse occurs u r
	186	\| TAction (_, d, r) =>
	187	List.exists (occurs u) (SM.listItems d)
	188	orelse List.exists (occurs u) (SM.listItems r)
	189	\| TError => false
	190	\| TUnif (_, ref (SOME t)) => occurs u t
	191	\| TUnif (_, u') => u = u'
	192
	193	fun unify (t1All as (t1, _), t2All as (t2, _)) =
	194	case (t1, t2) of
	195	(TBase s1, TBase s2) =>
	196	if s1 = s2 then
	197	()
	198	else
	199	raise Unify (UnifyTyp (t1All, t2All))
	200	\| (TList t1, TList t2) => unify (t1, t2)
	201	\| (TArrow (d1, r1), TArrow (d2, r2)) =>
	202	(unify (d1, d2);
	203	unify (r1, r2))
	204
	205	\| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
	206	((unifyPred (p1, p2);
	207	unifyRecord unify (d1, d2);
	208	unifyRecord unify (r1, r2))
	209	handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
	210
	211	\| (TUnif (_, ref (SOME t1)), _) => unify (t1, t2All)
	212	\| (_, TUnif (_, ref (SOME t2))) => unify (t1All, t2)
	213
	214	\| (TUnif (_, r1), TUnif (_, r2)) =>
	215	if r1 = r2 then
	216	()
	217	else
	218	r1 := SOME t2All
	219
	220	\| (TUnif (name, r), _) =>
	221	if occurs r t2All then
	222	raise (Unify (UnifyOccurs (name, t2All)))
	223	else
	224	r := SOME t2All
	225
	226	\| (_, TUnif (name, r)) =>
	227	if occurs r t1All then
	228	raise (Unify (UnifyOccurs (name, t1All)))
	229	else
	230	r := SOME t1All
	231
	232	\| (TError, _) => ()
	233	\| (_, TError) => ()
	234
	235	\| _ => raise Unify (UnifyTyp (t1All, t2All))
	236
	237	fun isError t =
	238	case t of
	239	(TError, _) => true
	240	\| _ => false
	241
	242	fun checkExp G (eAll as (e, loc)) =
	243	let
	244	val dte = describe_type_error loc
	245	in
	246	case e of
	247	EInt _ => (TBase "int", loc)
	248	\| EString _ => (TBase "string", loc)
	249	\| EList es =>
	250	let
	251	val t = (newUnif (), loc)
	252	in
	253	foldl (fn (e', ret) =>
	254	let
	255	val t' = checkExp G e'
	256	in
	257	(unify (t', t);
	258	if isError t' then
	259	(TList (TError, loc), loc)
	260	else
	261	ret)
	262	handle Unify ue =>
	263	(dte (WrongType ("List element",
	264	e',
	265	t',
	266	t,
	267	SOME ue));
	268	(TError, loc))
	269	end) (TList t, loc) es
	270	end
	271
	272	\| ELam (x, to, e) =>
	273	let
	274	val t =
	275	case to of
	276	NONE => (newUnif (), loc)
	277	\| SOME t => t
	278
	279	val G' = SM.insert (G, x, t)
	280	val t' = checkExp G' e
	281	in
	282	(TArrow (t, t'), loc)
	283	end
	284	\| EVar x =>
	285	(case SM.find (G, x) of
	286	NONE => (dte (UnboundVariable x);
	287	(TError, loc))
	288	\| SOME t => t)
	289	\| EApp (func, arg) =>
	290	let
	291	val dom = (newUnif (), loc)
	292	val ran = (newUnif (), loc)
	293
	294	val tf = checkExp G func
	295	val ta = checkExp G arg
	296	in
	297	(unify (tf, (TArrow (dom, ran), loc));
	298	unify (ta, dom)
	299	handle Unify ue =>
	300	dte (WrongType ("Function argument",
	301	arg,
	302	ta,
	303	dom,
	304	SOME ue));
	305	ran)
	306	handle Unify ue =>
	307	(dte (WrongForm ("Function to be applied",
	308	"function",
	309	func,
	310	tf,
	311	SOME ue));
	312	(TError, loc))
	313	end
	314
	315	\| _ => raise Fail "Not ready for that expression yet!"
	316	end
	317
	318	exception Ununif
	319
	320	fun ununif (tAll as (t, loc)) =
	321	case t of
	322	TBase _ => tAll
	323	\| TList t => (TList (ununif t), loc)
	324	\| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
	325	\| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
	326	\| TUnif (_, ref (SOME t)) => ununif t
	327	\| TError => tAll
	328
	329	\| TUnif (_, ref NONE) => raise Ununif
	330
	331	fun hasError (t, _) =
	332	case t of
	333	TBase _ => false
	334	\| TList t => hasError t
	335	\| TArrow (d, r) => hasError d orelse hasError r
	336	\| TAction (p, d, r) => List.exists hasError (SM.listItems d)
	337	orelse List.exists hasError (SM.listItems r)
	338	\| TError => false
	339	\| TUnif (_, ref (SOME t)) => hasError t
	340	\| TUnif (_, ref NONE) => false
	341
	342
	343	fun checkUnit G (eAll as (_, loc)) =
	344	let
	345	val _ = resetUnif ()
	346	val t = checkExp G eAll
	347	in
	348	if hasError t then
	349	t
	350	else
	351	ununif t
	352	handle Ununif =>
	353	(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
	354	printd (p_typ t);
	355	t)
	356	end
	357
	358	end