Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Translation.AbstractToConcrete

Description

The translation of abstract syntax to concrete syntax has two purposes. First it allows us to pretty print abstract syntax values without having to write a dedicated pretty printer, and second it serves as a sanity check for the concrete to abstract translation: translating from concrete to abstract and then back again should be (more or less) the identity.

Synopsis

Documentation

class ToConcrete a c | a -> c where Source #

Minimal complete definition

Nothing

Methods

toConcrete :: a -> AbsToCon c Source #

bindToConcrete :: a -> (c -> AbsToCon b) -> AbsToCon b Source #

Instances

Instances details
ToConcrete Bool Bool Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete () () Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: () -> AbsToCon () Source #

bindToConcrete :: () -> (() -> AbsToCon b) -> AbsToCon b Source #

ToConcrete InteractionId Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete NamedMeta Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete ModuleName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete QName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Name Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete ResolvedName QName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete AbstractName QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Pattern Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LHSCore Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LHS LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete SpineLHS LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete WhereDeclarations WhereClause Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete TypedBinding TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LamBinding LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete ModuleApplication ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Expr Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete BindName BoundName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete RangeAndPragma Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete LetBinding [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete Declaration [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete RHS (RHS, [RewriteEqn], [WithHiding Expr], [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete (Constr Constructor) Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete a c => ToConcrete [a] [c] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: [a] -> AbsToCon [c] Source #

bindToConcrete :: [a] -> ([c] -> AbsToCon b) -> AbsToCon b Source #

ToConcrete (Maybe QName) (Maybe Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete (Maybe Pattern) (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete a c => ToConcrete (Arg a) (Arg c) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Arg a -> AbsToCon (Arg c) Source #

bindToConcrete :: Arg a -> (Arg c -> AbsToCon b) -> AbsToCon b Source #

ToConcrete a c => ToConcrete (WithHiding a) (WithHiding c) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration] Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete a b => ToConcrete (Binder' a) (Binder' b) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ToConcrete a c => ToConcrete (IPBoundary' a) (IPBoundary' c) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (Either a1 a2) (Either c1 c2) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Either a1 a2 -> AbsToCon (Either c1 c2) Source #

bindToConcrete :: Either a1 a2 -> (Either c1 c2 -> AbsToCon b) -> AbsToCon b Source #

(ToConcrete a1 c1, ToConcrete a2 c2) => ToConcrete (a1, a2) (c1, c2) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: (a1, a2) -> AbsToCon (c1, c2) Source #

bindToConcrete :: (a1, a2) -> ((c1, c2) -> AbsToCon b) -> AbsToCon b Source #

ToConcrete a c => ToConcrete (Named name a) (Named name c) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: Named name a -> AbsToCon (Named name c) Source #

bindToConcrete :: Named name a -> (Named name c -> AbsToCon b) -> AbsToCon b Source #

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a1 c1, ToConcrete a2 c2, ToConcrete a3 c3) => ToConcrete (a1, a2, a3) (c1, c2, c3) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: (a1, a2, a3) -> AbsToCon (c1, c2, c3) Source #

bindToConcrete :: (a1, a2, a3) -> ((c1, c2, c3) -> AbsToCon b) -> AbsToCon b Source #

(ToConcrete p q, ToConcrete a b) => ToConcrete (RewriteEqn' qn p a) (RewriteEqn' () q b) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

toConcrete :: RewriteEqn' qn p a -> AbsToCon (RewriteEqn' () q b) Source #

bindToConcrete :: RewriteEqn' qn p a -> (RewriteEqn' () q b -> AbsToCon b0) -> AbsToCon b0 Source #

toConcreteCtx :: ToConcrete a c => Precedence -> a -> AbsToCon c Source #

Translate something in a context of the given precedence.

type MonadAbsToCon m = (MonadTCEnv m, ReadTCState m, MonadStConcreteNames m, HasOptions m, HasBuiltins m, MonadDebug m) Source #

We need: - Read access to the AbsToCon environment - Read access to the TC environment - Read access to the TC state - Read and write access to the stConcreteNames part of the TC state - Read access to the options - Permission to print debug messages

data AbsToCon a Source #

Instances

Instances details
Monad AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

(>>=) :: AbsToCon a -> (a -> AbsToCon b) -> AbsToCon b #

(>>) :: AbsToCon a -> AbsToCon b -> AbsToCon b #

return :: a -> AbsToCon a #

Functor AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fmap :: (a -> b) -> AbsToCon a -> AbsToCon b #

(<$) :: a -> AbsToCon b -> AbsToCon a #

MonadFail AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

fail :: String -> AbsToCon a #

Applicative AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

pure :: a -> AbsToCon a #

(<*>) :: AbsToCon (a -> b) -> AbsToCon a -> AbsToCon b #

liftA2 :: (a -> b -> c) -> AbsToCon a -> AbsToCon b -> AbsToCon c #

(*>) :: AbsToCon a -> AbsToCon b -> AbsToCon b #

(<*) :: AbsToCon a -> AbsToCon b -> AbsToCon a #

MonadTCEnv AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadStConcreteNames AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

ReadTCState AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadReader Env AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env #

local :: (Env -> Env) -> AbsToCon a -> AbsToCon a #

reader :: (Env -> a) -> AbsToCon a #

data Env Source #

Instances

Instances details
MonadReader Env AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

ask :: AbsToCon Env #

local :: (Env -> Env) -> AbsToCon a -> AbsToCon a #

reader :: (Env -> a) -> AbsToCon a #