cryptol-3.0.0: Cryptol: The Language of Cryptography

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
  - ifNewtypes :: Map Name Newtype
  - ifAbstractTypes :: Map Name AbstractType
  - 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 :: !(Maybe 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)

# 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

Generic (IfaceG name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep (IfaceG name) :: Type -> Type Source # Methods from :: IfaceG name -> Rep (IfaceG name) x Source # to :: Rep (IfaceG name) x -> IfaceG name Source #
Show name => Show (IfaceG name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceG name -> ShowS Source # show :: IfaceG name -> String Source # showList :: [IfaceG name] -> ShowS Source #
NFData name => NFData (IfaceG name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceG name -> () Source #
type Rep (IfaceG name) Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep (IfaceG name) = D1 ('MetaData "IfaceG" "Cryptol.ModuleSystem.Interface" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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
- ifNewtypes :: Map Name Newtype
- ifAbstractTypes :: Map Name AbstractType
- 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 Source # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls Source # mconcat :: [IfaceDecls] -> IfaceDecls Source #
Semigroup IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods (<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls Source # sconcat :: NonEmpty IfaceDecls -> IfaceDecls Source # stimes :: Integral b => b -> IfaceDecls -> IfaceDecls Source #
Generic IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep IfaceDecls :: Type -> Type Source # Methods from :: IfaceDecls -> Rep IfaceDecls x Source # to :: Rep IfaceDecls x -> IfaceDecls Source #
Show IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS Source # show :: IfaceDecls -> String Source # showList :: [IfaceDecls] -> ShowS Source #
NFData IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecls -> () Source #
type Rep IfaceDecls Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecls = D1 ('MetaData "IfaceDecls" "Cryptol.ModuleSystem.Interface" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "IfaceDecls" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifTySyns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name TySyn)) :*: (S1 ('MetaSel ('Just "ifNewtypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name Newtype)) :*: S1 ('MetaSel ('Just "ifAbstractTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name AbstractType)))) :*: ((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 Source # Methods from :: IfaceDecl -> Rep IfaceDecl x Source # to :: Rep IfaceDecl x -> IfaceDecl Source #
Show IfaceDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecl -> ShowS Source # show :: IfaceDecl -> String Source # showList :: [IfaceDecl] -> ShowS Source #
NFData IfaceDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods rnf :: IfaceDecl -> () Source #
type Rep IfaceDecl Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecl = D1 ('MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 :: !(Maybe Text)

  Documentation

#### Instances

Instances details

Generic (IfaceNames name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Associated Types type Rep (IfaceNames name) :: Type -> Type Source # Methods from :: IfaceNames name -> Rep (IfaceNames name) x Source # to :: Rep (IfaceNames name) x -> IfaceNames name Source #
Show name => Show (IfaceNames name) Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceNames name -> ShowS Source # show :: IfaceNames name -> String Source # showList :: [IfaceNames name] -> ShowS Source #
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 -> () Source #
type Rep (IfaceNames name) Source # |

Instance details

Defined in Cryptol.ModuleSystem.Interface

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