\begin{code}
{-# OPTIONS -cpp -funbox-strict-fields #-}
module MagicHaskeller.Types(Type(..), Kind, TyCon, TyVar, TypeName, Typed(..), tyvars, Subst, plusSubst,
emptySubst, apply, mgu, varBind, match, maxVarID, normalizeVarIDs, normalize, unChin,
Decoder(..), typer, typee, negateTVIDs, limitType, saferQuantify, quantify, quantify', unquantify, lookupSubst, unifyFunAp,
alltyvars, mapTV, size, unitSubst, applyCheck, assertsubst, substOK, eqType, getRet, getArity, getArities, getAritiesRet, splitArgs, getArgs, pushArgs, popArgs, mguFunAp, revSplitArgs, revGetArgs, module Data.Int
) where
import Data.List
import Control.Monad
import Data.Char(ord)
#ifdef QUICKCHECK
import Test.QuickCheck
#endif
import Data.Int
infixr :->, :>
trace :: p -> a -> a
trace p
_ = a -> a
forall a. a -> a
id
data Type = TV {-# UNPACK #-} !TyVar | TC {-# UNPACK #-} !TyCon | TA Type Type | Type :> Type | Type :-> Type | Type :=> Type
deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord, ReadPrec [Type]
ReadPrec Type
Int -> ReadS Type
ReadS [Type]
(Int -> ReadS Type)
-> ReadS [Type] -> ReadPrec Type -> ReadPrec [Type] -> Read Type
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Type]
$creadListPrec :: ReadPrec [Type]
readPrec :: ReadPrec Type
$creadPrec :: ReadPrec Type
readList :: ReadS [Type]
$creadList :: ReadS [Type]
readsPrec :: Int -> ReadS Type
$creadsPrec :: Int -> ReadS Type
Read)
size :: Type -> Int
size :: Type -> Int
size (TC TyCon
_) = Int
1
size (TV TyCon
_) = Int
1
size (TA Type
t0 Type
t1) = Type -> Int
size Type
t0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
size Type
t1
size (Type
t0 :> Type
t1) = Type -> Int
size Type
t0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
size Type
t1
size (Type
t0 :-> Type
t1) = Type -> Int
size Type
t0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
size Type
t1
#ifdef QUICKCHECK
instance Arbitrary Type where
arbitrary = sized arbType
arbType 0 = oneof [liftM TV arbitrary, liftM TC arbitrary]
arbType n = frequency [ (8, arbType 0),
(2, liftM2 TA (arbType (n `div` 2)) (arbType (n `div` 2))),
(2, liftM2 (:->) (arbType (n `div` 2)) (arbType (n `div` 2))) ]
#endif
mapTV :: (TyVar -> TyVar) -> Type -> Type
mapTV :: (TyCon -> TyCon) -> Type -> Type
mapTV TyCon -> TyCon
f Type
t =
Type -> Type
mtv Type
t
where mtv :: Type -> Type
mtv (TA Type
t0 Type
t1) = Type -> Type -> Type
TA (Type -> Type
mtv Type
t0) (Type -> Type
mtv Type
t1)
mtv (Type
t1 :=> Type
t0) = (Type -> Type
mtv Type
t1) Type -> Type -> Type
:=> (Type -> Type
mtv Type
t0)
mtv (Type
t1 :-> Type
t0) = (Type -> Type
mtv Type
t1) Type -> Type -> Type
:-> (Type -> Type
mtv Type
t0)
mtv (Type
t1 :> Type
t0) = (Type -> Type
mtv Type
t1) Type -> Type -> Type
:> (Type -> Type
mtv Type
t0)
mtv (TV TyCon
tv) = TyCon -> Type
TV (TyCon -> TyCon
f TyCon
tv)
mtv tc :: Type
tc@(TC TyCon
_) = Type
tc
negateTVIDs :: Type -> Type
negateTVIDs :: Type -> Type
negateTVIDs = (TyCon -> TyCon) -> Type -> Type
mapTV (\TyCon
tvid -> -TyCon
1 TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
- TyCon
tvid)
limitType :: a -> Type -> a
limitType a
n (TC TyCon
_) = a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1
limitType a
n (TV TyCon
_) = a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1
limitType a
n (Type
u :-> Type
t) = a -> Type -> Type -> a
lt a
n Type
t Type
u
limitType a
n (Type
u :> Type
t) = a -> Type -> Type -> a
lt a
n Type
t Type
u
limitType a
n (TA Type
t Type
u) = a -> Type -> Type -> a
lt a
n Type
t Type
u
lt :: a -> Type -> Type -> a
lt a
n Type
t Type
u = case a -> Type -> a
limitType a
n Type
t of a
m | a
m a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 -> a -> Type -> a
limitType a
m Type
u
| Bool
otherwise -> -a
1
alltyvars :: Type -> Subst -> [TyVar]
alltyvars :: Type -> Subst -> [TyCon]
alltyvars Type
ty Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
ty Subst
s []
alltyvars' :: Type -> Subst -> [TyVar] -> [TyVar]
alltyvars' :: Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' (TV TyCon
tv) Subst
s = case Subst -> TyCon -> Maybe Type
forall (m :: * -> *). MonadPlus m => Subst -> TyCon -> m Type
lookupSubst Subst
s TyCon
tv of Just Type
t -> Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s
Maybe Type
Nothing -> (TyCon
tvTyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
:)
alltyvars' (TC TyCon
tc) Subst
s = [TyCon] -> [TyCon]
forall a. a -> a
id
alltyvars' (TA Type
t Type
u) Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
u Subst
s
alltyvars' (Type
u :> Type
t) Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
u Subst
s
alltyvars' (Type
u :-> Type
t) Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
u Subst
s
alltyvars' (Type
u :=> Type
t) Subst
s = Type -> Subst -> [TyCon] -> [TyCon]
alltyvars' Type
t Subst
s
{-# INLINE tyvars #-}
{-# INLINE tyvars' #-}
tyvars :: Type -> [TyVar]
tyvars :: Type -> [TyCon]
tyvars Type
ty = Type -> [TyCon] -> [TyCon]
tyvars' Type
ty []
tyvars' :: Type -> [TyVar] -> [TyVar]
tyvars' :: Type -> [TyCon] -> [TyCon]
tyvars' (TV TyCon
tv) = (TyCon
tvTyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
:)
tyvars' (TC TyCon
tc) = [TyCon] -> [TyCon]
forall a. a -> a
id
tyvars' (TA Type
t Type
u) = Type -> [TyCon] -> [TyCon]
tyvars' Type
t ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCon] -> [TyCon]
tyvars' Type
u
tyvars' (Type
u :> Type
t) = Type -> [TyCon] -> [TyCon]
tyvars' Type
t ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCon] -> [TyCon]
tyvars' Type
u
tyvars' (Type
u :-> Type
t) = Type -> [TyCon] -> [TyCon]
tyvars' Type
t ([TyCon] -> [TyCon]) -> ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCon] -> [TyCon]
tyvars' Type
u
tyvars' (Type
u :=> Type
t) = Type -> [TyCon] -> [TyCon]
tyvars' Type
t
maxVarID :: Type -> TyVar
maxVarID :: Type -> TyCon
maxVarID (TV TyCon
tv) = TyCon
tv
maxVarID (TC TyCon
_) = -TyCon
1
maxVarID (TA Type
t Type
u) = Type -> TyCon
maxVarID Type
t TyCon -> TyCon -> TyCon
forall a. Ord a => a -> a -> a
`max` Type -> TyCon
maxVarID Type
u
maxVarID (Type
t :> Type
u) = Type -> TyCon
maxVarID Type
t TyCon -> TyCon -> TyCon
forall a. Ord a => a -> a -> a
`max` Type -> TyCon
maxVarID Type
u
maxVarID (Type
t :-> Type
u) = Type -> TyCon
maxVarID Type
t TyCon -> TyCon -> TyCon
forall a. Ord a => a -> a -> a
`max` Type -> TyCon
maxVarID Type
u
maxVarID (Type
_ :=> Type
u) = Type -> TyCon
maxVarID Type
u
type Kind = Int
type TyVar = Int8
type TyCon = TyVar
type TypeName = String
data Decoder = Dec [TyVar] TyVar
deriving Int -> Decoder -> ShowS
[Decoder] -> ShowS
Decoder -> String
(Int -> Decoder -> ShowS)
-> (Decoder -> String) -> ([Decoder] -> ShowS) -> Show Decoder
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Decoder] -> ShowS
$cshowList :: [Decoder] -> ShowS
show :: Decoder -> String
$cshow :: Decoder -> String
showsPrec :: Int -> Decoder -> ShowS
$cshowsPrec :: Int -> Decoder -> ShowS
Show
{-# INLINE normalizeVarIDs #-}
normalizeVarIDs :: Type -> TyVar -> (Type, Decoder)
normalizeVarIDs :: Type -> TyCon -> (Type, Decoder)
normalizeVarIDs Type
ty TyCon
mx = let decoList :: [TyCon]
decoList = [TyCon] -> [TyCon]
forall a. Eq a => [a] -> [a]
nub ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ Type -> [TyCon]
tyvars Type
ty
tup :: [(TyCon, TyCon)]
tup = [TyCon] -> [TyCon] -> [(TyCon, TyCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyCon]
decoList [TyCon
0..]
encoType :: Type
encoType = (TyCon -> TyCon) -> Type -> Type
mapTV (\TyCon
tv -> case TyCon -> [(TyCon, TyCon)] -> Maybe TyCon
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
tv [(TyCon, TyCon)]
tup of Just TyCon
n -> TyCon
n) Type
ty
len :: TyCon
len = [TyCon] -> TyCon
forall i a. Num i => [a] -> i
genericLength [TyCon]
decoList
margin :: TyCon
margin =
TyCon
mx TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
+ TyCon
1 TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
- TyCon
len
in
(Type
encoType, [TyCon] -> TyCon -> Decoder
Dec [TyCon]
decoList TyCon
margin)
normalize :: Type -> Type
normalize Type
ty = (Type, Decoder) -> Type
forall a b. (a, b) -> a
fst ((Type, Decoder) -> Type) -> (Type, Decoder) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> TyCon -> (Type, Decoder)
normalizeVarIDs Type
ty (String -> TyCon
forall a. HasCallStack => String -> a
error String
"undef of normalize")
eqType :: Type -> Type -> Bool
eqType :: Type -> Type -> Bool
eqType Type
t0 Type
t1 = Type -> Type
normalize Type
t0 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Type
normalize Type
t1
saferQuantify, quantify, quantify', unquantify :: Type -> Type
saferQuantify :: Type -> Type
saferQuantify = Type -> Type
quantify (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type
negUnquantify
negUnquantify :: Type -> Type
negUnquantify (TC TyCon
i) | TyCon
i TyCon -> TyCon -> Bool
forall a. Ord a => a -> a -> Bool
< TyCon
0 = TyCon -> Type
TV (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
forall a b. (Integral a, Num b) => a -> b
fromIntegral TyCon
i
negUnquantify (TA Type
t Type
u) = Type -> Type -> Type
TA (Type -> Type
negUnquantify Type
t) (Type -> Type
negUnquantify Type
u)
negUnquantify (Type
u :-> Type
t) = Type -> Type
negUnquantify Type
u Type -> Type -> Type
:-> Type -> Type
negUnquantify Type
t
negUnquantify (Type
u :> Type
t) = Type -> Type
negUnquantify Type
u Type -> Type -> Type
:> Type -> Type
negUnquantify Type
t
negUnquantify (Type
u :=> Type
t) = String -> Type
forall a. HasCallStack => String -> a
error String
"negUnquantify: applied to types with contexts"
negUnquantify Type
t = Type
t
quantify :: Type -> Type
quantify Type
ty = Type -> Type
quantify' (Type -> Type
normalize Type
ty)
quantify' :: Type -> Type
quantify' (TV TyCon
iD) = TyCon -> Type
TC (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
forall a b. (Integral a, Num b) => a -> b
fromIntegral (-TyCon
iDTyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
-TyCon
1)
quantify' tc :: Type
tc@(TC TyCon
_) = Type
tc
quantify' (TA Type
t Type
u) = Type -> Type -> Type
TA (Type -> Type
quantify' Type
t) (Type -> Type
quantify' Type
u)
quantify' (Type
u :-> Type
t) = Type -> Type
quantify' Type
u Type -> Type -> Type
:-> Type -> Type
quantify' Type
t
quantify' (Type
u :> Type
t) = Type -> Type
quantify' Type
u Type -> Type -> Type
:> Type -> Type
quantify' Type
t
unquantify :: Type -> Type
unquantify (TC TyCon
tc) | TyCon
tc TyCon -> TyCon -> Bool
forall a. Ord a => a -> a -> Bool
< TyCon
0 = TyCon -> Type
TV (TyCon -> Type) -> TyCon -> Type
forall a b. (a -> b) -> a -> b
$ TyCon -> TyCon
forall a b. (Integral a, Num b) => a -> b
fromIntegral (-TyCon
1TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
-TyCon
tc)
unquantify (TA Type
t Type
u) = Type -> Type -> Type
TA (Type -> Type
unquantify Type
t) (Type -> Type
unquantify Type
u)
unquantify (Type
u :-> Type
t) = Type -> Type
unquantify Type
u Type -> Type -> Type
:-> Type -> Type
unquantify Type
t
unquantify (Type
u :> Type
t) = Type -> Type
unquantify Type
u Type -> Type -> Type
:> Type -> Type
unquantify Type
t
unquantify (Type
u :=> Type
t) = String -> Type
forall a. HasCallStack => String -> a
error String
"unquantify: applied to types with contexts"
unquantify Type
t = Type
t
unifyFunAp :: String -> Type -> Type -> Type
unifyFunAp String
str Type
t Type
u = case Type -> Type -> Maybe Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
uniFunAp Type
t Type
u of Just Type
v -> String -> Type -> Type
forall p a. p -> a -> a
trace (String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". unify "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
t String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" and "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
u) Type
v
Maybe Type
Nothing -> String -> Type
forall a. HasCallStack => String -> a
error (String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". unifyFunAp: t = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
", and u = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
u)
uniFunAp :: MonadPlus m => Type -> Type -> m Type
uniFunAp :: Type -> Type -> m Type
uniFunAp (Type
a:->Type
r) Type
t = do Subst
subst <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu (Type -> Type
getRet Type
a) (Type -> Type
getRet Type
t)
Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst -> Type -> Type
apply Subst
subst Type
r)
uniFunAp (Type
a:=>Type
r) Type
t = Type -> Type -> m Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
uniFunAp (Type
aType -> Type -> Type
:->Type
r) Type
t
uniFunAp Type
f Type
t = m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
mguFunAp :: MonadPlus m => Type -> Type -> m Type
mguFunAp :: Type -> Type -> m Type
mguFunAp Type
t0 Type
t1 = String -> m Type -> m Type
forall p a. p -> a -> a
trace (String
"mguFunAp t0 = "String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t0String -> ShowS
forall a. [a] -> [a] -> [a]
++String
", and t1 = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
t1) (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$
case Type -> TyCon
maxVarID Type
t1 TyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
+ TyCon
1 of TyCon
mx -> Type -> Type -> m Type
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Type
mfa ((TyCon -> TyCon) -> Type -> Type
mapTV (TyCon
mxTyCon -> TyCon -> TyCon
forall a. Num a => a -> a -> a
+) Type
t0) Type
t1
mfa :: Type -> Type -> m Type
mfa (Type
a:->Type
r) Type
t = do Subst
subst <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
a Type
t
let retv :: Type
retv = (Subst -> Type -> Type
apply Subst
subst Type
r)
String -> m Type -> m Type
forall p a. p -> a -> a
trace (String
"retv = "String -> ShowS
forall a. [a] -> [a] -> [a]
++Type -> String
forall a. Show a => a -> String
show Type
retv) (m Type -> m Type) -> m Type -> m Type
forall a b. (a -> b) -> a -> b
$ Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
retv
mfa (Type
a:>Type
r) Type
t = Type -> Type -> m Type
mfa (Type
aType -> Type -> Type
:->Type
r) Type
t
mfa (Type
a:=>Type
r) Type
t = Type -> Type -> m Type
mfa (Type
aType -> Type -> Type
:->Type
r) Type
t
mfa t :: Type
t@(TV TyCon
_) Type
_ = Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
mfa Type
f Type
t = m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
pushArgsCPS :: Integral i => (i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS :: (i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS i -> i -> [Type] -> Type -> a
f = i -> i -> [Type] -> Type -> a
pa i
0 i
0
where
pa :: i -> i -> [Type] -> Type -> a
pa i
c i
n [Type]
args (Type
t0:->Type
t1) = i -> i -> [Type] -> Type -> a
pa i
c (i
ni -> i -> i
forall a. Num a => a -> a -> a
+i
1) (Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
t1
pa i
c i
n [Type]
args (Type
t0:>Type
t1) = i -> i -> [Type] -> Type -> a
pa i
c (i
ni -> i -> i
forall a. Num a => a -> a -> a
+i
1) (Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
t1
pa i
c i
n [Type]
args (Type
t0:=>Type
t1) = i -> i -> [Type] -> Type -> a
pa (i
ci -> i -> i
forall a. Num a => a -> a -> a
+i
1) i
n (Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
t1
pa i
c i
n [Type]
args Type
retty = i -> i -> [Type] -> Type -> a
f i
c i
n [Type]
args Type
retty
pushArgs :: [Type] -> Type -> ([Type],Type)
pushArgs :: [Type] -> Type -> ([Type], Type)
pushArgs = (Integer -> Integer -> [Type] -> Type -> ([Type], Type))
-> [Type] -> Type -> ([Type], Type)
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\Integer
_ Integer
_ [Type]
a Type
r -> ([Type]
a,Type
r))
getRet :: Type -> Type
getRet = (Integer -> Integer -> [Type] -> Type -> Type)
-> [Type] -> Type -> Type
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\Integer
_ Integer
_ [Type]
_ Type
r -> Type
r) [Type]
forall a. HasCallStack => a
undefined
getArgs :: Type -> [Type]
getArgs = (Integer -> Integer -> [Type] -> Type -> [Type])
-> [Type] -> Type -> [Type]
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\Integer
_ Integer
_ [Type]
a Type
_ -> [Type]
a) []
getNumCxts, getArity :: Integral i => Type -> i
getNumCxts :: Type -> i
getNumCxts = (i -> i -> [Type] -> Type -> i) -> [Type] -> Type -> i
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
c i
_ [Type]
_ Type
_ -> i
c) [Type]
forall a. HasCallStack => a
undefined
getArity :: Type -> i
getArity = (i -> i -> [Type] -> Type -> i) -> [Type] -> Type -> i
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
_ i
i [Type]
_ Type
_ -> i
i) [Type]
forall a. HasCallStack => a
undefined
getArities :: Integral i => Type -> (i,i)
getArities :: Type -> (i, i)
getArities = (i -> i -> [Type] -> Type -> (i, i)) -> [Type] -> Type -> (i, i)
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
c i
i [Type]
_ Type
_ -> (i
c,i
i)) [Type]
forall a. HasCallStack => a
undefined
getAritiesRet :: Integral i => Type -> (i,i,Type)
getAritiesRet :: Type -> (i, i, Type)
getAritiesRet = (i -> i -> [Type] -> Type -> (i, i, Type))
-> [Type] -> Type -> (i, i, Type)
forall i a.
Integral i =>
(i -> i -> [Type] -> Type -> a) -> [Type] -> Type -> a
pushArgsCPS (\i
c i
i [Type]
_ Type
r -> (i
c,i
i,Type
r)) [Type]
forall a. HasCallStack => a
undefined
splitArgs :: Type -> ([Type],Type)
splitArgs :: Type -> ([Type], Type)
splitArgs = [Type] -> Type -> ([Type], Type)
pushArgs []
revSplitArgs :: Integral i => Type -> (i,[Type],Type)
revSplitArgs :: Type -> (i, [Type], Type)
revSplitArgs (Type
t0:->Type
t1) = case Type -> (i, [Type], Type)
forall i. Integral i => Type -> (i, [Type], Type)
revSplitArgs Type
t1 of (i
n,[Type]
args,Type
ret) -> (i
ni -> i -> i
forall a. Num a => a -> a -> a
+i
1, Type
t0Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args, Type
ret)
revSplitArgs Type
t = (i
0, [], Type
t)
revGetArgs :: Type -> [Type]
revGetArgs :: Type -> [Type]
revGetArgs Type
ty = case Type -> (Integer, [Type], Type)
forall i. Integral i => Type -> (i, [Type], Type)
revSplitArgs Type
ty of (Integer
_,[Type]
ts,Type
_) -> [Type]
ts
popArgs :: [Type] -> Type -> Type
popArgs :: [Type] -> Type -> Type
popArgs = (Type -> [Type] -> Type) -> [Type] -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
(:->)))
\end{code}
data "Typed", taken from obsolete/Binding.hs
\begin{code}
data Typed a = a ::: !Type deriving (Int -> Typed a -> ShowS
[Typed a] -> ShowS
Typed a -> String
(Int -> Typed a -> ShowS)
-> (Typed a -> String) -> ([Typed a] -> ShowS) -> Show (Typed a)
forall a. Show a => Int -> Typed a -> ShowS
forall a. Show a => [Typed a] -> ShowS
forall a. Show a => Typed a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Typed a] -> ShowS
$cshowList :: forall a. Show a => [Typed a] -> ShowS
show :: Typed a -> String
$cshow :: forall a. Show a => Typed a -> String
showsPrec :: Int -> Typed a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Typed a -> ShowS
Show, Typed a -> Typed a -> Bool
(Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool) -> Eq (Typed a)
forall a. Eq a => Typed a -> Typed a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Typed a -> Typed a -> Bool
$c/= :: forall a. Eq a => Typed a -> Typed a -> Bool
== :: Typed a -> Typed a -> Bool
$c== :: forall a. Eq a => Typed a -> Typed a -> Bool
Eq, Eq (Typed a)
Eq (Typed a)
-> (Typed a -> Typed a -> Ordering)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Bool)
-> (Typed a -> Typed a -> Typed a)
-> (Typed a -> Typed a -> Typed a)
-> Ord (Typed a)
Typed a -> Typed a -> Bool
Typed a -> Typed a -> Ordering
Typed a -> Typed a -> Typed a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Typed a)
forall a. Ord a => Typed a -> Typed a -> Bool
forall a. Ord a => Typed a -> Typed a -> Ordering
forall a. Ord a => Typed a -> Typed a -> Typed a
min :: Typed a -> Typed a -> Typed a
$cmin :: forall a. Ord a => Typed a -> Typed a -> Typed a
max :: Typed a -> Typed a -> Typed a
$cmax :: forall a. Ord a => Typed a -> Typed a -> Typed a
>= :: Typed a -> Typed a -> Bool
$c>= :: forall a. Ord a => Typed a -> Typed a -> Bool
> :: Typed a -> Typed a -> Bool
$c> :: forall a. Ord a => Typed a -> Typed a -> Bool
<= :: Typed a -> Typed a -> Bool
$c<= :: forall a. Ord a => Typed a -> Typed a -> Bool
< :: Typed a -> Typed a -> Bool
$c< :: forall a. Ord a => Typed a -> Typed a -> Bool
compare :: Typed a -> Typed a -> Ordering
$ccompare :: forall a. Ord a => Typed a -> Typed a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (Typed a)
Ord)
typee :: Typed a -> a
typee (a
a ::: Type
_) = a
a
typer :: Typed a -> Type
typer (a
_ ::: Type
t) = Type
t
instance Functor Typed where
fmap :: (a -> b) -> Typed a -> Typed b
fmap a -> b
f (a
a ::: Type
t) = a -> b
f a
a b -> Type -> Typed b
forall a. a -> Type -> Typed a
::: Type
t
\end{code}
\section{Type inference tools}
\begin{code}
type Subst = [(TyVar,Type)]
showsAssoc :: [(a, a)] -> ShowS
showsAssoc [] = ShowS
forall a. a -> a
id
showsAssoc ((a
k,a
v):[(a, a)]
assocs) = (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Show a => a -> ShowS
shows a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"\t|-> "String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ShowS
forall a. Show a => a -> ShowS
shows a
v ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'\n'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, a)] -> ShowS
showsAssoc [(a, a)]
assocs
emptySubst :: [a]
emptySubst = []
unitSubst :: a -> b -> [(a, b)]
unitSubst a
k b
e = [(a
k, b
e)]
match, mgu :: MonadPlus m => Type -> Type -> m Subst
match :: Type -> Type -> m Subst
match (Type
l :-> Type
r) (Type
l' :-> Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
match2Ap Type
l Type
r Type
l' Type
r'
match (TA Type
l Type
r) (TA Type
l' Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
match2Ap Type
l Type
r Type
l' Type
r'
match (TV TyCon
u) Type
t = TyCon -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => TyCon -> Type -> m Subst
varBind TyCon
u Type
t
match (TC TyCon
tc1) (TC TyCon
tc2) | TyCon
tc1TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
==TyCon
tc2 = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
forall a. [a]
emptySubst
match Type
_ Type
_ = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero
match2Ap :: Type -> Type -> Type -> Type -> m Subst
match2Ap Type
l Type
r Type
l' Type
r' = do Subst
s1 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
match Type
l Type
l'
Subst
s2 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
match (Subst -> Type -> Type
apply Subst
s1 Type
r) Type
r'
Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
s2 Subst -> Subst -> Subst
`plusSubst` Subst
s1)
unChin :: Type -> Type
unChin (TA Type
l Type
r) = Type -> Type -> Type
TA Type
l (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
unChin Type
r
unChin (Type
l :> Type
r) = Type -> Type
unChin Type
l Type -> Type -> Type
:-> Type -> Type
unChin Type
r
unChin (Type
l :-> Type
r) = Type -> Type
unChin Type
l Type -> Type -> Type
:-> Type -> Type
unChin Type
r
unChin (Type
l :=> Type
r) = Type
l Type -> Type -> Type
:=> Type -> Type
unChin Type
r
unChin Type
t = Type
t
mgu :: Type -> Type -> m Subst
mgu (Type
l :-> Type
r) (Type
l' :-> Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
mgu2Ap Type
l Type
r Type
l' Type
r'
#ifdef REALDYNAMIC
mgu (l :-> r) (l' :> r') = mgu2Ap l r l' r'
mgu (l :> r) (l' :-> r') = mgu2Ap l r l' r'
mgu (l :> r) (l' :> r') = mgu2Ap l r l' r'
#endif
mgu (TA Type
l Type
r) (TA Type
l' Type
r') = Type -> Type -> Type -> Type -> m Subst
forall (m :: * -> *).
MonadPlus m =>
Type -> Type -> Type -> Type -> m Subst
mgu2Ap Type
l Type
r Type
l' Type
r'
mgu (TV TyCon
u) Type
t = TyCon -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => TyCon -> Type -> m Subst
varBind TyCon
u Type
t
mgu Type
t (TV TyCon
u) = TyCon -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => TyCon -> Type -> m Subst
varBind TyCon
u Type
t
mgu (TC TyCon
tc1) (TC TyCon
tc2) | TyCon
tc1TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
==TyCon
tc2 = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
forall a. [a]
emptySubst
mgu Type
_ Type
_ = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero
mgu2Ap :: Type -> Type -> Type -> Type -> m Subst
mgu2Ap Type
l Type
r Type
l' Type
r' = do Subst
s1 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu Type
l Type
l'
Subst
s2 <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
mgu (Subst -> Type -> Type
apply Subst
s1 Type
r) (Subst -> Type -> Type
apply Subst
s1 Type
r')
Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
s2 Subst -> Subst -> Subst
`plusSubst` Subst
s1)
varBind :: MonadPlus m => TyVar -> Type -> m Subst
varBind :: TyCon -> Type -> m Subst
varBind TyCon
_ (Type
_:=>Type
_) = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero
varBind TyCon
u Type
t | Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon -> Type
TV TyCon
u = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
forall a. [a]
emptySubst
| TyCon
u TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Type -> [TyCon]
tyvars Type
t) = m Subst
forall (m :: * -> *) a. MonadPlus m => m a
mzero
| Bool
otherwise = Subst -> m Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Type -> Subst
forall a b. a -> b -> [(a, b)]
unitSubst TyCon
u Type
t)
substOK :: Subst -> Bool
substOK :: Subst -> Bool
substOK = ((TyCon, Type) -> Bool) -> Subst -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (TyCon
i,Type
ty) -> Bool -> Bool
not (TyCon
i TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Type -> [TyCon]
tyvars Type
ty)))
assertsubst :: String -> Subst -> Subst
assertsubst :: String -> Subst -> Subst
assertsubst String
str = \Subst
s -> if Subst -> Bool
substOK Subst
s then Subst
s else String -> Subst
forall a. HasCallStack => String -> a
error (String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": assertsubst failed. substitution = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Subst -> String
forall a. Show a => a -> String
show Subst
s)
instance Show Type where
showsPrec :: Int -> Type -> ShowS
showsPrec Int
_ Type
ty = Integer -> Type -> ShowS
forall t. (Show t, Num t) => t -> Type -> ShowS
toString' Integer
0 Type
ty
where toString' :: t -> Type -> ShowS
toString' t
k (TV TyCon
i) = (Char
'a'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> ShowS
forall a. Show a => a -> ShowS
shows TyCon
i
toString' t
k (TC TyCon
i) = (Char
'K'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> ShowS
forall a. Show a => a -> ShowS
shows t
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'I'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> ShowS
forall a. Show a => a -> ShowS
shows TyCon
i
toString' t
k (TA Type
t0 Type
t1) = Bool -> ShowS -> ShowS
showParen Bool
True (t -> Type -> ShowS
toString' (t
kt -> t -> t
forall a. Num a => a -> a -> a
+t
1) Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)
toString' t
k (Type
t0 :=> Type
t1) = Bool -> ShowS -> ShowS
showParen Bool
True (t -> Type -> ShowS
toString' t
0 Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"=>"String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)
toString' t
k (Type
t0 :-> Type
t1) = Bool -> ShowS -> ShowS
showParen Bool
True (t -> Type -> ShowS
toString' t
0 Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"->"String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)
toString' t
k (Type
t0 :> Type
t1) = Bool -> ShowS -> ShowS
showParen Bool
True ((String
"(->) "String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t0 ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Type -> ShowS
toString' t
0 Type
t1)
plusSubst :: Subst -> Subst -> Subst
Subst
s0 plusSubst :: Subst -> Subst -> Subst
`plusSubst` Subst
s1 = [(TyCon
u,
Subst -> Type -> Type
applyCheck Subst
s0 Type
t) | (TyCon
u,Type
t) <- Subst
s1] Subst -> Subst -> Subst
forall a. [a] -> [a] -> [a]
++ Subst
s0
lookupSubst :: MonadPlus m => Subst -> TyVar -> m Type
lookupSubst :: Subst -> TyCon -> m Type
lookupSubst Subst
subst TyCon
i = case TyCon -> Subst -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
i Subst
subst of Maybe Type
Nothing -> m Type
forall (m :: * -> *) a. MonadPlus m => m a
mzero
Just Type
x -> Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
x
apply :: Subst -> Type -> Type
apply :: Subst -> Type -> Type
apply Subst
subst Type
ty = Type -> Type
apply' Type
ty
where apply' :: Type -> Type
apply' tc :: Type
tc@(TC TyCon
_) = Type
tc
apply' tg :: Type
tg@(TV TyCon
tv)
= case Subst -> TyCon -> Maybe Type
forall (m :: * -> *). MonadPlus m => Subst -> TyCon -> m Type
lookupSubst Subst
subst TyCon
tv of Just Type
tt -> Type
tt
Maybe Type
Nothing -> Type
tg
apply' (TA Type
t0 Type
t1) = Type -> Type -> Type
TA (Type -> Type
apply' Type
t0) (Type -> Type
apply' Type
t1)
apply' (Type
t0:->Type
t1) = Type -> Type
apply' Type
t0 Type -> Type -> Type
:-> Type -> Type
apply' Type
t1
apply' (Type
t0:>Type
t1) = Type -> Type
apply' Type
t0 Type -> Type -> Type
:> Type -> Type
apply' Type
t1
apply' (Type
t0:=>Type
t1) = Type -> Type
apply' Type
t0 Type -> Type -> Type
:=> Type -> Type
apply' Type
t1
applyCheck :: Subst -> Type -> Type
applyCheck Subst
subst Type
t =
Subst -> Type -> Type
apply Subst
subst Type
t
\end{code}