Safe Haskell | None |
---|---|
Language | Haskell2010 |
Translating from internal syntax to abstract syntax. Enables nice pretty printing of internal syntax.
TODO
- numbers on metas
- fake dependent functions to independent functions
- meta parameters
- shadowing
Synopsis
- class Reify i where
- type ReifiesTo i
- reify :: MonadReify m => i -> m (ReifiesTo i)
- reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i)
- type MonadReify (m :: Type -> Type) = (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m)
- data NamedClause = NamedClause QName Bool Clause
- reifyPatterns :: MonadReify m => [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
- reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)
- blankNotInScope :: (MonadTCEnv m, MonadDebug m, BlankVars a) => a -> m a
- reifyDisplayFormP :: MonadReify m => QName -> Patterns -> Patterns -> m (QName, Patterns)
Documentation
reify :: MonadReify m => i -> m (ReifiesTo i) Source #
reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i) Source #
Instances
type MonadReify (m :: Type -> Type) = (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m) Source #
data NamedClause Source #
NamedClause QName Bool Clause | Also tracks whether module parameters should be dropped from the patterns. |
Instances
Reify NamedClause Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract
reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause) Source # reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause) Source # | |||||
PrettyTCM NamedClause Source # | |||||
Defined in Agda.TypeChecking.Pretty prettyTCM :: MonadPretty m => NamedClause -> m Doc Source # | |||||
type ReifiesTo NamedClause Source # | |||||
Defined in Agda.Syntax.Translation.InternalToAbstract |
reifyPatterns :: MonadReify m => [NamedArg DeBruijnPattern] -> m [NamedArg Pattern] Source #
Assumes that pattern variables have been added to the context already. Picks pattern variable names from context.
reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i) Source #
Like reify
but instantiates blocking metas, useful for reporting.
blankNotInScope :: (MonadTCEnv m, MonadDebug m, BlankVars a) => a -> m a Source #
blankNotInScope e
replaces variables in expression e
with _
if they are currently not in scope.
:: MonadReify m | |
=> QName | LHS head symbol |
-> Patterns | Patterns to be taken into account to find display form. |
-> Patterns | Remaining trailing patterns ("with patterns"). |
-> m (QName, Patterns) | New head symbol and new patterns. |
reifyDisplayFormP
tries to recursively
rewrite a lhs with a display form.
Note: we are not necessarily in the empty context upon entry!