Better freshing/renaming?
Closed this issue · 5 comments
Right now freshing is often followed by renaming in a single rule. Take the function type as an example, to prove that two function types are the same, two freshings are done and then two renamings are done to use the new symbol instead. I wonder if this contributes to slowness, and if there's a way to merge these two steps to reduce abt rebuilds.
It should be possible to optimize this; ultimately, even doing these things once is going to be unbearably slow, but I guess there's no reason for us to do it twice unnecessarily 😄
Another thing to consider is the view: this is probably fairly expensive... It was quite important at a time when the syntax was changing very rapidly, but things seem to have calmed down a bit. I wonder if we should experiment with using the ABTs directly in places that are called a lot?
I'm really not sure, though. The ABT interface is already really slow, and it's hard for me to tell in advance of doing a bunch of tuning whether these marginal improvements are worth it.
Are we postponing this to RedPRL 2 then? I think the API would be something which takes a list of variable for refreshing.
The renaming stuff is easy enough that it can be done right away (as soon as anyone has time)
Actually, it might be helpful if...
- The view uses
absinsteadabt. The avoids refreshing. - There are two APIs: substitution for
abs(already there) and unsafe operator to open up an abstraction without any renaming.
This way we can avoid unnecessary refreshing.