{-# Language BlockArguments, ImplicitParams #-}
module Cryptol.TypeCheck.Module (doFunctorInst) where
import Data.List(partition)
import Data.Text(Text)
import Data.Map(Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Control.Monad(unless,forM_)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Ident(Ident,Namespace(..),isInfixIdent)
import Cryptol.Parser.Position (Range,Located(..), thing)
import qualified Cryptol.Parser.AST as P
import Cryptol.ModuleSystem.Name(nameIdent)
import Cryptol.ModuleSystem.Interface
( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..)
, filterIfaceDecls
)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Subst(Subst,listParamSubst,apSubst,mergeDistinctSubst)
import Cryptol.TypeCheck.Solve(proveImplication)
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Instantiate(instantiateWith)
import Cryptol.TypeCheck.ModuleInstance
import Cryptol.TypeCheck.ModuleBacktickInstance(MBQual, doBacktickInstance)
doFunctorInst ::
Located (P.ImpName Name) ->
Located (P.ImpName Name) ->
P.ModuleInstanceArgs Name ->
Map Name Name
->
Maybe Text ->
InferM (Maybe TCTopEntity)
doFunctorInst :: Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> Map Name Name
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst Located (ImpName Name)
m Located (ImpName Name)
f ModuleInstanceArgs Name
as Map Name Name
inst Maybe Text
doc =
Range -> InferM (Maybe TCTopEntity) -> InferM (Maybe TCTopEntity)
forall a. Range -> InferM a -> InferM a
inRange (Located (ImpName Name) -> Range
forall a. Located a -> Range
srcRange Located (ImpName Name)
m)
do ModuleG ()
mf <- ImpName Name -> InferM (ModuleG ())
lookupFunctor (Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
f)
[(Range, ModParam, ActualArg)]
argIs <- Range
-> ModuleG ()
-> ModuleInstanceArgs Name
-> InferM [(Range, ModParam, ActualArg)]
checkArity (Located (ImpName Name) -> Range
forall a. Located a -> Range
srcRange Located (ImpName Name)
f) ModuleG ()
mf ModuleInstanceArgs Name
as
ModuleG (Located (ImpName Name))
m2 <- do [ArgInst]
as2 <- ((Range, ModParam, ActualArg) -> InferM ArgInst)
-> [(Range, ModParam, ActualArg)] -> InferM [ArgInst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg [(Range, ModParam, ActualArg)]
argIs
let ([Subst]
tySus,[[Decl]]
decls) = [(Subst, [Decl])] -> ([Subst], [[Decl]])
forall a b. [(a, b)] -> ([a], [b])
unzip [ (Subst
su,[Decl]
ds) | DefinedInst Subst
su [Decl]
ds <- [ArgInst]
as2 ]
let ?tSu = [Subst] -> Subst
mergeDistinctSubst [Subst]
tySus
?vSu = ?vSu::Map Name Name
Map Name Name
inst
let m1 :: ModuleG ()
m1 = ModuleG () -> ModuleG ()
forall t.
(ModuleInstance t, (?tSu::Subst, ?vSu::Map Name Name)) =>
t -> t
moduleInstance ModuleG ()
mf
m2 :: ModuleG (Located (ImpName Name))
m2 = ModuleG ()
m1 { mName :: Located (ImpName Name)
mName = Located (ImpName Name)
m
, mDoc :: Maybe Text
mDoc = Maybe Text
forall a. Maybe a
Nothing
, mParamTypes :: Map Name ModTParam
mParamTypes = Map Name ModTParam
forall a. Monoid a => a
mempty
, mParamFuns :: Map Name ModVParam
mParamFuns = Map Name ModVParam
forall a. Monoid a => a
mempty
, mParamConstraints :: [Located Prop]
mParamConstraints = [Located Prop]
forall a. Monoid a => a
mempty
, mParams :: FunctorParams
mParams = FunctorParams
forall a. Monoid a => a
mempty
, mDecls :: [DeclGroup]
mDecls = (Decl -> DeclGroup) -> [Decl] -> [DeclGroup]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> DeclGroup
NonRecursive ([[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl]]
decls) [DeclGroup] -> [DeclGroup] -> [DeclGroup]
forall a. [a] -> [a] -> [a]
++
ModuleG () -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ()
m1
}
let ([Set (MBQual TParam)]
tps,[[Prop]]
tcs,[Map (MBQual Name) Prop]
vps) =
[(Set (MBQual TParam), [Prop], Map (MBQual Name) Prop)]
-> ([Set (MBQual TParam)], [[Prop]], [Map (MBQual Name) Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [ (Set (MBQual TParam)
xs,[Prop]
cs,Map (MBQual Name) Prop
fs) | ParamInst Set (MBQual TParam)
xs [Prop]
cs Map (MBQual Name) Prop
fs <- [ArgInst]
as2 ]
tpSet :: Set (MBQual TParam)
tpSet = [Set (MBQual TParam)] -> Set (MBQual TParam)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set (MBQual TParam)]
tps
tpSet' :: Set TParam
tpSet' = (MBQual TParam -> TParam) -> Set (MBQual TParam) -> Set TParam
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map MBQual TParam -> TParam
forall a b. (a, b) -> b
snd ([Set (MBQual TParam)] -> Set (MBQual TParam)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set (MBQual TParam)]
tps)
emit :: Located t -> Bool
emit Located t
p = Set TParam -> Bool
forall a. Set a -> Bool
Set.null (t -> Set TParam
forall t. FVS t => t -> Set TParam
freeParams (Located t -> t
forall a. Located a -> a
thing Located t
p)
Set TParam -> Set TParam -> Set TParam
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set TParam
tpSet')
([Located Prop]
emitPs,[Located Prop]
delayPs) = (Located Prop -> Bool)
-> [Located Prop] -> ([Located Prop], [Located Prop])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Located Prop -> Bool
forall {t}. FVS t => Located t -> Bool
emit (ModuleG () -> [Located Prop]
forall mname. ModuleG mname -> [Located Prop]
mParamConstraints ModuleG ()
m1)
[Located Prop] -> (Located Prop -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Located Prop]
emitPs \Located Prop
lp ->
ConstraintSource -> [Prop] -> InferM ()
newGoals (Range -> ConstraintSource
CtModuleInstance (Located Prop -> Range
forall a. Located a -> Range
srcRange Located Prop
lp)) [Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
lp]
Set (MBQual TParam)
-> [Prop]
-> Map (MBQual Name) Prop
-> ModuleG (Located (ImpName Name))
-> InferM (ModuleG (Located (ImpName Name)))
doBacktickInstance Set (MBQual TParam)
tpSet
((Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing [Located Prop]
delayPs [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Prop]]
tcs)
([Map (MBQual Name) Prop] -> Map (MBQual Name) Prop
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Map (MBQual Name) Prop]
vps)
ModuleG (Located (ImpName Name))
m2
case Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m of
P.ImpTop ModName
mn -> ModName -> ExportSpec Name -> InferM ()
newModuleScope ModName
mn (ModuleG (Located (ImpName Name)) -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG (Located (ImpName Name))
m2)
P.ImpNested Name
mn -> Name -> Maybe Text -> ExportSpec Name -> InferM ()
newSubmoduleScope Name
mn Maybe Text
doc (ModuleG (Located (ImpName Name)) -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG (Located (ImpName Name))
m2)
(TySyn -> InferM ()) -> [TySyn] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TySyn -> InferM ()
addTySyn (Map Name TySyn -> [TySyn]
forall k a. Map k a -> [a]
Map.elems (ModuleG (Located (ImpName Name)) -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG (Located (ImpName Name))
m2))
(Newtype -> InferM ()) -> [Newtype] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Newtype -> InferM ()
addNewtype (Map Name Newtype -> [Newtype]
forall k a. Map k a -> [a]
Map.elems (ModuleG (Located (ImpName Name)) -> Map Name Newtype
forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG (Located (ImpName Name))
m2))
(AbstractType -> InferM ()) -> [AbstractType] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ AbstractType -> InferM ()
addPrimType (Map Name AbstractType -> [AbstractType]
forall k a. Map k a -> [a]
Map.elems (ModuleG (Located (ImpName Name)) -> Map Name AbstractType
forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG (Located (ImpName Name))
m2))
Map Name ModParamNames -> InferM ()
addSignatures (ModuleG (Located (ImpName Name)) -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG (Located (ImpName Name))
m2)
Map Name (IfaceNames Name) -> InferM ()
addSubmodules (ModuleG (Located (ImpName Name)) -> Map Name (IfaceNames Name)
forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG (Located (ImpName Name))
m2)
Map Name (ModuleG Name) -> InferM ()
addFunctors (ModuleG (Located (ImpName Name)) -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG (Located (ImpName Name))
m2)
(DeclGroup -> InferM ()) -> [DeclGroup] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DeclGroup -> InferM ()
addDecls (ModuleG (Located (ImpName Name)) -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG (Located (ImpName Name))
m2)
case Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m of
P.ImpTop {} -> TCTopEntity -> Maybe TCTopEntity
forall a. a -> Maybe a
Just (TCTopEntity -> Maybe TCTopEntity)
-> InferM TCTopEntity -> InferM (Maybe TCTopEntity)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM TCTopEntity
endModule
P.ImpNested {} -> InferM ()
endSubmodule InferM ()
-> InferM (Maybe TCTopEntity) -> InferM (Maybe TCTopEntity)
forall a b. InferM a -> InferM b -> InferM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe TCTopEntity -> InferM (Maybe TCTopEntity)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TCTopEntity
forall a. Maybe a
Nothing
data ActualArg =
UseParameter ModParam
| UseModule (IfaceG ())
| AddDeclParams
checkArity ::
Range ->
ModuleG () ->
P.ModuleInstanceArgs Name ->
InferM [(Range, ModParam, ActualArg)]
checkArity :: Range
-> ModuleG ()
-> ModuleInstanceArgs Name
-> InferM [(Range, ModParam, ActualArg)]
checkArity Range
r ModuleG ()
mf ModuleInstanceArgs Name
args =
case ModuleInstanceArgs Name
args of
P.DefaultInstArg Located (ModuleInstanceArg Name)
arg ->
let i :: Located Ident
i = Located { srcRange :: Range
srcRange = Located (ModuleInstanceArg Name) -> Range
forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
arg
, thing :: Ident
thing = [Ident] -> Ident
forall a. HasCallStack => [a] -> a
head (FunctorParams -> [Ident]
forall k a. Map k a -> [k]
Map.keys FunctorParams
ps0)
}
in [(Range, ModParam, ActualArg)]
-> FunctorParams
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, ModParam, ActualArg)]
forall {a}.
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [] FunctorParams
ps0 [ Located Ident
-> Located (ModuleInstanceArg Name) -> ModuleInstanceNamedArg Name
forall name.
Located Ident
-> Located (ModuleInstanceArg name) -> ModuleInstanceNamedArg name
P.ModuleInstanceNamedArg Located Ident
i Located (ModuleInstanceArg Name)
arg ]
P.NamedInstArgs [ModuleInstanceNamedArg Name]
as -> [(Range, ModParam, ActualArg)]
-> FunctorParams
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, ModParam, ActualArg)]
forall {a}.
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [] FunctorParams
ps0 [ModuleInstanceNamedArg Name]
as
P.DefaultInstAnonArg {} -> String -> [String] -> InferM [(Range, ModParam, ActualArg)]
forall a. HasCallStack => String -> [String] -> a
panic String
"checkArity" [ String
"DefaultInstAnonArg" ]
where
ps0 :: FunctorParams
ps0 = ModuleG () -> FunctorParams
forall mname. ModuleG mname -> FunctorParams
mParams ModuleG ()
mf
checkArgs :: [(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [(Range, a, ActualArg)]
done Map Ident a
ps [ModuleInstanceNamedArg Name]
as =
case [ModuleInstanceNamedArg Name]
as of
[] -> do [Ident] -> (Ident -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Ident a -> [Ident]
forall k a. Map k a -> [k]
Map.keys Map Ident a
ps) \Ident
p ->
Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Ident -> Error
FunctorInstanceMissingArgument Ident
p)
[(Range, a, ActualArg)] -> InferM [(Range, a, ActualArg)]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Range, a, ActualArg)]
done
P.ModuleInstanceNamedArg Located Ident
ll Located (ModuleInstanceArg Name)
lm : [ModuleInstanceNamedArg Name]
more ->
case Ident -> Map Ident a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
ll) Map Ident a
ps of
Just a
i ->
do Maybe ActualArg
arg <- case Located (ModuleInstanceArg Name) -> ModuleInstanceArg Name
forall a. Located a -> a
thing Located (ModuleInstanceArg Name)
lm of
P.ModuleArg ImpName Name
m -> ActualArg -> Maybe ActualArg
forall a. a -> Maybe a
Just (ActualArg -> Maybe ActualArg)
-> (IfaceG () -> ActualArg) -> IfaceG () -> Maybe ActualArg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IfaceG () -> ActualArg
UseModule (IfaceG () -> Maybe ActualArg)
-> InferM (IfaceG ()) -> InferM (Maybe ActualArg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImpName Name -> InferM (IfaceG ())
lookupModule ImpName Name
m
P.ParameterArg Ident
p ->
do Maybe ModParam
mb <- Ident -> InferM (Maybe ModParam)
lookupModParam Ident
p
case Maybe ModParam
mb of
Maybe ModParam
Nothing ->
do Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Located (ModuleInstanceArg Name) -> Range
forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
lm)
(Error -> InferM ()
recordError (Ident -> Error
MissingModParam Ident
p))
Maybe ActualArg -> InferM (Maybe ActualArg)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ActualArg
forall a. Maybe a
Nothing
Just ModParam
a -> Maybe ActualArg -> InferM (Maybe ActualArg)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ActualArg -> Maybe ActualArg
forall a. a -> Maybe a
Just (ModParam -> ActualArg
UseParameter ModParam
a))
ModuleInstanceArg Name
P.AddParams -> Maybe ActualArg -> InferM (Maybe ActualArg)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ActualArg -> Maybe ActualArg
forall a. a -> Maybe a
Just ActualArg
AddDeclParams)
let next :: [(Range, a, ActualArg)]
next = case Maybe ActualArg
arg of
Maybe ActualArg
Nothing -> [(Range, a, ActualArg)]
done
Just ActualArg
a -> (Located (ModuleInstanceArg Name) -> Range
forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
lm, a
i, ActualArg
a) (Range, a, ActualArg)
-> [(Range, a, ActualArg)] -> [(Range, a, ActualArg)]
forall a. a -> [a] -> [a]
: [(Range, a, ActualArg)]
done
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [(Range, a, ActualArg)]
next (Ident -> Map Ident a -> Map Ident a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
ll) Map Ident a
ps) [ModuleInstanceNamedArg Name]
more
Maybe a
Nothing ->
do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just (Located Ident -> Range
forall a. Located a -> Range
srcRange Located Ident
ll))
(Ident -> Error
FunctorInstanceBadArgument (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
ll))
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [(Range, a, ActualArg)]
done Map Ident a
ps [ModuleInstanceNamedArg Name]
more
data ArgInst = DefinedInst Subst [Decl]
| ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type)
checkArg ::
(Range, ModParam, ActualArg) -> InferM ArgInst
checkArg :: (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg (Range
r,ModParam
expect,ActualArg
actual') =
case ActualArg
actual' of
ActualArg
AddDeclParams -> InferM ArgInst
paramInst
UseParameter {} -> InferM ArgInst
definedInst
UseModule {} -> InferM ArgInst
definedInst
where
paramInst :: InferM ArgInst
paramInst =
do let as :: Set (MBQual TParam)
as = [MBQual TParam] -> Set (MBQual TParam)
forall a. Ord a => [a] -> Set a
Set.fromList
((ModTParam -> MBQual TParam) -> [ModTParam] -> [MBQual TParam]
forall a b. (a -> b) -> [a] -> [b]
map (TParam -> MBQual TParam
forall {b}. b -> (Maybe ModName, b)
qual (TParam -> MBQual TParam)
-> (ModTParam -> TParam) -> ModTParam -> MBQual TParam
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModTParam -> TParam
mtpParam) (Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
params)))
cs :: [Prop]
cs = (Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing (ModParamNames -> [Located Prop]
mpnConstraints ModParamNames
params)
check :: ModVParam -> InferM (Maybe Prop)
check = Range -> Ident -> ModVParam -> InferM (Maybe Prop)
checkSimpleParameterValue Range
r (ModParam -> Ident
mpName ModParam
expect)
qual :: b -> (Maybe ModName, b)
qual b
a = (ModParam -> Maybe ModName
mpQual ModParam
expect, b
a)
Map Name Prop
fs <- (Name -> Maybe Prop -> Maybe Prop)
-> Map Name (Maybe Prop) -> Map Name Prop
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybeWithKey (\Name
_ Maybe Prop
v -> Maybe Prop
v) (Map Name (Maybe Prop) -> Map Name Prop)
-> InferM (Map Name (Maybe Prop)) -> InferM (Map Name Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModVParam -> InferM (Maybe Prop))
-> Map Name ModVParam -> InferM (Map Name (Maybe Prop))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Name a -> m (Map Name b)
mapM ModVParam -> InferM (Maybe Prop)
check (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
params)
ArgInst -> InferM ArgInst
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (MBQual TParam) -> [Prop] -> Map (MBQual Name) Prop -> ArgInst
ParamInst Set (MBQual TParam)
as [Prop]
cs ((Name -> MBQual Name) -> Map Name Prop -> Map (MBQual Name) Prop
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Name -> MBQual Name
forall {b}. b -> (Maybe ModName, b)
qual Map Name Prop
fs))
definedInst :: InferM ArgInst
definedInst =
do [[(TParam, Prop)]]
tRens <- ((Name, ModTParam) -> InferM [(TParam, Prop)])
-> [(Name, ModTParam)] -> InferM [[(TParam, Prop)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM [(TParam, Prop)]
checkParamType Range
r Map Ident (Kind, Prop)
tyMap) (Map Name ModTParam -> [(Name, ModTParam)]
forall k a. Map k a -> [(k, a)]
Map.toList (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
params))
let renSu :: Subst
renSu = [(TParam, Prop)] -> Subst
listParamSubst ([[(TParam, Prop)]] -> [(TParam, Prop)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(TParam, Prop)]]
tRens)
[Decl]
vDecls <- [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Decl]] -> [Decl]) -> InferM [[Decl]] -> InferM [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(ModVParam -> InferM [Decl]) -> [ModVParam] -> InferM [[Decl]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Range -> Map Ident (Name, Schema) -> ModVParam -> InferM [Decl]
checkParamValue Range
r Map Ident (Name, Schema)
vMap)
[ ModVParam
s { mvpType :: Schema
mvpType = Subst -> Schema -> Schema
forall t. TVars t => Subst -> t -> t
apSubst Subst
renSu (ModVParam -> Schema
mvpType ModVParam
s) }
| ModVParam
s <- Map Name ModVParam -> [ModVParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
params) ]
ArgInst -> InferM ArgInst
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst -> [Decl] -> ArgInst
DefinedInst Subst
renSu [Decl]
vDecls)
params :: ModParamNames
params = ModParam -> ModParamNames
mpParameters ModParam
expect
tyMap :: Map Ident (Kind, Type)
vMap :: Map Ident (Name, Schema)
(Map Ident (Kind, Prop)
tyMap,Map Ident (Name, Schema)
vMap) =
case ActualArg
actual' of
UseParameter ModParam
mp ->
( (ModTParam -> (Kind, Prop))
-> Map Name ModTParam -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap ModTParam -> (Kind, Prop)
fromTP (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ps)
, (ModVParam -> (Name, Schema))
-> Map Name ModVParam -> Map Ident (Name, Schema)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap ModVParam -> (Name, Schema)
fromVP (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
ps)
)
where
ps :: ModParamNames
ps = ModParam -> ModParamNames
mpParameters ModParam
mp
fromTP :: ModTParam -> (Kind, Prop)
fromTP ModTParam
tp = (ModTParam -> Kind
mtpKind ModTParam
tp, TVar -> Prop
TVar (TParam -> TVar
TVBound (ModTParam -> TParam
mtpParam ModTParam
tp)))
fromVP :: ModVParam -> (Name, Schema)
fromVP ModVParam
vp = (ModVParam -> Name
mvpName ModVParam
vp, ModVParam -> Schema
mvpType ModVParam
vp)
UseModule IfaceG ()
actual ->
( [Map Ident (Kind, Prop)] -> Map Ident (Kind, Prop)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [ (TySyn -> (Kind, Prop)) -> Map Name TySyn -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap TySyn -> (Kind, Prop)
fromTS (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
decls)
, (Newtype -> (Kind, Prop))
-> Map Name Newtype -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap Newtype -> (Kind, Prop)
fromNewtype (IfaceDecls -> Map Name Newtype
ifNewtypes IfaceDecls
decls)
, (AbstractType -> (Kind, Prop))
-> Map Name AbstractType -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap AbstractType -> (Kind, Prop)
fromPrimT (IfaceDecls -> Map Name AbstractType
ifAbstractTypes IfaceDecls
decls)
]
, (IfaceDecl -> (Name, Schema))
-> Map Name IfaceDecl -> Map Ident (Name, Schema)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap IfaceDecl -> (Name, Schema)
fromD (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
decls)
)
where
localNames :: Set Name
localNames = IfaceNames () -> Set Name
forall name. IfaceNames name -> Set Name
ifsPublic (IfaceG () -> IfaceNames ()
forall name. IfaceG name -> IfaceNames name
ifNames IfaceG ()
actual)
isLocal :: Name -> Bool
isLocal Name
x = Name
x Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
localNames
decls :: IfaceDecls
decls = (Name -> Bool) -> IfaceDecls -> IfaceDecls
filterIfaceDecls Name -> Bool
isLocal (IfaceG () -> IfaceDecls
forall name. IfaceG name -> IfaceDecls
ifDefines IfaceG ()
actual)
fromD :: IfaceDecl -> (Name, Schema)
fromD IfaceDecl
d = (IfaceDecl -> Name
ifDeclName IfaceDecl
d, IfaceDecl -> Schema
ifDeclSig IfaceDecl
d)
fromTS :: TySyn -> (Kind, Prop)
fromTS TySyn
ts = (TySyn -> Kind
forall t. HasKind t => t -> Kind
kindOf TySyn
ts, TySyn -> Prop
tsDef TySyn
ts)
fromNewtype :: Newtype -> (Kind, Prop)
fromNewtype Newtype
nt = (Newtype -> Kind
forall t. HasKind t => t -> Kind
kindOf Newtype
nt, Newtype -> [Prop] -> Prop
TNewtype Newtype
nt [])
fromPrimT :: AbstractType -> (Kind, Prop)
fromPrimT AbstractType
pt = (AbstractType -> Kind
forall t. HasKind t => t -> Kind
kindOf AbstractType
pt, TCon -> [Prop] -> Prop
TCon (AbstractType -> TCon
abstractTypeTC AbstractType
pt) [])
ActualArg
AddDeclParams -> String
-> [String] -> (Map Ident (Kind, Prop), Map Ident (Name, Schema))
forall a. HasCallStack => String -> [String] -> a
panic String
"checkArg" [String
"AddDeclParams"]
nameMapToIdentMap :: (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap :: forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap a -> b
f Map Name a
m =
[(Ident, b)] -> Map Ident b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name -> Ident
nameIdent Name
n, a -> b
f a
v) | (Name
n,a
v) <- Map Name a -> [(Name, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name a
m ]
checkParamType ::
Range ->
Map Ident (Kind,Type) ->
(Name,ModTParam) ->
InferM [(TParam,Type)]
checkParamType :: Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM [(TParam, Prop)]
checkParamType Range
r Map Ident (Kind, Prop)
tyMap (Name
name,ModTParam
mp) =
let i :: Ident
i = Name -> Ident
nameIdent Name
name
expectK :: Kind
expectK = ModTParam -> Kind
mtpKind ModTParam
mp
in
case Ident -> Map Ident (Kind, Prop) -> Maybe (Kind, Prop)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i Map Ident (Kind, Prop)
tyMap of
Maybe (Kind, Prop)
Nothing ->
do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Namespace -> Ident -> Error
FunctorInstanceMissingName Namespace
NSType Ident
i)
[(TParam, Prop)] -> InferM [(TParam, Prop)]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just (Kind
actualK,Prop
actualT) ->
do Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
expectK Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
actualK)
(Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r)
(Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch (TypeSource -> Maybe TypeSource
forall a. a -> Maybe a
Just (Name -> TypeSource
TVFromModParam Name
name))
Kind
expectK Kind
actualK))
[(TParam, Prop)] -> InferM [(TParam, Prop)]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(ModTParam -> TParam
mtpParam ModTParam
mp, Prop
actualT)]
checkParamValue ::
Range ->
Map Ident (Name,Schema) ->
ModVParam ->
InferM [Decl]
checkParamValue :: Range -> Map Ident (Name, Schema) -> ModVParam -> InferM [Decl]
checkParamValue Range
r Map Ident (Name, Schema)
vMap ModVParam
mp =
let name :: Name
name = ModVParam -> Name
mvpName ModVParam
mp
i :: Ident
i = Name -> Ident
nameIdent Name
name
expectT :: Schema
expectT = ModVParam -> Schema
mvpType ModVParam
mp
in case Ident -> Map Ident (Name, Schema) -> Maybe (Name, Schema)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i Map Ident (Name, Schema)
vMap of
Maybe (Name, Schema)
Nothing ->
do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Namespace -> Ident -> Error
FunctorInstanceMissingName Namespace
NSValue Ident
i)
[Decl] -> InferM [Decl]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just (Name, Schema)
actual ->
do Expr
e <- Range -> (Name, Schema) -> (Name, Schema) -> InferM Expr
mkParamDef Range
r (Name
name,Schema
expectT) (Name, Schema)
actual
let d :: Decl
d = Decl { dName :: Name
dName = Name
name
, dSignature :: Schema
dSignature = Schema
expectT
, dDefinition :: DeclDef
dDefinition = Expr -> DeclDef
DExpr Expr
e
, dPragmas :: [Pragma]
dPragmas = []
, dInfix :: Bool
dInfix = Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
name)
, dFixity :: Maybe Fixity
dFixity = ModVParam -> Maybe Fixity
mvpFixity ModVParam
mp
, dDoc :: Maybe Text
dDoc = ModVParam -> Maybe Text
mvpDoc ModVParam
mp
}
[Decl] -> InferM [Decl]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Decl
d]
checkSimpleParameterValue ::
Range ->
Ident ->
ModVParam ->
InferM (Maybe Type)
checkSimpleParameterValue :: Range -> Ident -> ModVParam -> InferM (Maybe Prop)
checkSimpleParameterValue Range
r Ident
i ModVParam
mp =
case (Schema -> [TParam]
sVars Schema
sch, Schema -> [Prop]
sProps Schema
sch) of
([],[]) -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> Maybe Prop
forall a. a -> Maybe a
Just (Schema -> Prop
sType Schema
sch))
([TParam], [Prop])
_ ->
do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r)
(BadBacktickInstance -> Error
FunctorInstanceBadBacktick
(Ident -> Ident -> BadBacktickInstance
BIPolymorphicArgument Ident
i (Name -> Ident
nameIdent (ModVParam -> Name
mvpName ModVParam
mp))))
Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Prop
forall a. Maybe a
Nothing
where
sch :: Schema
sch = ModVParam -> Schema
mvpType ModVParam
mp
mkParamDef ::
Range ->
(Name,Schema) ->
(Name,Schema) ->
InferM Expr
mkParamDef :: Range -> (Name, Schema) -> (Name, Schema) -> InferM Expr
mkParamDef Range
r (Name
pname,Schema
wantedS) (Name
arg,Schema
actualS) =
do (Expr
e,[Goal]
todo) <- InferM Expr -> InferM (Expr, [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
(InferM Expr -> InferM (Expr, [Goal]))
-> InferM Expr -> InferM (Expr, [Goal])
forall a b. (a -> b) -> a -> b
$ [TParam] -> InferM Expr -> InferM Expr
forall a. [TParam] -> InferM a -> InferM a
withTParams (Schema -> [TParam]
sVars Schema
wantedS)
do (Expr
e,Prop
t) <- Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
pname(Name -> Expr
EVar Name
arg) Schema
actualS []
[Prop]
props <- TypeWithSource -> Prop -> InferM [Prop]
unify WithSource { twsType :: Prop
twsType = Schema -> Prop
sType Schema
wantedS
, twsSource :: TypeSource
twsSource = Name -> TypeSource
TVFromModParam Name
arg
, twsRange :: Maybe Range
twsRange = Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r
}
Prop
t
ConstraintSource -> [Prop] -> InferM ()
newGoals (Range -> ConstraintSource
CtModuleInstance Range
r) [Prop]
props
Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e
Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
False
(Name -> Maybe Name
forall a. a -> Maybe a
Just Name
pname)
(Schema -> [TParam]
sVars Schema
wantedS)
(Schema -> [Prop]
sProps Schema
wantedS)
[Goal]
todo
let res :: Expr
res = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs Expr
res1 (Schema -> [TParam]
sVars Schema
wantedS)
res1 :: Expr
res1 = (Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e) (Schema -> [Prop]
sProps Schema
wantedS)
Expr -> InferM Expr
forall t. TVars t => t -> InferM t
applySubst Expr
res