-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