cryptol-2.8.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.ModuleSystem.Renamer

Description

 
Synopsis

Documentation

data NamingEnv Source #

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

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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (C1 (MetaCons "NamingEnv" PrefixI True) (S1 (MetaSel (Just "neExprs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (Map PName [Name])) :*: S1 (MetaSel (Just "neTypes") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (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
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

data InModule a Source #

Constructors

InModule !ModName a 
Instances
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 #

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

namingEnv' :: BindsNames a => a -> Supply -> (NamingEnv, Supply) Source #

Generate a NamingEnv using an explicit supply.

checkNamingEnv :: NamingEnv -> ([RenamerError], [RenamerWarning]) Source #

Throw errors for any names that overlap in a rewrite environment.

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

Defined in Cryptol.ModuleSystem.Renamer

Rename Type Source #

Resolve fixity, then rename the resulting type.

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 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 TopDecl Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

data RenameM a Source #

Instances
Monad RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Methods

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

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

return :: a -> RenameM a #

fail :: String -> RenameM a #

Functor RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Methods

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

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

Applicative RenameM Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

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

Methods

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

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

Defined in Cryptol.ModuleSystem.Renamer

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

Methods

mempty :: RenameM a #

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

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

data RenamerError Source #

Constructors

MultipleSyms (Located PName) [Name] NameDisp

Multiple imported symbols contain this name

UnboundExpr (Located PName) NameDisp

Expression name is not bound to any definition

UnboundType (Located PName) NameDisp

Type name is not bound to any definition

OverlappingSyms [Name] NameDisp

An environment has produced multiple overlapping symbols

ExpectedValue (Located PName) NameDisp

When a value is expected from the naming environment, but one or more types exist instead.

ExpectedType (Located PName) NameDisp

When a type is missing from the naming environment, but one or more values exist with the same name.

FixityError (Located Name) Fixity (Located Name) Fixity NameDisp

When the fixity of two operators conflict

InvalidConstraint (Type PName) NameDisp

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

MalformedBuiltin (Type PName) PName NameDisp

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

BoundReservedType PName (Maybe Range) Doc NameDisp

When a builtin type is named in a binder.

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

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

Instances
Show RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Associated Types

type Rep RenamerError :: Type -> Type #

NFData RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Methods

rnf :: RenamerError -> () #

PP RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Methods

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

type Rep RenamerError Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

type Rep RenamerError = D1 (MetaData "RenamerError" "Cryptol.ModuleSystem.Renamer" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp))) :+: C1 (MetaCons "UnboundExpr" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located PName)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp))) :+: (C1 (MetaCons "UnboundType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located PName)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp)) :+: (C1 (MetaCons "OverlappingSyms" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp)) :+: C1 (MetaCons "ExpectedValue" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located PName)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp))))) :+: ((C1 (MetaCons "ExpectedType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located PName)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp)) :+: (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) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp)))) :+: C1 (MetaCons "InvalidConstraint" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Type PName)) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp)))) :+: (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) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp))) :+: (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) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp))) :+: 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])) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NameDisp)))))))

data RenamerWarning Source #

Instances
Show RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Generic RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Associated Types

type Rep RenamerWarning :: Type -> Type #

NFData RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

Methods

rnf :: RenamerWarning -> () #

PP RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer

type Rep RenamerWarning Source # 
Instance details

Defined in Cryptol.ModuleSystem.Renamer