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

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 PrimIdent
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 PrimIdent Name
- primTypes :: Map PrimIdent Name
}
lookupPrimDecl :: PrimIdent -> PrimMap -> Name
lookupPrimType :: PrimIdent -> PrimMap -> Name

Names

data Name Source #

Instances

Eq Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Show Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
Generic Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep Name :: Type -> Type # Methods from :: Name -> Rep Name x # to :: Rep Name x -> Name #
NFData Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Name -> () #
PPName Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppNameFixity :: Name -> Maybe Fixity 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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Eq NameInfo Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: NameInfo -> NameInfo -> Bool # (/=) :: NameInfo -> NameInfo -> Bool #
Show NameInfo Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> NameInfo -> ShowS # show :: NameInfo -> String # showList :: [NameInfo] -> ShowS #
Generic NameInfo Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep NameInfo :: Type -> Type # Methods from :: NameInfo -> Rep NameInfo x # to :: Rep NameInfo x -> NameInfo #
NFData NameInfo Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: NameInfo -> () #
type Rep NameInfo Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep NameInfo = D1 (MetaData "NameInfo" "Cryptol.ModuleSystem.Name" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

Eq NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: NameSource -> NameSource -> Bool # (/=) :: NameSource -> NameSource -> Bool #
Show NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> NameSource -> ShowS # show :: NameSource -> String # showList :: [NameSource] -> ShowS #
Generic NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep NameSource :: Type -> Type # Methods from :: NameSource -> Rep NameSource x # to :: Rep NameSource x -> NameSource #
NFData NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: NameSource -> () #
type Rep NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep NameSource = D1 (MetaData "NameSource" "Cryptol.ModuleSystem.Name" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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 PrimIdent 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 #

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 PrimIdent Name primTypes :: Map PrimIdent Name

Instances

Show PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> PrimMap -> ShowS # show :: PrimMap -> String # showList :: [PrimMap] -> ShowS #
Generic PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep PrimMap :: Type -> Type # Methods from :: PrimMap -> Rep PrimMap x # to :: Rep PrimMap x -> PrimMap #
Semigroup PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (<>) :: PrimMap -> PrimMap -> PrimMap # sconcat :: NonEmpty PrimMap -> PrimMap # stimes :: Integral b => b -> PrimMap -> PrimMap #
NFData PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: PrimMap -> () #
type Rep PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep PrimMap = D1 (MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" False) (C1 (MetaCons "PrimMap" PrefixI True) (S1 (MetaSel (Just "primDecls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map PrimIdent Name)) :*: S1 (MetaSel (Just "primTypes") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Map PrimIdent Name))))

lookupPrimDecl :: PrimIdent -> 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 :: PrimIdent -> 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.

FreshM InferM Source #
Instance details Defined in Cryptol.TypeCheck.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> InferM a Source #
FreshM RenameM Source #
Instance details Defined in Cryptol.ModuleSystem.Renamer Methods liftSupply :: (Supply -> (a, Supply)) -> RenameM 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 #

MonadT SupplyT Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods lift :: Monad m => m a -> SupplyT m a #
Monad m => Monad (SupplyT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (>>=) :: SupplyT m a -> (a -> SupplyT m b) -> SupplyT m b # (>>) :: SupplyT m a -> SupplyT m b -> SupplyT m b # return :: a -> SupplyT m a # fail :: String -> SupplyT m a #
Monad m => Functor (SupplyT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods fmap :: (a -> b) -> SupplyT m a -> SupplyT m b # (<$) :: a -> SupplyT m b -> SupplyT m a #
MonadFix m => MonadFix (SupplyT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods mfix :: (a -> SupplyT m a) -> SupplyT m a #
Monad m => Applicative (SupplyT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods pure :: a -> SupplyT m a # (<>) :: SupplyT m (a -> b) -> SupplyT m a -> SupplyT m b # liftA2 :: (a -> b -> c) -> SupplyT m a -> SupplyT m b -> SupplyT m c # (>) :: SupplyT m a -> SupplyT m b -> SupplyT m b # (<*) :: SupplyT m a -> SupplyT m b -> SupplyT m a #
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 #
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 #

Show Supply Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Supply -> ShowS # show :: Supply -> String # showList :: [Supply] -> ShowS #
Generic Supply Source #
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep Supply :: Type -> Type # Methods from :: Supply -> Rep Supply x # to :: Rep Supply x -> Supply #
NFData Supply Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Supply -> () #
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 #
type Rep Supply Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep Supply = D1 (MetaData "Supply" "Cryptol.ModuleSystem.Name" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" False) (C1 (MetaCons "Supply" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)))

Names

Creation

Unique Supply

PrimMap