Agda Translation Efficiency improvements

[ramsay-t]

Change the order of the translation? decision procedure to try simple AST matching before it tries the translation relation. This makes the code more repetitive but it should be quicker.

This also adopts an idea from Ulf Norell that collapses the enormous number of lines needed in previous versions for all the non-matching AST patterns.

[effectfully]

It's probably more efficient indeed, but it's still way more guesswork than required for at least some of the transformations. But this way you are also going against what the actual optimizations do as they normally look at the outermost constructor first and I suppose it's possible that some of them may product the same constructor as a result (I don't have any concrete examples, sorry). Which isn't a correctness issue, just more legwork for the certifier to do.

Have we already tried running the certifier on some real word programs? We don't need to do it for all optimization passes simultaneously, doing just for some individually would already be interesting.

[ramsay-t]

But this way you are also going against what the actual optimizations do

I'm not sure I understand? This function runs on the entire ASTs of the before- and after- programs. I don't think any of the optimisations operate on the (program 1.1.0 part of the AST... Most of the optimisations leave the majority of the AST alone, only modifying some small parts. The way this function used to work was to try and match the translation relation at every node in the trees; the way it works now is to try assuming that, if nodes of the two trees are the same, then we probably didn't change anything here. Only where that doesn't work does it then try the translation relation that we have supplied. In some cases the translation relation doesn't change the top level bit of matching syntax, but I think most of them are only one or two steps below, so this function will backtrack up the tree but I doubt it will do so very much.

As you say: we should try it as see.

[effectfully]

The way this function used to work was to try and match the translation relation at every node in the trees

Yes , but if you're squint enough, that's kinda what the optimizations do. They don't just skip the entirety of the AST and then go bottom-up applying the rules, they do it top-down instead. Let's say we have an "optimization" that reorders lambdas and applications turning

(\x1 x2 ... xn -> body) a1 a2 ... an

into

(\xn ... x2 x1 -> body) an ... a2 a1

Since the certification has De Bruijn indices, x_i isn't distinguishable from x_j at the binding site but they are distinct at the call site, and so you can't spot early that the x has changed, meaning not only will you now end up skipping all the applications hoping there was no transformation there, you'll also process a potentially large part of body multiple times, because the applications will turn out to be unskippable.

There's no general solution to this, hence why I've been saying that certification for every optimization needs to be defined with efficiency concerns in mind. And if we do try to make the certifier efficient, then I think this PR makes things worse, not better, because previously you had control over how things evaluate and now you're forced to always optimistically skip matching constructors first.

But yes:

As you say: we should try it as see.