cryptol-2.8.0: Cryptol: The Language of Cryptography

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

Cryptol.ModuleSystem.Name

Contents

- Names
  - Creation
  - Unique Supply
  - PrimMap

Description

Synopsis

- data Name
- data NameInfo
  - = Declared !ModName !NameSource
  - | Parameter
- data NameSource
  - = SystemName
  - | UserName
- nameUnique :: Name -> Int
- nameIdent :: Name -> Ident
- nameInfo :: Name -> NameInfo
- nameLoc :: Name -> Range
- nameFixity :: Name -> Maybe Fixity
- asPrim :: Name -> Maybe Ident
- cmpNameLexical :: Name -> Name -> Ordering
- cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
- ppLocName :: Name -> Doc
- mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name, Supply)
- mkParameter :: Ident -> Range -> Supply -> (Name, Supply)
- toParamInstName :: Name -> Name
- asParamName :: Name -> Name
- paramModRecParam :: Name
- class Monad m => FreshM m where
  - liftSupply :: (Supply -> (a, Supply)) -> m a
- nextUniqueM :: FreshM m => m Int
- data SupplyT m a
- runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a, Supply)
- data Supply
- emptySupply :: Supply
- nextUnique :: Supply -> (Int, Supply)
- data PrimMap = PrimMap {
  - primDecls :: Map Ident Name
  - primTypes :: Map Ident Name
  }
- lookupPrimDecl :: Ident -> PrimMap -> Name
- lookupPrimType :: Ident -> PrimMap -> Name

# Names

data Name Source #

#### Instances

Instances details

Eq Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
Show Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
Generic Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep Name :: Type -> Type Source # Methods from :: Name -> Rep Name x Source # to :: Rep Name x -> Name Source #
NFData Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Name -> () Source #
PPName Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppNameFixity :: Name -> Maybe (Assoc, Int) Source # ppPrefixName :: Name -> Doc Source # ppInfixName :: Name -> Doc Source #
PP Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppPrec :: Int -> Name -> Doc Source #
ShowParseable Name Source # |
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Name -> Doc Source #
FromDecl (Decl Name) Source # |
Instance details Defined in Cryptol.TypeCheck.Depends Methods toBind :: Decl Name -> Maybe (Bind Name) Source # toParamFun :: Decl Name -> Maybe (ParameterFun Name) Source # toParamConstraints :: Decl Name -> [Located (Prop Name)] Source # toTyDecl :: Decl Name -> Maybe TyDecl Source # isTopDecl :: Decl Name -> Bool Source #
FromDecl (TopDecl Name) Source # |
Instance details Defined in Cryptol.TypeCheck.Depends Methods toBind :: TopDecl Name -> Maybe (Bind Name) Source # toParamFun :: TopDecl Name -> Maybe (ParameterFun Name) Source # toParamConstraints :: TopDecl Name -> [Located (Prop Name)] Source # toTyDecl :: TopDecl Name -> Maybe TyDecl Source # isTopDecl :: TopDecl Name -> Bool Source #
type Rep Name Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "Name" 'PrefixI 'True) ((S1 ('MetaSel ('Just "nUnique") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "nInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NameInfo)) :*: (S1 ('MetaSel ('Just "nIdent") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Ident) :*: (S1 ('MetaSel ('Just "nFixity") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "nLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range)))))

data NameInfo Source #

Information about the binding site of the name.

Constructors

Declared !ModName !NameSource | This name refers to a declaration from this module
Parameter | This name is a parameter (function or type)

#### Instances

Instances details

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

Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep NameInfo = D1 ('MetaData "NameInfo" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "Declared" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NameSource)) :+: C1 ('MetaCons "Parameter" 'PrefixI 'False) (U1 :: Type -> Type))

data NameSource Source #

Constructors

SystemName |
UserName |

#### Instances

Instances details

Eq NameSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: NameSource -> NameSource -> Bool Source # (/=) :: NameSource -> NameSource -> Bool Source #
Show NameSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> NameSource -> ShowS Source # show :: NameSource -> String Source # showList :: [NameSource] -> ShowS Source #
Generic NameSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep NameSource :: Type -> Type Source # Methods from :: NameSource -> Rep NameSource x Source # to :: Rep NameSource x -> NameSource Source #
NFData NameSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: NameSource -> () Source #
type Rep NameSource Source # |
Instance details Defined in Cryptol.ModuleSystem.Name type Rep NameSource = D1 ('MetaData "NameSource" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "SystemName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserName" 'PrefixI 'False) (U1 :: Type -> Type))

nameUnique :: Name -> Int Source #

nameIdent :: Name -> Ident Source #

nameInfo :: Name -> NameInfo Source #

nameLoc :: Name -> Range Source #

nameFixity :: Name -> Maybe Fixity Source #

asPrim :: Name -> Maybe Ident Source #

cmpNameLexical :: Name -> Name -> Ordering Source #

Compare two names lexically.

cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering Source #

Compare two names by the way they would be displayed.

ppLocName :: Name -> Doc Source #

Pretty-print a name with its source location information.

## Creation

mkDeclared :: ModName -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name, Supply) Source #

Make a new name for a declaration.

mkParameter :: Ident -> Range -> Supply -> (Name, Supply) Source #

Make a new parameter name.

toParamInstName :: Name -> Name Source #

asParamName :: Name -> Name Source #

paramModRecParam :: Name Source #

## Unique Supply

class Monad m => FreshM m where Source #

Methods

liftSupply :: (Supply -> (a, Supply)) -> m a Source #

#### Instances

Instances details

FreshM RenameM Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods liftSupply :: (Supply -> (a, Supply)) -> RenameM a Source #
FreshM InferM Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> InferM a Source #
FreshM REPL Source # |
Instance details Defined in Cryptol.REPL.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> REPL a Source #
Monad m => FreshM (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> SupplyT m a Source #
Monad m => FreshM (ModuleT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> ModuleT m a Source #
FreshM m => FreshM (ReaderT i m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> ReaderT i m a Source #
(Monoid i, FreshM m) => FreshM (WriterT i m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> WriterT i m a Source #
FreshM m => FreshM (StateT i m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> StateT i m a Source #
FreshM m => FreshM (ExceptionT i m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> ExceptionT i m a Source #

nextUniqueM :: FreshM m => m Int Source #

Retrieve the next unique from the supply.

data SupplyT m a Source #

A monad for easing the use of the supply.

#### Instances

Instances details

MonadT SupplyT Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods lift :: Monad m => m a -> SupplyT m a Source #
Monad m => Monad (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (>>=) :: SupplyT m a -> (a -> SupplyT m b) -> SupplyT m b Source # (>>) :: SupplyT m a -> SupplyT m b -> SupplyT m b Source # return :: a -> SupplyT m a Source #
Monad m => Functor (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods fmap :: (a -> b) -> SupplyT m a -> SupplyT m b Source # (<$) :: a -> SupplyT m b -> SupplyT m a Source #
MonadFix m => MonadFix (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods mfix :: (a -> SupplyT m a) -> SupplyT m a Source #
Monad m => Applicative (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods pure :: a -> SupplyT m a Source # (<*>) :: SupplyT m (a -> b) -> SupplyT m a -> SupplyT m b Source # liftA2 :: (a -> b -> c) -> SupplyT m a -> SupplyT m b -> SupplyT m c Source # (*>) :: SupplyT m a -> SupplyT m b -> SupplyT m b Source # (<*) :: SupplyT m a -> SupplyT m b -> SupplyT m a Source #
Monad m => FreshM (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> SupplyT m a Source #
BaseM m n => BaseM (SupplyT m) n Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods inBase :: n a -> SupplyT m a Source #
RunM m (a, Supply) r => RunM (SupplyT m) a (Supply -> r) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods runM :: SupplyT m a -> Supply -> r Source #

runSupplyT :: Monad m => Supply -> SupplyT m a -> m (a, Supply) Source #

data Supply Source #

#### Instances

Instances details

Show Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Supply -> ShowS Source # show :: Supply -> String Source # showList :: [Supply] -> ShowS Source #
Generic Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep Supply :: Type -> Type Source # Methods from :: Supply -> Rep Supply x Source # to :: Rep Supply x -> Supply Source #
NFData Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Supply -> () Source #
RunM m (a, Supply) r => RunM (SupplyT m) a (Supply -> r) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods runM :: SupplyT m a -> Supply -> r Source #
type Rep Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name type Rep Supply = D1 ('MetaData "Supply" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "Supply" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

emptySupply :: Supply Source #

This should only be used once at library initialization, and threaded through the rest of the session. The supply is started at 0x1000 to leave us plenty of room for names that the compiler needs to know about (wired-in constants).

nextUnique :: Supply -> (Int, Supply) Source #

## PrimMap

data PrimMap Source #

A mapping from an identifier defined in some module to its real name.

Constructors

PrimMap |

Fields

- primDecls :: Map Ident Name
- primTypes :: Map Ident Name

#### Instances

Instances details

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

Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" 'False) (C1 ('MetaCons "PrimMap" 'PrefixI 'True) (S1 ('MetaSel ('Just "primDecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident Name)) :*: S1 ('MetaSel ('Just "primTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Ident Name))))

lookupPrimDecl :: Ident -> PrimMap -> Name Source #

It's assumed that we're looking things up that we know already exist, so this will panic if it doesn't find the name.

lookupPrimType :: Ident -> PrimMap -> Name Source #

It's assumed that we're looking things up that we know already exist, so this will panic if it doesn't find the name.