Best of two worlds.

[thesz]

Unit testing Agda code with elisp.

Awesome. ;)

Comments

[pozorvlak]

Actually, there are three languages involved: the original agda-mode works as follows:

1. Emacs-lisp code constructs Haskell code which calls Agda-interpretation functions with the relevant Agda code passed as a string argument.
2. A slave GHCi process interprets the Haskell code, which in turn interprets the Agda code, and generates elisp code to insert the output into an Emacs buffer.
3. The calling elisp function evals the generated elisp code.

I can't imagine why they implemented it this way. I carefully didn't touch the Haskell-generating functions, but I did have to spend a lot of time in the GHCi interaction window to work out what arguments I needed to pass.

[nealar]

1. Elisp takes Agda from edit buffer, generates Haskell
2. passes this Haskell (with Agda as argument) to GHCi (with loaded Agda interpreter), getting more Elisp as result of interpretation
3. passes this Elisp back to Emacs where it is interpreted,
right?

Either you or Norrel seem to be kidding, making fun of poor me.

Is there such thing as a multiquine contest?

[pozorvlak]

That's exactly right, and I swear that's how it works. Have a look at the functions agda2-go and agda2-exec-responses in agda2-mode.el.

I don't think there's a multiquine contest, but Googling turns up a handful of polyglot quines: this Haskell/OCaml/Scheme one, a C/Ruby/Python/Perl/BF one, and a few more here.

[nealar]

Название ссылки разорвало моск. Боюсь по ней переходить.

[thesz]

Take a look what author wrote near. There's more than elisp out there. ;)