[Agda-dev] On the internal representation of clauses

[Jesper Cockx]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150707/73f4bfe2/attachment.html