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 a | i -> a where
data NamedClause = NamedClause QName Bool Clause
reifyPatterns :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern]

Documentation

class Reify i a | i -> a where #

Minimal complete definition

reify

Methods

reify :: i -> TCM a #

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

Instances

Reify MetaId Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: MetaId -> TCM Expr # reifyWhen :: Bool -> MetaId -> TCM Expr #
Reify Name Name #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Name -> TCM Name # reifyWhen :: Bool -> Name -> TCM Name #
Reify Literal Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Literal -> TCM Expr # reifyWhen :: Bool -> Literal -> TCM Expr #
Reify Level Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Level -> TCM Expr # reifyWhen :: Bool -> Level -> TCM Expr #
Reify Sort Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Sort -> TCM Expr # reifyWhen :: Bool -> Sort -> TCM Expr #
Reify Telescope Telescope #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope # reifyWhen :: Bool -> Telescope0 -> TCM Telescope #
Reify Type Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr # reifyWhen :: Bool -> Type -> TCM Expr #
Reify Term Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Term -> TCM Expr # reifyWhen :: Bool -> Term -> TCM Expr #
Reify Expr Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Expr -> TCM Expr # reifyWhen :: Bool -> Expr -> TCM Expr #
Reify DisplayTerm Expr #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: DisplayTerm -> TCM Expr # reifyWhen :: Bool -> DisplayTerm -> TCM Expr #
Reify NamedClause Clause #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: NamedClause -> TCM Clause # reifyWhen :: Bool -> NamedClause -> TCM Clause #
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) #
Reify Constraint (OutputConstraint Expr Expr) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) #
Reify (QNamed Clause) Clause #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause #
Reify i a => Reify [i] [a] #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: [i] -> TCM [a] # reifyWhen :: Bool -> [i] -> TCM [a] #
Reify i a => Reify (Dom i) (Arg a) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Dom i -> TCM (Arg a) # reifyWhen :: Bool -> Dom i -> TCM (Arg a) #
Reify i a => Reify (Arg i) (Arg a) #	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) # reifyWhen :: Bool -> Arg i -> TCM (Arg a) #
Reify i a => Reify (Elim' i) (Elim' a) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Elim' i -> TCM (Elim' a) # reifyWhen :: Bool -> Elim' i -> TCM (Elim' a) #
(Free i, Reify i a) => Reify (Abs i) (Name, a) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Abs i -> TCM (Name, a) # reifyWhen :: Bool -> Abs i -> TCM (Name, a) #
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: (i1, i2) -> TCM (a1, a2) # reifyWhen :: Bool -> (i1, i2) -> TCM (a1, a2) #
Reify i a => Reify (Named n i) (Named n a) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Named n i -> TCM (Named n a) # reifyWhen :: Bool -> Named n i -> TCM (Named n a) #
(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: (i1, i2, i3) -> TCM (a1, a2, a3) # reifyWhen :: Bool -> (i1, i2, i3) -> TCM (a1, a2, a3) #
(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4) #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) # reifyWhen :: Bool -> (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) #

data NamedClause #

Constructors

NamedClause QName Bool Clause

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

Instances

PrettyTCM NamedClause #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: NamedClause -> TCM Doc #
Reify NamedClause Clause #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: NamedClause -> TCM Clause # reifyWhen :: Bool -> NamedClause -> TCM Clause #

reifyPatterns :: MonadTCM tcm => [NamedArg DeBruijnPattern] -> tcm [NamedArg Pattern] #

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