1 (* HCoop
Domtool (http
://hcoop
.sourceforge
.net
/)
2 * Copyright (c
) 2006-2007, Adam Chlipala
3 * Copyright (c
) 2014 Clinton Ebadi
<clinton@unknownlamer
.org
>
5 * This program is free software
; you can redistribute it
and/or
6 * modify it under the terms
of the GNU General Public License
7 * as published by the Free Software Foundation
; either version
2
8 * of the License
, or (at your option
) any later version
.
10 * This program is distributed
in the hope that it will be useful
,
11 * but WITHOUT ANY WARRANTY
; without even the implied warranty
of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE
. See the
13 * GNU General Public License for more details
.
15 * You should have received a copy
of the GNU General Public License
16 * along
with this program
; if not
, write to the Free Software
17 * Foundation
, Inc
., 51 Franklin Street
, Fifth Floor
, Boston
, MA
02110-1301, USA
.
20 (* Domtool configuration language
type checking
*)
22 structure Tycheck
:> TYCHECK
= struct
26 structure SM
= StringMap
28 val externFlag
= ref
false
29 fun allowExterns () = externFlag
:= true
30 fun disallowExterns () = externFlag
:= false
35 fun resetUnif () = unifCount
:= 0
42 str (chr (ord #
"A" + c
))
44 "UNIF" ^
Int.toString (c
- 26)
47 TUnif (name
, ref NONE
)
52 fun predImplies (p1All
as (p1
, _
), p2All
as (p2
, _
)) =
54 (_
, CAnd (p1
, p2
)) => predImplies (p1All
, p1
) andalso predImplies (p1All
, p2
)
55 |
(CAnd (p1
, p2
), _
) => predImplies (p1
, p2All
) orelse predImplies (p2
, p2All
)
57 |
(_
, CPrefix (CRoot
, _
)) => true
58 |
(CNot (CPrefix (CRoot
, _
), _
), _
) => true
60 |
(CRoot
, CRoot
) => true
62 |
(CConst s1
, CConst s2
) => s1
= s2
64 |
(CPrefix p1
, CPrefix p2
) => predImplies (p1
, p2
)
65 |
(_
, CPrefix p2
) => predImplies (p1All
, p2
)
67 |
(CNot p1
, CNot p2
) => predImplies (p2
, p1
)
68 |
(CRoot
, CNot (CConst _
, _
)) => true
69 |
(CConst s1
, CNot (CConst s2
, _
)) => s1
<> s2
73 fun predSimpl (pAll
as (p
, loc
)) =
77 | CPrefix p
=> (CPrefix (predSimpl p
), loc
)
78 | CNot p
=> (CNot (predSimpl p
), loc
)
81 val p1
' = predSimpl p1
82 val p2
' = predSimpl p2
85 (CAnd (c1
, c2
), _
) => predSimpl (CAnd (c1
, (CAnd (c2
, p2
'), loc
)), loc
)
86 | _
=> if predImplies (p2
', p1
') then
88 else if predImplies (p1
', p2
') then
91 (CAnd (p1
', p2
'), loc
)
94 fun subPred (p1
, p2
) =
95 if predImplies (p1
, p2
) then
98 raise (Unify (UnifyPred (p1
, p2
)))
100 fun subRecord
f (r1
, r2
) =
101 SM
.appi (fn (k
, v2
) =>
102 case SM
.find (r1
, k
) of
103 NONE
=> raise Describe
.UnequalDomains
104 | SOME v1
=> f (v1
, v2
)) r2
106 fun occurs
u (t
, _
) =
109 | TList t
=> occurs u t
110 |
TArrow (d
, r
) => occurs u d
orelse occurs u r
111 |
TAction (_
, d
, r
) =>
112 List.exists (occurs u
) (SM
.listItems d
)
113 orelse List.exists (occurs u
) (SM
.listItems r
)
114 |
TNested (_
, t
) => occurs u t
116 |
TUnif (_
, ref (SOME t
)) => occurs u t
117 |
TUnif (_
, u
') => u
= u
'
119 fun subTyp (t1All
as (t1
, _
), t2All
as (t2
, _
)) =
121 (TBase s1
, TBase s2
) =>
125 raise Unify (UnifyTyp (t1All
, t2All
))
126 |
(TList t1
, TList t2
) => subTyp (t1
, t2
)
127 |
(TArrow (d1
, r1
), TArrow (d2
, r2
)) =>
131 |
(TAction (p1
, d1
, r1
), TAction (p2
, d2
, r2
)) =>
133 subRecord
subTyp (d2
, d1
);
134 subRecord
subTyp (r1
, r2
);
135 subRecord
subTyp (r2
, r1
))
136 handle UnequalDomains
=> raise Unify (UnifyTyp (t1All
, t2All
)))
138 |
(TNested (d1
, r1
), TNested (d2
, r2
)) =>
142 |
(TUnif (_
, ref (SOME t1
)), _
) => subTyp (t1
, t2All
)
143 |
(_
, TUnif (_
, ref (SOME t2
))) => subTyp (t1All
, t2
)
145 |
(TUnif (_
, r1
), TUnif (_
, r2
)) =>
151 |
(TUnif (name
, r
), _
) =>
152 if occurs r t2All
then
153 raise (Unify (UnifyOccurs (name
, t2All
)))
157 |
(_
, TUnif (name
, r
)) =>
158 if occurs r t1All
then
159 raise (Unify (UnifyOccurs (name
, t1All
)))
166 | _
=> raise Unify (UnifyTyp (t1All
, t2All
))
173 fun whnorm (tAll
as (t
, loc
)) =
175 TUnif (_
, ref (SOME tAll
)) => whnorm tAll
178 fun baseCondition t
=
180 (TBase name
, _
) => typeRule name
182 (case baseCondition t
of
184 | SOME f
=> SOME (fn (EList ls
, _
) => List.all f ls
188 fun simplifyKindOf e
=
190 (EApp ((EVar s
, _
), e
'), _
) =>
191 (case Env
.function s
of
199 fun hasTyp (e
, t1
, t2
) =
200 if (case baseCondition t2
of
202 | SOME rule
=> rule (simplifyKindOf e
)) then
207 fun checkPred
G (p
, loc
) =
209 val err
= ErrorMsg
.error (SOME loc
)
214 if lookupContext G s
then
217 err ("Unbound context " ^ s
)
218 | CPrefix p
=> checkPred G p
219 | CNot p
=> checkPred G p
220 |
CAnd (p1
, p2
) => (checkPred G p1
; checkPred G p2
)
223 fun checkTyp
G (tAll
as (t
, loc
)) =
225 val err
= ErrorMsg
.error (SOME loc
)
229 if lookupType G name
then
232 (err ("Unbound type name " ^ name
);
234 | TList t
=> (TList (checkTyp G t
), loc
)
235 |
TArrow (d
, r
) => (TArrow (checkTyp G d
, checkTyp G r
), loc
)
236 |
TAction (p
, d
, r
) => (checkPred G p
;
237 (TAction (p
, SM
.map (checkTyp G
) d
,
238 SM
.map (checkTyp G
) r
), loc
))
239 |
TNested (p
, t
) => (checkPred G p
;
240 (TNested (p
, checkTyp G t
), loc
))
241 | TError
=> raise Fail
"TError in parser-generated type"
242 | TUnif _
=> raise Fail
"TUnif in parser-generated type"
245 fun envVarSetFrom
v (e
, _
) =
252 |
EGet (_
, _
, _
, e
) => envVarSetFrom v e
253 | ESeq es
=> foldr (fn (e
, found
) =>
256 | NONE
=> envVarSetFrom v e
)
258 |
ELocal (_
, e
) => envVarSetFrom v e
262 val ununify
= Describe
.ununify
264 fun checkExp
G (eAll
as (e
, loc
)) =
266 val dte
= Describe
.describe_type_error loc
269 EInt _
=> (TBase
"int", loc
)
270 | EString _
=> (TBase
"string", loc
)
273 val t
= (newUnif (), loc
)
275 foldl (fn (e
', ret
) =>
277 val t
' = checkExp G e
'
279 (hasTyp (eAll
, t
', t
);
281 (TList (TError
, loc
), loc
)
285 (dte (WrongType ("List element",
291 end) (TList t
, loc
) es
298 NONE
=> (newUnif (), loc
)
299 | SOME t
=> checkTyp G t
301 val G
' = bindVal
G (x
, t
, NONE
)
302 val t
' = checkExp G
' e
304 (TArrow (t
, t
'), loc
)
307 (case lookupVal G x
of
308 NONE
=> (dte (UnboundVariable x
);
311 |
EApp (func
, arg
) =>
313 val dom
= (newUnif (), loc
)
314 val ran
= (newUnif (), loc
)
316 val tf
= checkExp G func
317 val ta
= checkExp G arg
319 (hasTyp (func
, tf
, (TArrow (dom
, ran
), loc
));
320 hasTyp (arg
, ta
, dom
)
322 dte (WrongType ("Function argument",
329 (dte (WrongForm ("Function to be applied",
339 val p
' = checkPred G p
341 val G
' = bindVal
G (x
, (TAction (p
, SM
.empty
, SM
.empty
), loc
), NONE
)
342 val t
' = whnorm (checkExp G
' e
)
345 (TAction _
, _
) => (TNested (p
, t
'), loc
)
346 | _
=> (dte (WrongForm ("Body of nested configuration 'fn'",
358 (TAction ((CPrefix (CRoot
, loc
), loc
),
360 SM
.insert (SM
.empty
, evar
, t
)),
363 |
EGet (x
, topt
, evar
, rest
) =>
365 val xt
= (newUnif (), loc
)
366 val G
' = bindVal
G (x
, xt
, NONE
)
368 val rt
= whnorm (checkExp G
' rest
)
372 | SOME t
=> subTyp (xt
, checkTyp G t
);
375 (TAction (p
, d
, r
), _
) =>
376 (case SM
.find (d
, evar
) of
377 NONE
=> (TAction (p
, SM
.insert (d
, evar
, xt
), r
), loc
)
381 dte (WrongType ("Retrieved environment variable",
388 | _
=> (dte (WrongForm ("Body of environment variable read",
396 | ESeq
[] => raise Fail
"Empty ESeq"
397 | ESeq
[e1
] => checkExp G e1
398 |
ESeq (e1
:: rest
) =>
400 val e2
= (ESeq rest
, loc
)
402 val t1
= whnorm (checkExp G e1
)
403 val t2
= whnorm (checkExp G e2
)
406 (TAction (p1
, d1
, r1
), _
) =>
408 (TAction (p2
, d2
, r2
), _
) =>
410 val p
' = predSimpl (CAnd (p1
, p2
), loc
)
412 val d
' = SM
.foldli (fn (name
, t
, d
') =>
413 case SM
.find (r1
, name
) of
415 (case SM
.find (d
', name
) of
416 NONE
=> SM
.insert (d
', name
, t
)
418 ((case envVarSetFrom name e1
of
419 NONE
=> subTyp (t
, t
')
420 | SOME e
=> hasTyp (e
, t
, t
'))
422 dte (WrongType ("Shared environment variable",
429 ((case envVarSetFrom name e1
of
430 NONE
=> subTyp (t
, t
')
431 | SOME e
=> hasTyp (e
, t
, t
'))
433 dte (WrongType ("Shared environment variable",
441 val r
' = SM
.foldli (fn (name
, t
, r
') => SM
.insert (r
', name
, t
))
444 (TAction (p
', d
', r
'), loc
)
447 | _
=> (dte (WrongForm ("First action to be sequenced",
454 | _
=> (dte (WrongForm ("Second action to be sequenced",
464 val t1
= whnorm (checkExp G e1
)
465 val t2
= whnorm (checkExp G e2
)
468 (TAction (p1
, d1
, r1
), _
) =>
470 (TAction (p2
, d2
, r2
), _
) =>
472 val p
' = predSimpl (CAnd (p1
, p2
), loc
)
474 val d
' = SM
.foldli (fn (name
, t
, d
') =>
475 case SM
.find (r1
, name
) of
477 (case SM
.find (d
', name
) of
478 NONE
=> SM
.insert (d
', name
, t
)
480 ((case envVarSetFrom name e1
of
481 NONE
=> subTyp (t
', t
)
482 | SOME e
=> hasTyp (e
, t
', t
))
484 dte (WrongType ("Shared environment variable",
491 ((case envVarSetFrom name e1
of
492 NONE
=> subTyp (t
', t
)
493 | SOME e
=> hasTyp (e
, t
', t
))
495 dte (WrongType ("Shared environment variable",
503 (TAction (p
', d
', r2
), loc
)
506 | _
=> (dte (WrongForm ("Body of local settings",
513 | _
=> (dte (WrongForm ("Local settings",
524 val t1
= whnorm (checkExp G e1
)
525 val t2
= whnorm (checkExp G e2
)
528 (TNested (pd
, (TAction (pr
, d1
, r1
), _
)), _
) =>
530 (TAction (p
, d
, r
), _
) =>
531 if predImplies (pd
, p
) then
534 SM
.unionWithi (fn (name
, t1
, t2
) =>
537 dte (WrongType ("Environment variable",
544 (TAction (pr
, combineRecs (d
, d1
),
545 combineRecs (r
, r1
)), loc
)
548 (dte (WrongPred ("nested action",
554 (dte (WrongForm ("Body of nested action",
562 (dte (WrongForm ("Container of nested action",
570 | ESkip
=> (TAction ((CPrefix (CRoot
, loc
), loc
),
571 SM
.empty
, SM
.empty
), loc
)
573 |
EIf (e1
, e2
, e3
) =>
575 val t1
= checkExp G e1
576 val t2
= checkExp G e2
577 val t3
= checkExp G e3
578 val bool = (TBase
"bool", loc
)
582 dte (WrongType ("\"if\" test",
587 (subTyp (t2
, t3
); t3
)
589 ((subTyp (t3
, t2
); t2
)
591 (dte (WrongType ("\"else\" case",
602 fun ununif (tAll
as (t
, loc
)) =
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
612 |
TUnif (_
, ref NONE
) => raise Ununif
614 fun hasError (t
, _
) =
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
)
623 |
TUnif (_
, ref (SOME t
)) => hasError t
624 |
TUnif (_
, ref NONE
) => false
627 fun checkUnit
G (eAll
as (_
, loc
)) =
630 val t
= checkExp G eAll
637 (ErrorMsg
.error (SOME loc
) "Unification variables remain in type:";
642 fun checkDecl
G (d
, _
, loc
) =
648 (ErrorMsg
.error (SOME loc
) "'extern type' not allowed in untrusted code";
650 |
DExternVal (name
, t
) =>
652 bindVal
G (name
, checkTyp G t
, NONE
)
654 (ErrorMsg
.error (SOME loc
) "'extern val' not allowed in untrusted code";
656 |
DVal (name
, to
, e
) =>
660 NONE
=> (newUnif (), loc
)
661 | SOME to
=> checkTyp G to
667 Describe
.describe_type_error loc
668 (WrongType ("Bound value",
673 bindVal
G (name
, to
, SOME e
)
675 |
DEnv (name
, to
, e
) =>
679 NONE
=> (newUnif (), loc
)
680 | SOME to
=> checkTyp G to
686 Describe
.describe_type_error loc
687 (WrongType ("Dynamically bound value",
692 bindInitialDynEnvVal
G (name
, to
, e
)
694 | DContext name
=> bindContext G name
696 fun printActionDiffs
{have
, need
} =
697 case (ununif have
, ununif need
) of
698 ((TAction (p1
, in1
, out1
), loc
), (TAction (p2
, in2
, out2
), _
)) =>
701 if predImplies (p1
, p2
) then
704 (ErrorMsg
.error (SOME loc
) "Files provides the wrong kind of configuration.";
705 preface ("Have:", p_pred p1
);
706 preface ("Need:", p_pred p2
))
709 SM
.appi (fn (name
, t
) =>
710 case SM
.find (in2
, name
) of
711 NONE
=> (ErrorMsg
.error (SOME loc
) "An unavailable environment variable is used.";
712 print ("Name: " ^ name ^
"\n");
713 preface ("Type:", p_typ t
))
717 (ErrorMsg
.error (SOME loc
) "Wrong type for environment variable.";
718 print (" Name: " ^ name ^
"\n");
719 preface (" Has type:", p_typ t
');
720 preface ("Used with type:", p_typ t
)))
724 SM
.appi (fn (name
, t
) =>
725 case SM
.find (out1
, name
) of
726 NONE
=> (ErrorMsg
.error (SOME loc
) "Missing an output environment variable.";
727 print ("Name: " ^ name ^
"\n");
728 preface ("Type:", p_typ t
))
732 (ErrorMsg
.error (SOME loc
) "Wrong type for output environment variable.";
733 print (" Name: " ^ name ^
"\n");
734 preface (" Has type:", p_typ t
');
735 preface ("Need type:", p_typ t
)))
746 fun checkFile
G (prog
as (_
, ds
, eo
)) =
748 val G
' = foldl (fn (d
, G
) => checkDecl G d
) G ds
750 fun tInitial prog env
=
751 (* This should likely only take the dynamic env
as an argument
*)
757 | ESeq es
=> List.all allSets es
760 val dmy
= ErrorMsg
.dummyLoc
762 fun bodyType (_
, _
, SOME e
) =
764 (CPrefix (CRoot
, dmy
), dmy
)
767 | bodyType _
= (CRoot
, dmy
)
769 (TAction (bodyType prog
,
770 Env
.initialDynEnvTypes env
,
778 |
SOME (e
as (_
, loc
)) =>
780 val t
= checkExp G
' e
781 val tInit
= tInitial prog G
'
785 if printActionDiffs
{have
= t
, need
= tInit
} then
788 ErrorMsg
.error (SOME loc
) "File ends in something that isn't a directive."