Skip to content
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.

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

Implement 'Attempt to fill hole' code action #431

Merged
merged 69 commits into from
Oct 3, 2020
Merged
Changes from 2 commits
Commits
Show all changes
69 commits
Select commit Hold shift + click to select a range
34cfa1d
[WIP] Start work on 'auto'
TOTBWF Sep 25, 2020
005bf87
Get current binding
isovector Sep 25, 2020
c2df687
Fix currentBindingName for class methods
isovector Sep 25, 2020
1d7a17e
Proper impl of getDefiningBindings
isovector Sep 25, 2020
18df4e6
Forgot to checkin bindsites
isovector Sep 25, 2020
646ff64
[WIP] Update version of refinery
TOTBWF Sep 25, 2020
59a29c8
Merge branch 'auto' of github.com:isovector/haskell-language-server i…
TOTBWF Sep 25, 2020
3dd9955
Bind all tyvars if possible
isovector Sep 25, 2020
73f1654
WIP: Instantiate polymorphic functions
isovector Sep 26, 2020
46df1a4
Split out fresh type variables when instantiating
isovector Sep 26, 2020
9163605
Make everything compile
isovector Sep 27, 2020
16932da
Separate out tactics
isovector Sep 28, 2020
262e8e1
oneWayUnifyRule
isovector Sep 28, 2020
607e1d6
[WIP] Add 'TacticState'
TOTBWF Sep 28, 2020
1c29915
Merge branch 'auto' of github.com:isovector/haskell-language-server i…
TOTBWF Sep 28, 2020
2fc23ee
[WIP] Tweak 'unify' and 'unifyOneWayRule'
TOTBWF Sep 28, 2020
d03449d
[WIP] Start work on skolem tracking
TOTBWF Sep 28, 2020
ff36b39
[WIP] Fix 'checkSkolemUnification'
TOTBWF Sep 28, 2020
8709694
Update judgement type
isovector Sep 28, 2020
2297df5
Merge branch 'auto' of github.com:isovector/haskell-language-server i…
isovector Sep 28, 2020
8751bb5
Add a Context to TacticM
isovector Sep 28, 2020
b0f233a
Don't destruct already destructed
isovector Sep 28, 2020
d5112be
Remove the internal lib
isovector Sep 28, 2020
34da9ef
Cleanup warnings
isovector Sep 28, 2020
05301ca
Move debug machinery into *.Debug
isovector Sep 28, 2020
2034717
Rip types out of machinery
isovector Sep 28, 2020
d2f093f
Cleanup warnings
isovector Sep 28, 2020
9f95124
Continue splitting Machinery
isovector Sep 28, 2020
03256b3
Rip out GHC and Naming
isovector Sep 28, 2020
6618588
Get it all compiling
isovector Sep 28, 2020
289f049
Stop re-exporting from Machinery
isovector Sep 28, 2020
fce02e2
Split out codegen/rules
isovector Sep 28, 2020
b01f77f
Remove gross/unused tactics
isovector Sep 28, 2020
f2e9f8b
Make newSubgoal derive from an existing judgement
isovector Sep 28, 2020
90c0435
remove newJudgement
isovector Sep 28, 2020
ec12dcd
Disallow current function from auto
isovector Sep 28, 2020
8fdf25b
Cleanup auto
isovector Sep 28, 2020
f08bd0d
Stop using the Judgement ctor
isovector Sep 29, 2020
92c697c
Track pattern value
isovector Sep 29, 2020
a175ff2
Better showAstData
isovector Sep 29, 2020
e7061f1
Get module-scoped funcs
isovector Sep 29, 2020
44e6bfc
Split all data constructors
isovector Sep 30, 2020
fdbb9f4
assumption -> assume
isovector Sep 30, 2020
cc5fcbd
Don't destruct if there are zero datacons
isovector Sep 30, 2020
84d47cd
Lambda case destruct tactics
isovector Sep 30, 2020
7a023b2
Fix the tests
isovector Sep 30, 2020
53ac0d5
Rip out debug stuff since it fails CI
isovector Sep 30, 2020
1f30cfe
Tests for lambda case actions
isovector Sep 30, 2020
9a50f47
Golden testing machinery
isovector Sep 30, 2020
f1d4db7
Merge remote-tracking branch 'upstream/master' into auto
isovector Sep 30, 2020
6d4eba3
Attempt to fill hole
isovector Sep 30, 2020
f56a923
[WIP] Use 'refinery-0.2.0.0'
TOTBWF Sep 30, 2020
fa7234c
[WIP] Update refinery in all stack.yaml files
TOTBWF Sep 30, 2020
ccf92b7
Bump version in cabal file
TOTBWF Sep 30, 2020
ae2afcf
Bump cabal index state
isovector Sep 30, 2020
002339d
Sort goals by heuristic
isovector Oct 1, 2020
cf943c8
Naming for unit types
isovector Oct 1, 2020
b65ccfa
Heuristic for auto
isovector Oct 1, 2020
419224b
Penalize holes more
isovector Oct 1, 2020
cfd3b06
Naming for unit types
isovector Oct 1, 2020
5add6f4
Merge branch 'heuristic' into auto
isovector Oct 1, 2020
141c363
Give the name "unit" to units
isovector Oct 1, 2020
54b335a
Fallback names for symbols and punctuation
isovector Oct 1, 2020
35040d6
Get "good" name for symbolic names
isovector Oct 1, 2020
e2005c9
Update plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
isovector Oct 3, 2020
061a65d
Make the TacticState strict
isovector Oct 3, 2020
14c58cc
Make the judgement strict
isovector Oct 3, 2020
8fa9102
Simplify when we use position mapping
isovector Oct 3, 2020
67bff91
Move bindsites to ghcide
isovector Oct 3, 2020
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
11 changes: 11 additions & 0 deletions plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
Original file line number Diff line number Diff line change
@@ -30,6 +30,7 @@ import DynFlags (unsafeGlobalDynFlags)
import qualified FastString as FS
import GHC.Generics
import GHC.SourceGen.Overloaded
import Ide.Plugin.Tactic.GHC (oneWayUnify)
import Name
import Outputable hiding ((<>))
import Refinery.Tactic
@@ -286,6 +287,16 @@ unify (CType t1) (CType t2) = case tcUnifyTy t1 t2 of
Just unifier -> pure unifier
Nothing -> throwError (UnificationError (CType t1) (CType t2))

oneWayUnifyRule
:: [TyVar] -- ^ binders
-> CType -- ^ type to instiate
-> CType -- ^ at this type
-> RuleM TCvSubst
oneWayUnifyRule binders t1 t2 =
case oneWayUnify binders (unCType t1) (unCType t2) of
Just subst -> pure subst
Nothing -> throwError $ UnificationError t1 t2


------------------------------------------------------------------------------
-- | Convert a DAML compiler Range to a GHC SrcSpan