[Agda] a new compiler MAlonzo

[Makoto Takeyama]

Dear Ulf and Marcin,

I have uploaded a patch that adds a new compiler MAlonzo
(for Modified Alonzo) to Agda Wiki

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Patch.Submitted

Currently, it is tested with just one moderate size program that uses
the standard library fairly heavily.  (It appears to compile all of the
library to ghc-compilable haskell code, but of course it doesn't mean
much with all that unsafeCoerce.)

Only a part of primitive functions known to the type checker are
implemented, but adding more should be easy.

I have started this before I noticed the recent changes to Alonzo, and
it does not use the latest pragmas for compilers yet.

The compilatin scheme is much the same as Alonzo, but while trying to
compile the standard library I ended up rewriting the whole thing from
scratch.

Below is the minimal explanation in Agda2/examples/MAlonzo/README

Best Wishes,

Makoto


Usage

  agda --compile --malonzo --malonzoDir <DIR> <FILE>.agda

Compiles <FILE>.agda and hereditarily imported agda files to Haskell.
Haskell files are written under the directory <DIR>/MAlonzo.
If --manlonzoDir <DIR> is omitted, the current directory is used instead.

Agda module A.B.C translates to Haskell module MAlonzo.A.B.C
(to avoid conflicts between Agda and Haskell standard libraries.)

To compile the output Haskell files by ghc, do

  ghc -i<DIR> -main-is MAlonzo.<FILE> <DIR>/Malonzo/<FILE>.hs --make

You need to add something like lib/System/IO.agda below to
the library.   Then, main : IO () in <FILE>.agda translates to
main :: IO () in <FILE>.hs

A known problem: it tries to compile like ghc --make (skipping an
imported file if it already has an up-to-date haskell file), but
it occasionally fails during type checking (an agda problem).



module System.IO where

open import Data.Unit   using (竓、)
open import Data.String using (String)

postulate
  IO : Set -> Set

{-# BUILTIN IO	 IO #-}
{-# BUILTIN UNIT 竓、  #-}

primitive
  primPutStr	     : String -> IO 竓、
  primIOReturn	     : {a : Set} -> a -> IO a
  primIOBind	     : {a b : Set} -> IO a -> (a -> IO b) -> IO b







-- 
Makoto Takeyama <makoto.takeyama at aist.go.jp>
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052