[Agda] Example Runnable Agda Programs

[Aaron Stump]

Hello, Philipp.  I have written an executable program in Agda called 
fore.  It is a type checker and translator for System F plus global 
positive-recursive type definitions.  I am using this for research on 
typed lambda encodings (Church, Parigot, a new one of ours).  It parses 
input -- using a parser produced by our gratr parser-generator, which 
targets OCaml and Agda -- then type checks it, and translates it to 
Racket and Haskell.  You can find the code, and examples, here:

http://www.cs.uiowa.edu/~astump/software/fore.zip

It's about 2kloc of Agda.  Let me know if you have any questions about 
this example.

It is great if you will improve the Agda compiler!

Best wishes,
Aaron

On 12/12/2014 08:47 AM, Philipp Hausmann wrote:
> Hi,
>
> I am looking for example programs to test the Agda compilers. Just by
> searching github, google & co I couldn't find many Agda programs which
> can actually be run and do something interesting.
>
> To give a bit of context, we are working on a new backend for Agda and
> would like to have some regression tests. We have some simple
> HelloWorld-style programs. but we are missing some more complicated
> examples. Currently we are porting the Eliza [1] example from GHC's
> nofib testsuite, but adding already existing Agda programs would be much
> less work....  Especially interesting would also be examples where the
> current MAlonzo backend fails or produces bad code. I remember seeing
> some emails about them on the mailing list [2, 3, 4], but I don't
> remember seeing any actual code example for reproducing these errors.
>
> As the behaviour of Agda programs should not really depend on the
> backend, I think the test programs would be useful for the MAlonzo
> backend as well.
>
> Long story short, does anyone have actual runnable Agda programs we
> could use for testing?
>
> Cheers,
> Philipp
>
> [1]
> https://github.com/phile314/agda/blob/compiler-tests/test/exec/with-stdlib/Eliza.agda
> [2] https://lists.chalmers.se/pipermail/agda/2012/004423.html
> [3] https://lists.chalmers.se/pipermail/agda/2013/005229.html
> [4] https://lists.chalmers.se/pipermail/agda/2014/006990.html
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda