hets/HasCASL/Unify.hs

	Unify.hs revision 36c6cc568751e4235502cfee00ba7b597dae78dc
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannModule      :  $Header$
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannCopyright   :  (c) Christian Maeder and Uni Bremen 2003
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannMaintainer  :  maeder@tzi.de
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannStability   :  experimental
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannPortability :  portable
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannsubstitution and unification of types
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-}
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannmodule HasCASL.Unify where
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport HasCASL.As
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.AsUtils
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport HasCASL.Le
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport qualified Common.Lib.Map as Map
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport qualified Common.Lib.Set as Set
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Common.PrettyPrint
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Id
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Lib.State
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.Result
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Data.List as List
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannimport Data.Maybe
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- | bound vars
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmanngenVarsOf :: Type -> [(Id, RawKind)]
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmanngenVarsOf = map snd . leaves (<0)
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
d024d9de9b6e7a7cfd72ef72d8efb0e57da5a01bChristian Maeder-- | vars or other ids
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannleaves :: (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannleaves b t =
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann    case t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           TypeName j k i -> if b(i)
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann                             then [(i, (j, k))]
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann                             else []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           TypeAppl t1 t2 -> leaves b t1 `List.union` leaves b t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           ExpandedType _ t2 -> leaves b t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           KindedType tk _ _ -> leaves b tk
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           LazyType tl _ -> leaves b tl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           ProductType l _ -> foldl List.union [] $ map (leaves b) l
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           FunType t1 _ t2 _ -> leaves b t1 `List.union` leaves b t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           _ -> error ("leaves: " ++ show t)
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | composition (reversed: first substitution first!)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercompSubst :: Subst -> Subst -> Subst
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercompSubst s1 s2 = Map.union (Map.map (subst s2) s1) s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | unifiability of type schemes including instantiation with fresh variables
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- (and looking up type aliases)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederisUnifiable :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederisUnifiable tm c = asSchemes c (unify tm)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | test if second scheme is a substitution instance
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinstScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinstScheme tm c = asSchemes c (subsume tm)
2ffa94a49389096aa73aaf93a8a5dc13ccb41ae0Christian Maeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | lift 'State' Int to 'State' Env
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoEnvState :: State Int a -> State Env a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoEnvState p =
2ffa94a49389096aa73aaf93a8a5dc13ccb41ae0Christian Maeder    do s <- get
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann       let (r, c) = runState p $ counter s
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann       put s { counter = c }
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann       return r
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmanntoSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertoSchemes f sc1 sc2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    do t1 <- freshInst sc1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder       t2 <- freshInst sc2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder       return $ f t1 t2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederasSchemes :: Int -> (Type -> Type -> a) -> TypeScheme -> TypeScheme -> a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederasSchemes c f sc1 sc2 = fst $ runState (toSchemes f sc1 sc2) c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- -------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfreshInst :: TypeScheme -> State Int Type
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederfreshInst (TypeScheme _ t _) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    do let ls = leaves (< 0) t -- generic vars
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           vs = map snd ls
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder       ts <- mkSubst vs
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann       return $ subst (Map.fromList $ zip (map fst ls) ts) t
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmanninc :: State Int Int
d024d9de9b6e7a7cfd72ef72d8efb0e57da5a01bChristian Maederinc = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    c <- get
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    put (c + 1)
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann    return c
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannfreshVar :: [Pos] -> State Int (Id, Int)
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannfreshVar ps = do
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann    c <- inc
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann    return (simpleIdToId $ Token ("_var_" ++ show c) ps, c)
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannmkSingleSubst :: (Id, RawKind) -> State Int Type
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannmkSingleSubst (i, rk) = do
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann    (ty, c) <- freshVar $ posOfId i
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann    return $ TypeName ty rk c
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannmkSubst :: [(Id, RawKind)] -> State Int [Type]
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannmkSubst = mapM mkSingleSubst
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmanntype Subst = Map.Map Int Type
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmanneps :: Subst
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmanneps = Map.empty
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederclass Unifiable a where
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann    subst :: Subst -> a -> a
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann    match :: TypeMap -> (TypeId -> TypeId -> Bool)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder          -> (Bool, a) -> (Bool, a) -> Result Subst
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | most general unifier via 'match'
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- where both sides may contribute substitutions
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannmgu :: Unifiable a => TypeMap -> a -> a -> Result Subst
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermgu tm a b = match tm (==) (True, a) (True, b)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel HausmannshapeMatch :: Unifiable a => TypeMap -> a -> a -> Result Subst
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedershapeMatch tm a b = match tm (const $ const True) (True, a) (True, b)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederunify :: Unifiable a => TypeMap -> a -> a -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederunify tm a b = isJust $ maybeResult $ mgu tm a b
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersubsume :: Unifiable a => TypeMap -> a -> a -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedersubsume tm a b =
    isJust $ maybeResult $ match tm (==) (False, a) (True, b)

equalSubs :: Unifiable a => TypeMap -> a -> a -> Bool
equalSubs tm a b = subsume tm a b && subsume tm b a

-- | get the type variable
getTypeVar :: TypeArg -> Id
getTypeVar(TypeArg v _ _ _) = v

idsOf :: (Int -> Bool) -> Type -> Set.Set TypeId
idsOf b = Set.fromList . map (fst . snd) . leaves b

instance Unifiable Type where
    subst m = rename (\ i k n ->
               case Map.lookup n m of
               Just s -> s
               _ -> TypeName i k n)
    match tm rel t1 (b2, ExpandedType _ t2) = match tm rel t1 (b2, t2)
    match tm rel (b1, ExpandedType _ t1) t2 = match tm rel (b1, t1) t2
    match tm rel t1 (b2, LazyType t2 _) = match tm rel t1 (b2, t2)
    match tm rel (b1, LazyType t1 _) t2 = match tm rel (b1, t1) t2
    match tm rel t1 (b2, KindedType t2 _ _) = match tm rel t1 (b2, t2)
    match tm rel (b1, KindedType t1 _ _) t2 = match tm rel (b1, t1) t2
    match _ rel (b1, t1@(TypeName i1 _k1 v1)) (b2, t2@(TypeName i2 _k2 v2)) =
        if rel i1 i2 && v1 == v2
           then return eps
        else if v1 > 0 && b1 then return $
                Map.singleton v1 t2
                else if v2 > 0 && b2 then return $
                     Map.singleton v2 t1
                        else uniResult "typename" t1
                                    "is not unifiable with typename" t2
    match _tm _ (b1, TypeName i1 _ v1) (_, t2) =
        if v1 > 0 && b1 then
           if null $ leaves (==v1) t2 then
              return $ Map.singleton v1 t2
           else uniResult "var" i1 "occurs in" t2
        else uniResult "typename" i1
                            "is not unifiable with type" t2
    match tm rel t2 t1@(_, TypeName _ _ _) = match tm rel t1 t2
    match tm rel (b1, TypeAppl t1 t2) (b2, TypeAppl t3 t4) =
        match tm rel (b1, (t1, t2)) (b2, (t3, t4))
    match tm rel (b1, ProductType p1 _) (b2, ProductType p2 _) =
        match tm rel (b1, p1) (b2, p2)
    match tm rel (b1, FunType t1 _ t2 _) (b2, FunType t3 _ t4 _) =
        match tm rel (b1, (t1, t2)) (b2, (t3, t4))
    match _ _ (_,t1) (_,t2) = uniResult "type" t1
                            "is not unifiable with type" t2

showPrettyWithPos :: (PrettyPrint a, PosItem a) => a -> ShowS
showPrettyWithPos a =  let p = get_pos a in
        showChar '\'' . showPretty a . showChar '\''
           . noShow (null p) (showChar ' ' .
               showParen True (showPos $ maximumBy comparePos p))

uniResult :: (PrettyPrint a, PosItem a, PrettyPrint b, PosItem b) =>
              String -> a -> String -> b -> Result Subst
uniResult s1 a s2 b =
      Result [Diag Hint ("in type\n" ++ "  " ++ s1 ++ " " ++
                         showPrettyWithPos a "\n  " ++ s2 ++ " " ++
                         showPrettyWithPos b "") []] Nothing

instance (Unifiable a, Unifiable b) => Unifiable (a, b) where
    subst s (t1, t2) = (subst s t1, subst s t2)
    match tm rel (b1, (t1, t2)) (b2, (t3, t4)) =
        let r1@(Result _ m1) = match tm rel (b1, t1) (b2, t3) in
           case m1 of
               Nothing -> r1
               Just s1 -> let r2@(Result _ m2) = match tm rel
                                   (b1, if b1 then subst s1 t2 else t2)
                                   (b2, if b2 then subst s1 t4 else t4)
                              in case m2 of
                                     Nothing -> r2
                                     Just s2 -> return $ compSubst s1 s2

instance (PrettyPrint a, PosItem a, Unifiable a) => Unifiable [a] where
    subst s = map (subst s)
    match _ _ (_, []) (_, []) = return eps
    match tm rel (b1, a1:r1) (b2, a2:r2) =
        match tm rel (b1, (a1, r1)) (b2, (a2, r2))
    match tm rel (b1, []) l = match tm rel l (b1, [])
    match _ _ (_, (a:_)) (_, []) = uniResult "type component" a
                       "is not unifiable with the empty list"
                       (mkSimpleId "[]")

instance (PrettyPrint a, PosItem a, Unifiable a) => Unifiable (Maybe a) where
    subst s = fmap (subst s)
    match _ _ (_, Nothing) _ = return eps
    match _ _ _ (_, Nothing) = return eps
    match tm rel (b1, Just a1) (b2, Just a2) = match tm rel (b1, a1) (b2, a2)

repl :: Map.Map Id Type -> Type -> Type
repl m = rename ( \ i k n ->
                 case Map.lookup i m of
                      Just s -> s
                      Nothing -> TypeName i k n)

expand :: TypeMap -> TypeScheme -> TypeScheme
expand = mapTypeOfScheme . expandAlias

expandAlias :: TypeMap -> Type -> Type
expandAlias tm t =
    let (ps, as, ta, b) = expandAliases tm t in
       if b && length ps == length as then
          ExpandedType t $ repl (Map.fromList (zip
                             (map getTypeVar ps) $ reverse as)) ta
          else ta

expandAliases :: TypeMap -> Type -> ([TypeArg], [Type], Type, Bool)
expandAliases tm t = case t of
    TypeName i _ _ -> case Map.lookup i tm of
            Just (TypeInfo _ _ _
                  (AliasTypeDefn (TypeScheme l ty _))) ->
                     (l, [], ty, True)
            Just (TypeInfo _ _ _
                  (Supertype _ (TypeScheme l ty _) _)) ->
                     case ty of
                     TypeName _ _ _ -> wrap t
                     _ -> (l, [], ty, True)
            _ -> wrap t
    TypeAppl t1 t2 ->
        let (ps, as, ta, b) = expandAliases tm t1
            t3 = expandAlias tm t2
        in if b then
          (ps, t3:as, ta, b)  -- reverse later on
          else wrap $ TypeAppl t1 t3
    FunType t1 a t2 ps ->
        wrap $ FunType (expandAlias tm t1) a (expandAlias tm t2) ps
    ProductType ts ps -> wrap $ ProductType (map (expandAlias tm) ts) ps
    LazyType ty ps -> wrap $ LazyType (expandAlias tm ty) ps
    ExpandedType t1 t2 -> wrap $ ExpandedType t1 $ expandAlias tm t2
    KindedType ty k ps -> wrap $ KindedType (expandAlias tm ty) k ps
    _ -> wrap t
    where wrap ty = ([], [], ty, False)