66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |

81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : generalized unification of types

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : Christian.Maeder@dfki.de

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederStability : experimental

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederPortability : portable

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maedersubstitution and unification of types

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maedermodule HasCASL.Unify where

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.AsUtils

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport HasCASL.PrintAs ()

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport HasCASL.TypeAna

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport HasCASL.Le

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederimport qualified Data.Map as Map

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.DocUtils

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Id

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Lib.State

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Result

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Data.List as List

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Data.Maybe

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | bound vars

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedergenVarsOf :: Type -> [(Id, RawKind)]

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedergenVarsOf = map snd . leaves (<0)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder-- | composition (reversed: first substitution first!)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercompSubst :: Subst -> Subst -> Subst

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercompSubst s1 s2 = Map.union (Map.map (subst s2) s1) s2

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | unifiability of type schemes including instantiation with fresh variables

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- (and looking up type aliases)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederisUnifiable :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederisUnifiable tm c = asSchemes c (unify tm)

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | test if second scheme is a substitution instance

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederinstScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaederinstScheme tm c = asSchemes c (subsume tm)

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder-- | lift 'State' Int to 'State' Env

8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian MaedertoEnvState :: State Int a -> State Env a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertoEnvState p =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do s <- get

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let (r, c) = runState p $ counter s

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder put s { counter = c }

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return r

07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedertoSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertoSchemes f sc1 sc2 =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do (t1, _) <- freshInst sc1

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (t2, _) <- freshInst sc2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ f t1 t2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederasSchemes :: Int -> (Type -> Type -> a) -> TypeScheme -> TypeScheme -> a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederasSchemes c f sc1 sc2 = fst $ runState (toSchemes f sc1 sc2) c

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedersubstTypeArg :: Subst -> TypeArg -> VarKind

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersubstTypeArg s (TypeArg _ _ vk _ _ _ _) = case vk of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Downset super -> Downset $ subst s super

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> vk

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)]

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapArgs s ts = foldr ( \ ta l ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder maybe l ( \ (_, t) -> (t, substTypeArg s ta) : l) $

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder find ( \ (j, _) -> getTypeVar ta == j) ts) []

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederfreshInst :: TypeScheme -> State Int (Type, [(Type, VarKind)])

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederfreshInst (TypeScheme tArgs t _) =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do let ls = leaves (< 0) t -- generic vars

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder vs = map snd ls

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ts <- mkSubst vs

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let s = Map.fromList $ zip (map fst ls) ts

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (subst s t, mapArgs s (zip (map fst vs) ts) tArgs)

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinc :: State Int Int

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederinc = do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder c <- get

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder put (c + 1)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return c

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederfreshVar :: Id -> State Int (Id, Int)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederfreshVar i@(Id ts _ _) = do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder c <- inc

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (Id [mkSimpleId $ "_v" ++ show c ++ case ts of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [t] -> "_" ++ dropWhile (== '_') (tokStr t)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> ""] [] $ posOfId i, c)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermkSingleSubst :: (Id, RawKind) -> State Int Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermkSingleSubst (i, rk) = do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (ty, c) <- freshVar i

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder return $ TypeName ty rk c

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermkSubst :: [(Id, RawKind)] -> State Int [Type]

81d182b21020b815887e9057959228546cf61b6bChristian MaedermkSubst = mapM mkSingleSubst

5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedertype Subst = Map.Map Int Type

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedereps :: Subst

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedereps = Map.empty

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederflatKind :: Type -> RawKind

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederflatKind = mapKindV (const InVar) id . rawKindOfType

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedernoAbs :: Type -> Bool

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedernoAbs t = case t of

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder TypeAbs _ _ _ -> False

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder _ -> True

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maedermatch :: TypeMap -> (Id -> Id -> Bool)

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder -> (Bool, Type) -> (Bool, Type) -> Result Subst

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedermatch tm rel p1@(b1, ty1) p2@(b2, ty2) =

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder if flatKind ty1 == flatKind ty2 then case (ty1, ty2) of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (_, ExpandedType _ t2) | noAbs t2 -> match tm rel p1 (b2, t2)

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder (ExpandedType _ t1, _) | noAbs t1 -> match tm rel (b1, t1) p2

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder (_, TypeAppl (TypeName l _ _) t2) | l == lazyTypeId ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder match tm rel p1 (b2, t2)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (TypeAppl (TypeName l _ _) t1, _) | l == lazyTypeId ->

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder match tm rel (b1, t1) p2

8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder (_, KindedType t2 _ _) -> match tm rel p1 (b2, t2)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (KindedType t1 _ _, _) -> match tm rel (b1, t1) p2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (TypeName i1 _k1 v1, TypeName i2 _k2 v2) ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if rel i1 i2 && v1 == v2

61091743da1a9ed6dfd5e077fdcc972553358962Christian Maeder then return eps

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else if v1 > 0 && b1 then return $ Map.singleton v1 ty2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else if v2 > 0 && b2 then return $ Map.singleton v2 ty1

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder{- the following two conditions only guarantee that instScheme also matches for

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder a partial function that is mapped to a total one.

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder Maybe a subtype condition is better. -}

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else if not b1 && b2 && v1 == 0 && v2 == 0 && Set.member i1

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (superIds tm i2) then return eps

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder else if b1 && not b2 && v1 == 0 && v2 == 0 && Set.member i2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (superIds tm i1) then return eps

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder else uniResult "typename" ty1 "is not unifiable with typename" ty2

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder (TypeName _ _ v1, _) ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if hasRedex ty2 then match tm rel p1 (b2, redStep ty2) else

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if v1 > 0 && b1 then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null $ leaves (==v1) ty2 then

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder return $ Map.singleton v1 ty2

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder else uniResult "var" ty1 "occurs in" ty2

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder else uniResult "typename" ty1

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder "is not unifiable with type" ty2

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder (_, TypeName _ _ _) -> match tm rel p2 p1

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder (TypeAppl f1 a1, TypeAppl f2 a2) ->

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let res = do

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder s1 <- match tm rel (b1, f1) (b2, f2)

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder s2 <- match tm rel (b1, if b1 then subst s1 a1 else a1)

405b95208385572f491e1e0207d8d14e31022fa6Christian Maeder (b2, if b2 then subst s1 a2 else a2)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ compSubst s1 s2

8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder res1@(Result _ ms1) = if hasRedex ty1 then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder match tm rel (b1, redStep ty1) p2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else fail "match1"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder res2@(Result _ ms2) = if hasRedex ty2 then

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder match tm rel p1 (b2, redStep ty2)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else fail "match2"

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in case ms1 of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> case ms2 of

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> res

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just _ -> res2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just _ -> res1

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> if ty1 == ty2 then return eps else

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder uniResult "type" ty1 "is not unifiable with type" ty2

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder else uniResult "type" ty1 "is not unifiable with differently kinded type" ty2

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- | most general unifier via 'match'

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- where both sides may contribute substitutions

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermgu :: TypeMap -> Type -> Type -> Result Subst

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedermgu tm a b = match tm (==) (True, a) (True, b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermguList :: TypeMap -> [Type] -> [Type] -> Result Subst

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermguList tm l1 l2 = case (l1, l2) of

341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder ([], []) -> return eps

341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder (h1 : t1, h2 : t2) -> do

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder s1 <- mgu tm h1 h2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder s2 <- mguList tm (map (subst s1) t1) $ map (subst s1) t2

return $ compSubst s1 s2

_ -> mkError "no unification of differently long argument lists"

(head $ l1 ++ l2)

shapeMatch :: TypeMap -> Type -> Type -> Result Subst

shapeMatch tm a b = match tm (const $ const True) (True, a) (True, b)

unify :: TypeMap -> Type -> Type -> Bool

unify tm a b = isJust $ maybeResult $ mgu tm a b

subsume :: TypeMap -> Type -> Type -> Bool

subsume tm a b =

isJust $ maybeResult $ match tm (==) (False, a) (True, b)

subst :: Subst -> Type -> Type

subst m = rename (\ i k n ->

case Map.lookup n m of

Just s -> s

_ -> TypeName i k n)

showDocWithPos :: Type -> ShowS

showDocWithPos a = let p = getRange a in

showChar '\'' . showDoc a . showChar '\''

. noShow (isNullRange p) (showChar ' ' .

showParen True (showPos $ maximumBy comparePos (rangeToList p)))

uniResult :: String -> Type -> String -> Type -> Result Subst

uniResult s1 a s2 b =

Result [Diag Hint ("in type\n" ++ " " ++ s1 ++ " " ++

showDocWithPos a "\n " ++ s2 ++ " " ++

showDocWithPos b "") nullRange] Nothing

-- | make representation of bound variables unique

generalize :: [TypeArg] -> Type -> Type

generalize tArgs =

subst $ Map.fromList $ zipWith

( \ (TypeArg i _ _ rk c _ _) n ->

(c, TypeName i rk n)) tArgs [-1, -2..]

genTypeArgs :: [TypeArg] -> [TypeArg]

genTypeArgs tArgs = snd $ mapAccumL ( \ n (TypeArg i v vk rk _ s ps) ->

(n-1, TypeArg i v (case vk of

Downset t -> Downset $ generalize tArgs t

_ -> vk) rk n s ps)) (-1) tArgs