81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : generalized unification of types
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : experimental
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedersubstitution and unification of types
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder-- | composition (reversed: first substitution first!)
0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaedercompSubst :: Subst -> Subst -> Subst
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedercompSubst s1 s2 = Map.union (Map.map (subst s2) s1) s2
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder-- | test if second scheme is a substitution instance
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaederinstScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederinstScheme tm c = asSchemes c (subsume tm)
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian MaederspecializedScheme :: ClassMap -> [TypeArg] -> [TypeArg] -> Bool
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederspecializedScheme cm args1 args2 = length args1 == length args2 && and
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (zipWith (\ (TypeArg _ v1 vk1 _ _ _ _) (TypeArg _ v2 vk2 _ _ _ _) ->
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian Maeder (v1 == v2 || v1 == NonVar) && case (vk1, vk2) of
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (VarKind k1, VarKind k2) -> lesserKind cm k1 k2
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder _ -> vk1 == vk2) args1 args2)
ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder-- | lift 'State' Int to 'State' Env
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedertoEnvState :: State Int a -> State Env a
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaedertoEnvState p = do
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder let (r, c) = runState p $ counter s
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder put s { counter = c }
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaedertoSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaedertoSchemes f sc1 sc2 = do
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (t1, _) <- freshInst sc1
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (t2, _) <- freshInst sc2
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder return $ f t1 t2
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaederasSchemes :: Int -> (Type -> Type -> a) -> TypeScheme -> TypeScheme -> a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederasSchemes c f sc1 sc2 = evalState (toSchemes f sc1 sc2) c
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedersubstTypeArg :: Subst -> TypeArg -> VarKind
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedersubstTypeArg s (TypeArg _ _ vk _ _ _ _) = case vk of
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder Downset super -> Downset $ substGen s super
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedermapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)]
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaedermapArgs s ts = foldr ( \ ta l ->
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder maybe l ( \ (_, t) -> (t, substTypeArg s ta) : l) $
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder find ( \ (j, _) -> getTypeVar ta == j) ts) []
9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian MaederfreshInst :: TypeScheme -> State Int (Type, [(Type, VarKind)])
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederfreshInst (TypeScheme tArgs t _) = do
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder let ls = leaves (< 0) t -- generic vars
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder vs = map snd ls
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder ts <- mkSubst vs
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder let s = Map.fromList $ zip (map fst ls) ts
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder return (substGen s t, mapArgs s (zip (map fst vs) ts) tArgs)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederinc :: State Int Int
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederfreshVar :: Id -> State Int (Id, Int)
ab0f35d8b9012e459417e086773049ce33dda2a0Christian MaederfreshVar i@(Id ts _ _) = do
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder return (Id [mkSimpleId $ "_v" ++ show c ++ case ts of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder [t] -> '_' : dropWhile (== '_') (tokStr t)
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder _ -> ""] [] $ posOfId i, c)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermkSingleSubst :: (Id, RawKind) -> State Int Type
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedermkSingleSubst (i, rk) = do
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder (ty, c) <- freshVar i
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return $ TypeName ty rk c
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermkSubst :: [(Id, RawKind)] -> State Int [Type]
7dec34aee2b609b9535c48d060e0f7baf3536457Christian MaedermkSubst = mapM mkSingleSubst
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maedertype Subst = Map.Map Int Type
0b14ccc700093e203914052bf6aceda3164af730Christian MaederflatKind :: Type -> RawKind
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian MaederflatKind = nonVarRawKind . rawKindOfType
9c03fbe72966fb21c99238c449efdb0126dae9deChristian MaedernoAbs :: Type -> Bool
9c03fbe72966fb21c99238c449efdb0126dae9deChristian MaedernoAbs t = case t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder TypeAbs {} -> False
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maedermatch :: TypeMap -> (Id -> Id -> Bool)
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder -> (Bool, Type) -> (Bool, Type) -> Result Subst
793945d4ac7c0f22760589c87af8e71427c76118Christian Maedermatch tm rel p1@(b1, ty1) p2@(b2, ty2) =
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder if flatKind ty1 == flatKind ty2 then case (ty1, ty2) of
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder (_, ExpandedType _ t2) | noAbs t2 -> match tm rel p1 (b2, t2)
9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder (ExpandedType _ t1, _) | noAbs t1 -> match tm rel (b1, t1) p2
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (_, TypeAppl (TypeName l _ _) t2) | l == lazyTypeId ->
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder match tm rel p1 (b2, t2)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (TypeAppl (TypeName l _ _) t1, _) | l == lazyTypeId ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder match tm rel (b1, t1) p2
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (_, KindedType t2 _ _) -> match tm rel p1 (b2, t2)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder (KindedType t1 _ _, _) -> match tm rel (b1, t1) p2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TypeName i1 _k1 v1, TypeName i2 _k2 v2)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | rel i1 i2 && v1 == v2 -> return eps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | v1 > 0 && b1 -> return $ Map.singleton v1 ty2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | v2 > 0 && b2 -> return $ Map.singleton v2 ty1
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder{- the following two conditions only guarantee that instScheme also matches for
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder a partial function that is mapped to a total one.
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Maybe a subtype condition is better. -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | not b1 && b2 && v1 == 0 && v2 == 0 && Set.member i1 (superIds tm i2) ||
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder b1 && not b2 && v1 == 0 && v2 == 0 && Set.member i2 (superIds tm i1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | otherwise -> uniResult "typename" ty1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "is not unifiable with typename" ty2
a716971174535184da7713ed308423e355a4aa66Christian Maeder (TypeName _ _ v1, _) -> case redStep ty2 of
a716971174535184da7713ed308423e355a4aa66Christian Maeder Just ry2 -> match tm rel p1 (b2, ry2)
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder if v1 > 0 && b1 then
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if null $ leaves (== v1) ty2 then
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder else uniResult "var" ty1 "occurs in" ty2
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder else uniResult "typename" ty1
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder "is not unifiable with type" ty2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (_, TypeName {}) -> match tm rel p2 p1
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder (TypeAppl f1 a1, TypeAppl f2 a2) -> case redStep ty1 of
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder Just ry1 -> match tm rel (b1, ry1) p2
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder Nothing -> case redStep ty2 of
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder Just ry2 -> match tm rel p1 (b2, ry2)
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder Nothing -> do
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder s1 <- match tm rel (b1, f1) (b2, f2)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder s2 <- match tm rel (b1, if b1 then subst s1 a1 else a1)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (b2, if b2 then subst s1 a2 else a2)
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder return $ compSubst s1 s2
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder _ -> if ty1 == ty2 then return eps else
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder uniResult "type" ty1 "is not unifiable with type" ty2
0b14ccc700093e203914052bf6aceda3164af730Christian Maeder else uniResult "type" ty1 "is not unifiable with differently kinded type" ty2
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedershapeMatch :: TypeMap -> Type -> Type -> Result Subst
15c12a3ac049a4528da05b1017b78145f308aeb0Christian MaedershapeMatch tm a b = match tm (const $ const True) (True, a) (True, b)
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maedersubsume :: TypeMap -> Type -> Type -> Bool
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maedersubsume tm a b =
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder isJust $ maybeResult $ match tm (==) (False, a) (True, b)
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder-- | substitute generic variables with negative index
ad623ebb0fa505940a039fe967ecff8749719ac9Christian MaedersubstGen :: Subst -> Type -> Type
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaedersubstGen m = foldType mapTypeRec
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { foldTypeName = \ t _ _ n -> if n >= 0 then t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Data.Maybe.fromMaybe t (Map.lookup n m)
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder , foldTypeAbs = \ t v1@(TypeArg _ _ _ _ c _ _) ty p ->
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder if Map.member c m then substGen (Map.delete c m) t else TypeAbs v1 ty p }
e9490701e16d1e8abd995ef876d6f937da93b412Christian MaedergetTypeOf :: Monad m => Term -> m Type
e9490701e16d1e8abd995ef876d6f937da93b412Christian MaedergetTypeOf trm = case trm of
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder TypedTerm _ q t _ -> return $ case q of
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder InType -> unitType
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder QualVar (VarDecl _ t _ _) -> return t
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder QualOp _ _ (TypeScheme _ t _) is _ _ -> return $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder substGen (Map.fromList $ zip [-1, -2 ..] is) t
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder TupleTerm ts ps -> if null ts then return unitType else do
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder tys <- mapM getTypeOf ts
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder return $ mkProductTypeWithRange tys ps
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder QuantifiedTerm _ _ t _ -> getTypeOf t
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder LetTerm _ _ t _ -> getTypeOf t
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder AsPattern _ p _ -> getTypeOf p
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder _ -> fail $ "getTypeOf: " ++ showDoc trm ""
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder-- | substitute variables with positive index
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maedersubst :: Subst -> Type -> Type
ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maedersubst m = if Map.null m then id else foldType mapTypeRec
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { foldTypeName = \ t _ _ n -> if n <= 0 then t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Data.Maybe.fromMaybe t (Map.lookup n m) }
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaedershowDocWithPos :: Type -> ShowS
de2f13b8310de00ca228385b1530660e036054c2Christian MaedershowDocWithPos a = let p = getRange a in
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder showChar '\'' . showDoc a . showChar '\''
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder . noShow (isNullRange p) (showChar ' ' .
cca95d3c69ecae807ff0129ccaa9be30d4c3e759Christian Maeder showParen True (showPos $ maximum (rangeToList p)))
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederuniResult :: String -> Type -> String -> Type -> Result Subst
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederuniResult s1 a s2 b = Result [Diag Hint ("in type\n" ++ " " ++ s1 ++ " " ++
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder showDocWithPos a "\n " ++ s2 ++ " " ++
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder showDocWithPos b "") nullRange] Nothing
c9b711a46e5138b2742727817c8071960e673073Christian Maeder-- | make representation of bound variables unique
c9b711a46e5138b2742727817c8071960e673073Christian Maedergeneralize :: [TypeArg] -> Type -> Type
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maedergeneralize tArgs = subst $ Map.fromList $ zipWith
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ( \ (TypeArg i _ _ rk c _ _) n -> (c, TypeName i rk n)) tArgs [-1, -2 ..]
59c036af82aff7fbe074455dad50477b7878e2d8Christian MaedergenTypeArgs :: [TypeArg] -> [TypeArg]
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedergenTypeArgs tArgs = snd $ mapAccumL ( \ n (TypeArg i v vk rk _ s ps) ->
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder (n - 1, TypeArg i v (case vk of
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder Downset t -> Downset $ generalize tArgs t
6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder _ -> vk) rk n s ps)) (-1) tArgs