Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Signature

Synopsis

- setHardCompileTimeModeIfErased :: Erased -> TCM a -> TCM a
- setHardCompileTimeModeIfErased' :: LensQuantity q => q -> TCM a -> TCM a
- setRunTimeModeUnlessInHardCompileTimeMode :: TCM a -> TCM a
- setModeUnlessInHardCompileTimeMode :: Erased -> TCM a -> TCM a
- warnForPlentyInHardCompileTimeMode :: Erased -> TCM ()
- addConstant :: QName -> Definition -> TCM ()
- addConstant' :: QName -> ArgInfo -> Type -> Defn -> TCM ()
- setTerminates :: MonadTCState m => QName -> Bool -> m ()
- setCompiledClauses :: QName -> CompiledClauses -> TCM ()
- setSplitTree :: QName -> SplitTree -> TCM ()
- modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
- addClauses :: (MonadConstraint m, MonadTCState m) => QName -> [Clause] -> m ()
- mkPragma :: String -> TCM CompilerPragma
- addPragma :: BackendName -> QName -> String -> TCM ()
- getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
- setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
- markStatic :: QName -> TCM ()
- markInline :: Bool -> QName -> TCM ()
- markInjective :: QName -> TCM ()
- markFirstOrder :: QName -> TCM ()
- unionSignatures :: [Signature] -> Signature
- unionSignature :: Signature -> Signature -> Signature
- addSection :: ModuleName -> TCM ()
- setModuleCheckpoint :: ModuleName -> TCM ()
- getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)
- lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
- addDisplayForms :: QName -> TCM ()
- applySection :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
- applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
- addDisplayForm :: QName -> DisplayForm -> TCM ()
- isLocal :: ReadTCState m => QName -> m Bool
- getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
- hasDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m Bool
- class ChaseDisplayForms a where
  - chaseDisplayForms :: a -> Set QName -> TCM (Set QName)
- canonicalName :: HasConstInfo m => QName -> m QName
- sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)
- singleConstructorType :: QName -> TCM Bool
- data SigError
  - = SigUnknown String
  - | SigAbstract
  - | SigCubicalNotErasure
- notSoPrettySigCubicalNotErasure :: QName -> String
- prettySigCubicalNotErasure :: MonadPretty m => QName -> m Doc
- sigError :: (HasCallStack, MonadDebug m) => QName -> m a -> SigError -> m a
- class (Functor m, Applicative m, HasOptions m, MonadDebug m, MonadTCEnv m) => HasConstInfo (m :: Type -> Type) where
  - getConstInfo :: QName -> m Definition
  - getConstInfo' :: QName -> m (Either SigError Definition)
  - getRewriteRulesFor :: QName -> m RewriteRules
- getOriginalConstInfo :: (ReadTCState m, HasConstInfo m) => QName -> m Definition
- defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules
- getFilteredRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => Bool -> QName -> m RewriteRules
- getOriginalProjection :: HasConstInfo m => QName -> m QName
- defaultGetConstInfo :: (HasOptions m, MonadDebug m, MonadTCEnv m) => TCState -> TCEnv -> QName -> m (Either SigError Definition)
- getConInfo :: HasConstInfo m => ConHead -> m Definition
- getPolarity :: HasConstInfo m => QName -> m [Polarity]
- getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity]
- setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m ()
- getForcedArgs :: HasConstInfo m => QName -> m [IsForced]
- getOccurrencesFromType :: Type -> TCM [Occurrence]
- getArgOccurrence :: QName -> Nat -> TCM Occurrence
- setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m ()
- modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m ()
- setTreeless :: QName -> TTerm -> TCM ()
- setCompiledArgUse :: QName -> [ArgUsage] -> TCM ()
- getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled)
- getErasedConArgs :: HasConstInfo m => QName -> m [Bool]
- setErasedConArgs :: QName -> [Bool] -> TCM ()
- getTreeless :: HasConstInfo m => QName -> m (Maybe TTerm)
- getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage])
- addDataCons :: QName -> [QName] -> TCM ()
- getMutual :: QName -> TCM (Maybe [QName])
- getMutual_ :: Defn -> Maybe [QName]
- setMutual :: QName -> [QName] -> TCM ()
- mutuallyRecursive :: QName -> QName -> TCM Bool
- definitelyNonRecursive_ :: Defn -> Bool
- getCurrentModuleFreeVars :: TCM Nat
- getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName)
- getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat
- freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => QName -> m Args
- getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) => ModuleName -> m Nat
- moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args
- inFreshModuleIfFreeParams :: TCM a -> TCM a
- instantiateDef :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => Definition -> m Definition
- instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRule -> m RewriteRule
- instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRules -> m RewriteRules
- alwaysMakeAbstract :: Definition -> Maybe Definition
- inAbstractMode :: MonadTCEnv m => m a -> m a
- inConcreteMode :: MonadTCEnv m => m a -> m a
- ignoreAbstractMode :: MonadTCEnv m => m a -> m a
- underOpaqueId :: MonadTCEnv m => OpaqueId -> m a -> m a
- notUnderOpaque :: MonadTCEnv m => m a -> m a
- inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
- typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type
- relOfConst :: HasConstInfo m => QName -> m Relevance
- modalityOfConst :: HasConstInfo m => QName -> m Modality
- droppedPars :: Definition -> Int
- isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
- isProjection_ :: Defn -> Maybe Projection
- isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection)
- isRelevantProjection_ :: Definition -> Maybe Projection
- isStaticFun :: Defn -> Bool
- isInlineFun :: Defn -> Bool
- isProperProjection :: Defn -> Bool
- projectionArgs :: Definition -> Int
- usesCopatterns :: (HasConstInfo m, HasBuiltins m) => QName -> m Bool
- applyDef :: HasConstInfo m => ProjOrigin -> QName -> Arg Term -> m Term

# Documentation

setHardCompileTimeModeIfErased Source #

Arguments

:: Erased |
-> TCM a | Continuation.
-> TCM a |

If the first argument is ``Erased` something`, then hard compile-time mode is enabled when the continuation is run.

setHardCompileTimeModeIfErased' Source #

Arguments

:: LensQuantity q |
=> q | The quantity.
-> TCM a | Continuation.
-> TCM a |

If the quantity is "erased", then hard compile-time mode is enabled when the continuation is run.

Precondition: The quantity must not be ``Quantity1` something`.

setRunTimeModeUnlessInHardCompileTimeMode Source #

Arguments

:: TCM a | Continuation.
-> TCM a |

Use run-time mode in the continuation unless the current mode is the hard compile-time mode.

setModeUnlessInHardCompileTimeMode Source #

Arguments

:: Erased |
-> TCM a | Continuation.
-> TCM a |

Use hard compile-time mode in the continuation if the first argument is ``Erased` something`. Use run-time mode if the first argument is ``NotErased` something` and the current mode is not hard compile-time mode.

warnForPlentyInHardCompileTimeMode :: Erased -> TCM () Source #

Warn if the user explicitly wrote @`ω` or @`plenty` but the current mode is the hard compile-time mode.

addConstant :: QName -> Definition -> TCM () Source #

Add a constant to the signature. Lifts the definition to top level.

addConstant' :: QName -> ArgInfo -> Type -> Defn -> TCM () Source #

A combination of `addConstant` and `defaultDefn`. The `Language` does not need to be supplied.

setTerminates :: MonadTCState m => QName -> Bool -> m () Source #

Set termination info of a defined function symbol.

setCompiledClauses :: QName -> CompiledClauses -> TCM () Source #

Set CompiledClauses of a defined function symbol.

setSplitTree :: QName -> SplitTree -> TCM () Source #

Set SplitTree of a defined function symbol.

modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM () Source #

Modify the clauses of a function.

addClauses :: (MonadConstraint m, MonadTCState m) => QName -> [Clause] -> m () Source #

Lifts clauses to the top-level and adds them to definition. Also adjusts the `funCopatternLHS` field if necessary.

mkPragma :: String -> TCM CompilerPragma Source #

addPragma :: BackendName -> QName -> String -> TCM () Source #

Add a compiler pragma `{-# COMPILE backend name text #-}`

getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma) Source #

setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM () Source #

markStatic :: QName -> TCM () Source #

markInline :: Bool -> QName -> TCM () Source #

markInjective :: QName -> TCM () Source #

markFirstOrder :: QName -> TCM () Source #

unionSignatures :: [Signature] -> Signature Source #

unionSignature :: Signature -> Signature -> Signature Source #

addSection :: ModuleName -> TCM () Source #

Add a section to the signature.

The current context will be stored as the cumulative module parameters for this section.

setModuleCheckpoint :: ModuleName -> TCM () Source #

Sets the checkpoint for the given module to the current checkpoint.

getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section) Source #

Get a section.

Why Maybe? The reason is that we look up all prefixes of a module to compute number of parameters, and for hierarchical top-level modules, A.B.C say, A and A.B do not exist.

lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope Source #

Lookup a section telescope.

If it doesn't exist, like in hierarchical top-level modules, the section telescope is empty.

addDisplayForms :: QName -> TCM () Source #

Add display forms for a name `f` copied by a module application. Essentially if `f` can reduce to

    λ xs → A.B.C.f vs

by unfolding module application copies (`defCopy`), then we add a display form

    A.B.C.f vs ==> f xs

applySection Source #

Arguments

:: ModuleName | Name of new module defined by the module macro.
-> Telescope | Parameters of new module.
-> ModuleName | Name of old module applied to arguments.
-> Args | Arguments of module application.
-> ScopeCopyInfo | Imported names and modules
-> TCM () |

Module application (followed by module parameter abstraction).

applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM () Source #

addDisplayForm :: QName -> DisplayForm -> TCM () Source #

Add a display form to a definition (could be in this or imported signature).

isLocal :: ReadTCState m => QName -> m Bool Source #

getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm] Source #

hasDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m Bool Source #

class ChaseDisplayForms a where Source #

Find all names used (recursively) by display forms of a given name.

Methods

chaseDisplayForms Source #

Arguments

:: a | Search this recursively for display form names.
-> Set QName | Already processed names (accumulator).
-> TCM (Set QName) | Found names (superset of accumulator)

#### Instances

Instances details

ChaseDisplayForms QName Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods chaseDisplayForms :: QName -> Set QName -> TCM (Set QName) Source #
ChaseDisplayForms DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods chaseDisplayForms :: DisplayForm -> Set QName -> TCM (Set QName) Source #
ChaseDisplayForms DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods chaseDisplayForms :: DisplayTerm -> Set QName -> TCM (Set QName) Source #
ChaseDisplayForms a => ChaseDisplayForms (Open a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods chaseDisplayForms :: Open a -> Set QName -> TCM (Set QName) Source #
ChaseDisplayForms a => ChaseDisplayForms (Set a) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods chaseDisplayForms :: Set a -> Set QName -> TCM (Set QName) Source #
ChaseDisplayForms a => ChaseDisplayForms [a] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods chaseDisplayForms :: [a] -> Set QName -> TCM (Set QName) Source #

canonicalName :: HasConstInfo m => QName -> m QName Source #

sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName) Source #

singleConstructorType :: QName -> TCM Bool Source #

Does the given constructor come from a single-constructor type?

Precondition: The name has to refer to a constructor.

data SigError Source #

Signature lookup errors.

Constructors

SigUnknown String | The name is not in the signature; default error message.
SigAbstract | The name is not available, since it is abstract.
SigCubicalNotErasure | The name is not available because it was defined in Cubical Agda, but the current language is Erased Cubical Agda, and `--erasure` is not active.

notSoPrettySigCubicalNotErasure :: QName -> String Source #

Generates a string error message corresponding to `SigCubicalNotErasure` for a given `QName`.

prettySigCubicalNotErasure :: MonadPretty m => QName -> m Doc Source #

Generates an error message corresponding to `SigCubicalNotErasure` for a given `QName`.

sigError :: (HasCallStack, MonadDebug m) => QName -> m a -> SigError -> m a Source #

An eliminator for `SigError`. All constructors except for `SigAbstract` are assumed to be impossible.

class (Functor m, Applicative m, HasOptions m, MonadDebug m, MonadTCEnv m) => HasConstInfo (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

getConstInfo :: QName -> m Definition Source #

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

getConstInfo' :: QName -> m (Either SigError Definition) Source #

Version that reports exceptions:

default getConstInfo' :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (HasConstInfo n, MonadTrans t, m ~ t n) => QName -> m (Either SigError Definition) Source #

getRewriteRulesFor :: QName -> m RewriteRules Source #

Return the rewrite rules for the given head symbol that could be tried. Not categorically all rewrite rules are returned, in particular, none when reduction of the head symbol is disabled. Rewrite rules that only happen to be in the signature but are not in scope are also not returned.

default getRewriteRulesFor :: forall (n :: Type -> Type) (t :: (Type -> Type) -> Type -> Type). (HasConstInfo n, MonadTrans t, m ~ t n) => QName -> m RewriteRules Source #

#### Instances

Instances details

HasConstInfo TerM Source # |
Instance details Defined in Agda.Termination.Monad Methods getConstInfo :: QName -> TerM Definition Source # getConstInfo' :: QName -> TerM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> TerM RewriteRules Source #
HasConstInfo ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getConstInfo :: QName -> ReduceM Definition Source # getConstInfo' :: QName -> ReduceM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ReduceM RewriteRules Source #
HasConstInfo NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods getConstInfo :: QName -> NLM Definition Source # getConstInfo' :: QName -> NLM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> NLM RewriteRules Source #
HasConstInfo m => HasConstInfo (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods getConstInfo :: QName -> PureConversionT m Definition Source # getConstInfo' :: QName -> PureConversionT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> PureConversionT m RewriteRules Source #
HasConstInfo m => HasConstInfo (BlockT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> BlockT m Definition Source # getConstInfo' :: QName -> BlockT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> BlockT m RewriteRules Source #
HasConstInfo (TCMT IO) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> TCMT IO Definition Source # getConstInfo' :: QName -> TCMT IO (Either SigError Definition) Source # getRewriteRulesFor :: QName -> TCMT IO RewriteRules Source #
HasConstInfo m => HasConstInfo (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getConstInfo :: QName -> NamesT m Definition Source # getConstInfo' :: QName -> NamesT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> NamesT m RewriteRules Source #
HasConstInfo m => HasConstInfo (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ListT m Definition Source # getConstInfo' :: QName -> ListT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ListT m RewriteRules Source #
HasConstInfo m => HasConstInfo (ChangeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ChangeT m Definition Source # getConstInfo' :: QName -> ChangeT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ChangeT m RewriteRules Source #
HasConstInfo m => HasConstInfo (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> MaybeT m Definition Source # getConstInfo' :: QName -> MaybeT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> MaybeT m RewriteRules Source #
HasConstInfo m => HasConstInfo (ExceptT err m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ExceptT err m Definition Source # getConstInfo' :: QName -> ExceptT err m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ExceptT err m RewriteRules Source #
HasConstInfo m => HasConstInfo (IdentityT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> IdentityT m Definition Source # getConstInfo' :: QName -> IdentityT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> IdentityT m RewriteRules Source #
HasConstInfo m => HasConstInfo (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ReaderT r m Definition Source # getConstInfo' :: QName -> ReaderT r m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ReaderT r m RewriteRules Source #
HasConstInfo m => HasConstInfo (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> StateT s m Definition Source # getConstInfo' :: QName -> StateT s m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> StateT s m RewriteRules Source #
(Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> WriterT w m Definition Source # getConstInfo' :: QName -> WriterT w m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> WriterT w m RewriteRules Source #

getOriginalConstInfo :: (ReadTCState m, HasConstInfo m) => QName -> m Definition Source #

The computation `getConstInfo` sometimes tweaks the returned `Definition`, depending on the current `Language` and the `Language` of the `Definition`. This variant of `getConstInfo` does not perform any tweaks.

defaultGetRewriteRulesFor :: (ReadTCState m, MonadTCEnv m) => QName -> m RewriteRules Source #

Return the rewrite rules for the given head symbol that could be tried. Not categorically all rewrite rules are returned, e.g. none when reduction of the head symbol is disabled. Rewrite rules that only happen to be in the signature but are not in scope are also not returned.

getFilteredRewriteRulesFor Source #

Arguments

:: (ReadTCState m, MonadTCEnv m) |
=> Bool | Only return rewrite rules that are in scope?
-> QName | Head symbol.
-> m RewriteRules | Rules for the head symbol.

If the `Bool` parameter is `True`, get the rules in scope, otherwise, get *all* rules unfiltered.

getOriginalProjection :: HasConstInfo m => QName -> m QName Source #

Get the original name of the projection (the current one could be from a module application).

defaultGetConstInfo :: (HasOptions m, MonadDebug m, MonadTCEnv m) => TCState -> TCEnv -> QName -> m (Either SigError Definition) Source #

getConInfo :: HasConstInfo m => ConHead -> m Definition Source #

getPolarity :: HasConstInfo m => QName -> m [Polarity] Source #

Look up the polarity of a definition.

getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity] Source #

Look up polarity of a definition and compose with polarity represented by `Comparison`.

setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m () Source #

Set the polarity of a definition.

getForcedArgs :: HasConstInfo m => QName -> m [IsForced] Source #

Look up the forced arguments of a definition.

getOccurrencesFromType :: Type -> TCM [Occurrence] Source #

Returns the occurences given explicitely as polarity annotations in the function type

getArgOccurrence :: QName -> Nat -> TCM Occurrence Source #

Get argument occurrence info for argument `i` of definition `d` (never fails).

setArgOccurrences :: MonadTCState m => QName -> [Occurrence] -> m () Source #

Sets the `defArgOccurrences` for the given identifier (which should already exist in the signature).

modifyArgOccurrences :: MonadTCState m => QName -> ([Occurrence] -> [Occurrence]) -> m () Source #

setTreeless :: QName -> TTerm -> TCM () Source #

setCompiledArgUse :: QName -> [ArgUsage] -> TCM () Source #

getCompiled :: HasConstInfo m => QName -> m (Maybe Compiled) Source #

getErasedConArgs :: HasConstInfo m => QName -> m [Bool] Source #

Returns a list of length `conArity`. If no erasure analysis has been performed yet, this will be a list of `False`s.

setErasedConArgs :: QName -> [Bool] -> TCM () Source #

getTreeless :: HasConstInfo m => QName -> m (Maybe TTerm) Source #

getCompiledArgUse :: HasConstInfo m => QName -> m (Maybe [ArgUsage]) Source #

addDataCons :: QName -> [QName] -> TCM () Source #

add data constructors to a datatype

getMutual :: QName -> TCM (Maybe [QName]) Source #

Get the mutually recursive identifiers of a symbol from the signature.

getMutual_ :: Defn -> Maybe [QName] Source #

Get the mutually recursive identifiers from a `Definition`.

setMutual :: QName -> [QName] -> TCM () Source #

Set the mutually recursive identifiers.

TODO: This produces data of quadratic size (which has to be processed upon serialization). Presumably qs is usually short, but in some cases (for instance for generated code) it may be long. It would be better to assign a unique identifier to each SCC, and store the names separately.

mutuallyRecursive :: QName -> QName -> TCM Bool Source #

Check whether two definitions are mutually recursive.

definitelyNonRecursive_ :: Defn -> Bool Source #

A functiondatarecord definition is nonRecursive if it is not even mutually recursive with itself.

getCurrentModuleFreeVars :: TCM Nat Source #

Get the number of parameters to the current module.

getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName) Source #

getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat Source #

Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).

freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => QName -> m Args Source #

getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m) => ModuleName -> m Nat Source #

moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadTCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args Source #

Compute the context variables to apply a definition to.

We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)

Example: `module M₁ Γ where module M₁ Δ where f = ... module M₃ Θ where ... M₁.M₂.f [insert Γ raised by Θ]`

inFreshModuleIfFreeParams :: TCM a -> TCM a Source #

Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.

instantiateDef :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => Definition -> m Definition Source #

Instantiate a closed definition with the correct part of the current context.

instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRule -> m RewriteRule Source #

instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadTCEnv m, MonadDebug m) => RewriteRules -> m RewriteRules Source #

alwaysMakeAbstract :: Definition -> Maybe Definition Source #

Return the abstract view of a definition, regardless of whether the definition would be treated abstractly.

inAbstractMode :: MonadTCEnv m => m a -> m a Source #

Enter abstract mode. Abstract definition in the current module are transparent.

inConcreteMode :: MonadTCEnv m => m a -> m a Source #

Not in abstract mode. All abstract definitions are opaque.

ignoreAbstractMode :: MonadTCEnv m => m a -> m a Source #

Ignore abstract mode. All abstract definitions are transparent.

underOpaqueId :: MonadTCEnv m => OpaqueId -> m a -> m a Source #

Go under the given opaque block. The unfolding set will turn opaque definitions transparent.

notUnderOpaque :: MonadTCEnv m => m a -> m a Source #

Outside of any opaque blocks.

inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a Source #

Enter the reducibility environment associated with a definition: The environment will have the same concreteness as the name, and we will be in the opaque block enclosing the name, if any.

typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type Source #

Get type of a constant, instantiated to the current context.

relOfConst :: HasConstInfo m => QName -> m Relevance Source #

Get relevance of a constant.

modalityOfConst :: HasConstInfo m => QName -> m Modality Source #

Get modality of a constant.

droppedPars :: Definition -> Int Source #

The number of dropped parameters for a definition. 0 except for projection(-like) functions and constructors.

isProjection :: HasConstInfo m => QName -> m (Maybe Projection) Source #

Is it the name of a record projection?

isProjection_ :: Defn -> Maybe Projection Source #

isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection) Source #

Is it the name of a non-irrelevant record projection?

isRelevantProjection_ :: Definition -> Maybe Projection Source #

isStaticFun :: Defn -> Bool Source #

Is it a function marked STATIC?

isInlineFun :: Defn -> Bool Source #

Is it a function marked INLINE?

isProperProjection :: Defn -> Bool Source #

Returns `True` if we are dealing with a proper projection, i.e., not a projection-like function nor a record field value (projection applied to argument).

projectionArgs :: Definition -> Int Source #

Number of dropped initial arguments of a projection(-like) function.

usesCopatterns :: (HasConstInfo m, HasBuiltins m) => QName -> m Bool Source #

Check whether a definition uses copatterns.

applyDef :: HasConstInfo m => ProjOrigin -> QName -> Arg Term -> m Term Source #

Apply a function `f` to its first argument, producing the proper postfix projection if `f` is a projection which is not irrelevant.