| 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 a | i -> a where
- reify :: MonadReify m => i -> m a
- reifyWhen :: MonadReify m => Bool -> i -> m a
- type MonadReify m = (MonadReduce m, MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m, HasOptions m, HasBuiltins m, MonadDebug m)
- data NamedClause = NamedClause QName Bool Clause
- reifyPatterns :: MonadReify m => [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
- reifyUnblocked :: Reify i a => i -> TCM a
- blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a
- reifyDisplayFormP :: MonadReify m => QName -> Patterns -> Patterns -> m (QName, Patterns)
Documentation
class Reify i a | i -> a where Source #
Minimal complete definition
Methods
reify :: MonadReify m => i -> m a Source #
reifyWhen :: MonadReify m => Bool -> i -> m a Source #
Instances
type MonadReify m = (MonadReduce m, MonadAddContext m, MonadInteractionPoints m, MonadFresh NameId m, HasConstInfo m, HasOptions m, HasBuiltins m, MonadDebug m) Source #
data NamedClause Source #
Constructors
| NamedClause QName Bool Clause | Also tracks whether module parameters should be dropped from the patterns. |
Instances
| PrettyTCM NamedClause Source # | |
Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source # | |
| Reify NamedClause Clause Source # | |
Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MonadReify m => NamedClause -> m Clause Source # reifyWhen :: MonadReify m => Bool -> NamedClause -> m Clause Source # | |
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 a => i -> TCM a Source #
Like reify but instantiates blocking metas, useful for reporting.
blankNotInScope :: (MonadTCEnv 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!