cryptol-2.8.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

- data Iface = Iface {
  - ifModName :: !ModName
  - 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
  }
- 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 String
  }
- mkIfaceDecl :: Decl -> IfaceDecl
- data IfaceParams = IfaceParams {
  - ifParamTypes :: Map Name ModTParam
  - ifParamConstraints :: [Located Prop]
  - ifParamFuns :: Map Name ModVParam
  }
- genIface :: Module -> Iface
- ifacePrimMap :: Iface -> PrimMap
- noIfaceParams :: IfaceParams

# Documentation

data Iface Source #

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

Constructors

Iface |

Fields

- ifModName :: !ModName

  Module name

- ifPublic :: IfaceDecls

  Exported definitions

- ifPrivate :: IfaceDecls

  Private defintiions

- ifParams :: IfaceParams

  Uninterpreted constants (aka module params)

#### Instances

Instances details

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

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep Iface = D1 ('MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "Iface" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ifModName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: 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

#### Instances

Instances details

Show IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecls -> ShowS Source # show :: IfaceDecls -> String Source # showList :: [IfaceDecls] -> ShowS 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 #
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 #
Monoid IfaceDecls Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods mempty :: IfaceDecls Source # mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls Source # mconcat :: [IfaceDecls] -> IfaceDecls 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

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 String

  Documentation

#### Instances

Instances details

Show IfaceDecl Source # |
Instance details Defined in Cryptol.ModuleSystem.Interface Methods showsPrec :: Int -> IfaceDecl -> ShowS Source # show :: IfaceDecl -> String Source # showList :: [IfaceDecl] -> ShowS Source #
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 #
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-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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 String))))))

mkIfaceDecl :: Decl -> IfaceDecl Source #

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

Instance details

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceParams = D1 ('MetaData "IfaceParams" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))

genIface :: Module -> Iface Source #

Generate an Iface from a typechecked module.

ifacePrimMap :: Iface -> PrimMap Source #

Produce a PrimMap from an interface.

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

noIfaceParams :: IfaceParams Source #