Case splitting features

[pepeiborra]

Original Twitter threads: https://twitter.com/Anka213/status/1289724597735063552

Case splitting an equation (in Idris):

How this could be implemented in HLS:

• A code action provider to split equations with an empty rhs
• A completion provider with splitting suggestions for case [..] of

Tools that already do this:

• hackage.haskell.org/package/shplit
• https://hackage.haskell.org/package/ghc-mod-5.8.0.0/docs/GhcMod-Exe-CaseSplit.html

[jneira]

Just in case the references can help, the feature was included in hie (afaik using ghc-mod underneath and using hare by @Avi-D-coder): haskell/haskell-ide-engine#907

[isovector]

@TOTBWF and are tackling this (and other great things!)

[isovector]

It's looking really good! We want to get a little more code automation in before opening a PR.

[pepeiborra]

Wow, that looks fabulous!

[isovector]

Blocked by alanz/ghc-exactprint#91, since it prevents us from to synthesize new terms that respect layout.

[pepeiborra]

Blocked by alanz/ghc-exactprint#91, since it prevents us from to synthesize new terms that respect layout.

Oh no! Please share the ghcide/HLS branch and maybe someone can find a workaround.

[isovector]

@pepeiborra sure! I will be forever in your debt if you can. https://github.com/isovector/haskell-language-server/tree/tactics

Everything is hooked up and working, but TreeTransform (which uses ExactPrint) runs into this issue when trying to insert the generated terms back into the source.

[aryairani]

Should we reopen this for the latest version? (:

[pepeiborra]

@santiweight is already working on this, by reviving tactics to work with 9.x and beyond

[isovector]

We're in a bit of a weird situation here; I was planning on picking up the work from @santiweight due to a possible contract for this feature, but it didn't end up coming through. The work necessary to port things to 9.2 is hairy and thankless and I'm not particularly keen to push it through --- especially without a plan for how we can prevent breakage of this sort in the future. It's not a situation I love, but it is what it is.

[santiweight]

Unfortunately for myself I'm a little too keen to get it done! We have the case splitting functionality completely ported now, and passing all tests.

I would like to port the tactics functionality and I expect it will be possible. I will try my best over time to get it done: as Sandy says, it's quite hairy and opaque. Thankfully, I am now quite comfortable with the new exactprint api. The main thing I have left to learn is all of Sandy's fancy judgment features!

I think I now have enough knowledge to get the job finished :)

[santiweight]

Wrt to breakage in the future: I agree totally. It gives me a little anxiety... However, the new API, while hard to learn, is quite productive and understandable. As far as I know, this is the only planned change to the exact print infrastructure for the foreseeable future, and so I'm allowing myself to take the risk this time.

[MangoIV]

heya! can we expect that this will come back to hls? is there work being done or tracked elsewhere?
I would be happy if it came independently of a tactics plugin, just being able to case split would be awesome!