Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 BindName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs BindName 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 LHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHS Source #

ToConcrete LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs LHSCore 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 Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Pattern Source #

ToConcrete RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RHS Source #

ToConcrete SpineLHS Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs SpineLHS Source #

ToConcrete TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs TypedBinding Source #

ToConcrete WhereDeclarations Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs WhereDeclarations Source #

ToConcrete ModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ModuleName Source #

ToConcrete Name Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Name Source #

ToConcrete QName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs QName Source #

ToConcrete InteractionId Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs InteractionId Source #

ToConcrete AbstractName Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs AbstractName Source #

ToConcrete ResolvedName Source #

Assumes name is not UnknownName.

Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs ResolvedName Source #

ToConcrete RangeAndPragma Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs RangeAndPragma Source #

ToConcrete NamedMeta Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs NamedMeta 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 Bool Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs Bool Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Binder' 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 (Arg a) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Arg a) Source #

ToConcrete (Constr Constructor) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Constr Constructor) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Ranged 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 => ToConcrete (IPBoundary' a) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (IPBoundary' a) Source #

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

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (List1 a) Source #

ToConcrete (Maybe BindName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe BindName) Source #

ToConcrete (Maybe Pattern) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe Pattern) Source #

ToConcrete (Maybe QName) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Associated Types

type ConOfAbs (Maybe QName) 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 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 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 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 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 = (MonadFresh NameId m, MonadInteractionPoints m, MonadStConcreteNames m, HasOptions m, PureTCM m, IsString (m Doc), Null (m Doc), Semigroup (m Doc)) Source #

The function runAbsToCon can target any monad that satisfies the constraints of MonadAbsToCon.

data AbsToCon a Source #

Instances

Instances details
HasOptions AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadReduce AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadStConcreteNames AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadTCEnv 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

MonadAddContext AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadDebug AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

MonadInteractionPoints AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

PureTCM AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasConstInfo AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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 #

Functor AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Methods

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

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

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 #

MonadFresh NameId 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 #

Null (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

IsString (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

Semigroup (AbsToCon Doc) Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

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 #