end
end
-exception UnequalDomains
-
-fun eqRecord f (r1, r2) =
- (SM.appi (fn (k, v1) =>
- case SM.find (r2, k) of
- NONE => raise UnequalDomains
- | SOME v2 =>
- if f (v1, v2) then
- ()
- else
- raise UnequalDomains) r1;
- SM.appi (fn (k, v2) =>
- case SM.find (r1, k) of
- NONE => raise UnequalDomains
- | SOME v1 =>
- if f (v1, v2) then
- ()
- else
- raise UnequalDomains) r2;
- true)
- handle UnequalDomains => false
-
-fun eqPred ((p1, _), (p2, _)) =
- case (p1, p2) of
- (CRoot, CRoot) => true
- | (CConst s1, CConst s2) => s1 = s2
- | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
- | (CNot p1, CNot p2) => eqPred (p1, p2)
- | (CAnd (p1, q1), CAnd (p2, q2)) =>
- eqPred (p1, p2) andalso eqPred (q1, q2)
-
- | _ => false
-
-fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
- case (t1, t2) of
- (TBase s1, TBase s2) => s1 = s2
- | (TList t1, TList t2) => eqTy (t1, t2)
- | (TArrow (d1, r1), TArrow (d2, r2)) =>
- eqTy (d1, d2) andalso eqTy (r1, r2)
-
- | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
- 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)
-
- | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
-
- | (TError, TError) => true
-
- | _ => false
fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
case (p1, p2) of
fun subRecord f (r1, r2) =
SM.appi (fn (k, v2) =>
case SM.find (r1, k) of
- NONE => raise UnequalDomains
+ NONE => raise Describe.UnequalDomains
| SOME v1 => f (v1, v2)) r2
fun occurs u (t, _) =
| _ => false))
| _ => NONE
+fun simplifyKindOf e =
+ case e of
+ (EApp ((EVar s, _), e'), _) =>
+ (case Env.function s of
+ NONE => e
+ | SOME f =>
+ case f [e'] of
+ NONE => e
+ | SOME e => e)
+ | _ => e
+
fun hasTyp (e, t1, t2) =
if (case baseCondition t2 of
NONE => false
- | SOME rule => rule e) then
+ | SOME rule => rule (simplifyKindOf e)) then
()
else
subTyp (t1, t2)
ununif t
handle Ununif =>
(ErrorMsg.error (SOME loc) "Unification variables remain in type:";
- printd (p_typ t);
+ output (p_typ t);
t)
end