Unify.hs

{- |
Module      :  ./HasCASL/Unify.hs
Description :  generalized unification of types
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

substitution and unification of types
-}

module HasCASL.Unify where

import HasCASL.As
import HasCASL.FoldType
import HasCASL.AsUtils
import HasCASL.PrintAs ()
import HasCASL.ClassAna
import HasCASL.TypeAna
import HasCASL.Le

import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.DocUtils
import Common.Id
import Common.Lib.State
import Common.Result
import qualified Control.Monad.Fail as Fail

import Data.List as List
import Data.Maybe

-- | composition (reversed: first substitution first!)
compSubst :: Subst -> Subst -> Subst
compSubst s1 s2 = Map.union (Map.map (subst s2) s1) s2

-- | test if second scheme is a substitution instance
instScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Bool
instScheme tm c = asSchemes c (subsume tm)

specializedScheme :: ClassMap -> [TypeArg] -> [TypeArg] -> Bool
specializedScheme cm args1 args2 = length args1 == length args2 && and
    (zipWith (\ (TypeArg _ v1 vk1 _ _ _ _) (TypeArg _ v2 vk2 _ _ _ _) ->
        (v1 == v2 || v1 == NonVar) && case (vk1, vk2) of
          (VarKind k1, VarKind k2) -> lesserKind cm k1 k2
          _ -> vk1 == vk2) args1 args2)

-- | lift 'State' Int to 'State' Env
toEnvState :: State Int a -> State Env a
toEnvState p = do
    s <- get
    let (r, c) = runState p $ counter s
    put s { counter = c }
    return r

toSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a
toSchemes f sc1 sc2 = do
    (t1, _) <- freshInst sc1
    (t2, _) <- freshInst sc2
    return $ f t1 t2

asSchemes :: Int -> (Type -> Type -> a) -> TypeScheme -> TypeScheme -> a
asSchemes c f sc1 sc2 = evalState (toSchemes f sc1 sc2) c

substTypeArg :: Subst -> TypeArg -> VarKind
substTypeArg s (TypeArg _ _ vk _ _ _ _) = case vk of
    Downset super -> Downset $ substGen s super
    _ -> vk

mapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)]
mapArgs s ts = foldr ( \ ta l ->
    maybe l ( \ (_, t) -> (t, substTypeArg s ta) : l) $
            find ( \ (j, _) -> getTypeVar ta == j) ts) []

freshInst :: TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst (TypeScheme tArgs t _) = do
    let ls = leaves (< 0) t -- generic vars
        vs = map snd ls
    ts <- mkSubst vs
    let s = Map.fromList $ zip (map fst ls) ts
    return (substGen s t, mapArgs s (zip (map fst vs) ts) tArgs)

inc :: State Int Int
inc = do
    c <- get
    put (c + 1)
    return c

freshVar :: Id -> State Int (Id, Int)
freshVar i@(Id ts _ _) = do
    c <- inc
    return (Id [mkSimpleId $ "_v" ++ show c ++ case ts of
                  [t] -> '_' : dropWhile (== '_') (tokStr t)
                  _ -> ""] [] $ posOfId i, c)

mkSingleSubst :: (Id, RawKind) -> State Int Type
mkSingleSubst (i, rk) = do
    (ty, c) <- freshVar i
    return $ TypeName ty rk c

mkSubst :: [(Id, RawKind)] -> State Int [Type]
mkSubst = mapM mkSingleSubst

type Subst = Map.Map Int Type

eps :: Subst
eps = Map.empty

flatKind :: Type -> RawKind
flatKind = nonVarRawKind . rawKindOfType

noAbs :: Type -> Bool
noAbs t = case t of
    TypeAbs {} -> False
    _ -> True

match :: TypeMap -> (Id -> Id -> Bool)
      -> (Bool, Type) -> (Bool, Type) -> Result Subst
match tm rel p1@(b1, ty1) p2@(b2, ty2) =
  if flatKind ty1 == flatKind ty2 then case (ty1, ty2) of
    (_, ExpandedType _ t2) | noAbs t2 -> match tm rel p1 (b2, t2)
    (ExpandedType _ t1, _) | noAbs t1 -> match tm rel (b1, t1) p2
    (_, TypeAppl (TypeName l _ _) t2) | l == lazyTypeId ->
              match tm rel p1 (b2, t2)
    (TypeAppl (TypeName l _ _) t1, _) | l == lazyTypeId ->
              match tm rel (b1, t1) p2
    (_, KindedType t2 _ _) -> match tm rel p1 (b2, t2)
    (KindedType t1 _ _, _) -> match tm rel (b1, t1) p2
    (TypeName i1 _k1 v1, TypeName i2 _k2 v2)
     | rel i1 i2 && v1 == v2 -> return eps
     | v1 > 0 && b1 -> return $ Map.singleton v1 ty2
     | v2 > 0 && b2 -> return $ Map.singleton v2 ty1
{- the following two conditions only guarantee that instScheme also matches for
   a partial function that is mapped to a total one.
   Maybe a subtype condition is better. -}
     | not b1 && b2 && v1 == 0 && v2 == 0 && Set.member i1 (superIds tm i2) ||
       b1 && not b2 && v1 == 0 && v2 == 0 && Set.member i2 (superIds tm i1)
                 -> return eps
     | otherwise -> uniResult "typename" ty1
                     "is not unifiable with typename" ty2
    (TypeName _ _ v1, _) -> case redStep ty2 of
      Just ry2 -> match tm rel p1 (b2, ry2)
      Nothing ->
        if v1 > 0 && b1 then
           if null $ leaves (== v1) ty2 then
              return $ Map.singleton v1 ty2
           else uniResult "var" ty1 "occurs in" ty2
        else uniResult "typename" ty1
                            "is not unifiable with type" ty2
    (_, TypeName {}) -> match tm rel p2 p1
    (TypeAppl f1 a1, TypeAppl f2 a2) -> case redStep ty1 of
       Just ry1 -> match tm rel (b1, ry1) p2
       Nothing -> case redStep ty2 of
         Just ry2 -> match tm rel p1 (b2, ry2)
         Nothing -> do
            s1 <- match tm rel (b1, f1) (b2, f2)
            s2 <- match tm rel (b1, if b1 then subst s1 a1 else a1)
                   (b2, if b2 then subst s1 a2 else a2)
            return $ compSubst s1 s2
    _ -> if ty1 == ty2 then return eps else
             uniResult "type" ty1 "is not unifiable with type" ty2
  else uniResult "type" ty1 "is not unifiable with differently kinded type" ty2

shapeMatch :: TypeMap -> Type -> Type -> Result Subst
shapeMatch tm a b = match tm (const $ const True) (True, a) (True, b)

subsume :: TypeMap -> Type -> Type -> Bool
subsume tm a b =
    isJust $ maybeResult $ match tm (==) (False, a) (True, b)

-- | substitute generic variables with negative index
substGen :: Subst -> Type -> Type
substGen m = foldType mapTypeRec
  { foldTypeName = \ t _ _ n -> if n >= 0 then t
     else Data.Maybe.fromMaybe t (Map.lookup n m)
  , foldTypeAbs = \ t v1@(TypeArg _ _ _ _ c _ _) ty p ->
      if Map.member c m then substGen (Map.delete c m) t else TypeAbs v1 ty p }

getTypeOf :: Fail.MonadFail m => Term -> m Type
getTypeOf trm = case trm of
    TypedTerm _ q t _ -> return $ case q of
        InType -> unitType
        _ -> t
    QualVar (VarDecl _ t _ _) -> return t
    QualOp _ _ (TypeScheme _ t _) is _ _ -> return $
        substGen (Map.fromList $ zip [-1, -2 ..] is) t
    TupleTerm ts ps -> if null ts then return unitType else do
        tys <- mapM getTypeOf ts
        return $ mkProductTypeWithRange tys ps
    QuantifiedTerm _ _ t _ -> getTypeOf t
    LetTerm _ _ t _ -> getTypeOf t
    AsPattern _ p _ -> getTypeOf p
    _ -> Fail.fail $ "getTypeOf: " ++ showDoc trm ""

-- | substitute variables with positive index
subst :: Subst -> Type -> Type
subst m = if Map.null m then id else foldType mapTypeRec
  { foldTypeName = \ t _ _ n -> if n <= 0 then t
     else Data.Maybe.fromMaybe t (Map.lookup n m) }

showDocWithPos :: Type -> ShowS
showDocWithPos a = let p = getRange a in
    showChar '\'' . showDoc a . showChar '\''
    . noShow (isNullRange p) (showChar ' ' .
        showParen True (showPos $ maximum (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