[hcoop/debian/mlton.git] / mlton / xml / type-check.fun

(* Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh
 *    Jagannathan, and Stephen Weeks.
 * Copyright (C) 1997-2000 NEC Research Institute.
 *
 * MLton is released under a BSD-style license.
 * See the file MLton-LICENSE for details.
 *)

functor TypeCheck (S: TYPE_CHECK_STRUCTS): TYPE_CHECK = 
struct

open S
open Dec PrimExp

fun typeCheck (program as Program.T {datatypes, body, overflow}): unit =
   let
      (* tyvarInScope is used to ensure that tyvars never shadow themselves. *)
      val {get = tyvarInScope: Tyvar.t -> bool ref, ...} =
         Property.get (Tyvar.plist,
                       Property.initFun (fn _ => ref false))
      fun bindTyvars (vs: Tyvar.t vector): unit =
         Vector.foreach (vs, fn v =>
                         let
                            val r = tyvarInScope v
                         in
                            if !r
                               then Type.error ("tyvar already in scope",
                                                Tyvar.layout v)
                            else r := true
                         end)
      fun unbindTyvars (vs: Tyvar.t vector): unit =
         Vector.foreach (vs, fn v => tyvarInScope v := false)
      (* checkType makes sure all tyvars are bound. *)
      fun checkType (ty: Type.t): unit =
         Type.hom {ty = ty,
                   con = fn _ => (),
                   var = fn a => if !(tyvarInScope a)
                                    then ()
                                 else Type.error ("tyvar not in scope",
                                                  Tyvar.layout a)}
      fun checkTypes v = Vector.foreach (v, checkType)
      val {get = getCon: Con.t -> {tyvars: Tyvar.t vector, ty: Type.t},
           set, ...} =
         Property.getSetOnce (Con.plist,
                              Property.initRaise ("scheme", Con.layout))
      fun setCon ({con, arg}, tyvars, result: Type.t): unit =
         (checkType result
          ; set (con, {tyvars = tyvars,
                       ty = (case arg of
                                NONE => result
                              | SOME ty => (checkType ty
                                            ; Type.arrow (ty, result)))}))
      fun checkConExp (c: Con.t, ts: Type.t vector): Type.t =
         let
            val _ = checkTypes ts
            val {tyvars, ty} = getCon c
         in
            Type.substitute (ty, Vector.zip (tyvars, ts))
         end
      val {get = getVar: Var.t -> {tyvars: Tyvar.t vector, ty: Type.t},
           set = setVar, ...} =
         Property.getSet (Var.plist,
                          Property.initRaise ("var scheme", Var.layout))
      val getVar = 
         Trace.trace 
         ("Xml.TypeCheck.getVar", Var.layout, fn {tyvars, ty} =>
          Layout.record [("tyvars", Vector.layout Tyvar.layout tyvars),
                         ("ty", Type.layout ty)])
         getVar
      val setVar = 
         Trace.trace2 
         ("Xml.TypeCheck.setVar", Var.layout, fn {tyvars, ty} =>
          Layout.record [("tyvars", Vector.layout Tyvar.layout tyvars),
                         ("ty", Type.layout ty)], 
          Layout.ignore)
         setVar
      fun checkVarExp (VarExp.T {var, targs}): Type.t =
         let
            val _ = checkTypes targs
            val {tyvars, ty} = getVar var
         in if Vector.length targs = Vector.length tyvars
               then Type.substitute (ty, Vector.zip (tyvars, targs))
            else
               Type.error ("variable applied to wrong number of type args",
                          let open Layout
                          in align [Var.layout var,
                                   seq [str "tyvars: ",
                                        Vector.layout Tyvar.layout tyvars],
                                   seq [str "targs: ",
                                        Vector.layout Type.layout targs]]
                            end)
         end
      fun checkVarExps xs = Vector.map (xs, checkVarExp)
      fun checkPat (p as Pat.T {con, targs, arg}): Type.t =
         let
            val t = checkConExp (con, targs)
         in
            case (arg, Type.deArrowOpt t) of
                 (NONE, NONE) => t
               | (SOME (x, ty), SOME (t1, t2)) =>
                    (checkType ty
                     ; if Type.equals (t1, ty)
                          then (setVar (x, {tyvars = Vector.new0 (),
                                            ty = t1}) ; t2)
                       else (Type.error
                             ("argument constraint of wrong type",
                              let open Layout
                              in align [seq [str "constructor expects : ", Type.layout t1],
                                        seq [str "but got: ", Type.layout ty],
                                        seq [str "p: ", Pat.layout p]]
                              end)))
               | _ => Type.error ("constructor pattern mismatch", Pat.layout p)
         end
      val traceCheckExp =
         Trace.trace 
         ("Xml.TypeCheck.checkExp", Exp.layout, Type.layout)
      val traceCheckPrimExp = 
         Trace.trace2
         ("Xml.TypeCheck.checkPrimExp", PrimExp.layout, Type.layout, Type.layout)
      val traceCheckLambda = 
         Trace.trace 
         ("Xml.TypeCheck.checkLambda", Lambda.layout, Type.layout)
      val traceCheckDec = 
         Trace.trace 
         ("Xml.TypeCheck.checkDec", Dec.layout, Unit.layout)
      local
         val exnType = ref NONE
      in
         fun isExnType t =
            case !exnType of
               NONE => (exnType := SOME t; true)
             | SOME t' => Type.equals (t, t')
      end
      fun check (t: Type.t, t': Type.t, layout: unit -> Layout.t): unit =
         if Type.equals (t, t')
            then ()
         else Type.error ("type mismatch",
                          Layout.align [Type.layout t,
                                        Type.layout t',
                                        layout ()])
      fun checkExp arg: Type.t =
         traceCheckExp
         (fn (exp: Exp.t) =>
          let val {decs, result} = Exp.dest exp
          in List.foreach (decs, checkDec)
             ; checkVarExp result
          end) arg
      and checkPrimExp arg: Type.t =
         traceCheckPrimExp
         (fn (e: PrimExp.t, ty: Type.t) => 
         let
            fun error msg =
               Type.error (msg, let open Layout
                                in seq [str "exp: ", PrimExp.layout e]
                                end)
            fun checkApp (t1, x) =
               let
                  val t2 = checkVarExp x
               in
                  case Type.deArrowOpt t1 of
                     NONE => error "function not of arrow type"
                   | SOME (t2', t3) =>
                        if Type.equals (t2, t2') then t3
                        else
                           Type.error
                           ("actual and formal not of same type",
                            let open Layout
                            in align [seq [str "actual: ", Type.layout t2],
                                      seq [str "formal: ", Type.layout t2'],
                                      seq [str "expression: ",
                                           PrimExp.layout e]]
                            end)
               end
         in
            case e of
               App {arg, func} => checkApp (checkVarExp func, arg)
             | Case {cases, default, test} =>
                  let
                     val default = Option.map (default, checkExp o #1)
                     fun equalss v =
                        if Vector.isEmpty v
                           then Error.bug "Xml.TypeCheck.equalss"
                        else
                           let
                              val t = Vector.first v
                           in
                              if Vector.forall (v, fn t' => Type.equals (t, t'))
                                 then SOME t
                              else NONE
                           end
                     fun finish (ptys: Type.t vector,
                                 etys: Type.t vector): Type.t =
                        case (equalss ptys, equalss etys) of
                           (NONE, _) => error "patterns not of same type"
                         | (_, NONE) => error "branches not of same type"
                         | (SOME pty, SOME ety) =>
                              if Type.equals (checkVarExp test, pty)
                                 then
                                    case default of
                                       NONE => ety
                                     | SOME t =>
                                          if Type.equals (ety, t)
                                             then ety
                                          else error "default of wrong type"
                              else error "test and patterns of different types"
                     datatype z = datatype Cases.t
                  in
                     case cases of
                        Con cases =>
                           finish (Vector.unzip
                                   (Vector.map (cases, fn (p, e) =>
                                                (checkPat p, checkExp e))))
                      | Word (s, cs) =>
                           finish (Vector.new1 (Type.word s),
                                   Vector.map (cs, fn (_, e) => checkExp e))
                  end
             | ConApp {con, targs, arg} =>
                  let
                     val t = checkConExp (con, targs)
                  in
                     case arg of
                        NONE => t
                      | SOME e => checkApp (t, e)
                  end
             | Const c => Type.ofConst c
             | Handle {try, catch = (catch, catchType), handler, ...} =>
                  let
                     val _ = if isExnType catchType
                                then ()
                             else error "handle with non-exn type for catch"
                     val ty = checkExp try
                     val _ = setVar (catch, {tyvars = Vector.new0 (),
                                             ty = catchType})
                     val ty' = checkExp handler
                  in
                     if Type.equals (ty, ty')
                        then ty
                     else error "bad handle"
                  end
             | Lambda l => checkLambda l
             | PrimApp {args, prim, targs} =>
                  let
                     val _ = checkTypes targs
                     val () =
                        if Type.checkPrimApp {args = checkVarExps args,
                                              prim = prim,
                                              result = ty,
                                              targs = targs}
                           then ()
                        else error "bad primapp"
                  in
                     ty
                  end
             | Profile _ => Type.unit
             | Raise {exn, ...} =>
                  if isExnType (checkVarExp exn)
                     then ty
                  else error "bad raise"
             | Select {tuple, offset} =>
                  (case Type.deTupleOpt (checkVarExp tuple) of
                      NONE => error "selection from nontuple"
                    | SOME ts => Vector.sub (ts, offset))
             | Tuple xs =>
                  if 1 = Vector.length xs
                     then error "unary tuple"
                  else Type.tuple (checkVarExps xs)
             | Var x => checkVarExp x
         end) arg
      and checkLambda arg: Type.t =
         traceCheckLambda
         (fn (l: Lambda.t) =>
         let
            val {arg, argType, body, ...} = Lambda.dest l
            val _ = checkType argType
            val _ = setVar (arg, {tyvars = Vector.new0 (), ty = argType})
         in
            Type.arrow (argType, checkExp body)
         end) arg
      and checkDec arg: unit =
         traceCheckDec
         (fn (d: Dec.t) =>
         let
            val check = fn (t, t') => check (t, t', fn () => Dec.layout d)
         in
            case d of
               Exception c => setCon (c, Vector.new0 (), Type.exn)
             | Fun {tyvars, decs} =>
                  (bindTyvars tyvars
                   ; (Vector.foreach
                      (decs, fn {ty, var, ...} =>
                       (checkType ty
                        ; setVar (var, {tyvars = tyvars, ty = ty}))))
                   ; Vector.foreach (decs, fn {ty, lambda, ...} =>
                                     check (ty, checkLambda lambda))
                   ; unbindTyvars tyvars)
             | MonoVal {var, ty, exp} =>
                  (checkType ty
                   ; check (ty, checkPrimExp (exp, ty))
                   ; setVar (var, {tyvars = Vector.new0 (), ty = ty}))
             | PolyVal {tyvars, var, ty, exp} =>
                  (bindTyvars tyvars
                   ; checkType ty
                   ; check (ty, checkExp exp)
                   ; unbindTyvars tyvars
                   ; setVar (var, {tyvars = tyvars, ty = ty}))
         end) arg
      val _ =
         Vector.foreach
         (datatypes, fn {tycon, tyvars, cons} =>
          let
             val _ = bindTyvars tyvars
             val ty = Type.con (tycon, Vector.map (tyvars, Type.var))
             val _ = Vector.foreach (cons, fn c => setCon (c, tyvars, ty))
             val _ = unbindTyvars tyvars
          in
             ()
          end)
      val _ =
         if Type.equals (checkExp body, Type.unit)
            then ()
         else Error.bug "Xml.TypeCheck.typeCheck: program must be of type unit"
      val _ =
         case overflow of
            NONE => true
          | SOME x =>
               let val {tyvars, ty} = getVar x
               in
                  Vector.isEmpty tyvars
                  andalso Type.equals (ty, Type.exn)
               end
      val _ = Program.clear program
   in
      ()
   end

val typeCheck = 
   Trace.trace ("Xml.TypeCheck.typeCheck", Program.layout, Unit.layout) typeCheck

val typeCheck = Control.trace (Control.Pass, "typeCheck") typeCheck

end
Commit	Line	Data
7f918cf1 CE	1	(* Copyright (C) 1999-2007 Henry Cejtin, Matthew Fluet, Suresh
	2	* Jagannathan, and Stephen Weeks.
	3	* Copyright (C) 1997-2000 NEC Research Institute.
	4	*
	5	* MLton is released under a BSD-style license.
	6	* See the file MLton-LICENSE for details.
	7	*)
	8
	9	functor TypeCheck (S: TYPE_CHECK_STRUCTS): TYPE_CHECK =
	10	struct
	11
	12	open S
	13	open Dec PrimExp
	14
	15	fun typeCheck (program as Program.T {datatypes, body, overflow}): unit =
	16	let
	17	(* tyvarInScope is used to ensure that tyvars never shadow themselves. *)
	18	val {get = tyvarInScope: Tyvar.t -> bool ref, ...} =
	19	Property.get (Tyvar.plist,
	20	Property.initFun (fn _ => ref false))
	21	fun bindTyvars (vs: Tyvar.t vector): unit =
	22	Vector.foreach (vs, fn v =>
	23	let
	24	val r = tyvarInScope v
	25	in
	26	if !r
	27	then Type.error ("tyvar already in scope",
	28	Tyvar.layout v)
	29	else r := true
	30	end)
	31	fun unbindTyvars (vs: Tyvar.t vector): unit =
	32	Vector.foreach (vs, fn v => tyvarInScope v := false)
	33	(* checkType makes sure all tyvars are bound. *)
	34	fun checkType (ty: Type.t): unit =
	35	Type.hom {ty = ty,
	36	con = fn _ => (),
	37	var = fn a => if !(tyvarInScope a)
	38	then ()
	39	else Type.error ("tyvar not in scope",
	40	Tyvar.layout a)}
	41	fun checkTypes v = Vector.foreach (v, checkType)
	42	val {get = getCon: Con.t -> {tyvars: Tyvar.t vector, ty: Type.t},
	43	set, ...} =
	44	Property.getSetOnce (Con.plist,
	45	Property.initRaise ("scheme", Con.layout))
	46	fun setCon ({con, arg}, tyvars, result: Type.t): unit =
	47	(checkType result
	48	; set (con, {tyvars = tyvars,
	49	ty = (case arg of
	50	NONE => result
	51	\| SOME ty => (checkType ty
	52	; Type.arrow (ty, result)))}))
	53	fun checkConExp (c: Con.t, ts: Type.t vector): Type.t =
	54	let
	55	val _ = checkTypes ts
	56	val {tyvars, ty} = getCon c
	57	in
	58	Type.substitute (ty, Vector.zip (tyvars, ts))
	59	end
	60	val {get = getVar: Var.t -> {tyvars: Tyvar.t vector, ty: Type.t},
	61	set = setVar, ...} =
	62	Property.getSet (Var.plist,
	63	Property.initRaise ("var scheme", Var.layout))
	64	val getVar =
65	Trace.trace
66	("Xml.TypeCheck.getVar", Var.layout, fn {tyvars, ty} =>
67	Layout.record [("tyvars", Vector.layout Tyvar.layout tyvars),
68	("ty", Type.layout ty)])
69	getVar
70	val setVar =
71	Trace.trace2
72	("Xml.TypeCheck.setVar", Var.layout, fn {tyvars, ty} =>
73	Layout.record [("tyvars", Vector.layout Tyvar.layout tyvars),
74	("ty", Type.layout ty)],
75	Layout.ignore)
76	setVar
77	fun checkVarExp (VarExp.T {var, targs}): Type.t =
78	let
79	val _ = checkTypes targs
80	val {tyvars, ty} = getVar var
81	in if Vector.length targs = Vector.length tyvars
82	then Type.substitute (ty, Vector.zip (tyvars, targs))
83	else
84	Type.error ("variable applied to wrong number of type args",
85	let open Layout
86	in align [Var.layout var,
87	seq [str "tyvars: ",
88	Vector.layout Tyvar.layout tyvars],
89	seq [str "targs: ",
90	Vector.layout Type.layout targs]]
91	end)
92	end
93	fun checkVarExps xs = Vector.map (xs, checkVarExp)
94	fun checkPat (p as Pat.T {con, targs, arg}): Type.t =
95	let
96	val t = checkConExp (con, targs)
97	in
98	case (arg, Type.deArrowOpt t) of
99	(NONE, NONE) => t
100	\| (SOME (x, ty), SOME (t1, t2)) =>
101	(checkType ty
102	; if Type.equals (t1, ty)
103	then (setVar (x, {tyvars = Vector.new0 (),
104	ty = t1}) ; t2)
105	else (Type.error
106	("argument constraint of wrong type",
107	let open Layout
108	in align [seq [str "constructor expects : ", Type.layout t1],
109	seq [str "but got: ", Type.layout ty],
110	seq [str "p: ", Pat.layout p]]
111	end)))
112	\| _ => Type.error ("constructor pattern mismatch", Pat.layout p)
113	end
114	val traceCheckExp =
115	Trace.trace
116	("Xml.TypeCheck.checkExp", Exp.layout, Type.layout)
117	val traceCheckPrimExp =
118	Trace.trace2
119	("Xml.TypeCheck.checkPrimExp", PrimExp.layout, Type.layout, Type.layout)
120	val traceCheckLambda =
121	Trace.trace
122	("Xml.TypeCheck.checkLambda", Lambda.layout, Type.layout)
123	val traceCheckDec =
124	Trace.trace
125	("Xml.TypeCheck.checkDec", Dec.layout, Unit.layout)
126	local
127	val exnType = ref NONE
128	in
129	fun isExnType t =
130	case !exnType of
131	NONE => (exnType := SOME t; true)
132	\| SOME t' => Type.equals (t, t')
133	end
134	fun check (t: Type.t, t': Type.t, layout: unit -> Layout.t): unit =
135	if Type.equals (t, t')
136	then ()
137	else Type.error ("type mismatch",
138	Layout.align [Type.layout t,
139	Type.layout t',
140	layout ()])
141	fun checkExp arg: Type.t =
142	traceCheckExp
143	(fn (exp: Exp.t) =>
144	let val {decs, result} = Exp.dest exp
145	in List.foreach (decs, checkDec)
146	; checkVarExp result
147	end) arg
148	and checkPrimExp arg: Type.t =
149	traceCheckPrimExp
150	(fn (e: PrimExp.t, ty: Type.t) =>
151	let
152	fun error msg =
153	Type.error (msg, let open Layout
154	in seq [str "exp: ", PrimExp.layout e]
155	end)
156	fun checkApp (t1, x) =
157	let
158	val t2 = checkVarExp x
159	in
160	case Type.deArrowOpt t1 of
161	NONE => error "function not of arrow type"
162	\| SOME (t2', t3) =>
163	if Type.equals (t2, t2') then t3
164	else
165	Type.error
166	("actual and formal not of same type",
167	let open Layout
168	in align [seq [str "actual: ", Type.layout t2],
169	seq [str "formal: ", Type.layout t2'],
170	seq [str "expression: ",
171	PrimExp.layout e]]
172	end)
173	end
174	in
175	case e of
176	App {arg, func} => checkApp (checkVarExp func, arg)
177	\| Case {cases, default, test} =>
178	let
179	val default = Option.map (default, checkExp o #1)
180	fun equalss v =
181	if Vector.isEmpty v
182	then Error.bug "Xml.TypeCheck.equalss"
183	else
184	let
185	val t = Vector.first v
186	in
187	if Vector.forall (v, fn t' => Type.equals (t, t'))
188	then SOME t
189	else NONE
190	end
191	fun finish (ptys: Type.t vector,
192	etys: Type.t vector): Type.t =
193	case (equalss ptys, equalss etys) of
194	(NONE, _) => error "patterns not of same type"
195	\| (_, NONE) => error "branches not of same type"
196	\| (SOME pty, SOME ety) =>
197	if Type.equals (checkVarExp test, pty)
198	then
199	case default of
200	NONE => ety
201	\| SOME t =>
202	if Type.equals (ety, t)
203	then ety
204	else error "default of wrong type"
205	else error "test and patterns of different types"
206	datatype z = datatype Cases.t
207	in
208	case cases of
209	Con cases =>
210	finish (Vector.unzip
211	(Vector.map (cases, fn (p, e) =>
212	(checkPat p, checkExp e))))
213	\| Word (s, cs) =>
214	finish (Vector.new1 (Type.word s),
215	Vector.map (cs, fn (_, e) => checkExp e))
216	end
217	\| ConApp {con, targs, arg} =>
218	let
219	val t = checkConExp (con, targs)
220	in
221	case arg of
222	NONE => t
223	\| SOME e => checkApp (t, e)
224	end
225	\| Const c => Type.ofConst c
226	\| Handle {try, catch = (catch, catchType), handler, ...} =>
227	let
228	val _ = if isExnType catchType
229	then ()
230	else error "handle with non-exn type for catch"
231	val ty = checkExp try
232	val _ = setVar (catch, {tyvars = Vector.new0 (),
233	ty = catchType})
234	val ty' = checkExp handler
235	in
236	if Type.equals (ty, ty')
237	then ty
238	else error "bad handle"
239	end
240	\| Lambda l => checkLambda l
241	\| PrimApp {args, prim, targs} =>
242	let
243	val _ = checkTypes targs
244	val () =
245	if Type.checkPrimApp {args = checkVarExps args,
246	prim = prim,
247	result = ty,
248	targs = targs}
249	then ()
250	else error "bad primapp"
251	in
252	ty
253	end
254	\| Profile _ => Type.unit
255	\| Raise {exn, ...} =>
256	if isExnType (checkVarExp exn)
257	then ty
258	else error "bad raise"
259	\| Select {tuple, offset} =>
260	(case Type.deTupleOpt (checkVarExp tuple) of
261	NONE => error "selection from nontuple"
262	\| SOME ts => Vector.sub (ts, offset))
263	\| Tuple xs =>
264	if 1 = Vector.length xs
265	then error "unary tuple"
266	else Type.tuple (checkVarExps xs)
267	\| Var x => checkVarExp x
268	end) arg
269	and checkLambda arg: Type.t =
270	traceCheckLambda
271	(fn (l: Lambda.t) =>
272	let
273	val {arg, argType, body, ...} = Lambda.dest l
274	val _ = checkType argType
275	val _ = setVar (arg, {tyvars = Vector.new0 (), ty = argType})
276	in
277	Type.arrow (argType, checkExp body)
278	end) arg
279	and checkDec arg: unit =
280	traceCheckDec
281	(fn (d: Dec.t) =>
282	let
283	val check = fn (t, t') => check (t, t', fn () => Dec.layout d)
284	in
285	case d of
286	Exception c => setCon (c, Vector.new0 (), Type.exn)
287	\| Fun {tyvars, decs} =>
288	(bindTyvars tyvars
289	; (Vector.foreach
290	(decs, fn {ty, var, ...} =>
291	(checkType ty
292	; setVar (var, {tyvars = tyvars, ty = ty}))))
293	; Vector.foreach (decs, fn {ty, lambda, ...} =>
294	check (ty, checkLambda lambda))
295	; unbindTyvars tyvars)
296	\| MonoVal {var, ty, exp} =>
297	(checkType ty
298	; check (ty, checkPrimExp (exp, ty))
299	; setVar (var, {tyvars = Vector.new0 (), ty = ty}))
300	\| PolyVal {tyvars, var, ty, exp} =>
301	(bindTyvars tyvars
302	; checkType ty
303	; check (ty, checkExp exp)
304	; unbindTyvars tyvars
305	; setVar (var, {tyvars = tyvars, ty = ty}))
306	end) arg
307	val _ =
308	Vector.foreach
309	(datatypes, fn {tycon, tyvars, cons} =>
310	let
311	val _ = bindTyvars tyvars
312	val ty = Type.con (tycon, Vector.map (tyvars, Type.var))
313	val _ = Vector.foreach (cons, fn c => setCon (c, tyvars, ty))
314	val _ = unbindTyvars tyvars
315	in
316	()
317	end)
318	val _ =
319	if Type.equals (checkExp body, Type.unit)
320	then ()
321	else Error.bug "Xml.TypeCheck.typeCheck: program must be of type unit"
322	val _ =
323	case overflow of
324	NONE => true
325	\| SOME x =>
326	let val {tyvars, ty} = getVar x
327	in
328	Vector.isEmpty tyvars
329	andalso Type.equals (ty, Type.exn)
330	end
331	val _ = Program.clear program
332	in
333	()
334	end
335
336	val typeCheck =
337	Trace.trace ("Xml.TypeCheck.typeCheck", Program.layout, Unit.layout) typeCheck
338
339	val typeCheck = Control.trace (Control.Pass, "typeCheck") typeCheck
340
341	end