Merged
Conversation
Contributor
Author
|
Same old question/todo: Questions for reviewers: I'm not sure what conventional commit prefixes to use on a bunch of these, also I haven't worried about what changes are breaking -- for a dumb openapi frontend they should all be fine, but may break "smarter" clients, (and as with #958 something may well break the DB. I need to think about this). |
brprice
commented
Apr 24, 2023
This was referenced Apr 24, 2023
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
e905688 to
ab4a10f
Compare
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
4c2a561 to
d26c774
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
ab4a10f to
da76901
Compare
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
3 times, most recently
from
e49183d to
edcec45
Compare
Contributor
I have tended to use Anyway, I think we agreed with @dhess recently that it's not worth worrying too much about CC prefixes on individual commits, with PR titles being more important (I had been doing the opposite, and not using prefixes on PR titles, but I will from now on). |
georgefst
approved these changes
May 9, 2023
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
3 times, most recently
from
1d1ebdb to
981252c
Compare
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
edcec45 to
a6e9d65
Compare
This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors. (Both versions of the testsuite currently pass, but when constructors are checkable the old version would fail.)
This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors. (Both versions of the testsuite currently pass, but when constructors are checkable the old version would fail.)
…only This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors. (Both versions of the testsuite currently pass, but when constructors are checkable the old version would fail.)
This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors. (Both versions of the testsuite currently pass, but when constructors are checkable the old version would fail.)
This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors.
This ensures that they are consistent with constructors being checkable only. This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors.
…or/literal This is a step towards only generating terms which are consistent with treating constructors as checkable. That in itself is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors. Note that literals will be synthesisable, but constructors will only be checkable. This commit slightly generalises what terms we generate, since we can now generate primcons for non-hole types.
…e only This is a step towards being able to change the typechecker to treat constructors as checkable, rather than synthesisable. This would then enable us to drop indices from constructors.
Add some tests which will show the difference in smartholes behaviour once constructors are considered checkable. Currently they are synthesisable, so smartholes puts a constructor directly inside a hole.
Add some tests which will show the difference in action behaviour once constructors are considered checkable. Currently they are synthesisable, so they (via smartholes) put constructors directly inside holes.
This has a knock-on effect on ConstructRefinedCon: if there is no valid refinement (and we thus fall back to inserting a saturated constructor in a hole), we need to put an annotation on the constructor which is inside a hole. BREAKING CHANGE: this will reject some programs that previous versions of primer would consider valid. Thus it may break loading a database that was generated by a older version of primer.
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
a6e9d65 to
f00e897
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
981252c to
251c13d
Compare
brprice
changed the title
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
This PR changes the typechecking treatment of constructors to be checkable (rather than synthesisable).