Conversation
|
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
force-pushed
the
brprice/saturated-constructors-4
branch
from
4c2a561 to
d26c774
Compare
brprice
force-pushed
the
brprice/saturated-constructors-5
branch
2 times, most recently
from
774cf55 to
8661e86
Compare
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
21b50df to
e49183d
Compare
brprice
force-pushed
the
brprice/saturated-constructors-5
branch
from
8661e86 to
89b73cf
Compare
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
e49183d to
edcec45
Compare
brprice
force-pushed
the
brprice/saturated-constructors-5
branch
from
89b73cf to
7f9237b
Compare
|
EDIT: both of these have been addressed TODO: is there any point in having both saturate and refine ctor actions now that they do not contain indices? TODO: I have deployed this and noticed a couple of bugs when using it interactively (to do with typecaches and actions)
|
What's the current thinking on this? I think when we met in person two weeks ago you said, after explaining to me the differences between the two actions, that this needed some re-thinking in the context of always-saturated constructors, but that you were leaning towards unifying them. If so, will we see that change in this PR?
We've seen this before in #927. |
Yes, I'll add another commit, which should be fairly trivial
Thanks -- this is then an old bug that I won't worry about in this pr. |
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
edcec45 to
a6e9d65
Compare
brprice
force-pushed
the
brprice/saturated-constructors-5
branch
from
95199d9 to
520ccb1
Compare
This changes the order of operations in a `do` block, which will have the effect of changing what IDs each node gets assigned. The reason for this is somewhat technical and somewhat trivial: it happens to be necessary so we can split some future changes up into separate commits. The particular change we are aiming for is to drop type arguments from constructors. We'll reduce churn in the main commit by changing the DSL's `con` to ignore its type argument but still tick the fresh ID counter for it (thus we can make the change to the AST without updating much of the testsuite). There will then be a followup which mechanically drops all the ignored arguments. There is a small wrinkle in this plan: if `con` is used in such a way as to ignore a node which would previously be assigned the highest ID in a program, then a test that checks that the `nextProgID` of that program is what was returned by `create` will fail. This actually happens in exactly one place: `Tests.App.unit_mkAppSafe_mapOddProg`. We solve this by a simple (and subtle) reordering so the last ID in `mapOddProg` is in its type, and thus not dropped.
This changes the definition of `Con`, removing the type arguments.
This simplifies typechecking constructors (including removing some
now-unused error cases), removes the actions for entering type
children of a constructor, removes the workaround for Eval (that
focusType did not look at type arguments in constuctors) and
simplifies Eval (when doing a case reduction, we do not need to worry
about inconsistencies between indices of a constructor and its annotation).
We remove some tests that relied on having indices:
- unit_type_preservation_case_hole_regression: its starting point is impossible
- unit_con_hole_app_type_5
- unit_con_tyargs_consistent_sh
There are some test updates to pay particular attention to, since they
importantly depend on the types in constructor indices (thus not
changing the test, i.e. so these arguments are simply ignored, will
either break the test or subtly change what is being tested):
- Tests.Action.unit_rename_LAM{,_2}
- Tests.Action.Capture.unit_ty_tm_same_namespace
- Tests.Action.Prog.unit_copy_paste_expr_1
- Tests.Action.Prog.setConFieldTypeHelper
- Tests.Eval.unit_redexes_lettype_2
- Tests.Questions.unit_variablesInScope_shadowed
To avoid too much churn in this commit we make the DSL ignore these
index arguments, but still update the ID counter for them. (We will
return to this in a subsequent commit.) Some golden test output has
thus changed.
BREAKING CHANGE: this changes the definition of `Expr'`, which breaks
compatibility with databases generated by previous versions of primer.
In a subsequent commit we will remove the argument altogether.
Now that constructors are fully saturated and do not store their indices, there is essentially no difference between inserting a saturated constructor and a refined constructor. This is because they both insert that constructor applied to the same number empty term holes (dictated by the number of fields that constructor has). In the past, when constructors were applied to types corresponding to the parameters of their parent datatype definition, "saturated" would put empty type holes, whereas "refine" would infer what types it must be applied to from context. Note that above we said "essentially no difference". The inessential differences occur when one of the following is true - there are internal failures in refinement, which should never happen - smartholes are off, which is an unsupported mode for clients (it is intended for internal testing purposes) - one tries to "refine" in a synthesisable-only context, which shouldn't happen with an openapi client, since we wouldn't offer that action in that context anyway BREAKING CHANGE: this removes an action that may have been stored in an undo log in a database created by a previous version of primer, thus breaking loading such DBs.
brprice
force-pushed
the
brprice/saturated-constructors-4
branch
from
a6e9d65 to
f00e897
Compare
brprice
force-pushed
the
brprice/saturated-constructors-5
branch
from
520ccb1 to
07043e0
Compare
|
FTR: This PR replaces #891, and I have checked the todo list there works as expected |
brprice
changed the title
2 participants
This final PR in the saturated constructors saga removes indices (i.e. type arguments) from constructors.