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

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

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

Reify Level Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Level 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Sort Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Sort 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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

Reify Term Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Term 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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

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

Reify NamedClause Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo NamedClause 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Constraint Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ReifiesTo Constraint 
Instance details

Defined in Agda.Interaction.BasicOps

Reify DisplayTerm Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo DisplayTerm 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify ProblemConstraint Source # 
Instance details

Defined in Agda.Interaction.BasicOps

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

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

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

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

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.

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!