1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006-2007, 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
27 val externFlag
= ref
false
28 fun allowExterns () = externFlag
:= true
29 fun disallowExterns () = externFlag
:= false
34 fun resetUnif () = unifCount
:= 0
41 str (chr (ord #
"A" + c
))
43 "UNIF" ^
Int.toString (c
- 26)
46 TUnif (name
, ref NONE
)
51 fun predImplies (p1All
as (p1
, _
), p2All
as (p2
, _
)) =
53 (_
, CAnd (p1
, p2
)) => predImplies (p1All
, p1
) andalso predImplies (p1All
, p2
)
54 |
(CAnd (p1
, p2
), _
) => predImplies (p1
, p2All
) orelse predImplies (p2
, p2All
)
56 |
(_
, CPrefix (CRoot
, _
)) => true
57 |
(CNot (CPrefix (CRoot
, _
), _
), _
) => true
59 |
(CRoot
, CRoot
) => true
61 |
(CConst s1
, CConst s2
) => s1
= s2
63 |
(CPrefix p1
, CPrefix p2
) => predImplies (p1
, p2
)
64 |
(_
, CPrefix p2
) => predImplies (p1All
, p2
)
66 |
(CNot p1
, CNot p2
) => predImplies (p2
, p1
)
67 |
(CRoot
, CNot (CConst _
, _
)) => true
68 |
(CConst s1
, CNot (CConst s2
, _
)) => s1
<> s2
72 fun predSimpl (pAll
as (p
, loc
)) =
76 | CPrefix p
=> (CPrefix (predSimpl p
), loc
)
77 | CNot p
=> (CNot (predSimpl p
), loc
)
80 val p1
' = predSimpl p1
81 val p2
' = predSimpl p2
84 (CAnd (c1
, c2
), _
) => predSimpl (CAnd (c1
, (CAnd (c2
, p2
'), loc
)), loc
)
85 | _
=> if predImplies (p2
', p1
') then
87 else if predImplies (p1
', p2
') then
90 (CAnd (p1
', p2
'), loc
)
93 fun subPred (p1
, p2
) =
94 if predImplies (p1
, p2
) then
97 raise (Unify (UnifyPred (p1
, p2
)))
99 fun subRecord
f (r1
, r2
) =
100 SM
.appi (fn (k
, v2
) =>
101 case SM
.find (r1
, k
) of
102 NONE
=> raise Describe
.UnequalDomains
103 | SOME v1
=> f (v1
, v2
)) r2
105 fun occurs
u (t
, _
) =
108 | TList t
=> occurs u t
109 |
TArrow (d
, r
) => occurs u d
orelse occurs u r
110 |
TAction (_
, d
, r
) =>
111 List.exists (occurs u
) (SM
.listItems d
)
112 orelse List.exists (occurs u
) (SM
.listItems r
)
113 |
TNested (_
, t
) => occurs u t
115 |
TUnif (_
, ref (SOME t
)) => occurs u t
116 |
TUnif (_
, u
') => u
= u
'
118 fun subTyp (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
120 (TBase s1
, TBase s2
) =>
124 raise Unify (UnifyTyp (t1All
, t2All
))
125 |
(TList t1
, TList t2
) => subTyp (t1
, t2
)
126 |
(TArrow (d1
, r1
), TArrow (d2
, r2
)) =>
130 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
132 subRecord
subTyp (d2
, d1
);
133 subRecord
subTyp (r1
, r2
);
134 subRecord
subTyp (r2
, r1
))
135 handle UnequalDomains
=> raise Unify (UnifyTyp (t1All
, t2All
)))
137 |
(TNested (d1
, r1
), TNested (d2
, r2
)) =>
141 |
(TUnif (_
, ref (SOME t1
)), _
) => subTyp (t1
, t2All
)
142 |
(_
, TUnif (_
, ref (SOME t2
))) => subTyp (t1All
, t2
)
144 |
(TUnif (_
, r1
), TUnif (_
, r2
)) =>
150 |
(TUnif (name
, r
), _
) =>
151 if occurs r t2All
then
152 raise (Unify (UnifyOccurs (name
, t2All
)))
156 |
(_
, TUnif (name
, r
)) =>
157 if occurs r t1All
then
158 raise (Unify (UnifyOccurs (name
, t1All
)))
165 | _
=> raise Unify (UnifyTyp (t1All
, t2All
))
172 fun whnorm (tAll
as (t
, loc
)) =
174 TUnif (_
, ref (SOME tAll
)) => whnorm tAll
177 fun baseCondition t
=
179 (TBase name
, _
) => typeRule name
181 (case baseCondition t
of
183 | SOME f
=> SOME (fn (EList ls
, _
) => List.all f ls
187 fun simplifyKindOf e
=
189 (EApp ((EVar s
, _
), e
'), _
) =>
190 (case Env
.function s
of
198 fun hasTyp (e
, t1
, t2
) =
199 if (case baseCondition t2
of
201 | SOME rule
=> rule (simplifyKindOf e
)) then
206 fun checkPred
G (p
, loc
) =
208 val err
= ErrorMsg
.error (SOME loc
)
213 if lookupContext G s
then
216 err ("Unbound context " ^ s
)
217 | CPrefix p
=> checkPred G p
218 | CNot p
=> checkPred G p
219 |
CAnd (p1
, p2
) => (checkPred G p1
; checkPred G p2
)
222 fun checkTyp
G (tAll
as (t
, loc
)) =
224 val err
= ErrorMsg
.error (SOME loc
)
228 if lookupType G name
then
231 (err ("Unbound type name " ^ name
);
233 | TList t
=> (TList (checkTyp G t
), loc
)
234 |
TArrow (d
, r
) => (TArrow (checkTyp G d
, checkTyp G r
), loc
)
235 |
TAction (p
, d
, r
) => (checkPred G p
;
236 (TAction (p
, SM
.map (checkTyp G
) d
,
237 SM
.map (checkTyp G
) r
), loc
))
238 |
TNested (p
, t
) => (checkPred G p
;
239 (TNested (p
, checkTyp G t
), loc
))
240 | TError
=> raise Fail
"TError in parser-generated type"
241 | TUnif _
=> raise Fail
"TUnif in parser-generated type"
244 fun envVarSetFrom
v (e
, _
) =
251 |
EGet (_
, _
, _
, e
) => envVarSetFrom v e
252 | ESeq es
=> foldr (fn (e
, found
) =>
255 | NONE
=> envVarSetFrom v e
)
257 |
ELocal (_
, e
) => envVarSetFrom v e
261 fun ununify (tAll
as (t
, _
)) =
263 TUnif (_
, ref (SOME t
)) => ununify t
266 fun checkExp
G (eAll
as (e
, loc
)) =
268 val dte
= Describe
.describe_type_error loc
271 EInt _
=> (TBase
"int", loc
)
272 | EString _
=> (TBase
"string", loc
)
275 val t
= (newUnif (), loc
)
277 foldl (fn (e
', ret
) =>
279 val t
' = checkExp G e
'
281 (hasTyp (eAll
, t
', t
);
283 (TList (TError
, loc
), loc
)
287 (dte (WrongType ("List element",
293 end) (TList t
, loc
) es
300 NONE
=> (newUnif (), loc
)
301 | SOME t
=> checkTyp G t
303 val G
' = bindVal
G (x
, t
, NONE
)
304 val t
' = checkExp G
' e
306 (TArrow (t
, t
'), loc
)
309 (case lookupVal G x
of
310 NONE
=> (dte (UnboundVariable x
);
313 |
EApp (func
, arg
) =>
315 val dom
= (newUnif (), loc
)
316 val ran
= (newUnif (), loc
)
318 val tf
= checkExp G func
319 val ta
= checkExp G arg
321 (hasTyp (func
, tf
, (TArrow (dom
, ran
), loc
));
322 hasTyp (arg
, ta
, dom
)
324 dte (WrongType ("Function argument",
331 (dte (WrongForm ("Function to be applied",
341 val p
' = checkPred G p
343 val G
' = bindVal
G (x
, (TAction (p
, SM
.empty
, SM
.empty
), loc
), NONE
)
344 val t
' = whnorm (checkExp G
' e
)
347 (TAction _
, _
) => (TNested (p
, t
'), loc
)
348 | _
=> (dte (WrongForm ("Body of nested configuration 'fn'",
360 (TAction ((CPrefix (CRoot
, loc
), loc
),
362 SM
.insert (SM
.empty
, evar
, t
)),
365 |
EGet (x
, topt
, evar
, rest
) =>
367 val xt
= (newUnif (), loc
)
368 val G
' = bindVal
G (x
, xt
, NONE
)
370 val rt
= whnorm (checkExp G
' rest
)
374 | SOME t
=> subTyp (xt
, checkTyp G t
);
377 (TAction (p
, d
, r
), _
) =>
378 (case SM
.find (d
, evar
) of
379 NONE
=> (TAction (p
, SM
.insert (d
, evar
, xt
), r
), loc
)
383 dte (WrongType ("Retrieved environment variable",
390 | _
=> (dte (WrongForm ("Body of environment variable read",
398 | ESeq
[] => raise Fail
"Empty ESeq"
399 | ESeq
[e1
] => checkExp G e1
400 |
ESeq (e1
:: rest
) =>
402 val e2
= (ESeq rest
, loc
)
404 val t1
= whnorm (checkExp G e1
)
405 val t2
= whnorm (checkExp G e2
)
408 (TAction (p1
, d1
, r1
), _
) =>
410 (TAction (p2
, d2
, r2
), _
) =>
412 val p
' = predSimpl (CAnd (p1
, p2
), loc
)
414 val d
' = SM
.foldli (fn (name
, t
, d
') =>
415 case SM
.find (r1
, name
) of
417 (case SM
.find (d
', name
) of
418 NONE
=> SM
.insert (d
', name
, t
)
420 ((case envVarSetFrom name e1
of
421 NONE
=> subTyp (t
, t
')
422 | SOME e
=> hasTyp (e
, t
, t
'))
424 dte (WrongType ("Shared environment variable",
431 ((case envVarSetFrom name e1
of
432 NONE
=> subTyp (t
, t
')
433 | SOME e
=> hasTyp (e
, t
, t
'))
435 dte (WrongType ("Shared environment variable",
443 val r
' = SM
.foldli (fn (name
, t
, r
') => SM
.insert (r
', name
, t
))
446 (TAction (p
', d
', r
'), loc
)
449 | _
=> (dte (WrongForm ("Action to be sequenced",
456 | _
=> (dte (WrongForm ("Action to be sequenced",
466 val t1
= whnorm (checkExp G e1
)
467 val t2
= whnorm (checkExp G e2
)
470 (TAction (p1
, d1
, r1
), _
) =>
472 (TAction (p2
, d2
, r2
), _
) =>
474 val p
' = predSimpl (CAnd (p1
, p2
), loc
)
476 val d
' = SM
.foldli (fn (name
, t
, d
') =>
477 case SM
.find (r1
, name
) of
479 (case SM
.find (d
', name
) of
480 NONE
=> SM
.insert (d
', name
, t
)
482 ((case envVarSetFrom name e1
of
483 NONE
=> subTyp (t
', t
)
484 | SOME e
=> hasTyp (e
, t
', t
))
486 dte (WrongType ("Shared environment variable",
493 ((case envVarSetFrom name e1
of
494 NONE
=> subTyp (t
', t
)
495 | SOME e
=> hasTyp (e
, t
', t
))
497 dte (WrongType ("Shared environment variable",
505 (TAction (p
', d
', r2
), loc
)
508 | _
=> (dte (WrongForm ("Action to be sequenced",
515 | _
=> (dte (WrongForm ("Action to be sequenced",
526 val t1
= whnorm (checkExp G e1
)
527 val t2
= whnorm (checkExp G e2
)
530 (TNested (pd
, (TAction (pr
, d1
, r1
), _
)), _
) =>
532 (TAction (p
, d
, r
), _
) =>
533 if predImplies (pd
, p
) then
536 SM
.unionWithi (fn (name
, t1
, t2
) =>
539 dte (WrongType ("Environment variable",
546 (TAction (pr
, combineRecs (d
, d1
),
547 combineRecs (r
, r1
)), loc
)
550 (dte (WrongPred ("nested action",
556 (dte (WrongForm ("Body of nested action",
564 (dte (WrongForm ("Container of nested action",
572 | ESkip
=> (TAction ((CPrefix (CRoot
, loc
), loc
),
573 SM
.empty
, SM
.empty
), loc
)
578 fun ununif (tAll
as (t
, loc
)) =
581 | TList t
=> (TList (ununif t
), loc
)
582 |
TArrow (d
, r
) => (TArrow (ununif d
, ununif r
), loc
)
583 |
TAction (p
, d
, r
) => (TAction (p
, SM
.map ununif d
, SM
.map ununif r
), loc
)
584 |
TUnif (_
, ref (SOME t
)) => ununif t
588 |
TUnif (_
, ref NONE
) => raise Ununif
590 fun hasError (t
, _
) =
593 | TList t
=> hasError t
594 |
TArrow (d
, r
) => hasError d
orelse hasError r
595 |
TAction (p
, d
, r
) => List.exists
hasError (SM
.listItems d
)
596 orelse List.exists
hasError (SM
.listItems r
)
599 |
TUnif (_
, ref (SOME t
)) => hasError t
600 |
TUnif (_
, ref NONE
) => false
603 fun checkUnit
G (eAll
as (_
, loc
)) =
606 val t
= checkExp G eAll
613 (ErrorMsg
.error (SOME loc
) "Unification variables remain in type:";
618 fun checkDecl
G (d
, _
, loc
) =
624 (ErrorMsg
.error (SOME loc
) "'extern type' not allowed in untrusted code";
626 |
DExternVal (name
, t
) =>
628 bindVal
G (name
, checkTyp G t
, NONE
)
630 (ErrorMsg
.error (SOME loc
) "'extern val' not allowed in untrusted code";
632 |
DVal (name
, to
, e
) =>
636 NONE
=> (newUnif (), loc
)
637 | SOME to
=> checkTyp G to
643 Describe
.describe_type_error loc
644 (WrongType ("Bound value",
649 bindVal
G (name
, to
, SOME e
)
651 | DContext name
=> bindContext G name
653 fun checkFile G
tInit (_
, ds
, eo
) =
655 val G
' = foldl (fn (d
, G
) => checkDecl G d
) G ds
659 |
SOME (e
as (_
, loc
)) =>
661 val t
= checkExp G
' e
665 (ErrorMsg
.error (SOME loc
) "Bad type for final expression of source file.";
666 preface ("Actual:", p_typ t
);
667 preface ("Needed:", p_typ tInit
))