Reflection

See the official user manual for the most up-to-date version of the information on this page.

TOC

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.