cryptol-3.1.0: src/Cryptol/TypeCheck/Module.hs
{-# 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) {- ^ Name for the new module -} ->
Located (P.ImpName Name) {- ^ Functor being instantiated -} ->
P.ModuleInstanceArgs Name {- ^ Instance arguments -} ->
Map Name Name
{- ^ Instantitation. These is the renaming for the functor that arises from
generativity (i.e., it is something that will make the names "fresh").
-} ->
NamingEnv
{- ^ Names in the enclosing scope of the instantiated module -} ->
Maybe Text {- ^ Documentation -} ->
InferM (Maybe TCTopEntity)
doFunctorInst m f as instMap0 enclosingInScope doc =
inRange (srcRange m)
do mf <- lookupFunctor (thing f)
argIs <- checkArity (srcRange f) mf as
m2 <- do let mpath = P.impNameModPath (thing m)
as2 <- mapM (checkArg mpath) argIs
let (tySus,paramTySyns,decls,paramInstMaps) =
unzip4 [ (su,ts,ds,im) | DefinedInst su ts ds im <- as2 ]
instMap <- addMissingTySyns mpath mf instMap0
let ?tVarSu = mergeDistinctSubst tySus
?nameSu = instMap <> mconcat paramInstMaps
let m1 = moduleInstance mf
m2 = 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 (tps,tcs,vps) =
unzip3 [ (xs,cs,fs) | ParamInst xs cs fs <- as2 ]
tpSet = Set.unions tps
tpSet' = Set.map snd (Set.unions tps)
emit p = Set.null (freeParams (thing p)
`Set.intersection` tpSet')
(emitPs,delayPs) = partition emit (mParamConstraints m1)
forM_ emitPs \lp ->
newGoals (CtModuleInstance (srcRange lp)) [thing lp]
doBacktickInstance tpSet
(map thing delayPs ++ concat tcs)
(Map.unions vps)
m2
-- An instantiation doesn't really have anything "in scope" per se, but
-- here we compute what would be in scope as if you hand wrote the
-- instantiation by copy-pasting the functor then substituting the
-- parameters. That is, it would be whatever is in scope in the functor,
-- together with any names in the enclosing scope if this is a nested
-- module, with the functor's names taking precedence. This is used to
-- determine what is in scope at the REPL when the instantiation is loaded
-- and focused.
--
-- The exception is when instantiating with _, in which case we must delete
-- the module parameters from the naming environment.
let inScope0 = mInScope m2 `without`
mconcat [ modParamNamingEnv mp | (_, mp, AddDeclParams) <- argIs ]
inScope = inScope0 `shadowing` enclosingInScope
case thing m of
P.ImpTop mn -> newModuleScope mn (mExports m2) inScope
P.ImpNested mn -> newSubmoduleScope mn doc (mExports m2) inScope
mapM_ addTySyn (Map.elems (mTySyns m2))
mapM_ addNominal (Map.elems (mNominalTypes m2))
addSignatures (mSignatures m2)
addSubmodules (mSubmodules m2)
addFunctors (mFunctors m2)
mapM_ addDecls (mDecls m2)
case thing m of
P.ImpTop {} -> Just <$> endModule
P.ImpNested {} -> endSubmodule >> pure Nothing
data ActualArg =
UseParameter ModParam -- ^ Instantiate using this parameter
| UseModule (IfaceG ()) -- ^ Instantiate using this module
| AddDeclParams -- ^ Instantiate by adding parameters
{- | Validate a functor application, just checking the argument names.
The result associates a module parameter with the concrete way it should
be instantiated.
-}
checkArity ::
Range {- ^ Location for reporting errors -} ->
ModuleG () {- ^ The functor being instantiated -} ->
P.ModuleInstanceArgs Name {- ^ The arguments -} ->
InferM [(Range, ModParam, ActualArg)]
{- ^ Associates functor parameters with the interfaces of the
instantiating modules -}
checkArity r mf args =
case args of
P.DefaultInstArg arg ->
let i = Located { srcRange = srcRange arg
, thing = head (Map.keys ps0)
}
in checkArgs [] ps0 [ P.ModuleInstanceNamedArg i arg ]
P.NamedInstArgs as -> checkArgs [] ps0 as
P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ]
where
ps0 = mParams mf
checkArgs done ps as =
case as of
[] -> do forM_ (Map.keys ps) \p ->
recordErrorLoc (Just r) (FunctorInstanceMissingArgument p)
pure done
P.ModuleInstanceNamedArg ll lm : more ->
case Map.lookup (thing ll) ps of
Just i ->
do arg <- case thing lm of
P.ModuleArg m -> Just . UseModule <$> lookupModule m
P.ParameterArg p ->
do mb <- lookupModParam p
case mb of
Nothing ->
do inRange (srcRange lm)
(recordError (MissingModParam p))
pure Nothing
Just a -> pure (Just (UseParameter a))
P.AddParams -> pure (Just AddDeclParams)
let next = case arg of
Nothing -> done
Just a -> (srcRange lm, i, a) : done
checkArgs next (Map.delete (thing ll) ps) more
Nothing ->
do recordErrorLoc (Just (srcRange ll))
(FunctorInstanceBadArgument (thing ll))
checkArgs done ps more
data ArgInst = -- | Argument that defines the params
DefinedInst Subst
(Map Name TySyn)
-- ^ Type synonyms created from the functor's type parameters
[Decl]
-- ^ Bindings for value parameters
(Map Name Name)
-- ^ Map from the functor's parameter names to the new names
-- created for the instantiation
| ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual Name) Type)
-- ^ Argument that add parameters
-- The type parameters are in their module type parameter
-- form (i.e., tpFlav is TPModParam)
{- | Check the argument to a functor parameter.
Returns:
* A substitution which will replace the parameter types with
the concrete types that were provided
* Some declarations that define the parameters in terms of the provided
values.
* XXX: Extra parameters for instantiation by adding params
-}
checkArg ::
ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg mpath (r,expect,actual') =
case actual' of
AddDeclParams -> paramInst
UseParameter {} -> definedInst
UseModule {} -> definedInst
where
paramInst =
do let as = Set.fromList
(map (qual . mtpParam) (Map.elems (mpnTypes params)))
cs = map thing (mpnConstraints params)
check = checkSimpleParameterValue r (mpName expect)
qual a = (mpQual expect, a)
fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params)
pure (ParamInst as cs (Map.mapKeys qual fs))
definedInst =
do (tRens, tSyns, tInstMaps) <- unzip3 <$>
mapM (checkParamType mpath r tyMap) (Map.toList (mpnTypes params))
let renSu = listParamSubst (concat tRens)
{- Note: the constraints from the signature are already added to the
constraints for the functor and they are checked all at once in
doFunctorInst -}
(vDecls, vInstMaps) <-
mapAndUnzipM (checkParamValue mpath r vMap)
[ s { mvpType = apSubst renSu (mvpType s) }
| s <- Map.elems (mpnFuns params) ]
pure $ DefinedInst renSu (mconcat tSyns)
(concat vDecls) (mconcat tInstMaps <> mconcat vInstMaps)
params = mpParameters expect
-- Things provided by the argument module
tyMap :: Map Ident (Kind, Type)
vMap :: Map Ident (Name, Schema)
(tyMap,vMap) =
case actual' of
UseParameter mp ->
( nameMapToIdentMap fromTP (mpnTypes ps)
, nameMapToIdentMap fromVP (mpnFuns ps)
)
where
ps = mpParameters mp
fromTP tp = (mtpKind tp, TVar (TVBound (mtpParam tp)))
fromVP vp = (mvpName vp, mvpType vp)
UseModule actual ->
( Map.unions [ nameMapToIdentMap fromTS (ifTySyns decls)
, nameMapToIdentMap fromNominal (ifNominalTypes decls)
]
, nameMapToIdentMap fromD (ifDecls decls)
)
where
localNames = ifsPublic (ifNames actual)
isLocal x = x `Set.member` localNames
-- Things defined by the argument module
decls = filterIfaceDecls isLocal (ifDefines actual)
fromD d = (ifDeclName d, ifDeclSig d)
fromTS ts = (kindOf ts, tsDef ts)
fromNominal nt = (kindOf nt, TNominal nt [])
AddDeclParams -> panic "checkArg" ["AddDeclParams"]
nameMapToIdentMap :: (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap f m =
Map.fromList [ (nameIdent n, f v) | (n,v) <- Map.toList m ]
-- | Check a type parameter to a module.
checkParamType ::
ModPath {- ^ The new module we are creating -} ->
Range {- ^ Location for error reporting -} ->
Map Ident (Kind,Type) {- ^ Actual types -} ->
(Name,ModTParam) {- ^ Type parameter -} ->
InferM ([(TParam,Type)], Map Name TySyn, Map Name Name)
{- ^ Mapping from parameter name to actual type (for type substitution),
type synonym map from a fresh type name to the actual type
(only so that the type can be referred to in the REPL;
type synonyms are fully inlined into types at this point),
and a map from the old type name to the fresh type name
(for instantiation) -}
checkParamType mpath r tyMap (name,mp) =
let i = nameIdent name
expectK = mtpKind mp
in
case Map.lookup i tyMap of
Nothing ->
do recordErrorLoc (Just r) (FunctorInstanceMissingName NSType i)
pure ([], Map.empty, Map.empty)
Just (actualK,actualT) ->
do unless (expectK == actualK)
(recordErrorLoc (Just r)
(KindMismatch (Just (TVFromModParam name))
expectK actualK))
name' <- newFunctorInst mpath name
let tySyn = TySyn { tsName = name'
, tsParams = []
, tsConstraints = []
, tsDef = actualT
, tsDoc = mtpDoc mp }
pure ( [(mtpParam mp, actualT)]
, Map.singleton name' tySyn
, Map.singleton name name'
)
-- | Check a value parameter to a module.
checkParamValue ::
ModPath {- ^ The new module we are creating -} ->
Range {- ^ Location for error reporting -} ->
Map Ident (Name,Schema) {- ^ Actual values -} ->
ModVParam {- ^ The parameter we are checking -} ->
InferM ([Decl], Map Name Name)
{- ^ Decl mapping a new name to the actual value,
and a map from the value param name in the functor to the new name
(for instantiation) -}
checkParamValue mpath r vMap mp =
let name = mvpName mp
i = nameIdent name
expectT = mvpType mp
in case Map.lookup i vMap of
Nothing ->
do recordErrorLoc (Just r) (FunctorInstanceMissingName NSValue i)
pure ([], Map.empty)
Just actual ->
do e <- mkParamDef r (name,expectT) actual
name' <- newFunctorInst mpath name
let d = Decl { dName = name'
, dSignature = expectT
, dDefinition = DExpr e
, dPragmas = []
, dInfix = isInfixIdent (nameIdent name')
, dFixity = mvpFixity mp
, dDoc = mvpDoc mp
}
pure ([d], Map.singleton name name')
checkSimpleParameterValue ::
Range {- ^ Location for error reporting -} ->
Ident {- ^ Name of functor parameter -} ->
ModVParam {- ^ Module parameter -} ->
InferM (Maybe Type) {- ^ Type to add to things, `Nothing` on err -}
checkSimpleParameterValue r i mp =
case (sVars sch, sProps sch) of
([],[]) -> pure (Just (sType sch))
_ ->
do recordErrorLoc (Just r)
(FunctorInstanceBadBacktick
(BIPolymorphicArgument i (nameIdent (mvpName mp))))
pure Nothing
where
sch = mvpType mp
{- | Make an "adaptor" that instantiates the paramter into the form expected
by the functor. If the actual type is:
> {x} P => t
and the provided type is:
> f : {y} Q => s
The result, if successful would be:
/\x \{P}. f @a {Q}
To do this we need to find types `a` to instantiate `y`, and prove that:
{x} P => Q[a/y] /\ s = t
-}
mkParamDef ::
Range {- ^ Location of instantiation for error reporting -} ->
(Name,Schema) {- ^ Name and type of parameter -} ->
(Name,Schema) {- ^ Name and type of actual argument -} ->
InferM Expr
mkParamDef r (pname,wantedS) (arg,actualS) =
do (e,todo) <- collectGoals
$ withTParams (sVars wantedS)
do (e,t) <- instantiateWith pname(EVar arg) actualS []
props <- unify WithSource { twsType = sType wantedS
, twsSource = TVFromModParam arg
, twsRange = Just r
}
t
newGoals (CtModuleInstance r) props
pure e
su <- proveImplication False
(Just pname)
(sVars wantedS)
(sProps wantedS)
todo
let res = foldr ETAbs res1 (sVars wantedS)
res1 = foldr EProofAbs (apSubst su e) (sProps wantedS)
applySubst res
-- | The instMap we get from the renamer will not contain the fresh names for
-- certain things in the functor generated in the typechecking stage, if we are
-- instantiating a functor that is in the same file, since renaming and
-- typechecking happens together with the instantiation. In particular, if the
-- functor's interface has type synonyms, they will only get copied over into
-- the functor in the typechecker, so the renamer will not see them. Here we
-- make the fresh names for those missing type synonyms and add them to the
-- instMap.
addMissingTySyns ::
ModPath {- ^ The new module we are creating -} ->
ModuleG () {- ^ The functor -} ->
Map Name Name {- ^ instMap we get from renamer -} ->
InferM (Map Name Name) {- ^ the complete instMap -}
addMissingTySyns mpath f = Map.mergeA
(Map.traverseMissing \name _ -> newFunctorInst mpath name)
Map.preserveMissing
(Map.zipWithMatched \_ _ name' -> name')
(mTySyns f)