Unification modulo overloaded constructors proposal #882
Conversation
traiansf
changed the title
| other constructors, as overloaded constructors are injective | ||
| - overloaded constructor vs. different (overloaded) constructor: unification | ||
| fails, similarly to the other constructors | ||
| - overloaded constructor vs. injection: |
There was a problem hiding this comment.
We can also short-circuit this step by looking at the klabel attribute: If the overload-ed constructor and the inj's child do not have the same klabel, then there is no reason to even attempt an overload axiom.
| This is K's way to deal with overloading. An additional restriction imposed by | ||
| K implementations is that of __SingleOverloadPerSort__: | ||
|
|
||
| > Given sort `s` and label `l` there exists at most one production of result |
There was a problem hiding this comment.
This additional restriction should be checked and an error or at least a warning should be generated if the semantics violates it.
There was a problem hiding this comment.
I added a TODO for that; I'm thinking this should be done in the frontend though (as the frontend generates the overloading axioms).
There was a problem hiding this comment.
I think it would be a good idea to check in the backend, also.
| oveloaded operation is that with an injection operation as given by the | ||
| overloading axioms. | ||
|
|
||
| Hence, the proposed solution for handling problem (1) specified above is to |
There was a problem hiding this comment.
This will break the "additivity" of attributes because constructor doesn't mean the symbol is indeed a constructor. Therefore, all backends, even those designed to handle only constructors without overloading, need to read all attributes to tell if a symbol is a constructor. I think it is better to use a different attribute keyword, say overloaded-constructor.
There was a problem hiding this comment.
Based on your comments (and the way it's implemented in the llvm-backend) I've proposed a different mechanism which collects overloaded information from the attributes associated to overloading axioms
| This is K's way to deal with overloading. An additional restriction imposed by | ||
| K implementations is that of __SingleOverloadPerSort__: | ||
|
|
||
| > Given sort `s` and label `l` there exists at most one production of result |
There was a problem hiding this comment.
I think it would be a good idea to check in the backend, also.
| ``` | ||
|
|
||
| The rule above requires that the second argument of the application expression | ||
| (which should be a list of expressions, is actually a list of values). |
There was a problem hiding this comment.
This parenthesis seems wrong. The open parenthesis should probably be a comma, the closing one should probably be removed.
…l proposal
Reviewer checklist
stack test --coveragestack haddockstylish-haskell