[Agda] Epic compiler backend.

[Olle Fredriksson]

Hello Andreas,

It looks like you are missing the Boehm garbage collector (
http://www.hpl.hp.com/personal/Hans_Boehm/gc/) and the GNU MP library (
http://gmplib.org/), see http://www.cs.st-andrews.ac.uk/~eb/epic.php. There
should be packages for these libraries available at least for Mac OS X 10.4,
according to the Epic page (but neither of us has a Mac, so we have not been
able to try it for ourselves).

If this is an issue for others, maybe we should consider hiding the Epic
backend and its dependencies under a specific Cabal flag. What do you think?

Regards,
Olle

On 14 December 2010 21:59, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101214/674003a8/attachment-0001.html