Pragmas

Pragmas are special declarations that pass extra information to Agda about how regular declarations are to be interpreted. They are written similar to block comments so that users may easily skip them in a first reading of an Agda document. The general format is:

  1. {-# <PRAGMA_NAME> <arguments> #-}

Index of pragmas

See also Command-line and pragma options.

The DISPLAY pragma

Users can declare a display form via the DISPLAY pragma:

  1. {-# DISPLAY f e1 .. en = e #-}

This causes f e1 .. en to be printed in the same way as e, where ei can bind variables used in e. The expressions ei and e are scope checked, but not type checked.

For example this can be used to print overloaded (instance) functions with the overloaded name:

  1. instance
  2.   NumNat : Num Nat
  3.   NumNat = record { ..; _+_ = natPlus }
  5. {-# DISPLAY natPlus a b = a + b #-}

Limitations:

  • Left-hand sides of the display form are restricted to variables, constructors, defined functions or types, and literals. In particular, lambdas are not allowed in left-hand sides.

  • Since display forms are not type checked, implicit argument insertion may not work properly if the type of f computes to an implicit function space after pattern matching.

  • An ill-typed display form can make Agda crash with an internal error when Agda tries to use it (issue #6476 <https://github.com/agda/agda/issues/6476&gt;).

The INJECTIVE pragma

Injective pragmas can be used to mark a definition as injective for the pattern matching unifier. This can be used as a version of --injective-type-constructors that only applies to specific datatypes.

Example:

  1. open import Agda.Builtin.Equality
  2. open import Agda.Builtin.Nat
  4. data Fin : Nat → Set where
  5.   zero : {n : Nat} → Fin (suc n)
  6.   suc  : {n : Nat} → Fin n → Fin (suc n)
  8. {-# INJECTIVE Fin #-}
  10. Fin-injective : {m n : Nat} → Fin m ≡ Fin n → m ≡ n
  11. Fin-injective refl = refl

Aside from datatypes, this pragma can also be used to mark other definitions as being injective (for example postulates).

At the moment it only gives you propositional injectivity, so you can pattern match on a proof of Fin x ≡ Fin y in example above, but does not give you definitional injectivity, so the constraint solver does not know how to solve the constraint Fin x = Fin _. Relevant issue: https://github.com/agda/agda/issues/4106#issuecomment-534904561

The INLINE and NOINLINE pragmas

A function definition marked with an INLINE pragma is inlined during compilation. If it is a simple function definition that does no pattern matching, it is also inlined in function bodies at type-checking time.

When the --auto-inline command-line option is enabled, function definitions are automatically marked INLINE if they satisfy the following criteria:

  • No pattern matching.

  • Uses each argument at most once.

  • Does not use all its arguments.

Automatic inlining can be prevented using the NOINLINE pragma.

Example:

  1. -- Would be auto-inlined since it doesn't use the type arguments.
  2. _∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
  3. (f ∘ g) x = f (g x)
  5. {-# NOINLINE _∘_ #-} -- prevents auto-inlining
  7. -- Would not be auto-inlined since it's using all its arguments
  8. _o_ : (Set → Set) → (Set → Set) → Set → Set
  9. (F o G) X = F (G X)
  11. {-# INLINE _o_ #-} -- force inlining

Inlining constructor right-hand sides

New in version 2.6.4.

Constructors can also be marked INLINE (for types supporting co-pattern matching):

  1. record Stream (A : Set) : Set where
  2.   coinductive; constructor _∷_
  3.   field head : A
  4.         tail : Stream A
  5. open Stream
  6. {-# INLINE _∷_ #-}

Functions definitions using these constructors will be translated to use co-pattern matching instead, e.g.:

  1. nats : Nat → Stream Nat
  2. nats n = n ∷ nats (1 + n)

is translated to:

  1. nats' : Nat → Stream Nat
  2. nats' n .head = n
  3. nats' n .tail = nats (n + 1)

which passes termination-checking.

This translation only works for fully-applied constructors at the root of a function definition’s right-hand side.

If --exact-split is on, the inlining will trigger a InlineNoExactSplit warning for nats.

The NON_COVERING pragma

New in version 2.6.1.

The NON_COVERING pragma can be placed before a function (or a block of mutually defined functions) which the user knows to be partial. To be used as a version of --allow-incomplete-matches that only applies to specific functions.

The NOT_PROJECTION_LIKE pragma

New in version 2.6.3.

The NOT_PROJECTION_LIKE pragma disables projection-likeness analysis for a particular function, which must be defined before it can be affected by the pragma. To be used as a version of --no-projection-like that only applies to specific functions.

For example, suppose you have a function which projects a field from an instance argument, and instance selection depends on a visible argument. If an application of this function is generated by metaprogramming, and inserted in the source code by elaborate-and-give (C-c C-m in Emacs), the visible argument would instead be printed as _, because it was erased!

Example:

  1. open import Agda.Builtin.Bool
  3. record P (n : Nat) : Set where
  4.   field the-bool : Bool
  5. open P
  7. -- Agda would normally mark this projection-like, so it would have its
  8. -- (n : Nat) argument erased when printing, including by e.g.
  9. -- elaborate-and-give
  10. get-bool-from-p : (n : Nat) ⦃ has-p : P n ⦄ → Bool
  11. get-bool-from-p _ ⦃ p ⦄ = p .the-bool
  12. {-# NOT_PROJECTION_LIKE get-bool-from-p #-}
  14. -- With the pragma, it gets treated as a regular function.

The OPTIONS pragma

Some options can be given at the top of .agda files in the form

{-# OPTIONS --{opt₁} --{opt₂} ... #-}

The possible options are listed in Command-line and pragma options.

The WARNING_ON_ pragmas

A library author can use a WARNING_ON_USAGE pragma to attach to a defined name a warning to be raised whenever this name is used (since Agda 2.5.4).

Similarly they can use a WARNING_ON_IMPORT pragma to attach to a module a warning to be raised whenever this module is imported (since Agda 2.6.1).

This would typically be used to declare a name or a module ‘DEPRECATED’ and advise the end-user to port their code before the feature is dropped.

Users can turn these warnings off by using the --warn=noUserWarning option. For more information about the warning machinery, see Warnings.

Example:

  1. -- The new name for the identity
  2. id : {A : Set} → A → A
  3. id x = x
  5. -- The deprecated name
  6. λx→x = id
  8. -- The warning
  9. {-# WARNING_ON_USAGE λx→x "DEPRECATED: Use `id` instead of `λx→x`" #-}
  10. {-# WARNING_ON_IMPORT "DEPRECATED: Use module `Function.Identity` rather than `Identity`" #-}