What is Agate
Agate is a translator that converts an
Agda program into a Haskell program. The generated program can be
with GHC (Glasgow Haskell Compiler) into executable code and then
executed. Agate provides a
mechanism to access some built-in features of Haskell such as I/O using
the 'native' or 'postulate' syntax of Agda. Future
releases of Agate will feature optimization based on type information
in the program, although it is not available in this release.
You need Glasgow
version 6.4.x to build and use
Note that the version 6.6 cannot
build Agate and cannot be used as back-end of Agate currently.
need aclocal (automake) and autoconf to build Agate.
the source tarball of the latest version
How to Build
% aclocal-I macros
% ./configure --enable-newsyntax
How to Install
% make install
How to Use
% agate [options] file.agda ...
% ghc [ghc-options...] a.hs
show this help
--library-path DIR, -L DIR set library path
specify output file