-- | This module contains data types that are used to store information -- about declared functions, (type) variables and (type) constructors -- in the environment. module FreeC.Environment.Entry where import Data.Function ( on ) import Data.Tuple.Extra ( (&&&) ) import qualified FreeC.Backend.Agda.Syntax as Agda import qualified FreeC.Backend.Coq.Syntax as Coq import FreeC.IR.SrcSpan import qualified FreeC.IR.Syntax as IR import FreeC.LiftedIR.Effect import FreeC.Util.Predicate -- | Entry of the environment. data EnvEntry = -- | Entry for a data type declaration. DataEntry { 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 :: Coq.Qualid -- ^ The name of the data type in Coq. , entryAgdaIdent :: Agda.QName -- ^ The name of the data type in Agda. , entryName :: IR.QName -- ^ The name of the data type in the module it has been defined in. , entryConsNames :: [IR.ConName] -- ^ The names of the constructors of the data type. } -- | Entry for a type synonym declaration. | TypeSynEntry { entrySrcSpan :: SrcSpan -- ^ The source code location where the type synonym was declared. , entryArity :: Int -- ^ The number of type arguments expected by the type constructor. , entryTypeArgs :: [IR.TypeVarIdent] -- ^ The names of the type arguments. , entryTypeSyn :: IR.Type -- ^ The type that is abbreviated by this type synonym. , entryIdent :: Coq.Qualid -- ^ The name of the type synonym in Coq. , entryAgdaIdent :: Agda.QName -- ^ The name of the type synonym in Agda. , entryName :: IR.QName -- ^ The name of the type synonym in the module it has been defined in. } -- | Entry for a type variable. | TypeVarEntry { entrySrcSpan :: SrcSpan -- ^ The source code location where the type variable was declared. , entryIdent :: Coq.Qualid -- ^ The name of the type variable in Coq. , entryAgdaIdent :: Agda.QName -- ^ The name of the type variable in Agda. , entryName :: IR.QName -- ^ The name of the type variable (must be unqualified). } -- | Entry for a data constructor. | ConEntry { entrySrcSpan :: SrcSpan -- ^ The source code location where the data constructor was declared. , entryArity :: Int -- ^ The number of arguments expected by the data constructor. , entryTypeArgs :: [IR.TypeVarIdent] -- ^ The names of the type arguments. , entryArgTypes :: [IR.Type] -- ^ The types of the constructor's arguments. -- Contains exactly 'entryArity' elements. , entryReturnType :: IR.Type -- ^ The return type of the data constructor. , entryIdent :: Coq.Qualid -- ^ The name of the regular data constructor in Coq. , entryAgdaIdent :: Agda.QName -- ^ The name of the regular data constructor in Agda. , entrySmartIdent :: Coq.Qualid -- ^ The name of the corresponding smart constructor in Coq. , entryAgdaSmartIdent :: Agda.QName -- ^ The name of the corresponding smart constructor in Agda. , entryName :: IR.QName -- ^ The name of the data constructor in the module it has been -- defined in. } -- | Entry for a function declaration. | FuncEntry { entrySrcSpan :: SrcSpan -- ^ The source code location where the function was declared. , entryArity :: Int -- ^ The number of arguments expected by the function. , entryTypeArgs :: [IR.TypeVarIdent] -- ^ The names of the type arguments. , entryArgTypes :: [IR.Type] -- ^ The types of the function arguments. -- Contains exactly 'entryArity' elements. , entryStrictArgs :: [Bool] -- ^ Whether each argument is strict. -- Contains exactly 'entryArity' elements. , entryReturnType :: IR.Type -- ^ The return type of the function (if known). , 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 :: Coq.Qualid -- ^ The name of the function in Coq. , entryAgdaIdent :: Agda.QName -- ^ The name of the function in Agda. , entryName :: IR.QName -- ^ The name of the function in the module it has been defined in. } -- | Entry for a variable. | VarEntry { entrySrcSpan :: SrcSpan -- ^ The source code location where the variable was declared. , entryIsPure :: Bool -- ^ Whether the variable has not been lifted to the free monad. , entryIdent :: Coq.Qualid -- ^ The name of the variable in Coq. , entryAgdaIdent :: Agda.QName -- ^ The name of the variable in Agda. , entryName :: IR.QName -- ^ The name of the variable (must be unqualified). , entryType :: Maybe IR.Type -- ^ The type of the variable (if known). } -- | 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 | FreshEntry { entryIdent :: Coq.Qualid -- ^ The renamed fresh Coq identifier. , entryAgdaIdent :: Agda.QName -- ^ The name of the variable in Agda. , entryName :: IR.QName -- ^ The actual fresh identifier before renaming. } deriving Show ------------------------------------------------------------------------------- -- Comparison -- ------------------------------------------------------------------------------- -- | Entries are identified by their original name. instance Eq EnvEntry where (==) = (==) `on` entryScopedName -- | Entries are ordered by their original name. instance Ord EnvEntry where compare = compare `on` entryScopedName ------------------------------------------------------------------------------- -- Getters -- ------------------------------------------------------------------------------- -- | Gets the scope an entry needs to be defined in. entryScope :: EnvEntry -> IR.Scope entryScope DataEntry {} = IR.TypeScope entryScope TypeSynEntry {} = IR.TypeScope entryScope TypeVarEntry {} = IR.TypeScope entryScope ConEntry {} = IR.ValueScope entryScope FuncEntry {} = IR.ValueScope entryScope VarEntry {} = IR.ValueScope entryScope FreshEntry {} = IR.FreshScope -- | Gets the scope and name of the given entry. entryScopedName :: EnvEntry -> IR.ScopedName entryScopedName = entryScope &&& entryName ------------------------------------------------------------------------------- -- Predicates -- ------------------------------------------------------------------------------- -- | Tests whether the given entry of the environment describes a data type. isDataEntry :: EnvEntry -> Bool isDataEntry DataEntry {} = True isDataEntry _ = False -- | Tests whether the given entry of the environment describes a type synonym. isTypeSynEntry :: EnvEntry -> Bool isTypeSynEntry TypeSynEntry {} = True isTypeSynEntry _ = False -- | Tests whether the given entry of the environment describes a type -- variable. isTypeVarEntry :: EnvEntry -> Bool isTypeVarEntry TypeVarEntry {} = True isTypeVarEntry _ = False -- | Tests whether the given entry of the environment describes a data -- constructor. isConEntry :: EnvEntry -> Bool isConEntry ConEntry {} = True isConEntry _ = False -- | Tests whether the given entry of the environment describes a function. isFuncEntry :: EnvEntry -> Bool isFuncEntry FuncEntry {} = True isFuncEntry _ = False -- | Tests whether the given entry of the environment describes a variable. isVarEntry :: EnvEntry -> Bool isVarEntry VarEntry {} = True isVarEntry _ = False -- | Tests whether the given entry of the environment describes a top-level -- data type, type synonym, constructor or function. -- -- Type variables and local variables are no top level entries. isTopLevelEntry :: EnvEntry -> Bool isTopLevelEntry = not . (isVarEntry .||. isTypeVarEntry) -- | Tests whether the given entry distinguishes between a @entryIdent@ and -- @entrySmartIdent@. entryHasSmartIdent :: EnvEntry -> Bool entryHasSmartIdent = isConEntry ------------------------------------------------------------------------------- -- Pretty Printing -- ------------------------------------------------------------------------------- -- | Gets a human readable description of the entry type. prettyEntryType :: EnvEntry -> String prettyEntryType DataEntry {} = "data type" prettyEntryType TypeSynEntry {} = "type synonym" prettyEntryType TypeVarEntry {} = "type variable" prettyEntryType ConEntry {} = "constructor" prettyEntryType FuncEntry {} = "function" prettyEntryType VarEntry {} = "variable" prettyEntryType FreshEntry {} = "fresh identifier"