module Cryptol.TypeCheck.Interface where
import qualified Data.Map as Map
import Cryptol.Utils.Ident(Namespace(..))
import Cryptol.ModuleSystem.Interface
import Cryptol.TypeCheck.AST
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl Decl
d = IfaceDecl :: Name
-> Schema
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe Text
-> IfaceDecl
IfaceDecl
{ ifDeclName :: Name
ifDeclName = Decl -> Name
dName Decl
d
, ifDeclSig :: Schema
ifDeclSig = Decl -> Schema
dSignature Decl
d
, ifDeclPragmas :: [Pragma]
ifDeclPragmas = Decl -> [Pragma]
dPragmas Decl
d
, ifDeclInfix :: Bool
ifDeclInfix = Decl -> Bool
dInfix Decl
d
, ifDeclFixity :: Maybe Fixity
ifDeclFixity = Decl -> Maybe Fixity
dFixity Decl
d
, ifDeclDoc :: Maybe Text
ifDeclDoc = Decl -> Maybe Text
dDoc Decl
d
}
genIface :: ModuleG mname -> IfaceG mname
genIface :: ModuleG mname -> IfaceG mname
genIface ModuleG mname
m = Iface :: forall mname.
mname -> IfaceDecls -> IfaceDecls -> IfaceParams -> IfaceG mname
Iface
{ ifModName :: mname
ifModName = ModuleG mname -> mname
forall mname. ModuleG mname -> mname
mName ModuleG mname
m
, ifPublic :: IfaceDecls
ifPublic = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> Map Name (IfaceG Name)
-> IfaceDecls
IfaceDecls
{ ifTySyns :: Map Name IfaceTySyn
ifTySyns = Map Name IfaceTySyn
tsPub
, ifNewtypes :: Map Name IfaceNewtype
ifNewtypes = Map Name IfaceNewtype
ntPub
, ifAbstractTypes :: Map Name IfaceAbstractType
ifAbstractTypes = Map Name IfaceAbstractType
atPub
, ifDecls :: Map Name IfaceDecl
ifDecls = Map Name IfaceDecl
dPub
, ifModules :: Map Name (IfaceG Name)
ifModules = Map Name (IfaceG Name)
mPub
}
, ifPrivate :: IfaceDecls
ifPrivate = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> Map Name (IfaceG Name)
-> IfaceDecls
IfaceDecls
{ ifTySyns :: Map Name IfaceTySyn
ifTySyns = Map Name IfaceTySyn
tsPriv
, ifNewtypes :: Map Name IfaceNewtype
ifNewtypes = Map Name IfaceNewtype
ntPriv
, ifAbstractTypes :: Map Name IfaceAbstractType
ifAbstractTypes = Map Name IfaceAbstractType
atPriv
, ifDecls :: Map Name IfaceDecl
ifDecls = Map Name IfaceDecl
dPriv
, ifModules :: Map Name (IfaceG Name)
ifModules = Map Name (IfaceG Name)
mPriv
}
, ifParams :: IfaceParams
ifParams = IfaceParams :: Map Name ModTParam
-> [Located Prop] -> Map Name ModVParam -> IfaceParams
IfaceParams
{ ifParamTypes :: Map Name ModTParam
ifParamTypes = ModuleG mname -> Map Name ModTParam
forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG mname
m
, ifParamConstraints :: [Located Prop]
ifParamConstraints = ModuleG mname -> [Located Prop]
forall mname. ModuleG mname -> [Located Prop]
mParamConstraints ModuleG mname
m
, ifParamFuns :: Map Name ModVParam
ifParamFuns = ModuleG mname -> Map Name ModVParam
forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG mname
m
}
}
where
(Map Name IfaceTySyn
tsPub,Map Name IfaceTySyn
tsPriv) =
(Name -> IfaceTySyn -> Bool)
-> Map Name IfaceTySyn
-> (Map Name IfaceTySyn, Map Name IfaceTySyn)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceTySyn
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m )
(ModuleG mname -> Map Name IfaceTySyn
forall mname. ModuleG mname -> Map Name IfaceTySyn
mTySyns ModuleG mname
m)
(Map Name IfaceNewtype
ntPub,Map Name IfaceNewtype
ntPriv) =
(Name -> IfaceNewtype -> Bool)
-> Map Name IfaceNewtype
-> (Map Name IfaceNewtype, Map Name IfaceNewtype)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceNewtype
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m )
(ModuleG mname -> Map Name IfaceNewtype
forall mname. ModuleG mname -> Map Name IfaceNewtype
mNewtypes ModuleG mname
m)
(Map Name IfaceAbstractType
atPub,Map Name IfaceAbstractType
atPriv) =
(Name -> IfaceAbstractType -> Bool)
-> Map Name IfaceAbstractType
-> (Map Name IfaceAbstractType, Map Name IfaceAbstractType)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\Name
qn IfaceAbstractType
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m)
(ModuleG mname -> Map Name IfaceAbstractType
forall mname. ModuleG mname -> Map Name IfaceAbstractType
mPrimTypes ModuleG mname
m)
(Map Name IfaceDecl
dPub,Map Name IfaceDecl
dPriv) =
(Name -> IfaceDecl -> Bool)
-> Map Name IfaceDecl -> (Map Name IfaceDecl, Map Name IfaceDecl)
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceDecl
_ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedBind` ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m)
(Map Name IfaceDecl -> (Map Name IfaceDecl, Map Name IfaceDecl))
-> Map Name IfaceDecl -> (Map Name IfaceDecl, Map Name IfaceDecl)
forall a b. (a -> b) -> a -> b
$ [(Name, IfaceDecl)] -> Map Name IfaceDecl
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
qn,Decl -> IfaceDecl
mkIfaceDecl Decl
d) | DeclGroup
dg <- ModuleG mname -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG mname
m
, Decl
d <- DeclGroup -> [Decl]
groupDecls DeclGroup
dg
, let qn :: Name
qn = Decl -> Name
dName Decl
d
]
(Map Name (IfaceG Name)
mPub,Map Name (IfaceG Name)
mPriv) =
(Name -> IfaceG Name -> Bool)
-> Map Name (IfaceG Name)
-> (Map Name (IfaceG Name), Map Name (IfaceG Name))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ Name
qn IfaceG Name
_ -> Namespace -> Name -> ExportSpec Name -> Bool
forall name.
Ord name =>
Namespace -> name -> ExportSpec name -> Bool
isExported Namespace
NSModule Name
qn (ModuleG mname -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG mname
m))
(Map Name (IfaceG Name)
-> (Map Name (IfaceG Name), Map Name (IfaceG Name)))
-> Map Name (IfaceG Name)
-> (Map Name (IfaceG Name), Map Name (IfaceG Name))
forall a b. (a -> b) -> a -> b
$ ModuleG mname -> Map Name (IfaceG Name)
forall mname. ModuleG mname -> Map Name (IfaceG Name)
mSubModules ModuleG mname
m