Usage
agda --compile --compile-dir <DIR> --ghc-flag "<GHC FLAGS>" <FILE>.agda
Compiles <FILE>.agda and hereditarily imported agda files to Haskell and to an executable.
Haskell files are written under the directory <DIR>/MAlonzo. If --compile-dir <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.)
Those Haskell files are then automatically compiled to object files and an executable by the command
ghc <GHC FLAGS> -i<DIR> -main-is MAlonzo.<FILE> <DIR>/Malonzo/<FILE>.hs --make
It is assumed that <FILE>.agda contains a definition of main :: IO a. If it does not, ghc finishes with an error, but never mind. The executable is <DIR>/MAlonzo/<FILE>(.exe), or whatever you specify via <GHC FLAGS>.
You can use IO from the standard library if you want to do some input/output.