# Reflection

Since AIM XI, it has become possible to access a representation of the current goal. The development version of Agda now comes with two constructs (`quoteGoal_in_`

and `quote`

) and a datatype (`Term`

) which allow functions to scrutinize the goal.

## Related files

You might want to take a look at these two files:

Agda/test/succeed/Reflection.agda Agda/test/succeed/Common/Reflect.agda

They are not really re-usable at the moment as they are referring to built-in booleans, naturals: if you try to load the corresponding libraries, Agda will yield « Duplicate binding for built-in thing XXX ».

If you want to use these files, you will have to modify them a little bit in order to use only one binding.

## Typing rules

quoteGoal gives access to the current goal:

Γ , t : ′A ⊢ e : Aℕ1 : Check 1 ℕ1 = quoteGoal t in t is unknown of course ℕ1 = quoteGoal t in t is con ( quote ℕ.suc ) (argᵛʳ (con (quote ℕ.zero) []) ∷ []) of course ======================== Γ ⊢ quoteGoal t in e : A

If `x`

is the identifier of a definition (function, datatype, ...), then we have:

Γ ⊢ x : A ================ Γ ⊢ quote x : ′A

## Internal representation

The quoted terms are represented using the datatype `Term`

which definition depends on the definition of `Arg`

and `Args`

.

`Hiding`

is an alias for`Bool`

and has a straightforward meaning;- Variables refer to their binders thanks to de Bruijn indices;
`unknown`

is used to make the`Term`

grammar total. Values such as`1`

will be referred to using this constructor. data Arg A : Set where arg : Hiding → A → Arg A mutual

data Term : Set where var : Nat → Args → Term con : QName → Args → Term def : QName → Args → Term lam : Hiding → Term → Term pi : Arg Term → Term → Term sort : Term unknown : Term Args = List (Arg Term)

## How to use it?

Here are a couple of examples to illustrate the way goals are quoted. The `Check`

construct allows to construct interactively the `Term`

corresponding to the goal given as an argument (see the missing definitions in the above related files).

Nat : Check ℕ Nat = quoteGoal t in t is def (quote ℕ) [] of course ℕ1 : Check 1 ℕ1 = quoteGoal t in t is con ( quote ℕ.suc ) (argᵛʳ (con (quote ℕ.zero) []) ∷ []) of course identity : Check ((A : Set) → A → A) identity = quoteGoal t in t is pi (argᵛʳ set₀) (el₀ (pi (argᵛʳ (el₀ (var 0 []))) (el₀ (var 1 [])))) of course

- Reflection. There are two new constructs for reflection:

- quoteGoal x in e In e the value of x will be a representation of the goal type (the type expected of the whole expression) as an element in a datatype of Agda terms (see below). For instance, example : ℕ example = quoteGoal x in {! at this point x = def (quote ℕ) [] !} - quote x : Name If x is the name of a definition (function, datatype, record, or a constructor), quote x gives you the representation of x as a value in the primitive type Name (see below).

- Quoted terms use the following BUILTINs and primitives (available from the standard library module Reflection):

-- The type of Agda names. postulate Name : Set {-# BUILTIN QNAME Name #-} primitive primQNameEquality : Name → Name → Bool -- Arguments. Explicit? = Bool data Arg A : Set where arg : Explicit? → A → Arg A {-# BUILTIN ARG Arg #-} {-# BUILTIN ARGARG arg #-} -- The type of Agda terms. data Term : Set where var : ℕ → List (Arg Term) → Term con : Name → List (Arg Term) → Term def : Name → List (Arg Term) → Term lam : Explicit? → Term → Term pi : Arg Term → Term → Term sort : Term unknown : Term {-# BUILTIN AGDATERM Term #-} {-# BUILTIN AGDATERMVAR var #-} {-# BUILTIN AGDATERMCON con #-} {-# BUILTIN AGDATERMDEF def #-} {-# BUILTIN AGDATERMLAM lam #-} {-# BUILTIN AGDATERMPI pi #-}t : Check ℕ Nat = quoteGoal t in t is def (quote ℕ) [] of course {-# BUILTIN AGDATERMSORT sort #-} {-# BUILTIN AGDATERMUNSUPPORTED unknown #-} Reflection may be useful when working with internal decision procedures, such as the standard library's ring solver.