Hello Andreas,<div><br></div><div>It looks like you are missing the Boehm garbage collector (<a href="http://www.hpl.hp.com/personal/Hans_Boehm/gc/">http://www.hpl.hp.com/personal/Hans_Boehm/gc/</a>) and the GNU MP library (<meta http-equiv="content-type" content="text/html; charset=utf-8"><a href="http://gmplib.org/">http://gmplib.org/</a>), see <meta http-equiv="content-type" content="text/html; charset=utf-8"><a href="http://www.cs.st-andrews.ac.uk/~eb/epic.php">http://www.cs.st-andrews.ac.uk/~eb/epic.php</a>. 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).</div>
<div><br></div><div>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?</div><div><br></div><div>Regards,</div><div>Olle<br>
<br><div class="gmail_quote">On 14 December 2010 21:59, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi Daniel and Olle,<br>
<br>
this is great, thanks!<br>
<br>
Can you help me install epic such that I can continue to compile Agda?<br>
<br>
cabal install epic<br>
...<br>
Linking dist/build/epic/epic ...<br>
gcc -Wall -O3 -DUSE_BOEHM -c -o closure.o closure.c<br>
In file included from closure.h:4,<br>
from closure.c:1:<br>
gc_header.h:10:19: error: gc/gc.h: No such file or directory<br>
In file included from closure.c:1:<br>
closure.h:7:17: error: gmp.h: No such file or directory<br>
In file included from closure.c:1:<br>
closure.h:261: error: syntax error before ‘*’ token<br>
...<br>
<br>
I am using Mac OS X 10.5 and macports.<br>
<br>
Cheers,<br>
Andreas<br>
<br>
On 12/14/10 9:28 PM, Daniel Gustafsson wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello all,<br>
<br>
A new backend for Agda to compile to Epic has been created. Epic is a language<br>
used by Idris and Epigram made by Edwin Brady. Almost all of Agda should work<br>
when using this backend, but it needs more testing.<br>
<br>
It should be noted that this is very much EXPERIMENTAL code.<br>
<br>
There is a new pragma for giving the Epic code for postulated definitions.<br>
The Epic code given can then contain the definition itself, or use a foreign<br>
call to call a C function. The pragma is {-# COMPILED_EPIC def code #-} and<br>
works similar to the COMPILED pragma but instead of expecting Haskell code,<br>
it expects Epic code. The code includes function arguments, return<br>
type and the function body. Note that def is the name of an Agda definition,<br>
which will be translated to a valid Epic name automatically.<br>
<br>
The Epic backend supports Agda's primitive pragma for primitive functions that<br>
are defined (with the same name) in the AgdaPrelude.e<br>
(Agda/src/data/EpicInclude/) file.<br>
<br>
Usage:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
agda --epic --includeC=<C-FILE> --compile-dir=<DIR> <FILE>.agda<br>
</blockquote>
<br>
A new directory, Epic, will be created in the compile-dir (default: the<br>
project root), containing the file main.e with the Epic source code. The<br>
compiler will also do a system call running the Epic compiler on that file.<br>
<br>
The compilation requires a definition of main, which should be of type IO Unit.<br>
Currently IO A actions are represented in Epic as functions from Unit to A.<br>
Because of this the main function is applied a single unit.<br>
<br>
Here follows how to define the IO monad:<br>
postulate<br>
IO : Set → Set<br>
return : ∀ {A} → A → IO A<br>
_>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B<br>
<br>
{-# COMPILED_EPIC return (u1 : Unit, a : Any) -> Any = ioreturn(a) #-}<br>
{-# COMPILED_EPIC _>>=_ (u1 : Unit, u2 : Unit, x : Any, f : Any) -><br>
Any = iobind(x,f) #-}<br>
<br>
ioreturn and iobind are Epic functions defined in AgdaPrelude.e which is<br>
always included. This is how IO is defined in the standard library<br>
(IO.Primitive). We only need to add the new COMPILED_EPIC pragmas.<br>
<br>
The backend supports the {-# BUILTIN #-} pragma, which can be used e.g. to get<br>
Natural numbers and their operations to be represented more efficiently as<br>
BigInts and operations on them in Epic.<br>
<br>
Currently, the backend will remove forced constructor arguments. Consider:<br>
<br>
data Fin : Nat -> Set where<br>
fz : {n : Nat} -> Fin (suc n)<br>
fs : {n : Nat} -> Fin n -> Fin (suc n)<br>
<br>
f : (n : Nat) -> Fin n -> Bool<br>
f .(suc zero) (fz {zero}) = true<br>
f .(suc (suc n)) (fs {suc n} i) = false<br>
<br>
here we don't need to store the Nat in the constructors since we can always<br>
rewrite the pattern matching on them. Note that we currently DO NOT do this<br>
and therefore functions like f above will give a runtime error. This can be<br>
disabled by using the flag --no-forcing.<br>
<br>
All types that looks like Nats after forced constructor arguments have been<br>
removed - i.e. if they have two constructors: one with no arguments and one<br>
with a single recursive argument - will be represented as BigInts. This applies<br>
to the standard Fin type as defined above.<br>
<br>
Compilation using Epic requires a few libraries. Particularly gcc, the Boehm<br>
garbage collector and the GNU MP library. For more information, check out<br>
Epic's homepage: <a href="http://www.cs.st-andrews.ac.uk/~eb/epic.php" target="_blank">http://www.cs.st-andrews.ac.uk/~eb/epic.php</a><br>
<br>
Some differences compared to MAlonzo:<br>
- Does not have support for calling Haskell functions.<br>
- Recompiles all modules during compilation.<br>
+ Types that are like Natural numbers will always be represented as BigInts:<br>
No conversion between BigInt and Constructor representation.<br>
+ Epic has no fancy type system that we need to convince (no coercions).<br>
<br>
Daniel Gustafsson<br>
Olle Fredriksson<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br><font color="#888888">
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></blockquote></div><br></div>