Release notes for Agda 2 version 2.2.10
=======================================

Language
--------

* New flag: `--without-K`.

  This flag makes pattern matching more restricted. If the flag is
  activated, then Agda only accepts certain case-splits. If the type
  of the variable to be split is `D pars ixs`, where `D` is a data (or
  record) type, pars stands for the parameters, and `ixs` the indices,
  then the following requirements must be satisfied:

  - The indices `ixs` must be applications of constructors to distinct
    variables.

  - These variables must not be free in pars.

  The intended purpose of `--without-K` is to enable experiments with
  a propositional equality without the K rule. Let us define
  propositional equality as follows:

  ```agda
  data _≡_ {A : Set} : A → A → Set where
    refl : ∀ x → x ≡ x
  ```

  Then the obvious implementation of the J rule is accepted:

  ```agda
  J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
      (∀ x → P (refl x)) →
      ∀ {x y} (x≡y : x ≡ y) → P x≡y
  J P p (refl x) = p x
  ```

  The same applies to Christine Paulin-Mohring's version of the J rule:

  ```agda
  J′ : {A : Set} {x : A} (P : {y : A} → x ≡ y → Set) →
       P (refl x) →
       ∀ {y} (x≡y : x ≡ y) → P x≡y
  J′ P p (refl x) = p
  ```

  On the other hand, the obvious implementation of the K rule is not
  accepted:

  ```agda
  K : {A : Set} (P : {x : A} → x ≡ x → Set) →
      (∀ x → P (refl x)) →
      ∀ {x} (x≡x : x ≡ x) → P x≡x
  K P p (refl x) = p x
  ```

  However, we have *not* proved that activation of `--without-K`
  ensures that the K rule cannot be proved in some other way.

* Irrelevant declarations.

  Postulates and functions can be marked as irrelevant by prefixing
  the name with a dot when the name is declared. Example:

  ```agda
  postulate
    .irrelevant : {A : Set} → .A → A
  ```

  Irrelevant names may only be used in irrelevant positions or in
  definitions of things which have been declared irrelevant.

  The axiom irrelevant above can be used to define a projection from
  an irrelevant record field:

  ```agda
  data Subset (A : Set) (P : A → Set) : Set where
    _#_ : (a : A) → .(P a) → Subset A P

  elem : ∀ {A P} → Subset A P → A
  elem (a # p) = a

  .certificate : ∀ {A P} (x : Subset A P) → P (elem x)
  certificate (a # p) = irrelevant p
  ```

  The right-hand side of certificate is relevant, so we cannot define

  ```agda
  certificate (a # p) = p
  ```

  (because `p` is irrelevant). However, certificate is declared to be
  irrelevant, so it can use the axiom irrelevant. Furthermore the
  first argument of the axiom is irrelevant, which means that
  irrelevant `p` is well-formed.

  As shown above the axiom irrelevant justifies irrelevant
  projections. Previously no projections were generated for irrelevant
  record fields, such as the field certificate in the following
  record type:

  ```agda
  record Subset (A : Set) (P : A → Set) : Set where
    constructor _#_
    field
      elem         : A
      .certificate : P elem
  ```

  Now projections are generated automatically for irrelevant fields
  (unless the flag `--no-irrelevant-projections` is used). Note that
  irrelevant projections are highly experimental.

* Termination checker recognises projections.

  Projections now preserve sizes, both in patterns and expressions.
  Example:

  ```agda
  record Wrap (A : Set) : Set where
    constructor wrap
    field
      unwrap : A

  open Wrap public

  data WNat : Set where
    zero : WNat
    suc  : Wrap WNat → WNat

  id : WNat → WNat
  id zero    = zero
  id (suc w) = suc (wrap (id (unwrap w)))
  ```

  In the structural ordering `unwrap w` ≤ `w`. This means that

  ```agda
    unwrap w ≤ w < suc w,
  ```

  and hence the recursive call to id is accepted.

  Projections also preserve guardedness.

Tools
-----

* Hyperlinks for top-level module names now point to the start of the
  module rather than to the declaration of the module name. This
  applies both to the Emacs mode and to the output of `agda --html`.

* Most occurrences of record field names are now highlighted as
  "fields". Previously many occurrences were highlighted as
  "functions".

* Emacs mode: It is no longer possible to change the behaviour of the
  `TAB` key by customising `agda2-indentation`.

* Epic compiler backend.

  A new compiler backend is being implemented. This backend makes use
  of Edwin Brady's language Epic
  (http://www.cs.st-andrews.ac.uk/~eb/epic.php) and its compiler. The
  backend should handle most Agda code, but is still at an
  experimental stage: more testing is needed, and some things written
  below may not be entirely true.

  The Epic compiler can be invoked from the command line using the
  flag `--epic`:

  ```
  agda --epic --epic-flag=<EPIC-FLAG> --compile-dir=<DIR> <FILE>.agda
  ```

  The `--epic-flag` flag can be given multiple times; each flag is
  given verbatim to the Epic compiler (in the given order). The
  resulting executable is named after the main module and placed in
  the directory specified by the `--compile-dir` flag (default: the
  project root). Intermediate files are placed in a subdirectory
  called `Epic`.

  The backend requires that there is a definition named main. This
  definition should be a value of type `IO Unit`, but at the moment
  this is not checked (so it is easy to produce a program which
  segfaults).  Currently the backend represents actions of type `IO A`
  as functions from `Unit` to `A`, and main is applied to the unit
  value.

  The Epic compiler compiles via C, not Haskell, so the pragmas
  related to the Haskell FFI (`IMPORT`, `COMPILED_DATA` and
  `COMPILED`) are not used by the Epic backend. Instead there is a new
  pragma `COMPILED_EPIC`. This pragma is used to give Epic code for
  postulated definitions (Epic code can in turn call C code). The form
  of the pragma is `{-# COMPILED_EPIC def code #-}`, where `def` is
  the name of an Agda postulate and `code` is some Epic code which
  should include the function arguments, return type and function
  body. As an example the `IO` monad can be defined as follows:

  ```agda
  postulate
    IO     : Set → Set
    return : ∀ {A} → A → IO A
    _>>=_  : ∀ {A B} → IO A → (A → IO B) → IO B

  {-# COMPILED_EPIC return (u : Unit, a : Any) -> Any =
                      ioreturn(a) #-}
  {-# COMPILED_EPIC
        _>>=_ (u1 : Unit, u2 : Unit, x : Any, f : Any) -> Any =
          iobind(x,f) #-}
  ```

  Here `ioreturn` and `iobind` are Epic functions which are defined in
  the file `AgdaPrelude.e` which is always included.

  By default the backend will remove so-called forced constructor
  arguments (and case-splitting on forced variables will be
  rewritten). This optimisation can be disabled by using the flag
  `--no-forcing`.

  All data types which look like unary natural numbers after forced
  constructor arguments have been removed (i.e. types with two
  constructors, one nullary and one with a single recursive argument)
  will be represented as "BigInts". This applies to the standard `Fin`
  type, for instance.

  The backend supports Agda's primitive functions and the BUILTIN
  pragmas. If the BUILTIN pragmas for unary natural numbers are used,
  then some operations, like addition and multiplication, will use
  more efficient "BigInt" operations.

  If you want to make use of the Epic backend you need to install some
  dependencies, see the README.

* The Emacs mode can compile using either the MAlonzo or the Epic
  backend. The variable `agda2-backend` controls which backend is
  used.