{-# Language BlockArguments, ImplicitParams #-}
module Cryptol.TypeCheck.Module (doFunctorInst) where
import Data.List(partition,unzip4)
import Data.Text(Text)
import Data.Map(Map)
import qualified Data.Map as Map
import qualified Data.Map.Merge.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Control.Monad(unless,forM_,mapAndUnzipM)
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Ident(Ident,Namespace(..),ModPath,isInfixIdent)
import Cryptol.Parser.Position (Range,Located(..), thing)
import qualified Cryptol.Parser.AST as P
import Cryptol.ModuleSystem.Binds(newFunctorInst)
import Cryptol.ModuleSystem.Name(nameIdent)
import Cryptol.ModuleSystem.NamingEnv
(NamingEnv(..), modParamNamingEnv, shadowing, without)
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
->
NamingEnv
->
Maybe Text ->
InferM (Maybe TCTopEntity)
doFunctorInst :: Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> Map Name Name
-> NamingEnv
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst Located (ImpName Name)
m Located (ImpName Name)
f ModuleInstanceArgs Name
as Map Name Name
instMap0 NamingEnv
enclosingInScope 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 let mpath :: ModPath
mpath = ImpName Name -> ModPath
P.impNameModPath (Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m)
[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 (ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg ModPath
mpath) [(Range, ModParam, ActualArg)]
argIs
let ([Subst]
tySus,[Map Name TySyn]
paramTySyns,[[Decl]]
decls,[Map Name Name]
paramInstMaps) =
[(Subst, Map Name TySyn, [Decl], Map Name Name)]
-> ([Subst], [Map Name TySyn], [[Decl]], [Map Name Name])
forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 [ (Subst
su,Map Name TySyn
ts,[Decl]
ds,Map Name Name
im) | DefinedInst Subst
su Map Name TySyn
ts [Decl]
ds Map Name Name
im <- [ArgInst]
as2 ]
Map Name Name
instMap <- ModPath -> ModuleG () -> Map Name Name -> InferM (Map Name Name)
addMissingTySyns ModPath
mpath ModuleG ()
mf Map Name Name
instMap0
let ?tVarSu = [Subst] -> Subst
mergeDistinctSubst [Subst]
tySus
?nameSu = Map Name Name
instMap Map Name Name -> Map Name Name -> Map Name Name
forall a. Semigroup a => a -> a -> a
<> [Map Name Name] -> Map Name Name
forall a. Monoid a => [a] -> a
mconcat [Map Name Name]
paramInstMaps
let m1 :: ModuleG ()
m1 = ModuleG () -> ModuleG ()
forall t.
(ModuleInstance t, (?tVarSu::Subst, ?nameSu::Map Name Name)) =>
t -> t
moduleInstance ModuleG ()
mf
m2 :: ModuleG (Located (ImpName Name))
m2 = ModuleG ()
m1 { mName = m
, mDoc = Nothing
, mParamTypes = mempty
, mParamFuns = mempty
, mParamConstraints = mempty
, mParams = mempty
, mTySyns = mconcat paramTySyns <> mTySyns m1
, mDecls = map NonRecursive (concat decls) ++
mDecls 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
let inScope0 :: NamingEnv
inScope0 = ModuleG (Located (ImpName Name)) -> NamingEnv
forall mname. ModuleG mname -> NamingEnv
mInScope ModuleG (Located (ImpName Name))
m2 NamingEnv -> NamingEnv -> NamingEnv
`without`
[NamingEnv] -> NamingEnv
forall a. Monoid a => [a] -> a
mconcat [ ModParam -> NamingEnv
modParamNamingEnv ModParam
mp | (Range
_, ModParam
mp, ActualArg
AddDeclParams) <- [(Range, ModParam, ActualArg)]
argIs ]
inScope :: NamingEnv
inScope = NamingEnv
inScope0 NamingEnv -> NamingEnv -> NamingEnv
`shadowing` NamingEnv
enclosingInScope
case Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m of
P.ImpTop ModName
mn -> ModName -> ExportSpec Name -> NamingEnv -> InferM ()
newModuleScope ModName
mn (ModuleG (Located (ImpName Name)) -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG (Located (ImpName Name))
m2) NamingEnv
inScope
P.ImpNested Name
mn -> Name -> Maybe Text -> ExportSpec Name -> NamingEnv -> 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) NamingEnv
inScope
(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))
(NominalType -> InferM ()) -> [NominalType] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ NominalType -> InferM ()
addNominal (Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (ModuleG (Located (ImpName Name)) -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes 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
(Map Name TySyn)
[Decl]
(Map Name Name)
| ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type)
checkArg ::
ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg :: ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg ModPath
mpath (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, [Map Name TySyn]
tSyns, [Map Name Name]
tInstMaps) <- [([(TParam, Prop)], Map Name TySyn, Map Name Name)]
-> ([[(TParam, Prop)]], [Map Name TySyn], [Map Name Name])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([(TParam, Prop)], Map Name TySyn, Map Name Name)]
-> ([[(TParam, Prop)]], [Map Name TySyn], [Map Name Name]))
-> InferM [([(TParam, Prop)], Map Name TySyn, Map Name Name)]
-> InferM ([[(TParam, Prop)]], [Map Name TySyn], [Map Name Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
((Name, ModTParam)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name))
-> [(Name, ModTParam)]
-> InferM [([(TParam, Prop)], Map Name TySyn, Map Name Name)]
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 (ModPath
-> Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
checkParamType ModPath
mpath 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, [Map Name Name]
vInstMaps) <-
(ModVParam -> InferM ([Decl], Map Name Name))
-> [ModVParam] -> InferM ([[Decl]], [Map Name Name])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (ModPath
-> Range
-> Map Ident (Name, Schema)
-> ModVParam
-> InferM ([Decl], Map Name Name)
checkParamValue ModPath
mpath Range
r Map Ident (Name, Schema)
vMap)
[ ModVParam
s { mvpType = apSubst renSu (mvpType 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 (ArgInst -> InferM ArgInst) -> ArgInst -> InferM ArgInst
forall a b. (a -> b) -> a -> b
$ Subst -> Map Name TySyn -> [Decl] -> Map Name Name -> ArgInst
DefinedInst Subst
renSu ([Map Name TySyn] -> Map Name TySyn
forall a. Monoid a => [a] -> a
mconcat [Map Name TySyn]
tSyns)
([[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl]]
vDecls) ([Map Name Name] -> Map Name Name
forall a. Monoid a => [a] -> a
mconcat [Map Name Name]
tInstMaps Map Name Name -> Map Name Name -> Map Name Name
forall a. Semigroup a => a -> a -> a
<> [Map Name Name] -> Map Name Name
forall a. Monoid a => [a] -> a
mconcat [Map Name Name]
vInstMaps)
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)
, (NominalType -> (Kind, Prop))
-> Map Name NominalType -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap NominalType -> (Kind, Prop)
fromNominal (IfaceDecls -> Map Name NominalType
ifNominalTypes 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)
fromNominal :: NominalType -> (Kind, Prop)
fromNominal NominalType
nt = (NominalType -> Kind
forall t. HasKind t => t -> Kind
kindOf NominalType
nt, NominalType -> [Prop] -> Prop
TNominal NominalType
nt [])
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 ::
ModPath ->
Range ->
Map Ident (Kind,Type) ->
(Name,ModTParam) ->
InferM ([(TParam,Type)], Map Name TySyn, Map Name Name)
checkParamType :: ModPath
-> Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
checkParamType ModPath
mpath 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)], Map Name TySyn, Map Name Name)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Map Name TySyn
forall k a. Map k a
Map.empty, Map Name Name
forall k a. Map k a
Map.empty)
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))
Name
name' <- ModPath -> Name -> InferM Name
forall (m :: * -> *). FreshM m => ModPath -> Name -> m Name
newFunctorInst ModPath
mpath Name
name
let tySyn :: TySyn
tySyn = TySyn { tsName :: Name
tsName = Name
name'
, tsParams :: [TParam]
tsParams = []
, tsConstraints :: [Prop]
tsConstraints = []
, tsDef :: Prop
tsDef = Prop
actualT
, tsDoc :: Maybe Text
tsDoc = ModTParam -> Maybe Text
mtpDoc ModTParam
mp }
([(TParam, Prop)], Map Name TySyn, Map Name Name)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [(ModTParam -> TParam
mtpParam ModTParam
mp, Prop
actualT)]
, Name -> TySyn -> Map Name TySyn
forall k a. k -> a -> Map k a
Map.singleton Name
name' TySyn
tySyn
, Name -> Name -> Map Name Name
forall k a. k -> a -> Map k a
Map.singleton Name
name Name
name'
)
checkParamValue ::
ModPath ->
Range ->
Map Ident (Name,Schema) ->
ModVParam ->
InferM ([Decl], Map Name Name)
checkParamValue :: ModPath
-> Range
-> Map Ident (Name, Schema)
-> ModVParam
-> InferM ([Decl], Map Name Name)
checkParamValue ModPath
mpath 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], Map Name Name) -> InferM ([Decl], Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Map Name Name
forall k a. Map k a
Map.empty)
Just (Name, Schema)
actual ->
do Expr
e <- Range -> (Name, Schema) -> (Name, Schema) -> InferM Expr
mkParamDef Range
r (Name
name,Schema
expectT) (Name, Schema)
actual
Name
name' <- ModPath -> Name -> InferM Name
forall (m :: * -> *). FreshM m => ModPath -> Name -> m Name
newFunctorInst ModPath
mpath Name
name
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], Map Name Name) -> InferM ([Decl], Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Decl
d], Name -> Name -> Map Name Name
forall k a. k -> a -> Map k a
Map.singleton Name
name Name
name')
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
addMissingTySyns ::
ModPath ->
ModuleG () ->
Map Name Name ->
InferM (Map Name Name)
addMissingTySyns :: ModPath -> ModuleG () -> Map Name Name -> InferM (Map Name Name)
addMissingTySyns ModPath
mpath ModuleG ()
f = WhenMissing InferM Name TySyn Name
-> WhenMissing InferM Name Name Name
-> WhenMatched InferM Name TySyn Name Name
-> Map Name TySyn
-> Map Name Name
-> InferM (Map Name Name)
forall (f :: * -> *) k a c b.
(Applicative f, Ord k) =>
WhenMissing f k a c
-> WhenMissing f k b c
-> WhenMatched f k a b c
-> Map k a
-> Map k b
-> f (Map k c)
Map.mergeA
((Name -> TySyn -> InferM Name)
-> WhenMissing InferM Name TySyn Name
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> f y) -> WhenMissing f k x y
Map.traverseMissing \Name
name TySyn
_ -> ModPath -> Name -> InferM Name
forall (m :: * -> *). FreshM m => ModPath -> Name -> m Name
newFunctorInst ModPath
mpath Name
name)
WhenMissing InferM Name Name Name
forall (f :: * -> *) k x. Applicative f => WhenMissing f k x x
Map.preserveMissing
((Name -> TySyn -> Name -> Name)
-> WhenMatched InferM Name TySyn Name Name
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
Map.zipWithMatched \Name
_ TySyn
_ Name
name' -> Name
name')
(ModuleG () -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ()
f)