HCoop / hcoop / domtool2.git / blob
? search:


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