cryptol-3.1.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
Monoid NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

Semigroup NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

Generic NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

Associated Types

type Rep NamingEnv :: Type -> Type #

Show NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

BindsNames NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: NamingEnv -> BuildNamingEnv

ModuleInstance NamingEnv Source # 
Instance details

Defined in Cryptol.TypeCheck.ModuleInstance

PP NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

Methods

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

NFData NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

Methods

rnf :: NamingEnv -> () #

type Rep NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.NamingEnv.Types

type Rep NamingEnv = D1 ('MetaData "NamingEnv" "Cryptol.ModuleSystem.NamingEnv.Types" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'True) (C1 ('MetaCons "NamingEnv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Namespace (Map PName Names)))))

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

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

class BindsNames a Source #

Things that define exported names.

Minimal complete definition

namingEnv

Instances

Instances details
BindsNames NamingEnv Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: NamingEnv -> BuildNamingEnv

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (EnumDecl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (NestedModule PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (PrimType PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (SigDecl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

BindsNames (Pattern PName) Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Pattern PName -> BuildNamingEnv

BindsNames (Schema PName) Source #

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

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Schema PName -> BuildNamingEnv

BindsNames (TParam PName) Source #

Generate the naming environment for a type parameter.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: TParam PName -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: Maybe a -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: [a] -> BuildNamingEnv

data InModule a Source #

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

By wrapping types with this, we can pass the module path to methods that need the extra information.

Constructors

InModule (Maybe ModPath) a 

Instances

Instances details
Foldable InModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

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.Binds

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

Functor InModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

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

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

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

Defined in Cryptol.ModuleSystem.Binds

Methods

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

show :: InModule a -> String #

showList :: [InModule a] -> ShowS #

BindsNames (InModule (Bind PName)) Source #

Introduce the name

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

BindsNames (InModule (Decl PName)) Source #

The naming environment for a single declaration.

Instance details

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (EnumDecl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (NestedModule PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (PrimType PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (SigDecl PName) -> BuildNamingEnv

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

Defined in Cryptol.ModuleSystem.Binds

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

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 Bind Source #

Rename a binding.

Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename BindDef Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename BindImpl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename CaseAlt Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Decl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename EnumDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Expr Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename FunDesc Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ImpName Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Match Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ModParam Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ModuleInstanceArg Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ModuleInstanceArgs Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename ModuleInstanceNamedArg Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename NestedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Newtype 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 Pattern Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename PrimType Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Prop Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename PropGuardCase Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename PropSyn 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 SigDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename TParam Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename TopDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename TySyn Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Rename Type 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

data RenameM a Source #

Instances

Instances details
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 #

Functor RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

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

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

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 #

FreshM RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Monad

Methods

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

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

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 #

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

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

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

InvalidDependency [DepName]

Things that can't depend on each other

MultipleModParams Ident [Range]

Module parameters with the same name

InvalidFunctorImport (ImpName Name)

Can't import functors directly

UnexpectedNest Range PName

Nested modules were not supposed to appear here

ModuleKindMismatch Range (ImpName Name) ModKind ModKind

Exepcted one kind (first one) but found the other (second one)

Instances

Instances details
Generic RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Associated Types

type Rep RenamerError :: Type -> Type #

Show RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

PP RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

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

NFData RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

rnf :: RenamerError -> () #

Eq RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Ord RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

type Rep RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

type Rep RenamerError = D1 ('MetaData "RenamerError" "Cryptol.ModuleSystem.Renamer.Error" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 "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])) :+: C1 ('MetaCons "MultipleModParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Range])))) :+: (C1 ('MetaCons "InvalidFunctorImport" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ImpName Name))) :+: (C1 ('MetaCons "UnexpectedNest" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PName)) :+: C1 ('MetaCons "ModuleKindMismatch" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ImpName Name))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModKind)))))))

data RenamerWarning Source #

Instances

Instances details
Generic RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Associated Types

type Rep RenamerWarning :: Type -> Type #

Show RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

PP RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

NFData RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Methods

rnf :: RenamerWarning -> () #

Eq RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

Ord RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

type Rep RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer.Error

renameModule :: Module PName -> RenameM RenamedModule Source #

Entry point. This is used for renaming a top-level module.

renameTopDecls :: ModName -> [TopDecl PName] -> RenameM (NamingEnv, [TopDecl Name]) Source #

Entry point. Rename a list of top-level declarations. This is used for declaration that don't live in a module (e.g., define on the command line.)

We assume that these declarations do not contain any nested modules.

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 #

The result of renaming a module

Constructors

RenamedModule 

Fields

Instances

Instances details
PP RenamedModule Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer