6d58e435db6062956e5a7e9713932209fac7ea62
[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 Env
24
25 structure SM = StringMap
26
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
90 | (TNested (p1, q1), TNested (p2, q2)) =>
91 eqPred (p1, p2) andalso eqTy (q1, q2)
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 | WrongPred of string * pred * pred
114
115 fun describe_unification_error t ue =
116 case ue of
117 UnifyPred (p1, p2) =>
118 (print "Reason: Incompatible contexts.\n";
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")
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))
156
157 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
158 case (p1, p2) of
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
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)
170 | (_, CPrefix p2) => predImplies (p1All, p2)
171
172 | (CNot p1, CNot p2) => predImplies (p2, p1)
173
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'
191 else if predImplies (p1', p2') then
192 p1'
193 else
194 (CAnd (p1', p2'), loc)
195 end
196
197 fun subPred (p1, p2) =
198 if predImplies (p1, p2) then
199 ()
200 else
201 raise (Unify (UnifyPred (p1, p2)))
202
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
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)
217 | TNested (_, t) => occurs u t
218 | TError => false
219 | TUnif (_, ref (SOME t)) => occurs u t
220 | TUnif (_, u') => u = u'
221
222 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
223 case (t1, t2) of
224 (TBase s1, TBase s2) =>
225 if s1 = s2 then
226 ()
227 else
228 raise Unify (UnifyTyp (t1All, t2All))
229 | (TList t1, TList t2) => subTyp (t1, t2)
230 | (TArrow (d1, r1), TArrow (d2, r2)) =>
231 (subTyp (d2, d1);
232 subTyp (r1, r2))
233
234 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
235 ((subPred (p2, p1);
236 subRecord subTyp (d2, d1);
237 subRecord subTyp (r1, r2);
238 subRecord subTyp (r2, r1))
239 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
240
241 | (TNested (d1, r1), TNested (d2, r2)) =>
242 (subPred (d2, d1);
243 subTyp (r1, r2))
244
245 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
246 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
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
276 fun whnorm (tAll as (t, loc)) =
277 case t of
278 TUnif (_, ref (SOME tAll)) => whnorm tAll
279 | _ => tAll
280
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
291 fun hasTyp (e, t1, t2) =
292 if (case baseCondition t2 of
293 NONE => false
294 | SOME rule => rule e) then
295 ()
296 else
297 subTyp (t1, t2)
298
299 fun checkPred G (p, loc) =
300 let
301 val err = ErrorMsg.error (SOME loc)
302 in
303 case p of
304 CRoot => ()
305 | CConst s =>
306 if lookupContext G s then
307 ()
308 else
309 err ("Unbound context " ^ s)
310 | CPrefix p => checkPred G p
311 | CNot p => checkPred G p
312 | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
313 end
314
315 fun checkTyp G (tAll as (t, loc)) =
316 let
317 val err = ErrorMsg.error (SOME loc)
318 in
319 case t of
320 TBase name =>
321 if lookupType G name then
322 tAll
323 else
324 (err ("Unbound type name " ^ name);
325 (TError, loc))
326 | TList t => (TList (checkTyp G t), loc)
327 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
328 | TAction (p, d, r) => (checkPred G p;
329 (TAction (p, SM.map (checkTyp G) d,
330 SM.map (checkTyp G) r), loc))
331 | TNested (p, t) => (checkPred G p;
332 (TNested (p, checkTyp G t), loc))
333 | TError => raise Fail "TError in parser-generated type"
334 | TUnif _ => raise Fail "TUnif in parser-generated type"
335 end
336
337 fun envVarSetFrom v (e, _) =
338 case e of
339 ESet (v', e) =>
340 if v = v' then
341 SOME e
342 else
343 NONE
344 | EGet (_, _, e) => envVarSetFrom v e
345 | ESeq es => foldr (fn (e, found) =>
346 case found of
347 SOME _ => found
348 | NONE => envVarSetFrom v e)
349 NONE es
350 | ELocal (_, e) => envVarSetFrom v e
351
352 | _ => NONE
353
354 fun checkExp G (eAll as (e, loc)) =
355 let
356 val dte = describe_type_error loc
357 in
358 case e of
359 EInt _ => (TBase "int", loc)
360 | EString _ => (TBase "string", loc)
361 | EList es =>
362 let
363 val t = (newUnif (), loc)
364 in
365 foldl (fn (e', ret) =>
366 let
367 val t' = checkExp G e'
368 in
369 (hasTyp (eAll, t', t);
370 if isError t' then
371 (TList (TError, loc), loc)
372 else
373 ret)
374 handle Unify ue =>
375 (dte (WrongType ("List element",
376 e',
377 t',
378 t,
379 SOME ue));
380 (TError, loc))
381 end) (TList t, loc) es
382 end
383
384 | ELam (x, to, e) =>
385 let
386 val t =
387 case to of
388 NONE => (newUnif (), loc)
389 | SOME t => checkTyp G t
390
391 val G' = bindVal G (x, t, NONE)
392 val t' = checkExp G' e
393 in
394 (TArrow (t, t'), loc)
395 end
396 | EVar x =>
397 (case lookupVal G x of
398 NONE => (dte (UnboundVariable x);
399 (TError, loc))
400 | SOME t => t)
401 | EApp (func, arg) =>
402 let
403 val dom = (newUnif (), loc)
404 val ran = (newUnif (), loc)
405
406 val tf = checkExp G func
407 val ta = checkExp G arg
408 in
409 (hasTyp (func, tf, (TArrow (dom, ran), loc));
410 hasTyp (arg, ta, dom)
411 handle Unify ue =>
412 dte (WrongType ("Function argument",
413 arg,
414 ta,
415 dom,
416 SOME ue));
417 ran)
418 handle Unify ue =>
419 (dte (WrongForm ("Function to be applied",
420 "function",
421 func,
422 tf,
423 SOME ue));
424 (TError, loc))
425 end
426
427 | ESet (evar, e) =>
428 let
429 val t = checkExp G e
430 in
431 (TAction ((CPrefix (CRoot, loc), loc),
432 SM.empty,
433 SM.insert (SM.empty, evar, t)),
434 loc)
435 end
436 | EGet (x, evar, rest) =>
437 let
438 val xt = (newUnif (), loc)
439 val G' = bindVal G (x, xt, NONE)
440
441 val rt = whnorm (checkExp G' rest)
442 in
443 case rt of
444 (TAction (p, d, r), _) =>
445 (case SM.find (d, evar) of
446 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
447 | SOME xt' =>
448 (subTyp (xt', xt)
449 handle Unify ue =>
450 dte (WrongType ("Retrieved environment variable",
451 (EVar x, loc),
452 xt',
453 xt,
454 SOME ue));
455 rt))
456 | (TError, _) => rt
457 | _ => (dte (WrongForm ("Body of environment variable read",
458 "action",
459 rest,
460 rt,
461 NONE));
462 (TError, loc))
463 end
464
465 | ESeq [] => raise Fail "Empty ESeq"
466 | ESeq [e1] => checkExp G e1
467 | ESeq (e1 :: rest) =>
468 let
469 val e2 = (ESeq rest, loc)
470
471 val t1 = whnorm (checkExp G e1)
472 val t2 = whnorm (checkExp G e2)
473 in
474 case t1 of
475 (TAction (p1, d1, r1), _) =>
476 (case t2 of
477 (TAction (p2, d2, r2), _) =>
478 let
479 val p' = predSimpl (CAnd (p1, p2), loc)
480
481 val d' = SM.foldli (fn (name, t, d') =>
482 case SM.find (r1, name) of
483 NONE =>
484 (case SM.find (d', name) of
485 NONE => SM.insert (d', name, t)
486 | SOME t' =>
487 ((case envVarSetFrom name e1 of
488 NONE => subTyp (t, t')
489 | SOME e => hasTyp (e, t, t'))
490 handle Unify ue =>
491 dte (WrongType ("Shared environment variable",
492 (EVar name, loc),
493 t',
494 t,
495 SOME ue));
496 d'))
497 | SOME t' =>
498 ((case envVarSetFrom name e1 of
499 NONE => subTyp (t, t')
500 | SOME e => hasTyp (e, t, t'))
501 handle Unify ue =>
502 dte (WrongType ("Shared environment variable",
503 (EVar name, loc),
504 t',
505 t,
506 SOME ue));
507 d'))
508 d1 d2
509
510 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
511 r1 r2
512 in
513 (TAction (p', d', r'), loc)
514 end
515 | (TError, _) => t2
516 | _ => (dte (WrongForm ("Action to be sequenced",
517 "action",
518 e2,
519 t2,
520 NONE));
521 (TError, loc)))
522 | (TError, _) => t1
523 | _ => (dte (WrongForm ("Action to be sequenced",
524 "action",
525 e1,
526 t1,
527 NONE));
528 (TError, loc))
529 end
530
531 | ELocal (e1, e2) =>
532 let
533 val t1 = whnorm (checkExp G e1)
534 val t2 = whnorm (checkExp G e2)
535 in
536 case t1 of
537 (TAction (p1, d1, r1), _) =>
538 (case t2 of
539 (TAction (p2, d2, r2), _) =>
540 let
541 val p' = predSimpl (CAnd (p1, p2), loc)
542
543 val d' = SM.foldli (fn (name, t, d') =>
544 case SM.find (r1, name) of
545 NONE =>
546 (case SM.find (d', name) of
547 NONE => SM.insert (d', name, t)
548 | SOME t' =>
549 ((case envVarSetFrom name e1 of
550 NONE => subTyp (t', t)
551 | SOME e => hasTyp (e, t', t))
552 handle Unify ue =>
553 dte (WrongType ("Shared environment variable",
554 (EVar name, loc),
555 t',
556 t,
557 SOME ue));
558 d'))
559 | SOME t' =>
560 ((case envVarSetFrom name e1 of
561 NONE => subTyp (t', t)
562 | SOME e => hasTyp (e, t', t))
563 handle Unify ue =>
564 dte (WrongType ("Shared environment variable",
565 (EVar name, loc),
566 t',
567 t,
568 SOME ue));
569 d'))
570 d1 d2
571 in
572 (TAction (p', d', r2), loc)
573 end
574 | (TError, _) => t2
575 | _ => (dte (WrongForm ("Action to be sequenced",
576 "action",
577 e2,
578 t2,
579 NONE));
580 (TError, loc)))
581 | (TError, _) => t1
582 | _ => (dte (WrongForm ("Action to be sequenced",
583 "action",
584 e1,
585 t1,
586 NONE));
587 (TError, loc))
588 end
589
590
591 | EWith (e1, e2) =>
592 let
593 val t1 = whnorm (checkExp G e1)
594 val t2 = whnorm (checkExp G e2)
595 in
596 case t1 of
597 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
598 (case t2 of
599 (TAction (p, d, r), _) =>
600 if predImplies (pd, p) then
601 let
602 val combineRecs =
603 SM.unionWithi (fn (name, t1, t2) =>
604 (subTyp (t1, t2)
605 handle Unify ue =>
606 dte (WrongType ("Environment variable",
607 (EVar name, loc),
608 t1,
609 t2,
610 SOME ue));
611 t2))
612 in
613 (TAction (pr, combineRecs (d, d1),
614 combineRecs (r, r1)), loc)
615 end
616 else
617 (dte (WrongPred ("nested action",
618 pd,
619 p));
620 (TError, loc))
621 | (TError, _) => t2
622 | _ =>
623 (dte (WrongForm ("Body of nested action",
624 "action",
625 e2,
626 t2,
627 NONE));
628 (TError, loc)))
629 | (TError, _) => t1
630 | _ =>
631 (dte (WrongForm ("Container of nested action",
632 "action",
633 e1,
634 t1,
635 NONE));
636 (TError, loc))
637 end
638
639 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
640 SM.empty, SM.empty), loc)
641 end
642
643 exception Ununif
644
645 fun ununif (tAll as (t, loc)) =
646 case t of
647 TBase _ => tAll
648 | TList t => (TList (ununif t), loc)
649 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
650 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
651 | TUnif (_, ref (SOME t)) => ununif t
652 | TNested _ => tAll
653 | TError => tAll
654
655 | TUnif (_, ref NONE) => raise Ununif
656
657 fun hasError (t, _) =
658 case t of
659 TBase _ => false
660 | TList t => hasError t
661 | TArrow (d, r) => hasError d orelse hasError r
662 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
663 orelse List.exists hasError (SM.listItems r)
664 | TNested _ => false
665 | TError => false
666 | TUnif (_, ref (SOME t)) => hasError t
667 | TUnif (_, ref NONE) => false
668
669
670 fun checkUnit G (eAll as (_, loc)) =
671 let
672 val _ = resetUnif ()
673 val t = checkExp G eAll
674 in
675 if hasError t then
676 t
677 else
678 ununif t
679 handle Ununif =>
680 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
681 printd (p_typ t);
682 t)
683 end
684
685 fun checkDecl G (d, _, loc) =
686 case d of
687 DExternType name => bindType G name
688 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
689 | DVal (name, to, e) =>
690 let
691 val to =
692 case to of
693 NONE => (newUnif (), loc)
694 | SOME to => checkTyp G to
695
696 val t = checkExp G e
697 in
698 hasTyp (e, t, to)
699 handle Unify ue =>
700 describe_type_error loc
701 (WrongType ("Bound value",
702 e,
703 t,
704 to,
705 SOME ue));
706 bindVal G (name, to, SOME e)
707 end
708 | DContext name => bindContext G name
709
710 fun checkFile G tInit (_, ds, eo) =
711 let
712 val G' = foldl (fn (d, G) => checkDecl G d) G ds
713 in
714 case eo of
715 NONE => ()
716 | SOME (e as (_, loc)) =>
717 let
718 val t = checkExp G' e
719 in
720 hasTyp (e, t, tInit)
721 handle Unify ue =>
722 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
723 preface ("Actual:", p_typ t);
724 preface ("Needed:", p_typ tInit))
725 end;
726 G'
727 end
728
729 end