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

Instances details

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 # (/=) :: 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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 # (/=) :: 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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

Instances details

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.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 #
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.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "Supply" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

Names

Instances

Instances

Instances

Creation

Unique Supply

Instances

Instances

Instances

PrimMap

Instances