Skip to content

Split main Tactics module #1391

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 41 commits into from
Feb 17, 2021
Merged

Split main Tactics module #1391

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
41 commits
Select commit Hold shift + click to select a range
4552fb8
Agda splitting machinery
isovector Feb 12, 2021
81c7411
Expand decls!
isovector Feb 12, 2021
bf4e670
Only very top-level lambda to args
isovector Feb 12, 2021
ee2094e
Preserve top-level args (but it doesnt work very well)
isovector Feb 12, 2021
cf75b1e
Preserve existing patterns and matches when agdasplitting
isovector Feb 14, 2021
14fa9f6
Add traceFX debug function
isovector Feb 14, 2021
f3ea83f
Force a few iterations of splitAgda
isovector Feb 14, 2021
0e120de
Merge branch 'master' into agda-case-split
isovector Feb 14, 2021
d573e7a
Cleanup imports
isovector Feb 14, 2021
de541c2
Put wildcard patterns in for unused variables
isovector Feb 14, 2021
af02f05
Update tests
isovector Feb 14, 2021
6a5f2e4
Agda-unfold on instance deps
isovector Feb 15, 2021
5a38557
wildify at the very end of simplifying
isovector Feb 15, 2021
e78549c
Haddock for top-level functions
isovector Feb 15, 2021
cca1f34
Move case splitting stuff into its own module
isovector Feb 15, 2021
8fcb936
Exactprint comments
isovector Feb 15, 2021
41c7461
Haddock for casesplit
isovector Feb 15, 2021
c6112c4
Use PatCompat
isovector Feb 15, 2021
57c2da2
Remove HsDumpAst
isovector Feb 15, 2021
0d698aa
Use Pat, not LPat
isovector Feb 16, 2021
5c1f3e0
More massaging Pats
isovector Feb 16, 2021
96f566b
Only unXPat on 8.0.8
isovector Feb 16, 2021
57e906f
Haddock and cleanup -Wall
isovector Feb 16, 2021
b857ca7
Cleanup sus errors
isovector Feb 16, 2021
3ea09c3
Fix parse errors in GHC > 8.8
isovector Feb 16, 2021
5348c61
Merge branch 'master' into agda-case-split
isovector Feb 16, 2021
b2236b8
Update comment around unXPat
isovector Feb 16, 2021
1261489
Cleanup ExactPrint to split FunBind matches
isovector Feb 16, 2021
d8a8198
Minor haddock tweak
isovector Feb 16, 2021
529e4dd
Bad suggest, hlint
isovector Feb 16, 2021
cffba27
I hate hlint with so much passion
isovector Feb 16, 2021
d8b3753
Pull out tactic providers
isovector Feb 17, 2021
a73a305
Stick judgment and context into the RTR
isovector Feb 17, 2021
b16c730
Add type for mkWorkspaceEdits
isovector Feb 17, 2021
c71b3f7
Split up judgementForHole
isovector Feb 17, 2021
41ebd2e
Pull LSP-specific stuff out of the main module
isovector Feb 17, 2021
0563434
Clean up tacticCmd
isovector Feb 17, 2021
c1ded82
Minor renaming
isovector Feb 17, 2021
6161373
Merge branch 'master' into cleanup-main-module
isovector Feb 17, 2021
67badc8
Rename noteT to throwError; minor haddock
isovector Feb 17, 2021
ae0830d
Move a few more things into the LanguageServer
isovector Feb 17, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,8 @@ library
Ide.Plugin.Tactic.Judgements
Ide.Plugin.Tactic.KnownStrategies
Ide.Plugin.Tactic.KnownStrategies.QuickCheck
Ide.Plugin.Tactic.LanguageServer
Ide.Plugin.Tactic.LanguageServer.TacticProviders
Ide.Plugin.Tactic.Machinery
Ide.Plugin.Tactic.Naming
Ide.Plugin.Tactic.Range
Expand Down
Loading