cryptol-3.0.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.ModuleSystem.Binds

Synopsis

- class BindsNames a
- data TopDef
  - = TopMod ModName (Mod ())
  - | TopInst ModName (ImpName PName) (ModuleInstanceArgs PName)
- data Mod a = Mod {
  - modImports :: [ImportG (ImpName PName)]
  - modKind :: ModKind
  - modInstances :: Map Name (ImpName PName, ModuleInstanceArgs PName)
  - modMods :: Map Name (Mod a)
  - modDefines :: NamingEnv
  - modPublic :: !(Set Name)
  - modState :: a
  }
- data ModKind
  - = AFunctor
  - | ASignature
  - | AModule
- modNested :: Mod a -> Set Name
- modBuilder :: ModBuilder a -> Supply -> ((a, [RenamerError]), Supply)
- topModuleDefs :: Module PName -> ModBuilder TopDef
- topDeclsDefs :: ModPath -> [TopDecl PName] -> ModBuilder (Mod ())
- newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name
- data InModule a = InModule (Maybe ModPath) a
- ifaceToMod :: IfaceG name -> Mod ()
- ifaceSigToMod :: ModParamNames -> Mod ()
- modToMap :: ImpName Name -> Mod () -> Map (ImpName Name) (Mod ()) -> Map (ImpName Name) (Mod ())
- defsOf :: BindsNames a => a -> Supply -> (NamingEnv, Supply)

# Documentation

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

Constructors

TopMod ModName (Mod ()) |
TopInst ModName (ImpName PName) (ModuleInstanceArgs PName) |

data Mod a Source #

Things defined by a module

Constructors

Mod |

Fields

- modImports :: [ImportG (ImpName PName)]
- modKind :: ModKind
- modInstances :: Map Name (ImpName PName, ModuleInstanceArgs PName)
- modMods :: Map Name (Mod a)

  this includes signatures

- modDefines :: NamingEnv

  Things defined by this module. Note the for normal modules we really just need the public names, however for things within functors we need all defined names, so that we can generate fresh names in instantiations

- modPublic :: !(Set Name)

  These are the exported names

- modState :: a

  Used in the import loop to track the current state of processing. The reason this is here, rather than just having a pair in the other algorithm is because this type is recursive (for nested modules) and it is conveninet to keep track for all modules at once

#### Instances

Instances details

Functor Mod Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods fmap :: (a -> b) -> Mod a -> Mod b Source # (<$) :: a -> Mod b -> Mod a Source #

data ModKind Source #

Constructors

AFunctor |
ASignature |
AModule |

#### Instances

Instances details

Generic ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Associated Types type Rep ModKind :: Type -> Type Source # Methods from :: ModKind -> Rep ModKind x Source # to :: Rep ModKind x -> ModKind Source #
Show ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods showsPrec :: Int -> ModKind -> ShowS Source # show :: ModKind -> String Source # showList :: [ModKind] -> ShowS Source #
PP ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods ppPrec :: Int -> ModKind -> Doc Source #
NFData ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods rnf :: ModKind -> () Source #
Eq ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods (==) :: ModKind -> ModKind -> Bool Source # (/=) :: ModKind -> ModKind -> Bool Source #
Ord ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error Methods compare :: ModKind -> ModKind -> Ordering Source # (<) :: ModKind -> ModKind -> Bool Source # (<=) :: ModKind -> ModKind -> Bool Source # (>) :: ModKind -> ModKind -> Bool Source # (>=) :: ModKind -> ModKind -> Bool Source # max :: ModKind -> ModKind -> ModKind Source # min :: ModKind -> ModKind -> ModKind Source #
type Rep ModKind Source # |
Instance details Defined in Cryptol.ModuleSystem.Renamer.Error type Rep ModKind = D1 ('MetaData "ModKind" "Cryptol.ModuleSystem.Renamer.Error" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "AFunctor" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ASignature" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AModule" 'PrefixI 'False) (U1 :: Type -> Type)))

modNested :: Mod a -> Set Name Source #

modBuilder :: ModBuilder a -> Supply -> ((a, [RenamerError]), Supply) Source #

topModuleDefs :: Module PName -> ModBuilder TopDef Source #

topDeclsDefs :: ModPath -> [TopDecl PName] -> ModBuilder (Mod ()) Source #

newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name Source #

Given a name in a signature, make a name for the parameter corresponding to the signature.

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

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

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

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

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

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

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

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

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

toList :: InModule a -> [a] Source #

null :: InModule a -> Bool Source #

length :: InModule a -> Int Source #

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

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

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

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

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

Traversable InModule Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods traverse :: Applicative f => (a -> f b) -> InModule a -> f (InModule b) Source # sequenceA :: Applicative f => InModule (f a) -> f (InModule a) Source # mapM :: Monad m => (a -> m b) -> InModule a -> m (InModule b) Source # sequence :: Monad m => InModule (m a) -> m (InModule a) Source #
Functor InModule Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods fmap :: (a -> b) -> InModule a -> InModule b Source # (<$) :: a -> InModule b -> InModule a Source #
Show a => Show (InModule a) Source # |
Instance details Defined in Cryptol.ModuleSystem.Binds Methods showsPrec :: Int -> InModule a -> ShowS Source # show :: InModule a -> String Source # showList :: [InModule a] -> ShowS Source #
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 (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

ifaceToMod :: IfaceG name -> Mod () Source #

Make a `Mod` from the public declarations in an interface. This is used to handle imports.

ifaceSigToMod :: ModParamNames -> Mod () Source #

modToMap :: ImpName Name -> Mod () -> Map (ImpName Name) (Mod ()) -> Map (ImpName Name) (Mod ()) Source #

Generate a map from this module and all modules nested in it.

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

Generate a `NamingEnv` using an explicit supply.