Skip to content

Commit dc0966e

Browse files
authored
Merge branch 'master' into optionalProgressReporting
2 parents 132a6f3 + 00c954d commit dc0966e

33 files changed

+475
-523
lines changed

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

Lines changed: 45 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -25,29 +25,30 @@ library
2525
hs-source-dirs: src
2626
exposed-modules:
2727
Ide.Plugin.Tactic
28-
Ide.Plugin.Tactic.Auto
29-
Ide.Plugin.Tactic.CaseSplit
30-
Ide.Plugin.Tactic.CodeGen
31-
Ide.Plugin.Tactic.CodeGen.Utils
32-
Ide.Plugin.Tactic.Context
33-
Ide.Plugin.Tactic.Debug
34-
Ide.Plugin.Tactic.FeatureSet
35-
Ide.Plugin.Tactic.GHC
36-
Ide.Plugin.Tactic.Judgements
37-
Ide.Plugin.Tactic.Judgements.Theta
38-
Ide.Plugin.Tactic.KnownStrategies
39-
Ide.Plugin.Tactic.KnownStrategies.QuickCheck
40-
Ide.Plugin.Tactic.LanguageServer
41-
Ide.Plugin.Tactic.LanguageServer.TacticProviders
42-
Ide.Plugin.Tactic.Machinery
43-
Ide.Plugin.Tactic.Naming
44-
Ide.Plugin.Tactic.Range
45-
Ide.Plugin.Tactic.Simplify
46-
Ide.Plugin.Tactic.Tactics
47-
Ide.Plugin.Tactic.Types
28+
Wingman.Auto
29+
Wingman.CaseSplit
30+
Wingman.CodeGen
31+
Wingman.CodeGen.Utils
32+
Wingman.Context
33+
Wingman.Debug
34+
Wingman.FeatureSet
35+
Wingman.GHC
36+
Wingman.Judgements
37+
Wingman.Judgements.Theta
38+
Wingman.KnownStrategies
39+
Wingman.KnownStrategies.QuickCheck
40+
Wingman.LanguageServer
41+
Wingman.LanguageServer.TacticProviders
42+
Wingman.Machinery
43+
Wingman.Naming
44+
Wingman.Plugin
45+
Wingman.Range
46+
Wingman.Simplify
47+
Wingman.Tactics
48+
Wingman.Types
4849

4950
ghc-options:
50-
-Wno-name-shadowing -Wredundant-constraints -Wno-unticked-promoted-constructors
51+
-Wall -Wno-name-shadowing -Wredundant-constraints -Wno-unticked-promoted-constructors
5152
if flag(pedantic)
5253
ghc-options: -Werror
5354

@@ -78,7 +79,29 @@ library
7879
, deepseq
7980

8081
default-language: Haskell2010
81-
default-extensions: DataKinds, TypeOperators
82+
default-extensions:
83+
DataKinds,
84+
DeriveAnyClass,
85+
DeriveFunctor,
86+
DeriveGeneric,
87+
DeriveDataTypeable,
88+
DeriveFoldable,
89+
DeriveTraversable,
90+
DerivingStrategies,
91+
DerivingVia,
92+
FlexibleContexts,
93+
FlexibleInstances,
94+
GADTs,
95+
GeneralizedNewtypeDeriving,
96+
LambdaCase,
97+
MultiParamTypeClasses,
98+
NumDecimals,
99+
OverloadedLabels,
100+
PatternSynonyms,
101+
ScopedTypeVariables,
102+
TypeApplications,
103+
TypeOperators,
104+
ViewPatterns
82105

83106

84107
executable test-server
Lines changed: 1 addition & 269 deletions
Original file line numberDiff line numberDiff line change
@@ -1,277 +1,9 @@
1-
{-# LANGUAGE FlexibleContexts #-}
2-
{-# LANGUAGE GADTs #-}
3-
{-# LANGUAGE LambdaCase #-}
4-
{-# LANGUAGE NumDecimals #-}
5-
{-# LANGUAGE OverloadedStrings #-}
6-
{-# LANGUAGE ScopedTypeVariables #-}
7-
{-# LANGUAGE TypeApplications #-}
8-
91
-- | A plugin that uses tactics to synthesize code
102
module Ide.Plugin.Tactic
113
( descriptor
124
, tacticTitle
135
, TacticCommand (..)
146
) where
157

16-
import Bag (bagToList, listToBag)
17-
import Control.Exception (evaluate)
18-
import Control.Monad
19-
import Control.Monad.Trans
20-
import Control.Monad.Trans.Maybe
21-
import Data.Aeson
22-
import Data.Bifunctor (first)
23-
import Data.Data (Data)
24-
import Data.Foldable (for_)
25-
import Data.Generics.Aliases (mkQ)
26-
import Data.Generics.Schemes (everything)
27-
import Data.Maybe
28-
import Data.Monoid
29-
import qualified Data.Text as T
30-
import Data.Traversable
31-
import Development.IDE.Core.Shake (IdeState (..))
32-
import Development.IDE.GHC.Compat
33-
import Development.IDE.GHC.ExactPrint
34-
import Ide.Plugin.Tactic.CaseSplit
35-
import Ide.Plugin.Tactic.GHC
36-
import Ide.Plugin.Tactic.LanguageServer
37-
import Ide.Plugin.Tactic.LanguageServer.TacticProviders
38-
import Ide.Plugin.Tactic.Range
39-
import Ide.Plugin.Tactic.Tactics
40-
import Ide.Plugin.Tactic.Types
41-
import Ide.Types
42-
import Language.LSP.Server
43-
import Language.LSP.Types
44-
import Language.LSP.Types.Capabilities
45-
import OccName
46-
import Prelude hiding (span)
47-
import System.Timeout
48-
49-
50-
descriptor :: PluginId -> PluginDescriptor IdeState
51-
descriptor plId = (defaultPluginDescriptor plId)
52-
{ pluginCommands
53-
= fmap (\tc ->
54-
PluginCommand
55-
(tcCommandId tc)
56-
(tacticDesc $ tcCommandName tc)
57-
(tacticCmd $ commandTactic tc))
58-
[minBound .. maxBound]
59-
, pluginHandlers =
60-
mkPluginHandler STextDocumentCodeAction codeActionProvider
61-
}
62-
63-
64-
65-
codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
66-
codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
67-
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
68-
cfg <- getTacticConfig $ shakeExtras state
69-
liftIO $ fromMaybeT (Right $ List []) $ do
70-
(_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
71-
actions <- lift $
72-
-- This foldMap is over the function monoid.
73-
foldMap commandProvider [minBound .. maxBound]
74-
dflags
75-
cfg
76-
plId
77-
uri
78-
range
79-
jdg
80-
pure $ Right $ List actions
81-
codeActionProvider _ _ _ = pure $ Right $ List []
82-
83-
84-
showUserFacingMessage
85-
:: MonadLsp cfg m
86-
=> UserFacingMessage
87-
-> m (Either ResponseError a)
88-
showUserFacingMessage ufm = do
89-
showLspMessage $ mkShowMessageParams ufm
90-
pure $ Left $ mkErr InternalError $ T.pack $ show ufm
91-
92-
93-
tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
94-
tacticCmd tac state (TacticParams uri range var_name)
95-
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
96-
features <- getFeatureSet $ shakeExtras state
97-
ccs <- getClientCapabilities
98-
res <- liftIO $ runMaybeT $ do
99-
(range', jdg, ctx, dflags) <- judgementForHole state nfp range features
100-
let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
101-
pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
102-
103-
timingOut 2e8 $ join $
104-
case runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name of
105-
Left _ -> Left TacticErrors
106-
Right rtr ->
107-
case rtr_extract rtr of
108-
L _ (HsVar _ (L _ rdr)) | isHole (occName rdr) ->
109-
Left NothingToDo
110-
_ -> pure $ mkWorkspaceEdits span dflags ccs uri pm rtr
111-
112-
case res of
113-
Nothing -> do
114-
showUserFacingMessage TimedOut
115-
Just (Left ufm) -> do
116-
showUserFacingMessage ufm
117-
Just (Right edit) -> do
118-
sendRequest
119-
SWorkspaceApplyEdit
120-
(ApplyWorkspaceEditParams Nothing edit)
121-
(const $ pure ())
122-
pure $ Right Null
123-
tacticCmd _ _ _ =
124-
pure $ Left $ mkErr InvalidRequest "Bad URI"
125-
126-
127-
timingOut
128-
:: Int -- ^ Time in microseconds
129-
-> a -- ^ Computation to run
130-
-> MaybeT IO a
131-
timingOut t m = MaybeT $ timeout t $ evaluate m
132-
133-
134-
mkErr :: ErrorCode -> T.Text -> ResponseError
135-
mkErr code err = ResponseError code err Nothing
136-
137-
138-
joinNote :: e -> Maybe (Either e a) -> Either e a
139-
joinNote e Nothing = Left e
140-
joinNote _ (Just a) = a
141-
142-
143-
------------------------------------------------------------------------------
144-
-- | Turn a 'RunTacticResults' into concrete edits to make in the source
145-
-- document.
146-
mkWorkspaceEdits
147-
:: RealSrcSpan
148-
-> DynFlags
149-
-> ClientCapabilities
150-
-> Uri
151-
-> Annotated ParsedSource
152-
-> RunTacticResults
153-
-> Either UserFacingMessage WorkspaceEdit
154-
mkWorkspaceEdits span dflags ccs uri pm rtr = do
155-
for_ (rtr_other_solns rtr) $ traceMX "other solution"
156-
traceMX "solution" $ rtr_extract rtr
157-
let g = graftHole (RealSrcSpan span) rtr
158-
response = transform dflags ccs uri g pm
159-
in first (InfrastructureError . T.pack) response
160-
161-
162-
------------------------------------------------------------------------------
163-
-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly
164-
-- deals with top-level holes, in which we might need to fiddle with the
165-
-- 'Match's that bind variables.
166-
graftHole
167-
:: SrcSpan
168-
-> RunTacticResults
169-
-> Graft (Either String) ParsedSource
170-
graftHole span rtr
171-
| _jIsTopHole (rtr_jdg rtr)
172-
= graftSmallestDeclsWithM span
173-
$ graftDecl span $ \pats ->
174-
splitToDecl (fst $ last $ ctxDefiningFuncs $ rtr_ctx rtr)
175-
$ iterateSplit
176-
$ mkFirstAgda (fmap unXPat pats)
177-
$ unLoc
178-
$ rtr_extract rtr
179-
graftHole span rtr
180-
= graft span
181-
$ rtr_extract rtr
182-
183-
184-
------------------------------------------------------------------------------
185-
-- | Merge in the 'Match'es of a 'FunBind' into a 'HsDecl'. Used to perform
186-
-- agda-style case splitting in which we need to separate one 'Match' into
187-
-- many, without affecting any matches which might exist but don't need to be
188-
-- split.
189-
mergeFunBindMatches
190-
:: ([Pat GhcPs] -> LHsDecl GhcPs)
191-
-> SrcSpan
192-
-> HsBind GhcPs
193-
-> Either String (HsBind GhcPs)
194-
mergeFunBindMatches make_decl span
195-
(fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =
196-
pure $ fb
197-
{ fun_matches = mg
198-
{ mg_alts = L alts_src $ do
199-
alt@(L alt_src match) <- alts
200-
case span `isSubspanOf` alt_src of
201-
True -> do
202-
let pats = fmap fromPatCompatPs $ m_pats match
203-
L _ (ValD _ (FunBind {fun_matches = MG
204-
{mg_alts = L _ to_add}})) = make_decl pats
205-
to_add
206-
False -> pure alt
207-
}
208-
}
209-
mergeFunBindMatches _ _ _ =
210-
Left "mergeFunBindMatches: called on something that isnt a funbind"
211-
212-
213-
throwError :: String -> TransformT (Either String) a
214-
throwError = lift . Left
215-
216-
217-
------------------------------------------------------------------------------
218-
-- | Helper function to route 'mergeFunBindMatches' into the right place in an
219-
-- AST --- correctly dealing with inserting into instance declarations.
220-
graftDecl
221-
:: SrcSpan
222-
-> ([Pat GhcPs] -> LHsDecl GhcPs)
223-
-> LHsDecl GhcPs
224-
-> TransformT (Either String) (Maybe [LHsDecl GhcPs])
225-
graftDecl span
226-
make_decl
227-
(L src (ValD ext fb))
228-
= either throwError (pure . Just . pure . L src . ValD ext) $
229-
mergeFunBindMatches make_decl span fb
230-
-- TODO(sandy): add another case for default methods in class definitions
231-
graftDecl span
232-
make_decl
233-
(L src (InstD ext
234-
cid@ClsInstD{cid_inst =
235-
cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))
236-
= do
237-
binds' <-
238-
for (bagToList binds) $ \b@(L bsrc bind) -> do
239-
case bind of
240-
fb@FunBind{} | span `isSubspanOf` bsrc ->
241-
either throwError (pure . L bsrc) $
242-
mergeFunBindMatches make_decl span fb
243-
_ -> pure b
244-
245-
pure $ Just $ pure $ L src $ InstD ext $ cid
246-
{ cid_inst = cidi
247-
{ cid_binds = listToBag binds'
248-
}
249-
}
250-
graftDecl span _ x = do
251-
traceMX "biggest" $
252-
unsafeRender $
253-
locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x
254-
traceMX "first" $
255-
unsafeRender $
256-
locateFirst @(Match GhcPs (LHsExpr GhcPs)) x
257-
throwError "graftDecl: don't know about this AST form"
258-
259-
260-
fromMaybeT :: Functor m => a -> MaybeT m a -> m a
261-
fromMaybeT def = fmap (fromMaybe def) . runMaybeT
262-
263-
264-
locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r
265-
locateBiggest ss x = getFirst $ everything (<>)
266-
( mkQ mempty $ \case
267-
L span r | ss `isSubspanOf` span -> pure r
268-
_ -> mempty
269-
) x
270-
271-
272-
locateFirst :: (Data r, Data a) => a -> Maybe r
273-
locateFirst x = getFirst $ everything (<>)
274-
( mkQ mempty $ \case
275-
r -> pure r
276-
) x
8+
import Wingman.Plugin
2779

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Auto.hs renamed to plugins/hls-tactics-plugin/src/Wingman/Auto.hs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
1-
module Ide.Plugin.Tactic.Auto where
1+
module Wingman.Auto where
22

3-
import Control.Monad.State (gets)
4-
import Ide.Plugin.Tactic.Context
5-
import Ide.Plugin.Tactic.Judgements
6-
import Ide.Plugin.Tactic.KnownStrategies
7-
import Ide.Plugin.Tactic.Machinery (tracing)
8-
import Ide.Plugin.Tactic.Tactics
9-
import Ide.Plugin.Tactic.Types
3+
import Control.Monad.State (gets)
104
import Refinery.Tactic
5+
import Wingman.Context
6+
import Wingman.Judgements
7+
import Wingman.KnownStrategies
8+
import Wingman.Machinery (tracing)
9+
import Wingman.Tactics
10+
import Wingman.Types
1111

1212

1313
------------------------------------------------------------------------------

0 commit comments

Comments
 (0)