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 representing a typechecked 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 defined 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)

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep (IfaceG name) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 completely 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

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecls = D1 ('MetaData "IfaceDecls" "Cryptol.ModuleSystem.Interface" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecl = D1 ('MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep (IfaceNames name) = D1 ('MetaData "IfaceNames" "Cryptol.ModuleSystem.Interface" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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])))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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, compute 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.