Various fixes #2
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The `HOLE` rule is now only a part of path expressions. Removing the duplicate rule resolves a ton of reduce-reduce conflicts in the grammar.
...so that they can be pattern matched.
When determining whether a type contains a variable any undetermined inferred type may end up containing the variable.
The original code simply used a wrong variable in place of the field name.
See rule EUNWRAP in fig 9 in section 5.1 of JFP (draft) paper and rule EIF in fig 8 in section 4.2 of JFP (draft) paper.
Previously `annotP` only equated the types in the case when there was a sequence
of bindings produced by the nested patterns. This meant that inconsistent
patterns would type check. For example, before this PR, the REPL interaction
1ML> ({}: int) = 1;
1ML> ((x: int): text) = "1";
x : text
would not give errors. After this PR, the same interaction
1ML> ({}: int) = 1;
stdin:1.2-1.9: inconsistent types equated by `as': () vs int
1ML> ((x: int): text) = "1";
stdin:1.6-1.16: inconsistent types equated by `as': int vs text
gives reasonable errors.
Especially in the case of Set and Map abstractions that are supposed to use given ordering.
|
Wow, thanks! I'm on vacation right now, so only skimmed through so far. Some changes obviously make sense, some I'll need to think about (and swap in all the background first). So, yeah, it might help to split this up a little, e.g., one PR with all the obvious fixes, and then separately the others. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Here are some fixes I've accumulated while toying with 1ML.
See the individual commits for some details. One of the commits adds Travis CI integration (i.e. it is not a fix).
Sorry, @rossberg, for dumping these all at once. I can spend some time reworking this PR if you like.