Merged
Conversation
Contributor
Author
|
Notes for reviewers: I'd advise reviewing commit-by-commit, or at least looking at the big rename commit separately. 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
brprice
commented
Apr 24, 2023
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
63dbea1 to
c7abd43
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
b2e0e8b to
2b378a1
Compare
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
c7abd43 to
c3f9ccb
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
2b378a1 to
741c42e
Compare
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
c3f9ccb to
baeba66
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
741c42e to
23ae8b9
Compare
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
baeba66 to
54c9e8f
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-1
branch
from
54c9e8f to
1fc15f2
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
0dee414 to
bf29be2
Compare
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
1fc15f2 to
47b846b
Compare
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
bf29be2 to
7881060
Compare
We remove this as it is too fragile and difficult to maintain. It would have been broken by a subsequent commit that changes the interpretation of ConstructSaturatedCon.
(In the sense of "uses `conSat`" / "embeds the arguments in the `Expr` subtree rooted at a `Cons` node". Before this commit it created a constructor applied to these same arguments with `APP` and `App`.) Note this only changes `ConstructSaturatedCon`, not `ConstructRefinedCon`, and thus in an openapi frontend using the `MakeConSat` action the behaviour (i.e. what underlying AST is created) will differ depending whether it is in a position with no type info (i.e. where the type is a hole). In particular, in the program Cons @[?_1] [?_2, ?_3] we have - ?_2 : ?_1, so we would do a conSat here - ?_3 : List ?_1, but we would not here (do a refine) This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. BREAKING CHANGE: this will change the interpretation of some actions that may be stored in logs inside programs created from older primer versions. Thus it may break usage of older databases. (The programs should still load fine, and be editable, but undo may be broken if a ConstructSaturatedCon action happens to be in the log.)
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
2 times, most recently
from
bd72d81 to
c135de0
Compare
We remove this as it is too fragile and difficult to maintain. It would have been broken by a subsequent commit that changes the interpretation of ConstructRefinedCon.
(In the sense of "uses `conSat`" / "embeds the arguments in the `Expr` subtree rooted at a `Cons` node". Before this commit it created a constructor applied to these same arguments with `APP` and `App`.) Note that now both actions underlying the openapi `MakeConSat` action use `conSat`. This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant. Note that `spanMaybe` has been resurrected from the previously-removed primer-service/exe-replay/Main.hs BREAKING CHANGE: this will change the interpretation of some actions that may be stored in logs inside programs created from older primer versions. Thus it may break usage of older databases. (The programs should still load fine, and be editable, but undo may be broken if a ConstructRefinedCon action happens to be in the log.)
Now that constructors directly store their arguments, we need actions to enter (and exit) these tree positions, so one can edit them. It would be possible to combine `Child1`, `Child2` and `ConChild`, but for the sake of keeping this commit small and non-breaking we have added a new type of movement.
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. (We will shortly also update this to use saturated constructors for the list constructors.)
This is a trivial commit changing `con` to the equivalent `con0`. This is a step towards all constructors using the saturated combinators, at which point we can remove the legacy `con`.
This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant.
These have to change together as Tests.EvalFull.unit_8,9,prim_partial_map, Tests.Prelude.Polymorphism.tasty_map_prop all compare map output with list_. This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant.
Note that this is a naive translation -- in particular some of the constructors are not fully saturated (i.e. could applied to further arguments). This will be changed in a subsequent commit. However, none of them now appear to the left of an application node. This is a step towards all constructors using the saturated combinators, at which point we can remove the legacy `con`.
This is a step towards all constructors being saturated, at which point we can update the typechecker to enforce that invariant.
This is a trivial commit changing `con` to the equivalent `con0`. This is a step towards all constructors using the saturated combinators, at which point we can remove the legacy `con`.
This is a step towards all constructors being 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 a step towards all constructors being 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 a step towards all constructors being 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 a step towards all constructors being 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 a step towards all constructors being 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 a trivial commit changing `con` to the equivalent `con0`. This is a step towards all constructors using the saturated combinators, at which point we can remove the legacy `con`.
This is a step towards all constructors being 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 a step towards all constructors being 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 a trivial commit to Tests.API changing `con'` to the equivalent `con0'`. This is the final step towards all constructors using the saturated combinators. Now we can remove the legacy `con` and `con'`.
Since everything uses the new saturated combinators, and the old ones have been removed, we can rename to drop the `Sat` suffix.
brprice
force-pushed
the
brprice/saturated-constructors-2
branch
from
c135de0 to
51b93b8
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
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 removes all uses of the old "unsaturated" constructor DSL, and renames the "saturated" one. This also mostly changes all constructors to be fully saturated, but there are a few places that use the new DSL but don't give "enough" arguments. These will be changed in a subsequent PR in which the typechecker will enforce full saturation.