Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 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 #

Reify Level Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type 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 #

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 #

Reify NamedClause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo NamedClause Source #

Reify Constraint Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ReifiesTo Constraint Source #

Reify DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo DisplayTerm Source #

Reify ProblemConstraint Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type 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 #

Reify (QNamed System) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type 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 #

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 #

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 => 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!