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

Safe HaskellNone
LanguageHaskell2010

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

Documentation

class Reify i a | i -> a where Source #

Minimal complete definition

reify

Methods

reify :: MonadReify m => i -> m a Source #

reifyWhen :: MonadReify m => Bool -> i -> m a Source #

Instances
Reify Bool Bool Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Bool -> m Bool Source #

reifyWhen :: MonadReify m => Bool -> Bool -> m Bool Source #

Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Name -> m Name Source #

reifyWhen :: MonadReify m => Bool -> Name -> m Name Source #

Reify Literal Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Level Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Level -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Level -> m Expr Source #

Reify Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Sort -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Sort -> m Expr Source #

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Type Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Type -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Type -> m Expr Source #

Reify Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Term -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Term -> m Expr Source #

Reify Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Expr -> m Expr Source #

reifyWhen :: MonadReify m => Bool -> Expr -> m Expr Source #

Reify DisplayTerm Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify NamedClause Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Reify Constraint (OutputConstraint Expr Expr) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Reify (QNamed Clause) Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify i a => Reify [i] [a] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => [i] -> m [a] Source #

reifyWhen :: MonadReify m => Bool -> [i] -> m [a] Source #

Reify i a => Reify (Arg i) (Arg a) Source #

Skip reification of implicit and irrelevant args if option is off.

Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

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

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

Reify (QNamed System) [Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify i a => Reify (Elim' i) (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Elim' i -> m (Elim' a) Source #

reifyWhen :: MonadReify m => Bool -> Elim' i -> m (Elim' a) Source #

Reify i a => Reify (Dom i) (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Dom i -> m (Arg a) Source #

reifyWhen :: MonadReify m => Bool -> Dom i -> m (Arg a) Source #

Reify a e => Reify (IPBoundary' a) (IPBoundary' e) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Abs i -> m (Name, a) Source #

reifyWhen :: MonadReify m => Bool -> Abs i -> m (Name, a) Source #

(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => (i1, i2) -> m (a1, a2) Source #

reifyWhen :: MonadReify m => Bool -> (i1, i2) -> m (a1, a2) Source #

Reify i a => Reify (Named n i) (Named n a) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Named n i -> m (Named n a) Source #

reifyWhen :: MonadReify m => Bool -> Named n i -> m (Named n a) Source #

(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => (i1, i2, i3) -> m (a1, a2, a3) Source #

reifyWhen :: MonadReify m => Bool -> (i1, i2, i3) -> m (a1, a2, a3) Source #

(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => (i1, i2, i3, i4) -> m (a1, a2, a3, a4) Source #

reifyWhen :: MonadReify m => Bool -> (i1, i2, i3, i4) -> m (a1, a2, a3, a4) Source #

data NamedClause Source #

Constructors

NamedClause QName Bool Clause

Also tracks whether module parameters should be dropped from the patterns.

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.

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!