Tactic metaprogramming

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

@@ -44,9 +44,14 @@ library
     Wingman.KnownStrategies.QuickCheck
     Wingman.LanguageServer
     Wingman.LanguageServer.TacticProviders
+    Wingman.LanguageServer.Metaprogram
     Wingman.Machinery
+    Wingman.Metaprogramming.Lexer
+    Wingman.Metaprogramming.Parser
+    Wingman.Metaprogramming.ProofState
     Wingman.Naming
     Wingman.Plugin
+    Wingman.StaticPlugin
     Wingman.Range
     Wingman.Simplify
     Wingman.Tactics
@@ -86,6 +91,9 @@ library
     , transformers
     , unordered-containers
     , hyphenation
+    , megaparsec ^>=9
+    , parser-combinators
+    , prettyprinter
 
   default-language:   Haskell2010
   default-extensions:
@@ -123,6 +131,7 @@ test-suite tests
     CodeAction.DestructSpec
     CodeAction.IntrosSpec
     CodeAction.RefineSpec
+    CodeAction.RunMetaprogramSpec
     CodeAction.UseDataConSpec
     CodeLens.EmptyCaseSpec
     ProviderSpec

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

@@ -27,6 +27,7 @@ data Feature
   | FeatureKnownMonoid
   | FeatureEmptyCase
   | FeatureDestructPun
+  | FeatureMetaprogram
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 

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

@@ -355,3 +355,12 @@ liftMaybe a = MaybeT $ pure a
 typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
 typeCheck hscenv tcg = fmap snd . initDs hscenv tcg . fmap exprType . dsExpr
 
+
+mkFunTys' :: [Type] -> Type -> Type
+mkFunTys' =
+#if __GLASGOW_HASKELL__ <= 808
+  mkFunTys
+#else
+  mkVisFunTys
+#endif
+

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

@@ -4,12 +4,15 @@
 -- | Custom SYB traversals
 module Wingman.Judgements.SYB where
 
-import Data.Foldable (foldl')
-import Data.Generics hiding (typeRep)
-import Development.IDE.GHC.Compat
-import GHC.Exts (Any)
-import Type.Reflection
-import Unsafe.Coerce (unsafeCoerce)
+import           Data.Foldable (foldl')
+import           Data.Generics hiding (typeRep)
+import qualified Data.Text as T
+import           Development.IDE.GHC.Compat
+import           GHC.Exts (Any)
+import           GhcPlugins (unpackFS)
+import           Type.Reflection
+import           Unsafe.Coerce (unsafeCoerce)
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram)
 
 
 ------------------------------------------------------------------------------
@@ -81,3 +84,9 @@ sameTypeModuloLastApp =
             Nothing    -> False
         _ -> False
 
+
+metaprogramQ :: SrcSpan -> GenericQ [(SrcSpan, T.Text)]
+metaprogramQ ss = everythingContaining ss $ mkQ mempty $ \case
+  L new_span (WingmanMetaprogram program) -> pure (new_span, T.pack $ unpackFS $ program)
+  (_ :: LHsExpr GhcTc) -> mempty
+

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

@@ -10,18 +10,18 @@ module Wingman.LanguageServer where
 import           ConLike
 import           Control.Arrow ((***))
 import           Control.Monad
-import           Control.Monad.State (State, get, put, evalState)
+import           Control.Monad.IO.Class
+import           Control.Monad.RWS
+import           Control.Monad.State (State, evalState)
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (first)
 import           Data.Coerce
 import           Data.Functor ((<&>))
-import           Data.Generics.Aliases (mkQ)
-import           Data.Generics.Schemes (everything)
+import           Data.Functor.Identity (runIdentity)
 import qualified Data.HashMap.Strict as Map
 import           Data.IORef (readIORef)
 import qualified Data.Map as M
 import           Data.Maybe
-import           Data.Monoid
 import           Data.Set (Set)
 import qualified Data.Set as S
 import qualified Data.Text as T
@@ -34,33 +34,38 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (IdeState (..), uses, define, use)
 import qualified Development.IDE.Core.Shake as IDE
 import           Development.IDE.Core.UseStale
-import           Development.IDE.GHC.Compat
+import           Development.IDE.GHC.Compat hiding (parseExpr)
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
 import           Development.IDE.GHC.ExactPrint
-import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
 import           Development.IDE.Graph (Action, RuleResult, Rules, action)
-import           Development.IDE.Graph.Classes (Typeable, Binary, Hashable, NFData)
+import           Development.IDE.Graph.Classes (Binary, Hashable, NFData)
+import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
 import qualified FastString
 import           GHC.Generics (Generic)
-import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)
+import           Generics.SYB hiding (Generic)
+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
 import           Ide.PluginUtils (usePropertyLsp)
 import           Ide.Types (PluginId)
+import           Language.Haskell.GHC.ExactPrint (Transform)
+import           Language.Haskell.GHC.ExactPrint (modifyAnnsT, addAnnotationsForPretty)
 import           Language.LSP.Server (MonadLsp, sendNotification)
 import           Language.LSP.Types
 import           Language.LSP.Types.Capabilities
 import           OccName
 import           Prelude hiding (span)
+import           Retrie (transformA)
 import           SrcLoc (containsSpan)
 import           TcRnTypes (tcg_binds, TcGblEnv)
 import           Wingman.Context
 import           Wingman.FeatureSet
 import           Wingman.GHC
 import           Wingman.Judgements
-import           Wingman.Judgements.SYB (everythingContaining)
+import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
 import           Wingman.Judgements.Theta
 import           Wingman.Range
+import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
 import           Wingman.Types
 
 
@@ -178,6 +183,11 @@ getIdeDynflags state nfp = do
   msr <- unsafeRunStaleIde "getIdeDynflags" state nfp GetModSummaryWithoutTimestamps
   pure $ ms_hspp_opts $ msrModSummary msr
 
+getAllMetaprograms :: Data a => a -> [String]
+getAllMetaprograms = everything (<>) $ mkQ mempty $ \case
+  WingmanMetaprogram fs -> [ unpackFS fs ]
+  (_ :: HsExpr GhcTc)  -> mempty
+
 
 ------------------------------------------------------------------------------
 -- | Find the last typechecked module, and find the most specific span, as well
@@ -187,7 +197,7 @@ judgementForHole
     -> NormalizedFilePath
     -> Tracked 'Current Range
     -> Config
-    -> MaybeT IO (Tracked 'Current Range, Judgement, Context, DynFlags)
+    -> MaybeT IO HoleJudgment
 judgementForHole state nfp range cfg = do
   let stale a = runStaleIde "judgementForHole" state nfp a
 
@@ -197,12 +207,16 @@ judgementForHole state nfp range cfg = do
     HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do
       range' <- liftMaybe $ mapAgeFrom amapping range
       binds <- stale GetBindings
-      tcg <- fmap (fmap tmrTypechecked)
+      tcg@(TrackedStale tcg_t tcg_map)
+          <- fmap (fmap tmrTypechecked)
            $ stale TypeCheck
+
       hscenv <- stale GhcSessionDeps
 
       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
+
       new_rss <- liftMaybe $ mapAgeTo amapping rss
+      tcg_rss <- liftMaybe $ mapAgeFrom tcg_map new_rss
 
       -- KnownThings is just the instances in scope. There are no ranges
       -- involved, so it's not crucial to track ages.
@@ -211,10 +225,20 @@ judgementForHole state nfp range cfg = do
       kt <- knownThings (untrackedStaleValue tcg) henv
 
       (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
+      let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t
 
       dflags <- getIdeDynflags state nfp
-      pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
+      pure $ HoleJudgment
+        { hj_range = fmap realSrcSpanToRange new_rss
+        , hj_jdg = jdg
+        , hj_ctx = ctx
+        , hj_dflags = dflags
+        , hj_hole_sort = holeSortFor mp
+        }
+
 
+holeSortFor :: Maybe T.Text -> HoleSort
+holeSortFor = maybe Hole Metaprogram
 
 
 mkJudgementAndContext
@@ -285,8 +309,12 @@ getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
         ty <- listToMaybe $ nodeType info
         guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
         -- Ensure we're actually looking at a hole here
-        guard $ all (either (const False) $ isHole . occName)
-          $ M.keysSet $ nodeIdentifiers info
+        occ <- (either (const Nothing) (Just . occName) =<<)
+             . listToMaybe
+             . S.toList
+             . M.keysSet
+             $ nodeIdentifiers info
+        guard $ isHole occ
         pure (unsafeCopyAge r $ nodeSpan ast', ty)
 
 
@@ -543,5 +571,28 @@ mkWorkspaceEdits
     -> Graft (Either String) ParsedSource
     -> Either UserFacingMessage WorkspaceEdit
 mkWorkspaceEdits dflags ccs uri pm g = do
-  let response = transform dflags ccs uri g pm
+  let pm' = runIdentity $ transformA pm annotateMetaprograms
+  let response = transform dflags ccs uri g pm'
    in first (InfrastructureError . T.pack) response
+
+
+annotateMetaprograms :: Data a => a -> Transform a
+annotateMetaprograms = everywhereM $ mkM $ \case
+  L ss (WingmanMetaprogram mp) -> do
+    let x = L ss $ MetaprogramSyntax mp
+    let anns = addAnnotationsForPretty [] x mempty
+    modifyAnnsT $ mappend anns
+    pure x
+  (x :: LHsExpr GhcPs) -> pure x
+
+getMetaprogramAtSpan
+    :: Tracked age SrcSpan
+    -> Tracked age TcGblEnv
+    -> Maybe T.Text
+getMetaprogramAtSpan (unTrack -> ss)
+  = fmap snd
+  . listToMaybe
+  . metaprogramQ ss
+  . tcg_binds
+  . unTrack
+

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

@@ -0,0 +1,90 @@
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedStrings     #-}
+
+{-# LANGUAGE NoMonoLocalBinds  #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Wingman.LanguageServer.Metaprogram
+  ( hoverProvider
+  ) where
+
+import           Control.Applicative (empty)
+import           Control.Monad
+import           Control.Monad.Trans
+import           Control.Monad.Trans.Maybe
+import           Data.List (find)
+import           Data.Maybe
+import qualified Data.Text as T
+import           Data.Traversable
+import           Development.IDE (positionToRealSrcLoc)
+import           Development.IDE (realSrcSpanToRange)
+import           Development.IDE.Core.RuleTypes
+import           Development.IDE.Core.Shake (IdeState (..))
+import           Development.IDE.Core.UseStale
+import           Development.IDE.GHC.Compat
+import           GhcPlugins (containsSpan, realSrcLocSpan)
+import           Ide.Types
+import           Language.LSP.Types
+import           Prelude hiding (span)
+import           Prelude hiding (span)
+import           TcRnTypes (tcg_binds)
+import           Wingman.GHC
+import           Wingman.Judgements.SYB (metaprogramQ)
+import           Wingman.Metaprogramming.Parser (attempt_it)
+import           Wingman.LanguageServer
+import           Wingman.Types
+
+
+------------------------------------------------------------------------------
+-- | Provide the "empty case completion" code lens
+hoverProvider :: PluginMethodHandler IdeState TextDocumentHover
+hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurrent -> pos) _)
+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      let loc = fmap (realSrcLocSpan . positionToRealSrcLoc nfp) pos
+
+      cfg <- getTacticConfig plId
+      liftIO $ fromMaybeT (Right Nothing) $ do
+        -- guard $ hasFeature FeatureEmptyCase $ cfg_feature_set cfg
+
+        holes <- getMetaprogramsAtSpan state nfp $ RealSrcSpan $ unTrack loc
+
+        fmap (Right . Just) $
+          case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
+            Just (trss, program) -> do
+              let tr_range = fmap realSrcSpanToRange trss
+              HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
+              pure $ Hover
+                { _contents = HoverContents
+                            $ MarkupContent MkMarkdown
+                            $ either T.pack T.pack
+                            $ attempt_it ctx jdg
+                            $ T.unpack program
+                , _range = Just $ unTrack tr_range
+                }
+            Nothing -> empty
+hoverProvider _ _ _ = pure $ Right Nothing
+
+
+fromMaybeT :: Functor m => a -> MaybeT m a -> m a
+fromMaybeT def = fmap (fromMaybe def) . runMaybeT
+
+
+getMetaprogramsAtSpan
+    :: IdeState
+    -> NormalizedFilePath
+    -> SrcSpan
+    -> MaybeT IO [(Tracked 'Current RealSrcSpan, T.Text)]
+getMetaprogramsAtSpan state nfp ss = do
+    let stale a = runStaleIde "getMetaprogramsAtSpan" state nfp a
+
+    TrackedStale tcg tcg_map <- fmap (fmap tmrTypechecked) $ stale TypeCheck
+
+    let scrutinees = traverse (metaprogramQ ss . tcg_binds) tcg
+    for scrutinees $ \aged@(unTrack -> (ss, program)) -> do
+      case ss of
+        RealSrcSpan r   -> do
+          rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
+          pure (rss', program)
+        UnhelpfulSpan _ -> empty
+
+