Skip to content

Commit

Permalink
Implement 'Attempt to fill hole' code action (#431)
Browse files Browse the repository at this point in the history
* [WIP] Start work on 'auto'

* Get current binding

* Fix currentBindingName for class methods

* Proper impl of getDefiningBindings

* Forgot to checkin bindsites

* [WIP] Update version of refinery

* Bind all tyvars if possible

* WIP: Instantiate polymorphic functions

* Split out fresh type variables when instantiating

* Make everything compile

* Separate out tactics

* oneWayUnifyRule

* [WIP] Add 'TacticState'

* [WIP] Tweak 'unify' and 'unifyOneWayRule'

* [WIP] Start work on skolem tracking

* [WIP] Fix 'checkSkolemUnification'

* Update judgement type

* Add a Context to TacticM

* Don't destruct already destructed

* Remove the internal lib

* Cleanup warnings

* Move debug machinery into *.Debug

* Rip types out of machinery

* Cleanup warnings

* Continue splitting Machinery

* Rip out GHC and Naming

* Get it all compiling

* Stop re-exporting from Machinery

* Split out codegen/rules

* Remove gross/unused tactics

* Make newSubgoal derive from an existing judgement

* remove newJudgement

* Disallow current function from auto

* Cleanup auto

* Stop using the Judgement ctor

* Track pattern value

* Better showAstData

* Get module-scoped funcs

* Split all data constructors

* assumption -> assume

* Don't destruct if there are zero datacons

* Lambda case destruct tactics

* Fix the tests

* Rip out debug stuff since it fails CI

* Tests for lambda case actions

* Golden testing machinery

* Attempt to fill hole

* [WIP] Use 'refinery-0.2.0.0'

* [WIP] Update refinery in all stack.yaml files

* Bump version in cabal file

* Bump cabal index state

* Sort goals by heuristic

* Naming for unit types

* Heuristic for auto

* Penalize holes more

* Naming for unit types

* Give the name "unit" to units

* Fallback names for symbols and punctuation

* Get "good" name for symbolic names

* Update plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs

Co-authored-by: wz1000 <[email protected]>

* Make the TacticState strict

* Make the judgement strict

* Simplify when we use position mapping

* Move bindsites to ghcide

Co-authored-by: Sandy Maguire <[email protected]>
Co-authored-by: wz1000 <[email protected]>
  • Loading branch information
3 people authored Oct 3, 2020
1 parent 9f13e8f commit 2be03cc
Show file tree
Hide file tree
Showing 46 changed files with 1,192 additions and 531 deletions.
2 changes: 1 addition & 1 deletion cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,6 @@ package ghcide

write-ghc-environment-files: never

index-state: 2020-09-23T17:24:43Z
index-state: 2020-09-30T21:52:43Z

allow-newer: data-tree-print:base
2 changes: 1 addition & 1 deletion ghcide
20 changes: 15 additions & 5 deletions haskell-language-server.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ library
executable haskell-language-server
import: agpl, common-deps
main-is: Main.hs
hs-source-dirs: exe plugins/default/src
hs-source-dirs: exe plugins/default/src plugins/tactics/src
other-modules:
Ide.Plugin.Eval
Ide.Plugin.Example
Expand All @@ -93,9 +93,17 @@ executable haskell-language-server
Ide.Plugin.Retrie
Ide.Plugin.StylishHaskell
Ide.Plugin.Tactic
Ide.Plugin.Tactic.Types
Ide.Plugin.Tactic.CodeGen
Ide.Plugin.Tactic.Context
Ide.Plugin.Tactic.Debug
Ide.Plugin.Tactic.GHC
Ide.Plugin.Tactic.Judgements
Ide.Plugin.Tactic.Machinery
Ide.Plugin.Tactic.Naming
Ide.Plugin.Tactic.Range
Ide.Plugin.Tactic.Tactics
Ide.Plugin.Tactic.Types
Ide.Plugin.Tactic.TestTypes
Ide.TreeTransform

ghc-options:
Expand Down Expand Up @@ -147,8 +155,9 @@ executable haskell-language-server
, transformers
, unordered-containers
, ghc-source-gen
, refinery
, refinery >=0.2.0.0
, ghc-exactprint
, fingertree

if flag(agpl)
build-depends: brittany
Expand Down Expand Up @@ -237,7 +246,8 @@ test-suite func-test
, tasty-golden
, tasty-rerun

hs-source-dirs: test/functional plugins/default/src
hs-source-dirs: test/functional plugins/tactics/src

main-is: Main.hs
other-modules:
Command
Expand All @@ -258,7 +268,7 @@ test-suite func-test
Symbol
TypeDefinition
Tactic
Ide.Plugin.Tactic.Types
Ide.Plugin.Tactic.TestTypes

ghc-options:
-Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N
Expand Down
264 changes: 0 additions & 264 deletions plugins/default/src/Ide/Plugin/Tactic/Machinery.hs

This file was deleted.

Loading

0 comments on commit 2be03cc

Please sign in to comment.