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

Cryptol.ModuleSystem.Name

Contents

Names

Description

Synopsis

data Name
data NameInfo
- = GlobalName NameSource OrigName
- | LocalName Namespace Ident
data NameSource
- = SystemName
- | UserName
nameUnique :: Name -> Int
nameIdent :: Name -> Ident
mapNameIdent :: (Ident -> Ident) -> Name -> Name
nameInfo :: Name -> NameInfo
nameLoc :: Name -> Range
nameFixity :: Name -> Maybe Fixity
nameNamespace :: Name -> Namespace
nameToDefPName :: Name -> PName
asPrim :: Name -> Maybe PrimIdent
asOrigName :: Name -> Maybe OrigName
nameModPath :: Name -> ModPath
nameModPathMaybe :: Name -> Maybe ModPath
nameTopModule :: Name -> ModName
nameTopModuleMaybe :: Name -> Maybe ModName
ppLocName :: Name -> Doc
data Namespace
- = NSValue
- | NSConstructor
- | NSType
- | NSModule
data ModPath
- = TopModule ModName
- | Nested ModPath Ident
cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering
mkDeclared :: Namespace -> ModPath -> NameSource -> Ident -> Maybe Fixity -> Range -> Supply -> (Name, Supply)
mkLocal :: Namespace -> Ident -> Range -> Supply -> (Name, Supply)
asLocal :: Namespace -> Name -> Name
mkModParam :: ModPath -> Ident -> Range -> Name -> Supply -> (Name, Supply)
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)
runSupply :: Supply -> (forall m. FreshM m => m a) -> (a, Supply)
data Supply
emptySupply :: Supply
nextUnique :: Supply -> (Int, Supply)
freshNameFor :: ModPath -> Name -> Supply -> (Name, 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

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 #
Show Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
TraverseNames Name Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Name -> f Name Source #
ModuleInstance Name Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Name -> Name Source #
ShowParseable Name Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Name -> Doc Void Source #
PP Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppPrec :: Int -> Name -> Doc Source #
PPName Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods ppNameFixity :: Name -> Maybe Fixity Source # ppPrefixName :: Name -> Doc Source # ppInfixName :: Name -> Doc Source #
NFData Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Name -> () #
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 #
type Rep Name Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 "nFixity") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Fixity)) :*: S1 ('MetaSel ('Just "nLoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range))))

data NameInfo Source #

Constructors

GlobalName NameSource OrigName
LocalName Namespace Ident

Instances

Instances details

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 #
Show NameInfo Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> NameInfo -> ShowS # show :: NameInfo -> String # showList :: [NameInfo] -> ShowS #
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-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "GlobalName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameSource) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OrigName)) :+: C1 ('MetaCons "LocalName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Namespace) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)))

data NameSource Source #

Constructors

SystemName
UserName

Instances

Instances details

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 #
Show NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> NameSource -> ShowS # show :: NameSource -> String # showList :: [NameSource] -> ShowS #
NFData NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: NameSource -> () #
Eq NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: NameSource -> NameSource -> Bool # (/=) :: NameSource -> NameSource -> Bool #
type Rep NameSource Source #
Instance details Defined in Cryptol.ModuleSystem.Name type Rep NameSource = D1 ('MetaData "NameSource" "Cryptol.ModuleSystem.Name" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 #

mapNameIdent :: (Ident -> Ident) -> Name -> Name Source #

nameInfo :: Name -> NameInfo Source #

nameLoc :: Name -> Range Source #

nameFixity :: Name -> Maybe Fixity Source #

nameNamespace :: Name -> Namespace Source #

nameToDefPName :: Name -> PName Source #

Compute a PName for the definition site corresponding to the given Name. Usually this is an unqualified name, but names that come from module parameters are qualified with the corresponding parameter name.

asPrim :: Name -> Maybe PrimIdent Source #

Primtiives must be in a top level module, at least for now.

asOrigName :: Name -> Maybe OrigName Source #

nameModPath :: Name -> ModPath Source #

Get the module path for the given name. The name should be a top-level name.

nameModPathMaybe :: Name -> Maybe ModPath Source #

Get the module path for the given name.

nameTopModule :: Name -> ModName Source #

Get the name of the top-level module that introduced this name. Works only for top-level names (i.e., that have original names)

nameTopModuleMaybe :: Name -> Maybe ModName Source #

Get the name of the top-level module that introduced this name.

ppLocName :: Name -> Doc Source #

Pretty-print a name with its source location information.

data Namespace Source #

Namespaces for names

Constructors

NSValue
NSConstructor	This is for enum and newtype constructors
NSType
NSModule

Instances

Instances details

Bounded Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Methods minBound :: Namespace # maxBound :: Namespace #
Enum Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Methods succ :: Namespace -> Namespace # pred :: Namespace -> Namespace # toEnum :: Int -> Namespace # fromEnum :: Namespace -> Int # enumFrom :: Namespace -> [Namespace] # enumFromThen :: Namespace -> Namespace -> [Namespace] # enumFromTo :: Namespace -> Namespace -> [Namespace] # enumFromThenTo :: Namespace -> Namespace -> Namespace -> [Namespace] #
Generic Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep Namespace :: Type -> Type # Methods from :: Namespace -> Rep Namespace x # to :: Rep Namespace x -> Namespace #
Show Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> Namespace -> ShowS # show :: Namespace -> String # showList :: [Namespace] -> ShowS #
PP Namespace Source #
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> Namespace -> Doc Source #
NFData Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: Namespace -> () #
Eq Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: Namespace -> Namespace -> Bool # (/=) :: Namespace -> Namespace -> Bool #
Ord Namespace Source #
Instance details Defined in Cryptol.Utils.Ident Methods compare :: Namespace -> Namespace -> Ordering # (<) :: Namespace -> Namespace -> Bool # (<=) :: Namespace -> Namespace -> Bool # (>) :: Namespace -> Namespace -> Bool # (>=) :: Namespace -> Namespace -> Bool # max :: Namespace -> Namespace -> Namespace # min :: Namespace -> Namespace -> Namespace #
type Rep Namespace Source #
Instance details Defined in Cryptol.Utils.Ident type Rep Namespace = D1 ('MetaData "Namespace" "Cryptol.Utils.Ident" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) ((C1 ('MetaCons "NSValue" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NSConstructor" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NSType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NSModule" 'PrefixI 'False) (U1 :: Type -> Type)))

data ModPath Source #

Idnetifies a possibly nested module

Constructors

TopModule ModName
Nested ModPath Ident

Instances

Instances details

Generic ModPath Source #
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep ModPath :: Type -> Type # Methods from :: ModPath -> Rep ModPath x # to :: Rep ModPath x -> ModPath #
Show ModPath Source #
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> ModPath -> ShowS # show :: ModPath -> String # showList :: [ModPath] -> ShowS #
PP ModPath Source #
Instance details Defined in Cryptol.Utils.PP Methods ppPrec :: Int -> ModPath -> Doc Source #
NFData ModPath Source #
Instance details Defined in Cryptol.Utils.Ident Methods rnf :: ModPath -> () #
Eq ModPath Source #
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: ModPath -> ModPath -> Bool # (/=) :: ModPath -> ModPath -> Bool #
Ord ModPath Source #
Instance details Defined in Cryptol.Utils.Ident Methods compare :: ModPath -> ModPath -> Ordering # (<) :: ModPath -> ModPath -> Bool # (<=) :: ModPath -> ModPath -> Bool # (>) :: ModPath -> ModPath -> Bool # (>=) :: ModPath -> ModPath -> Bool # max :: ModPath -> ModPath -> ModPath # min :: ModPath -> ModPath -> ModPath #
type Rep ModPath Source #
Instance details Defined in Cryptol.Utils.Ident type Rep ModPath = D1 ('MetaData "ModPath" "Cryptol.Utils.Ident" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "TopModule" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModName)) :+: C1 ('MetaCons "Nested" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModPath) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)))

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

Compare two names by the way they would be displayed. This is used to order names nicely when showing what's in scope

Creation

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

Make a new name for a declaration.

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

Make a new parameter name.

asLocal :: Namespace -> Name -> Name Source #

Make a local name derived from the given name. This is a bit questionable, but it is used by the translation to SAW Core

mkModParam Source #

Arguments

:: ModPath	Module containing the parameter
-> Ident	Name of the module parameter
-> Range	Location
-> Name	Name in the signature
-> Supply
-> (Name, Supply)

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.Monad 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 #
FreshM InferM Source #
Instance details Defined in Cryptol.TypeCheck.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> InferM a Source #
Monad m => FreshM (ModuleT m) Source #
Instance details Defined in Cryptol.ModuleSystem.Monad Methods liftSupply :: (Supply -> (a, Supply)) -> ModuleT 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 #
FreshM m => FreshM (ExceptionT i m) Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> ExceptionT i 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 #
FreshM m => FreshM (StateT i m) Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods liftSupply :: (Supply -> (a, Supply)) -> StateT 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 #

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 #
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 => 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 #
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 => 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 #

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

runSupply :: Supply -> (forall m. FreshM m => m a) -> (a, Supply) Source #

data Supply Source #

Instances

Instances details

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 #
Show Supply Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Supply -> ShowS # show :: Supply -> String # showList :: [Supply] -> ShowS #
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-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 #

freshNameFor :: ModPath -> Name -> Supply -> (Name, Supply) Source #

This is used when instantiating functors

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

Semigroup PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods (<>) :: PrimMap -> PrimMap -> PrimMap # sconcat :: NonEmpty PrimMap -> PrimMap # stimes :: Integral b => b -> PrimMap -> PrimMap #
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 #
Show PrimMap Source #
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> PrimMap -> ShowS # show :: PrimMap -> String # showList :: [PrimMap] -> ShowS #
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-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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.