Skip to content

Commit b91b3cd

Browse files
isovectormergify[bot]
isovector
and
mergify[bot]
authored
Tactic metaprogramming (#1776)
* Metaprogramming parser * Enable quasiquotes by default in ghcide * Install the Wingman tactic syntax in ghcide * Underscores are allowed in identifiers too * Test showing we can expand out tactics * Use a more concrete type for mkWingmanMetaprogram * Cleanup lexer * Use operator parsing for multiple tactics * Tidy the parser * Add 'obvious' tactic * Add intros', which lets you bind the names you want * Add intro to the parser * Add a modifyDynFlags field to plugins; push it into the parsed module * Modify dflags when typechecking too * Use the dynflags modifier to remove wingman specific code from ghcide * Move the staticplugin out of ghcide * Add application, add split, rename split to ctor * Tidy parser * Track remaining subgoals for interactive proofstate * Add a pretty printer of the proofstate * Add sorry * Attach proof state as a hover action * Much prettier proof state * Tidy and tag hover as markdown * Be smarter about where we run the dflags endo * Undo changes * Make Plugin accumulators robust to changing defs * Remove unused exts from Session * Reannotate the AST with tactic blocks * Tidy parser * MetaprogramSyntax and exact combinator * Add introduce metaprogram code action * Use noExtField * Appease Hlint * Compat for mkFunTys * Guard the static plugin * Static plugin doesn't even need to be here! * textSpaces doesn't exist in old versions of prettyprinter * Use a record for the result of judgmentForHole * Return the hole's occName * Add HoleSort; filter code actions by their holesort * Minor tidying * Better name for metaprogram holes * Use a record for DynFlags modifications * More hlint * Use modified dynflags for parser with comments * Allow running custom code blocks * Don't assume tactic providers use occnames * Revert changes to ghcide * Add tests * Feature gate * Restrict metaprograms to >=8.8 Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
1 parent 7d7cfa2 commit b91b3cd

28 files changed

+796
-71
lines changed

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

+9
Original file line numberDiff line numberDiff line change
@@ -44,9 +44,14 @@ library
4444
Wingman.KnownStrategies.QuickCheck
4545
Wingman.LanguageServer
4646
Wingman.LanguageServer.TacticProviders
47+
Wingman.LanguageServer.Metaprogram
4748
Wingman.Machinery
49+
Wingman.Metaprogramming.Lexer
50+
Wingman.Metaprogramming.Parser
51+
Wingman.Metaprogramming.ProofState
4852
Wingman.Naming
4953
Wingman.Plugin
54+
Wingman.StaticPlugin
5055
Wingman.Range
5156
Wingman.Simplify
5257
Wingman.Tactics
@@ -86,6 +91,9 @@ library
8691
, transformers
8792
, unordered-containers
8893
, hyphenation
94+
, megaparsec ^>=9
95+
, parser-combinators
96+
, prettyprinter
8997

9098
default-language: Haskell2010
9199
default-extensions:
@@ -123,6 +131,7 @@ test-suite tests
123131
CodeAction.DestructSpec
124132
CodeAction.IntrosSpec
125133
CodeAction.RefineSpec
134+
CodeAction.RunMetaprogramSpec
126135
CodeAction.UseDataConSpec
127136
CodeLens.EmptyCaseSpec
128137
ProviderSpec

‎plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs

+1
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ data Feature
2727
| FeatureKnownMonoid
2828
| FeatureEmptyCase
2929
| FeatureDestructPun
30+
| FeatureMetaprogram
3031
deriving (Eq, Ord, Show, Read, Enum, Bounded)
3132

3233

‎plugins/hls-tactics-plugin/src/Wingman/GHC.hs

+9
Original file line numberDiff line numberDiff line change
@@ -355,3 +355,12 @@ liftMaybe a = MaybeT $ pure a
355355
typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
356356
typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr
357357

358+
359+
mkFunTys' :: [Type] -> Type -> Type
360+
mkFunTys' =
361+
#if __GLASGOW_HASKELL__ <= 808
362+
mkFunTys
363+
#else
364+
mkVisFunTys
365+
#endif
366+

‎plugins/hls-tactics-plugin/src/Wingman/Judgements/SYB.hs

+15-6
Original file line numberDiff line numberDiff line change
@@ -4,12 +4,15 @@
44
-- | Custom SYB traversals
55
module Wingman.Judgements.SYB where
66

7-
import Data.Foldable (foldl')
8-
import Data.Generics hiding (typeRep)
9-
import Development.IDE.GHC.Compat
10-
import GHC.Exts (Any)
11-
import Type.Reflection
12-
import Unsafe.Coerce (unsafeCoerce)
7+
import Data.Foldable (foldl')
8+
import Data.Generics hiding (typeRep)
9+
import qualified Data.Text as T
10+
import Development.IDE.GHC.Compat
11+
import GHC.Exts (Any)
12+
import GhcPlugins (unpackFS)
13+
import Type.Reflection
14+
import Unsafe.Coerce (unsafeCoerce)
15+
import Wingman.StaticPlugin (pattern WingmanMetaprogram)
1316

1417

1518
------------------------------------------------------------------------------
@@ -81,3 +84,9 @@ sameTypeModuloLastApp =
8184
Nothing -> False
8285
_ -> False
8386

87+
88+
metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]
89+
metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case
90+
L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
91+
(_ :: LHsExpr GhcTc) -> mempty
92+

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

+66-15
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,18 @@ module Wingman.LanguageServer where
1010
import ConLike
1111
import Control.Arrow ((***))
1212
import Control.Monad
13-
import Control.Monad.State (State, get, put, evalState)
13+
import Control.Monad.IO.Class
14+
import Control.Monad.RWS
15+
import Control.Monad.State (State, evalState)
1416
import Control.Monad.Trans.Maybe
1517
import Data.Bifunctor (first)
1618
import Data.Coerce
1719
import Data.Functor ((<&>))
18-
import Data.Generics.Aliases (mkQ)
19-
import Data.Generics.Schemes (everything)
20+
import Data.Functor.Identity (runIdentity)
2021
import qualified Data.HashMap.Strict as Map
2122
import Data.IORef (readIORef)
2223
import qualified Data.Map as M
2324
import Data.Maybe
24-
import Data.Monoid
2525
import Data.Set (Set)
2626
import qualified Data.Set as S
2727
import qualified Data.Text as T
@@ -34,33 +34,38 @@ import Development.IDE.Core.Service (runAction)
3434
import Development.IDE.Core.Shake (IdeState (..), uses, define, use)
3535
import qualified Development.IDE.Core.Shake as IDE
3636
import Development.IDE.Core.UseStale
37-
import Development.IDE.GHC.Compat
37+
import Development.IDE.GHC.Compat hiding (parseExpr)
3838
import Development.IDE.GHC.Error (realSrcSpanToRange)
3939
import Development.IDE.GHC.ExactPrint
40-
import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
4140
import Development.IDE.Graph (Action, RuleResult, Rules, action)
42-
import Development.IDE.Graph.Classes (Typeable, Binary, Hashable, NFData)
41+
import Development.IDE.Graph.Classes (Binary, Hashable, NFData)
42+
import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
4343
import qualified FastString
4444
import GHC.Generics (Generic)
45-
import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)
45+
import Generics.SYB hiding (Generic)
46+
import GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
4647
import qualified Ide.Plugin.Config as Plugin
4748
import Ide.Plugin.Properties
4849
import Ide.PluginUtils (usePropertyLsp)
4950
import Ide.Types (PluginId)
51+
import Language.Haskell.GHC.ExactPrint (Transform)
52+
import Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
5053
import Language.LSP.Server (MonadLsp, sendNotification)
5154
import Language.LSP.Types
5255
import Language.LSP.Types.Capabilities
5356
import OccName
5457
import Prelude hiding (span)
58+
import Retrie (transformA)
5559
import SrcLoc (containsSpan)
5660
import TcRnTypes (tcg_binds, TcGblEnv)
5761
import Wingman.Context
5862
import Wingman.FeatureSet
5963
import Wingman.GHC
6064
import Wingman.Judgements
61-
import Wingman.Judgements.SYB (everythingContaining)
65+
import Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
6266
import Wingman.Judgements.Theta
6367
import Wingman.Range
68+
import Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
6469
import Wingman.Types
6570

6671

@@ -178,6 +183,11 @@ getIdeDynflags state nfp = do
178183
msr <- unsafeRunStaleIde "getIdeDynflags" state nfp GetModSummaryWithoutTimestamps
179184
pure $ ms_hspp_opts $ msrModSummary msr
180185

186+
getAllMetaprograms :: Data a => a -> [String]
187+
getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
188+
WingmanMetaprogram fs -> [ unpackFS fs ]
189+
(_ :: HsExpr GhcTc) -> mempty
190+
181191

182192
------------------------------------------------------------------------------
183193
-- | Find the last typechecked module, and find the most specific span, as well
@@ -187,7 +197,7 @@ judgementForHole
187197
-> NormalizedFilePath
188198
-> Tracked 'Current Range
189199
-> Config
190-
-> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
200+
-> MaybeT IO HoleJudgment
191201
judgementForHole state nfp range cfg = do
192202
let stale a = runStaleIde "judgementForHole" state nfp a
193203

@@ -197,12 +207,16 @@ judgementForHole state nfp range cfg = do
197207
HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do
198208
range' <- liftMaybe $ mapAgeFrom amapping range
199209
binds <- stale GetBindings
200-
tcg <- fmap (fmap tmrTypechecked)
210+
tcg@(TrackedStale tcg_t tcg_map)
211+
<- fmap (fmap tmrTypechecked)
201212
$ stale TypeCheck
213+
202214
hscenv <- stale GhcSessionDeps
203215

204216
(rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
217+
205218
new_rss <- liftMaybe $ mapAgeTo amapping rss
219+
tcg_rss <- liftMaybe $ mapAgeFrom tcg_map new_rss
206220

207221
-- KnownThings is just the instances in scope. There are no ranges
208222
-- involved, so it's not crucial to track ages.
@@ -211,10 +225,20 @@ judgementForHole state nfp range cfg = do
211225
kt <- knownThings (untrackedStaleValue tcg) henv
212226

213227
(jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
228+
let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t
214229

215230
dflags <- getIdeDynflags state nfp
216-
pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
231+
pure $ HoleJudgment
232+
{ hj_range = fmap realSrcSpanToRange new_rss
233+
, hj_jdg = jdg
234+
, hj_ctx = ctx
235+
, hj_dflags = dflags
236+
, hj_hole_sort = holeSortFor mp
237+
}
238+
217239

240+
holeSortFor :: Maybe T.Text -> HoleSort
241+
holeSortFor = maybe Hole Metaprogram
218242

219243

220244
mkJudgementAndContext
@@ -285,8 +309,12 @@ getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
285309
ty <- listToMaybe $ nodeType info
286310
guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
287311
-- Ensure we're actually looking at a hole here
288-
guard $ all (either (const False) $ isHole . occName)
289-
$ M.keysSet $ nodeIdentifiers info
312+
occ <- (either (const Nothing) (Just . occName) =<<)
313+
. listToMaybe
314+
. S.toList
315+
. M.keysSet
316+
$ nodeIdentifiers info
317+
guard $ isHole occ
290318
pure (unsafeCopyAge r $ nodeSpan ast', ty)
291319

292320

@@ -543,5 +571,28 @@ mkWorkspaceEdits
543571
-> Graft (Either String) ParsedSource
544572
-> Either UserFacingMessage WorkspaceEdit
545573
mkWorkspaceEdits dflags ccs uri pm g = do
546-
let response = transform dflags ccs uri g pm
574+
let pm' = runIdentity $ transformA pm annotateMetaprograms
575+
let response = transform dflags ccs uri g pm'
547576
in first (InfrastructureError . T.pack) response
577+
578+
579+
annotateMetaprograms :: Data a => a -> Transform a
580+
annotateMetaprograms = everywhereM $ mkM $ \case
581+
L ss (WingmanMetaprogram mp) -> do
582+
let x = L ss $ MetaprogramSyntax mp
583+
let anns = addAnnotationsForPretty [] x mempty
584+
modifyAnnsT $ mappend anns
585+
pure x
586+
(x :: LHsExpr GhcPs) -> pure x
587+
588+
getMetaprogramAtSpan
589+
:: Tracked age SrcSpan
590+
-> Tracked age TcGblEnv
591+
-> Maybe T.Text
592+
getMetaprogramAtSpan (unTrack -> ss)
593+
= fmap snd
594+
. listToMaybe
595+
. metaprogramQ ss
596+
. tcg_binds
597+
. unTrack
598+

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs

+90
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
{-# LANGUAGE DuplicateRecordFields #-}
2+
{-# LANGUAGE OverloadedStrings #-}
3+
4+
{-# LANGUAGE NoMonoLocalBinds #-}
5+
{-# LANGUAGE RankNTypes #-}
6+
7+
module Wingman.LanguageServer.Metaprogram
8+
( hoverProvider
9+
) where
10+
11+
import Control.Applicative (empty)
12+
import Control.Monad
13+
import Control.Monad.Trans
14+
import Control.Monad.Trans.Maybe
15+
import Data.List (find)
16+
import Data.Maybe
17+
import qualified Data.Text as T
18+
import Data.Traversable
19+
import Development.IDE (positionToRealSrcLoc)
20+
import Development.IDE (realSrcSpanToRange)
21+
import Development.IDE.Core.RuleTypes
22+
import Development.IDE.Core.Shake (IdeState (..))
23+
import Development.IDE.Core.UseStale
24+
import Development.IDE.GHC.Compat
25+
import GhcPlugins (containsSpan, realSrcLocSpan)
26+
import Ide.Types
27+
import Language.LSP.Types
28+
import Prelude hiding (span)
29+
import Prelude hiding (span)
30+
import TcRnTypes (tcg_binds)
31+
import Wingman.GHC
32+
import Wingman.Judgements.SYB (metaprogramQ)
33+
import Wingman.Metaprogramming.Parser (attempt_it)
34+
import Wingman.LanguageServer
35+
import Wingman.Types
36+
37+
38+
------------------------------------------------------------------------------
39+
-- | Provide the "empty case completion" code lens
40+
hoverProvider :: PluginMethodHandler IdeState TextDocumentHover
41+
hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurrent -> pos) _)
42+
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
43+
let loc = fmap (realSrcLocSpan . positionToRealSrcLoc nfp) pos
44+
45+
cfg <- getTacticConfig plId
46+
liftIO $ fromMaybeT (Right Nothing) $ do
47+
-- guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
48+
49+
holes <- getMetaprogramsAtSpan state nfp $ RealSrcSpan $ unTrack loc
50+
51+
fmap (Right . Just) $
52+
case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
53+
Just (trss, program) -> do
54+
let tr_range = fmap realSrcSpanToRange trss
55+
HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
56+
pure $ Hover
57+
{ _contents = HoverContents
58+
$ MarkupContent MkMarkdown
59+
$ either T.pack T.pack
60+
$ attempt_it ctx jdg
61+
$ T.unpack program
62+
, _range = Just $ unTrack tr_range
63+
}
64+
Nothing -> empty
65+
hoverProvider _ _ _ = pure $ Right Nothing
66+
67+
68+
fromMaybeT :: Functor m => a -> MaybeT m a -> m a
69+
fromMaybeT def = fmap (fromMaybe def) . runMaybeT
70+
71+
72+
getMetaprogramsAtSpan
73+
:: IdeState
74+
-> NormalizedFilePath
75+
-> SrcSpan
76+
-> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]
77+
getMetaprogramsAtSpan state nfp ss = do
78+
let stale a = runStaleIde "getMetaprogramsAtSpan" state nfp a
79+
80+
TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck
81+
82+
let scrutinees = traverse (metaprogramQ ss . tcg_binds) tcg
83+
for scrutinees $ \aged@(unTrack -> (ss, program)) -> do
84+
case ss of
85+
RealSrcSpan r -> do
86+
rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
87+
pure (rss', program)
88+
UnhelpfulSpan _ -> empty
89+
90+

0 commit comments

Comments
 (0)