Release notes for Agda 2 version 2.4.0
======================================
Installation and infrastructure
-------------------------------
* A new module called `Agda.Primitive` has been introduced. This
module is available to all users, even if the standard library is
not used. Currently the module contains level primitives and their
representation in Haskell when compiling with MAlonzo:
```agda
infixl 6 _⊔_
postulate
Level : Set
lzero : Level
lsuc : (ℓ : Level) → Level
_⊔_ : (ℓ₁ ℓ₂ : Level) → Level
{-# COMPILED_TYPE Level () #-}
{-# COMPILED lzero () #-}
{-# COMPILED lsuc (\_ -> ()) #-}
{-# COMPILED _⊔_ (\_ _ -> ()) #-}
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}
```
To bring these declarations into scope you can use a declaration
like the following one:
```agda
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
```
The standard library reexports these primitives (using the names
`zero` and `suc` instead of `lzero` and `lsuc`) from the `Level`
module.
Existing developments using universe polymorphism might now trigger
the following error message:
```
Duplicate binding for built-in thing LEVEL, previous binding to
.Agda.Primitive.Level
```
To fix this problem, please remove the duplicate bindings.
Technical details (perhaps relevant to those who build Agda
packages):
The include path now always contains a directory
`<DATADIR>/lib/prim`, and this directory is supposed to contain a
subdirectory Agda containing a file `Primitive.agda`.
The standard location of `<DATADIR>` is system- and
installation-specific. E.g., in a Cabal `--user` installation of
Agda-2.3.4 on a standard single-ghc Linux system it would be
`$HOME/.cabal/share/Agda-2.3.4` or something similar.
The location of the `<DATADIR>` directory can be configured at
compile-time using Cabal flags (`--datadir` and `--datasubdir`).
The location can also be set at run-time, using the `Agda_datadir`
environment variable.
Pragmas and options
-------------------
* Pragma `NO_TERMINATION_CHECK` placed within a mutual block is now
applied to the whole mutual block (rather than being discarded
silently). Adding to the uses 1.-4. outlined in the release notes
for 2.3.2 we allow:
3a. Skipping an old-style mutual block: Somewhere within `mutual`
block before a type signature or first function clause.
```agda
mutual
{-# NO_TERMINATION_CHECK #-}
c : A
c = d
d : A
d = c
```
* New option `--no-pattern-matching`
Disables all forms of pattern matching (for the current file).
You can still import files that use pattern matching.
* New option `-v profile:7`
Prints some stats on which phases Agda spends how much time.
(Number might not be very reliable, due to garbage collection
interruptions, and maybe due to laziness of Haskell.)
* New option `--no-sized-types`
Option `--sized-types` is now default. `--no-sized-types` will turn
off an extra (inexpensive) analysis on data types used for subtyping
of sized types.
Language
--------
* Experimental feature: `quoteContext`
There is a new keyword `quoteContext` that gives users access to the
list of names in the current local context. For instance:
```agda
open import Data.Nat
open import Data.List
open import Reflection
foo : ℕ → ℕ → ℕ
foo 0 m = 0
foo (suc n) m = quoteContext xs in ?
```
In the remaining goal, the list `xs` will consist of two names, `n`
and `m`, corresponding to the two local variables. At the moment it
is not possible to access let bound variables (this feature may be
added in the future).
* Experimental feature: Varying arity.
Function clauses may now have different arity, e.g.,
```agda
Sum : ℕ → Set
Sum 0 = ℕ
Sum (suc n) = ℕ → Sum n
sum : (n : ℕ) → ℕ → Sum n
sum 0 acc = acc
sum (suc n) acc m = sum n (m + acc)
```
or,
```agda
T : Bool → Set
T true = Bool
T false = Bool → Bool
f : (b : Bool) → T b
f false true = false
f false false = true
f true = true
```
This feature is experimental. Yet unsupported:
- Varying arity and `with`.
- Compilation of functions with varying arity to Haskell, JS, or Epic.
* Experimental feature: copatterns. (Activated with option `--copatterns`)
We can now define a record by explaining what happens if you project
the record. For instance:
```agda
{-# OPTIONS --copatterns #-}
record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
open _×_
pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b
swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p
swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t) = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t
```
Taking a projection on the left hand side (lhs) is called a
projection pattern, applying to a pattern is called an application
pattern. (Alternative terms: projection/application copattern.)
In the first example, the symbol `pair`, if applied to variable
patterns `a` and `b` and then projected via `fst`, reduces to
`a`. `pair` by itself does not reduce.
A typical application are coinductive records such as streams:
```agda
record Stream (A : Set) : Set where
coinductive
field
head : A
tail : Stream A
open Stream
repeat : {A : Set} (a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a
```
Again, `repeat a` by itself will not reduce, but you can take a
projection (head or tail) and then it will reduce to the respective
rhs. This way, we get the lazy reduction behavior necessary to
avoid looping corecursive programs.
Application patterns do not need to be trivial (i.e., variable
patterns), if we mix with projection patterns. E.g., we can have
```agda
nats : Nat -> Stream Nat
head (nats zero) = zero
tail (nats zero) = nats zero
head (nats (suc x)) = x
tail (nats (suc x)) = nats x
```
Here is an example (not involving coinduction) which demostrates
records with fields of function type:
```agda
-- The State monad
record State (S A : Set) : Set where
constructor state
field
runState : S → A × S
open State
-- The Monad type class
record Monad (M : Set → Set) : Set1 where
constructor monad
field
return : {A : Set} → A → M A
_>>=_ : {A B : Set} → M A → (A → M B) → M B
-- State is an instance of Monad
-- Demonstrates the interleaving of projection and application patterns
stateMonad : {S : Set} → Monad (State S)
runState (Monad.return stateMonad a ) s = a , s
runState (Monad._>>=_ stateMonad m k) s₀ =
let a , s₁ = runState m s₀
in runState (k a) s₁
module MonadLawsForState {S : Set} where
open Monad (stateMonad {S})
leftId : {A B : Set}(a : A)(k : A → State S B) →
(return a >>= k) ≡ k a
leftId a k = refl
rightId : {A B : Set}(m : State S A) →
(m >>= return) ≡ m
rightId m = refl
assoc : {A B C : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
((m >>= k) >>= l) ≡ (m >>= λ a → (k a >>= l))
assoc m k l = refl
```
Copatterns are yet experimental and the following does not work:
- Copatterns and `with` clauses.
- Compilation of copatterns to Haskell, JS, or Epic.
- Projections generated by
```agda
open R {{...}}
```
are not handled properly on lhss yet.
- Conversion checking is slower in the presence of copatterns, since
stuck definitions of record type do no longer count as neutral,
since they can become unstuck by applying a projection. Thus,
comparing two neutrals currently requires comparing all they
projections, which repeats a lot of work.
* Top-level module no longer required.
The top-level module can be omitted from an Agda file. The module
name is then inferred from the file name by dropping the path and
the `.agda` extension. So, a module defined in `/A/B/C.agda` would get
the name `C`.
You can also suppress only the module name of the top-level module
by writing
```agda
module _ where
```
This works also for parameterised modules.
* Module parameters are now always hidden arguments in projections.
For instance:
```agda
module M (A : Set) where
record Prod (B : Set) : Set where
constructor _,_
field
fst : A
snd : B
open Prod public
open M
```
Now, the types of `fst` and `snd` are
```agda
fst : {A : Set}{B : Set} → Prod A B → A
snd : {A : Set}{B : Set} → Prod A B → B
```
Until 2.3.2, they were
```agda
fst : (A : Set){B : Set} → Prod A B → A
snd : (A : Set){B : Set} → Prod A B → B
```
This change is a step towards symmetry of constructors and projections.
(Constructors always took the module parameters as hidden arguments).
* Telescoping lets: Local bindings are now accepted in telescopes
of modules, function types, and lambda-abstractions.
The syntax of telescopes as been extended to support `let`:
```agda
id : (let ★ = Set) (A : ★) → A → A
id A x = x
```
In particular one can now `open` modules inside telescopes:
```agda
module Star where
★ : Set₁
★ = Set
module MEndo (let open Star) (A : ★) where
Endo : ★
Endo = A → A
```
Finally a shortcut is provided for opening modules:
```agda
module N (open Star) (A : ★) (open MEndo A) (f : Endo) where
...
```
The semantics of the latter is
```agda
module _ where
open Star
module _ (A : ★) where
open MEndo A
module N (f : Endo) where
...
```
The semantics of telescoping lets in function types and lambda
abstractions is just expanding them into ordinary lets.
* More liberal left-hand sides in lets
[Issue [#1028](https://github.com/agda/agda/issues/1028)]:
You can now write left-hand sides with arguments also for let
bindings without a type signature. For instance,
```agda
let f x = suc x in f zero
```
Let bound functions still can't do pattern matching though.
* Ambiguous names in patterns are now optimistically resolved in favor
of constructors. [Issue [#822](https://github.com/agda/agda/issues/822)]
In particular, the following succeeds now:
```agda
module M where
data D : Set₁ where
[_] : Set → D
postulate [_] : Set → Set
open M
Foo : _ → Set
Foo [ A ] = A
```
* Anonymous `where`-modules are opened
public. [Issue [#848](https://github.com/agda/agda/issues/848)]
```
<clauses>
f args = rhs
module _ telescope where
body
<more clauses>
```
means the following (not proper Agda code, since you cannot put a
module in-between clauses)
```
<clauses>
module _ {arg-telescope} telescope where
body
f args = rhs
<more clauses>
```
Example:
```agda
A : Set1
A = B module _ where
B : Set1
B = Set
C : Set1
C = B
```
* Builtin `ZERO` and `SUC` have been merged with `NATURAL`.
When binding the `NATURAL` builtin, `ZERO` and `SUC` are bound to
the appropriate constructors automatically. This means that instead
of writing
```agda
{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
```
you just write
```agda
{-# BUILTIN NATURAL Nat #-}
```
* Pattern synonym can now have implicit
arguments. [Issue [#860](https://github.com/agda/agda/issues/860)]
For example,
```agda
pattern tail=_ {x} xs = x ∷ xs
len : ∀ {A} → List A → Nat
len [] = 0
len (tail= xs) = 1 + len xs
```
* Syntax declarations can now have implicit
arguments. [Issue [#400](https://github.com/agda/agda/issues/400)]
For example
```agda
id : ∀ {a}{A : Set a} -> A -> A
id x = x
syntax id {A} x = x ∈ A
```
* Minor syntax changes
- `-}` is now parsed as end-comment even if no comment was begun. As
a consequence, the following definition gives a parse error
```agda
f : {A- : Set} -> Set
f {A-} = A-
```
because Agda now sees `ID(f) LBRACE ID(A) END-COMMENT`, and no
longer `ID(f) LBRACE ID(A-) RBRACE`.
The rational is that the previous lexing was to context-sensitive,
attempting to comment-out `f` using `{-` and `-}` lead to a parse
error.
- Fixities (binding strengths) can now be negative numbers as
well. [Issue [#1109](https://github.com/agda/agda/issues/1109)]
```agda
infix -1 _myop_
```
- Postulates are now allowed in mutual
blocks. [Issue [#977](https://github.com/agda/agda/issues/977)]
- Empty where blocks are now
allowed. [Issue [#947](https://github.com/agda/agda/issues/947)]
- Pattern synonyms are now allowed in parameterised
modules. [Issue [#941](https://github.com/agda/agda/issues/941)]
- Empty hiding and renaming lists in module directives are now allowed.
- Module directives `using`, `hiding`, `renaming` and `public` can
now appear in arbitrary order. Multiple
`using`/`hiding`/`renaming` directives are allowed, but you still
cannot have both using and `hiding` (because that doesn't make
sense). [Issue [#493](https://github.com/agda/agda/issues/493)]
Goal and error display
----------------------
* The error message `Refuse to construct infinite term` has been
removed, instead one gets unsolved meta variables. Reason: the
error was thrown over-eagerly.
[Issue [#795](https://github.com/agda/agda/issues/795)]
* If an interactive case split fails with message
```
Since goal is solved, further case distinction is not supported;
try `Solve constraints' instead
```
then the associated interaction meta is assigned to a solution.
Press `C-c C-=` (Show constraints) to view the solution and `C-c
C-s` (Solve constraints) to apply it.
[Issue [#289](https://github.com/agda/agda/issues/289)]
Type checking
-------------
* [ Issue [#376](https://github.com/agda/agda/issues/376) ]
Implemented expansion of bound record variables during meta
assignment. Now Agda can solve for metas X that are applied to
projected variables, e.g.:
```agda
X (fst z) (snd z) = z
X (fst z) = fst z
```
Technically, this is realized by substituting `(x , y)` for `z` with fresh
bound variables `x` and `y`. Here the full code for the examples:
```agda
record Sigma (A : Set)(B : A -> Set) : Set where
constructor _,_
field
fst : A
snd : B fst
open Sigma
test : (A : Set) (B : A -> Set) ->
let X : (x : A) (y : B x) -> Sigma A B
X = _
in (z : Sigma A B) -> X (fst z) (snd z) ≡ z
test A B z = refl
test' : (A : Set) (B : A -> Set) ->
let X : A -> A
X = _
in (z : Sigma A B) -> X (fst z) ≡ fst z
test' A B z = refl
```
The fresh bound variables are named `fst(z)` and `snd(z)` and can appear
in error messages, e.g.:
```agda
fail : (A : Set) (B : A -> Set) ->
let X : A -> Sigma A B
X = _
in (z : Sigma A B) -> X (fst z) ≡ z
fail A B z = refl
```
results in error:
```
Cannot instantiate the metavariable _7 to solution fst(z) , snd(z)
since it contains the variable snd(z) which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
when checking that the expression refl has type _7 A B (fst z) ≡ z
```
* Dependent record types and definitions by copatterns require
reduction with previous function clauses while checking the current
clause. [Issue [#907](https://github.com/agda/agda/issues/907)]
For a simple example, consider
```agda
test : ∀ {A} → Σ Nat λ n → Vec A n
proj₁ test = zero
proj₂ test = []
```
For the second clause, the lhs and rhs are typed as
```agda
proj₂ test : Vec A (proj₁ test)
[] : Vec A zero
```
In order for these types to match, we have to reduce the lhs type
with the first function clause.
Note that termination checking comes after type checking, so be
careful to avoid non-termination! Otherwise, the type checker
might get into an infinite loop.
* The implementation of the primitive `primTrustMe` has changed. It
now only reduces to `REFL` if the two arguments `x` and `y` have the
same computational normal form. Before, it reduced when `x` and `y`
were definitionally equal, which included type-directed equality
laws such as eta-equality. Yet because reduction is untyped,
calling conversion from reduction lead to Agda crashes
[Issue [#882](https://github.com/agda/agda/issues/882)].
The amended description of `primTrustMe` is (cf. release notes
for 2.2.6):
```agda
primTrustMe : {A : Set} {x y : A} → x ≡ y
```
Here `_≡_` is the builtin equality (see BUILTIN hooks for equality,
above).
If `x` and `y` have the same computational normal form, then
`primTrustMe {x = x} {y = y}` reduces to `refl`.
A note on `primTrustMe`'s runtime behavior: The MAlonzo compiler
replaces all uses of `primTrustMe` with the `REFL` builtin, without
any check for definitional equality. Incorrect uses of `primTrustMe`
can potentially lead to segfaults or similar problems of the
compiled code.
* Implicit patterns of record type are now only eta-expanded if there
is a record constructor.
[Issues [#473](https://github.com/agda/agda/issues/473),
[#635](https://github.com/agda/agda/issues/635)]
```agda
data D : Set where
d : D
data P : D → Set where
p : P d
record Rc : Set where
constructor c
field f : D
works : {r : Rc} → P (Rc.f r) → Set
works p = D
```
This works since the implicit pattern `r` is eta-expanded to `c x`
which allows the type of `p` to reduce to `P x` and `x` to be
unified with `d`. The corresponding explicit version is:
```agda
works' : (r : Rc) → P (Rc.f r) → Set
works' (c .d) p = D
```
However, if the record constructor is removed, the same example will
fail:
```agda
record R : Set where
field f : D
fails : {r : R} → P (R.f r) → Set
fails p = D
-- d != R.f r of type D
-- when checking that the pattern p has type P (R.f r)
```
The error is justified since there is no pattern we could write down
for `r`. It would have to look like
```agda
record { f = .d }
```
but anonymous record patterns are not part of the language.
* Absurd lambdas at different source locations are no longer
different. [Issue [#857](https://github.com/agda/agda/issues/857)]
In particular, the following code type-checks now:
```agda
absurd-equality : _≡_ {A = ⊥ → ⊥} (λ()) λ()
absurd-equality = refl
```
Which is a good thing!
* Printing of named implicit function types.
When printing terms in a context with bound variables Agda renames
new bindings to avoid clashes with the previously bound names. For
instance, if `A` is in scope, the type `(A : Set) → A` is printed as
`(A₁ : Set) → A₁`. However, for implicit function types the name of
the binding matters, since it can be used when giving implicit
arguments.
For this situation, the following new syntax has been introduced:
`{x = y : A} → B` is an implicit function type whose bound variable
(in scope in `B`) is `y`, but where the name of the argument is `x`
for the purposes of giving it explicitly. For instance, with `A` in
scope, the type `{A : Set} → A` is now printed as `{A = A₁ : Set} →
A₁`.
This syntax is only used when printing and is currently not being parsed.
* Changed the semantics of `--without-K`.
[Issue [#712](https://github.com/agda/agda/issues/712),
Issue [#865](https://github.com/agda/agda/issues/865),
Issue [#1025](https://github.com/agda/agda/issues/1025)]
New specification of `--without-K`:
When `--without-K` is enabled, the unification of indices for
pattern matching is restricted in two ways:
1. Reflexive equations of the form `x == x` are no longer solved,
instead Agda gives an error when such an equation is encountered.
2. When unifying two same-headed constructor forms `c us` and `c vs`
of type `D pars ixs`, the datatype indices `ixs` (but not the
parameters) have to be *self-unifiable*, i.e. unification of
`ixs` with itself should succeed positively. This is a nontrivial
requirement because of point 1.
Examples:
- 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
```agda
This definition is accepted since unification of `x` with `y`
doesn't require deletion or injectivity.
- The K rule is rejected.
```agda
K : {A : Set} (P : {x : A} → x ≡ x → Set) →
(∀ x → P (refl {x = x})) →
∀ {x} (x≡x : x ≡ x) → P x≡x
K P p refl = p _
```
Definition is rejected with the following error:
```
Cannot eliminate reflexive equation x = x of type A because K has
been disabled.
when checking that the pattern refl has type x ≡ x
```
- Symmetry of the new criterion.
```agda
test₁ : {k l m : ℕ} → k + l ≡ m → ℕ
test₁ refl = zero
test₂ : {k l m : ℕ} → k ≡ l + m → ℕ
test₂ refl = zero
```
Both versions are now accepted (previously only the first one was).
- Handling of parameters.
```agda
cons-injective : {A : Set} (x y : A) → (x ∷ []) ≡ (y ∷ []) → x ≡ y
cons-injective x .x refl = refl
```
Parameters are not unified, so they are ignored by the new criterion.
- A larger example: antisymmetry of ≤.
```agda
data _≤_ : ℕ → ℕ → Set where
lz : (n : ℕ) → zero ≤ n
ls : (m n : ℕ) → m ≤ n → suc m ≤ suc n
≤-antisym : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n
≤-antisym .zero .zero (lz .zero) (lz .zero) = refl
≤-antisym .(suc m) .(suc n) (ls m n p) (ls .n .m q) =
cong suc (≤-antisym m n p q)
```
- [ Issue [#1025](https://github.com/agda/agda/issues/1025) ]
```agda
postulate mySpace : Set
postulate myPoint : mySpace
data Foo : myPoint ≡ myPoint → Set where
foo : Foo refl
test : (i : foo ≡ foo) → i ≡ refl
test refl = {!!}
```
When applying injectivity to the equation `foo ≡ foo` of type `Foo
refl`, it is checked that the index `refl` of type `myPoint ≡
myPoint` is self-unifiable. The equation `refl ≡ refl` again
requires injectivity, so now the index `myPoint` is checked for
self-unifiability, hence the error:
```
Cannot eliminate reflexive equation myPoint = myPoint of type
mySpace because K has been disabled.
when checking that the pattern refl has type foo ≡ foo
```
Termination checking
--------------------
* A buggy facility coined "matrix-shaped orders" that supported
uncurried functions (which take tuples of arguments instead of one
argument after another) has been removed from the termination
checker. [Issue [#787](https://github.com/agda/agda/issues/787)]
* Definitions which fail the termination checker are not unfolded any
longer to avoid loops or stack overflows in Agda. However, the
termination checker for a mutual block is only invoked after
type-checking, so there can still be loops if you define a
non-terminating function. But termination checking now happens
before the other supplementary checks: positivity, polarity,
injectivity and projection-likeness. Note that with the pragma `{-#
NO_TERMINATION_CHECK #-}` you can make Agda treat any function as
terminating.
* Termination checking of functions defined by `with` has been improved.
Cases which previously required `--termination-depth` to pass the
termination checker (due to use of `with`) no longer need the
flag. For example
```agda
merge : List A → List A → List A
merge [] ys = ys
merge xs [] = xs
merge (x ∷ xs) (y ∷ ys) with x ≤ y
merge (x ∷ xs) (y ∷ ys) | false = y ∷ merge (x ∷ xs) ys
merge (x ∷ xs) (y ∷ ys) | true = x ∷ merge xs (y ∷ ys)
```
This failed to termination check previously, since the `with`
expands to an auxiliary function `merge-aux`:
```agda
merge-aux x y xs ys false = y ∷ merge (x ∷ xs) ys
merge-aux x y xs ys true = x ∷ merge xs (y ∷ ys)
```
This function makes a call to `merge` in which the size of one of
the arguments is increasing. To make this pass the termination
checker now inlines the definition of `merge-aux` before checking,
thus effectively termination checking the original source program.
As a result of this transformation doing `with` on a variable no longer
preserves termination. For instance, this does not termination check:
```agda
bad : Nat → Nat
bad n with n
... | zero = zero
... | suc m = bad m
```
* The performance of the termination checker has been improved. For
higher `--termination-depth` the improvement is significant. While
the default `--termination-depth` is still 1, checking with higher
`--termination-depth` should now be feasible.
Compiler backends
-----------------
* The MAlonzo compiler backend now has support for compiling modules
that are not full programs (i.e. don't have a main function). The
goal is that you can write part of a program in Agda and the rest in
Haskell, and invoke the Agda functions from the Haskell code. The
following features were added for this reason:
- A new command-line option `--compile-no-main`: the command
```
agda --compile-no-main Test.agda
```
will compile `Test.agda` and all its dependencies to Haskell and
compile the resulting Haskell files with `--make`, but (unlike
`--compile`) not tell GHC to treat `Test.hs` as the main
module. This type of compilation can be invoked from Emacs by
customizing the `agda2-backend` variable to value `MAlonzoNoMain` and
then calling `C-c C-x C-c` as before.
- A new pragma `COMPILED_EXPORT` was added as part of the MAlonzo
FFI. If we have an Agda file containing the following:
```agda
module A.B where
test : SomeType
test = someImplementation
{-# COMPILED_EXPORT test someHaskellId #-}
```
then test will be compiled to a Haskell function called
`someHaskellId` in module `MAlonzo.Code.A.B` that can be invoked
from other Haskell code. Its type will be translated according to
the normal MAlonzo rules.
Tools
-----
### Emacs mode
* A new goal command `Helper Function Type` (`C-c C-h`) has been added.
If you write an application of an undefined function in a goal, the
`Helper Function Type` command will print the type that the function
needs to have in order for it to fit the goal. The type is also
added to the Emacs kill-ring and can be pasted into the buffer using
`C-y`.
The application must be of the form `f args` where `f` is the name of the
helper function you want to create. The arguments can use all the normal
features like named implicits or instance arguments.
Example:
Here's a start on a naive reverse on vectors:
```agda
reverse : ∀ {A n} → Vec A n → Vec A n
reverse [] = []
reverse (x ∷ xs) = {!snoc (reverse xs) x!}
```
Calling `C-c C-h` in the goal prints
```agda
snoc : ∀ {A} {n} → Vec A n → A → Vec A (suc n)
```
* A new command `Explain why a particular name is in scope` (`C-c
C-w`) has been added.
[Issue [#207](https://github.com/agda/agda/issues/207)]
This command can be called from a goal or from the top-level and will as the
name suggests explain why a particular name is in scope.
For each definition or module that the given name can refer to a trace is
printed of all open statements and module applications leading back to the
original definition of the name.
For example, given
```agda
module A (X : Set₁) where
data Foo : Set where
mkFoo : Foo
module B (Y : Set₁) where
open A Y public
module C = B Set
open C
```
Calling `C-c C-w` on `mkFoo` at the top-level prints
```
mkFoo is in scope as
* a constructor Issue207.C._.Foo.mkFoo brought into scope by
- the opening of C at Issue207.agda:13,6-7
- the application of B at Issue207.agda:11,12-13
- the application of A at Issue207.agda:9,8-9
- its definition at Issue207.agda:6,5-10
```
This command is useful if Agda complains about an ambiguous name and
you need to figure out how to hide the undesired interpretations.
* Improvements to the `make case` command (`C-c C-c`)
- One can now also split on hidden variables, using the name
(starting with `.`) with which they are printed. Use `C-c C-`, to
see all variables in context.
- Concerning the printing of generated clauses:
* Uses named implicit arguments to improve readability.
* Picks explicit occurrences over implicit ones when there is a
choice of binding site for a variable.
* Avoids binding variables in implicit positions by replacing dot
patterns that uses them by wildcards (`._`).
* Key bindings for lots of "mathematical" characters (examples: 𝐴𝑨𝒜𝓐𝔄)
have been added to the Agda input method. Example: type
`\MiA\MIA\McA\MCA\MfA` to get 𝐴𝑨𝒜𝓐𝔄.
Note: `\McB` does not exist in Unicode (as well as others in that style),
but the `\MC` (bold) alphabet is complete.
* Key bindings for "blackboard bold" B (𝔹) and 0-9 (𝟘-𝟡) have been
added to the Agda input method (`\bb` and `\b[0-9]`).
* Key bindings for controlling simplification/normalisation:
Commands like `Goal type and context` (`C-c C-,`) could previously
be invoked in two ways. By default the output was normalised, but if
a prefix argument was used (for instance via `C-u C-c C-,`), then no
explicit normalisation was performed. Now there are three options:
- By default (`C-c C-,`) the output is simplified.
- If `C-u` is used exactly once (`C-u C-c C-,`), then the result is
neither (explicitly) normalised nor simplified.
- If `C-u` is used twice (`C-u C-u C-c C-,`), then the result is
normalised.
### LaTeX-backend
* Two new color scheme options were added to `agda.sty`:
`\usepackage[bw]{agda}`, which highlights in black and white;
`\usepackage[conor]{agda}`, which highlights using Conor's colors.
The default (no options passed) is to use the standard colors.
* If `agda.sty` cannot be found by the LateX environment, it is now
copied into the LateX output directory (`latex` by default) instead
of the working directory. This means that the commands needed to
produce a PDF now is
```
agda --latex -i . <file>.lagda
cd latex
pdflatex <file>.tex
```
* The LaTeX-backend has been made more tool agnostic, in particular
XeLaTeX and LuaLaTeX should now work. Here is a small example
(`test/LaTeXAndHTML/succeed/UnicodeInput.lagda`):
```latex
\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{code}
data αβγδεζθικλμνξρστυφχψω : Set₁ where
postulate
→⇒⇛⇉⇄↦⇨↠⇀⇁ : Set
\end{code}
\[
∀X [ ∅ ∉ X ⇒ ∃f:X ⟶ ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
\]
\end{document}
```
Compiled as follows, it should produce a nice looking PDF (tested with
TeX Live 2012):
```
agda --latex <file>.lagda
cd latex
xelatex <file>.tex (or lualatex <file>.tex)
```
If symbols are missing or XeLaTeX/LuaLaTeX complains about the font
missing, try setting a different font using:
```latex
\setmathfont{<math-font>}
```
Use the `fc-list` tool to list available fonts.
* Add experimental support for hyperlinks to identifiers
If the `hyperref` LateX package is loaded before the Agda package
and the links option is passed to the Agda package, then the Agda
package provides a function called `\AgdaTarget`. Identifiers which
have been declared targets, by the user, will become clickable
hyperlinks in the rest of the document. Here is a small example
(`test/LaTeXAndHTML/succeed/Links.lagda`):
```latex
\documentclass{article}
\usepackage{hyperref}
\usepackage[links]{agda}
\begin{document}
\AgdaTarget{ℕ}
\AgdaTarget{zero}
\begin{code}
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
\end{code}
See next page for how to define \AgdaFunction{two} (doesn't turn into a
link because the target hasn't been defined yet). We could do it
manually though; \hyperlink{two}{\AgdaDatatype{two}}.
\newpage
\AgdaTarget{two}
\hypertarget{two}{}
\begin{code}
two : ℕ
two = suc (suc zero)
\end{code}
\AgdaInductiveConstructor{zero} is of type
\AgdaDatatype{ℕ}. \AgdaInductiveConstructor{suc} has not been defined to
be a target so it doesn't turn into a link.
\newpage
Now that the target for \AgdaFunction{two} has been defined the link
works automatically.
\begin{code}
data Bool : Set where
true false : Bool
\end{code}
The AgdaTarget command takes a list as input, enabling several
targets to be specified as follows:
\AgdaTarget{if, then, else, if\_then\_else\_}
\begin{code}
if_then_else_ : {A : Set} → Bool → A → A → A
if true then t else f = t
if false then t else f = f
\end{code}
\newpage
Mixfix identifier need their underscores escaped:
\AgdaFunction{if\_then\_else\_}.
\end{document}
```
The boarders around the links can be suppressed using hyperref's
hidelinks option:
```latex
\usepackage[hidelinks]{hyperref}
```
Note that the current approach to links does not keep track of scoping
or types, and hence overloaded names might create links which point to
the wrong place. Therefore it is recommended to not overload names
when using the links option at the moment, this might get fixed in the
future.