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

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

# 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 Methods reify :: MetaId -> TCM Expr Source # reifyWhen :: Bool -> MetaId -> TCM Expr Source #
Reify Name Name Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Name -> TCM Name Source # reifyWhen :: Bool -> Name -> TCM Name Source #
Reify Literal Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Literal -> TCM Expr Source # reifyWhen :: Bool -> Literal -> TCM Expr Source #
Reify Level Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Level -> TCM Expr Source # reifyWhen :: Bool -> Level -> TCM Expr Source #
Reify Sort Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Sort -> TCM Expr Source # reifyWhen :: Bool -> Sort -> TCM Expr Source #
Reify Telescope Telescope Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Telescope0 -> TCM Telescope Source # reifyWhen :: Bool -> Telescope0 -> TCM Telescope Source #
Reify Type Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Type -> TCM Expr Source # reifyWhen :: Bool -> Type -> TCM Expr Source #
Reify Term Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Term -> TCM Expr Source # reifyWhen :: Bool -> Term -> TCM Expr Source #
Reify Expr Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: Expr -> TCM Expr Source # reifyWhen :: Bool -> Expr -> TCM Expr Source #
Reify DisplayTerm Expr Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: DisplayTerm -> TCM Expr Source # reifyWhen :: Bool -> DisplayTerm -> TCM Expr Source #
Reify NamedClause Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: NamedClause -> TCM Clause Source # reifyWhen :: Bool -> NamedClause -> TCM Clause Source #
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source #
Reify Constraint (OutputConstraint Expr Expr) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) Source # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) Source #
Reify (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed Clause0 -> TCM Clause Source # reifyWhen :: Bool -> QNamed Clause0 -> TCM Clause Source #
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 (QNamed System) [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: QNamed System -> TCM [Clause] Source # reifyWhen :: Bool -> QNamed System -> TCM [Clause] 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.

Instances

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

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.