Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Cryptol.ModuleSystem.Interface

Description

Synopsis

type Iface = IfaceG ModName
data IfaceG mname = Iface {
- ifModName :: !mname
- ifPublic :: IfaceDecls
- ifPrivate :: IfaceDecls
- ifParams :: IfaceParams
}
data IfaceDecls = IfaceDecls {
- ifTySyns :: Map Name IfaceTySyn
- ifNewtypes :: Map Name IfaceNewtype
- ifAbstractTypes :: Map Name IfaceAbstractType
- ifDecls :: Map Name IfaceDecl
- ifModules :: !(Map Name (IfaceG Name))
}
type IfaceTySyn = TySyn
ifTySynName :: TySyn -> Name
type IfaceNewtype = Newtype
data IfaceDecl = IfaceDecl {
- ifDeclName :: !Name
- ifDeclSig :: Schema
- ifDeclPragmas :: [Pragma]
- ifDeclInfix :: Bool
- ifDeclFixity :: Maybe Fixity
- ifDeclDoc :: Maybe Text
}
data IfaceParams = IfaceParams {
- ifParamTypes :: Map Name ModTParam
- ifParamConstraints :: [Located Prop]
- ifParamFuns :: Map Name ModVParam
}
emptyIface :: mname -> IfaceG mname
ifacePrimMap :: Iface -> PrimMap
noIfaceParams :: IfaceParams
isEmptyIfaceParams :: IfaceParams -> Bool
ifaceIsFunctor :: IfaceG mname -> Bool
flatPublicIface :: IfaceG mname -> IfaceDecls
flatPublicDecls :: IfaceDecls -> IfaceDecls
filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
ifaceDeclsNames :: IfaceDecls -> Set Name

Documentation

type Iface = IfaceG ModName Source #

data IfaceG mname Source #

The resulting interface generated by a module that has been typechecked.

Constructors

Iface
Fields ifModName :: !mname Module name ifPublic :: IfaceDecls Exported definitions ifPrivate :: IfaceDecls Private defintiions ifParams :: IfaceParams Uninterpreted constants (aka module params)

Instances

Instances details

Show mname => Show (IfaceG mname) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceG mname -> ShowS # show :: IfaceG mname -> String # showList :: [IfaceG mname] -> ShowS #
Generic (IfaceG mname) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep (IfaceG mname) :: Type -> Type # Methods from :: IfaceG mname -> Rep (IfaceG mname) x # to :: Rep (IfaceG mname) x -> IfaceG mname #
NFData mname => NFData (IfaceG mname) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceG mname -> () #
type Rep (IfaceG mname) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep (IfaceG mname) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifModName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 mname) :: S1 ('MetaSel ('Just "ifPublic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls)) :: (S1 ('MetaSel ('Just "ifPrivate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls) :*: S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceParams))))

data IfaceDecls Source #

Constructors

IfaceDecls
Fields ifTySyns :: Map Name IfaceTySyn ifNewtypes :: Map Name IfaceNewtype ifAbstractTypes :: Map Name IfaceAbstractType ifDecls :: Map Name IfaceDecl ifModules :: !(Map Name (IfaceG Name))

Instances

Instances details

Show IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS #
Generic IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecls :: Type -> Type # Methods from :: IfaceDecls -> Rep IfaceDecls x # to :: Rep IfaceDecls x -> IfaceDecls #
Semigroup IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls # sconcat :: NonEmpty IfaceDecls -> IfaceDecls # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls #
Monoid IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> IfaceDecls #
NFData IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () #
type Rep IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecls

type IfaceTySyn = TySyn Source #

ifTySynName :: TySyn -> Name Source #

type IfaceNewtype = Newtype Source #

data IfaceDecl Source #

Constructors

IfaceDecl
Fields ifDeclName :: !Name Name of thing ifDeclSig :: Schema Type ifDeclPragmas :: [Pragma] Pragmas ifDeclInfix :: Bool Is this an infix thing ifDeclFixity :: Maybe Fixity Fixity information ifDeclDoc :: Maybe Text Documentation

Instances

Instances details

Show IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecl -> ShowS # show :: IfaceDecl -> String # showList :: [IfaceDecl] -> ShowS #
Generic IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecl :: Type -> Type # Methods from :: IfaceDecl -> Rep IfaceDecl x # to :: Rep IfaceDecl x -> IfaceDecl #
NFData IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecl -> () #
type Rep IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep IfaceDecl = D1 ('MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "IfaceDecl" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifDeclName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :: (S1 ('MetaSel ('Just "ifDeclSig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema) :: S1 ('MetaSel ('Just "ifDeclPragmas") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Pragma]))) :: (S1 ('MetaSel ('Just "ifDeclInfix") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "ifDeclFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "ifDeclDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data IfaceParams Source #

Constructors

IfaceParams
Fields ifParamTypes :: Map Name ModTParam ifParamConstraints :: [Located Prop] Constraints on param. types ifParamFuns :: Map Name ModVParam

Instances

Instances details

Show IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceParams -> ShowS # show :: IfaceParams -> String # showList :: [IfaceParams] -> ShowS #
Generic IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceParams :: Type -> Type # Methods from :: IfaceParams -> Rep IfaceParams x # to :: Rep IfaceParams x -> IfaceParams #
NFData IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceParams -> () #
type Rep IfaceParams Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep IfaceParams = D1 ('MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "IfaceParams" 'PrefixI 'True) (S1 ('MetaSel ('Just "ifParamTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam)) :: (S1 ('MetaSel ('Just "ifParamConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :: S1 ('MetaSel ('Just "ifParamFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam)))))

emptyIface :: mname -> IfaceG mname Source #

ifacePrimMap :: Iface -> PrimMap Source #

Produce a PrimMap from an interface.

NOTE: the map will expose both public and private names.

noIfaceParams :: IfaceParams Source #

isEmptyIfaceParams :: IfaceParams -> Bool Source #

ifaceIsFunctor :: IfaceG mname -> Bool Source #

flatPublicIface :: IfaceG mname -> IfaceDecls Source #

The public declarations in all modules, including nested The modules field contains public functors Assumes that we are not a functor.

flatPublicDecls :: IfaceDecls -> IfaceDecls Source #

filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls Source #

ifaceDeclsNames :: IfaceDecls -> Set Name Source #