1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006, Adam Chlipala
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
.
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
.
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
.
19 (* Domtool configuration language
type checking
*)
21 structure Tycheck
:> TYCHECK
= struct
25 structure SM
= StringMap
30 fun resetUnif () = unifCount
:= 0
37 str (chr (ord #
"A" + c
))
39 "UNIF" ^
Int.toString (c
- 26)
42 TUnif (name
, ref NONE
)
46 exception UnequalDomains
48 fun eqRecord
f (r1
, r2
) =
49 (SM
.appi (fn (k
, v1
) =>
50 case SM
.find (r2
, k
) of
51 NONE
=> raise UnequalDomains
56 raise UnequalDomains
) r1
;
57 SM
.appi (fn (k
, v2
) =>
58 case SM
.find (r1
, k
) of
59 NONE
=> raise UnequalDomains
64 raise UnequalDomains
) r2
;
66 handle UnequalDomains
=> false
68 fun eqPred ((p1
, _
), (p2
, _
)) =
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
)
79 fun eqTy (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
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
)
86 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
87 eqPred (p1
, p2
) andalso eqRecord
eqTy (d1
, d2
)
88 andalso eqRecord
eqTy (r1
, r2
)
90 |
(TNested (p1
, q1
), TNested (p2
, q2
)) =>
91 eqPred (p1
, p2
) andalso eqTy (q1
, q2
)
93 |
(TUnif (_
, ref (SOME t1
)), _
) => eqTy (t1
, t2All
)
94 |
(_
, TUnif (_
, ref (SOME t2
))) => eqTy (t1All
, t2
)
96 |
(TUnif (_
, r1
), TUnif (_
, r2
)) => r1
= r2
98 |
(TError
, TError
) => true
102 datatype unification_error
=
103 UnifyPred
of pred
* pred
104 | UnifyTyp
of typ
* typ
105 | UnifyOccurs
of string * typ
107 exception Unify
of unification_error
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
115 fun describe_unification_error t ue
=
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
) =>
125 (print
"Reason: Incompatible types.\n";
126 preface ("Have:", p_typ t1
);
127 preface ("Need:", p_typ t2
))
128 |
UnifyOccurs (name
, t
') =>
132 (print
"Reason: Occurs check failed for ";
137 fun describe_type_error loc te
=
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
))
157 fun predImplies (p1All
as (p1
, _
), p2All
as (p2
, _
)) =
159 (_
, CAnd (p1
, p2
)) => predImplies (p1All
, p1
) andalso predImplies (p1All
, p2
)
160 |
(CAnd (p1
, p2
), _
) => predImplies (p1
, p2All
) orelse predImplies (p2
, p2All
)
162 |
(_
, CPrefix (CRoot
, _
)) => true
163 |
(CNot (CPrefix (CRoot
, _
), _
), _
) => true
165 |
(CRoot
, CRoot
) => true
167 |
(CConst s1
, CConst s2
) => s1
= s2
169 |
(CPrefix p1
, CPrefix p2
) => predImplies (p1
, p2
)
170 |
(_
, CPrefix p2
) => predImplies (p1All
, p2
)
172 |
(CNot p1
, CNot p2
) => predImplies (p2
, p1
)
173 |
(CRoot
, CNot (CConst _
, _
)) => true
174 |
(CConst s1
, CNot (CConst s2
, _
)) => s1
<> s2
178 fun predSimpl (pAll
as (p
, loc
)) =
182 | CPrefix p
=> (CPrefix (predSimpl p
), loc
)
183 | CNot p
=> (CNot (predSimpl p
), loc
)
186 val p1
' = predSimpl p1
187 val p2
' = predSimpl p2
190 (CAnd (c1
, c2
), _
) => predSimpl (CAnd (c1
, (CAnd (c2
, p2
'), loc
)), loc
)
191 | _
=> if predImplies (p2
', p1
') then
193 else if predImplies (p1
', p2
') then
196 (CAnd (p1
', p2
'), loc
)
199 fun subPred (p1
, p2
) =
200 if predImplies (p1
, p2
) then
203 raise (Unify (UnifyPred (p1
, p2
)))
205 fun subRecord
f (r1
, r2
) =
206 SM
.appi (fn (k
, v2
) =>
207 case SM
.find (r1
, k
) of
208 NONE
=> raise UnequalDomains
209 | SOME v1
=> f (v1
, v2
)) r2
211 fun occurs
u (t
, _
) =
214 | TList t
=> occurs u t
215 |
TArrow (d
, r
) => occurs u d
orelse occurs u r
216 |
TAction (_
, d
, r
) =>
217 List.exists (occurs u
) (SM
.listItems d
)
218 orelse List.exists (occurs u
) (SM
.listItems r
)
219 |
TNested (_
, t
) => occurs u t
221 |
TUnif (_
, ref (SOME t
)) => occurs u t
222 |
TUnif (_
, u
') => u
= u
'
224 fun subTyp (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
226 (TBase s1
, TBase s2
) =>
230 raise Unify (UnifyTyp (t1All
, t2All
))
231 |
(TList t1
, TList t2
) => subTyp (t1
, t2
)
232 |
(TArrow (d1
, r1
), TArrow (d2
, r2
)) =>
236 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
238 subRecord
subTyp (d2
, d1
);
239 subRecord
subTyp (r1
, r2
);
240 subRecord
subTyp (r2
, r1
))
241 handle UnequalDomains
=> raise Unify (UnifyTyp (t1All
, t2All
)))
243 |
(TNested (d1
, r1
), TNested (d2
, r2
)) =>
247 |
(TUnif (_
, ref (SOME t1
)), _
) => subTyp (t1
, t2All
)
248 |
(_
, TUnif (_
, ref (SOME t2
))) => subTyp (t1All
, t2
)
250 |
(TUnif (_
, r1
), TUnif (_
, r2
)) =>
256 |
(TUnif (name
, r
), _
) =>
257 if occurs r t2All
then
258 raise (Unify (UnifyOccurs (name
, t2All
)))
262 |
(_
, TUnif (name
, r
)) =>
263 if occurs r t1All
then
264 raise (Unify (UnifyOccurs (name
, t1All
)))
271 | _
=> raise Unify (UnifyTyp (t1All
, t2All
))
278 fun whnorm (tAll
as (t
, loc
)) =
280 TUnif (_
, ref (SOME tAll
)) => whnorm tAll
283 fun baseCondition t
=
285 (TBase name
, _
) => typeRule name
287 (case baseCondition t
of
289 | SOME f
=> SOME (fn (EList ls
, _
) => List.all f ls
293 fun hasTyp (e
, t1
, t2
) =
294 if (case baseCondition t2
of
296 | SOME rule
=> rule e
) then
301 fun checkPred
G (p
, loc
) =
303 val err
= ErrorMsg
.error (SOME loc
)
308 if lookupContext G s
then
311 err ("Unbound context " ^ s
)
312 | CPrefix p
=> checkPred G p
313 | CNot p
=> checkPred G p
314 |
CAnd (p1
, p2
) => (checkPred G p1
; checkPred G p2
)
317 fun checkTyp
G (tAll
as (t
, loc
)) =
319 val err
= ErrorMsg
.error (SOME loc
)
323 if lookupType G name
then
326 (err ("Unbound type name " ^ name
);
328 | TList t
=> (TList (checkTyp G t
), loc
)
329 |
TArrow (d
, r
) => (TArrow (checkTyp G d
, checkTyp G r
), loc
)
330 |
TAction (p
, d
, r
) => (checkPred G p
;
331 (TAction (p
, SM
.map (checkTyp G
) d
,
332 SM
.map (checkTyp G
) r
), loc
))
333 |
TNested (p
, t
) => (checkPred G p
;
334 (TNested (p
, checkTyp G t
), loc
))
335 | TError
=> raise Fail
"TError in parser-generated type"
336 | TUnif _
=> raise Fail
"TUnif in parser-generated type"
339 fun envVarSetFrom
v (e
, _
) =
346 |
EGet (_
, _
, e
) => envVarSetFrom v e
347 | ESeq es
=> foldr (fn (e
, found
) =>
350 | NONE
=> envVarSetFrom v e
)
352 |
ELocal (_
, e
) => envVarSetFrom v e
356 fun checkExp
G (eAll
as (e
, loc
)) =
358 val dte
= describe_type_error loc
361 EInt _
=> (TBase
"int", loc
)
362 | EString _
=> (TBase
"string", loc
)
365 val t
= (newUnif (), loc
)
367 foldl (fn (e
', ret
) =>
369 val t
' = checkExp G e
'
371 (hasTyp (eAll
, t
', t
);
373 (TList (TError
, loc
), loc
)
377 (dte (WrongType ("List element",
383 end) (TList t
, loc
) es
390 NONE
=> (newUnif (), loc
)
391 | SOME t
=> checkTyp G t
393 val G
' = bindVal
G (x
, t
, NONE
)
394 val t
' = checkExp G
' e
396 (TArrow (t
, t
'), loc
)
399 (case lookupVal G x
of
400 NONE
=> (dte (UnboundVariable x
);
403 |
EApp (func
, arg
) =>
405 val dom
= (newUnif (), loc
)
406 val ran
= (newUnif (), loc
)
408 val tf
= checkExp G func
409 val ta
= checkExp G arg
411 (hasTyp (func
, tf
, (TArrow (dom
, ran
), loc
));
412 hasTyp (arg
, ta
, dom
)
414 dte (WrongType ("Function argument",
421 (dte (WrongForm ("Function to be applied",
431 val p
' = checkPred G p
433 val G
' = bindVal
G (x
, (TAction (p
, SM
.empty
, SM
.empty
), loc
), NONE
)
434 val t
' = checkExp G
' e
437 (TAction _
, _
) => (TNested (p
, t
'), loc
)
438 | _
=> (dte (WrongForm ("Body of nested configuration 'fn'",
450 (TAction ((CPrefix (CRoot
, loc
), loc
),
452 SM
.insert (SM
.empty
, evar
, t
)),
455 |
EGet (x
, evar
, rest
) =>
457 val xt
= (newUnif (), loc
)
458 val G
' = bindVal
G (x
, xt
, NONE
)
460 val rt
= whnorm (checkExp G
' rest
)
463 (TAction (p
, d
, r
), _
) =>
464 (case SM
.find (d
, evar
) of
465 NONE
=> (TAction (p
, SM
.insert (d
, evar
, xt
), r
), loc
)
469 dte (WrongType ("Retrieved environment variable",
476 | _
=> (dte (WrongForm ("Body of environment variable read",
484 | ESeq
[] => raise Fail
"Empty ESeq"
485 | ESeq
[e1
] => checkExp G e1
486 |
ESeq (e1
:: rest
) =>
488 val e2
= (ESeq rest
, loc
)
490 val t1
= whnorm (checkExp G e1
)
491 val t2
= whnorm (checkExp G e2
)
494 (TAction (p1
, d1
, r1
), _
) =>
496 (TAction (p2
, d2
, r2
), _
) =>
498 val p
' = predSimpl (CAnd (p1
, p2
), loc
)
500 val d
' = SM
.foldli (fn (name
, t
, d
') =>
501 case SM
.find (r1
, name
) of
503 (case SM
.find (d
', name
) of
504 NONE
=> SM
.insert (d
', name
, t
)
506 ((case envVarSetFrom name e1
of
507 NONE
=> subTyp (t
, t
')
508 | SOME e
=> hasTyp (e
, t
, t
'))
510 dte (WrongType ("Shared environment variable",
517 ((case envVarSetFrom name e1
of
518 NONE
=> subTyp (t
, t
')
519 | SOME e
=> hasTyp (e
, t
, t
'))
521 dte (WrongType ("Shared environment variable",
529 val r
' = SM
.foldli (fn (name
, t
, r
') => SM
.insert (r
', name
, t
))
532 (TAction (p
', d
', r
'), loc
)
535 | _
=> (dte (WrongForm ("Action to be sequenced",
542 | _
=> (dte (WrongForm ("Action to be sequenced",
552 val t1
= whnorm (checkExp G e1
)
553 val t2
= whnorm (checkExp G e2
)
556 (TAction (p1
, d1
, r1
), _
) =>
558 (TAction (p2
, d2
, r2
), _
) =>
560 val p
' = predSimpl (CAnd (p1
, p2
), loc
)
562 val d
' = SM
.foldli (fn (name
, t
, d
') =>
563 case SM
.find (r1
, name
) of
565 (case SM
.find (d
', name
) of
566 NONE
=> SM
.insert (d
', name
, t
)
568 ((case envVarSetFrom name e1
of
569 NONE
=> subTyp (t
', t
)
570 | SOME e
=> hasTyp (e
, t
', t
))
572 dte (WrongType ("Shared environment variable",
579 ((case envVarSetFrom name e1
of
580 NONE
=> subTyp (t
', t
)
581 | SOME e
=> hasTyp (e
, t
', t
))
583 dte (WrongType ("Shared environment variable",
591 (TAction (p
', d
', r2
), loc
)
594 | _
=> (dte (WrongForm ("Action to be sequenced",
601 | _
=> (dte (WrongForm ("Action to be sequenced",
612 val t1
= whnorm (checkExp G e1
)
613 val t2
= whnorm (checkExp G e2
)
616 (TNested (pd
, (TAction (pr
, d1
, r1
), _
)), _
) =>
618 (TAction (p
, d
, r
), _
) =>
619 if predImplies (pd
, p
) then
622 SM
.unionWithi (fn (name
, t1
, t2
) =>
625 dte (WrongType ("Environment variable",
632 (TAction (pr
, combineRecs (d
, d1
),
633 combineRecs (r
, r1
)), loc
)
636 (dte (WrongPred ("nested action",
642 (dte (WrongForm ("Body of nested action",
650 (dte (WrongForm ("Container of nested action",
658 | ESkip
=> (TAction ((CPrefix (CRoot
, loc
), loc
),
659 SM
.empty
, SM
.empty
), loc
)
664 fun ununif (tAll
as (t
, loc
)) =
667 | TList t
=> (TList (ununif t
), loc
)
668 |
TArrow (d
, r
) => (TArrow (ununif d
, ununif r
), loc
)
669 |
TAction (p
, d
, r
) => (TAction (p
, SM
.map ununif d
, SM
.map ununif r
), loc
)
670 |
TUnif (_
, ref (SOME t
)) => ununif t
674 |
TUnif (_
, ref NONE
) => raise Ununif
676 fun hasError (t
, _
) =
679 | TList t
=> hasError t
680 |
TArrow (d
, r
) => hasError d
orelse hasError r
681 |
TAction (p
, d
, r
) => List.exists
hasError (SM
.listItems d
)
682 orelse List.exists
hasError (SM
.listItems r
)
685 |
TUnif (_
, ref (SOME t
)) => hasError t
686 |
TUnif (_
, ref NONE
) => false
689 fun checkUnit
G (eAll
as (_
, loc
)) =
692 val t
= checkExp G eAll
699 (ErrorMsg
.error (SOME loc
) "Unification variables remain in type:";
704 fun checkDecl
G (d
, _
, loc
) =
706 DExternType name
=> bindType G name
707 |
DExternVal (name
, t
) => bindVal
G (name
, checkTyp G t
, NONE
)
708 |
DVal (name
, to
, e
) =>
712 NONE
=> (newUnif (), loc
)
713 | SOME to
=> checkTyp G to
719 describe_type_error loc
720 (WrongType ("Bound value",
725 bindVal
G (name
, to
, SOME e
)
727 | DContext name
=> bindContext G name
729 fun checkFile G
tInit (_
, ds
, eo
) =
731 val G
' = foldl (fn (d
, G
) => checkDecl G d
) G ds
735 |
SOME (e
as (_
, loc
)) =>
737 val t
= checkExp G
' e
741 (ErrorMsg
.error (SOME loc
) "Bad type for final expression of source file.";
742 preface ("Actual:", p_typ t
);
743 preface ("Needed:", p_typ tInit
))