[ #155 ] Add COMPILE ... to pragmas for data types and functions

[jespercockx]

This is a first attempt at implementing a COMPILE ... to pragma for compiling a datatype or function to an existing Haskell definition, as described in #155. Currently there are the following limitations:

• It makes use of an IORef to keep track of the mapping between names, which hopefully should not be a problem.
• When checking a COMPILE ... to pragma, despite generating no code it still compiles both the definition in the pragma and the target definition, which is a bit wasteful. It would perhaps be more efficient to store the compiled definitions in another IORef so we don't need to recompile them later (there are other places in the agda2hs codebase where this would be useful too).
• Type classes, type aliases, and anything that's not a regular datatype or a function with a normal COMPILE pragma is not yet supported.
• I only did minimal testing so far.

I'll probably add some more tests (including failing ones) later and perhaps add support for type aliases too, but I'm already curious to see what people think about this.

[jespercockx]

@J0s3c4rl0s perhaps you would be interested to give this a try for some of the examples from your thesis.

[jespercockx]

And maybe @anuyts is interested too since he commented on #155 recently.

[J0s3c4rl0s]

Yes this sounds interesting, I could use some of the agda examples in src/AgdaRunIdExamples.agda from my runtime_id_fn repo I used for my thesis to test the feature.

[omelkonian]

Looks good! Although the new feature is incomplete (cover type aliases/classes, etc.), there's no harm in merging this partial solution as it already seems very useful.

[jespercockx]

Looks good! Although the new feature is incomplete (cover type aliases/classes, etc.), there's no harm in merging this partial solution as it already seems very useful.

Thank you for the review. I agree that this could use more testing, but since we're not close to a release I'll just merge this so it's easier for others to test out too.