[Agda-dev] On the internal representation of clauses

[Ulf Norell]

It's probably a good idea, the permutation is indeed horrible to work with,
but getting the refactoring right might take some effort.

/ Ulf

On Tue, Jul 7, 2015 at 8:26 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> Hi all,
>
> I'm currently working on a new implementation of the unifier used by Agda
> for pattern matching. While adapting the LHS checker to my new
> implementation, I noticed a peculiarity in Agda's internal representation
> of function clauses that makes my implementation quite a bit harder than I
> think is necessary.
>
> Currently, the internal syntax for clauses contains a permutation that
> tells in which order the pattern variables should be bound. However, this
> order is not respected by the right-hand side of the clause; instead it
> binds the pattern variables left-to-right. It also reserves de
> Bruijn-indices for dot patterns, even though these indices should never be
> used and really don't make much sense.
>
> In my opinion, it would be much clearer to get rid of the permutation
> altogether and just have each pattern variable store the de Bruijn index
> that it binds (relative to the clause telescope). Agda already has a
> datatype for this (Syntax.Internal.DeBruijnPattern), it's just not used
> very much at the moment. Using the DeBruijnPattern type instead of the
> regular Pattern would simplify a lot of code that currently has to
> reconstruct these indices (you'd be surprised how many times the code for
> this reconstruction is repeated in the Agda codebase).
>
> However, this would require a quite (really) big refactoring throughout
> the whole of Agda's codebase, and there's a few pieces that I'm not sure of
> how to handle
> - The compilers currently ignore the permutation and just use the
> left-to-right ordering of pattern variables, and reserve indices for dot
> patterns.
> - The reflection mechanism also ignores the permutation, and reserves
> indices for dot patterns as well.
> - The termination checker does inlining of with clauses, which manipulates
> the clause's permutation, and I'm not sure what's going on there.
> - Probably other things I haven't noticed yet.
>
> All in all, I think this refactoring would make the internal syntax of
> function definitions significantly more understandable and easier to
> handle. What are your opinions on this issue?
>
> cheers,
> Jesper
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150707/9b8db918/attachment.html