Basic type-checking
[hcoop/domtool2.git] / src / tycheck.sml
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