[Agda] Epic compiler backend.

[Edwin Brady]

Hi Andreas,
This suggests you don't have the Boehm garbage collector or the GMP  
libraries installed. The packages in macports are "boehmgc" and "gmp".

Another macports annoyance is the need to set your library paths. I  
used to have...

export C_INCLUDE_PATH=/opt/local/include:$C_INCLUDE_PATH
export CPLUS_INCLUDE_PATH=/opt/local/include:$CPLUS_INCLUDE_PATH
export LD_LIBRARY_PATH=/opt/local/lib:$LD_LIBRARY_PATH
export LIBRARY_PATH=/opt/local/lib:$LIBRARY_PATH

...but I now solve the problem by not using macports if I can avoid it!

Anyway, it's nice to see this new backend, thanks Daniel and Olle! I  
look forward to hearing how well it works.

Edwin.

On 14 Dec 2010, at 20:59, Andreas Abel 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

-- 

Edwin Brady - http://www.cs.st-and.ac.uk/~eb/
The University of St Andrews is a charity registered in Scotland : No  
SC013532