[Agda] Epic compiler backend.

[Andreas Abel]

Hi Daniel and Olle,

this is great, thanks!

Can you help me install epic such that I can continue to compile Agda?

cabal install epic
...
Linking dist/build/epic/epic ...
gcc -Wall -O3 -DUSE_BOEHM   -c -o closure.o closure.c
In file included from closure.h:4,
                  from closure.c:1:
gc_header.h:10:19: error: gc/gc.h: No such file or directory
In file included from closure.c:1:
closure.h:7:17: error: gmp.h: No such file or directory
In file included from closure.c:1:
closure.h:261: error: syntax error before ‘*’ token
...

I am using Mac OS X 10.5 and macports.

Cheers,
Andreas

On 12/14/10 9:28 PM, Daniel Gustafsson wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/