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