Agda-2.5.4.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 :: i -> TCM a Source #

reifyWhen :: Bool -> i -> TCM a Source #

Instances
Reify MetaId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Literal Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Level Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Sort Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Telescope Telescope Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Type Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Term Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Reify Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

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 :: [i] -> TCM [a] Source #

reifyWhen :: Bool -> [i] -> TCM [a] Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Dom i -> TCM (Arg a) Source #

reifyWhen :: Bool -> Dom i -> TCM (Arg 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 :: Arg i -> TCM (Arg a) Source #

reifyWhen :: Bool -> Arg i -> TCM (Arg a) Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Elim' i -> TCM (Elim' a) Source #

reifyWhen :: Bool -> Elim' i -> TCM (Elim' a) Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Abs i -> TCM (Name, a) Source #

reifyWhen :: Bool -> Abs i -> TCM (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 :: (i1, i2) -> TCM (a1, a2) Source #

reifyWhen :: Bool -> (i1, i2) -> TCM (a1, a2) Source #

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

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: Named n i -> TCM (Named n a) Source #

reifyWhen :: Bool -> Named n i -> TCM (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 :: (i1, i2, i3) -> TCM (a1, a2, a3) Source #

reifyWhen :: Bool -> (i1, i2, i3) -> TCM (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 :: (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) Source #

reifyWhen :: Bool -> (i1, i2, i3, i4) -> TCM (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 :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern] Source #

Assumes that pattern variables have been added to the context already. Picks pattern variable names from context.