| UnboundVariable name =>
ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
-fun unifyPred (p1All as (p1, _), p2All as (p2, _)) =
+fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
case (p1, p2) of
- (CRoot, CRoot) => ()
- | (CConst s1, CConst s2) =>
- if s1 = s2 then
- ()
- else
- raise (Unify (UnifyPred (p1All, p2All)))
- | (CPrefix p1, CPrefix p2) => unifyPred (p1, p2)
- | (CNot p1, CNot p2) => unifyPred (p1, p2)
- | (CAnd (p1, q1), CAnd (p2, q2)) =>
- (unifyPred (p1, p2);
- unifyPred (q1, q2))
+ (_, CPrefix (CRoot, _)) => true
+ | (CNot (CPrefix (CRoot, _), _), _) => true
+
+ | (CRoot, CRoot) => true
+
+ | (CConst s1, CConst s2) => s1 = s2
+
+ | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
+
+ | (CNot p1, CNot p2) => predImplies (p2, p1)
- | _ => raise (Unify (UnifyPred (p1All, p2All)))
+ | (_, 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)) =
+ case p of
+ CRoot => pAll
+ | CConst _ => pAll
+ | CPrefix p => (CPrefix (predSimpl p), loc)
+ | CNot p => (CNot (predSimpl p), loc)
+ | CAnd (p1, p2) =>
+ let
+ val p1' = predSimpl p1
+ val p2' = predSimpl p2
+ in
+ case p1' of
+ (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
+ | _ => if predImplies (p2', p1') then
+ p2'
+ else
+ (CAnd (p1', p2'), loc)
+ end
+
+fun unifyPred (p1, p2) =
+ if predImplies (p1, p2) then
+ ()
+ else
+ raise (Unify (UnifyPred (p1, p2)))
fun unifyRecord f (r1, r2) =
(SM.appi (fn (k, v1) =>
(TError, _) => true
| _ => false
+fun whnorm (tAll as (t, loc)) =
+ case t of
+ TUnif (_, ref (SOME tAll)) => whnorm tAll
+ | _ => tAll
+
fun checkExp G (eAll as (e, loc)) =
let
val dte = describe_type_error loc
SOME ue));
(TError, loc))
end
-
- | _ => raise Fail "Not ready for that expression yet!"
+
+ | ESet (evar, e) =>
+ let
+ val t = checkExp G e
+ in
+ (TAction ((CPrefix (CRoot, loc), loc),
+ SM.empty,
+ SM.insert (SM.empty, evar, t)),
+ loc)
+ end
+ | EGet (x, evar, rest) =>
+ let
+ val xt = (newUnif (), loc)
+ val G' = SM.insert (G, x, xt)
+
+ val rt = whnorm (checkExp G' rest)
+ in
+ case rt of
+ (TAction (p, d, r), _) =>
+ (case SM.find (d, evar) of
+ NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
+ | SOME xt' =>
+ (unify (xt', xt)
+ handle Unify ue =>
+ dte (WrongType ("Retrieved environment variable",
+ (EVar x, loc),
+ xt',
+ xt,
+ SOME ue));
+ rt))
+ | _ => (dte (WrongForm ("Body of environment variable read",
+ "action",
+ rest,
+ rt,
+ NONE));
+ (TError, loc))
+ end
+
+ | ESeq [] => raise Fail "Empty ESeq"
+ | ESeq [e1] => checkExp G e1
+ | ESeq (e1 :: rest) =>
+ let
+ val e2 = (ESeq rest, loc)
+
+ val t1 = whnorm (checkExp G e1)
+ val t2 = whnorm (checkExp G e2)
+ in
+ 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' =>
+ (unify (t, t')
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t,
+ t',
+ SOME ue));
+ d'))
+ | SOME t' =>
+ (unify (t, t')
+ handle Unify ue =>
+ dte (WrongType ("Shared environment variable",
+ (EVar name, loc),
+ t,
+ t',
+ SOME ue));
+ d'))
+ d1 d2
+
+ val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
+ r1 r2
+ in
+ (TAction (p', d', r'), loc)
+ end
+ | _ => (dte (WrongForm ("Action to be sequenced",
+ "action",
+ e2,
+ t2,
+ NONE));
+ (TError, loc)))
+ | _ => (dte (WrongForm ("Action to be sequenced",
+ "action",
+ e1,
+ t1,
+ NONE));
+ (TError, loc))
+ end
+
+ | ELocal e =>
+ let
+ val rt = whnorm (checkExp G e)
+ in
+ case rt of
+ (TAction (p, d, _), _) =>
+ (TAction (p, d, SM.empty), loc)
+ | _ => (dte (WrongForm ("Body of local action",
+ "action",
+ e,
+ rt,
+ NONE));
+ (TError, loc))
+ end
end
exception Ununif