Merged
Conversation
brprice
commented
Apr 24, 2023
Contributor
Author
|
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
brprice
commented
Apr 24, 2023
This was referenced Apr 24, 2023
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
b2e0e8b to
2b378a1
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
3 times, most recently
from
da76901 to
6c62177
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
741c42e to
23ae8b9
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
6c62177 to
2bb45b0
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
23ae8b9 to
0dee414
Compare
georgefst
approved these changes
Apr 27, 2023
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
3 times, most recently
from
7881060 to
bd72d81
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
2bb45b0 to
26d0e08
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
bd72d81 to
c135de0
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
26d0e08 to
1d1ebdb
Compare
This is a step towards all constructors being (fully) saturated, at which point we can update the typechecker to enforce that invariant. (Both versions of the testsuite currently pass, but when non-saturated constructors are rejected the old version would fail.)
This is preperation for removal of the `ConstructCon` action, which will make no sense once the typechecker enforces all constructors to be fully saturated.
Prior to this commit, "Insert a saturated constructor" did not offer nullary constructors. Nullary constructors were offered only by "Insert a constructor". With this commit, "Insert a saturated constructor" now always offers nullary constructors, and in beginner mode only offers nullary constructors. This change is with a view to merging "Insert a saturated constructor" and "Insert a constructor" actions. This commit changes the data we emit via the OpenAPI endpoints. However, it obeys the same schema (and consumers are expected to not care about the exact data we emit), and is thus not a breaking change. Note that it does not affect the actions stored in undo logs, and thus will not break programs loaded from older databases that were created with older versions of primer.
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
c135de0 to
51b93b8
Compare
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
1d1ebdb to
981252c
Compare
brprice
changed the title
We leave ConstructSaturatedCon, ConstructRefinedCon and MakeConSat which create saturated constructors. Note that they behave the same for nullary constructors, and inserting a non-applied constructor (which has arguments) will not make sense when all constructors must be saturated. This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. BREAKING CHANGE: this removes an action that may be stored in the undo log of a program from a database created with an older version of primer. This will break loading old databases.
This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant.
This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant.
This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant.
This is the last step towards all constructors being saturated. We can now update the typechecker to enforce that invariant. BREAKING CHANGE: this changes the interpretation of an action that may be stored in program's undo logs. This may break the undo action of programs loaded from a database which was created by an earlier version of primer.
Some tests also need updating: - We also remove a couple of tests that need unsaturated constructors (i.e. partially applied constructors). - A couple of fragile name also needed updating. - A tests checking acceptance of under-saturated constructors now checks they are rejected (at hole types). Added a test an unsaturated constructor is rejected (at a concrete type). BREAKING CHANGE: this will reject some programs that were previously accepted. This will break loading databases created by older versions of primer.
Also remove dead code `foldApp` and `unfoldAPP`.
…ated In the handlers for `SetConFieldType` and `AddConField` we can now use `transformM` instead of manually doing the recursion. This change was enabled by the previous commit, which removed the handling of non-saturated constructors. Prior to that we had to recurse top-down, since for an unsaturated term such as `C x xs` (which would be represented as `App (App (Con "C" [] []) (Var "x")) (Var "xs")) we need to act on the outer `App` node and then recurse into the arguments (here, `x` and `xs`). Note that we must not act on the "inner" `App` node, since we would then believe that the constructor is only applied to one argument. Thus `transformM` is inappropriate as it is a bottom-up traversal, and we must hand-roll the traversal with `descendM`. Since we now know that all constructors are saturated, we know that the above situation is imposible, and the representation must in fact be `Con "C" [] [Var "x", Var "xs"]`. This sidesteps all the issues, enabling us to use the standard bottom-up traversal `transformM`.
brprice
force-pushed
the
brprice/saturated-constructors-3
branch
from
981252c to
251c13d
Compare
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
3 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 enforces all constructors to be fully saturated. Now this is the case it would be possible for constructors to not store their indices (i.e. not have type applications) -- this will be done in a subsequent PR.