Allow typedef deletions regardless of whether type is in use #1153

georgefst · 2023-09-28T14:47:11Z

Closes #401.

In the absence of a full feature request, due to this being a fairly straightforward extension of the ideas of #267 with little scope for controversy (by contrast, #402, which I've started some initial work on alongside this, is more exploratory, and I believe will justify a formal feature spec), the behaviour implemented here is as follows:

Deleting a type

Replace all uses of the type with a hole: in expressions, types of top-level definitions, and constructor fields
Replace all uses of any constructor of the type with a hole
Run a full typechecking pass
- There would otherwise be some awkward cases to patch up, such as modifying metadata in type annotations to reflect the change from KType to KHole
- We intend to revisit this sort of thing anyway, including potentially running the typechecker on all actions: Run typechecker whenever a typedef changes #399
- This also automatically cleans up all pattern matches on this type, since we will have set the type of the scrutinee to a hole, and thus the typechecker removes all branches
Set selection to empty

Deleting a constructor

Replace all uses of the constructor with a hole
Remove the corresponding branch from any pattern matches, as well as any appropriate wildcards
Set selection to the type

Deleting the nth field of a constructor

Remove the nth child from all uses of the constructor
Remove the nth child from all patterns featuring the constructor
Set selection to the constructor

dhess · 2023-10-17T14:49:56Z

What's the status of this PR? How much work remains before it's ready for review?

georgefst · 2023-10-17T14:53:09Z

What's the status of this PR? How much work remains before it's ready for review?

None! I just somehow forgot to ask for a review.

primer/src/Primer/App.hs

brprice · 2023-10-17T16:04:34Z

primer/src/Primer/Action/Available.hs

-forTypeDefConsFieldNode con index id l Editable tydefs defs tdName td =
+forTypeDefConsFieldNode con index id l Editable _ _ _ td =


Maybe worth removing these arguments entirely?

Maybe. I suspect we may well re-add them at some point, and even with them unused, the uniformity helps in simplifying the definition of Primer.API.availableActions. Ideally we'd probably refactor this to pass around a record for the common fields, in which case we'd be unlikely to complain that not all fields of the record are used in every function which receives it.

Fair point. I don't have strong opinions either way.

primer/src/Primer/App.hs

brprice · 2023-10-17T16:09:46Z

primer/src/Primer/App.hs

+      updateType = transformM \case
+        TCon _ n | n == d -> tEmptyHole
+        e -> pure e


It is somewhat odd to have updateExpr defined above in a let, but updateType defined below in a where. Any particular reason?

Agreed, but we mostly use where in the other cases, but updateExpr can't go there because then def would be out of scope. It's a bit weird, but I don't think it's worth changing.

primer/src/Primer/App.hs

brprice · 2023-10-17T16:23:25Z

primer/test/Tests/Action/Prog.hs

+unit_DeleteTypeDef :: Assertion
+unit_DeleteTypeDef = progActionTest
+  ( defaultProgEditableTypeDefs
+      $ sequence
+        [ do
+            x <- emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tEmptyHole)
+            astDef "def" x <$> tEmptyHole
+        ]


Might be better to also use the type's constructors at term level, both as constructors and as patterns in a case

brprice · 2023-10-17T16:24:11Z

primer/test/Tests/Action/Prog.hs

+unit_DeleteCon :: Assertion
+unit_DeleteCon = progActionTest
+  ( defaultProgEditableTypeDefs
+      $ sequence
+        [ do
+            x <-
+              case_
+                (emptyHole `ann` (tcon tT `tapp` tcon (tcn "Bool") `tapp` tcon (tcn "Int")))
+                [ branch cA [("x", Nothing), ("y", Nothing), ("z", Nothing)] emptyHole
+                , branch cB [("s", Nothing), ("t", Nothing)] emptyHole
+                ]
+            astDef "def" x <$> tEmptyHole


Could we also use cA as a constructor? (Maybe in the RHS of the cB branch)

brprice

Looks pretty good. I have a handful of small comments and one large one that has triggered me to put "Request changes": the issue about scoping when deleting a field (#1153 (comment))

Signed-off-by: George Thomas <[email protected]>

I haven't found any particular test case which is affected by this, but it seems safer, and will also make it easier to factor out this code. This appears to be an oversight from `257cb77: feat: Implement actions for editing type parameter kinds`. Signed-off-by: George Thomas <[email protected]>

Signed-off-by: George Thomas <[email protected]>

georgefst · 2023-11-27T15:59:42Z

What's the status of this PR? How much work remains before it's ready for review?

None! I just somehow forgot to ask for a review.

Actually, I think it was because I had intended to add a few more tests. I'm just finishing these now, along with @brprice's suggested tests.

This includes fixing up expressions utilising the deleted type/constructor/field so that they still make sense. Mostly this involves replacing subexpressions with holes. Note that this does not yet include deleting type parameters, which we still cannot modify at all when the type is in use. But we aim to relax this restriction as well shortly. We add a unit tests for each action. Note that we didn't actually have any for the old behaviour, due to time constraints when that was implemented. Although the `tasty_available_actions_accepted` property test caught a lot of issues for us. Signed-off-by: George Thomas <[email protected]>

georgefst mentioned this pull request Sep 28, 2023

Editable typedefs: deletion #401

Closed

georgefst force-pushed the georgefst/typedef-deletion branch 3 times, most recently from 9f121c1 to f45ba15 Compare October 5, 2023 15:03

georgefst requested a review from a team October 17, 2023 14:52

brprice reviewed Oct 17, 2023

View reviewed changes

primer/src/Primer/App.hs Outdated Show resolved Hide resolved

brprice reviewed Oct 17, 2023

View reviewed changes

primer/src/Primer/App.hs Show resolved Hide resolved

brprice reviewed Oct 17, 2023

View reviewed changes

primer/src/Primer/App.hs Outdated Show resolved Hide resolved

brprice reviewed Oct 17, 2023

View reviewed changes

brprice requested changes Oct 17, 2023

View reviewed changes

georgefst force-pushed the georgefst/typedef-deletion branch from f45ba15 to ebafd4f Compare October 19, 2023 17:27

georgefst added 3 commits November 23, 2023 15:40

refactor: Generalise deleteAt to return deleted value

900315f

Signed-off-by: George Thomas <[email protected]>

refactor: Factor out running typechecking pass for applying actions

775651d

Signed-off-by: George Thomas <[email protected]>

georgefst force-pushed the georgefst/typedef-deletion branch from ebafd4f to e906f3a Compare November 27, 2023 14:14

brprice approved these changes Nov 27, 2023

View reviewed changes

georgefst force-pushed the georgefst/typedef-deletion branch from e906f3a to 81f235a Compare November 28, 2023 10:29

georgefst enabled auto-merge November 28, 2023 10:29

georgefst force-pushed the georgefst/typedef-deletion branch from 81f235a to 26aaa83 Compare November 28, 2023 11:28

georgefst added this pull request to the merge queue Nov 28, 2023

Merged via the queue into main with commit 4db7bf8 Nov 28, 2023
2 checks passed

georgefst deleted the georgefst/typedef-deletion branch November 28, 2023 11:43

This was referenced Nov 28, 2023

Allow deleting an in-use term definition #1182

Merged

How to avoid deleting students' work #1133

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow typedef deletions regardless of whether type is in use #1153

Allow typedef deletions regardless of whether type is in use #1153

georgefst commented Sep 28, 2023 •

edited

Loading

dhess commented Oct 17, 2023

georgefst commented Oct 17, 2023

brprice Oct 17, 2023

georgefst Oct 19, 2023

brprice Oct 24, 2023

brprice Oct 17, 2023

georgefst Nov 27, 2023

brprice Oct 17, 2023

brprice Oct 17, 2023

brprice left a comment •

edited

Loading

georgefst commented Nov 27, 2023

		forTypeDefConsFieldNode con index id l Editable tydefs defs tdName td =
		forTypeDefConsFieldNode con index id l Editable _ _ _ td =

Allow typedef deletions regardless of whether type is in use #1153

Allow typedef deletions regardless of whether type is in use #1153

Conversation

georgefst commented Sep 28, 2023 • edited Loading

Deleting a type

Deleting a constructor

Deleting the nth field of a constructor

dhess commented Oct 17, 2023

georgefst commented Oct 17, 2023

brprice Oct 17, 2023

Choose a reason for hiding this comment

georgefst Oct 19, 2023

Choose a reason for hiding this comment

brprice Oct 24, 2023

Choose a reason for hiding this comment

brprice Oct 17, 2023

Choose a reason for hiding this comment

georgefst Nov 27, 2023

Choose a reason for hiding this comment

brprice Oct 17, 2023

Choose a reason for hiding this comment

brprice Oct 17, 2023

Choose a reason for hiding this comment

brprice left a comment • edited Loading

Choose a reason for hiding this comment

georgefst commented Nov 27, 2023

georgefst commented Sep 28, 2023 •

edited

Loading

brprice left a comment •

edited

Loading