* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
-*)
+ *)
(* Domtool configuration language type checking *)
structure Tycheck :> TYCHECK = struct
-open Ast Print
+open Ast Print Env
structure SM = StringMap
-type env = typ SM.map
-val empty = SM.empty
-
local
val unifCount = ref 0
in
eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
andalso eqRecord eqTy (r1, r2)
+ | (TNested (p1, q1), TNested (p2, q2)) =>
+ eqPred (p1, p2) andalso eqTy (q1, q2)
+
| (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
| (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
WrongType of string * exp * typ * typ * unification_error option
| WrongForm of string * string * exp * typ * unification_error option
| UnboundVariable of string
+ | WrongPred of string * pred * pred
fun preface (s, d) = printd (PD.hovBox (PD.PPS.Rel 0,
[PD.string s, PD.space 1, d]))
fun describe_unification_error t ue =
case ue of
UnifyPred (p1, p2) =>
- (print "Reason: Incompatible predicates.\n";
+ (print "Reason: Incompatible contexts.\n";
preface ("Have:", p_pred p1);
preface ("Need:", p_pred p2))
| UnifyTyp (t1, t2) =>
Option.app (describe_unification_error t) ueo)
| UnboundVariable name =>
ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
+ | WrongPred (place, p1, p2) =>
+ (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
+ preface ("Have:", p_pred p1);
+ preface ("Need:", p_pred p2))
fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
case (p1, p2) of
- (_, CPrefix (CRoot, _)) => true
+ (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
+ | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
+
+ | (_, CPrefix (CRoot, _)) => true
| (CNot (CPrefix (CRoot, _), _), _) => true
| (CRoot, CRoot) => true
| (CConst s1, CConst s2) => s1 = s2
| (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
+ | (_, CPrefix p2) => predImplies (p1All, p2)
| (CNot p1, CNot p2) => predImplies (p2, p1)
- | (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
- | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
-
| _ => false
fun predSimpl (pAll as (p, loc)) =
(CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
| _ => if predImplies (p2', p1') then
p2'
+ else if predImplies (p1', p2') then
+ p1'
else
(CAnd (p1', p2'), loc)
end
-fun unifyPred (p1, p2) =
+fun subPred (p1, p2) =
if predImplies (p1, p2) then
()
else
raise (Unify (UnifyPred (p1, p2)))
-fun unifyRecord f (r1, r2) =
- (SM.appi (fn (k, v1) =>
- case SM.find (r2, k) of
- NONE => raise UnequalDomains
- | SOME v2 => f (v1, v2)) r1;
- SM.appi (fn (k, v2) =>
- case SM.find (r1, k) of
- NONE => raise UnequalDomains
- | SOME v1 => f (v1, v2)) r2)
+fun subRecord f (r1, r2) =
+ SM.appi (fn (k, v2) =>
+ case SM.find (r1, k) of
+ NONE => raise UnequalDomains
+ | SOME v1 => f (v1, v2)) r2
fun occurs u (t, _) =
case t of
| TAction (_, d, r) =>
List.exists (occurs u) (SM.listItems d)
orelse List.exists (occurs u) (SM.listItems r)
+ | TNested (_, t) => occurs u t
| TError => false
| TUnif (_, ref (SOME t)) => occurs u t
| TUnif (_, u') => u = u'
-fun unify (t1All as (t1, _), t2All as (t2, _)) =
+fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
case (t1, t2) of
(TBase s1, TBase s2) =>
if s1 = s2 then
()
else
raise Unify (UnifyTyp (t1All, t2All))
- | (TList t1, TList t2) => unify (t1, t2)
+ | (TList t1, TList t2) => subTyp (t1, t2)
| (TArrow (d1, r1), TArrow (d2, r2)) =>
- (unify (d1, d2);
- unify (r1, r2))
+ (subTyp (d2, d1);
+ subTyp (r1, r2))
| (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
- ((unifyPred (p1, p2);
- unifyRecord unify (d1, d2);
- unifyRecord unify (r1, r2))
+ ((subPred (p2, p1);
+ subRecord subTyp (d2, d1);
+ subRecord subTyp (r1, r2);
+ subRecord subTyp (r2, r1))
handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
- | (TUnif (_, ref (SOME t1)), _) => unify (t1, t2All)
- | (_, TUnif (_, ref (SOME t2))) => unify (t1All, t2)
+ | (TNested (d1, r1), TNested (d2, r2)) =>
+ (subPred (d2, d1);
+ subTyp (r1, r2))
+
+ | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
+ | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
| (TUnif (_, r1), TUnif (_, r2)) =>
if r1 = r2 then
TUnif (_, ref (SOME tAll)) => whnorm tAll
| _ => tAll
+fun hasTyp (e, t1, t2) =
+ case whnorm t2 of
+ (TBase name, _) =>
+ (case typeRule name of
+ NONE => subTyp (t1, t2)
+ | SOME rule =>
+ if rule e then
+ ()
+ else
+ subTyp (t1, t2))
+ | _ => subTyp (t1, t2)
+
+fun checkTyp G (tAll as (t, loc)) =
+ let
+ val err = ErrorMsg.error (SOME loc)
+ in
+ case t of
+ TBase name =>
+ if lookupType G name then
+ tAll
+ else
+ (err ("Unbound type name " ^ name);
+ (TError, loc))
+ | TList t => (TList (checkTyp G t), loc)
+ | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
+ | TAction (p, d, r) => (TAction (p, SM.map (checkTyp G) d,
+ SM.map (checkTyp G) r), loc)
+ | TNested (p, t) => (TNested (p, checkTyp G t), loc)
+ | TError => raise Fail "TError in parser-generated type"
+ | TUnif _ => raise Fail "TUnif in parser-generated type"
+ end
+
fun checkExp G (eAll as (e, loc)) =
let
val dte = describe_type_error loc
let
val t' = checkExp G e'
in
- (unify (t', t);
+ (hasTyp (eAll, t', t);
if isError t' then
(TList (TError, loc), loc)
else
val t =
case to of
NONE => (newUnif (), loc)
- | SOME t => t
+ | SOME t => checkTyp G t
- val G' = SM.insert (G, x, t)
+ val G' = bindVal G (x, t, NONE)
val t' = checkExp G' e
in
(TArrow (t, t'), loc)
end
| EVar x =>
- (case SM.find (G, x) of
+ (case lookupVal G x of
NONE => (dte (UnboundVariable x);
(TError, loc))
| SOME t => t)
val tf = checkExp G func
val ta = checkExp G arg
in
- (unify (tf, (TArrow (dom, ran), loc));
- unify (ta, dom)
+ (hasTyp (func, tf, (TArrow (dom, ran), loc));
+ hasTyp (arg, ta, dom)
handle Unify ue =>
dte (WrongType ("Function argument",
arg,
| EGet (x, evar, rest) =>
let
val xt = (newUnif (), loc)
- val G' = SM.insert (G, x, xt)
+ val G' = bindVal G (x, xt, NONE)
val rt = whnorm (checkExp G' rest)
in
(case SM.find (d, evar) of
NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
| SOME xt' =>
- (unify (xt', xt)
+ (subTyp (xt', xt)
handle Unify ue =>
dte (WrongType ("Retrieved environment variable",
(EVar x, loc),
xt,
SOME ue));
rt))
+ | (TError, _) => rt
| _ => (dte (WrongForm ("Body of environment variable read",
"action",
rest,
(case SM.find (d', name) of
NONE => SM.insert (d', name, t)
| SOME t' =>
- (unify (t, t')
+ (subTyp (t, t')
handle Unify ue =>
dte (WrongType ("Shared environment variable",
(EVar name, loc),
SOME ue));
d'))
| SOME t' =>
- (unify (t, t')
+ (subTyp (t, t')
handle Unify ue =>
dte (WrongType ("Shared environment variable",
(EVar name, loc),
in
(TAction (p', d', r'), loc)
end
+ | (TError, _) => t2
| _ => (dte (WrongForm ("Action to be sequenced",
"action",
e2,
t2,
NONE));
(TError, loc)))
+ | (TError, _) => t1
| _ => (dte (WrongForm ("Action to be sequenced",
"action",
e1,
(TError, loc))
end
- | ELocal e =>
+ | ELocal (e1, e2) =>
let
- val rt = whnorm (checkExp G e)
+ val t1 = whnorm (checkExp G e1)
+ val t2 = whnorm (checkExp G e2)
in
- case rt of
- (TAction (p, d, _), _) =>
- (TAction (p, d, SM.empty), loc)
- | _ => (dte (WrongForm ("Body of local action",
+ case t1 of
+ (TAction (p1, d1, r1), _) =>
+ (case t2 of
+ (TAction (p2, d2, r2), _) =>
+ let
+ val p' = predSimpl (CAnd (p1, p2), loc)
+
+ val d' = SM.foldli (fn (name, t, d') =>
+ case SM.find (r1, name) of
+ NONE =>
+ (case SM.find (d', name) of
+ NONE => SM.insert (d', name, t)
+ | SOME t' =>
+ (subTyp (t, t')
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t,
+ t',
+ SOME ue));
+ d'))
+ | SOME t' =>
+ (subTyp (t, t')
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t,
+ t',
+ SOME ue));
+ d'))
+ d1 d2
+ in
+ (TAction (p', d', r2), loc)
+ end
+ | (TError, _) => t2
+ | _ => (dte (WrongForm ("Action to be sequenced",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | (TError, _) => t1
+ | _ => (dte (WrongForm ("Action to be sequenced",
"action",
- e,
- rt,
+ e1,
+ t1,
NONE));
(TError, loc))
end
+
+
+ | EWith (e1, e2) =>
+ let
+ val t1 = whnorm (checkExp G e1)
+ val t2 = whnorm (checkExp G e2)
+ in
+ case t1 of
+ (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
+ (case t2 of
+ (TAction (p, d, r), _) =>
+ if predImplies (pd, p) then
+ let
+ val combineRecs =
+ SM.unionWithi (fn (name, t1, t2) =>
+ (subTyp (t1, t2)
+ handle Unify ue =>
+ dte (WrongType ("Environment variable",
+ (EVar name, loc),
+ t1,
+ t2,
+ SOME ue));
+ t2))
+ in
+ (TAction (pr, combineRecs (d, d1),
+ combineRecs (r, r1)), loc)
+ end
+ else
+ (dte (WrongPred ("nested action",
+ pd,
+ p));
+ (TError, loc))
+ | (TError, _) => t2
+ | _ =>
+ (dte (WrongForm ("Body of nested action",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | (TError, _) => t1
+ | _ =>
+ (dte (WrongForm ("Container of nested action",
+ "action",
+ e1,
+ t1,
+ NONE));
+ (TError, loc))
+ end
+
+ | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
+ SM.empty, SM.empty), loc)
end
exception Ununif
| TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
| TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
| TUnif (_, ref (SOME t)) => ununif t
+ | TNested _ => tAll
| TError => tAll
| TUnif (_, ref NONE) => raise Ununif
| TArrow (d, r) => hasError d orelse hasError r
| TAction (p, d, r) => List.exists hasError (SM.listItems d)
orelse List.exists hasError (SM.listItems r)
+ | TNested _ => false
| TError => false
| TUnif (_, ref (SOME t)) => hasError t
| TUnif (_, ref NONE) => false
t)
end
+fun checkDecl G (d, _, loc) =
+ case d of
+ DExternType name => bindType G name
+ | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+ | DVal (name, to, e) =>
+ let
+ val to =
+ case to of
+ NONE => (newUnif (), loc)
+ | SOME to => checkTyp G to
+
+ val t = checkExp G e
+ in
+ hasTyp (e, t, to)
+ handle Unify ue =>
+ describe_type_error loc
+ (WrongType ("Bound value",
+ e,
+ t,
+ to,
+ SOME ue));
+ bindVal G (name, to, SOME e)
+ end
+
+fun checkFile G tInit (ds, eo) =
+ let
+ val G' = foldl (fn (d, G) => checkDecl G d) G ds
+ in
+ case eo of
+ NONE => ()
+ | SOME (e as (_, loc)) =>
+ let
+ val t = checkExp G' e
+ in
+ hasTyp (e, t, tInit)
+ handle Unify ue =>
+ (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
+ preface ("Actual:", p_typ t);
+ preface ("Needed:", p_typ tInit))
+ end;
+ G'
+ end
+
end