Cryptol.ModuleSystem.Interface

Documentation

data Iface

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

Show Iface

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> Iface -> ShowS

show :: Iface -> String

showList :: [Iface] -> ShowS

Generic Iface

Defined in Cryptol.ModuleSystem.Interface

Associated Types

type Rep Iface :: Type -> Type

Methods

from :: Iface -> Rep Iface x

to :: Rep Iface x -> Iface

NFData Iface

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: Iface -> ()

type Rep Iface

Defined in Cryptol.ModuleSystem.Interface

type Rep Iface = D1 (MetaData "Iface" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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

Constructors

IfaceDecls

Fields

• ifTySyns :: Map Name IfaceTySyn
• ifNewtypes :: Map Name IfaceNewtype
• ifAbstractTypes :: Map Name IfaceAbstractType
• ifDecls :: Map Name IfaceDecl

Instances

Show IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceDecls -> ShowS

show :: IfaceDecls -> String

showList :: [IfaceDecls] -> ShowS

Generic IfaceDecls

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

Defined in Cryptol.ModuleSystem.Interface

Methods

(<>) :: IfaceDecls -> IfaceDecls -> IfaceDecls

sconcat :: NonEmpty IfaceDecls -> IfaceDecls

stimes :: Integral b => b -> IfaceDecls -> IfaceDecls

Monoid IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

Methods

mempty :: IfaceDecls

mappend :: IfaceDecls -> IfaceDecls -> IfaceDecls

mconcat :: [IfaceDecls] -> IfaceDecls

NFData IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecls -> ()

type Rep IfaceDecls

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecls

type IfaceTySyn = TySyn

ifTySynName :: TySyn -> Name

type IfaceNewtype = Newtype

data IfaceDecl

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

Show IfaceDecl

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceDecl -> ShowS

show :: IfaceDecl -> String

showList :: [IfaceDecl] -> ShowS

Generic IfaceDecl

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

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceDecl -> ()

type Rep IfaceDecl

Defined in Cryptol.ModuleSystem.Interface

type Rep IfaceDecl = D1 (MetaData "IfaceDecl" "Cryptol.ModuleSystem.Interface" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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

data IfaceParams

Constructors

IfaceParams

Fields

• ifParamTypes :: Map Name ModTParam
• ifParamConstraints :: [Located Prop]

  Constraints on param. types

• ifParamFuns :: Map Name ModVParam

Instances

Show IfaceParams

Defined in Cryptol.ModuleSystem.Interface

Methods

showsPrec :: Int -> IfaceParams -> ShowS

show :: IfaceParams -> String

showList :: [IfaceParams] -> ShowS

Generic IfaceParams

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

Defined in Cryptol.ModuleSystem.Interface

Methods

rnf :: IfaceParams -> ()

type Rep IfaceParams

Defined in Cryptol.ModuleSystem.Interface

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

Generate an Iface from a typechecked module.

ifacePrimMap :: Iface -> PrimMap

Produce a PrimMap from an interface.

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

noIfaceParams :: IfaceParams