Cryptol.ModuleSystem.Name

Names

data Name

Instances

Eq Name

Defined in Cryptol.ModuleSystem.Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Ord Name

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

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

Generic Name

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

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: Name -> ()

PPName Name

Defined in Cryptol.ModuleSystem.Name

Methods

ppNameFixity :: Name -> Maybe Fixity

ppPrefixName :: Name -> Doc

ppInfixName :: Name -> Doc

PP Name

Defined in Cryptol.ModuleSystem.Name

Methods

ppPrec :: Int -> Name -> Doc

ShowParseable Name

Defined in Cryptol.TypeCheck.Parseable

Methods

showParseable :: Name -> Doc

FromDecl (Decl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: Decl Name -> Maybe (Bind Name)

toParamFun :: Decl Name -> Maybe (ParameterFun Name)

toParamConstraints :: Decl Name -> [Located (Prop Name)]

toTyDecl :: Decl Name -> Maybe TyDecl

isTopDecl :: Decl Name -> Bool

FromDecl (TopDecl Name)

Defined in Cryptol.TypeCheck.Depends

Methods

toBind :: TopDecl Name -> Maybe (Bind Name)

toParamFun :: TopDecl Name -> Maybe (ParameterFun Name)

toParamConstraints :: TopDecl Name -> [Located (Prop Name)]

toTyDecl :: TopDecl Name -> Maybe TyDecl

isTopDecl :: TopDecl Name -> Bool

type Rep Name

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

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

Defined in Cryptol.ModuleSystem.Name

Methods

(==) :: NameInfo -> NameInfo -> Bool

(/=) :: NameInfo -> NameInfo -> Bool

Show NameInfo

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> NameInfo -> ShowS

show :: NameInfo -> String

showList :: [NameInfo] -> ShowS

Generic NameInfo

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

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: NameInfo -> ()

type Rep NameInfo

Defined in Cryptol.ModuleSystem.Name

type Rep NameInfo = D1 ('MetaData "NameInfo" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

Constructors

SystemName

UserName

Instances

Eq NameSource

Defined in Cryptol.ModuleSystem.Name

Methods

(==) :: NameSource -> NameSource -> Bool

(/=) :: NameSource -> NameSource -> Bool

Show NameSource

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> NameSource -> ShowS

show :: NameSource -> String

showList :: [NameSource] -> ShowS

Generic NameSource

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

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: NameSource -> ()

type Rep NameSource

Defined in Cryptol.ModuleSystem.Name

type Rep NameSource = D1 ('MetaData "NameSource" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "SystemName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UserName" 'PrefixI 'False) (U1 :: Type -> Type))

nameUnique :: Name -> Int

nameIdent :: Name -> Ident

nameInfo :: Name -> NameInfo

nameLoc :: Name -> Range

nameFixity :: Name -> Maybe Fixity

asPrim :: Name -> Maybe PrimIdent

cmpNameLexical :: Name -> Name -> Ordering

Compare two names lexically.

cmpNameDisplay :: NameDisp -> Name -> Name -> Ordering

Compare two names by the way they would be displayed.

ppLocName :: Name -> Doc

Pretty-print a name with its source location information.

Creation

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

Make a new name for a declaration.

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

Make a new parameter name.

toParamInstName :: Name -> Name

asParamName :: Name -> Name

paramModRecParam :: Name

Unique Supply

class Monad m => FreshM m where

Methods

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

Instances

FreshM InferM

Defined in Cryptol.TypeCheck.Monad

Methods

liftSupply :: (Supply -> (a, Supply)) -> InferM a

FreshM RenameM

Defined in Cryptol.ModuleSystem.Renamer

Methods

liftSupply :: (Supply -> (a, Supply)) -> RenameM a

FreshM REPL

Defined in Cryptol.REPL.Monad

Methods

liftSupply :: (Supply -> (a, Supply)) -> REPL a

Monad m => FreshM (SupplyT m)

Defined in Cryptol.ModuleSystem.Name

Methods

liftSupply :: (Supply -> (a, Supply)) -> SupplyT m a

Monad m => FreshM (ModuleT m)

Defined in Cryptol.ModuleSystem.Monad

Methods

liftSupply :: (Supply -> (a, Supply)) -> ModuleT m a

FreshM m => FreshM (ReaderT i m)

Defined in Cryptol.ModuleSystem.Name

Methods

liftSupply :: (Supply -> (a, Supply)) -> ReaderT i m a

(Monoid i, FreshM m) => FreshM (WriterT i m)

Defined in Cryptol.ModuleSystem.Name

Methods

liftSupply :: (Supply -> (a, Supply)) -> WriterT i m a

FreshM m => FreshM (StateT i m)

Defined in Cryptol.ModuleSystem.Name

Methods

liftSupply :: (Supply -> (a, Supply)) -> StateT i m a

FreshM m => FreshM (ExceptionT i m)

Defined in Cryptol.ModuleSystem.Name

Methods

liftSupply :: (Supply -> (a, Supply)) -> ExceptionT i m a

nextUniqueM :: FreshM m => m Int

Retrieve the next unique from the supply.

data SupplyT m a

A monad for easing the use of the supply.

Instances

MonadT SupplyT

Defined in Cryptol.ModuleSystem.Name

Methods

lift :: Monad m => m a -> SupplyT m a

Monad m => Monad (SupplyT m)

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)

Defined in Cryptol.ModuleSystem.Name

Methods

fmap :: (a -> b) -> SupplyT m a -> SupplyT m b

(<$) :: a -> SupplyT m b -> SupplyT m a

Monad m => Applicative (SupplyT m)

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)

Defined in Cryptol.ModuleSystem.Name

Methods

liftSupply :: (Supply -> (a, Supply)) -> SupplyT m a

BaseM m n => BaseM (SupplyT m) n

Defined in Cryptol.ModuleSystem.Name

Methods

inBase :: n a -> SupplyT m a

RunM m (a, Supply) r => RunM (SupplyT m) a (Supply -> r)

Defined in Cryptol.ModuleSystem.Name

Methods

runM :: SupplyT m a -> Supply -> r

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

data Supply

Instances

Show Supply

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> Supply -> ShowS

show :: Supply -> String

showList :: [Supply] -> ShowS

Generic Supply

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

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: Supply -> ()

RunM m (a, Supply) r => RunM (SupplyT m) a (Supply -> r)

Defined in Cryptol.ModuleSystem.Name

Methods

runM :: SupplyT m a -> Supply -> r

type Rep Supply

Defined in Cryptol.ModuleSystem.Name

type Rep Supply = D1 ('MetaData "Supply" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" 'False) (C1 ('MetaCons "Supply" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

emptySupply :: Supply

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)

PrimMap

data PrimMap

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

Defined in Cryptol.ModuleSystem.Name

Methods

showsPrec :: Int -> PrimMap -> ShowS

show :: PrimMap -> String

showList :: [PrimMap] -> ShowS

Generic PrimMap

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

Defined in Cryptol.ModuleSystem.Name

Methods

(<>) :: PrimMap -> PrimMap -> PrimMap

sconcat :: NonEmpty PrimMap -> PrimMap

stimes :: Integral b => b -> PrimMap -> PrimMap

NFData PrimMap

Defined in Cryptol.ModuleSystem.Name

Methods

rnf :: PrimMap -> ()

type Rep PrimMap

Defined in Cryptol.ModuleSystem.Name

type Rep PrimMap = D1 ('MetaData "PrimMap" "Cryptol.ModuleSystem.Name" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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

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

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.