Safe Haskell	Safe-Inferred
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 where
- type ReifiesTo i
- reify :: MonadReify m => i -> m (ReifiesTo i)
- reifyWhen :: MonadReify m => Bool -> i -> m (ReifiesTo i)
type MonadReify m = (PureTCM m, MonadInteractionPoints m, MonadFresh NameId m)
data NamedClause = NamedClause QName Bool Clause
reifyPatterns :: MonadReify m => [NamedArg DeBruijnPattern] -> m [NamedArg Pattern]
reifyUnblocked :: Reify i => i -> TCM (ReifiesTo i)
blankNotInScope :: (MonadTCEnv m, BlankVars a) => a -> m a
reifyDisplayFormP :: MonadReify m => QName -> Patterns -> Patterns -> m (QName, Patterns)

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 # Methods reify :: MonadReify m => MetaId -> m (ReifiesTo MetaId) Source # reifyWhen :: MonadReify m => Bool -> MetaId -> m (ReifiesTo MetaId) Source #
Reify Level Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo Level Source # Methods reify :: MonadReify m => Level -> m (ReifiesTo Level) Source # reifyWhen :: MonadReify m => Bool -> Level -> m (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 # Methods reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source # reifyWhen :: MonadReify m => Bool -> Telescope -> m (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 # Methods reify :: MonadReify m => Literal -> m (ReifiesTo Literal) Source # reifyWhen :: MonadReify m => Bool -> Literal -> m (ReifiesTo Literal) Source #
Reify NamedClause Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo NamedClause Source # Methods reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause) Source # reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause) Source #
Reify Constraint Source #
Instance details Defined in Agda.Interaction.BasicOps Associated Types type ReifiesTo Constraint Source # Methods reify :: MonadReify m => Constraint -> m (ReifiesTo Constraint) Source # reifyWhen :: MonadReify m => Bool -> Constraint -> m (ReifiesTo Constraint) Source #
Reify DisplayTerm Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo DisplayTerm Source # Methods reify :: MonadReify m => DisplayTerm -> m (ReifiesTo DisplayTerm) Source # reifyWhen :: MonadReify m => Bool -> DisplayTerm -> m (ReifiesTo DisplayTerm) Source #
Reify ProblemConstraint Source #
Instance details Defined in Agda.Interaction.BasicOps Associated Types type ReifiesTo ProblemConstraint Source # Methods reify :: MonadReify m => ProblemConstraint -> m (ReifiesTo ProblemConstraint) Source # reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (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 # Methods reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source # reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #
Reify (QNamed System) Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo (QNamed System) Source # Methods reify :: MonadReify m => QNamed System -> m (ReifiesTo (QNamed System)) Source # reifyWhen :: MonadReify m => Bool -> QNamed System -> m (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 # Methods reify :: MonadReify m => IPBoundary' a -> m (ReifiesTo (IPBoundary' a)) Source # reifyWhen :: MonadReify m => Bool -> IPBoundary' a -> m (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 #

type MonadReify m = (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.

Instances

Instances details

Reify NamedClause Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract Associated Types type ReifiesTo NamedClause Source # Methods reify :: MonadReify m => NamedClause -> m (ReifiesTo NamedClause) Source # reifyWhen :: MonadReify m => Bool -> NamedClause -> m (ReifiesTo NamedClause) Source #
PrettyTCM NamedClause Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => NamedClause -> m Doc Source #
type ReifiesTo NamedClause Source #
Instance details Defined in Agda.Syntax.Translation.InternalToAbstract type ReifiesTo NamedClause = Clause

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