Safe Haskell	None
Language	Haskell2010

FreeC.Environment.Entry

Description

This module contains data types that are used to store information about declared functions, (type) variables and (type) constructors in the environment.

Synopsis

data EnvEntry
- = DataEntry {
  - entrySrcSpan :: SrcSpan
  - entryArity :: Int
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entryName :: QName
  - entryConsNames :: [ConName]
  }
- | TypeSynEntry {
  - entrySrcSpan :: SrcSpan
  - entryArity :: Int
  - entryTypeArgs :: [TypeVarIdent]
  - entryTypeSyn :: Type
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entryName :: QName
  }
- | TypeVarEntry {
  - entrySrcSpan :: SrcSpan
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entryName :: QName
  }
- | ConEntry {
  - entrySrcSpan :: SrcSpan
  - entryArity :: Int
  - entryTypeArgs :: [TypeVarIdent]
  - entryArgTypes :: [Type]
  - entryReturnType :: Type
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entrySmartIdent :: Qualid
  - entryAgdaSmartIdent :: QName
  - entryName :: QName
  }
- | FuncEntry {
  - entrySrcSpan :: SrcSpan
  - entryArity :: Int
  - entryTypeArgs :: [TypeVarIdent]
  - entryArgTypes :: [Type]
  - entryStrictArgs :: [Bool]
  - entryReturnType :: Type
  - entryNeedsFreeArgs :: Bool
  - entryEncapsulatesEffects :: Bool
  - entryEffects :: [Effect]
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entryName :: QName
  }
- | VarEntry {
  - entrySrcSpan :: SrcSpan
  - entryIsPure :: Bool
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entryName :: QName
  - entryType :: Maybe Type
  }
- | FreshEntry {
  - entryIdent :: Qualid
  - entryAgdaIdent :: QName
  - entryName :: QName
  }
entryScope :: EnvEntry -> Scope
entryScopedName :: EnvEntry -> ScopedName
isDataEntry :: EnvEntry -> Bool
isTypeSynEntry :: EnvEntry -> Bool
isTypeVarEntry :: EnvEntry -> Bool
isConEntry :: EnvEntry -> Bool
isFuncEntry :: EnvEntry -> Bool
isVarEntry :: EnvEntry -> Bool
isTopLevelEntry :: EnvEntry -> Bool
entryHasSmartIdent :: EnvEntry -> Bool
prettyEntryType :: EnvEntry -> String

Documentation

data EnvEntry Source #

Entry of the environment.

Constructors

DataEntry	Entry for a data type declaration.
Fields entrySrcSpan :: SrcSpan The source code location where the data type was declared. entryArity :: Int The number of type arguments expected by the type constructor. entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entryName :: QName The name of the data type in the module it has been defined in. entryConsNames :: [ConName] The names of the constructors of the data type.
TypeSynEntry	Entry for a type synonym declaration.
Fields entrySrcSpan :: SrcSpan The source code location where the data type was declared. entryArity :: Int The number of type arguments expected by the type constructor. entryTypeArgs :: [TypeVarIdent] The names of the type arguments. entryTypeSyn :: Type The type that is abbreviated by this type synonym. entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entryName :: QName The name of the data type in the module it has been defined in.
TypeVarEntry	Entry for a type variable.
Fields entrySrcSpan :: SrcSpan The source code location where the data type was declared. entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entryName :: QName The name of the data type in the module it has been defined in.
ConEntry	Entry for a data constructor.
Fields entrySrcSpan :: SrcSpan The source code location where the data type was declared. entryArity :: Int The number of type arguments expected by the type constructor. entryTypeArgs :: [TypeVarIdent] The names of the type arguments. entryArgTypes :: [Type] The types of the constructor's arguments. Contains exactly `entryArity` elements. entryReturnType :: Type The return type of the data constructor. entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entrySmartIdent :: Qualid The name of the corresponding smart constructor in Coq. entryAgdaSmartIdent :: QName The name of the corresponding smart constructor in Agda. entryName :: QName The name of the data type in the module it has been defined in.
FuncEntry	Entry for a function declaration.
Fields entrySrcSpan :: SrcSpan The source code location where the data type was declared. entryArity :: Int The number of type arguments expected by the type constructor. entryTypeArgs :: [TypeVarIdent] The names of the type arguments. entryArgTypes :: [Type] The types of the constructor's arguments. Contains exactly `entryArity` elements. entryStrictArgs :: [Bool] Whether each argument is strict. Contains exactly `entryArity` elements. entryReturnType :: Type The return type of the data constructor. entryNeedsFreeArgs :: Bool Whether the arguments of the `Free` monad need to be passed to the function. entryEncapsulatesEffects :: Bool Whether the function should encapsulate effects. entryEffects :: [Effect] The effects of the function, i.e. which type classes are needed during the translation. entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entryName :: QName The name of the data type in the module it has been defined in.
VarEntry	Entry for a variable.
Fields entrySrcSpan :: SrcSpan The source code location where the data type was declared. entryIsPure :: Bool Whether the variable has not been lifted to the free monad. entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entryName :: QName The name of the data type in the module it has been defined in. entryType :: Maybe Type The type of the variable (if known).
FreshEntry	Entry for fresh variables. The purpose of these entries is to prevent two fresh variables with the same name to be issued for generated AST nodes that have no corresponding
Fields entryIdent :: Qualid The name of the data type in Coq. entryAgdaIdent :: QName The name of the data type in Agda. entryName :: QName The name of the data type in the module it has been defined in.

Instances

Eq EnvEntry Source #	Entries are identified by their original name.
Instance details Defined in FreeC.Environment.Entry Methods (==) :: EnvEntry -> EnvEntry -> Bool Source # (/=) :: EnvEntry -> EnvEntry -> Bool Source #
Ord EnvEntry Source #	Entries are ordered by their original name.
Instance details Defined in FreeC.Environment.Entry Methods compare :: EnvEntry -> EnvEntry -> Ordering Source # (<) :: EnvEntry -> EnvEntry -> Bool Source # (<=) :: EnvEntry -> EnvEntry -> Bool Source # (>) :: EnvEntry -> EnvEntry -> Bool Source # (>=) :: EnvEntry -> EnvEntry -> Bool Source # max :: EnvEntry -> EnvEntry -> EnvEntry Source # min :: EnvEntry -> EnvEntry -> EnvEntry Source #
Show EnvEntry Source #
Instance details Defined in FreeC.Environment.Entry Methods showsPrec :: Int -> EnvEntry -> ShowS Source # show :: EnvEntry -> String Source # showList :: [EnvEntry] -> ShowS Source #