Create a meaningful function definition using existing elaborator constructs

[tdidriksen]

The first step to elaborated copatterns is obtaining the power to create auxiliarty functions with the elaborator. Discuss!

[david-christiansen]

I'm not sure what you mean by this - both the Haskell elaborator and my recently-added reflection of it can create auxiliary definitions. The Haskell elaborator does this while elaborating case blocks, among other things, while you can see e.g. https://github.com/david-christiansen/derive-all-the-instances/blob/master/src/Derive/Disjoint.idr for a reflected elaborator that derives non-overlappingness lemmas.

[tdidriksen]

Agreed, the question is not whether auxiliary functions can be created. However, we (or I, at least) need to figure out the best approach to creating auxiliary functions using the elaborator. Specifically, given a definition with both nested copatterns and standard pattern matching, an auxiliary function should be created for each level of copatterns. Also, any argument on which non-trivial pattern matching is performed requires its own auxiliary function. The reflected elaborator looks like a good venue for experimentation!

[david-christiansen]

Hopefully it makes experimentation easier, anyway - it sure beats recompiling Idris when working on a slower machine! One day I'd like to make an elaborator for Idris using the reflected elaborator that can do at least a big subset of the high-level language. That would make experimenting with new features much easier.