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

Safe Haskell | Safe-Inferred
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 = (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, BlankVars a) => a -> m a
- reifyDisplayFormP :: MonadReify m => QName -> Patterns -> Patterns -> m (QName, Patterns)

# Documentation

class Reify i where Source #

Minimal complete definition

reify

Associated Types

type ReifiesTo i Source #

Methods

reify :: MonadReify m => i -> m (ReifiesTo i) Source #

reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i) Source #

#### Instances

Instances details

Reify Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Expr Source # Methods reify :: MonadReify m => Expr -> m (ReifiesTo Expr) Source # reifyWhen :: MonadReify m => Bool -> Expr -> m (ReifiesTo Expr) Source #
Reify Name Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Name Source # Methods reify :: MonadReify m => Name -> m (ReifiesTo Name) Source # reifyWhen :: MonadReify m => Bool -> Name -> m (ReifiesTo Name) Source #
Reify MetaId Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo MetaId Source # Methods reify :: MonadReify m => MetaId -> m (ReifiesTo MetaId) Source # reifyWhen :: MonadReify m => Bool -> MetaId -> m (ReifiesTo MetaId) Source #
Reify Level Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Level Source # Methods reify :: MonadReify m => Level -> m (ReifiesTo Level) Source # reifyWhen :: MonadReify m => Bool -> Level -> m (ReifiesTo Level) Source #
Reify Sort Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Sort Source # Methods reify :: MonadReify m => Sort -> m (ReifiesTo Sort) Source # reifyWhen :: MonadReify m => Bool -> Sort -> m (ReifiesTo Sort) Source #
Reify Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Telescope Source # Methods reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source # reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #
Reify Term Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Term Source # Methods reify :: MonadReify m => Term -> m (ReifiesTo Term) Source # reifyWhen :: MonadReify m => Bool -> Term -> m (ReifiesTo Term) Source #
Reify Type Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Type Source # Methods reify :: MonadReify m => Type -> m (ReifiesTo Type) Source # reifyWhen :: MonadReify m => Bool -> Type -> m (ReifiesTo Type) Source #
Reify Literal Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Literal Source # Methods reify :: MonadReify m => Literal -> m (ReifiesTo Literal) Source # reifyWhen :: MonadReify m => Bool -> Literal -> m (ReifiesTo Literal) Source #
Reify NamedClause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo NamedClause Source # Methods reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause) Source # reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause) Source #
Reify Constraint Source # |
Instance details Defined in Agda.Interaction.BasicOps Associated Types type ReifiesTo Constraint Source # Methods reify :: MonadReify m => Constraint -> m (ReifiesTo Constraint) Source # reifyWhen :: MonadReify m => Bool -> Constraint -> m (ReifiesTo Constraint) Source #
Reify DisplayTerm Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo DisplayTerm Source # Methods reify :: MonadReify m => DisplayTerm -> m (ReifiesTo DisplayTerm) Source # reifyWhen :: MonadReify m => Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm) Source #
Reify ProblemConstraint Source # |
Instance details Defined in Agda.Interaction.BasicOps Associated Types type ReifiesTo ProblemConstraint Source # Methods reify :: MonadReify m => ProblemConstraint -> m (ReifiesTo ProblemConstraint) Source # reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (ReifiesTo ProblemConstraint) Source #
Reify Bool Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Bool Source # Methods reify :: MonadReify m => Bool -> m (ReifiesTo Bool) Source # reifyWhen :: MonadReify m => Bool -> Bool -> m (ReifiesTo Bool) Source #
Reify (QNamed Clause) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (QNamed Clause) Source # Methods reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source # reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #
Reify (QNamed System) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (QNamed System) Source # Methods reify :: MonadReify m => QNamed System -> m (ReifiesTo (QNamed System)) Source # reifyWhen :: MonadReify m => Bool -> QNamed System -> m (ReifiesTo (QNamed System)) Source #
Reify i => Reify (Arg i) Source # | Skip reification of implicit and irrelevant args if option is off.
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Arg i) Source # Methods reify :: MonadReify m => Arg i -> m (ReifiesTo (Arg i)) Source # reifyWhen :: MonadReify m => Bool -> Arg i -> m (ReifiesTo (Arg i)) Source #
(Free i, Reify i) => Reify (Abs i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Abs i) Source # Methods reify :: MonadReify m => Abs i -> m (ReifiesTo (Abs i)) Source # reifyWhen :: MonadReify m => Bool -> Abs i -> m (ReifiesTo (Abs i)) Source #
Reify i => Reify (Dom i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Dom i) Source # Methods reify :: MonadReify m => Dom i -> m (ReifiesTo (Dom i)) Source # reifyWhen :: MonadReify m => Bool -> Dom i -> m (ReifiesTo (Dom i)) Source #
Reify i => Reify (Elim' i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Elim' i) Source # Methods reify :: MonadReify m => Elim' i -> m (ReifiesTo (Elim' i)) Source # reifyWhen :: MonadReify m => Bool -> Elim' i -> m (ReifiesTo (Elim' i)) Source #
Reify a => Reify (IPBoundary' a) Source # |
Instance details Defined in Agda.Interaction.BasicOps Associated Types type ReifiesTo (IPBoundary' a) Source # Methods reify :: MonadReify m => IPBoundary' a -> m (ReifiesTo (IPBoundary' a)) Source # reifyWhen :: MonadReify m => Bool -> IPBoundary' a -> m (ReifiesTo (IPBoundary' a)) Source #
Reify i => Reify [i] Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo [i] Source # Methods reify :: MonadReify m => [i] -> m (ReifiesTo [i]) Source # reifyWhen :: MonadReify m => Bool -> [i] -> m (ReifiesTo [i]) Source #
Reify i => Reify (Named n i) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (Named n i) Source # Methods reify :: MonadReify m => Named n i -> m (ReifiesTo (Named n i)) Source # reifyWhen :: MonadReify m => Bool -> Named n i -> m (ReifiesTo (Named n i)) Source #
(Reify i1, Reify i2) => Reify (i1, i2) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (i1, i2) Source # Methods reify :: MonadReify m => (i1, i2) -> m (ReifiesTo (i1, i2)) Source # reifyWhen :: MonadReify m => Bool -> (i1, i2) -> m (ReifiesTo (i1, i2)) Source #
(Reify i1, Reify i2, Reify i3) => Reify (i1, i2, i3) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (i1, i2, i3) Source # Methods reify :: MonadReify m => (i1, i2, i3) -> m (ReifiesTo (i1, i2, i3)) Source # reifyWhen :: MonadReify m => Bool -> (i1, i2, i3) -> m (ReifiesTo (i1, i2, i3)) Source #
(Reify i1, Reify i2, Reify i3, Reify i4) => Reify (i1, i2, i3, i4) Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (i1, i2, i3, i4) Source # Methods reify :: MonadReify m => (i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4)) Source # reifyWhen :: MonadReify m => Bool -> (i1, i2, i3, i4) -> m (ReifiesTo (i1, i2, i3, i4)) Source #

type MonadReify m = (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

Instances details

Reify NamedClause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo NamedClause Source # Methods reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause) Source # reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause) Source #
PrettyTCM NamedClause Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source #
type ReifiesTo NamedClause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo NamedClause = Clause

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, BlankVars a) => a -> m a Source #

`blankNotInScope e` replaces variables in expression `e` with `_` if they are currently not in scope.

reifyDisplayFormP Source #

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!