Case splitting and lambda introduction #391

isovector · 2020-09-09T21:36:20Z

@TOTBWF and I had a mini hackathon last weekend and this is the results. It provides case splitting, homomorphic case splitting[^1], and lambda introduction. It does a reasonable job of coming up with good names, and implements a lot of general-purpose machinery for other plugins.

[^1] Case splitting to the same datacons --- useful for writing things like functor instances.

It looks like this:

Fixes #323 --- although that usecase could be improved with a separate action that flattens foo = \x y z -> bar into foo x y z = bar.

We have plans to follow this up with more type-directed code generation; a great deal of it is already implemented, but not yet polished. Most of Ide.Plugin.Tactic.Tactics is towards that purpose.

isovector · 2020-09-09T21:44:43Z

I think this needs refinery added to the stack.yamls, but was hoping CI could tell me.

expipiplus1 · 2020-09-10T04:07:06Z

It would be nice if it were configurable to generate LambdaCase splits too.

For the example in OP:

fmapEither = \fab -> \case
  Left c -> Left _ 
  Right a -> Right _

Of course this feature request shouldn't interfere with this being merged!

pepeiborra

Super cool, thanks @isovector and @TOTBWF !!!!

I won't claim to understand all that is going on, but see my comments for minor nits on ghcide specifics.

Tests would be very welcome in future PRs to ensure that the plugin doesn't break accidentally.

src/Ide/LocalBindings.hs

src/Ide/Plugin/Tactic/Machinery.hs

src/Ide/Plugin/Tactic/Tactics.hs

src/Ide/TreeTransform.hs

src/Ide/Plugin/Tactic.hs

isovector · 2020-09-10T07:58:47Z

@pepeiborra what sorts of tests would you be interested in? Things to show the tactics do what they say? Or tests more along the lines of the plugin integration at large?

wz1000 · 2020-09-10T08:10:58Z

src/Ide/LocalBindings.hs

+-- **WARNING:** This doesn't yet work over TH splices or arrow syntax --- and
+-- possibly other obscure pieces of the AST.
+dataBindings :: Data a => S.Set Id -> a -> M.Map SrcSpan (S.Set Id)
+dataBindings in_scope = foldMapOf biplate $ cool collect


This information is computed in .hie files. If you look at the refmap in the result of the GetHieFile rule, you will get a map Map Identifier [(Span, IdentifierDetails Type)]. IdentifierDetails contains a set of ContextInfo, from which you recover the scope for that particular identifier using getScopeFromContext.

I'd love to get rid of this; but if I'm reading your comment correctly, that mapping is the wrong direction. We want to go from a span to every binding in scope inside of it.

Yes, you need to invert the map into something like a IntervalMap, which should be pretty straightforward to construct. What we have is essentially a Map Name [Scope], what we need is an IntervalMap SrcLoc Name, right?

Delightfully good idea. I'll implement it today. Thanks!

I gave this a go, and got as far as getting back a TypeIndex from hie. But I can't figure out how to reconstitute this into a proper GHC Type, which is necessary for how we've set up refinery. Holding off on moving forwards until someone can point me in the right direction on that one!

See #396, that should make this work

pepeiborra · 2020-09-10T08:25:01Z

@pepeiborra what sorts of tests would you be interested in? Things to show the tactics do what they say? Or tests more along the lines of the plugin integration at large?

See the tests for the Eval plugin - golden tests to show that all the plugin salient features work as expected.

isovector · 2020-09-10T08:30:25Z

I'll tackle the tests and suggestions tomorrow :)

isovector · 2020-09-11T04:29:21Z

@expipiplus1 happy to implement that immediately after. Please file a bug if one doesn't already exist!

expipiplus1 · 2020-09-11T04:40:40Z

@isovector done, thanks! #394

test/functional/Tactic.hs

isovector · 2020-09-11T06:56:43Z

@pepeiborra tests are added and passing.

pepeiborra · 2020-09-11T07:50:47Z

Needs rebasing

jneira · 2020-09-11T09:18:37Z

Yeah, i moved part of exe/Main to src/Ide/Main and modules and lib dependencies related with plugins to the executable component in the .cabal file. The plugin list continue being in exe/Main.hs though.
I hope the rebase is relatively easy but feel free to ask any question.

georgefst · 2020-09-11T18:10:06Z

that usecase could be improved with a separate action that flattens foo = \x y z -> bar into foo x y z = bar

HLint will deal with that, whenever that plugin is completed.

isovector · 2020-09-12T03:19:29Z

Rebased and everything is a go. The stack files need some new additions, but I was hoping CI would tell me what changes need to happen. How can we get CI running on this PR?

plugins/default/src/Ide/LocalBindings.hs

wz1000

Thanks, great work here! Look forward to using it.

[WIP] Add Skeleton for Tactic Plugin Local bindings [WIP] Add more to the code action provider more cases for bindings is it a hole? Beginning of tactics machinery tactics machinery split out tactics machinery; finish porting tactics Haddock for tactics machinery Use a map for hypothesis Better types on LocalBindings render the result of running a tactic Hypothesis from bindings Sort types mostSpecificSpan Render Actually add the tactic plugin :) [WIP] Do stuff slightly better span better sorting for specific spans Fix size [WIP] It does the thing!! Multiple tactic actions Parenthesize if necessary [WIP] Home on the 'Range' destruct and homo fix naming and parens Cleanup Plugin Tactic context dependent destruct and homo Generalized interface More composable Remove TacticVariety Haddock Describe spooky monoidal behavior Only look at actual holes Auto if possible debugging Maybe grafting works now Transformation works; tree doesnt Remove debugging Proper indentation and parenthesizing Less fancy parenthesizing Don't crash if we can't lookup things Holes must start with an underscore Haddock pass Module restructuring Fix the cabal file Intros, and disable some of the unpolished tactics Disable autoIfPossible Fix stack.yaml Respond to simple PR comments. Get a proper dflags WIP on a better bindings interface Simplify dflags lookup and expose titles Tactic tests Add a few more tests Cleanup imports Haddock the tests Rebase on ghcide HEAD (haskell#378) * Rebase on top of ghcide HEAD * use Development.IDE to trim imports * Fix Eval plugin to use GhcSessionDeps Use stale data in explicit imports lens (haskell#383) This prevents the lenses from disappearing while editing, which causes lots of unpleasant jumping Create hls-plugin-api and move plugins to exe Keep current version Add hls-plugin-api component to cradle Move exe modules to main library Format .cabal files with `cabal-fmt --ident 2` Restore ghcide ref Fix cradles Move tactic plugin Almost there! Get the tests running again Empty commit for CI Add refinery to stack more stack woes Duplicate NoExt and less dependency on ghc Cradle is necessary bump ghcide submodule (haskell#396) * Bump ghcide submodule * Update stack descriptors Co-authored-by: Pepe Iborra <[email protected]> Update ghcide Compute an interval map of what's in scope Fix 'binding'

wz1000 · 2020-09-16T09:29:35Z

@isovector please review the last two commits.

jneira · 2020-09-16T16:54:18Z

Hi, could we keep the default stack.yaml with ghc-8.6.5?, please
ghc-8.8.2 is not reliable in Windows
Moreover, a new version of ghc-lib has just been released, fixing a bug building it.
Thanks!

Anrock · 2020-10-05T14:48:39Z

Um, how do I trigger case splitting on argument like

foo :: EnumLike -> Bool
foo Enum1 = ...
foo Enum2 = ...

In neovim I don't have those nice light bulbs to see where code actions are available and I've tried

foo :: EnumLike -> Bool  -- no available actions on foo
foo _ = ... -- no available actions on underscore

foo :: EnumLike -> Bool -- no available actions on foo
foo = ... -- no available actions on foo here either

Where should I put my text cursor exactly to see case splitting or is it only for case of?

wz1000 · 2020-10-05T14:52:45Z

@Anrock try foo x = _

Anrock · 2020-10-06T10:05:38Z

@wz1000 thanks, that works, however it produces (case x of ...) and I wanted multiple definitions of function. I guess this would be another feature.

isovector · 2020-10-06T15:05:14Z

pull requests welcome!

pepeiborra approved these changes Sep 10, 2020

View reviewed changes

isovector mentioned this pull request Sep 10, 2020

Plugin infrastructure for performing WorkspaceApplyEdit with correct indentation #385

Closed

wz1000 reviewed Sep 10, 2020

View reviewed changes

expipiplus1 mentioned this pull request Sep 11, 2020

Allow using LambdaCase in case splitting plugin #394

Closed

googleson78 reviewed Sep 11, 2020

View reviewed changes

test/functional/Tactic.hs Outdated Show resolved Hide resolved

wz1000 mentioned this pull request Sep 12, 2020

Add GetHieAsts rule, Replace SpanInfo, add support for DocumentHighlight and scope-aware completions for local variables haskell/ghcide#784

Merged

4 tasks

isovector mentioned this pull request Sep 13, 2020

Tactics again (hoping CI will pick up this PR) #397

Closed

wz1000 reviewed Sep 13, 2020

View reviewed changes

plugins/default/src/Ide/LocalBindings.hs Outdated Show resolved Hide resolved

wz1000 approved these changes Sep 15, 2020

View reviewed changes

isovector and others added 3 commits September 16, 2020 00:22

Create Types module to reduce test dependencies

7565509

Make it compile with 8.10, handle errors, move LocalBinding to ghcide

3d017aa

wz1000 force-pushed the tactics branch from f9f1adc to 3d017aa Compare September 16, 2020 09:28

fix 8.10 stack yaml (let's pray)

ea46307

wz1000 force-pushed the tactics branch from ba25122 to 79e2636 Compare September 16, 2020 10:57

update stack.yamls

b458743

wz1000 force-pushed the tactics branch from 79e2636 to b458743 Compare September 16, 2020 11:01

wz1000 added 4 commits September 16, 2020 16:43

add missing file

3583d54

relax exactprint bound

418b9bd

aarghhh add missing '-' to stack-8.6.5.yaml

7ada538

Only produce code actions for unbound variables

85713e8

make 8.6.5 default stack.yaml

ea48756

wz1000 merged commit b43a8cd into haskell:master Sep 16, 2020

isovector mentioned this pull request Sep 22, 2020

Split HLS plugins into internal libraries #421

Closed

jneira linked an issue Sep 23, 2020 that may be closed by this pull request

Allow using LambdaCase in case splitting plugin #394

Closed

jneira removed a link to an issue Sep 23, 2020

Allow using LambdaCase in case splitting plugin #394

Closed

jneira mentioned this pull request Sep 23, 2020

Converge on implicit cradle discovery mechanism #38

Closed

isovector deleted the tactics branch May 21, 2021 16:43

isovector mentioned this pull request Jun 12, 2021

Disable hole fit suggestions when running Wingman #1873

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Case splitting and lambda introduction #391

Case splitting and lambda introduction #391

isovector commented Sep 9, 2020 •

edited

Loading

isovector commented Sep 9, 2020

expipiplus1 commented Sep 10, 2020

pepeiborra left a comment

isovector commented Sep 10, 2020

wz1000 Sep 10, 2020 •

edited

Loading

isovector Sep 10, 2020

wz1000 Sep 10, 2020

isovector Sep 10, 2020

isovector Sep 11, 2020

wz1000 Sep 12, 2020

pepeiborra commented Sep 10, 2020

isovector commented Sep 10, 2020

isovector commented Sep 11, 2020

expipiplus1 commented Sep 11, 2020

isovector commented Sep 11, 2020

pepeiborra commented Sep 11, 2020

jneira commented Sep 11, 2020 •

edited

Loading

georgefst commented Sep 11, 2020

isovector commented Sep 12, 2020

wz1000 left a comment

wz1000 commented Sep 16, 2020

jneira commented Sep 16, 2020 •

edited

Loading

Anrock commented Oct 5, 2020 •

edited

Loading

wz1000 commented Oct 5, 2020

Anrock commented Oct 6, 2020 •

edited

Loading

isovector commented Oct 6, 2020

Case splitting and lambda introduction #391

Case splitting and lambda introduction #391

Conversation

isovector commented Sep 9, 2020 • edited Loading

isovector commented Sep 9, 2020

expipiplus1 commented Sep 10, 2020

pepeiborra left a comment

Choose a reason for hiding this comment

isovector commented Sep 10, 2020

wz1000 Sep 10, 2020 • edited Loading

Choose a reason for hiding this comment

isovector Sep 10, 2020

Choose a reason for hiding this comment

wz1000 Sep 10, 2020

Choose a reason for hiding this comment

isovector Sep 10, 2020

Choose a reason for hiding this comment

isovector Sep 11, 2020

Choose a reason for hiding this comment

wz1000 Sep 12, 2020

Choose a reason for hiding this comment

pepeiborra commented Sep 10, 2020

isovector commented Sep 10, 2020

isovector commented Sep 11, 2020

expipiplus1 commented Sep 11, 2020

isovector commented Sep 11, 2020

pepeiborra commented Sep 11, 2020

jneira commented Sep 11, 2020 • edited Loading

georgefst commented Sep 11, 2020

isovector commented Sep 12, 2020

wz1000 left a comment

Choose a reason for hiding this comment

wz1000 commented Sep 16, 2020

jneira commented Sep 16, 2020 • edited Loading

Anrock commented Oct 5, 2020 • edited Loading

wz1000 commented Oct 5, 2020

Anrock commented Oct 6, 2020 • edited Loading

isovector commented Oct 6, 2020

isovector commented Sep 9, 2020 •

edited

Loading

wz1000 Sep 10, 2020 •

edited

Loading

jneira commented Sep 11, 2020 •

edited

Loading

jneira commented Sep 16, 2020 •

edited

Loading

Anrock commented Oct 5, 2020 •

edited

Loading

Anrock commented Oct 6, 2020 •

edited

Loading