search

haskell / haskell-language-server

Official haskell ide support via language server (LSP). Successor of ghcide & haskell-ide-engine.
Apache License 2.0
2.65k stars 355 forks source link

Case splitting features #323

Closed pepeiborra closed 4 years ago

pepeiborra commented 4 years ago

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

Case splitting an equation (in Idris):

idris

How this could be implemented in HLS:

Tools that already do this:

jneira commented 4 years ago

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): https://github.com/haskell/haskell-ide-engine/issues/907

isovector commented 4 years ago

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

isovector commented 4 years ago

Peek 2020-09-07 16-46

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

pepeiborra commented 4 years ago

Wow, that looks fabulous!

isovector commented 4 years ago

Blocked by https://github.com/alanz/ghc-exactprint/issues/91, since it prevents us from to synthesize new terms that respect layout.

pepeiborra commented 4 years ago

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 commented 4 years ago

@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 commented 2 years ago

Should we reopen this for the latest version? (:

pepeiborra commented 2 years ago

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

isovector commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 commented 4 months ago

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!