cryptol-3.0.0: Cryptol: The Language of Cryptography

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
  - Creation
  - Unique Supply
  - PrimMap

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
- 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
  - | 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 Source # Methods from :: Name -> Rep Name x Source # to :: Rep Name x -> Name Source #
Show Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Name -> ShowS Source # show :: Name -> String Source # showList :: [Name] -> ShowS Source #
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 -> () Source #
Eq Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #
Ord Name Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods compare :: Name -> Name -> Ordering Source # (<) :: Name -> Name -> Bool Source # (<=) :: Name -> Name -> Bool Source # (>) :: Name -> Name -> Bool Source # (>=) :: Name -> Name -> Bool Source # max :: Name -> Name -> Name Source # min :: Name -> Name -> Name Source #
type Rep Name Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

type Rep Name = D1 ('MetaData "Name" "Cryptol.ModuleSystem.Name" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 Source # Methods from :: NameInfo -> Rep NameInfo x Source # to :: Rep NameInfo x -> NameInfo Source #
Show NameInfo Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> NameInfo -> ShowS Source # show :: NameInfo -> String Source # showList :: [NameInfo] -> ShowS Source #
NFData NameInfo Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: NameInfo -> () Source #
type Rep NameInfo Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

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

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 |
NSType |
NSModule |

#### Instances

Instances details

Bounded Namespace Source # |
Instance details Defined in Cryptol.Utils.Ident Methods minBound :: Namespace Source # maxBound :: Namespace Source #
Enum Namespace Source # |

Instance details

Defined in Cryptol.Utils.Ident

Methods

succ :: Namespace -> Namespace Source #

pred :: Namespace -> Namespace Source #

toEnum :: Int -> Namespace Source #

fromEnum :: Namespace -> Int Source #

enumFrom :: Namespace -> [Namespace] Source #

enumFromThen :: Namespace -> Namespace -> [Namespace] Source #

enumFromTo :: Namespace -> Namespace -> [Namespace] Source #

enumFromThenTo :: Namespace -> Namespace -> Namespace -> [Namespace] Source #

Generic Namespace Source # |
Instance details Defined in Cryptol.Utils.Ident Associated Types type Rep Namespace :: Type -> Type Source # Methods from :: Namespace -> Rep Namespace x Source # to :: Rep Namespace x -> Namespace Source #
Show Namespace Source # |
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> Namespace -> ShowS Source # show :: Namespace -> String Source # showList :: [Namespace] -> ShowS Source #
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 -> () Source #
Eq Namespace Source # |
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: Namespace -> Namespace -> Bool Source # (/=) :: Namespace -> Namespace -> Bool Source #
Ord Namespace Source # |

Instance details

Defined in Cryptol.Utils.Ident

Methods

compare :: Namespace -> Namespace -> Ordering Source #

(<) :: Namespace -> Namespace -> Bool Source #

(<=) :: Namespace -> Namespace -> Bool Source #

(>) :: Namespace -> Namespace -> Bool Source #

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

max :: Namespace -> Namespace -> Namespace Source #

min :: Namespace -> Namespace -> Namespace Source #

type Rep Namespace Source # |
Instance details Defined in Cryptol.Utils.Ident type Rep Namespace = D1 ('MetaData "Namespace" "Cryptol.Utils.Ident" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 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 Source # Methods from :: ModPath -> Rep ModPath x Source # to :: Rep ModPath x -> ModPath Source #
Show ModPath Source # |
Instance details Defined in Cryptol.Utils.Ident Methods showsPrec :: Int -> ModPath -> ShowS Source # show :: ModPath -> String Source # showList :: [ModPath] -> ShowS Source #
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 -> () Source #
Eq ModPath Source # |
Instance details Defined in Cryptol.Utils.Ident Methods (==) :: ModPath -> ModPath -> Bool Source # (/=) :: ModPath -> ModPath -> Bool Source #
Ord ModPath Source # |
Instance details Defined in Cryptol.Utils.Ident Methods compare :: ModPath -> ModPath -> Ordering Source # (<) :: ModPath -> ModPath -> Bool Source # (<=) :: ModPath -> ModPath -> Bool Source # (>) :: ModPath -> ModPath -> Bool Source # (>=) :: ModPath -> ModPath -> Bool Source # max :: ModPath -> ModPath -> ModPath Source # min :: ModPath -> ModPath -> ModPath Source #
type Rep ModPath Source # |

Instance details

Defined in Cryptol.Utils.Ident

type Rep ModPath = D1 ('MetaData "ModPath" "Cryptol.Utils.Ident" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 Source #
Monad m => Applicative (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods pure :: a -> SupplyT m a Source # (<*>) :: SupplyT m (a -> b) -> SupplyT m a -> SupplyT m b Source # liftA2 :: (a -> b -> c) -> SupplyT m a -> SupplyT m b -> SupplyT m c Source # (*>) :: SupplyT m a -> SupplyT m b -> SupplyT m b Source # (<*) :: SupplyT m a -> SupplyT m b -> SupplyT m a Source #
Monad m => Functor (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods fmap :: (a -> b) -> SupplyT m a -> SupplyT m b Source # (<$) :: a -> SupplyT m b -> SupplyT m a Source #
Monad m => Monad (SupplyT m) Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods (>>=) :: SupplyT m a -> (a -> SupplyT m b) -> SupplyT m b Source # (>>) :: SupplyT m a -> SupplyT m b -> SupplyT m b Source # return :: a -> SupplyT 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 #
BaseM m n => BaseM (SupplyT m) n Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods inBase :: n a -> SupplyT m a Source #
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 Source #

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 Source # Methods from :: Supply -> Rep Supply x Source # to :: Rep Supply x -> Supply Source #
Show Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> Supply -> ShowS Source # show :: Supply -> String Source # showList :: [Supply] -> ShowS Source #
NFData Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: Supply -> () Source #
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 Source #
type Rep Supply Source # |
Instance details Defined in Cryptol.ModuleSystem.Name type Rep Supply = D1 ('MetaData "Supply" "Cryptol.ModuleSystem.Name" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 Source # sconcat :: NonEmpty PrimMap -> PrimMap Source # stimes :: Integral b => b -> PrimMap -> PrimMap Source #
Generic PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Associated Types type Rep PrimMap :: Type -> Type Source # Methods from :: PrimMap -> Rep PrimMap x Source # to :: Rep PrimMap x -> PrimMap Source #
Show PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods showsPrec :: Int -> PrimMap -> ShowS Source # show :: PrimMap -> String Source # showList :: [PrimMap] -> ShowS Source #
NFData PrimMap Source # |
Instance details Defined in Cryptol.ModuleSystem.Name Methods rnf :: PrimMap -> () Source #
type Rep PrimMap Source # |

Instance details

Defined in Cryptol.ModuleSystem.Name

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