cryptol-2.13.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Cryptol.ModuleSystem.Renamer

Description

 
Synopsis

Documentation

data NamingEnv Source #

The NamingEnv is used by the renamer to determine what identifiers refer to.

Instances

Instances details
Show NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Generic NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Associated Types

type Rep NamingEnv :: Type -> Type #

Semigroup NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Monoid NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

NFData NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

rnf :: NamingEnv -> () #

PP NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

ppPrec :: Int -> NamingEnv -> Doc Source #

BindsNames NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep NamingEnv = D1 ('MetaData "NamingEnv" "Cryptol.ModuleSystem.NamingEnv" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'True) (C1 ('MetaCons "NamingEnv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Namespace (Map PName [Name])))))

shadowing :: NamingEnv -> NamingEnv -> NamingEnv Source #

Like mappend, but when merging, prefer values on the lhs.

class BindsNames a where Source #

Things that define exported names.

Instances

Instances details
BindsNames ImportIface Source #

Produce a naming environment from an interface file, that contains a mapping only from unqualified names to qualified ones.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames a => BindsNames [a] Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: [a] -> BuildNamingEnv Source #

BindsNames a => BindsNames (Maybe a) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (TParam PName) Source #

Generate the naming environment for a type parameter.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (Schema PName) Source #

Generate a type renaming environment from the parameters that are bound by this schema.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (Module PName) Source #

The naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (PrimType PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Newtype PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (ParameterFun PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (ParameterType PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (TopDecl PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (NestedModule PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

data InModule a Source #

Do somethign in context. If Nothing than we are working with a local declaration. Otherwise we are at the top-level of the given module.

Constructors

InModule (Maybe ModPath) a 

Instances

Instances details
Functor InModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

fmap :: (a -> b) -> InModule a -> InModule b #

(<$) :: a -> InModule b -> InModule a #

Foldable InModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

fold :: Monoid m => InModule m -> m #

foldMap :: Monoid m => (a -> m) -> InModule a -> m #

foldMap' :: Monoid m => (a -> m) -> InModule a -> m #

foldr :: (a -> b -> b) -> b -> InModule a -> b #

foldr' :: (a -> b -> b) -> b -> InModule a -> b #

foldl :: (b -> a -> b) -> b -> InModule a -> b #

foldl' :: (b -> a -> b) -> b -> InModule a -> b #

foldr1 :: (a -> a -> a) -> InModule a -> a #

foldl1 :: (a -> a -> a) -> InModule a -> a #

toList :: InModule a -> [a] #

null :: InModule a -> Bool #

length :: InModule a -> Int #

elem :: Eq a => a -> InModule a -> Bool #

maximum :: Ord a => InModule a -> a #

minimum :: Ord a => InModule a -> a #

sum :: Num a => InModule a -> a #

product :: Num a => InModule a -> a #

Traversable InModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

traverse :: Applicative f => (a -> f b) -> InModule a -> f (InModule b) #

sequenceA :: Applicative f => InModule (f a) -> f (InModule a) #

mapM :: Monad m => (a -> m b) -> InModule a -> m (InModule b) #

sequence :: Monad m => InModule (m a) -> m (InModule a) #

Show a => Show (InModule a) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

showsPrec :: Int -> InModule a -> ShowS #

show :: InModule a -> String #

showList :: [InModule a] -> ShowS #

BindsNames (InModule (PrimType PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Newtype PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (ParameterFun PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (ParameterType PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (TopDecl PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

BindsNames (InModule (NestedModule PName)) Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv

shadowNames :: BindsNames env => env -> RenameM a -> RenameM a Source #

Shadow the current naming environment with some more names.

class Rename f where Source #

Methods

rename :: f PName -> RenameM (f Name) Source #

Instances

Instances details
Rename Prop Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Type Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename TParam Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Schema Source #

Rename a schema, assuming that none of its type variables are already in scope.

Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Pattern Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Match Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename TypeInst Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename UpdField Source #

Note that after this point the -> updates have an explicit function and there are no more nested updates.

Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename FunDesc Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Expr Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename PrimType Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Newtype Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename BindDef Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Bind Source #

Rename a binding.

Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename PropSyn Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename TySyn Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ParameterFun Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ParameterType Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Decl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ImpName Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

data RenameM a Source #

Instances

Instances details
Monad RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

(>>=) :: RenameM a -> (a -> RenameM b) -> RenameM b #

(>>) :: RenameM a -> RenameM b -> RenameM b #

return :: a -> RenameM a #

Functor RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

fmap :: (a -> b) -> RenameM a -> RenameM b #

(<$) :: a -> RenameM b -> RenameM a #

Applicative RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

pure :: a -> RenameM a #

(<*>) :: RenameM (a -> b) -> RenameM a -> RenameM b #

liftA2 :: (a -> b -> c) -> RenameM a -> RenameM b -> RenameM c #

(*>) :: RenameM a -> RenameM b -> RenameM b #

(<*) :: RenameM a -> RenameM b -> RenameM a #

FreshM RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

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

Semigroup a => Semigroup (RenameM a) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

(<>) :: RenameM a -> RenameM a -> RenameM a #

sconcat :: NonEmpty (RenameM a) -> RenameM a #

stimes :: Integral b => b -> RenameM a -> RenameM a #

(Semigroup a, Monoid a) => Monoid (RenameM a) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

mempty :: RenameM a #

mappend :: RenameM a -> RenameM a -> RenameM a #

mconcat :: [RenameM a] -> RenameM a #

data RenamerError Source #

Constructors

MultipleSyms (Located PName) [Name]

Multiple imported symbols contain this name

UnboundName Namespace (Located PName)

Some name not bound to any definition

OverlappingSyms [Name]

An environment has produced multiple overlapping symbols

WrongNamespace Namespace Namespace (Located PName)

expected, actual. When a name is missing from the expected namespace, but exists in another

FixityError (Located Name) Fixity (Located Name) Fixity

When the fixity of two operators conflict

InvalidConstraint (Type PName)

When it's not possible to produce a Prop from a Type.

MalformedBuiltin (Type PName) PName

When a builtin type/type-function is used incorrectly.

BoundReservedType PName (Maybe Range) Doc

When a builtin type is named in a binder.

OverlappingRecordUpdate (Located [Selector]) (Located [Selector])

When record updates overlap (e.g., { r | x = e1, x.y = e2 })

InvalidDependency [DepName] 

Instances

Instances details
Show RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Generic RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Associated Types

type Rep RenamerError :: Type -> Type #

NFData RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

rnf :: RenamerError -> () #

PP RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

ppPrec :: Int -> RenamerError -> Doc Source #

type Rep RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

type Rep RenamerError = D1 ('MetaData "RenamerError" "Cryptol.ModuleSystem.Renamer.Error" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (((C1 ('MetaCons "MultipleSyms" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located PName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: C1 ('MetaCons "UnboundName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Namespace) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located PName)))) :+: (C1 ('MetaCons "OverlappingSyms" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "WrongNamespace" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Namespace) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Namespace) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located PName)))) :+: C1 ('MetaCons "FixityError" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Fixity)))))) :+: ((C1 ('MetaCons "InvalidConstraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type PName))) :+: C1 ('MetaCons "MalformedBuiltin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Type PName)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PName))) :+: (C1 ('MetaCons "BoundReservedType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PName) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Range)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc))) :+: (C1 ('MetaCons "OverlappingRecordUpdate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located [Selector])) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located [Selector]))) :+: C1 ('MetaCons "InvalidDependency" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DepName]))))))

data RenamerWarning Source #

Instances

Instances details
Eq RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Ord RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Show RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Generic RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Associated Types

type Rep RenamerWarning :: Type -> Type #

NFData RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

rnf :: RenamerWarning -> () #

PP RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

type Rep RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

data RenamerInfo Source #

Information needed to do some renaming.

Constructors

RenamerInfo 

Fields

data NameType Source #

Indicates if a name is in a binding poisition or a use site

Constructors

NameBind 
NameUse 

data RenamedModule Source #

Constructors

RenamedModule 

Fields