{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Interface where
import qualified Data.Map as Map
import Data.Set(Set)
import qualified Data.Set as Set
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Exports(allExported)
import Cryptol.TypeCheck.AST
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl Decl
d = IfaceDecl
{ ifDeclName :: Name
ifDeclName = Decl -> Name
dName Decl
d
, ifDeclSig :: Schema
ifDeclSig = Decl -> Schema
dSignature Decl
d
, ifDeclIsPrim :: Bool
ifDeclIsPrim = case Decl -> DeclDef
dDefinition Decl
d of
DPrim {} -> Bool
True
DeclDef
_ -> Bool
False
, 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
}
genIfaceNames :: ModuleG name -> IfaceNames name
genIfaceNames :: forall name. ModuleG name -> IfaceNames name
genIfaceNames ModuleG name
m = IfaceNames
{ ifsName :: name
ifsName = forall mname. ModuleG mname -> mname
mName ModuleG name
m
, ifsNested :: Set Name
ifsNested = forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m
, ifsDefines :: Set Name
ifsDefines = forall mname. ModuleG mname -> Set Name
genModDefines ModuleG name
m
, ifsPublic :: Set Name
ifsPublic = forall name. Ord name => ExportSpec name -> Set name
allExported (forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG name
m)
, ifsDoc :: Maybe Text
ifsDoc = forall mname. ModuleG mname -> Maybe Text
mDoc ModuleG name
m
}
genModDefines :: ModuleG name -> Set Name
genModDefines :: forall mname. ModuleG mname -> Set Name
genModDefines ModuleG name
m =
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
[ forall k a. Map k a -> Set k
Map.keysSet (forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG name
m)
, forall k a. Map k a -> Set k
Map.keysSet (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG name
m)
, forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map Newtype -> Name
ntConName (forall k a. Map k a -> [a]
Map.elems (forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG name
m)))
, forall k a. Map k a -> Set k
Map.keysSet (forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG name
m)
, forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map Decl -> Name
dName (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DeclGroup -> [Decl]
groupDecls (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG name
m)))
, forall k a. Map k a -> Set k
Map.keysSet (forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG name
m)
, forall k a. Map k a -> Set k
Map.keysSet (forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG name
m)
, forall k a. Map k a -> Set k
Map.keysSet (forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG name
m)
] forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Name -> Set Name
nestedInSet (forall mname. ModuleG mname -> Set Name
mNested ModuleG name
m)
where
nestedInSet :: Set Name -> Set Name
nestedInSet = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Name -> Set Name
inNested forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList
inNested :: Name -> Set Name
inNested Name
x = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
x (forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG name
m) of
Just IfaceNames Name
y -> forall name. IfaceNames name -> Set Name
ifsDefines IfaceNames Name
y forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set Name -> Set Name
nestedInSet (forall name. IfaceNames name -> Set Name
ifsNested IfaceNames Name
y)
Maybe (IfaceNames Name)
Nothing -> forall a. Set a
Set.empty
genIface :: ModuleG name -> IfaceG name
genIface :: forall name. ModuleG name -> IfaceG name
genIface ModuleG name
m = forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames (forall name. ModuleG name -> IfaceNames name
genIfaceNames ModuleG name
m) ModuleG name
m
genIfaceWithNames :: IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames :: forall name ignored.
IfaceNames name -> ModuleG ignored -> IfaceG name
genIfaceWithNames IfaceNames name
names ModuleG ignored
m =
Iface
{ ifNames :: IfaceNames name
ifNames = IfaceNames name
names
, ifDefines :: IfaceDecls
ifDefines = IfaceDecls
{ ifTySyns :: Map Name TySyn
ifTySyns = forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ignored
m
, ifNewtypes :: Map Name Newtype
ifNewtypes = forall mname. ModuleG mname -> Map Name Newtype
mNewtypes ModuleG ignored
m
, ifAbstractTypes :: Map Name AbstractType
ifAbstractTypes = forall mname. ModuleG mname -> Map Name AbstractType
mPrimTypes ModuleG ignored
m
, ifDecls :: Map Name IfaceDecl
ifDecls = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
qn,Decl -> IfaceDecl
mkIfaceDecl Decl
d)
| DeclGroup
dg <- forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ignored
m
, Decl
d <- DeclGroup -> [Decl]
groupDecls DeclGroup
dg
, let qn :: Name
qn = Decl -> Name
dName Decl
d
]
, ifModules :: Map Name (IfaceNames Name)
ifModules = forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG ignored
m
, ifSignatures :: Map Name ModParamNames
ifSignatures = forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG ignored
m
, ifFunctors :: Map Name (IfaceG Name)
ifFunctors = forall name. ModuleG name -> IfaceG name
genIface forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG ignored
m
}
, ifParams :: FunctorParams
ifParams = forall mname. ModuleG mname -> FunctorParams
mParams ModuleG ignored
m
}