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

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

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Expr = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Name = Name

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo MetaId = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Level = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Sort = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Term = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Type = Type

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Literal = Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo NamedClause = Clause

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 |
Instance details Defined in Agda.Interaction.BasicOps type ReifiesTo Constraint = OutputConstraint Expr Expr

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 |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo DisplayTerm = Expr

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 |
Instance details Defined in Agda.Interaction.BasicOps type ReifiesTo ProblemConstraint = Closure (OutputForm Expr Expr)

Methods

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

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

Reify ContextEntry Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo ContextEntry |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo ContextEntry = TypedBinding

Methods

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

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

Reify Bool Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Bool |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Bool = Bool

Methods

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

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

Reify Char Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Char |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo Char = Char

Methods

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

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

Reify (QNamed Clause) Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed Clause) = Clause

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed System) = [Clause]

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Arg i) = Arg (ReifiesTo i)

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Abs i) = (Name, ReifiesTo i)

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Elim' i) = Elim' (ReifiesTo i)

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) |
Instance details Defined in Agda.Interaction.BasicOps type ReifiesTo (IPBoundary' a) = IPBoundary' (ReifiesTo a)

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 (List1 i) Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (List1 i) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (List1 i) = List1 (ReifiesTo i)

Methods

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

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

Reify i => Reify [i] Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo [i] |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo [i] = [ReifiesTo i]

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (Named n i) = Named n (ReifiesTo i)

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (i1, i2) = (ReifiesTo i1, ReifiesTo i2)

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (i1, i2, i3) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3)

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) |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo (i1, i2, i3, i4) = (ReifiesTo i1, ReifiesTo i2, ReifiesTo i3, ReifiesTo i4)

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 :: 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

Instances details

Reify NamedClause Source # |

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo NamedClause |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo NamedClause = Clause

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, MonadDebug 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!