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

Cryptol.ModuleSystem.Interface

Description

Synopsis

type Iface = IfaceG ModName
data IfaceG name = Iface {
- ifNames :: IfaceNames name
- ifParams :: FunctorParams
- ifDefines :: IfaceDecls
}
data IfaceDecls = IfaceDecls {
- ifTySyns :: Map Name TySyn
- ifNominalTypes :: Map Name NominalType
- ifDecls :: Map Name IfaceDecl
- ifModules :: !(Map Name (IfaceNames Name))
- ifSignatures :: !(Map Name ModParamNames)
- ifFunctors :: !(Map Name (IfaceG Name))
}
data IfaceDecl = IfaceDecl {
- ifDeclName :: !Name
- ifDeclSig :: Schema
- ifDeclIsPrim :: !Bool
- ifDeclPragmas :: [Pragma]
- ifDeclInfix :: Bool
- ifDeclFixity :: Maybe Fixity
- ifDeclDoc :: Maybe Text
}
data IfaceNames name = IfaceNames {
- ifsName :: name
- ifsNested :: Set Name
- ifsDefines :: Set Name
- ifsPublic :: Set Name
- ifsDoc :: ![Text]
}
ifModName :: IfaceG name -> name
emptyIface :: ModName -> Iface
ifacePrimMap :: Iface -> PrimMap
ifaceForgetName :: IfaceG name -> IfaceG ()
ifaceIsFunctor :: IfaceG name -> Bool
filterIfaceDecls :: (Name -> Bool) -> IfaceDecls -> IfaceDecls
ifaceDeclsNames :: IfaceDecls -> Set Name
ifaceOrigNameMap :: IfaceG name -> Map Namespace (Map OrigName Name)
ifaceNameToModuleMap :: Iface -> Map Name (ImpName Name)

Documentation

type Iface = IfaceG ModName Source #

data IfaceG name Source #

The interface repersenting a typecheck top-level module.

Constructors

Iface
Fields ifNames :: IfaceNames name Info about names in this module ifParams :: FunctorParams Module parameters, if any ifDefines :: IfaceDecls All things defines in the module (includes nested definitions)

Instances

Instances details

Functor IfaceG Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods fmap :: (a -> b) -> IfaceG a -> IfaceG b # (<$) :: a -> IfaceG b -> IfaceG a #
Generic (IfaceG name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep (IfaceG name) :: Type -> Type # Methods from :: IfaceG name -> Rep (IfaceG name) x # to :: Rep (IfaceG name) x -> IfaceG name #
Show name => Show (IfaceG name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceG name -> ShowS # show :: IfaceG name -> String # showList :: [IfaceG name] -> ShowS #
NFData name => NFData (IfaceG name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceG name -> () #
type Rep (IfaceG name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep (IfaceG name) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) (S1 ('MetaSel ('Just "ifNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (IfaceNames name)) :: (S1 ('MetaSel ('Just "ifParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunctorParams) :: S1 ('MetaSel ('Just "ifDefines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IfaceDecls))))

data IfaceDecls Source #

Declarations in a module. Note that this includes things from nested modules, but not things from nested functors, which are in ifFunctors.

Constructors

IfaceDecls

Fields

ifTySyns :: Map Name TySyn
ifNominalTypes :: Map Name NominalType
ifDecls :: Map Name IfaceDecl
ifModules :: !(Map Name (IfaceNames Name))
ifSignatures :: !(Map Name ModParamNames)
ifFunctors :: !(Map Name (IfaceG Name))
XXX: Maybe arg info? Also, with the current implementation we aim to complete remove functors by essentially inlining them. To achieve this with just interfaces we'd have to store here the entire module, not just its interface. At the moment we work around this by passing all loaded modules to the type checker, so it looks up functors there, instead of in the interfaces, but we'd need to change this if we want better support for separate compilation.

Instances

Instances details

Monoid IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls # mconcat :: [IfaceDecls] -> 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 #
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 #
Show IfaceDecls Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS # show :: IfaceDecls -> String # showList :: [IfaceDecls] -> ShowS #
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 = D1 ('MetaData "IfaceDecls" "Cryptol.ModuleSystem.Interface" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "IfaceDecls" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :: (S1 ('MetaSel ('Just "ifNominalTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name NominalType)) :: S1 ('MetaSel ('Just "ifDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name IfaceDecl)))) :: (S1 ('MetaSel ('Just "ifModules") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name (IfaceNames Name))) :: (S1 ('MetaSel ('Just "ifSignatures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name ModParamNames)) :*: S1 ('MetaSel ('Just "ifFunctors") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name (IfaceG Name)))))))

data IfaceDecl Source #

Constructors

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

Instances

Instances details

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 #
Show IfaceDecl Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecl -> ShowS # show :: IfaceDecl -> String # showList :: [IfaceDecl] -> ShowS #
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-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 "ifDeclIsPrim") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Bool))) :: ((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 IfaceNames name Source #

Information about the names in a module.

Constructors

IfaceNames
Fields ifsName :: name Name of this submodule ifsNested :: Set Name Things nested in this module ifsDefines :: Set Name Things defined in this module ifsPublic :: Set Name Subset of `ifsDefines` that is public ifsDoc :: ![Text] Documentation: more specific to least specific

Instances

Instances details

Functor IfaceNames Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods fmap :: (a -> b) -> IfaceNames a -> IfaceNames b # (<$) :: a -> IfaceNames b -> IfaceNames a #
Generic (IfaceNames name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep (IfaceNames name) :: Type -> Type # Methods from :: IfaceNames name -> Rep (IfaceNames name) x # to :: Rep (IfaceNames name) x -> IfaceNames name #
Show name => Show (IfaceNames name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceNames name -> ShowS # show :: IfaceNames name -> String # showList :: [IfaceNames name] -> ShowS #
ModuleInstance name => ModuleInstance (IfaceNames name) Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: IfaceNames name -> IfaceNames name Source #
NFData name => NFData (IfaceNames name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceNames name -> () #
type Rep (IfaceNames name) Source #
Instance details Defined in Cryptol.ModuleSystem.Interface type Rep (IfaceNames name) = D1 ('MetaData "IfaceNames" "Cryptol.ModuleSystem.Interface" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "IfaceNames" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 name) :: S1 ('MetaSel ('Just "ifsNested") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name))) :: (S1 ('MetaSel ('Just "ifsDefines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :: (S1 ('MetaSel ('Just "ifsPublic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Name)) :: S1 ('MetaSel ('Just "ifsDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Text])))))

ifModName :: IfaceG name -> name Source #

Access the name of a module.

emptyIface :: ModName -> Iface Source #

ifacePrimMap :: Iface -> PrimMap Source #

Produce a PrimMap from an interface.

NOTE: the map will expose both public and private names. NOTE: this is a bit misnamed, as it is used to resolve known names that Cryptol introduces (e.g., during type checking). These names need not be primitives. A better way to do this in the future might be to use original names instead (see #1522).

ifaceForgetName :: IfaceG name -> IfaceG () Source #

Remove the name of a module. This is useful for dealing with collections of modules, as in `Map (ImpName Name) (IfaceG ())`.

ifaceIsFunctor :: IfaceG name -> Bool Source #

Is this interface for a functor.

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

ifaceDeclsNames :: IfaceDecls -> Set Name Source #

ifaceOrigNameMap :: IfaceG name -> Map Namespace (Map OrigName Name) Source #

Given an interface computing a map from original names to actual names, grouped by namespace.

ifaceNameToModuleMap :: Iface -> Map Name (ImpName Name) Source #

For every name in the interface compute the direct module that defines it. This does not traverse into functors or interfaces.