HCoop / hcoop / domtool2.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
E-mail aliases
[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
234b917a
AC		 299fun checkTyp G (tAll as (t, loc)) =
300 let
301 val err = ErrorMsg.error (SOME loc)
302 in
303 case t of
304 TBase name =>
305 if lookupType G name then
306 tAll
307 else
308 (err ("Unbound type name " ^ name);
309 (TError, loc))
310 | TList t => (TList (checkTyp G t), loc)
311 | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
312 | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
313 SM.map (checkTyp G) r), loc)
1a4e5a6c 314 | TNested (p, t) => (TNested (p, checkTyp G t), loc)
234b917a
AC		 315 | TError => raise Fail "TError in parser-generated type"
316 | TUnif _ => raise Fail "TUnif in parser-generated type"
317 end
318
27d9de59
AC		 319fun checkExp G (eAll as (e, loc)) =
320 let
321 val dte = describe_type_error loc
322 in
323 case e of
324 EInt _ => (TBase "int", loc)
325 | EString _ => (TBase "string", loc)
326 | EList es =>
327 let
328 val t = (newUnif (), loc)
329 in
330 foldl (fn (e', ret) =>
331 let
332 val t' = checkExp G e'
333 in
6be996d4 334 (hasTyp (eAll, t', t);
27d9de59
AC		 335 if isError t' then
336 (TList (TError, loc), loc)
337 else
338 ret)
339 handle Unify ue =>
340 (dte (WrongType ("List element",
341 e',
342 t',
343 t,
344 SOME ue));
345 (TError, loc))
346 end) (TList t, loc) es
347 end
348
349 | ELam (x, to, e) =>
350 let
351 val t =
352 case to of
353 NONE => (newUnif (), loc)
234b917a 354 | SOME t => checkTyp G t
27d9de59 355
492c1cff 356 val G' = bindVal G (x, t, NONE)
27d9de59
AC		 357 val t' = checkExp G' e
358 in
359 (TArrow (t, t'), loc)
360 end
361 | EVar x =>
234b917a 362 (case lookupVal G x of
27d9de59
AC		 363 NONE => (dte (UnboundVariable x);
364 (TError, loc))
365 | SOME t => t)
366 | EApp (func, arg) =>
367 let
368 val dom = (newUnif (), loc)
369 val ran = (newUnif (), loc)
370
371 val tf = checkExp G func
372 val ta = checkExp G arg
373 in
6be996d4
AC		 374 (hasTyp (func, tf, (TArrow (dom, ran), loc));
375 hasTyp (arg, ta, dom)
27d9de59
AC		 376 handle Unify ue =>
377 dte (WrongType ("Function argument",
378 arg,
379 ta,
380 dom,
381 SOME ue));
382 ran)
383 handle Unify ue =>
384 (dte (WrongForm ("Function to be applied",
385 "function",
386 func,
387 tf,
388 SOME ue));
389 (TError, loc))
390 end
db427c67
AC		 391
392 | ESet (evar, e) =>
393 let
394 val t = checkExp G e
395 in
396 (TAction ((CPrefix (CRoot, loc), loc),
397 SM.empty,
398 SM.insert (SM.empty, evar, t)),
399 loc)
400 end
401 | EGet (x, evar, rest) =>
402 let
403 val xt = (newUnif (), loc)
492c1cff 404 val G' = bindVal G (x, xt, NONE)
db427c67
AC		 405
406 val rt = whnorm (checkExp G' rest)
407 in
408 case rt of
409 (TAction (p, d, r), _) =>
410 (case SM.find (d, evar) of
411 NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
412 | SOME xt' =>
234b917a 413 (subTyp (xt', xt)
db427c67
AC		 414 handle Unify ue =>
415 dte (WrongType ("Retrieved environment variable",
416 (EVar x, loc),
417 xt',
418 xt,
419 SOME ue));
420 rt))
234b917a 421 | (TError, _) => rt
db427c67
AC		 422 | _ => (dte (WrongForm ("Body of environment variable read",
423 "action",
424 rest,
425 rt,
426 NONE));
427 (TError, loc))
428 end
429
430 | ESeq [] => raise Fail "Empty ESeq"
431 | ESeq [e1] => checkExp G e1
432 | ESeq (e1 :: rest) =>
433 let
434 val e2 = (ESeq rest, loc)
435
436 val t1 = whnorm (checkExp G e1)
437 val t2 = whnorm (checkExp G e2)
438 in
439 case t1 of
440 (TAction (p1, d1, r1), _) =>
441 (case t2 of
442 (TAction (p2, d2, r2), _) =>
443 let
444 val p' = predSimpl (CAnd (p1, p2), loc)
445
446 val d' = SM.foldli (fn (name, t, d') =>
447 case SM.find (r1, name) of
448 NONE =>
449 (case SM.find (d', name) of
450 NONE => SM.insert (d', name, t)
451 | SOME t' =>
234b917a 452 (subTyp (t, t')
db427c67
AC		 453 handle Unify ue =>
454 dte (WrongType ("Shared environment variable",
455 (EVar name, loc),
456 t,
457 t',
458 SOME ue));
459 d'))
460 | SOME t' =>
234b917a 461 (subTyp (t, t')
db427c67
AC		 462 handle Unify ue =>
463 dte (WrongType ("Shared environment variable",
464 (EVar name, loc),
465 t,
466 t',
467 SOME ue));
468 d'))
469 d1 d2
470
471 val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
472 r1 r2
473 in
474 (TAction (p', d', r'), loc)
475 end
234b917a 476 | (TError, _) => t2
db427c67
AC		 477 | _ => (dte (WrongForm ("Action to be sequenced",
478 "action",
479 e2,
480 t2,
481 NONE));
482 (TError, loc)))
234b917a 483 | (TError, _) => t1
db427c67
AC		 484 | _ => (dte (WrongForm ("Action to be sequenced",
485 "action",
486 e1,
487 t1,
488 NONE));
489 (TError, loc))
490 end
491
1a4e5a6c 492 | ELocal (e1, e2) =>
db427c67 493 let
1a4e5a6c
AC		 494 val t1 = whnorm (checkExp G e1)
495 val t2 = whnorm (checkExp G e2)
db427c67 496 in
1a4e5a6c
AC		 497 case t1 of
498 (TAction (p1, d1, r1), _) =>
499 (case t2 of
500 (TAction (p2, d2, r2), _) =>
501 let
502 val p' = predSimpl (CAnd (p1, p2), loc)
503
504 val d' = SM.foldli (fn (name, t, d') =>
505 case SM.find (r1, name) of
506 NONE =>
507 (case SM.find (d', name) of
508 NONE => SM.insert (d', name, t)
509 | SOME t' =>
510 (subTyp (t, t')
511 handle Unify ue =>
512 dte (WrongType ("Shared environment variable",
513 (EVar name, loc),
514 t,
515 t',
516 SOME ue));
517 d'))
518 | SOME t' =>
519 (subTyp (t, t')
520 handle Unify ue =>
521 dte (WrongType ("Shared environment variable",
522 (EVar name, loc),
523 t,
524 t',
525 SOME ue));
526 d'))
527 d1 d2
528 in
529 (TAction (p', d', r2), loc)
530 end
531 | (TError, _) => t2
532 | _ => (dte (WrongForm ("Action to be sequenced",
533 "action",
534 e2,
535 t2,
536 NONE));
537 (TError, loc)))
538 | (TError, _) => t1
539 | _ => (dte (WrongForm ("Action to be sequenced",
db427c67 540 "action",
1a4e5a6c
AC		 541 e1,
542 t1,
db427c67
AC		 543 NONE));
544 (TError, loc))
545 end
234b917a 546
1a4e5a6c 547
234b917a
AC		 548 | EWith (e1, e2) =>
549 let
550 val t1 = whnorm (checkExp G e1)
551 val t2 = whnorm (checkExp G e2)
552 in
553 case t1 of
1a4e5a6c 554 (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
234b917a
AC		 555 (case t2 of
556 (TAction (p, d, r), _) =>
557 if predImplies (pd, p) then
1a4e5a6c
AC		 558 let
559 val combineRecs =
560 SM.unionWithi (fn (name, t1, t2) =>
561 (subTyp (t1, t2)
562 handle Unify ue =>
563 dte (WrongType ("Environment variable",
564 (EVar name, loc),
565 t1,
566 t2,
567 SOME ue));
568 t2))
569 in
570 (TAction (pr, combineRecs (d, d1),
571 combineRecs (r, r1)), loc)
572 end
234b917a
AC		 573 else
574 (dte (WrongPred ("nested action",
575 pd,
576 p));
577 (TError, loc))
578 | (TError, _) => t2
579 | _ =>
580 (dte (WrongForm ("Body of nested action",
581 "action",
582 e2,
583 t2,
584 NONE));
585 (TError, loc)))
586 | (TError, _) => t1
587 | _ =>
588 (dte (WrongForm ("Container of nested action",
589 "action",
590 e1,
591 t1,
592 NONE));
593 (TError, loc))
594 end
595
596 | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
597 SM.empty, SM.empty), loc)
27d9de59
AC		 598 end
599
600exception Ununif
601
602fun ununif (tAll as (t, loc)) =
603 case t of
604 TBase _ => tAll
605 | TList t => (TList (ununif t), loc)
606 | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
607 | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
608 | TUnif (_, ref (SOME t)) => ununif t
234b917a 609 | TNested _ => tAll
27d9de59
AC		 610 | TError => tAll
611
612 | TUnif (_, ref NONE) => raise Ununif
613
614fun hasError (t, _) =
615 case t of
616 TBase _ => false
617 | TList t => hasError t
618 | TArrow (d, r) => hasError d orelse hasError r
619 | TAction (p, d, r) => List.exists hasError (SM.listItems d)
620 orelse List.exists hasError (SM.listItems r)
234b917a 621 | TNested _ => false
27d9de59
AC		 622 | TError => false
623 | TUnif (_, ref (SOME t)) => hasError t
624 | TUnif (_, ref NONE) => false
625
626
627fun checkUnit G (eAll as (_, loc)) =
628 let
629 val _ = resetUnif ()
630 val t = checkExp G eAll
631 in
632 if hasError t then
633 t
634 else
635 ununif t
636 handle Ununif =>
637 (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
638 printd (p_typ t);
639 t)
640 end
641
234b917a
AC		 642fun checkDecl G (d, _, loc) =
643 case d of
644 DExternType name => bindType G name
492c1cff
AC		 645 | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
646 | DVal (name, to, e) =>
647 let
648 val to =
649 case to of
650 NONE => (newUnif (), loc)
651 | SOME to => checkTyp G to
652
653 val t = checkExp G e
654 in
6be996d4 655 hasTyp (e, t, to)
492c1cff
AC		 656 handle Unify ue =>
657 describe_type_error loc
658 (WrongType ("Bound value",
659 e,
660 t,
661 to,
662 SOME ue));
663 bindVal G (name, to, SOME e)
664 end
234b917a
AC		 665
666fun checkFile G tInit (ds, eo) =
667 let
668 val G' = foldl (fn (d, G) => checkDecl G d) G ds
669 in
670 case eo of
671 NONE => ()
672 | SOME (e as (_, loc)) =>
673 let
674 val t = checkExp G' e
675 in
6be996d4 676 hasTyp (e, t, tInit)
234b917a
AC		 677 handle Unify ue =>
678 (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
679 preface ("Actual:", p_typ t);
680 preface ("Needed:", p_typ tInit))
681 end;
682 G'
683 end
684
27d9de59 685end
Unnamed repository; edit this file to name it for gitweb.