Conversation
The name binding structure that results from multi-parameter functions with repeated names, and the interaction with pattern desugaring is currently very counterintuitive. See issue #567 for more discussion.
Multi-argument functions are now desuguared into nested lambdas in the `NoPat` phase instead of during typechecking. This gives more sensible results when the same variable is shadowed in the argument list. In particular, extra "where" bindings that are added for pattern desugaring now have a scope that is outside patterns and variables occuring further to the right. Some programs that used to produce "overlapping symbols" errors are now accepted with a shadowing warning instead. The main downside of this refactoring is that the `checkFun` operation no longer has access to function name or argument numbers for definitions, as all functions have become single-argument lambdas by typechecking time. This can be fixed by recording this information in the AST during the NoPat desugaring instead.
This allows us to attach information to `EFun` nodes that describe which named function the lambda belongs to, and which arguments it handles. This information is filled in by the `NoPat` pass as it desugars multi-argument functions into a sequence of lambdas and is used during typechecking to produce error messages. There is an odd potential for the renamer to get things wrong here. If a named function has an argument that shadows it's own name, the renamer may incorrectly resolve the name in a function description for later arguments. The resulting error message will then point to the wrong name (although it will be in the vicinity...). It's hard to fix this without folding the NoPat pass into the renamer (which we should also do, but it's a nontrivial refactoring).
Reordering the where declarations in pattern desugaring caused some minor changes in error message output, as well as changes in the specializer.
brianhuffman
left a comment
brianhuffman
left a comment
There was a problem hiding this comment.
This looks reasonable to me.
yav
left a comment
yav
left a comment
There was a problem hiding this comment.
I am not sure this is the right thing to do here, these are my thoughts:
- I think there might be value in preserving the arity of functions, especially as we look more into generating code
- it seems to me that
\x x -> eshould be an error, rather than a warning, just like\(x,x) -> eis an error - if you do think that's the right thing to do though, it looks like
Bindnow never has any parameters afterNoPatso we should probably remove implementations for that from the following passes - I have a whole lot of changes to the renamer on my modules branch, and am about to start working on the type checker this week, so there's lot's of potential for merge conflicts, so we may want to hold off on simplifying the following passes for now
|
Well, the typechecker reduces the arity of all functions to 1 already, so I don't think we're losing anything here. As to the error situations: I'm open to the idea that these should be errors instead, but I couldn't figure out a good way to do that without doing a much larger refactoring that merges the NoPat pass directly into the Renamer. I think that's a good idea, eventually, but I don't understand all the working pieces well enough to know how difficult that would be. As to simplifying |
|
I agree that duplicate variables like |
|
I am fine with merging it, as it is fairly localized change. However, we should probably do some sort of larger refactoring too---I've cleaned up a bunch of stuff in the renamer on the |
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
The following included cryptol PRs required changes to saw-script: - GaloisInc/cryptol#1077 "nopat-refactor" - GaloisInc/cryptol#1075 "persist-solver"
3 participants
Refactor NoPat to fix #567