Skip to content

Commit b43a8cd

Browse files
isovectorwz1000
isovector
and
wz1000
authored
Case splitting and lambda introduction (#391)
Case split and tactics via refinery Bump ghcide submodule to get completion for local variables. Co-authored-by: Zubin Duggal <[email protected]>
1 parent 34eff96 commit b43a8cd

23 files changed

+1068
-9
lines changed

‎cabal.project

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,6 @@ package ghcide
2020

2121
write-ghc-environment-files: never
2222

23-
index-state: 2020-09-09T00:00:00Z
23+
index-state: 2020-09-16T00:00:00Z
2424

2525
allow-newer: data-tree-print:base

‎exe/Main.hs

+4
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ import Ide.Plugin.ImportLens as ImportLens
2020
import Ide.Plugin.Ormolu as Ormolu
2121
import Ide.Plugin.StylishHaskell as StylishHaskell
2222
import Ide.Plugin.Retrie as Retrie
23+
import Ide.Plugin.Tactic as Tactic
2324
#if AGPL
2425
import Ide.Plugin.Brittany as Brittany
2526
#endif
@@ -45,6 +46,9 @@ idePlugins includeExamples = pluginDescToIdePlugins allPlugins
4546
, Pragmas.descriptor "pragmas"
4647
, Floskell.descriptor "floskell"
4748
, Fourmolu.descriptor "fourmolu"
49+
, Tactic.descriptor "tactic"
50+
-- , genericDescriptor "generic"
51+
-- , ghcmodDescriptor "ghcmod"
4852
, Ormolu.descriptor "ormolu"
4953
, StylishHaskell.descriptor "stylish-haskell"
5054
, Retrie.descriptor "retrie"

‎ghcide

Submodule ghcide updated 28 files

‎haskell-language-server.cabal

+22-1
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,11 @@ executable haskell-language-server
9292
Ide.Plugin.Pragmas
9393
Ide.Plugin.Retrie
9494
Ide.Plugin.StylishHaskell
95+
Ide.Plugin.Tactic
96+
Ide.Plugin.Tactic.Types
97+
Ide.Plugin.Tactic.Machinery
98+
Ide.Plugin.Tactic.Tactics
99+
Ide.TreeTransform
95100

96101
ghc-options:
97102
-threaded -Wall -Wno-name-shadowing -Wredundant-constraints
@@ -123,13 +128,27 @@ executable haskell-language-server
123128
, ormolu ^>=0.1.2
124129
, regex-tdfa
125130
, retrie >=0.1.1.0
131+
, hslogger
132+
, optparse-applicative
133+
, haskell-lsp ^>=0.22
134+
, hls-plugin-api
135+
, lens
136+
, mtl
137+
, ormolu ^>=0.1.2
138+
, regex-tdfa
139+
, retrie >=0.1.1.0
126140
, safe-exceptions
127141
, shake >=0.17.5
128142
, stylish-haskell ^>=0.11
129143
, temporary
144+
, text
145+
, syb
130146
, time
131147
, transformers
132148
, unordered-containers
149+
, ghc-source-gen
150+
, refinery
151+
, ghc-exactprint
133152

134153
if flag(agpl)
135154
build-depends: brittany
@@ -218,7 +237,7 @@ test-suite func-test
218237
, tasty-golden
219238
, tasty-rerun
220239

221-
hs-source-dirs: test/functional
240+
hs-source-dirs: test/functional plugins/default/src
222241
main-is: Main.hs
223242
other-modules:
224243
Command
@@ -238,6 +257,8 @@ test-suite func-test
238257
Rename
239258
Symbol
240259
TypeDefinition
260+
Tactic
261+
Ide.Plugin.Tactic.Types
241262

242263
ghc-options:
243264
-Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N

‎plugins/default/src/Ide/Plugin/Tactic.hs

+269
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,269 @@
1+
{-# LANGUAGE DeriveAnyClass #-}
2+
{-# LANGUAGE DeriveGeneric #-}
3+
{-# LANGUAGE LambdaCase #-}
4+
{-# LANGUAGE OverloadedStrings #-}
5+
{-# LANGUAGE TupleSections #-}
6+
{-# LANGUAGE TypeApplications #-}
7+
{-# LANGUAGE ViewPatterns #-}
8+
9+
-- | A plugin that uses tactics to synthesize code
10+
module Ide.Plugin.Tactic
11+
( descriptor
12+
, tacticTitle
13+
, TacticCommand (..)
14+
) where
15+
16+
import Control.Monad
17+
import Control.Monad.Trans
18+
import Control.Monad.Trans.Maybe
19+
import Data.Aeson
20+
import Data.Coerce
21+
import qualified Data.Map as M
22+
import qualified Data.Set as S
23+
import Data.Maybe
24+
import qualified Data.Text as T
25+
import Data.Traversable
26+
import Development.IDE.Core.PositionMapping
27+
import Development.IDE.Core.RuleTypes
28+
import Development.IDE.Core.Service (runAction)
29+
import Development.IDE.Core.Shake (useWithStale, IdeState (..))
30+
import Development.IDE.GHC.Compat
31+
import Development.IDE.GHC.Error (realSrcSpanToRange)
32+
import Development.IDE.GHC.Util (hscEnv)
33+
import Development.Shake (Action)
34+
import GHC.Generics (Generic)
35+
import HscTypes (hsc_dflags)
36+
import Ide.Plugin (mkLspCommand)
37+
import Ide.Plugin.Tactic.Machinery
38+
import Ide.Plugin.Tactic.Tactics
39+
import Ide.Plugin.Tactic.Types
40+
import Ide.TreeTransform (transform, graft, useAnnotatedSource)
41+
import Ide.Types
42+
import Language.Haskell.LSP.Core (clientCapabilities)
43+
import Language.Haskell.LSP.Types
44+
import OccName
45+
import qualified FastString
46+
47+
48+
descriptor :: PluginId -> PluginDescriptor
49+
descriptor plId = (defaultPluginDescriptor plId)
50+
{ pluginCommands
51+
= fmap (\tc ->
52+
PluginCommand
53+
(tcCommandId tc)
54+
(tacticDesc $ tcCommandName tc)
55+
(tacticCmd $ commandTactic tc))
56+
enabledTactics
57+
, pluginCodeActionProvider = Just codeActionProvider
58+
}
59+
60+
tacticDesc :: T.Text -> T.Text
61+
tacticDesc name = "fill the hole using the " <> name <> " tactic"
62+
63+
------------------------------------------------------------------------------
64+
65+
enabledTactics :: [TacticCommand]
66+
enabledTactics = [Intros, Destruct, Homomorphism]
67+
68+
------------------------------------------------------------------------------
69+
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
70+
-- UI.
71+
type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
72+
73+
74+
------------------------------------------------------------------------------
75+
-- | Construct a 'CommandId'
76+
tcCommandId :: TacticCommand -> CommandId
77+
tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
78+
79+
80+
------------------------------------------------------------------------------
81+
-- | The name of the command for the LS.
82+
tcCommandName :: TacticCommand -> T.Text
83+
tcCommandName = T.pack . show
84+
85+
------------------------------------------------------------------------------
86+
-- | Mapping from tactic commands to their contextual providers. See 'provide',
87+
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
88+
commandProvider :: TacticCommand -> TacticProvider
89+
commandProvider Auto = provide Auto ""
90+
commandProvider Split = provide Split ""
91+
commandProvider Intro =
92+
filterGoalType isFunction $
93+
provide Intro ""
94+
commandProvider Intros =
95+
filterGoalType isFunction $
96+
provide Intros ""
97+
commandProvider Destruct =
98+
filterBindingType destructFilter $ \occ _ ->
99+
provide Destruct $ T.pack $ occNameString occ
100+
commandProvider Homomorphism =
101+
filterBindingType homoFilter $ \occ _ ->
102+
provide Homomorphism $ T.pack $ occNameString occ
103+
104+
105+
------------------------------------------------------------------------------
106+
-- | A mapping from tactic commands to actual tactics for refinery.
107+
commandTactic :: TacticCommand -> OccName -> TacticsM ()
108+
commandTactic Auto = const auto
109+
commandTactic Split = const split
110+
commandTactic Intro = const intro
111+
commandTactic Intros = const intros
112+
commandTactic Destruct = destruct
113+
commandTactic Homomorphism = homo
114+
115+
116+
------------------------------------------------------------------------------
117+
-- | We should show homos only when the goal type is the same as the binding
118+
-- type, and that both are usual algebraic types.
119+
homoFilter :: Type -> Type -> Bool
120+
homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
121+
homoFilter _ _ = False
122+
123+
124+
------------------------------------------------------------------------------
125+
-- | We should show destruct for bindings only when those bindings have usual
126+
-- algebraic types.
127+
destructFilter :: Type -> Type -> Bool
128+
destructFilter _ (algebraicTyCon -> Just _) = True
129+
destructFilter _ _ = False
130+
131+
132+
runIde :: IdeState -> Action a -> IO a
133+
runIde state = runAction "tactic" state
134+
135+
136+
codeActionProvider :: CodeActionProvider
137+
codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
138+
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
139+
fromMaybeT (Right $ List []) $ do
140+
(_, span, jdg) <- MaybeT $ judgementForHole state nfp range
141+
actions <- lift $
142+
-- This foldMap is over the function monoid.
143+
foldMap commandProvider enabledTactics
144+
plId
145+
uri
146+
span
147+
jdg
148+
pure $ Right $ List actions
149+
codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []
150+
151+
152+
codeActions :: [CodeAction] -> List CAResult
153+
codeActions = List . fmap CACodeAction
154+
155+
156+
------------------------------------------------------------------------------
157+
-- | Terminal constructor for providing context-sensitive tactics. Tactics
158+
-- given by 'provide' are always available.
159+
provide :: TacticCommand -> T.Text -> TacticProvider
160+
provide tc name plId uri range _ = do
161+
let title = tacticTitle tc name
162+
params = TacticParams { file = uri , range = range , var_name = name }
163+
cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
164+
pure
165+
$ pure
166+
$ CACodeAction
167+
$ CodeAction title (Just CodeActionQuickFix) Nothing Nothing
168+
$ Just cmd
169+
170+
171+
------------------------------------------------------------------------------
172+
-- | Restrict a 'TacticProvider', making sure it appears only when the given
173+
-- predicate holds for the goal.
174+
filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
175+
filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) =
176+
case p g of
177+
True -> tp plId uri range jdg
178+
False -> pure []
179+
180+
181+
------------------------------------------------------------------------------
182+
-- | Multiply a 'TacticProvider' for each binding, making sure it appears only
183+
-- when the given predicate holds over the goal and binding types.
184+
filterBindingType
185+
:: (Type -> Type -> Bool) -- ^ Goal and then binding types.
186+
-> (OccName -> Type -> TacticProvider)
187+
-> TacticProvider
188+
filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) =
189+
fmap join $ for (M.toList hys) $ \(occ, CType ty) ->
190+
case p g ty of
191+
True -> tp occ ty plId uri range jdg
192+
False -> pure []
193+
194+
195+
data TacticParams = TacticParams
196+
{ file :: Uri -- ^ Uri of the file to fill the hole in
197+
, range :: Range -- ^ The range of the hole
198+
, var_name :: T.Text
199+
}
200+
deriving (Show, Eq, Generic, ToJSON, FromJSON)
201+
202+
203+
------------------------------------------------------------------------------
204+
-- | Find the last typechecked module, and find the most specific span, as well
205+
-- as the judgement at the given range.
206+
judgementForHole
207+
:: IdeState
208+
-> NormalizedFilePath
209+
-> Range
210+
-> IO (Maybe (PositionMapping, Range, Judgement))
211+
judgementForHole state nfp range = runMaybeT $ do
212+
(asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp
213+
range' <- liftMaybe $ fromCurrentRange amapping range
214+
215+
(binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp
216+
217+
(rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast ->
218+
case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of
219+
Nothing -> Nothing
220+
Just ast' -> do
221+
let info = nodeInfo ast'
222+
ty <- listToMaybe $ nodeType info
223+
guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
224+
pure (nodeSpan ast', ty)
225+
226+
resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
227+
228+
let hyps = hypothesisFromBindings rss binds
229+
pure (amapping, resulting_range, Judgement hyps $ CType goal)
230+
231+
232+
tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
233+
tacticCmd tac lf state (TacticParams uri range var_name)
234+
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
235+
fromMaybeT (Right Null, Nothing) $ do
236+
(pos, _, jdg) <- MaybeT $ judgementForHole state nfp range
237+
-- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
238+
-- which don't change very often.
239+
(hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp
240+
let dflags = hsc_dflags $ hscEnv hscenv
241+
pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
242+
case runTactic jdg
243+
$ tac
244+
$ mkVarOcc
245+
$ T.unpack var_name of
246+
Left err ->
247+
pure $ (, Nothing)
248+
$ Left
249+
$ ResponseError InvalidRequest (T.pack $ show err) Nothing
250+
Right res -> do
251+
range' <- liftMaybe $ toCurrentRange pos range
252+
let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range'
253+
g = graft span res
254+
let response = transform dflags (clientCapabilities lf) uri g pm
255+
pure $ case response of
256+
Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
257+
Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
258+
tacticCmd _ _ _ _ =
259+
pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing
260+
, Nothing
261+
)
262+
263+
264+
fromMaybeT :: Functor m => a -> MaybeT m a -> m a
265+
fromMaybeT def = fmap (fromMaybe def) . runMaybeT
266+
267+
liftMaybe :: Monad m => Maybe a -> MaybeT m a
268+
liftMaybe a = MaybeT $ pure a
269+

0 commit comments

Comments
 (0)