{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.ModuleSystem.Interface (
Iface(..)
, IfaceDecls(..)
, IfaceTySyn, ifTySynName
, IfaceNewtype
, IfaceDecl(..), mkIfaceDecl
, IfaceParams(..)
, genIface
, ifacePrimMap
, noIfaceParams
) where
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (ModName)
import Cryptol.Parser.Position(Located)
import qualified Data.Map as Map
import Data.Semigroup
import GHC.Generics (Generic)
import Control.DeepSeq
import Prelude ()
import Prelude.Compat
data Iface = Iface
{ Iface -> ModName
ifModName :: !ModName
, Iface -> IfaceDecls
ifPublic :: IfaceDecls
, Iface -> IfaceDecls
ifPrivate :: IfaceDecls
, Iface -> IfaceParams
ifParams :: IfaceParams
} deriving (Int -> Iface -> ShowS
[Iface] -> ShowS
Iface -> String
(Int -> Iface -> ShowS)
-> (Iface -> String) -> ([Iface] -> ShowS) -> Show Iface
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Iface] -> ShowS
$cshowList :: [Iface] -> ShowS
show :: Iface -> String
$cshow :: Iface -> String
showsPrec :: Int -> Iface -> ShowS
$cshowsPrec :: Int -> Iface -> ShowS
Show, (forall x. Iface -> Rep Iface x)
-> (forall x. Rep Iface x -> Iface) -> Generic Iface
forall x. Rep Iface x -> Iface
forall x. Iface -> Rep Iface x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Iface x -> Iface
$cfrom :: forall x. Iface -> Rep Iface x
Generic, Iface -> ()
(Iface -> ()) -> NFData Iface
forall a. (a -> ()) -> NFData a
rnf :: Iface -> ()
$crnf :: Iface -> ()
NFData)
data IfaceParams = IfaceParams
{ IfaceParams -> Map Name ModTParam
ifParamTypes :: Map.Map Name ModTParam
, IfaceParams -> [Located Prop]
ifParamConstraints :: [Located Prop]
, IfaceParams -> Map Name ModVParam
ifParamFuns :: Map.Map Name ModVParam
} deriving (Int -> IfaceParams -> ShowS
[IfaceParams] -> ShowS
IfaceParams -> String
(Int -> IfaceParams -> ShowS)
-> (IfaceParams -> String)
-> ([IfaceParams] -> ShowS)
-> Show IfaceParams
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IfaceParams] -> ShowS
$cshowList :: [IfaceParams] -> ShowS
show :: IfaceParams -> String
$cshow :: IfaceParams -> String
showsPrec :: Int -> IfaceParams -> ShowS
$cshowsPrec :: Int -> IfaceParams -> ShowS
Show, (forall x. IfaceParams -> Rep IfaceParams x)
-> (forall x. Rep IfaceParams x -> IfaceParams)
-> Generic IfaceParams
forall x. Rep IfaceParams x -> IfaceParams
forall x. IfaceParams -> Rep IfaceParams x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IfaceParams x -> IfaceParams
$cfrom :: forall x. IfaceParams -> Rep IfaceParams x
Generic, IfaceParams -> ()
(IfaceParams -> ()) -> NFData IfaceParams
forall a. (a -> ()) -> NFData a
rnf :: IfaceParams -> ()
$crnf :: IfaceParams -> ()
NFData)
noIfaceParams :: IfaceParams
noIfaceParams :: IfaceParams
noIfaceParams = IfaceParams :: Map Name ModTParam
-> [Located Prop] -> Map Name ModVParam -> IfaceParams
IfaceParams
{ ifParamTypes :: Map Name ModTParam
ifParamTypes = Map Name ModTParam
forall k a. Map k a
Map.empty
, ifParamConstraints :: [Located Prop]
ifParamConstraints = []
, ifParamFuns :: Map Name ModVParam
ifParamFuns = Map Name ModVParam
forall k a. Map k a
Map.empty
}
data IfaceDecls = IfaceDecls
{ IfaceDecls -> Map Name IfaceTySyn
ifTySyns :: Map.Map Name IfaceTySyn
, IfaceDecls -> Map Name IfaceNewtype
ifNewtypes :: Map.Map Name IfaceNewtype
, IfaceDecls -> Map Name IfaceAbstractType
ifAbstractTypes :: Map.Map Name IfaceAbstractType
, IfaceDecls -> Map Name IfaceDecl
ifDecls :: Map.Map Name IfaceDecl
} deriving (Int -> IfaceDecls -> ShowS
[IfaceDecls] -> ShowS
IfaceDecls -> String
(Int -> IfaceDecls -> ShowS)
-> (IfaceDecls -> String)
-> ([IfaceDecls] -> ShowS)
-> Show IfaceDecls
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IfaceDecls] -> ShowS
$cshowList :: [IfaceDecls] -> ShowS
show :: IfaceDecls -> String
$cshow :: IfaceDecls -> String
showsPrec :: Int -> IfaceDecls -> ShowS
$cshowsPrec :: Int -> IfaceDecls -> ShowS
Show, (forall x. IfaceDecls -> Rep IfaceDecls x)
-> (forall x. Rep IfaceDecls x -> IfaceDecls) -> Generic IfaceDecls
forall x. Rep IfaceDecls x -> IfaceDecls
forall x. IfaceDecls -> Rep IfaceDecls x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IfaceDecls x -> IfaceDecls
$cfrom :: forall x. IfaceDecls -> Rep IfaceDecls x
Generic, IfaceDecls -> ()
(IfaceDecls -> ()) -> NFData IfaceDecls
forall a. (a -> ()) -> NFData a
rnf :: IfaceDecls -> ()
$crnf :: IfaceDecls -> ()
NFData)
instance Semigroup IfaceDecls where
l :: IfaceDecls
l <> :: IfaceDecls -> IfaceDecls -> IfaceDecls
<> r :: IfaceDecls
r = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> IfaceDecls
IfaceDecls
{ ifTySyns :: Map Name IfaceTySyn
ifTySyns = Map Name IfaceTySyn -> Map Name IfaceTySyn -> Map Name IfaceTySyn
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name IfaceTySyn
ifTySyns IfaceDecls
l) (IfaceDecls -> Map Name IfaceTySyn
ifTySyns IfaceDecls
r)
, ifNewtypes :: Map Name IfaceNewtype
ifNewtypes = Map Name IfaceNewtype
-> Map Name IfaceNewtype -> Map Name IfaceNewtype
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name IfaceNewtype
ifNewtypes IfaceDecls
l) (IfaceDecls -> Map Name IfaceNewtype
ifNewtypes IfaceDecls
r)
, ifAbstractTypes :: Map Name IfaceAbstractType
ifAbstractTypes = Map Name IfaceAbstractType
-> Map Name IfaceAbstractType -> Map Name IfaceAbstractType
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name IfaceAbstractType
ifAbstractTypes IfaceDecls
l) (IfaceDecls -> Map Name IfaceAbstractType
ifAbstractTypes IfaceDecls
r)
, ifDecls :: Map Name IfaceDecl
ifDecls = Map Name IfaceDecl -> Map Name IfaceDecl -> Map Name IfaceDecl
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
l) (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
r)
}
instance Monoid IfaceDecls where
mempty :: IfaceDecls
mempty = Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> IfaceDecls
IfaceDecls Map Name IfaceTySyn
forall k a. Map k a
Map.empty Map Name IfaceNewtype
forall k a. Map k a
Map.empty Map Name IfaceAbstractType
forall k a. Map k a
Map.empty Map Name IfaceDecl
forall k a. Map k a
Map.empty
mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls
mappend l :: IfaceDecls
l r :: IfaceDecls
r = IfaceDecls
l IfaceDecls -> IfaceDecls -> IfaceDecls
forall a. Semigroup a => a -> a -> a
<> IfaceDecls
r
mconcat :: [IfaceDecls] -> IfaceDecls
mconcat ds :: [IfaceDecls]
ds = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> IfaceDecls
IfaceDecls
{ ifTySyns :: Map Name IfaceTySyn
ifTySyns = [Map Name IfaceTySyn] -> Map Name IfaceTySyn
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name IfaceTySyn)
-> [IfaceDecls] -> [Map Name IfaceTySyn]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name IfaceTySyn
ifTySyns [IfaceDecls]
ds)
, ifNewtypes :: Map Name IfaceNewtype
ifNewtypes = [Map Name IfaceNewtype] -> Map Name IfaceNewtype
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name IfaceNewtype)
-> [IfaceDecls] -> [Map Name IfaceNewtype]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name IfaceNewtype
ifNewtypes [IfaceDecls]
ds)
, ifAbstractTypes :: Map Name IfaceAbstractType
ifAbstractTypes = [Map Name IfaceAbstractType] -> Map Name IfaceAbstractType
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name IfaceAbstractType)
-> [IfaceDecls] -> [Map Name IfaceAbstractType]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name IfaceAbstractType
ifAbstractTypes [IfaceDecls]
ds)
, ifDecls :: Map Name IfaceDecl
ifDecls = [Map Name IfaceDecl] -> Map Name IfaceDecl
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ((IfaceDecls -> Map Name IfaceDecl)
-> [IfaceDecls] -> [Map Name IfaceDecl]
forall a b. (a -> b) -> [a] -> [b]
map IfaceDecls -> Map Name IfaceDecl
ifDecls [IfaceDecls]
ds)
}
type IfaceTySyn = TySyn
ifTySynName :: TySyn -> Name
ifTySynName :: IfaceTySyn -> Name
ifTySynName = IfaceTySyn -> Name
tsName
type IfaceNewtype = Newtype
type IfaceAbstractType = AbstractType
data IfaceDecl = IfaceDecl
{ IfaceDecl -> Name
ifDeclName :: !Name
, IfaceDecl -> Schema
ifDeclSig :: Schema
, IfaceDecl -> [Pragma]
ifDeclPragmas :: [Pragma]
, IfaceDecl -> Bool
ifDeclInfix :: Bool
, IfaceDecl -> Maybe Fixity
ifDeclFixity :: Maybe Fixity
, IfaceDecl -> Maybe String
ifDeclDoc :: Maybe String
} deriving (Int -> IfaceDecl -> ShowS
[IfaceDecl] -> ShowS
IfaceDecl -> String
(Int -> IfaceDecl -> ShowS)
-> (IfaceDecl -> String)
-> ([IfaceDecl] -> ShowS)
-> Show IfaceDecl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IfaceDecl] -> ShowS
$cshowList :: [IfaceDecl] -> ShowS
show :: IfaceDecl -> String
$cshow :: IfaceDecl -> String
showsPrec :: Int -> IfaceDecl -> ShowS
$cshowsPrec :: Int -> IfaceDecl -> ShowS
Show, (forall x. IfaceDecl -> Rep IfaceDecl x)
-> (forall x. Rep IfaceDecl x -> IfaceDecl) -> Generic IfaceDecl
forall x. Rep IfaceDecl x -> IfaceDecl
forall x. IfaceDecl -> Rep IfaceDecl x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IfaceDecl x -> IfaceDecl
$cfrom :: forall x. IfaceDecl -> Rep IfaceDecl x
Generic, IfaceDecl -> ()
(IfaceDecl -> ()) -> NFData IfaceDecl
forall a. (a -> ()) -> NFData a
rnf :: IfaceDecl -> ()
$crnf :: IfaceDecl -> ()
NFData)
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl d :: Decl
d = $WIfaceDecl :: Name
-> Schema
-> [Pragma]
-> Bool
-> Maybe Fixity
-> Maybe String
-> 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 String
ifDeclDoc = Decl -> Maybe String
dDoc Decl
d
}
genIface :: Module -> Iface
genIface :: Module -> Iface
genIface m :: Module
m = $WIface :: ModName -> IfaceDecls -> IfaceDecls -> IfaceParams -> Iface
Iface
{ ifModName :: ModName
ifModName = Module -> ModName
mName Module
m
, ifPublic :: IfaceDecls
ifPublic = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> 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
}
, ifPrivate :: IfaceDecls
ifPrivate = IfaceDecls :: Map Name IfaceTySyn
-> Map Name IfaceNewtype
-> Map Name IfaceAbstractType
-> Map Name IfaceDecl
-> 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
}
, ifParams :: IfaceParams
ifParams = IfaceParams :: Map Name ModTParam
-> [Located Prop] -> Map Name ModVParam -> IfaceParams
IfaceParams
{ ifParamTypes :: Map Name ModTParam
ifParamTypes = Module -> Map Name ModTParam
mParamTypes Module
m
, ifParamConstraints :: [Located Prop]
ifParamConstraints = Module -> [Located Prop]
mParamConstraints Module
m
, ifParamFuns :: Map Name ModVParam
ifParamFuns = Module -> Map Name ModVParam
mParamFuns Module
m
}
}
where
(tsPub :: Map Name IfaceTySyn
tsPub,tsPriv :: 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 (\ qn :: Name
qn _ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` Module -> ExportSpec Name
mExports Module
m )
(Module -> Map Name IfaceTySyn
mTySyns Module
m)
(ntPub :: Map Name IfaceNewtype
ntPub,ntPriv :: 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 (\ qn :: Name
qn _ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` Module -> ExportSpec Name
mExports Module
m )
(Module -> Map Name IfaceNewtype
mNewtypes Module
m)
(atPub :: Map Name IfaceAbstractType
atPub,atPriv :: 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 (\qn :: Name
qn _ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedType` Module -> ExportSpec Name
mExports Module
m)
(Module -> Map Name IfaceAbstractType
mPrimTypes Module
m)
(dPub :: Map Name IfaceDecl
dPub,dPriv :: 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 (\ qn :: Name
qn _ -> Name
qn Name -> ExportSpec Name -> Bool
forall name. Ord name => name -> ExportSpec name -> Bool
`isExportedBind` Module -> ExportSpec Name
mExports Module
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 <- Module -> [DeclGroup]
mDecls Module
m
, Decl
d <- DeclGroup -> [Decl]
groupDecls DeclGroup
dg
, let qn :: Name
qn = Decl -> Name
dName Decl
d
]
ifacePrimMap :: Iface -> PrimMap
ifacePrimMap :: Iface -> PrimMap
ifacePrimMap Iface { .. } =
PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap
PrimMap { primDecls :: Map Ident Name
primDecls = (PrimMap -> Map Ident Name) -> Map Ident Name
forall k a. Ord k => (PrimMap -> Map k a) -> Map k a
merge PrimMap -> Map Ident Name
primDecls
, primTypes :: Map Ident Name
primTypes = (PrimMap -> Map Ident Name) -> Map Ident Name
forall k a. Ord k => (PrimMap -> Map k a) -> Map k a
merge PrimMap -> Map Ident Name
primTypes }
where
merge :: (PrimMap -> Map k a) -> Map k a
merge f :: PrimMap -> Map k a
f = Map k a -> Map k a -> Map k a
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (PrimMap -> Map k a
f PrimMap
public) (PrimMap -> Map k a
f PrimMap
private)
public :: PrimMap
public = IfaceDecls -> PrimMap
ifaceDeclsPrimMap IfaceDecls
ifPublic
private :: PrimMap
private = IfaceDecls -> PrimMap
ifaceDeclsPrimMap IfaceDecls
ifPrivate
ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
ifaceDeclsPrimMap :: IfaceDecls -> PrimMap
ifaceDeclsPrimMap IfaceDecls { .. } =
PrimMap :: Map Ident Name -> Map Ident Name -> PrimMap
PrimMap { primDecls :: Map Ident Name
primDecls = [(Ident, Name)] -> Map Ident Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Ident, Name)]
newtypes [(Ident, Name)] -> [(Ident, Name)] -> [(Ident, Name)]
forall a. [a] -> [a] -> [a]
++ [(Ident, Name)]
exprs)
, primTypes :: Map Ident Name
primTypes = [(Ident, Name)] -> Map Ident Name
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Ident, Name)]
newtypes [(Ident, Name)] -> [(Ident, Name)] -> [(Ident, Name)]
forall a. [a] -> [a] -> [a]
++ [(Ident, Name)]
types)
}
where
exprs :: [(Ident, Name)]
exprs = [ (Name -> Ident
nameIdent Name
n, Name
n) | Name
n <- Map Name IfaceDecl -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name IfaceDecl
ifDecls ]
newtypes :: [(Ident, Name)]
newtypes = [ (Name -> Ident
nameIdent Name
n, Name
n) | Name
n <- Map Name IfaceNewtype -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name IfaceNewtype
ifNewtypes ]
types :: [(Ident, Name)]
types = [ (Name -> Ident
nameIdent Name
n, Name
n) | Name
n <- Map Name IfaceTySyn -> [Name]
forall k a. Map k a -> [k]
Map.keys Map Name IfaceTySyn
ifTySyns ]