Skip to content

Commit f3809b5

Browse files
authored
Split main Tactics module (#1391)
* Agda splitting machinery * Expand decls! * Only very top-level lambda to args * Preserve top-level args (but it doesnt work very well) * Preserve existing patterns and matches when agdasplitting * Add traceFX debug function * Force a few iterations of splitAgda * Cleanup imports * Put wildcard patterns in for unused variables * Update tests * Agda-unfold on instance deps * wildify at the very end of simplifying * Haddock for top-level functions * Move case splitting stuff into its own module * Exactprint comments * Haddock for casesplit * Use PatCompat * Remove HsDumpAst * Use Pat, not LPat * More massaging Pats * Only unXPat on 8.0.8 * Haddock and cleanup -Wall * Cleanup sus errors * Fix parse errors in GHC > 8.8 * Update comment around unXPat * Cleanup ExactPrint to split FunBind matches * Minor haddock tweak * Bad suggest, hlint * I hate hlint with so much passion * Pull out tactic providers * Stick judgment and context into the RTR * Add type for mkWorkspaceEdits * Split up judgementForHole * Pull LSP-specific stuff out of the main module * Clean up tacticCmd * Minor renaming * Rename noteT to throwError; minor haddock * Move a few more things into the LanguageServer
1 parent 8067d4f commit f3809b5

File tree

6 files changed

+467
-333
lines changed

6 files changed

+467
-333
lines changed

plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,8 @@ library
3333
Ide.Plugin.Tactic.Judgements
3434
Ide.Plugin.Tactic.KnownStrategies
3535
Ide.Plugin.Tactic.KnownStrategies.QuickCheck
36+
Ide.Plugin.Tactic.LanguageServer
37+
Ide.Plugin.Tactic.LanguageServer.TacticProviders
3638
Ide.Plugin.Tactic.Machinery
3739
Ide.Plugin.Tactic.Naming
3840
Ide.Plugin.Tactic.Range

0 commit comments

Comments
 (0)