module Language.Futhark.TypeChecker.Modules
( matchMTys,
newNamesForMTy,
refineEnv,
applyFunctor,
)
where
import Control.Monad.Except
import Control.Monad.Writer hiding (Sum)
import Data.Either
import Data.List (intersect)
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Ord
import Data.Set qualified as S
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.Semantic
import Language.Futhark.TypeChecker.Monad
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify (doUnification)
import Prelude hiding (abs, mod)
substituteTypesInMod :: TypeSubs -> Mod -> Mod
substituteTypesInMod :: TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs (ModEnv Env
e) =
Env -> Mod
ModEnv forall a b. (a -> b) -> a -> b
$ TypeSubs -> Env -> Env
substituteTypesInEnv TypeSubs
substs Env
e
substituteTypesInMod TypeSubs
substs (ModFun (FunSig TySet
abs Mod
mod MTy
mty)) =
FunSig -> Mod
ModFun forall a b. (a -> b) -> a -> b
$ TySet -> Mod -> MTy -> FunSig
FunSig TySet
abs (TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs Mod
mod) (TypeSubs -> MTy -> MTy
substituteTypesInMTy TypeSubs
substs MTy
mty)
substituteTypesInMTy :: TypeSubs -> MTy -> MTy
substituteTypesInMTy :: TypeSubs -> MTy -> MTy
substituteTypesInMTy TypeSubs
substs (MTy TySet
abs Mod
mod) = TySet -> Mod -> MTy
MTy TySet
abs forall a b. (a -> b) -> a -> b
$ TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs Mod
mod
substituteTypesInEnv :: TypeSubs -> Env -> Env
substituteTypesInEnv :: TypeSubs -> Env -> Env
substituteTypesInEnv TypeSubs
substs Env
env =
Env
env
{ envVtable :: Map VName BoundV
envVtable = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
substs) forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
env,
envTypeTable :: Map VName TypeBinding
envTypeTable = forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey VName -> TypeBinding -> TypeBinding
subT forall a b. (a -> b) -> a -> b
$ Env -> Map VName TypeBinding
envTypeTable Env
env,
envModTable :: Map VName Mod
envModTable = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeSubs -> Mod -> Mod
substituteTypesInMod TypeSubs
substs) forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
env
}
where
subT :: VName -> TypeBinding -> TypeBinding
subT VName
name (TypeAbbr Liftedness
l [TypeParam]
_ StructRetType
_)
| Just (Subst [TypeParam]
ps StructRetType
rt) <- TypeSubs
substs VName
name = Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps StructRetType
rt
subT VName
_ (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims TypeBase Size ()
t)) =
Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l [TypeParam]
ps forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
substs forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase Size ()
t
substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV :: TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV TypeSubs
substs (BoundV [TypeParam]
tps TypeBase Size ()
t) =
let RetType [VName]
dims TypeBase Size ()
t' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
substs forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
t
in [TypeParam] -> TypeBase Size () -> BoundV
BoundV ([TypeParam]
tps forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall vn. vn -> SrcLoc -> TypeParamBase vn
`TypeParamDim` forall a. Monoid a => a
mempty) [VName]
dims) TypeBase Size ()
t'
allNamesInEnv :: Env -> S.Set VName
allNamesInEnv :: Env -> Set VName
allNamesInEnv (Env Map VName BoundV
vtable Map VName TypeBinding
ttable Map VName MTy
stable Map VName Mod
modtable NameMap
_names) =
forall a. Ord a => [a] -> Set a
S.fromList
( forall k a. Map k a -> [k]
M.keys Map VName BoundV
vtable
forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [k]
M.keys Map VName TypeBinding
ttable
forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [k]
M.keys Map VName MTy
stable
forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [k]
M.keys Map VName Mod
modtable
)
forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat
( forall a b. (a -> b) -> [a] -> [b]
map MTy -> Set VName
allNamesInMTy (forall k a. Map k a -> [a]
M.elems Map VName MTy
stable)
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Mod -> Set VName
allNamesInMod (forall k a. Map k a -> [a]
M.elems Map VName Mod
modtable)
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map TypeBinding -> Set VName
allNamesInType (forall k a. Map k a -> [a]
M.elems Map VName TypeBinding
ttable)
)
where
allNamesInType :: TypeBinding -> Set VName
allNamesInType (TypeAbbr Liftedness
_ [TypeParam]
ps StructRetType
_) = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps
allNamesInMod :: Mod -> S.Set VName
allNamesInMod :: Mod -> Set VName
allNamesInMod (ModEnv Env
env) = Env -> Set VName
allNamesInEnv Env
env
allNamesInMod ModFun {} = forall a. Monoid a => a
mempty
allNamesInMTy :: MTy -> S.Set VName
allNamesInMTy :: MTy -> Set VName
allNamesInMTy (MTy TySet
abs Mod
mod) =
forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
abs) forall a. Semigroup a => a -> a -> a
<> Mod -> Set VName
allNamesInMod Mod
mod
newNamesForMTy :: MTy -> TypeM (MTy, M.Map VName VName)
newNamesForMTy :: MTy -> TypeM (MTy, Map VName VName)
newNamesForMTy MTy
orig_mty = do
[(VName, VName)]
pairs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ MTy -> Set VName
allNamesInMTy MTy
orig_mty) forall a b. (a -> b) -> a -> b
$ \VName
v -> do
VName
v' <- forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName VName
v
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
v, VName
v')
let substs :: Map VName VName
substs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(VName, VName)]
pairs
rev_substs :: Map VName VName
rev_substs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip (,)) [(VName, VName)]
pairs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName -> MTy -> MTy
substituteInMTy Map VName VName
substs MTy
orig_mty, Map VName VName
rev_substs)
where
substituteInMTy :: M.Map VName VName -> MTy -> MTy
substituteInMTy :: Map VName VName -> MTy -> MTy
substituteInMTy Map VName VName
substs (MTy TySet
mty_abs Mod
mty_mod) =
TySet -> Mod -> MTy
MTy (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) TySet
mty_abs) (Mod -> Mod
substituteInMod Mod
mty_mod)
where
substituteInEnv :: Env -> Env
substituteInEnv (Env Map VName BoundV
vtable Map VName TypeBinding
ttable Map VName MTy
_stable Map VName Mod
modtable NameMap
names) =
let vtable' :: Map VName BoundV
vtable' = forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap BoundV -> BoundV
substituteInBinding Map VName BoundV
vtable
ttable' :: Map VName TypeBinding
ttable' = forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap TypeBinding -> TypeBinding
substituteInTypeBinding Map VName TypeBinding
ttable
mtable' :: Map VName Mod
mtable' = forall {a} {a}. (a -> a) -> Map VName a -> Map VName a
substituteInMap Mod -> Mod
substituteInMod Map VName Mod
modtable
in Env
{ envVtable :: Map VName BoundV
envVtable = Map VName BoundV
vtable',
envTypeTable :: Map VName TypeBinding
envTypeTable = Map VName TypeBinding
ttable',
envSigTable :: Map VName MTy
envSigTable = forall a. Monoid a => a
mempty,
envModTable :: Map VName Mod
envModTable = Map VName Mod
mtable',
envNameMap :: NameMap
envNameMap = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) NameMap
names
}
substitute :: VName -> VName
substitute VName
v =
forall a. a -> Maybe a -> a
fromMaybe VName
v forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName VName
substs
substituteInMap :: (a -> a) -> Map VName a -> Map VName a
substituteInMap a -> a
f Map VName a
m =
let ([VName]
ks, [a]
vs) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList Map VName a
m
in forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
forall a b. [a] -> [b] -> [(a, b)]
zip
(forall a b. (a -> b) -> [a] -> [b]
map (\VName
k -> forall a. a -> Maybe a -> a
fromMaybe VName
k forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
k Map VName VName
substs) [VName]
ks)
(forall a b. (a -> b) -> [a] -> [b]
map a -> a
f [a]
vs)
substituteInBinding :: BoundV -> BoundV
substituteInBinding (BoundV [TypeParam]
ps TypeBase Size ()
t) =
[TypeParam] -> TypeBase Size () -> BoundV
BoundV (forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) (TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t)
substituteInMod :: Mod -> Mod
substituteInMod (ModEnv Env
env) =
Env -> Mod
ModEnv forall a b. (a -> b) -> a -> b
$ Env -> Env
substituteInEnv Env
env
substituteInMod (ModFun FunSig
funsig) =
FunSig -> Mod
ModFun forall a b. (a -> b) -> a -> b
$ FunSig -> FunSig
substituteInFunSig FunSig
funsig
substituteInFunSig :: FunSig -> FunSig
substituteInFunSig (FunSig TySet
abs Mod
mod MTy
mty) =
TySet -> Mod -> MTy -> FunSig
FunSig
(forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
M.mapKeys (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> VName
substitute) TySet
abs)
(Mod -> Mod
substituteInMod Mod
mod)
(Map VName VName -> MTy -> MTy
substituteInMTy Map VName VName
substs MTy
mty)
substituteInTypeBinding :: TypeBinding -> TypeBinding
substituteInTypeBinding (TypeAbbr Liftedness
l [TypeParam]
ps (RetType [VName]
dims TypeBase Size ()
t)) =
Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
l (forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeParam
substituteInTypeParam [TypeParam]
ps) forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t
substituteInTypeParam :: TypeParam -> TypeParam
substituteInTypeParam (TypeParamDim VName
p SrcLoc
loc) =
forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim (VName -> VName
substitute VName
p) SrcLoc
loc
substituteInTypeParam (TypeParamType Liftedness
l VName
p SrcLoc
loc) =
forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l (VName -> VName
substitute VName
p) SrcLoc
loc
substituteInType :: StructType -> StructType
substituteInType :: TypeBase Size () -> TypeBase Size ()
substituteInType (Scalar (TypeVar () Uniqueness
u (QualName [VName]
qs VName
v) [TypeArg Size]
targs)) =
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
u (forall vn. [vn] -> vn -> QualName vn
QualName (forall a b. (a -> b) -> [a] -> [b]
map VName -> VName
substitute [VName]
qs) forall a b. (a -> b) -> a -> b
$ VName -> VName
substitute VName
v) forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map TypeArg Size -> TypeArg Size
substituteInTypeArg [TypeArg Size]
targs
substituteInType (Scalar (Prim PrimType
t)) =
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t
substituteInType (Scalar (Record Map Name (TypeBase Size ())
ts)) =
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeBase Size () -> TypeBase Size ()
substituteInType Map Name (TypeBase Size ())
ts
substituteInType (Scalar (Sum Map Name [TypeBase Size ()]
ts)) =
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) TypeBase Size () -> TypeBase Size ()
substituteInType Map Name [TypeBase Size ()]
ts
substituteInType (Array () Uniqueness
u Shape Size
shape ScalarTypeBase Size ()
t) =
forall as dim.
Monoid as =>
Uniqueness -> Shape dim -> TypeBase dim as -> TypeBase dim as
arrayOf Uniqueness
u (Shape Size -> Shape Size
substituteInShape Shape Size
shape) (TypeBase Size () -> TypeBase Size ()
substituteInType forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar ScalarTypeBase Size ()
t)
substituteInType (Scalar (Arrow ()
als PName
v TypeBase Size ()
t1 (RetType [VName]
dims TypeBase Size ()
t2))) =
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow ()
als PName
v (TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t1) forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t2
substituteInShape :: Shape Size -> Shape Size
substituteInShape (Shape [Size]
ds) =
forall dim. [dim] -> Shape dim
Shape forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Size -> Size
substituteInDim [Size]
ds
substituteInDim :: Size -> Size
substituteInDim (NamedSize (QualName [VName]
qs VName
v)) =
QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall vn. [vn] -> vn -> QualName vn
QualName (forall a b. (a -> b) -> [a] -> [b]
map VName -> VName
substitute [VName]
qs) forall a b. (a -> b) -> a -> b
$ VName -> VName
substitute VName
v
substituteInDim Size
d = Size
d
substituteInTypeArg :: TypeArg Size -> TypeArg Size
substituteInTypeArg (TypeArgDim (NamedSize (QualName [VName]
qs VName
v)) SrcLoc
loc) =
forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall vn. [vn] -> vn -> QualName vn
QualName (forall a b. (a -> b) -> [a] -> [b]
map VName -> VName
substitute [VName]
qs) forall a b. (a -> b) -> a -> b
$ VName -> VName
substitute VName
v) SrcLoc
loc
substituteInTypeArg (TypeArgDim (ConstSize Int
x) SrcLoc
loc) =
forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (Int -> Size
ConstSize Int
x) SrcLoc
loc
substituteInTypeArg (TypeArgDim (AnySize Maybe VName
v) SrcLoc
loc) =
forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (Maybe VName -> Size
AnySize Maybe VName
v) SrcLoc
loc
substituteInTypeArg (TypeArgType TypeBase Size ()
t SrcLoc
loc) =
forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType (TypeBase Size () -> TypeBase Size ()
substituteInType TypeBase Size ()
t) SrcLoc
loc
mtyTypeAbbrs :: MTy -> M.Map VName TypeBinding
mtyTypeAbbrs :: MTy -> Map VName TypeBinding
mtyTypeAbbrs (MTy TySet
_ Mod
mod) = Mod -> Map VName TypeBinding
modTypeAbbrs Mod
mod
modTypeAbbrs :: Mod -> M.Map VName TypeBinding
modTypeAbbrs :: Mod -> Map VName TypeBinding
modTypeAbbrs (ModEnv Env
env) =
Env -> Map VName TypeBinding
envTypeAbbrs Env
env
modTypeAbbrs (ModFun (FunSig TySet
_ Mod
mod MTy
mty)) =
Mod -> Map VName TypeBinding
modTypeAbbrs Mod
mod forall a. Semigroup a => a -> a -> a
<> MTy -> Map VName TypeBinding
mtyTypeAbbrs MTy
mty
envTypeAbbrs :: Env -> M.Map VName TypeBinding
envTypeAbbrs :: Env -> Map VName TypeBinding
envTypeAbbrs Env
env =
Env -> Map VName TypeBinding
envTypeTable Env
env
forall a. Semigroup a => a -> a -> a
<> (forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Mod -> Map VName TypeBinding
modTypeAbbrs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [a]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Map VName Mod
envModTable) Env
env
refineEnv ::
SrcLoc ->
TySet ->
Env ->
QualName Name ->
[TypeParam] ->
StructType ->
TypeM (QualName VName, TySet, Env)
refineEnv :: SrcLoc
-> TySet
-> Env
-> QualName Name
-> [TypeParam]
-> TypeBase Size ()
-> TypeM (QualName VName, TySet, Env)
refineEnv SrcLoc
loc TySet
tset Env
env QualName Name
tname [TypeParam]
ps TypeBase Size ()
t
| Just (QualName VName
tname', TypeAbbr Liftedness
_ [TypeParam]
cur_ps (RetType [VName]
_ (Scalar (TypeVar () Uniqueness
_ (QualName [VName]
qs VName
v) [TypeArg Size]
_)))) <-
QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef QualName Name
tname (Env -> Mod
ModEnv Env
env),
forall vn. [vn] -> vn -> QualName vn
QualName (forall vn. QualName vn -> [vn]
qualQuals QualName VName
tname') VName
v forall k a. Ord k => k -> Map k a -> Bool
`M.member` TySet
tset =
if [TypeParam] -> [TypeParam] -> Bool
paramsMatch [TypeParam]
cur_ps [TypeParam]
ps
then
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( QualName VName
tname',
forall vn. [vn] -> vn -> QualName vn
QualName [VName]
qs VName
v forall k a. Ord k => k -> Map k a -> Map k a
`M.delete` TySet
tset,
TypeSubs -> Env -> Env
substituteTypesInEnv
( forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup forall a b. (a -> b) -> a -> b
$
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
[ (forall vn. QualName vn -> vn
qualLeaf QualName VName
tname', forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
cur_ps forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
t),
(VName
v, forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size ()
t)
]
)
Env
env
)
else
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Cannot refine a type having"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall {a} {ann}. Pretty a => [a] -> Doc ann
tpMsg [TypeParam]
ps forall a. Semigroup a => a -> a -> a
<> Doc ()
" with a type having " forall a. Semigroup a => a -> a -> a
<> forall {a} {ann}. Pretty a => [a] -> Doc ann
tpMsg [TypeParam]
cur_ps forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
| Bool
otherwise =
forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$ forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
tname) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is not an abstract type in the module type."
where
tpMsg :: [a] -> Doc ann
tpMsg [] = Doc ann
"no type parameters"
tpMsg [a]
xs = Doc ann
"type parameters" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [a]
xs)
paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch :: [TypeParam] -> [TypeParam] -> Bool
paramsMatch [TypeParam]
ps1 [TypeParam]
ps2 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps2 Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {vn} {vn}. (TypeParamBase vn, TypeParamBase vn) -> Bool
match (forall a b. [a] -> [b] -> [(a, b)]
zip [TypeParam]
ps1 [TypeParam]
ps2)
where
match :: (TypeParamBase vn, TypeParamBase vn) -> Bool
match (TypeParamType Liftedness
l1 vn
_ SrcLoc
_, TypeParamType Liftedness
l2 vn
_ SrcLoc
_) = Liftedness
l1 forall a. Ord a => a -> a -> Bool
<= Liftedness
l2
match (TypeParamDim vn
_ SrcLoc
_, TypeParamDim vn
_ SrcLoc
_) = Bool
True
match (TypeParamBase vn, TypeParamBase vn)
_ = Bool
False
findBinding ::
(Env -> M.Map VName v) ->
Namespace ->
Name ->
Env ->
Maybe (VName, v)
findBinding :: forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName v
table Namespace
namespace Name
name Env
the_env = do
QualName [VName]
_ VName
name' <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
namespace, Name
name) forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
the_env
(VName
name',) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
name' (Env -> Map VName v
table Env
the_env)
findTypeDef :: QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef :: QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef QualName Name
_ ModFun {} = forall a. Maybe a
Nothing
findTypeDef (QualName [] Name
name) (ModEnv Env
the_env) = do
(VName
name', TypeBinding
tb) <- forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName TypeBinding
envTypeTable Namespace
Type Name
name Env
the_env
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall v. v -> QualName v
qualName VName
name', TypeBinding
tb)
findTypeDef (QualName (Name
q : [Name]
qs) Name
name) (ModEnv Env
the_env) = do
(VName
q', Mod
q_mod) <- forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName Mod
envModTable Namespace
Term Name
q Env
the_env
(QualName [VName]
qs' VName
name', TypeBinding
tb) <- QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef (forall vn. [vn] -> vn -> QualName vn
QualName [Name]
qs Name
name) Mod
q_mod
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall vn. [vn] -> vn -> QualName vn
QualName (VName
q' forall a. a -> [a] -> [a]
: [VName]
qs') VName
name', TypeBinding
tb)
resolveAbsTypes ::
TySet ->
Mod ->
TySet ->
Loc ->
Either TypeError (M.Map VName (QualName VName, TypeBinding))
resolveAbsTypes :: TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod TySet
sig_abs Loc
loc = do
let abs_mapping :: Map (QualName Name) (QualName VName, Liftedness)
abs_mapping =
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
forall a b. [a] -> [b] -> [(a, b)]
zip
(forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList TySet
mod_abs)
(forall k a. Map k a -> [(k, a)]
M.toList TySet
mod_abs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
M.toList TySet
sig_abs) forall a b. (a -> b) -> a -> b
$ \(QualName VName
name, Liftedness
name_l) ->
case QualName Name -> Mod -> Maybe (QualName VName, TypeBinding)
findTypeDef (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name) Mod
mod of
Just (QualName VName
name', TypeAbbr Liftedness
mod_l [TypeParam]
ps StructRetType
t)
| Liftedness
mod_l forall a. Ord a => a -> a -> Bool
> Liftedness
name_l ->
forall {b}.
Liftedness
-> [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedLiftedness
Liftedness
name_l
(forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
mod_abs)
QualName VName
name
(Liftedness
mod_l, [TypeParam]
ps, StructRetType
t)
| Liftedness
name_l forall a. Ord a => a -> a -> Bool
< Liftedness
SizeLifted,
Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall dim as. RetTypeBase dim as -> [VName]
retDims StructRetType
t ->
forall {b}.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
anonymousSizes
(forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys TySet
mod_abs)
QualName VName
name
(Liftedness
mod_l, [TypeParam]
ps, StructRetType
t)
| Just (QualName VName
abs_name, Liftedness
_) <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name) Map (QualName Name) (QualName VName, Liftedness)
abs_mapping ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall vn. QualName vn -> vn
qualLeaf QualName VName
name, (QualName VName
abs_name, Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
name_l [TypeParam]
ps StructRetType
t))
| Bool
otherwise ->
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall vn. QualName vn -> vn
qualLeaf QualName VName
name, (QualName VName
name', Liftedness -> [TypeParam] -> StructRetType -> TypeBinding
TypeAbbr Liftedness
name_l [TypeParam]
ps StructRetType
t))
Maybe (QualName VName, TypeBinding)
_ ->
forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VName -> Name
baseName QualName VName
name
where
mismatchedLiftedness :: Liftedness
-> [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedLiftedness Liftedness
name_l [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf Loc
loc) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module defines"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module type requires"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
what forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
where
what :: Doc ()
what = case Liftedness
name_l of
Liftedness
Unlifted -> Doc ()
"a non-lifted type"
Liftedness
SizeLifted -> Doc ()
"a size-lifted type"
Liftedness
Lifted -> Doc ()
"a lifted type"
anonymousSizes :: [VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
anonymousSizes [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError (forall a. Located a => a -> Loc
locOf Loc
loc) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module defines"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness, [TypeParam], StructRetType)
mod_t)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"which contains anonymous sizes, but module type requires non-lifted type."
resolveMTyNames ::
MTy ->
MTy ->
M.Map VName (QualName VName)
resolveMTyNames :: MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames = MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames'
where
resolveMTyNames' :: MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames' (MTy TySet
_mod_abs Mod
mod) (MTy TySet
_sig_abs Mod
sig) =
Mod -> Mod -> Map VName (QualName VName)
resolveModNames Mod
mod Mod
sig
resolveModNames :: Mod -> Mod -> Map VName (QualName VName)
resolveModNames (ModEnv Env
mod_env) (ModEnv Env
sig_env) =
Env -> Env -> Map VName (QualName VName)
resolveEnvNames Env
mod_env Env
sig_env
resolveModNames (ModFun FunSig
mod_fun) (ModFun FunSig
sig_fun) =
Mod -> Mod -> Map VName (QualName VName)
resolveModNames (FunSig -> Mod
funSigMod FunSig
mod_fun) (FunSig -> Mod
funSigMod FunSig
sig_fun)
forall a. Semigroup a => a -> a -> a
<> MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames' (FunSig -> MTy
funSigMty FunSig
mod_fun) (FunSig -> MTy
funSigMty FunSig
sig_fun)
resolveModNames Mod
_ Mod
_ =
forall a. Monoid a => a
mempty
resolveEnvNames :: Env -> Env -> Map VName (QualName VName)
resolveEnvNames Env
mod_env Env
sig_env =
let mod_substs :: Map VName (QualName VName)
mod_substs = forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Term Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig_env
onMod :: (VName, Mod) -> Map VName (QualName VName)
onMod (VName
modname, Mod
mod_env_mod) =
case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
modname Map VName (QualName VName)
mod_substs of
Just (QualName [VName]
_ VName
modname')
| Just Mod
sig_env_mod <-
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
modname' forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
mod_env ->
Mod -> Mod -> Map VName (QualName VName)
resolveModNames Mod
sig_env_mod Mod
mod_env_mod
Maybe (QualName VName)
_ -> forall a. Monoid a => a
mempty
in forall a. Monoid a => [a] -> a
mconcat
[ forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Term Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Type Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
forall {a}.
Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
Signature Env
mod_env forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig_env,
Map VName (QualName VName)
mod_substs,
forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (VName, Mod) -> Map VName (QualName VName)
onMod forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig_env
]
resolve :: Namespace -> Env -> Map VName a -> Map VName (QualName VName)
resolve Namespace
namespace Env
mod_env = forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey forall {p}. VName -> p -> Maybe (QualName VName)
resolve'
where
resolve' :: VName -> p -> Maybe (QualName VName)
resolve' VName
name p
_ =
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
namespace, VName -> Name
baseName VName
name) forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
mod_env
missingType :: Pretty a => Loc -> a -> Either TypeError b
missingType :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc a
name =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module does not define a type named" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
name forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
missingVal :: Pretty a => Loc -> a -> Either TypeError b
missingVal :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingVal Loc
loc a
name =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module does not define a value named" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
name forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
missingMod :: Pretty a => Loc -> a -> Either TypeError b
missingMod :: forall a b. Pretty a => Loc -> a -> Either TypeError b
missingMod Loc
loc a
name =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module does not define a module named" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
name forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
mismatchedType ::
Loc ->
[VName] ->
[VName] ->
VName ->
(Liftedness, [TypeParam], StructRetType) ->
(Liftedness, [TypeParam], StructRetType) ->
Either TypeError b
mismatchedType :: forall b.
Loc
-> [VName]
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructRetType)
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedType Loc
loc [VName]
abs [VName]
quals VName
name (Liftedness, [TypeParam], StructRetType)
spec_t (Liftedness, [TypeParam], StructRetType)
env_t =
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module defines"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness, [TypeParam], StructRetType)
env_t)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module type requires"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness, [TypeParam], StructRetType)
spec_t)
ppTypeAbbr :: [VName] -> QualName VName -> (Liftedness, [TypeParam], StructRetType) -> Doc a
ppTypeAbbr :: forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [VName]
abs QualName VName
name (Liftedness
l, [TypeParam]
ps, RetType [] (Scalar (TypeVar () Uniqueness
_ QualName VName
tn [TypeArg Size]
args)))
| forall vn. QualName vn -> vn
qualLeaf QualName VName
tn forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
abs,
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> TypeArg Size
typeParamToArg [TypeParam]
ps forall a. Eq a => a -> a -> Bool
== [TypeArg Size]
args =
Doc a
"type" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Liftedness
l
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
name
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
ps)
ppTypeAbbr [VName]
_ QualName VName
name (Liftedness
l, [TypeParam]
ps, StructRetType
t) =
Doc a
"type" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Liftedness
l
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a ann. Pretty a => a -> Doc ann
pretty QualName VName
name forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
ps)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
equals
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty StructRetType
t))
matchMTys ::
MTy ->
MTy ->
Loc ->
Either TypeError (M.Map VName VName)
matchMTys :: MTy -> MTy -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
orig_mty MTy
orig_mty_sig =
Map VName (Subst StructRetType)
-> [VName]
-> MTy
-> MTy
-> Loc
-> Either TypeError (Map VName VName)
matchMTys'
(forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall t. Size -> Subst t
SizeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize) forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> Map VName (QualName VName)
resolveMTyNames MTy
orig_mty MTy
orig_mty_sig)
[]
MTy
orig_mty
MTy
orig_mty_sig
where
matchMTys' ::
M.Map VName (Subst StructRetType) ->
[VName] ->
MTy ->
MTy ->
Loc ->
Either TypeError (M.Map VName VName)
matchMTys' :: Map VName (Subst StructRetType)
-> [VName]
-> MTy
-> MTy
-> Loc
-> Either TypeError (Map VName VName)
matchMTys' Map VName (Subst StructRetType)
_ [VName]
_ (MTy TySet
_ ModFun {}) (MTy TySet
_ ModEnv {}) Loc
loc =
forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
Loc -> Notes -> Doc () -> TypeError
TypeError
Loc
loc
forall a. Monoid a => a
mempty
Doc ()
"Cannot match parametric module with non-parametric module type."
matchMTys' Map VName (Subst StructRetType)
_ [VName]
_ (MTy TySet
_ ModEnv {}) (MTy TySet
_ ModFun {}) Loc
loc =
forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
Loc -> Notes -> Doc () -> TypeError
TypeError
Loc
loc
forall a. Monoid a => a
mempty
Doc ()
"Cannot match non-parametric module with paramatric module type."
matchMTys' Map VName (Subst StructRetType)
old_abs_subst_to_type [VName]
quals (MTy TySet
mod_abs Mod
mod) (MTy TySet
sig_abs Mod
sig) Loc
loc = do
Map VName (QualName VName, TypeBinding)
abs_substs <- TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod TySet
sig_abs Loc
loc
let abs_subst_to_type :: Map VName (Subst StructRetType)
abs_subst_to_type =
Map VName (Subst StructRetType)
old_abs_subst_to_type forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
abs_substs
abs_name_substs :: Map VName VName
abs_name_substs = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall vn. QualName vn -> vn
qualLeaf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Map VName (QualName VName, TypeBinding)
abs_substs
Map VName VName
substs <- Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals Mod
mod Mod
sig Loc
loc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName
substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
abs_name_substs)
matchMods ::
M.Map VName (Subst StructRetType) ->
[VName] ->
Mod ->
Mod ->
Loc ->
Either TypeError (M.Map VName VName)
matchMods :: Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
_ [VName]
_ ModEnv {} ModFun {} Loc
loc =
forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
Loc -> Notes -> Doc () -> TypeError
TypeError
Loc
loc
forall a. Monoid a => a
mempty
Doc ()
"Cannot match non-parametric module with parametric module type."
matchMods Map VName (Subst StructRetType)
_ [VName]
_ ModFun {} ModEnv {} Loc
loc =
forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
Loc -> Notes -> Doc () -> TypeError
TypeError
Loc
loc
forall a. Monoid a => a
mempty
Doc ()
"Cannot match parametric module with non-parametric module type."
matchMods Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals (ModEnv Env
mod) (ModEnv Env
sig) Loc
loc =
Map VName (Subst StructRetType)
-> [VName]
-> Env
-> Env
-> Loc
-> Either TypeError (Map VName VName)
matchEnvs Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals Env
mod Env
sig Loc
loc
matchMods
Map VName (Subst StructRetType)
old_abs_subst_to_type
[VName]
quals
(ModFun (FunSig TySet
mod_abs Mod
mod_pmod MTy
mod_mod))
(ModFun (FunSig TySet
sig_abs Mod
sig_pmod MTy
sig_mod))
Loc
loc = do
Map VName (QualName VName, TypeBinding)
abs_substs <- TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
mod_abs Mod
mod_pmod TySet
sig_abs Loc
loc
Map VName (QualName VName, TypeBinding)
p_abs_substs <- TySet
-> Mod
-> TySet
-> Loc
-> Either TypeError (Map VName (QualName VName, TypeBinding))
resolveAbsTypes TySet
sig_abs Mod
sig_pmod TySet
mod_abs Loc
loc
let abs_subst_to_type :: Map VName (Subst StructRetType)
abs_subst_to_type =
Map VName (Subst StructRetType)
old_abs_subst_to_type forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
abs_substs
p_abs_subst_to_type :: Map VName (Subst StructRetType)
p_abs_subst_to_type =
Map VName (Subst StructRetType)
old_abs_subst_to_type forall a. Semigroup a => a -> a -> a
<> forall a b k. (a -> b) -> Map k a -> Map k b
M.map (TypeBinding -> Subst StructRetType
substFromAbbr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Map VName (QualName VName, TypeBinding)
p_abs_substs
abs_name_substs :: Map VName VName
abs_name_substs = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall vn. QualName vn -> vn
qualLeaf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Map VName (QualName VName, TypeBinding)
abs_substs
Map VName VName
pmod_substs <- Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
p_abs_subst_to_type [VName]
quals Mod
sig_pmod Mod
mod_pmod Loc
loc
Map VName VName
mod_substs <- Map VName (Subst StructRetType)
-> [VName]
-> MTy
-> MTy
-> Loc
-> Either TypeError (Map VName VName)
matchMTys' Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals MTy
mod_mod MTy
sig_mod Loc
loc
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map VName VName
pmod_substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
mod_substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
abs_name_substs)
matchEnvs ::
M.Map VName (Subst StructRetType) ->
[VName] ->
Env ->
Env ->
Loc ->
Either TypeError (M.Map VName VName)
matchEnvs :: Map VName (Subst StructRetType)
-> [VName]
-> Env
-> Env
-> Loc
-> Either TypeError (Map VName VName)
matchEnvs Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals Env
env Env
sig Loc
loc = do
let visible :: Set VName
visible = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall vn. QualName vn -> vn
qualLeaf forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
M.elems forall a b. (a -> b) -> a -> b
$ Env -> NameMap
envNameMap Env
sig
isVisible :: VName -> Bool
isVisible VName
name = VName
name forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
visible
Map VName VName
abbr_name_substs <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Bool
isVisible forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName TypeBinding
envTypeTable Env
sig) forall a b. (a -> b) -> a -> b
$
\(VName
name, TypeAbbr Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t) ->
case forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName TypeBinding
envTypeTable Namespace
Type (VName -> Name
baseName VName
name) Env
env of
Just (VName
name', TypeAbbr Liftedness
l [TypeParam]
ps StructRetType
t) ->
Loc
-> Map VName (Subst StructRetType)
-> [VName]
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> Either TypeError (VName, VName)
matchTypeAbbr Loc
loc Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals VName
name Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t VName
name' Liftedness
l [TypeParam]
ps StructRetType
t
Maybe (VName, TypeBinding)
Nothing -> forall a b. Pretty a => Loc -> a -> Either TypeError b
missingType Loc
loc forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
name
Map VName VName
val_substs <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName BoundV
envVtable Env
sig) forall a b. (a -> b) -> a -> b
$ \(VName
name, BoundV
spec_bv) -> do
let spec_bv' :: BoundV
spec_bv' = TypeSubs -> BoundV -> BoundV
substituteTypesInBoundV (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
abs_subst_to_type) BoundV
spec_bv
case forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName BoundV
envVtable Namespace
Term (VName -> Name
baseName VName
name) Env
env of
Just (VName
name', BoundV
bv) -> Loc
-> [VName]
-> VName
-> BoundV
-> VName
-> BoundV
-> Either TypeError (VName, VName)
matchVal Loc
loc [VName]
quals VName
name BoundV
spec_bv' VName
name' BoundV
bv
Maybe (VName, BoundV)
_ -> forall a b. Pretty a => Loc -> a -> Either TypeError b
missingVal Loc
loc (VName -> Name
baseName VName
name)
Map VName VName
mod_substs <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Env -> Map VName Mod
envModTable Env
sig) forall a b. (a -> b) -> a -> b
$ \(VName
name, Mod
modspec) ->
case forall v.
(Env -> Map VName v)
-> Namespace -> Name -> Env -> Maybe (VName, v)
findBinding Env -> Map VName Mod
envModTable Namespace
Term (VName -> Name
baseName VName
name) Env
env of
Just (VName
name', Mod
mod) ->
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
name VName
name'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map VName (Subst StructRetType)
-> [VName]
-> Mod
-> Mod
-> Loc
-> Either TypeError (Map VName VName)
matchMods Map VName (Subst StructRetType)
abs_subst_to_type ([VName]
quals forall a. [a] -> [a] -> [a]
++ [VName
name]) Mod
mod Mod
modspec Loc
loc
Maybe (VName, Mod)
Nothing ->
forall a b. Pretty a => Loc -> a -> Either TypeError b
missingMod Loc
loc forall a b. (a -> b) -> a -> b
$ VName -> Name
baseName VName
name
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Map VName VName
val_substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
mod_substs forall a. Semigroup a => a -> a -> a
<> Map VName VName
abbr_name_substs
matchTypeAbbr ::
Loc ->
M.Map VName (Subst StructRetType) ->
[VName] ->
VName ->
Liftedness ->
[TypeParam] ->
StructRetType ->
VName ->
Liftedness ->
[TypeParam] ->
StructRetType ->
Either TypeError (VName, VName)
matchTypeAbbr :: Loc
-> Map VName (Subst StructRetType)
-> [VName]
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> VName
-> Liftedness
-> [TypeParam]
-> StructRetType
-> Either TypeError (VName, VName)
matchTypeAbbr Loc
loc Map VName (Subst StructRetType)
abs_subst_to_type [VName]
quals VName
spec_name Liftedness
spec_l [TypeParam]
spec_ps StructRetType
spec_t VName
name Liftedness
l [TypeParam]
ps StructRetType
t = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
spec_ps forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps) forall a b. (a -> b) -> a -> b
$ forall {b}. StructRetType -> Either TypeError b
nomatch StructRetType
spec_t
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall k a. Ord k => k -> Map k a -> Bool
M.member VName
spec_name Map VName (Subst StructRetType)
abs_subst_to_type) forall a b. (a -> b) -> a -> b
$
case forall a. Set a -> [a]
S.toList (TypeBase Size () -> Set VName
mustBeExplicitInType (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
t)) forall a. Eq a => [a] -> [a] -> [a]
`intersect` forall a b. (a -> b) -> [a] -> [b]
map forall vn. TypeParamBase vn -> vn
typeParamName [TypeParam]
ps of
[] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
VName
d : [VName]
_ ->
forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Type"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall a.
[VName]
-> QualName VName
-> (Liftedness, [TypeParam], StructRetType)
-> Doc a
ppTypeAbbr [] (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
name) (Liftedness
l, [TypeParam]
ps, StructRetType
t))
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"cannot be made abstract because size parameter"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. Text -> Doc a
textwrap Text
"is not used as an array size in the definition."
let spec_t' :: StructRetType
spec_t' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
abs_subst_to_type) StructRetType
spec_t
nonrigid :: [TypeParam]
nonrigid = [TypeParam]
ps forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map (forall vn. vn -> SrcLoc -> TypeParamBase vn
`TypeParamDim` forall a. Monoid a => a
mempty) (forall dim as. RetTypeBase dim as -> [VName]
retDims StructRetType
t)
case Loc
-> [TypeParam]
-> [TypeParam]
-> TypeBase Size ()
-> TypeBase Size ()
-> Either TypeError (TypeBase Size ())
doUnification Loc
loc [TypeParam]
spec_ps [TypeParam]
nonrigid (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
spec_t') (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
t) of
Right TypeBase Size ()
t'
| forall as. TypeBase Size as -> TypeBase () as
noSizes TypeBase Size ()
t' TypeBase () () -> TypeBase () () -> Bool
`subtypeOf` forall as. TypeBase Size as -> TypeBase () as
noSizes (forall dim as. RetTypeBase dim as -> TypeBase dim as
retType StructRetType
spec_t') -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
spec_name, VName
name)
Either TypeError (TypeBase Size ())
_ -> forall {b}. StructRetType -> Either TypeError b
nomatch StructRetType
spec_t'
where
nomatch :: StructRetType -> Either TypeError b
nomatch StructRetType
spec_t' =
forall b.
Loc
-> [VName]
-> [VName]
-> VName
-> (Liftedness, [TypeParam], StructRetType)
-> (Liftedness, [TypeParam], StructRetType)
-> Either TypeError b
mismatchedType
Loc
loc
(forall k a. Map k a -> [k]
M.keys Map VName (Subst StructRetType)
abs_subst_to_type)
[VName]
quals
VName
spec_name
(Liftedness
spec_l, [TypeParam]
spec_ps, StructRetType
spec_t')
(Liftedness
l, [TypeParam]
ps, StructRetType
t)
matchVal ::
Loc ->
[VName] ->
VName ->
BoundV ->
VName ->
BoundV ->
Either TypeError (VName, VName)
matchVal :: Loc
-> [VName]
-> VName
-> BoundV
-> VName
-> BoundV
-> Either TypeError (VName, VName)
matchVal Loc
loc [VName]
quals VName
spec_name BoundV
spec_v VName
name BoundV
v =
case Loc -> BoundV -> BoundV -> Maybe (Maybe (Doc ()))
matchValBinding Loc
loc BoundV
spec_v BoundV
v of
Maybe (Maybe (Doc ()))
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
spec_name, VName
name)
Just Maybe (Doc ())
problem ->
forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$
Loc -> Notes -> Doc () -> TypeError
TypeError Loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
Doc ()
"Module type specifies"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall {a} {ann}. Pretty a => a -> BoundV -> Doc ann
ppValBind (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
spec_name) BoundV
spec_v)
forall ann. Doc ann -> Doc ann -> Doc ann
</> Doc ()
"but module provides"
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall {a} {ann}. Pretty a => a -> BoundV -> Doc ann
ppValBind (forall vn. [vn] -> vn -> QualName vn
QualName [VName]
quals VName
spec_name) BoundV
v)
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall a. a -> Maybe a -> a
fromMaybe forall a. Monoid a => a
mempty Maybe (Doc ())
problem
matchValBinding :: Loc -> BoundV -> BoundV -> Maybe (Maybe (Doc ()))
matchValBinding :: Loc -> BoundV -> BoundV -> Maybe (Maybe (Doc ()))
matchValBinding Loc
loc (BoundV [TypeParam]
spec_tps TypeBase Size ()
orig_spec_t) (BoundV [TypeParam]
tps TypeBase Size ()
orig_t) = do
case Loc
-> [TypeParam]
-> [TypeParam]
-> TypeBase Size ()
-> TypeBase Size ()
-> Either TypeError (TypeBase Size ())
doUnification Loc
loc [TypeParam]
spec_tps [TypeParam]
tps (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
orig_spec_t) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size ()
orig_t) of
Left (TypeError Loc
_ Notes
notes Doc ()
msg) ->
forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Doc ()
msg forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Notes
notes
Right TypeBase Size ()
t
| forall as. TypeBase Size as -> TypeBase () as
noSizes TypeBase Size ()
t TypeBase () () -> TypeBase () () -> Bool
`subtypeOf` forall as. TypeBase Size as -> TypeBase () as
noSizes TypeBase Size ()
orig_spec_t -> forall a. Maybe a
Nothing
| Bool
otherwise -> forall a. a -> Maybe a
Just forall a. Maybe a
Nothing
ppValBind :: a -> BoundV -> Doc ann
ppValBind a
v (BoundV [TypeParam]
tps TypeBase Size ()
t) =
Doc ann
"val"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty a
v
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
tps)
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
colon
forall ann. Doc ann -> Doc ann -> Doc ann
</> forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (forall ann. Doc ann -> Doc ann
align (forall a ann. Pretty a => a -> Doc ann
pretty TypeBase Size ()
t))
applyFunctor ::
Loc ->
FunSig ->
MTy ->
TypeM
( MTy,
M.Map VName VName,
M.Map VName VName
)
applyFunctor :: Loc
-> FunSig -> MTy -> TypeM (MTy, Map VName VName, Map VName VName)
applyFunctor Loc
applyloc (FunSig TySet
p_abs Mod
p_mod MTy
body_mty) MTy
a_mty = do
Map VName VName
p_subst <- forall a. Either TypeError a -> TypeM a
badOnLeft forall a b. (a -> b) -> a -> b
$ MTy -> MTy -> Loc -> Either TypeError (Map VName VName)
matchMTys MTy
a_mty (TySet -> Mod -> MTy
MTy TySet
p_abs Mod
p_mod) Loc
applyloc
let a_abbrs :: Map VName TypeBinding
a_abbrs = MTy -> Map VName TypeBinding
mtyTypeAbbrs MTy
a_mty
isSub :: TypeSubs
isSub VName
v = case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Map VName TypeBinding
a_abbrs of
Just TypeBinding
abbr -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ TypeBinding -> Subst StructRetType
substFromAbbr TypeBinding
abbr
Maybe TypeBinding
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
v
type_subst :: Map VName (Subst StructRetType)
type_subst = forall a b k. (a -> Maybe b) -> Map k a -> Map k b
M.mapMaybe TypeSubs
isSub Map VName VName
p_subst
body_mty' :: MTy
body_mty' = TypeSubs -> MTy -> MTy
substituteTypesInMTy (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst StructRetType)
type_subst) MTy
body_mty
(MTy
body_mty'', Map VName VName
body_subst) <- MTy -> TypeM (MTy, Map VName VName)
newNamesForMTy MTy
body_mty'
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MTy
body_mty'', Map VName VName
p_subst, Map VName VName
body_subst)