{- |
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 :: Subst -> Subst -> Subst
compSubst s1 :: Subst
s1 s2 :: Subst
s2 = Subst -> Subst -> Subst
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ((Type -> Type) -> Subst -> Subst
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Subst -> Type -> Type
subst Subst
s2) Subst
s1) Subst
s2

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

specializedScheme :: ClassMap -> [TypeArg] -> [TypeArg] -> Bool
specializedScheme :: ClassMap -> [TypeArg] -> [TypeArg] -> Bool
specializedScheme cm :: ClassMap
cm args1 :: [TypeArg]
args1 args2 :: [TypeArg]
args2 = [TypeArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg]
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg]
args2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
    ((TypeArg -> TypeArg -> Bool) -> [TypeArg] -> [TypeArg] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ (TypeArg _ v1 :: Variance
v1 vk1 :: VarKind
vk1 _ _ _ _) (TypeArg _ v2 :: Variance
v2 vk2 :: VarKind
vk2 _ _ _ _) ->
        (Variance
v1 Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
v2 Bool -> Bool -> Bool
|| Variance
v1 Variance -> Variance -> Bool
forall a. Eq a => a -> a -> Bool
== Variance
NonVar) Bool -> Bool -> Bool
&& case (VarKind
vk1, VarKind
vk2) of
          (VarKind k1 :: Kind
k1, VarKind k2 :: Kind
k2) -> ClassMap -> Kind -> Kind -> Bool
lesserKind ClassMap
cm Kind
k1 Kind
k2
          _ -> VarKind
vk1 VarKind -> VarKind -> Bool
forall a. Eq a => a -> a -> Bool
== VarKind
vk2) [TypeArg]
args1 [TypeArg]
args2)

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

toSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a
toSchemes :: (Type -> Type -> a) -> TypeScheme -> TypeScheme -> State Int a
toSchemes f :: Type -> Type -> a
f sc1 :: TypeScheme
sc1 sc2 :: TypeScheme
sc2 = do
    (t1 :: Type
t1, _) <- TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst TypeScheme
sc1
    (t2 :: Type
t2, _) <- TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst TypeScheme
sc2
    a -> State Int a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> State Int a) -> a -> State Int a
forall a b. (a -> b) -> a -> b
$ Type -> Type -> a
f Type
t1 Type
t2

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

substTypeArg :: Subst -> TypeArg -> VarKind
substTypeArg :: Subst -> TypeArg -> VarKind
substTypeArg s :: Subst
s (TypeArg _ _ vk :: VarKind
vk _ _ _ _) = case VarKind
vk of
    Downset super :: Type
super -> Type -> VarKind
Downset (Type -> VarKind) -> Type -> VarKind
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
substGen Subst
s Type
super
    _ -> VarKind
vk

mapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)]
mapArgs :: Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)]
mapArgs s :: Subst
s ts :: [(Id, Type)]
ts = (TypeArg -> [(Type, VarKind)] -> [(Type, VarKind)])
-> [(Type, VarKind)] -> [TypeArg] -> [(Type, VarKind)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ ta :: TypeArg
ta l :: [(Type, VarKind)]
l ->
    [(Type, VarKind)]
-> ((Id, Type) -> [(Type, VarKind)])
-> Maybe (Id, Type)
-> [(Type, VarKind)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(Type, VarKind)]
l ( \ (_, t :: Type
t) -> (Type
t, Subst -> TypeArg -> VarKind
substTypeArg Subst
s TypeArg
ta) (Type, VarKind) -> [(Type, VarKind)] -> [(Type, VarKind)]
forall a. a -> [a] -> [a]
: [(Type, VarKind)]
l) (Maybe (Id, Type) -> [(Type, VarKind)])
-> Maybe (Id, Type) -> [(Type, VarKind)]
forall a b. (a -> b) -> a -> b
$
            ((Id, Type) -> Bool) -> [(Id, Type)] -> Maybe (Id, Type)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ( \ (j :: Id
j, _) -> TypeArg -> Id
getTypeVar TypeArg
ta Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j) [(Id, Type)]
ts) []

freshInst :: TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst :: TypeScheme -> State Int (Type, [(Type, VarKind)])
freshInst (TypeScheme tArgs :: [TypeArg]
tArgs t :: Type
t _) = do
    let ls :: [(Int, (Id, RawKind))]
ls = (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0) Type
t -- generic vars
        vs :: [(Id, RawKind)]
vs = ((Int, (Id, RawKind)) -> (Id, RawKind))
-> [(Int, (Id, RawKind))] -> [(Id, RawKind)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Id, RawKind)) -> (Id, RawKind)
forall a b. (a, b) -> b
snd [(Int, (Id, RawKind))]
ls
    [Type]
ts <- [(Id, RawKind)] -> State Int [Type]
mkSubst [(Id, RawKind)]
vs
    let s :: Subst
s = [(Int, Type)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Int, (Id, RawKind)) -> Int) -> [(Int, (Id, RawKind))] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Id, RawKind)) -> Int
forall a b. (a, b) -> a
fst [(Int, (Id, RawKind))]
ls) [Type]
ts
    (Type, [(Type, VarKind)]) -> State Int (Type, [(Type, VarKind)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Type -> Type
substGen Subst
s Type
t, Subst -> [(Id, Type)] -> [TypeArg] -> [(Type, VarKind)]
mapArgs Subst
s ([Id] -> [Type] -> [(Id, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Id, RawKind) -> Id) -> [(Id, RawKind)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, RawKind) -> Id
forall a b. (a, b) -> a
fst [(Id, RawKind)]
vs) [Type]
ts) [TypeArg]
tArgs)

inc :: State Int Int
inc :: State Int Int
inc = do
    Int
c <- State Int Int
forall s. State s s
get
    Int -> State Int ()
forall s. s -> State s ()
put (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
    Int -> State Int Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
c

freshVar :: Id -> State Int (Id, Int)
freshVar :: Id -> State Int (Id, Int)
freshVar i :: Id
i@(Id ts :: [Token]
ts _ _) = do
    Int
c <- State Int Int
inc
    (Id, Int) -> State Int (Id, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> [Id] -> Range -> Id
Id [String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ "_v" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ case [Token]
ts of
                  [t :: Token
t] -> '_' Char -> String -> String
forall a. a -> [a] -> [a]
: (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '_') (Token -> String
tokStr Token
t)
                  _ -> ""] [] (Range -> Id) -> Range -> Id
forall a b. (a -> b) -> a -> b
$ Id -> Range
posOfId Id
i, Int
c)

mkSingleSubst :: (Id, RawKind) -> State Int Type
mkSingleSubst :: (Id, RawKind) -> State Int Type
mkSingleSubst (i :: Id
i, rk :: RawKind
rk) = do
    (ty :: Id
ty, c :: Int
c) <- Id -> State Int (Id, Int)
freshVar Id
i
    Type -> State Int Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> State Int Type) -> Type -> State Int Type
forall a b. (a -> b) -> a -> b
$ Id -> RawKind -> Int -> Type
TypeName Id
ty RawKind
rk Int
c

mkSubst :: [(Id, RawKind)] -> State Int [Type]
mkSubst :: [(Id, RawKind)] -> State Int [Type]
mkSubst = ((Id, RawKind) -> State Int Type)
-> [(Id, RawKind)] -> State Int [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Id, RawKind) -> State Int Type
mkSingleSubst

type Subst = Map.Map Int Type

eps :: Subst
eps :: Subst
eps = Subst
forall k a. Map k a
Map.empty

flatKind :: Type -> RawKind
flatKind :: Type -> RawKind
flatKind = RawKind -> RawKind
nonVarRawKind (RawKind -> RawKind) -> (Type -> RawKind) -> Type -> RawKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RawKind
rawKindOfType

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

match :: TypeMap -> (Id -> Id -> Bool)
      -> (Bool, Type) -> (Bool, Type) -> Result Subst
match :: TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match tm :: TypeMap
tm rel :: Id -> Id -> Bool
rel p1 :: (Bool, Type)
p1@(b1 :: Bool
b1, ty1 :: Type
ty1) p2 :: (Bool, Type)
p2@(b2 :: Bool
b2, ty2 :: Type
ty2) =
  if Type -> RawKind
flatKind Type
ty1 RawKind -> RawKind -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> RawKind
flatKind Type
ty2 then case (Type
ty1, Type
ty2) of
    (_, ExpandedType _ t2 :: Type
t2) | Type -> Bool
noAbs Type
t2 -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool, Type)
p1 (Bool
b2, Type
t2)
    (ExpandedType _ t1 :: Type
t1, _) | Type -> Bool
noAbs Type
t1 -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool
b1, Type
t1) (Bool, Type)
p2
    (_, TypeAppl (TypeName l :: Id
l _ _) t2 :: Type
t2) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
              TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool, Type)
p1 (Bool
b2, Type
t2)
    (TypeAppl (TypeName l :: Id
l _ _) t1 :: Type
t1, _) | Id
l Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId ->
              TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool
b1, Type
t1) (Bool, Type)
p2
    (_, KindedType t2 :: Type
t2 _ _) -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool, Type)
p1 (Bool
b2, Type
t2)
    (KindedType t1 :: Type
t1 _ _, _) -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool
b1, Type
t1) (Bool, Type)
p2
    (TypeName i1 :: Id
i1 _k1 :: RawKind
_k1 v1 :: Int
v1, TypeName i2 :: Id
i2 _k2 :: RawKind
_k2 v2 :: Int
v2)
     | Id -> Id -> Bool
rel Id
i1 Id
i2 Bool -> Bool -> Bool
&& Int
v1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v2 -> Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
eps
     | Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& Bool
b1 -> Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
v1 Type
ty2
     | Int
v2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& Bool
b2 -> Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
v2 Type
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. -}
     | Bool -> Bool
not Bool
b1 Bool -> Bool -> Bool
&& Bool
b2 Bool -> Bool -> Bool
&& Int
v1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& Int
v2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i1 (TypeMap -> Id -> Set Id
superIds TypeMap
tm Id
i2) Bool -> Bool -> Bool
||
       Bool
b1 Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
b2 Bool -> Bool -> Bool
&& Int
v1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& Int
v2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 Bool -> Bool -> Bool
&& Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
i2 (TypeMap -> Id -> Set Id
superIds TypeMap
tm Id
i1)
                 -> Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
eps
     | Bool
otherwise -> String -> Type -> String -> Type -> Result Subst
uniResult "typename" Type
ty1
                     "is not unifiable with typename" Type
ty2
    (TypeName _ _ v1 :: Int
v1, _) -> case Type -> Maybe Type
redStep Type
ty2 of
      Just ry2 :: Type
ry2 -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool, Type)
p1 (Bool
b2, Type
ry2)
      Nothing ->
        if Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
&& Bool
b1 then
           if [(Int, (Id, RawKind))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Int, (Id, RawKind))] -> Bool) -> [(Int, (Id, RawKind))] -> Bool
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> Type -> [(Int, (Id, RawKind))]
leaves (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v1) Type
ty2 then
              Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Subst
forall k a. k -> a -> Map k a
Map.singleton Int
v1 Type
ty2
           else String -> Type -> String -> Type -> Result Subst
uniResult "var" Type
ty1 "occurs in" Type
ty2
        else String -> Type -> String -> Type -> Result Subst
uniResult "typename" Type
ty1
                            "is not unifiable with type" Type
ty2
    (_, TypeName {}) -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool, Type)
p2 (Bool, Type)
p1
    (TypeAppl f1 :: Type
f1 a1 :: Type
a1, TypeAppl f2 :: Type
f2 a2 :: Type
a2) -> case Type -> Maybe Type
redStep Type
ty1 of
       Just ry1 :: Type
ry1 -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool
b1, Type
ry1) (Bool, Type)
p2
       Nothing -> case Type -> Maybe Type
redStep Type
ty2 of
         Just ry2 :: Type
ry2 -> TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool, Type)
p1 (Bool
b2, Type
ry2)
         Nothing -> do
            Subst
s1 <- TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool
b1, Type
f1) (Bool
b2, Type
f2)
            Subst
s2 <- TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
rel (Bool
b1, if Bool
b1 then Subst -> Type -> Type
subst Subst
s1 Type
a1 else Type
a1)
                   (Bool
b2, if Bool
b2 then Subst -> Type -> Type
subst Subst
s1 Type
a2 else Type
a2)
            Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Result Subst) -> Subst -> Result Subst
forall a b. (a -> b) -> a -> b
$ Subst -> Subst -> Subst
compSubst Subst
s1 Subst
s2
    _ -> if Type
ty1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty2 then Subst -> Result Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
eps else
             String -> Type -> String -> Type -> Result Subst
uniResult "type" Type
ty1 "is not unifiable with type" Type
ty2
  else String -> Type -> String -> Type -> Result Subst
uniResult "type" Type
ty1 "is not unifiable with differently kinded type" Type
ty2

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

subsume :: TypeMap -> Type -> Type -> Bool
subsume :: TypeMap -> Type -> Type -> Bool
subsume tm :: TypeMap
tm a :: Type
a b :: Type
b =
    Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ Result Subst -> Maybe Subst
forall a. Result a -> Maybe a
maybeResult (Result Subst -> Maybe Subst) -> Result Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ TypeMap
-> (Id -> Id -> Bool)
-> (Bool, Type)
-> (Bool, Type)
-> Result Subst
match TypeMap
tm Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Bool
False, Type
a) (Bool
True, Type
b)

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

getTypeOf :: Fail.MonadFail m => Term -> m Type
getTypeOf :: Term -> m Type
getTypeOf trm :: Term
trm = case Term
trm of
    TypedTerm _ q :: TypeQual
q t :: Type
t _ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ case TypeQual
q of
        InType -> Type
unitType
        _ -> Type
t
    QualVar (VarDecl _ t :: Type
t _ _) -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    QualOp _ _ (TypeScheme _ t :: Type
t _) is :: [Type]
is _ _ -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$
        Subst -> Type -> Type
substGen ([(Int, Type)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [-1, -2 ..] [Type]
is) Type
t
    TupleTerm ts :: [Term]
ts ps :: Range
ps -> if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts then Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
unitType else do
        [Type]
tys <- (Term -> m Type) -> [Term] -> m [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> m Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf [Term]
ts
        Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Range -> Type
mkProductTypeWithRange [Type]
tys Range
ps
    QuantifiedTerm _ _ t :: Term
t _ -> Term -> m Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
t
    LetTerm _ _ t :: Term
t _ -> Term -> m Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
t
    AsPattern _ p :: Term
p _ -> Term -> m Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
p
    _ -> String -> m Type
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m Type) -> String -> m Type
forall a b. (a -> b) -> a -> b
$ "getTypeOf: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Term
trm ""

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

showDocWithPos :: Type -> ShowS
showDocWithPos :: Type -> String -> String
showDocWithPos a :: Type
a = let p :: Range
p = Type -> Range
forall a. GetRange a => a -> Range
getRange Type
a in
    Char -> String -> String
showChar '\'' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Type
a (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar '\''
    (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> (String -> String) -> String -> String
noShow (Range -> Bool
isNullRange Range
p) (Char -> String -> String
showChar ' ' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        Bool -> (String -> String) -> String -> String
showParen Bool
True (Pos -> String -> String
showPos (Pos -> String -> String) -> Pos -> String -> String
forall a b. (a -> b) -> a -> b
$ [Pos] -> Pos
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Range -> [Pos]
rangeToList Range
p)))

uniResult :: String -> Type -> String -> Type -> Result Subst
uniResult :: String -> Type -> String -> Type -> Result Subst
uniResult s1 :: String
s1 a :: Type
a s2 :: String
s2 b :: Type
b = [Diagnosis] -> Maybe Subst -> Result Subst
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Hint ("in type\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ "  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++
    Type -> String -> String
showDocWithPos Type
a "\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++
    Type -> String -> String
showDocWithPos Type
b "") Range
nullRange] Maybe Subst
forall a. Maybe a
Nothing

-- | make representation of bound variables unique
generalize :: [TypeArg] -> Type -> Type
generalize :: [TypeArg] -> Type -> Type
generalize tArgs :: [TypeArg]
tArgs = Subst -> Type -> Type
subst (Subst -> Type -> Type) -> Subst -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [(Int, Type)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Type)] -> Subst) -> [(Int, Type)] -> Subst
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Int -> (Int, Type))
-> [TypeArg] -> [Int] -> [(Int, Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
    ( \ (TypeArg i :: Id
i _ _ rk :: RawKind
rk c :: Int
c _ _) n :: Int
n -> (Int
c, Id -> RawKind -> Int -> Type
TypeName Id
i RawKind
rk Int
n)) [TypeArg]
tArgs [-1, -2 ..]

genTypeArgs :: [TypeArg] -> [TypeArg]
genTypeArgs :: [TypeArg] -> [TypeArg]
genTypeArgs tArgs :: [TypeArg]
tArgs = (Int, [TypeArg]) -> [TypeArg]
forall a b. (a, b) -> b
snd ((Int, [TypeArg]) -> [TypeArg]) -> (Int, [TypeArg]) -> [TypeArg]
forall a b. (a -> b) -> a -> b
$ (Int -> TypeArg -> (Int, TypeArg))
-> Int -> [TypeArg] -> (Int, [TypeArg])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL ( \ n :: Int
n (TypeArg i :: Id
i v :: Variance
v vk :: VarKind
vk rk :: RawKind
rk _ s :: SeparatorKind
s ps :: Range
ps) ->
    (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1, Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v (case VarKind
vk of
      Downset t :: Type
t -> Type -> VarKind
Downset (Type -> VarKind) -> Type -> VarKind
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Type
generalize [TypeArg]
tArgs Type
t
      _ -> VarKind
vk) RawKind
rk Int
n SeparatorKind
s Range
ps)) (-1) [TypeArg]
tArgs