Custom base types
[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 preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
116 [PD.string s, PD.space 1, d]))
117
118 fun describe_unification_error t ue =
119 case ue of
120 UnifyPred (p1, p2) =>
121 (print "Reason: Incompatible contexts.\n";
122 preface ("Have:", p_pred p1);
123 preface ("Need:", p_pred p2))
124 | UnifyTyp (t1, t2) =>
125 if eqTy (t, t1) then
126 ()
127 else
128 (print "Reason: Incompatible types.\n";
129 preface ("Have:", p_typ t1);
130 preface ("Need:", p_typ t2))
131 | UnifyOccurs (name, t') =>
132 if eqTy (t, t') then
133 ()
134 else
135 (print "Reason: Occurs check failed for ";
136 print name;
137 print " in:\n";
138 printd (p_typ t))
139
140 fun describe_type_error loc te =
141 case te of
142 WrongType (place, e, t1, t2, ueo) =>
143 (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
144 preface (" Expression:", p_exp e);
145 preface ("Actual type:", p_typ t1);
146 preface ("Needed type:", p_typ t2);
147 Option.app (describe_unification_error t1) ueo)
148 | WrongForm (place, form, e, t, ueo) =>
149 (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
150 preface ("Expression:", p_exp e);
151 preface (" Type:", p_typ t);
152 Option.app (describe_unification_error t) ueo)
153 | UnboundVariable name =>
154 ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
155 | WrongPred (place, p1, p2) =>
156 (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
157 preface ("Have:", p_pred p1);
158 preface ("Need:", p_pred p2))
159
160 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
161 case (p1, p2) of
162 (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
163 | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
164
165 | (_, CPrefix (CRoot, _)) => true
166 | (CNot (CPrefix (CRoot, _), _), _) => true
167
168 | (CRoot, CRoot) => true
169
170 | (CConst s1, CConst s2) => s1 = s2
171
172 | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
173 | (_, CPrefix p2) => predImplies (p1All, p2)
174
175 | (CNot p1, CNot p2) => predImplies (p2, p1)
176
177 | _ => false
178
179 fun predSimpl (pAll as (p, loc)) =
180 case p of
181 CRoot => pAll
182 | CConst _ => pAll
183 | CPrefix p => (CPrefix (predSimpl p), loc)
184 | CNot p => (CNot (predSimpl p), loc)
185 | CAnd (p1, p2) =>
186 let
187 val p1' = predSimpl p1
188 val p2' = predSimpl p2
189 in
190 case p1' of
191 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
192 | _ => if predImplies (p2', p1') then
193 p2'
194 else if predImplies (p1', p2') then
195 p1'
196 else
197 (CAnd (p1', p2'), loc)
198 end
199
200 fun subPred (p1, p2) =
201 if predImplies (p1, p2) then
202 ()
203 else
204 raise (Unify (UnifyPred (p1, p2)))
205
206 fun subRecord f (r1, r2) =
207 SM.appi (fn (k, v2) =>
208 case SM.find (r1, k) of
209 NONE => raise UnequalDomains
210 | SOME v1 => f (v1, v2)) r2
211
212 fun occurs u (t, _) =
213 case t of
214 TBase _ => false
215 | TList t => occurs u t
216 | TArrow (d, r) => occurs u d orelse occurs u r
217 | TAction (_, d, r) =>
218 List.exists (occurs u) (SM.listItems d)
219 orelse List.exists (occurs u) (SM.listItems r)
220 | TNested (_, t) => occurs u t
221 | TError => false
222 | TUnif (_, ref (SOME t)) => occurs u t
223 | TUnif (_, u') => u = u'
224
225 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
226 case (t1, t2) of
227 (TBase s1, TBase s2) =>
228 if s1 = s2 then
229 ()
230 else
231 raise Unify (UnifyTyp (t1All, t2All))
232 | (TList t1, TList t2) => subTyp (t1, t2)
233 | (TArrow (d1, r1), TArrow (d2, r2)) =>
234 (subTyp (d2, d1);
235 subTyp (r1, r2))
236
237 | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
238 ((subPred (p2, p1);
239 subRecord subTyp (d2, d1);
240 subRecord subTyp (r1, r2);
241 subRecord subTyp (r2, r1))
242 handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
243
244 | (TNested (d1, r1), TNested (d2, r2)) =>
245 (subPred (d2, d1);
246 subTyp (r1, r2))
247
248 | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
249 | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
250
251 | (TUnif (_, r1), TUnif (_, r2)) =>
252 if r1 = r2 then
253 ()
254 else
255 r1 := SOME t2All
256
257 | (TUnif (name, r), _) =>
258 if occurs r t2All then
259 raise (Unify (UnifyOccurs (name, t2All)))
260 else
261 r := SOME t2All
262
263 | (_, TUnif (name, r)) =>
264 if occurs r t1All then
265 raise (Unify (UnifyOccurs (name, t1All)))
266 else
267 r := SOME t1All
268
269 | (TError, _) => ()
270 | (_, TError) => ()
271
272 | _ => raise Unify (UnifyTyp (t1All, t2All))
273
274 fun isError t =
275 case t of
276 (TError, _) => true
277 | _ => false
278
279 fun whnorm (tAll as (t, loc)) =
280 case t of
281 TUnif (_, ref (SOME tAll)) => whnorm tAll
282 | _ => tAll
283
284 fun hasTyp (e, t1, t2) =
285 case whnorm t2 of
286 (TBase name, _) =>
287 (case typeRule name of
288 NONE => subTyp (t1, t2)
289 | SOME rule =>
290 if rule e then
291 ()
292 else
293 subTyp (t1, t2))
294 | _ => subTyp (t1, t2)
295
296 fun checkTyp G (tAll as (t, loc)) =
297 let
298 val err = ErrorMsg.error (SOME loc)
299 in
300 case t of
301 TBase name =>
302 if lookupType G name then
303 tAll
304 else
305 (err ("Unbound type name " ^ name);
306 (TError, loc))
307 | TList t => (TList (checkTyp G t), loc)
308 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
309 | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
310 SM.map (checkTyp G) r), loc)
311 | TNested (p, t) => (TNested (p, checkTyp G t), loc)
312 | TError => raise Fail "TError in parser-generated type"
313 | TUnif _ => raise Fail "TUnif in parser-generated type"
314 end
315
316 fun checkExp G (eAll as (e, loc)) =
317 let
318 val dte = describe_type_error loc
319 in
320 case e of
321 EInt _ => (TBase "int", loc)
322 | EString _ => (TBase "string", loc)
323 | EList es =>
324 let
325 val t = (newUnif (), loc)
326 in
327 foldl (fn (e', ret) =>
328 let
329 val t' = checkExp G e'
330 in
331 (hasTyp (eAll, t', t);
332 if isError t' then
333 (TList (TError, loc), loc)
334 else
335 ret)
336 handle Unify ue =>
337 (dte (WrongType ("List element",
338 e',
339 t',
340 t,
341 SOME ue));
342 (TError, loc))
343 end) (TList t, loc) es
344 end
345
346 | ELam (x, to, e) =>
347 let
348 val t =
349 case to of
350 NONE => (newUnif (), loc)
351 | SOME t => checkTyp G t
352
353 val G' = bindVal G (x, t, NONE)
354 val t' = checkExp G' e
355 in
356 (TArrow (t, t'), loc)
357 end
358 | EVar x =>
359 (case lookupVal G x of
360 NONE => (dte (UnboundVariable x);
361 (TError, loc))
362 | SOME t => t)
363 | EApp (func, arg) =>
364 let
365 val dom = (newUnif (), loc)
366 val ran = (newUnif (), loc)
367
368 val tf = checkExp G func
369 val ta = checkExp G arg
370 in
371 (hasTyp (func, tf, (TArrow (dom, ran), loc));
372 hasTyp (arg, ta, dom)
373 handle Unify ue =>
374 dte (WrongType ("Function argument",
375 arg,
376 ta,
377 dom,
378 SOME ue));
379 ran)
380 handle Unify ue =>
381 (dte (WrongForm ("Function to be applied",
382 "function",
383 func,
384 tf,
385 SOME ue));
386 (TError, loc))
387 end
388
389 | ESet (evar, e) =>
390 let
391 val t = checkExp G e
392 in
393 (TAction ((CPrefix (CRoot, loc), loc),
394 SM.empty,
395 SM.insert (SM.empty, evar, t)),
396 loc)
397 end
398 | EGet (x, evar, rest) =>
399 let
400 val xt = (newUnif (), loc)
401 val G' = bindVal G (x, xt, NONE)
402
403 val rt = whnorm (checkExp G' rest)
404 in
405 case rt of
406 (TAction (p, d, r), _) =>
407 (case SM.find (d, evar) of
408 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
409 | SOME xt' =>
410 (subTyp (xt', xt)
411 handle Unify ue =>
412 dte (WrongType ("Retrieved environment variable",
413 (EVar x, loc),
414 xt',
415 xt,
416 SOME ue));
417 rt))
418 | (TError, _) => rt
419 | _ => (dte (WrongForm ("Body of environment variable read",
420 "action",
421 rest,
422 rt,
423 NONE));
424 (TError, loc))
425 end
426
427 | ESeq [] => raise Fail "Empty ESeq"
428 | ESeq [e1] => checkExp G e1
429 | ESeq (e1 :: rest) =>
430 let
431 val e2 = (ESeq rest, loc)
432
433 val t1 = whnorm (checkExp G e1)
434 val t2 = whnorm (checkExp G e2)
435 in
436 case t1 of
437 (TAction (p1, d1, r1), _) =>
438 (case t2 of
439 (TAction (p2, d2, r2), _) =>
440 let
441 val p' = predSimpl (CAnd (p1, p2), loc)
442
443 val d' = SM.foldli (fn (name, t, d') =>
444 case SM.find (r1, name) of
445 NONE =>
446 (case SM.find (d', name) of
447 NONE => SM.insert (d', name, t)
448 | SOME t' =>
449 (subTyp (t, t')
450 handle Unify ue =>
451 dte (WrongType ("Shared environment variable",
452 (EVar name, loc),
453 t,
454 t',
455 SOME ue));
456 d'))
457 | SOME t' =>
458 (subTyp (t, t')
459 handle Unify ue =>
460 dte (WrongType ("Shared environment variable",
461 (EVar name, loc),
462 t,
463 t',
464 SOME ue));
465 d'))
466 d1 d2
467
468 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
469 r1 r2
470 in
471 (TAction (p', d', r'), loc)
472 end
473 | (TError, _) => t2
474 | _ => (dte (WrongForm ("Action to be sequenced",
475 "action",
476 e2,
477 t2,
478 NONE));
479 (TError, loc)))
480 | (TError, _) => t1
481 | _ => (dte (WrongForm ("Action to be sequenced",
482 "action",
483 e1,
484 t1,
485 NONE));
486 (TError, loc))
487 end
488
489 | ELocal (e1, e2) =>
490 let
491 val t1 = whnorm (checkExp G e1)
492 val t2 = whnorm (checkExp G e2)
493 in
494 case t1 of
495 (TAction (p1, d1, r1), _) =>
496 (case t2 of
497 (TAction (p2, d2, r2), _) =>
498 let
499 val p' = predSimpl (CAnd (p1, p2), loc)
500
501 val d' = SM.foldli (fn (name, t, d') =>
502 case SM.find (r1, name) of
503 NONE =>
504 (case SM.find (d', name) of
505 NONE => SM.insert (d', name, t)
506 | SOME t' =>
507 (subTyp (t, t')
508 handle Unify ue =>
509 dte (WrongType ("Shared environment variable",
510 (EVar name, loc),
511 t,
512 t',
513 SOME ue));
514 d'))
515 | SOME t' =>
516 (subTyp (t, t')
517 handle Unify ue =>
518 dte (WrongType ("Shared environment variable",
519 (EVar name, loc),
520 t,
521 t',
522 SOME ue));
523 d'))
524 d1 d2
525 in
526 (TAction (p', d', r2), loc)
527 end
528 | (TError, _) => t2
529 | _ => (dte (WrongForm ("Action to be sequenced",
530 "action",
531 e2,
532 t2,
533 NONE));
534 (TError, loc)))
535 | (TError, _) => t1
536 | _ => (dte (WrongForm ("Action to be sequenced",
537 "action",
538 e1,
539 t1,
540 NONE));
541 (TError, loc))
542 end
543
544
545 | EWith (e1, e2) =>
546 let
547 val t1 = whnorm (checkExp G e1)
548 val t2 = whnorm (checkExp G e2)
549 in
550 case t1 of
551 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
552 (case t2 of
553 (TAction (p, d, r), _) =>
554 if predImplies (pd, p) then
555 let
556 val combineRecs =
557 SM.unionWithi (fn (name, t1, t2) =>
558 (subTyp (t1, t2)
559 handle Unify ue =>
560 dte (WrongType ("Environment variable",
561 (EVar name, loc),
562 t1,
563 t2,
564 SOME ue));
565 t2))
566 in
567 (TAction (pr, combineRecs (d, d1),
568 combineRecs (r, r1)), loc)
569 end
570 else
571 (dte (WrongPred ("nested action",
572 pd,
573 p));
574 (TError, loc))
575 | (TError, _) => t2
576 | _ =>
577 (dte (WrongForm ("Body of nested action",
578 "action",
579 e2,
580 t2,
581 NONE));
582 (TError, loc)))
583 | (TError, _) => t1
584 | _ =>
585 (dte (WrongForm ("Container of nested action",
586 "action",
587 e1,
588 t1,
589 NONE));
590 (TError, loc))
591 end
592
593 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
594 SM.empty, SM.empty), loc)
595 end
596
597 exception Ununif
598
599 fun ununif (tAll as (t, loc)) =
600 case t of
601 TBase _ => tAll
602 | TList t => (TList (ununif t), loc)
603 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
604 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
605 | TUnif (_, ref (SOME t)) => ununif t
606 | TNested _ => tAll
607 | TError => tAll
608
609 | TUnif (_, ref NONE) => raise Ununif
610
611 fun hasError (t, _) =
612 case t of
613 TBase _ => false
614 | TList t => hasError t
615 | TArrow (d, r) => hasError d orelse hasError r
616 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
617 orelse List.exists hasError (SM.listItems r)
618 | TNested _ => false
619 | TError => false
620 | TUnif (_, ref (SOME t)) => hasError t
621 | TUnif (_, ref NONE) => false
622
623
624 fun checkUnit G (eAll as (_, loc)) =
625 let
626 val _ = resetUnif ()
627 val t = checkExp G eAll
628 in
629 if hasError t then
630 t
631 else
632 ununif t
633 handle Ununif =>
634 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
635 printd (p_typ t);
636 t)
637 end
638
639 fun checkDecl G (d, _, loc) =
640 case d of
641 DExternType name => bindType G name
642 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
643 | DVal (name, to, e) =>
644 let
645 val to =
646 case to of
647 NONE => (newUnif (), loc)
648 | SOME to => checkTyp G to
649
650 val t = checkExp G e
651 in
652 hasTyp (e, t, to)
653 handle Unify ue =>
654 describe_type_error loc
655 (WrongType ("Bound value",
656 e,
657 t,
658 to,
659 SOME ue));
660 bindVal G (name, to, SOME e)
661 end
662
663 fun checkFile G tInit (ds, eo) =
664 let
665 val G' = foldl (fn (d, G) => checkDecl G d) G ds
666 in
667 case eo of
668 NONE => ()
669 | SOME (e as (_, loc)) =>
670 let
671 val t = checkExp G' e
672 in
673 hasTyp (e, t, tInit)
674 handle Unify ue =>
675 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
676 preface ("Actual:", p_typ t);
677 preface ("Needed:", p_typ tInit))
678 end;
679 G'
680 end
681
682 end