Cryptol.ModuleSystem.Renamer

Documentation

data NamingEnv

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

Instances

Show NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

showsPrec :: Int -> NamingEnv -> ShowS

show :: NamingEnv -> String

showList :: [NamingEnv] -> ShowS

Generic NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Associated Types

type Rep NamingEnv :: Type -> Type

Methods

from :: NamingEnv -> Rep NamingEnv x

to :: Rep NamingEnv x -> NamingEnv

Semigroup NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

(<>) :: NamingEnv -> NamingEnv -> NamingEnv

sconcat :: NonEmpty NamingEnv -> NamingEnv

stimes :: Integral b => b -> NamingEnv -> NamingEnv

Monoid NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

mempty :: NamingEnv

mappend :: NamingEnv -> NamingEnv -> NamingEnv

mconcat :: [NamingEnv] -> NamingEnv

NFData NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

rnf :: NamingEnv -> ()

BindsNames NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: NamingEnv -> BuildNamingEnv

type Rep NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

type Rep NamingEnv = D1 ('MetaData "NamingEnv" "Cryptol.ModuleSystem.NamingEnv" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

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

class BindsNames a where

Things that define exported names.

Methods

namingEnv :: a -> BuildNamingEnv

Instances

BindsNames ImportIface

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

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: ImportIface -> BuildNamingEnv

BindsNames NamingEnv

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: NamingEnv -> BuildNamingEnv

BindsNames a => BindsNames [a]

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: [a] -> BuildNamingEnv

BindsNames a => BindsNames (Maybe a)

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Maybe a -> BuildNamingEnv

BindsNames (TParam PName)

Generate the naming environment for a type parameter.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: TParam PName -> BuildNamingEnv

BindsNames (Schema PName)

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

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Schema PName -> BuildNamingEnv

BindsNames (Module PName)

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

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: Module PName -> BuildNamingEnv

BindsNames (InModule (PrimType PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (PrimType PName) -> BuildNamingEnv

BindsNames (InModule (Newtype PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

BindsNames (InModule (Bind PName))

Introduce the name

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

BindsNames (InModule (ParameterFun PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

BindsNames (InModule (ParameterType PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

BindsNames (InModule (Decl PName))

The naming environment for a single declaration.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

BindsNames (InModule (TopDecl PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

data InModule a

Constructors

InModule !ModName a

Instances

Functor InModule

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

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

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

Foldable InModule

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

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)

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

showsPrec :: Int -> InModule a -> ShowS

show :: InModule a -> String

showList :: [InModule a] -> ShowS

BindsNames (InModule (PrimType PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (PrimType PName) -> BuildNamingEnv

BindsNames (InModule (Newtype PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Newtype PName) -> BuildNamingEnv

BindsNames (InModule (Bind PName))

Introduce the name

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Bind PName) -> BuildNamingEnv

BindsNames (InModule (ParameterFun PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterFun PName) -> BuildNamingEnv

BindsNames (InModule (ParameterType PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (ParameterType PName) -> BuildNamingEnv

BindsNames (InModule (Decl PName))

The naming environment for a single declaration.

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (Decl PName) -> BuildNamingEnv

BindsNames (InModule (TopDecl PName))

Defined in Cryptol.ModuleSystem.NamingEnv

Methods

namingEnv :: InModule (TopDecl PName) -> BuildNamingEnv

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

Generate a NamingEnv using an explicit supply.

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

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

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

Shadow the current naming environment with some more names.

class Rename f where

Methods

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

Instances

Rename Prop

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Prop PName -> RenameM (Prop Name)

Rename Type

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Type PName -> RenameM (Type Name)

Rename TParam

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TParam PName -> RenameM (TParam Name)

Rename Schema

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

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Schema PName -> RenameM (Schema Name)

Rename Pattern

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Pattern PName -> RenameM (Pattern Name)

Rename Match

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Match PName -> RenameM (Match Name)

Rename TypeInst

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TypeInst PName -> RenameM (TypeInst Name)

Rename UpdField

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

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: UpdField PName -> RenameM (UpdField Name)

Rename Expr

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Expr PName -> RenameM (Expr Name)

Rename PrimType

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: PrimType PName -> RenameM (PrimType Name)

Rename Newtype

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Newtype PName -> RenameM (Newtype Name)

Rename BindDef

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: BindDef PName -> RenameM (BindDef Name)

Rename Bind

Rename a binding.

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Bind PName -> RenameM (Bind Name)

Rename PropSyn

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: PropSyn PName -> RenameM (PropSyn Name)

Rename TySyn

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TySyn PName -> RenameM (TySyn Name)

Rename ParameterFun

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: ParameterFun PName -> RenameM (ParameterFun Name)

Rename ParameterType

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: ParameterType PName -> RenameM (ParameterType Name)

Rename Decl

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: Decl PName -> RenameM (Decl Name)

Rename TopDecl

Defined in Cryptol.ModuleSystem.Renamer

Methods

rename :: TopDecl PName -> RenameM (TopDecl Name)

runRenamer :: Supply -> ModName -> NamingEnv -> RenameM a -> (Either [RenamerError] (a, Supply), [RenamerWarning])

data RenameM a

Instances

Monad RenameM

Defined in Cryptol.ModuleSystem.Renamer

Methods

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

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

return :: a -> RenameM a

Functor RenameM

Defined in Cryptol.ModuleSystem.Renamer

Methods

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

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

Applicative RenameM

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

Defined in Cryptol.ModuleSystem.Renamer

Methods

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

Semigroup a => Semigroup (RenameM a)

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)

Defined in Cryptol.ModuleSystem.Renamer

Methods

mempty :: RenameM a

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

mconcat :: [RenameM a] -> RenameM a

data RenamerError

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

Defined in Cryptol.ModuleSystem.Renamer

Methods

showsPrec :: Int -> RenamerError -> ShowS

show :: RenamerError -> String

showList :: [RenamerError] -> ShowS

Generic RenamerError

Defined in Cryptol.ModuleSystem.Renamer

Associated Types

type Rep RenamerError :: Type -> Type

Methods

from :: RenamerError -> Rep RenamerError x

to :: Rep RenamerError x -> RenamerError

NFData RenamerError

Defined in Cryptol.ModuleSystem.Renamer

Methods

rnf :: RenamerError -> ()

PP RenamerError

Defined in Cryptol.ModuleSystem.Renamer

Methods

ppPrec :: Int -> RenamerError -> Doc

type Rep RenamerError

Defined in Cryptol.ModuleSystem.Renamer

type Rep RenamerError = D1 ('MetaData "RenamerError" "Cryptol.ModuleSystem.Renamer" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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

Constructors

SymbolShadowed Name [Name] NameDisp

UnusedName Name NameDisp

Instances

Show RenamerWarning

Defined in Cryptol.ModuleSystem.Renamer

Methods

showsPrec :: Int -> RenamerWarning -> ShowS

show :: RenamerWarning -> String

showList :: [RenamerWarning] -> ShowS

Generic RenamerWarning

Defined in Cryptol.ModuleSystem.Renamer

Associated Types

type Rep RenamerWarning :: Type -> Type

Methods

from :: RenamerWarning -> Rep RenamerWarning x

to :: Rep RenamerWarning x -> RenamerWarning

NFData RenamerWarning

Defined in Cryptol.ModuleSystem.Renamer

Methods

rnf :: RenamerWarning -> ()

PP RenamerWarning

Defined in Cryptol.ModuleSystem.Renamer

Methods

ppPrec :: Int -> RenamerWarning -> Doc

type Rep RenamerWarning

Defined in Cryptol.ModuleSystem.Renamer

type Rep RenamerWarning = D1 ('MetaData "RenamerWarning" "Cryptol.ModuleSystem.Renamer" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (C1 ('MetaCons "SymbolShadowed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameDisp))) :+: C1 ('MetaCons "UnusedName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NameDisp)))

renameVar :: PName -> RenameM Name

renameType :: PName -> RenameM Name

renameModule :: Module PName -> RenameM (NamingEnv, Module Name)