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 Void

type Rep Name

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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 "nNamespace") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Namespace))) :*: (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 !ModPath !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.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "Declared" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 ModPath) :*: 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.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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

nameNamespace :: Name -> Namespace

asPrim :: Name -> Maybe PrimIdent

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

asOrigName :: Name -> Maybe OrigName

ppLocName :: Name -> Doc

Pretty-print a name with its source location information.

data Namespace

Namespaces for names

Constructors

NSValue

NSType

NSModule

Instances

Bounded Namespace

Defined in Cryptol.Utils.Ident

Methods

minBound :: Namespace

maxBound :: Namespace

Enum Namespace

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]

Eq Namespace

Defined in Cryptol.Utils.Ident

Methods

(==) :: Namespace -> Namespace -> Bool

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

Ord Namespace

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

Show Namespace

Defined in Cryptol.Utils.Ident

Methods

showsPrec :: Int -> Namespace -> ShowS

show :: Namespace -> String

showList :: [Namespace] -> ShowS

Generic Namespace

Defined in Cryptol.Utils.Ident

Associated Types

type Rep Namespace :: Type -> Type

Methods

from :: Namespace -> Rep Namespace x

to :: Rep Namespace x -> Namespace

NFData Namespace

Defined in Cryptol.Utils.Ident

Methods

rnf :: Namespace -> ()

PP Namespace

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> Namespace -> Doc

type Rep Namespace

Defined in Cryptol.Utils.Ident

type Rep Namespace = D1 ('MetaData "Namespace" "Cryptol.Utils.Ident" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "NSValue" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NSType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NSModule" 'PrefixI 'False) (U1 :: Type -> Type)))

data ModPath

Idnetifies a possibly nested module

Constructors

TopModule ModName

Nested ModPath Ident

Instances

Eq ModPath

Defined in Cryptol.Utils.Ident

Methods

(==) :: ModPath -> ModPath -> Bool

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

Ord ModPath

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

Show ModPath

Defined in Cryptol.Utils.Ident

Methods

showsPrec :: Int -> ModPath -> ShowS

show :: ModPath -> String

showList :: [ModPath] -> ShowS

Generic ModPath

Defined in Cryptol.Utils.Ident

Associated Types

type Rep ModPath :: Type -> Type

Methods

from :: ModPath -> Rep ModPath x

to :: Rep ModPath x -> ModPath

NFData ModPath

Defined in Cryptol.Utils.Ident

Methods

rnf :: ModPath -> ()

PP ModPath

Defined in Cryptol.Utils.PP

Methods

ppPrec :: Int -> ModPath -> Doc

type Rep ModPath

Defined in Cryptol.Utils.Ident

type Rep ModPath = D1 ('MetaData "ModPath" "Cryptol.Utils.Ident" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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

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)

Make a new name for a declaration.

mkParameter :: Namespace -> 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.Monad

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.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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.