[Agda] Epic compiler backend.

[Daniel Gustafsson]

Hello all,

A new backend for Agda to compile to Epic has been created. Epic is a language
used by Idris and Epigram made by Edwin Brady. Almost all of Agda should work
when using this backend, but it needs more testing.

It should be noted that this is very much EXPERIMENTAL code.

There is a new pragma for giving the Epic code for postulated definitions.
The Epic code given can then contain the definition itself, or use a foreign
call to call a C function. The pragma is {-# COMPILED_EPIC def code #-} and
works similar to the COMPILED pragma but instead of expecting Haskell code,
it expects Epic code. The code includes function arguments, return
type and the function body. Note that def is the name of an Agda definition,
which will be translated to a valid Epic name automatically.

The Epic backend supports Agda's primitive pragma for primitive functions that
are defined (with the same name) in the AgdaPrelude.e
(Agda/src/data/EpicInclude/) file.

Usage:
> agda --epic --includeC=<C-FILE> --compile-dir=<DIR> <FILE>.agda

A new directory, Epic, will be created in the compile-dir (default: the
project root), containing the file main.e with the Epic source code. The
compiler will also do a system call running the Epic compiler on that file.

The compilation requires a definition of main, which should be of type IO Unit.
Currently IO A actions are represented in Epic as functions from Unit to A.
Because of this the main function is applied a single unit.

Here follows how to define the IO monad:
  postulate
    IO : Set → Set
    return  : ∀ {A} → A → IO A
    _>>=_   : ∀ {A B} → IO A → (A → IO B) → IO B

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

ioreturn and iobind are Epic functions defined in AgdaPrelude.e which is
always included. This is how IO is defined in the standard library
(IO.Primitive). We only need to add the new COMPILED_EPIC pragmas.

The backend supports the {-# BUILTIN #-} pragma, which can be used e.g. to get
Natural numbers and their operations to be represented more efficiently as
BigInts and operations on them in Epic.

Currently, the backend will remove forced constructor arguments. Consider:

data Fin : Nat -> Set where
  fz : {n : Nat} -> Fin (suc n)
  fs : {n : Nat} -> Fin n -> Fin (suc n)

f : (n : Nat) -> Fin n -> Bool
f .(suc zero)    (fz {zero})    = true
f .(suc (suc n)) (fs {suc n} i) = false

here we don't need to store the Nat in the constructors since we can always
rewrite the pattern matching on them. Note that we currently DO NOT do this
and therefore functions like f above will give a runtime error. This can be
disabled by using the flag --no-forcing.

All types that looks like Nats after forced constructor arguments have been
removed - i.e. if they have two constructors: one with no arguments and one
with a single recursive argument - will be represented as BigInts. This applies
to the standard Fin type as defined above.

Compilation using Epic requires a few libraries. Particularly gcc, the Boehm
garbage collector and the GNU MP library. For more information, check out
Epic's homepage: http://www.cs.st-andrews.ac.uk/~eb/epic.php

Some differences compared to MAlonzo:
  - Does not have support for calling Haskell functions.
  - Recompiles all modules during compilation.
  + Types that are like Natural numbers will always be represented as BigInts:
    No conversion between BigInt and Constructor representation.
  + Epic has no fancy type system that we need to convince (no coercions).

Daniel Gustafsson
Olle  Fredriksson