Agda-2.6.2.2: 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 where Source #

Minimal complete definition

Nothing

Associated Types

type ConOfAbs a Source #

Instances

Instances details
ToConcrete Bool Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Bool Source #

ToConcrete () Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs () Source #

Methods

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

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

ToConcrete InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId Source #

ToConcrete NamedMeta Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta Source #

ToConcrete ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName Source #

ToConcrete QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName Source #

ToConcrete Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name Source #

ToConcrete ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName Source #

ToConcrete AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName Source #

ToConcrete Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore Source #

ToConcrete LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS Source #

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS Source #

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS Source #

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations Source #

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding Source #

ToConcrete LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LamBinding Source #

ToConcrete LetBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LetBinding Source #

ToConcrete ModuleApplication Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleApplication Source #

ToConcrete Declaration Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Declaration Source #

ToConcrete Expr Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Expr Source #

ToConcrete BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName Source #

ToConcrete RangeAndPragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs [a] Source #

Methods

toConcrete :: [a] -> AbsToCon (ConOfAbs [a]) Source #

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

ToConcrete (Maybe QName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName) Source #

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) Source #

ToConcrete a => ToConcrete (List1 a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a) Source #

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (WithHiding a) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (FieldAssignment' a) Source #

(ToConcrete a, ConOfAbs a ~ LHS) => ToConcrete (Clause' a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Clause' a) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' a) Source #

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

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (IPBoundary' a) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Either a1 a2) Source #

Methods

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

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

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2) Source #

Methods

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

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

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Named name a) Source #

Methods

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

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

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

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b) Source #

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

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b) Source #

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

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (a1, a2, a3) Source #

Methods

toConcrete :: (a1, a2, a3) -> AbsToCon (ConOfAbs (a1, a2, a3)) Source #

bindToConcrete :: (a1, a2, a3) -> (ConOfAbs (a1, a2, a3) -> AbsToCon b) -> AbsToCon b Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (RewriteEqn' qn BindName p a) Source #

toConcreteCtx :: ToConcrete a => Precedence -> a -> AbsToCon (ConOfAbs a) 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 #

MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadTCEnv 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

HasBuiltins 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 #