| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Translation.InternalToAbstract
Description
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
Minimal complete definition
Methods
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 #
Constructors
| 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 Associated Types
Methods 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 Methods 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.
Arguments
| :: 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!