{-# Language ImplicitParams, ConstraintKinds #-}
module Cryptol.TypeCheck.ModuleInstance where
import Data.Map(Map)
import qualified Data.Map as Map
import Data.Set(Set)
import qualified Data.Set as Set
import Cryptol.Parser.Position(Located)
import Cryptol.ModuleSystem.Interface(IfaceNames(..))
import Cryptol.IR.TraverseNames(TraverseNames,mapNames)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst)
type Su = (?tSu :: Subst, ?vSu :: Map Name Name)
doVInst :: (Su, TraverseNames a) => a -> a
doVInst :: forall a. (Su, TraverseNames a) => a -> a
doVInst = forall t. TraverseNames t => (Name -> Name) -> t -> t
mapNames (\Name
x -> forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Name
x Name
x ?vSu::Map Name Name
?vSu)
doTInst :: (Su, TVars a) => a -> a
doTInst :: forall a. (Su, TVars a) => a -> a
doTInst = forall t. TVars t => Subst -> t -> t
apSubst ?tSu::Subst
?tSu
doTVInst :: (Su, TVars a, TraverseNames a) => a -> a
doTVInst :: forall a. (Su, TVars a, TraverseNames a) => a -> a
doTVInst = forall t. TVars t => Subst -> t -> t
apSubst ?tSu::Subst
?tSu forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Su, TraverseNames a) => a -> a
doVInst
doMap :: (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap :: forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap Map Name a
mp =
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance Name
x, forall t. (ModuleInstance t, Su) => t -> t
moduleInstance a
d) | (Name
x,a
d) <- forall k a. Map k a -> [(k, a)]
Map.toList Map Name a
mp ]
doSet :: Su => Set Name -> Set Name
doSet :: Su => Set Name -> Set Name
doSet = forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall t. (ModuleInstance t, Su) => t -> t
moduleInstance forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
class ModuleInstance t where
moduleInstance :: Su => t -> t
instance ModuleInstance a => ModuleInstance [a] where
moduleInstance :: Su => [a] -> [a]
moduleInstance = forall a b. (a -> b) -> [a] -> [b]
map forall t. (ModuleInstance t, Su) => t -> t
moduleInstance
instance ModuleInstance a => ModuleInstance (Located a) where
moduleInstance :: Su => Located a -> Located a
moduleInstance Located a
l = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located a
l
instance ModuleInstance Name where
moduleInstance :: Su => Name -> Name
moduleInstance = forall a. (Su, TraverseNames a) => a -> a
doVInst
instance ModuleInstance name => ModuleInstance (ImpName name) where
moduleInstance :: Su => ImpName name -> ImpName name
moduleInstance ImpName name
x =
case ImpName name
x of
ImpTop ModName
t -> forall name. ModName -> ImpName name
ImpTop ModName
t
ImpNested name
n -> forall name. name -> ImpName name
ImpNested (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance name
n)
instance ModuleInstance (ModuleG name) where
moduleInstance :: Su => ModuleG name -> ModuleG name
moduleInstance ModuleG name
m =
Module { mName :: name
mName = forall mname. ModuleG mname -> mname
mName ModuleG name
m
, mDoc :: Maybe Text
mDoc = forall a. Maybe a
Nothing
, mExports :: ExportSpec Name
mExports = forall a. (Su, TraverseNames a) => a -> a
doVInst (forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG name
m)
, mParamTypes :: Map Name ModTParam
mParamTypes = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG name
m)
, mParamFuns :: Map Name ModVParam
mParamFuns = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG name
m)
, mParamConstraints :: [Located Prop]
mParamConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (forall mname. ModuleG mname -> [Located Prop]
mParamConstraints ModuleG name
m)
, mParams :: FunctorParams
mParams = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall mname. ModuleG mname -> FunctorParams
mParams ModuleG name
m
, mFunctors :: Map Name (ModuleG Name)
mFunctors = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG name
m)
, mNested :: Set Name
mNested = Su => Set Name -> Set Name
doSet (forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m)
, mTySyns :: Map Name TySyn
mTySyns = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG name
m)
, mNewtypes :: Map Name Newtype
mNewtypes = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG name
m)
, mPrimTypes :: Map Name AbstractType
mPrimTypes = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG name
m)
, mDecls :: [DeclGroup]
mDecls = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG name
m)
, mSubmodules :: Map Name (IfaceNames Name)
mSubmodules = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG name
m)
, mSignatures :: Map Name ModParamNames
mSignatures = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG name
m)
}
instance ModuleInstance Type where
moduleInstance :: Su => Prop -> Prop
moduleInstance = forall a. (Su, TVars a) => a -> a
doTInst
instance ModuleInstance Schema where
moduleInstance :: Su => Schema -> Schema
moduleInstance = forall a. (Su, TVars a) => a -> a
doTInst
instance ModuleInstance TySyn where
moduleInstance :: Su => TySyn -> TySyn
moduleInstance TySyn
ts =
TySyn { tsName :: Name
tsName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (TySyn -> Name
tsName TySyn
ts)
, tsParams :: [TParam]
tsParams = TySyn -> [TParam]
tsParams TySyn
ts
, tsConstraints :: [Prop]
tsConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (TySyn -> [Prop]
tsConstraints TySyn
ts)
, tsDef :: Prop
tsDef = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (TySyn -> Prop
tsDef TySyn
ts)
, tsDoc :: Maybe Text
tsDoc = TySyn -> Maybe Text
tsDoc TySyn
ts
}
instance ModuleInstance Newtype where
moduleInstance :: Su => Newtype -> Newtype
moduleInstance Newtype
nt =
Newtype { ntName :: Name
ntName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Newtype -> Name
ntName Newtype
nt)
, ntParams :: [TParam]
ntParams = Newtype -> [TParam]
ntParams Newtype
nt
, ntConstraints :: [Prop]
ntConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Newtype -> [Prop]
ntConstraints Newtype
nt)
, ntConName :: Name
ntConName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (Newtype -> Name
ntConName Newtype
nt)
, ntFields :: RecordMap Ident Prop
ntFields = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Newtype -> RecordMap Ident Prop
ntFields Newtype
nt
, ntDoc :: Maybe Text
ntDoc = Newtype -> Maybe Text
ntDoc Newtype
nt
}
instance ModuleInstance AbstractType where
moduleInstance :: Su => AbstractType -> AbstractType
moduleInstance AbstractType
at =
AbstractType { atName :: Name
atName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (AbstractType -> Name
atName AbstractType
at)
, atKind :: Kind
atKind = AbstractType -> Kind
atKind AbstractType
at
, atCtrs :: ([TParam], [Prop])
atCtrs = let ([TParam]
ps,[Prop]
cs) = AbstractType -> ([TParam], [Prop])
atCtrs AbstractType
at
in ([TParam]
ps, forall t. (ModuleInstance t, Su) => t -> t
moduleInstance [Prop]
cs)
, atFixitiy :: Maybe Fixity
atFixitiy = AbstractType -> Maybe Fixity
atFixitiy AbstractType
at
, atDoc :: Maybe Text
atDoc = AbstractType -> Maybe Text
atDoc AbstractType
at
}
instance ModuleInstance DeclGroup where
moduleInstance :: Su => DeclGroup -> DeclGroup
moduleInstance DeclGroup
dg =
case DeclGroup
dg of
Recursive [Decl]
ds -> [Decl] -> DeclGroup
Recursive (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance [Decl]
ds)
NonRecursive Decl
d -> Decl -> DeclGroup
NonRecursive (forall t. (ModuleInstance t, Su) => t -> t
moduleInstance Decl
d)
instance ModuleInstance Decl where
moduleInstance :: Su => Decl -> Decl
moduleInstance = forall a. (Su, TVars a, TraverseNames a) => a -> a
doTVInst
instance ModuleInstance name => ModuleInstance (IfaceNames name) where
moduleInstance :: Su => IfaceNames name -> IfaceNames name
moduleInstance IfaceNames name
ns =
IfaceNames { ifsName :: name
ifsName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (forall name. IfaceNames name -> name
ifsName IfaceNames name
ns)
, ifsNested :: Set Name
ifsNested = Su => Set Name -> Set Name
doSet (forall name. IfaceNames name -> Set Name
ifsNested IfaceNames name
ns)
, ifsDefines :: Set Name
ifsDefines = Su => Set Name -> Set Name
doSet (forall name. IfaceNames name -> Set Name
ifsDefines IfaceNames name
ns)
, ifsPublic :: Set Name
ifsPublic = Su => Set Name -> Set Name
doSet (forall name. IfaceNames name -> Set Name
ifsPublic IfaceNames name
ns)
, ifsDoc :: Maybe Text
ifsDoc = forall name. IfaceNames name -> Maybe Text
ifsDoc IfaceNames name
ns
}
instance ModuleInstance ModParamNames where
moduleInstance :: Su => ModParamNames -> ModParamNames
moduleInstance ModParamNames
si =
ModParamNames { mpnTypes :: Map Name ModTParam
mpnTypes = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
si)
, mpnConstraints :: [Located Prop]
mpnConstraints = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModParamNames -> [Located Prop]
mpnConstraints ModParamNames
si)
, mpnFuns :: Map Name ModVParam
mpnFuns = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
si)
, mpnTySyn :: Map Name TySyn
mpnTySyn = forall a. (Su, ModuleInstance a) => Map Name a -> Map Name a
doMap (ModParamNames -> Map Name TySyn
mpnTySyn ModParamNames
si)
, mpnDoc :: Maybe Text
mpnDoc = ModParamNames -> Maybe Text
mpnDoc ModParamNames
si
}
instance ModuleInstance ModTParam where
moduleInstance :: Su => ModTParam -> ModTParam
moduleInstance ModTParam
mp =
ModTParam { mtpName :: Name
mtpName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModTParam -> Name
mtpName ModTParam
mp)
, mtpKind :: Kind
mtpKind = ModTParam -> Kind
mtpKind ModTParam
mp
, mtpDoc :: Maybe Text
mtpDoc = ModTParam -> Maybe Text
mtpDoc ModTParam
mp
}
instance ModuleInstance ModVParam where
moduleInstance :: Su => ModVParam -> ModVParam
moduleInstance ModVParam
mp =
ModVParam { mvpName :: Name
mvpName = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModVParam -> Name
mvpName ModVParam
mp)
, mvpType :: Schema
mvpType = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModVParam -> Schema
mvpType ModVParam
mp)
, mvpDoc :: Maybe Text
mvpDoc = ModVParam -> Maybe Text
mvpDoc ModVParam
mp
, mvpFixity :: Maybe Fixity
mvpFixity = ModVParam -> Maybe Fixity
mvpFixity ModVParam
mp
}
instance ModuleInstance ModParam where
moduleInstance :: Su => ModParam -> ModParam
moduleInstance ModParam
p =
ModParam { mpName :: Ident
mpName = ModParam -> Ident
mpName ModParam
p
, mpIface :: ImpName Name
mpIface = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModParam -> ImpName Name
mpIface ModParam
p)
, mpParameters :: ModParamNames
mpParameters = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance (ModParam -> ModParamNames
mpParameters ModParam
p)
, mpQual :: Maybe ModName
mpQual = ModParam -> Maybe ModName
mpQual ModParam
p
}