hls-tactics-plugin 0.5.1.0 → 1.0.0.0

raw patch · 24 files changed

+1700/−670 lines, 24 filesdep +bytestringdep +data-defaultdep +hspec-expectationsdep −haskell-lspdep ~basedep ~ghcidedep ~hls-plugin-apinew-component:exe:test-serverPVP ok

version bump matches the API change (PVP)

Dependencies added: bytestring, data-default, hspec-expectations, lsp, lsp-test, lsp-types, megaparsec, tasty, tasty-ant-xml, tasty-expected-failure, tasty-golden, tasty-hunit, tasty-rerun

Dependencies removed: haskell-lsp

Dependency ranges changed: base, ghcide, hls-plugin-api, shake

API changes (from Hackage documentation)

Files

• README.md +54/−0
• hls-tactics-plugin.cabal +61/−15
• src/Ide/Plugin/Tactic.hs +187/−284
• src/Ide/Plugin/Tactic/CaseSplit.hs +87/−0
• src/Ide/Plugin/Tactic/CodeGen.hs +24/−81
• src/Ide/Plugin/Tactic/CodeGen/Utils.hs +72/−0
• src/Ide/Plugin/Tactic/Context.hs +9/−10
• src/Ide/Plugin/Tactic/Debug.hs +4/−0
• src/Ide/Plugin/Tactic/FeatureSet.hs +92/−0
• src/Ide/Plugin/Tactic/GHC.hs +147/−11
• src/Ide/Plugin/Tactic/Judgements.hs +52/−25
• src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +0/−2
• src/Ide/Plugin/Tactic/LanguageServer.hs +212/−0
• src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs +192/−0
• src/Ide/Plugin/Tactic/Machinery.hs +15/−16
• src/Ide/Plugin/Tactic/Naming.hs +13/−9
• src/Ide/Plugin/Tactic/Simplify.hs +108/−0
• src/Ide/Plugin/Tactic/Tactics.hs +54/−60
• src/Ide/Plugin/Tactic/TestTypes.hs +23/−0
• src/Ide/Plugin/Tactic/Types.hs +39/−17
• src/Ide/TreeTransform.hs +0/−122
• test/AutoTupleSpec.hs +12/−18
• test/GoldenSpec.hs +224/−0
• test/Server.hs +19/−0

@@ -0,0 +1,54 @@+<p align="center">+<img src="https://haskellwingman.dev/wingman.png" height="256" alt="Wingman for Haskell" title="Wingman for Haskell">+</p>++<p>&nbsp;</p>++# Wingman for Haskell++[![Hackage](https://img.shields.io/hackage/v/hls-tactics-plugin.svg?logo=haskell&label=hls-tactics-plugin)](https://hackage.haskell.org/package/hls-tactics-plugin)++"Focus on the important stuff; delegate the rest"+++## Dedication++> There's a lot of automation that can happen that isn't a replacement of+> humans, but of mind-numbing behavior.+>+> --Stewart Butterfield+++## Overview++Wingman writes the boring, auxiliary code, so you don't have to. Generate+functions from type signatures, and intelligently complete holes.+++## Getting Started++Wingman for Haskell is enabled by default in all [official release of Haskell+Language Server.][hls] Just hover over a typed hole, run the "Attempt to+fill hole" code action, *et voila!*++[hls]: https://github.com/haskell/haskell-language-server/releases+++## Features++* [Type-directed code synthesis][auto], including pattern matching and recursion+* [Automatic case-splitting][case] --- just run the "Case split on <x>" code action+* [Smart next actions][next], for those times it can't read your mind++[auto]: https://haskellwingman.dev/foldr.gif+[case]: https://haskellwingman.dev/case-split.gif+[next]: https://haskellwingman.dev/intros.gif+++## Support++Please consider [pledging on Patreon][patreon] to support the project and get+access to cutting-edge features.++[patreon]: https://www.patreon.com/wingman_for_haskell+

@@ -1,17 +1,19 @@ cabal-version:      2.2 category:           Development name:               hls-tactics-plugin-version:            0.5.1.0-synopsis:           Tactics plugin for Haskell Language Server+version:            1.0.0.0+synopsis:           Wingman plugin for Haskell Language Server description:        Please see README.md author:             Sandy Maguire, Reed Mullanix maintainer:         sandy@sandymaguire.me copyright:          Sandy Maguire, Reed Mullanix+homepage:           https://haskellwingman.dev+bug-reports:        https://github.com/haskell/haskell-language-server/issues license:            Apache-2.0 license-file:       LICENSE build-type:         Simple--- extra-source-files:---   README.md+extra-source-files:+  README.md --   ChangeLog.md  flag pedantic@@ -24,23 +26,28 @@   exposed-modules:     Ide.Plugin.Tactic     Ide.Plugin.Tactic.Auto+    Ide.Plugin.Tactic.CaseSplit     Ide.Plugin.Tactic.CodeGen+    Ide.Plugin.Tactic.CodeGen.Utils     Ide.Plugin.Tactic.Context     Ide.Plugin.Tactic.Debug+    Ide.Plugin.Tactic.FeatureSet     Ide.Plugin.Tactic.GHC     Ide.Plugin.Tactic.Judgements     Ide.Plugin.Tactic.KnownStrategies     Ide.Plugin.Tactic.KnownStrategies.QuickCheck+    Ide.Plugin.Tactic.LanguageServer+    Ide.Plugin.Tactic.LanguageServer.TacticProviders     Ide.Plugin.Tactic.Machinery     Ide.Plugin.Tactic.Naming     Ide.Plugin.Tactic.Range+    Ide.Plugin.Tactic.Simplify     Ide.Plugin.Tactic.Tactics     Ide.Plugin.Tactic.Types     Ide.Plugin.Tactic.TestTypes-    Ide.TreeTransform    ghc-options:-    -Wno-name-shadowing -Wredundant-constraints+    -Wno-name-shadowing -Wredundant-constraints -Wno-unticked-promoted-constructors   if flag(pedantic)     ghc-options: -Werror @@ -57,9 +64,9 @@     , ghc-boot-th     , ghc-exactprint     , ghc-source-gen-    , ghcide         >=0.1-    , haskell-lsp    ^>=0.22-    , hls-plugin-api+    , ghcide         ^>= 1.0.0.0+    , lsp+    , hls-plugin-api ^>= 1.0.0.0     , lens     , mtl     , refinery       ^>=0.3@@ -71,27 +78,66 @@     , deepseq    default-language: Haskell2010+  default-extensions: DataKinds, TypeOperators ++executable test-server+  default-language:   Haskell2010+  build-depends:+    , base+    , data-default+    , ghcide+    , hls-tactics-plugin+    , hls-plugin-api+    , shake+  main-is: Server.hs+  hs-source-dirs: test+  ghc-options:+    "-with-rtsopts=-I0 -A128M"+    -threaded -Wall -Wno-name-shadowing -Wredundant-constraints+ test-suite tests   type: exitcode-stdio-1.0   main-is: Main.hs   other-modules:     AutoTupleSpec+    GoldenSpec     UnificationSpec   hs-source-dirs:       test   ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N   build-depends:       QuickCheck+    , aeson     , base+    , bytestring     , checkers+    , containers+    , data-default+    , deepseq+    , directory+    , filepath+    , ghc+    , ghcide                >= 0.7.5.0+    , hie-bios+    , hls-plugin-api+    , hls-tactics-plugin     , hspec+    , hspec-expectations+    , lens+    , lsp-test+    , lsp-types+    , megaparsec     , mtl-    , hls-tactics-plugin-    , hls-plugin-api-    , hie-bios-    , ghc-    , containers-  build-tool-depends: hspec-discover:hspec-discover+    , tasty+    , tasty-ant-xml           >=1.1.6+    , tasty-expected-failure+    , tasty-golden+    , tasty-hunit+    , tasty-rerun+    , text+  build-tool-depends:+      hspec-discover:hspec-discover+    , hls-tactics-plugin:test-server -any   default-language: Haskell2010 

@@ -1,13 +1,10 @@-{-# LANGUAGE DeriveAnyClass      #-}-{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-} {-# LANGUAGE LambdaCase          #-} {-# LANGUAGE NumDecimals         #-} {-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE PatternSynonyms     #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TupleSections       #-} {-# LANGUAGE TypeApplications    #-}-{-# LANGUAGE ViewPatterns        #-}  -- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic@@ -16,52 +13,43 @@   , TacticCommand (..)   ) where -import           Control.Arrow+import           Bag                                              (bagToList,+                                                                   listToBag)+import           Control.Exception                                (evaluate) import           Control.Monad import           Control.Monad.Trans import           Control.Monad.Trans.Maybe import           Data.Aeson-import           Data.Coerce-import           Data.Functor ((<&>))-import           Data.Generics.Aliases (mkQ)-import           Data.Generics.Schemes (everything)-import           Data.List-import           Data.Map (Map)-import qualified Data.Map as M+import           Data.Bifunctor                                   (Bifunctor (bimap))+import           Data.Bool                                        (bool)+import           Data.Data                                        (Data)+import           Data.Generics.Aliases                            (mkQ)+import           Data.Generics.Schemes                            (everything) import           Data.Maybe import           Data.Monoid-import qualified Data.Set as S-import qualified Data.Text as T+import qualified Data.Text                                        as T import           Data.Traversable-import           Development.IDE.Core.PositionMapping-import           Development.IDE.Core.RuleTypes-import           Development.IDE.Core.Service (runAction)-import           Development.IDE.Core.Shake (useWithStale, IdeState (..))+import           Development.IDE.Core.Shake                       (IdeState (..)) import           Development.IDE.GHC.Compat-import           Development.IDE.GHC.Error (realSrcSpanToRange)-import           Development.IDE.Spans.LocalBindings (getDefiningBindings)-import           Development.Shake (Action)-import           DynFlags (xopt)-import qualified FastString-import           GHC.Generics (Generic)-import           GHC.LanguageExtensions.Type (Extension (LambdaCase))-import           Ide.Plugin.Tactic.Auto-import           Ide.Plugin.Tactic.Context+import           Development.IDE.GHC.ExactPrint+import           Development.Shake.Classes+import           Ide.Plugin.Tactic.CaseSplit+import           Ide.Plugin.Tactic.FeatureSet                     (Feature (..),+                                                                   hasFeature) import           Ide.Plugin.Tactic.GHC-import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.LanguageServer+import           Ide.Plugin.Tactic.LanguageServer.TacticProviders import           Ide.Plugin.Tactic.Range import           Ide.Plugin.Tactic.Tactics import           Ide.Plugin.Tactic.TestTypes import           Ide.Plugin.Tactic.Types-import           Ide.PluginUtils-import           Ide.TreeTransform (transform, graft, useAnnotatedSource) import           Ide.Types-import           Language.Haskell.LSP.Core (clientCapabilities)-import           Language.Haskell.LSP.Types+import           Language.LSP.Server+import           Language.LSP.Types+import           Language.LSP.Types.Capabilities import           OccName-import           SrcLoc (containsSpan)+import           Prelude                                          hiding (span) import           System.Timeout-import           TcRnTypes (tcg_binds)   descriptor :: PluginId -> PluginDescriptor IdeState@@ -73,296 +61,211 @@               (tacticDesc $ tcCommandName tc)               (tacticCmd $ commandTactic tc))               [minBound .. maxBound]-    , pluginCodeActionProvider = Just codeActionProvider+    , pluginHandlers =+        mkPluginHandler STextDocumentCodeAction codeActionProvider     } -tacticDesc :: T.Text -> T.Text-tacticDesc name = "fill the hole using the " <> name <> " tactic" ---------------------------------------------------------------------------------- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS--- UI.-type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] ----------------------------------------------------------------------------------- | Construct a 'CommandId'-tcCommandId :: TacticCommand -> CommandId-tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"------------------------------------------------------------------------------------ | The name of the command for the LS.-tcCommandName :: TacticCommand -> T.Text-tcCommandName = T.pack . show----------------------------------------------------------------------------------- | Mapping from tactic commands to their contextual providers. See 'provide',--- 'filterGoalType' and 'filterBindingType' for the nitty gritty.-commandProvider :: TacticCommand -> TacticProvider-commandProvider Auto  = provide Auto ""-commandProvider Intros =-  filterGoalType isFunction $-    provide Intros ""-commandProvider Destruct =-  filterBindingType destructFilter $ \occ _ ->-    provide Destruct $ T.pack $ occNameString occ-commandProvider Homomorphism =-  filterBindingType homoFilter $ \occ _ ->-    provide Homomorphism $ T.pack $ occNameString occ-commandProvider DestructLambdaCase =-  requireExtension LambdaCase $-    filterGoalType (isJust . lambdaCaseable) $-      provide DestructLambdaCase ""-commandProvider HomomorphismLambdaCase =-  requireExtension LambdaCase $-    filterGoalType ((== Just True) . lambdaCaseable) $-      provide HomomorphismLambdaCase ""------------------------------------------------------------------------------------ | A mapping from tactic commands to actual tactics for refinery.-commandTactic :: TacticCommand -> OccName -> TacticsM ()-commandTactic Auto         = const auto-commandTactic Intros       = const intros-commandTactic Destruct     = destruct-commandTactic Homomorphism = homo-commandTactic DestructLambdaCase     = const destructLambdaCase-commandTactic HomomorphismLambdaCase = const homoLambdaCase------------------------------------------------------------------------------------ | We should show homos only when the goal type is the same as the binding--- type, and that both are usual algebraic types.-homoFilter :: Type -> Type -> Bool-homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2-homoFilter _ _ = False------------------------------------------------------------------------------------ | We should show destruct for bindings only when those bindings have usual--- algebraic types.-destructFilter :: Type -> Type -> Bool-destructFilter _ (algebraicTyCon -> Just _) = True-destructFilter _ _ = False---runIde :: IdeState -> Action a -> IO a-runIde state = runAction "tactic" state---codeActionProvider :: CodeActionProvider IdeState-codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =-      fromMaybeT (Right $ List []) $ do-        (_, jdg, _, dflags) <- judgementForHole state nfp range+codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction+codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do+      features <- getFeatureSet (shakeExtras state)+      liftIO $ fromMaybeT (Right $ List []) $ do+        (_, jdg, _, dflags) <- judgementForHole state nfp range features         actions <- lift $           -- This foldMap is over the function monoid.           foldMap commandProvider [minBound .. maxBound]             dflags+            features             plId             uri             range             jdg         pure $ Right $ List actions-codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []+codeActionProvider _ _ _ = pure $ Right $ List []  -codeActions :: [CodeAction] -> List CAResult-codeActions = List . fmap CACodeAction+tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams+tacticCmd tac state (TacticParams uri range var_name)+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do+      features <- getFeatureSet (shakeExtras state)+      ccs <- getClientCapabilities+      res <- liftIO $ fromMaybeT (Right Nothing) $ do+        (range', jdg, ctx, dflags) <- judgementForHole state nfp range features+        let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'+        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp +        timingOut 2e8 $ join $+          bimap (mkErr InvalidRequest . T.pack . show)+                (mkWorkspaceEdits span dflags ccs uri pm)+            $ runTactic ctx jdg $ tac $ mkVarOcc $ T.unpack var_name ---------------------------------------------------------------------------------- | Terminal constructor for providing context-sensitive tactics. Tactics--- given by 'provide' are always available.-provide :: TacticCommand -> T.Text -> TacticProvider-provide tc name _ plId uri range _ = do-  let title = tacticTitle tc name-      params = TacticParams { file = uri , range = range , var_name = name }-  cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])-  pure-    $ pure-    $ CACodeAction-    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing-    $ Just cmd+      case res of+        Left err -> pure $ Left err+        Right medit -> do+          forM_ medit $ \edit ->+            sendRequest+              SWorkspaceApplyEdit+              (ApplyWorkspaceEditParams Nothing edit)+              (const $ pure ())+          pure $ Right Null+tacticCmd _ _ _ =+  pure $ Left $ mkErr InvalidRequest "Bad URI"  ---------------------------------------------------------------------------------- | Restrict a 'TacticProvider', making sure it appears only when the given--- predicate holds for the goal.-requireExtension :: Extension -> TacticProvider -> TacticProvider-requireExtension ext tp dflags plId uri range jdg =-  case xopt ext dflags of-    True  -> tp dflags plId uri range jdg-    False -> pure []+timingOut+    :: Int                     -- ^ Time in microseconds+    -> Either ResponseError a  -- ^ Computation to run+    -> MaybeT IO (Either ResponseError a)+timingOut t m = do+  x <- lift $ timeout t $ evaluate m+  pure $ joinNote (mkErr InvalidRequest "timed out") x  ---------------------------------------------------------------------------------- | Restrict a 'TacticProvider', making sure it appears only when the given--- predicate holds for the goal.-filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider-filterGoalType p tp dflags plId uri range jdg =-  case p $ unCType $ jGoal jdg of-    True  -> tp dflags plId uri range jdg-    False -> pure []+mkErr :: ErrorCode -> T.Text -> ResponseError+mkErr code err = ResponseError code err Nothing  ---------------------------------------------------------------------------------- | Multiply a 'TacticProvider' for each binding, making sure it appears only--- when the given predicate holds over the goal and binding types.-filterBindingType-    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.-    -> (OccName -> Type -> TacticProvider)-    -> TacticProvider-filterBindingType p tp dflags plId uri range jdg =-  let hy = jHypothesis jdg-      g  = jGoal jdg-   in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) ->-        case p (unCType g) ty of-          True  -> tp occ ty dflags plId uri range jdg-          False -> pure []+joinNote :: e -> Maybe (Either e a) -> Either e a+joinNote e Nothing  = Left e+joinNote _ (Just a) = a  -data TacticParams = TacticParams-    { file :: Uri -- ^ Uri of the file to fill the hole in-    , range :: Range -- ^ The range of the hole-    , var_name :: T.Text-    }-  deriving (Show, Eq, Generic, ToJSON, FromJSON)+------------------------------------------------------------------------------+-- | Turn a 'RunTacticResults' into concrete edits to make in the source+-- document.+mkWorkspaceEdits+    :: RealSrcSpan+    -> DynFlags+    -> ClientCapabilities+    -> Uri+    -> Annotated ParsedSource+    -> RunTacticResults+    -> Either ResponseError (Maybe WorkspaceEdit)+mkWorkspaceEdits span dflags ccs uri pm rtr = do+  let g = graftHole (RealSrcSpan span) rtr+      response = transform dflags ccs uri g pm+   in case response of+        Right res -> Right $ Just res+        Left err  -> Left $ mkErr InternalError $ T.pack err   --------------------------------------------------------------------------------- | Find the last typechecked module, and find the most specific span, as well--- as the judgement at the given range.-judgementForHole-    :: IdeState-    -> NormalizedFilePath-    -> Range-    -> MaybeT IO (Range, Judgement, Context, DynFlags)-judgementForHole state nfp range = do-  (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp-  range' <- liftMaybe $ fromCurrentRange amapping range+-- | Graft a 'RunTacticResults' into the correct place in an AST. Correctly+-- deals with top-level holes, in which we might need to fiddle with the+-- 'Match's that bind variables.+graftHole+    :: SrcSpan+    -> RunTacticResults+    -> Graft (Either String) ParsedSource+graftHole span rtr+  | _jIsTopHole (rtr_jdg rtr)+      = graftSmallestDeclsWithM span+      $ graftDecl span $ \pats ->+        splitToDecl (fst $ last $ ctxDefiningFuncs $ rtr_ctx rtr)+      $ iterateSplit+      $ mkFirstAgda (fmap unXPat pats)+      $ unLoc+      $ rtr_extract rtr+graftHole span rtr+  = graftWithoutParentheses span+    -- Parenthesize the extract iff we're not in a top level hole+  $ bool maybeParensAST id (_jIsTopHole $ rtr_jdg rtr)+  $ rtr_extract rtr -  (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp -  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'-  -- which don't change very often.-  ((modsum,_), _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp-  let dflags = ms_hspp_opts modsum+------------------------------------------------------------------------------+-- | Merge in the 'Match'es of a 'FunBind' into a 'HsDecl'. Used to perform+-- agda-style case splitting in which we need to separate one 'Match' into+-- many, without affecting any matches which might exist but don't need to be+-- split.+mergeFunBindMatches+    :: ([Pat GhcPs] -> LHsDecl GhcPs)+    -> SrcSpan+    -> HsBind GhcPs+    -> Either String (HsBind GhcPs)+mergeFunBindMatches make_decl span+    (fb@FunBind {fun_matches = mg@MG {mg_alts = L alts_src alts}}) =+  pure $ fb+    { fun_matches = mg+      { mg_alts = L alts_src $ do+          alt@(L alt_src match) <- alts+          case span `isSubspanOf` alt_src of+            True -> do+              let pats = fmap fromPatCompatPs $ m_pats match+                  L _ (ValD _ (FunBind {fun_matches = MG+                        {mg_alts = L _ to_add}})) = make_decl pats+              to_add+            False -> pure alt+      }+    }+mergeFunBindMatches _ _ _ =+  Left "mergeFunBindMatches: called on something that isnt a funbind" -  (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast ->-      case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of-        Nothing -> Nothing-        Just ast' -> do-          let info = nodeInfo ast'-          ty <- listToMaybe $ nodeType info-          guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info-          pure (nodeSpan ast', ty) -  resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss-  (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp-  let tcg  = tmrTypechecked tcmod-      tcs = tcg_binds tcg-      ctx = mkContext-              (mapMaybe (sequenceA . (occName *** coerce))-                $ getDefiningBindings binds rss)-              tcg-      top_provs = getRhsPosVals rss tcs-      local_hy = spliceProvenance top_provs-               $ hypothesisFromBindings rss binds-      cls_hy = contextMethodHypothesis ctx-  pure ( resulting_range-       , mkFirstJudgement-           (local_hy <> cls_hy)-           (isRhsHole rss tcs)-           goal-       , ctx-       , dflags-       )+throwError :: String -> TransformT (Either String) a+throwError = lift . Left  -spliceProvenance-    :: Map OccName Provenance-    -> Map OccName (HyInfo a)-    -> Map OccName (HyInfo a)-spliceProvenance provs =-  M.mapWithKey $ \name hi ->-    overProvenance (maybe id const $ M.lookup name provs) hi-+------------------------------------------------------------------------------+-- | Helper function to route 'mergeFunBindMatches' into the right place in an+-- AST --- correctly dealing with inserting into instance declarations.+graftDecl+    :: SrcSpan+    -> ([Pat GhcPs] -> LHsDecl GhcPs)+    -> LHsDecl GhcPs+    -> TransformT (Either String) (Maybe [LHsDecl GhcPs])+graftDecl span+    make_decl+    (L src (ValD ext fb))+  = either throwError (pure . Just . pure . L src . ValD ext) $+      mergeFunBindMatches make_decl span fb+-- TODO(sandy): add another case for default methods in class definitions+graftDecl span+    make_decl+    (L src (InstD ext+      cid@ClsInstD{cid_inst =+        cidi@ClsInstDecl{cid_sigs = _sigs, cid_binds = binds}}))+  = do+      binds' <-+        for (bagToList binds) $ \b@(L bsrc bind) -> do+          case bind of+            fb@FunBind{} | span `isSubspanOf` bsrc ->+              either throwError (pure . L bsrc) $+                mergeFunBindMatches make_decl span fb+            _ -> pure b -tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams-tacticCmd tac lf state (TacticParams uri range var_name)-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =-      fromMaybeT (Right Null, Nothing) $ do-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range-        let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'-        pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp-        x <- lift $ timeout 2e8 $-          case runTactic ctx jdg-                $ tac-                $ mkVarOcc-                $ T.unpack var_name of-            Left err ->-              pure $ (, Nothing)-                $ Left-                $ ResponseError InvalidRequest (T.pack $ show err) Nothing-            Right rtr -> do-              traceMX "solns" $ rtr_other_solns rtr-              let g = graft (RealSrcSpan span) $ rtr_extract rtr-                  response = transform dflags (clientCapabilities lf) uri g pm-              pure $ case response of-                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))-                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)-        pure $ case x of-          Just y -> y-          Nothing -> (, Nothing)-                   $ Left-                   $ ResponseError InvalidRequest "timed out" Nothing-tacticCmd _ _ _ _ =-  pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing-       , Nothing-       )+      pure $ Just $ pure $ L src $ InstD ext $ cid+        { cid_inst = cidi+          { cid_binds = listToBag binds'+          }+        }+graftDecl span _ x = do+  traceMX "biggest" $+    unsafeRender $+      locateBiggest @(Match GhcPs (LHsExpr GhcPs)) span x+  traceMX "first" $+    unsafeRender $+      locateFirst @(Match GhcPs (LHsExpr GhcPs)) x+  throwError "graftDecl: don't know about this AST form"   fromMaybeT :: Functor m => a -> MaybeT m a -> m a fromMaybeT def = fmap (fromMaybe def) . runMaybeT -liftMaybe :: Monad m => Maybe a -> MaybeT m a-liftMaybe a = MaybeT $ pure a ----------------------------------------------------------------------------------- | Is this hole immediately to the right of an equals sign?-isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool-isRhsHole rss tcs = everything (||) (mkQ False $ \case-  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span-  _ -> False-  ) tcs------------------------------------------------------------------------------------ | Compute top-level position vals of a function-getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance-getRhsPosVals rss tcs-  = M.fromList-  $ join-  $ maybeToList-  $ getFirst-  $ everything (<>) (mkQ mempty $ \case-      TopLevelRHS name ps-          (L (RealSrcSpan span)  -- body with no guards and a single defn-            (HsVar _ (L _ hole)))-        | containsSpan rss span  -- which contains our span-        , isHole $ occName hole  -- and the span is a hole-        -> First $ do-            patnames <- traverse getPatName ps-            pure $ zip patnames $ [0..] <&> TopLevelArgPrv name-      _ -> mempty-  ) tcs-+locateBiggest :: (Data r, Data a) => SrcSpan -> a -> Maybe r+locateBiggest ss x = getFirst $ everything (<>)+  ( mkQ mempty $ \case+    L span r | ss `isSubspanOf` span -> pure r+    _                                -> mempty+  ) x  --- TODO(sandy): Make this more robust-isHole :: OccName -> Bool-isHole = isPrefixOf "_" . occNameString+locateFirst :: (Data r, Data a) => a -> Maybe r+locateFirst x = getFirst $ everything (<>)+  ( mkQ mempty $ \case+    r -> pure r+  ) x 

@@ -0,0 +1,87 @@+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE ViewPatterns        #-}++module Ide.Plugin.Tactic.CaseSplit+  ( mkFirstAgda+  , iterateSplit+  , splitToDecl+  ) where++import           Data.Bool (bool)+import           Data.Data+import           Data.Generics+import           Data.Set (Set)+import qualified Data.Set as S+import           Development.IDE.GHC.Compat+import           GHC.Exts (IsString(fromString))+import           GHC.SourceGen (funBinds, match, wildP)+import           Ide.Plugin.Tactic.GHC+import           Ide.Plugin.Tactic.Types+import           OccName++++------------------------------------------------------------------------------+-- | Construct an 'AgdaMatch' from patterns in scope (should be the LHS of the+-- match) and a body.+mkFirstAgda :: [Pat GhcPs] -> HsExpr GhcPs -> AgdaMatch+mkFirstAgda pats (Lambda pats' body) = mkFirstAgda (pats <> pats') body+mkFirstAgda pats body = AgdaMatch pats body+++------------------------------------------------------------------------------+-- | Transform an 'AgdaMatch' whose body is a case over a bound pattern, by+-- splitting it into multiple matches: one for each alternative of the case.+agdaSplit :: AgdaMatch -> [AgdaMatch]+agdaSplit (AgdaMatch pats (Case (HsVar _ (L _ var)) matches)) = do+  (pat, body) <- matches+  -- TODO(sandy): use an at pattern if necessary+  pure $ AgdaMatch (rewriteVarPat var pat pats) body+agdaSplit x = [x]+++------------------------------------------------------------------------------+-- | Replace unused bound patterns with wild patterns.+wildify :: AgdaMatch -> AgdaMatch+wildify (AgdaMatch pats body) =+  let make_wild = bool id (wildifyT (allOccNames body)) $ not $ containsHole body+   in AgdaMatch (make_wild pats) body+++------------------------------------------------------------------------------+-- | Helper function for 'wildify'.+wildifyT :: Data a => Set OccName -> a -> a+wildifyT (S.map occNameString -> used) = everywhere $ mkT $ \case+  VarPat _ (L _ var) | S.notMember (occNameString $ occName var) used -> wildP+  (x :: Pat GhcPs) -> x+++------------------------------------------------------------------------------+-- | Replace a 'VarPat' with the given @'Pat' GhcPs@.+rewriteVarPat :: Data a => RdrName -> Pat GhcPs -> a -> a+rewriteVarPat name rep = everywhere $ mkT $ \case+  VarPat _ (L _ var) | eqRdrName name var -> rep+  (x :: Pat GhcPs) -> x+++------------------------------------------------------------------------------+-- | Construct an 'HsDecl' from a set of 'AgdaMatch'es.+splitToDecl+    :: OccName  -- ^ The name of the function+    -> [AgdaMatch]+    -> LHsDecl GhcPs+splitToDecl name ams = noLoc $ funBinds (fromString . occNameString . occName $ name) $ do+  AgdaMatch pats body <- ams+  pure $ match pats body+++------------------------------------------------------------------------------+-- | Sometimes 'agdaSplit' exposes another opportunity to do 'agdaSplit'. This+-- function runs it a few times, hoping it will find a fixpoint.+iterateSplit :: AgdaMatch -> [AgdaMatch]+iterateSplit am =+  let iterated = iterate (agdaSplit =<<) $ pure am+   in fmap wildify . head . drop 5 $ iterated+

@@ -1,10 +1,12 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections    #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns     #-} -module Ide.Plugin.Tactic.CodeGen where+module Ide.Plugin.Tactic.CodeGen+  ( module Ide.Plugin.Tactic.CodeGen+  , module Ide.Plugin.Tactic.CodeGen.Utils+  ) where  import           Control.Lens ((+~), (%~), (<>~)) import           Control.Monad.Except@@ -18,7 +20,6 @@ import           DataCon import           Development.IDE.GHC.Compat import           GHC.Exts-import           GHC.SourceGen (RdrNameStr) import           GHC.SourceGen.Binds import           GHC.SourceGen.Expr import           GHC.SourceGen.Overloaded@@ -28,14 +29,14 @@ import           Ide.Plugin.Tactic.Machinery import           Ide.Plugin.Tactic.Naming import           Ide.Plugin.Tactic.Types-import           Name+import           Ide.Plugin.Tactic.CodeGen.Utils import           Type hiding (Var)   useOccName :: MonadState TacticState m => Judgement -> OccName -> m () useOccName jdg name =   -- Only score points if this is in the local hypothesis-  case M.lookup name $ jLocalHypothesis jdg of+  case M.lookup name $ hyByName $ jLocalHypothesis jdg of     Just{}  -> modify              $ (withUsedVals $ S.insert name)              . (field @"ts_unused_top_vals" %~ S.delete name)@@ -75,7 +76,7 @@         [] -> throwError $ GoalMismatch "destruct" g         _ -> fmap unzipTrace $ for dcs $ \dc -> do           let args = dataConInstOrigArgTys' dc apps-          names <- mkManyGoodNames hy args+          names <- mkManyGoodNames (hyNamesInScope hy) args           let hy' = zip names $ coerce args               j = introducingPat scrut dc hy'                 $ withNewGoal g jdg@@ -150,23 +151,20 @@ -- | Combinator for performing case splitting, and running sub-rules on the -- resulting matches. -destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule-destruct' f term jdg = do+destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule+destruct' f hi jdg = do   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic-  let hy = jHypothesis jdg-  case M.lookup term hy of-    Nothing -> throwError $ UndefinedHypothesis term-    Just (hi_type -> t) -> do-      useOccName jdg term-      (tr, ms)-          <- destructMatches-               f-               (Just term)-               t-               $ disallowing AlreadyDestructed [term] jdg-      pure ( rose ("destruct " <> show term) $ pure tr-           , noLoc $ case' (var' term) ms-           )+  let term = hi_name hi+  useOccName jdg term+  (tr, ms)+      <- destructMatches+           f+           (Just term)+           (hi_type hi)+           $ disallowing AlreadyDestructed [term] jdg+  pure ( rose ("destruct " <> show term) $ pure tr+       , noLoc $ case' (var' term) ms+       )   ------------------------------------------------------------------------------@@ -178,7 +176,7 @@   let g  = jGoal jdg   case splitFunTy_maybe (unCType g) of     Just (arg, _) | isAlgType arg ->-      fmap (fmap noLoc $ lambdaCase) <$>+      fmap (fmap noLoc lambdaCase) <$>         destructMatches f Nothing (CType arg) jdg     _ -> throwError $ GoalMismatch "destructLambdaCase'" g @@ -190,8 +188,8 @@     -> DataCon            -- ^ The data con to build     -> [Type]             -- ^ Type arguments for the data con     -> RuleM (Trace, LHsExpr GhcPs)-buildDataCon jdg dc apps = do-  let args = dataConInstOrigArgTys' dc apps+buildDataCon jdg dc tyapps = do+  let args = dataConInstOrigArgTys' dc tyapps   (tr, sgs)       <- fmap unzipTrace        $ traverse ( \(arg, n) ->@@ -204,59 +202,4 @@   pure     . (rose (show dc) $ pure tr,)     $ mkCon dc sgs---mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs-mkCon dcon (fmap unLoc -> args)-  | isTupleDataCon dcon =-      noLoc $ tuple args-  | dataConIsInfix dcon-  , (lhs : rhs : args') <- args =-      noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'-  | otherwise =-      noLoc $ foldl' (@@) (bvar' $ occName $ dcon_name) args-  where-    dcon_name = dataConName dcon----coerceName :: HasOccName a => a -> RdrNameStr-coerceName = fromString . occNameString . occName------------------------------------------------------------------------------------- | Like 'var', but works over standard GHC 'OccName's.-var' :: Var a => OccName -> a-var' = var . fromString . occNameString------------------------------------------------------------------------------------ | Like 'bvar', but works over standard GHC 'OccName's.-bvar' :: BVar a => OccName -> a-bvar' = bvar . fromString . occNameString------------------------------------------------------------------------------------ | Get an HsExpr corresponding to a function name.-mkFunc :: String -> HsExpr GhcPs-mkFunc = var' . mkVarOcc------------------------------------------------------------------------------------ | Get an HsExpr corresponding to a value name.-mkVal :: String -> HsExpr GhcPs-mkVal = var' . mkVarOcc------------------------------------------------------------------------------------ | Like 'op', but easier to call.-infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs-infixCall s = flip op (fromString s)------------------------------------------------------------------------------------ | Like '(@@)', but uses a dollar instead of parentheses.-appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs-appDollar = infixCall "$" 

@@ -0,0 +1,72 @@+{-# LANGUAGE ViewPatterns #-}++module Ide.Plugin.Tactic.CodeGen.Utils where++import Data.List+import DataCon+import Development.IDE.GHC.Compat+import GHC.Exts+import GHC.SourceGen (recordConE, RdrNameStr)+import GHC.SourceGen.Overloaded+import Ide.Plugin.Tactic.GHC (getRecordFields)+import Name+++------------------------------------------------------------------------------+-- | Make a data constructor with the given arguments.+mkCon :: DataCon -> [LHsExpr GhcPs] -> LHsExpr GhcPs+mkCon dcon (fmap unLoc -> args)+  | isTupleDataCon dcon =+      noLoc $ tuple args+  | dataConIsInfix dcon+  , (lhs : rhs : args') <- args =+      noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'+  | Just fields <- getRecordFields dcon =+      noLoc $ recordConE (coerceName dcon_name) $ do+        (arg, (field, _)) <- zip args fields+        pure (coerceName field, arg)+  | otherwise =+      noLoc $ foldl' (@@) (bvar' $ occName dcon_name) args+  where+    dcon_name = dataConName dcon+++coerceName :: HasOccName a => a -> RdrNameStr+coerceName = fromString . occNameString . occName+++------------------------------------------------------------------------------+-- | Like 'var', but works over standard GHC 'OccName's.+var' :: Var a => OccName -> a+var' = var . fromString . occNameString+++------------------------------------------------------------------------------+-- | Like 'bvar', but works over standard GHC 'OccName's.+bvar' :: BVar a => OccName -> a+bvar' = bvar . fromString . occNameString+++------------------------------------------------------------------------------+-- | Get an HsExpr corresponding to a function name.+mkFunc :: String -> HsExpr GhcPs+mkFunc = var' . mkVarOcc+++------------------------------------------------------------------------------+-- | Get an HsExpr corresponding to a value name.+mkVal :: String -> HsExpr GhcPs+mkVal = var' . mkVarOcc+++------------------------------------------------------------------------------+-- | Like 'op', but easier to call.+infixCall :: String -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs+infixCall s = flip op (fromString s)+++------------------------------------------------------------------------------+-- | Like '(@@)', but uses a dollar instead of parentheses.+appDollar :: HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs+appDollar = infixCall "$"+

@@ -7,8 +7,6 @@ import           Control.Arrow import           Control.Monad.Reader import           Data.List-import           Data.Map (Map)-import qualified Data.Map as M import           Data.Maybe (mapMaybe) import           Data.Set (Set) import qualified Data.Set as S@@ -20,24 +18,26 @@ import           TcRnTypes import           TcType (substTy, tcSplitSigmaTy) import           Unify (tcUnifyTy)+import Ide.Plugin.Tactic.FeatureSet (FeatureSet)  -mkContext :: [(OccName, CType)] -> TcGblEnv -> Context-mkContext locals tcg = Context+mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context+mkContext features locals tcg = Context   { ctxDefiningFuncs = locals   , ctxModuleFuncs = fmap splitId                    . (getFunBindId =<<)                    . fmap unLoc                    . bagToList                    $ tcg_binds tcg+  , ctxFeatureSet = features   }   ------------------------------------------------------------------------------ -- | Find all of the class methods that exist from the givens in the context.-contextMethodHypothesis :: Context -> Map OccName (HyInfo CType)+contextMethodHypothesis :: Context -> Hypothesis CType contextMethodHypothesis ctx-  = M.fromList+  = Hypothesis   . excludeForbiddenMethods   . join   . concatMap@@ -54,8 +54,8 @@ -- | Many operations are defined in typeclasses for performance reasons, rather -- than being a true part of the class. This function filters out those, in -- order to keep our hypothesis space small.-excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)]-excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)+excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)   where     forbiddenMethods :: Set OccName     forbiddenMethods = S.map mkVarOcc $ S.fromList@@ -89,8 +89,7 @@   getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]-getCurrentDefinitions = asks $ ctxDefiningFuncs+getCurrentDefinitions = asks ctxDefiningFuncs  getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)] getModuleHypothesis = asks ctxModuleFuncs-

@@ -11,6 +11,7 @@   , traceX   , traceIdX   , traceMX+  , traceFX   ) where  import Control.DeepSeq@@ -52,4 +53,7 @@  traceIdX :: (Show a) => String -> a -> a traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a++traceFX :: String -> (a -> String) -> a -> a+traceFX str f a = trace (mappend ("!!!" <> str <> ": ") $ f a) a 

@@ -0,0 +1,92 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PatternSynonyms   #-}+{-# LANGUAGE ViewPatterns      #-}++module Ide.Plugin.Tactic.FeatureSet+  ( Feature (..)+  , FeatureSet+  , hasFeature+  , defaultFeatures+  , allFeatures+  , parseFeatureSet+  , prettyFeatureSet+  ) where++import           Data.List (intercalate)+import           Data.Maybe (mapMaybe, listToMaybe)+import           Data.Set (Set)+import qualified Data.Set as S+import qualified Data.Text as T+++------------------------------------------------------------------------------+-- | All the available features. A 'FeatureSet' describes the ones currently+-- available to the user.+data Feature = CantHaveAnEmptyDataType+  deriving (Eq, Ord, Show, Read, Enum, Bounded)+++------------------------------------------------------------------------------+-- | A collection of enabled features.+type FeatureSet = Set Feature+++------------------------------------------------------------------------------+-- | Parse a feature set.+parseFeatureSet :: T.Text -> FeatureSet+parseFeatureSet+  = mappend defaultFeatures+  . S.fromList+  . mapMaybe (readMaybe . mappend featurePrefix . rot13 . T.unpack)+  . T.split (== '/')+++------------------------------------------------------------------------------+-- | Features that are globally enabled for all users.+defaultFeatures :: FeatureSet+defaultFeatures = S.fromList+  [+  ]+++------------------------------------------------------------------------------+-- | All available features.+allFeatures :: FeatureSet+allFeatures = S.fromList $ enumFromTo minBound maxBound+++------------------------------------------------------------------------------+-- | Pretty print a feature set.+prettyFeatureSet :: FeatureSet -> String+prettyFeatureSet+  = intercalate "/"+  . fmap (rot13 . drop (length featurePrefix) . show)+  . S.toList+++------------------------------------------------------------------------------+-- | Is a given 'Feature' currently enabled?+hasFeature :: Feature -> FeatureSet -> Bool+hasFeature = S.member+++------------------------------------------------------------------------------+-- | Like 'read', but not partial.+readMaybe :: Read a => String -> Maybe a+readMaybe = fmap fst . listToMaybe . reads+++featurePrefix :: String+featurePrefix = "Feature"+++rot13 :: String -> String+rot13 = fmap (toEnum . rot13int . fromEnum)+++rot13int :: Integral a => a -> a+rot13int x+  | (fromIntegral x :: Word) - 97 < 26 = 97 + rem (x - 84) 26+  | (fromIntegral x :: Word) - 65 < 26 = 65 + rem (x - 52) 26+  | otherwise   = x+

@@ -1,17 +1,26 @@-{-# LANGUAGE CPP              #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE PatternSynonyms  #-}-{-# LANGUAGE ViewPatterns     #-}+{-# LANGUAGE CPP                 #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE ViewPatterns        #-}  module Ide.Plugin.Tactic.GHC where  import           Control.Monad.State+import           Data.Function (on)+import           Data.List (isPrefixOf) import qualified Data.Map as M import           Data.Maybe (isJust)+import           Data.Set (Set)+import qualified Data.Set as S import           Data.Traversable-import qualified DataCon as DataCon+import           DataCon import           Development.IDE.GHC.Compat-import           Generics.SYB (mkT, everywhere)+import           GHC.SourceGen (match, case', lambda)+import           Generics.SYB (mkQ, everything, listify, Data, mkT, everywhere) import           Ide.Plugin.Tactic.Types import           OccName import           TcType@@ -21,6 +30,7 @@ import           Unique import           Var + tcTyVar_maybe :: Type -> Maybe Var tcTyVar_maybe ty | Just ty' <- tcView ty = tcTyVar_maybe ty' tcTyVar_maybe (CastTy ty _) = tcTyVar_maybe ty  -- look through casts, as@@ -78,7 +88,7 @@   reps <- fmap M.fromList         $ for tvs $ \tv -> do             uniq <- freshUnique-            pure $ (tv, setTyVarUnique tv uniq)+            pure (tv, setTyVarUnique tv uniq)   pure $     everywhere       (mkT $ \tv ->@@ -89,6 +99,18 @@   ------------------------------------------------------------------------------+-- | Given a datacon, extract its record fields' names and types. Returns+-- nothing if the datacon is not a record.+getRecordFields :: DataCon -> Maybe [(OccName, CType)]+getRecordFields dc =+  case dataConFieldLabels dc of+    [] -> Nothing+    lbls -> for lbls $ \lbl -> do+      (_, ty) <- dataConFieldType_maybe dc $ flLabel lbl+      pure (mkVarOccFS $ flLabel lbl, CType ty)+++------------------------------------------------------------------------------ -- | Is this an algebraic type? algebraicTyCon :: Type -> Maybe TyCon algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))@@ -100,7 +122,103 @@   | otherwise = Just tycon algebraicTyCon _ = Nothing + ------------------------------------------------------------------------------+-- | We can't compare 'RdrName' for equality directly. Instead, compare them by+-- their 'OccName's.+eqRdrName :: RdrName -> RdrName -> Bool+eqRdrName = (==) `on` occNameString . occName+++------------------------------------------------------------------------------+-- | Does this thing contain any references to 'HsVar's with the given+-- 'RdrName'?+containsHsVar :: Data a => RdrName -> a -> Bool+containsHsVar name x = not $ null $ listify (+  \case+    ((HsVar _ (L _ a)) :: HsExpr GhcPs) | eqRdrName a name -> True+    _ -> False+  ) x+++------------------------------------------------------------------------------+-- | Does this thing contain any holes?+containsHole :: Data a => a -> Bool+containsHole x = not $ null $ listify (+  \case+    ((HsVar _ (L _ name)) :: HsExpr GhcPs) -> isHole $ occName name+    _ -> False+  ) x+++------------------------------------------------------------------------------+-- | Check if an 'OccName' is a hole+isHole :: OccName -> Bool+-- TODO(sandy): Make this more robust+isHole = isPrefixOf "_" . occNameString+++------------------------------------------------------------------------------+-- | Get all of the referenced occnames.+allOccNames :: Data a => a -> Set OccName+allOccNames = everything (<>) $ mkQ mempty $ \case+    a -> S.singleton a+++++------------------------------------------------------------------------------+-- | A pattern over the otherwise (extremely) messy AST for lambdas.+pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs+pattern Lambda pats body <-+  HsLam _+    (MG {mg_alts = L _ [L _+      (Match { m_pats = fmap fromPatCompatPs -> pats+             , m_grhss = UnguardedRHSs body+             })]})+  where+    -- If there are no patterns to bind, just stick in the body+    Lambda [] body   = body+    Lambda pats body = lambda pats body+++------------------------------------------------------------------------------+-- | A GRHS that caontains no guards.+pattern UnguardedRHSs :: HsExpr GhcPs -> GRHSs GhcPs (LHsExpr GhcPs)+pattern UnguardedRHSs body <-+  GRHSs {grhssGRHSs = [L _ (GRHS _ [] (L _ body))]}+++------------------------------------------------------------------------------+-- | A match with a single pattern. Case matches are always 'SinglePatMatch'es.+pattern SinglePatMatch :: Pat GhcPs -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)+pattern SinglePatMatch pat body <-+  Match { m_pats = [fromPatCompatPs -> pat]+        , m_grhss = UnguardedRHSs body+        }+++------------------------------------------------------------------------------+-- | Helper function for defining the 'Case' pattern.+unpackMatches :: [Match GhcPs (LHsExpr GhcPs)] -> Maybe [(Pat GhcPs, HsExpr GhcPs)]+unpackMatches [] = Just []+unpackMatches (SinglePatMatch pat body : matches) =+  (:) <$> pure (pat, body) <*> unpackMatches matches+unpackMatches _ = Nothing+++------------------------------------------------------------------------------+-- | A pattern over the otherwise (extremely) messy AST for lambdas.+pattern Case :: HsExpr GhcPs -> [(Pat GhcPs, HsExpr GhcPs)] -> HsExpr GhcPs+pattern Case scrutinee matches <-+  HsCase _ (L _ scrutinee)+    (MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})+  where+    Case scrutinee matches =+      case' scrutinee $ fmap (\(pat, body) -> match [pat] body) matches+++------------------------------------------------------------------------------ -- | Can ths type be lambda-cased? -- -- Return: 'Nothing' if no@@ -112,13 +230,17 @@   = Just $ isJust $ algebraicTyCon res lambdaCaseable _ = Nothing -fromPatCompat :: PatCompat GhcTc -> Pat GhcTc+-- It's hard to generalize over these since weird type families are involved.+fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc+fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs #if __GLASGOW_HASKELL__ == 808 type PatCompat pass = Pat pass-fromPatCompat = id+fromPatCompatTc = id+fromPatCompatPs = id #else type PatCompat pass = LPat pass-fromPatCompat = unLoc+fromPatCompatTc = unLoc+fromPatCompatPs = unLoc #endif  ------------------------------------------------------------------------------@@ -132,7 +254,7 @@       [L _ (GRHS _ [] body)] _)  getPatName :: PatCompat GhcTc -> Maybe OccName-getPatName (fromPatCompat -> p0) =+getPatName (fromPatCompatTc -> p0) =   case p0 of     VarPat  _ x   -> Just $ occName $ unLoc x     LazyPat _ p   -> getPatName p@@ -154,3 +276,17 @@ #else dataConExTys = DataCon.dataConExTyVars #endif+++------------------------------------------------------------------------------+-- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'.+-- The nitty gritty details are explained at+-- https://blog.shaynefletcher.org/2020/03/ghc-haskell-pats-and-lpats.html+--+-- We need to remove these in order to succesfull find patterns.+unXPat :: Pat GhcPs -> Pat GhcPs+#if __GLASGOW_HASKELL__ == 808+unXPat (XPat (L _ pat)) = unXPat pat+#endif+unXPat pat = pat+

@@ -1,7 +1,3 @@-{-# LANGUAGE DataKinds        #-}-{-# LANGUAGE LambdaCase       #-}-{-# LANGUAGE RecordWildCards  #-}-{-# LANGUAGE TupleSections    #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns     #-} @@ -29,8 +25,11 @@   , mkFirstJudgement   , hypothesisFromBindings   , isTopLevel+  , hyNamesInScope+  , hyByName   ) where +import           Control.Arrow import           Control.Lens hiding (Context) import           Data.Bool import           Data.Char@@ -51,20 +50,20 @@  ------------------------------------------------------------------------------ -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.-hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)+hypothesisFromBindings :: RealSrcSpan -> Bindings -> Hypothesis CType hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span   ------------------------------------------------------------------------------ -- | Convert a @Set Id@ into a hypothesis.-buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType)+buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType buildHypothesis-  = M.fromList+  = Hypothesis   . mapMaybe go   where     go (occName -> occ, t)       | Just ty <- t-      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty)+      , isAlpha . head . occNameString $ occ = Just $ HyInfo occ UserPrv $ CType ty       | otherwise = Nothing  @@ -99,8 +98,8 @@     -> Judgement' a     -> Judgement' a introducing f ns =-  field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>-    \(pos, (name, ty)) -> (name, HyInfo (f pos) ty))+  field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&>+    \(pos, (name, ty)) -> HyInfo name (f pos) ty)   ------------------------------------------------------------------------------@@ -152,7 +151,7 @@     -> Judgement     -> Judgement filterAncestry ancestry reason jdg =-    disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg+    disallowing reason (M.keys $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg   where     go name _       = not@@ -175,7 +174,7 @@ findPositionVal jdg defn pos = listToMaybe $ do   -- It's important to inspect the entire hypothesis here, as we need to trace   -- ancstry through potentially disallowed terms in the hypothesis.-  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg+  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg   case hi_provenance hi of     TopLevelArgPrv defn' pos'       | defn == defn'@@ -191,7 +190,7 @@ -- 'filterSameTypeFromOtherPositions'. findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName] findDconPositionVals jdg dcon pos = do-  (name, hi) <- M.toList $ jHypothesis jdg+  (name, hi) <- M.toList $ hyByName $ jHypothesis jdg   case hi_provenance hi of     PatternMatchPrv pv       | pv_datacon  pv == Uniquely dcon@@ -206,14 +205,15 @@ -- other term which might match. filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement filterSameTypeFromOtherPositions dcon pos jdg =-  let hy = jHypothesis+  let hy = hyByName+         . jHypothesis          $ filterAncestry              (findDconPositionVals jdg dcon pos)              (WrongBranch pos)              jdg       tys = S.fromList $ hi_type <$> M.elems hy       to_remove =-        M.filter (flip S.member tys . hi_type) (jHypothesis jdg)+        M.filter (flip S.member tys . hi_type) (hyByName $ jHypothesis jdg)           M.\\ hy    in disallowing Shadowed (M.keys to_remove) jdg @@ -270,8 +270,8 @@ -- them from 'jHypothesis', but not from 'jEntireHypothesis'. disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a disallowing reason (S.fromList -> ns) =-  field @"_jHypothesis" %~ (M.mapWithKey $ \name hi ->-    case S.member name ns of+  field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->+    case S.member (hi_name hi) ns of       True -> overProvenance (DisallowedPrv reason) hi       False -> hi                            )@@ -280,20 +280,28 @@ ------------------------------------------------------------------------------ -- | The hypothesis, consisting of local terms and the ambient environment -- (impors and class methods.) Hides disallowed values.-jHypothesis :: Judgement' a -> Map OccName (HyInfo a)-jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis+jHypothesis :: Judgement' a -> Hypothesis a+jHypothesis+  = Hypothesis+  . filter (not . isDisallowed . hi_provenance)+  . unHypothesis+  . jEntireHypothesis   ------------------------------------------------------------------------------ -- | The whole hypothesis, including things disallowed.-jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)+jEntireHypothesis :: Judgement' a -> Hypothesis a jEntireHypothesis = _jHypothesis   ------------------------------------------------------------------------------ -- | Just the local hypothesis.-jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)-jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis+jLocalHypothesis :: Judgement' a -> Hypothesis a+jLocalHypothesis+  = Hypothesis+  . filter (isLocalHypothesis . hi_provenance)+  . unHypothesis+  . jHypothesis   ------------------------------------------------------------------------------@@ -308,9 +316,29 @@   ------------------------------------------------------------------------------+-- | What names are currently in scope in the hypothesis?+hyNamesInScope :: Hypothesis a -> Set OccName+hyNamesInScope = M.keysSet . hyByName+++------------------------------------------------------------------------------+-- | Fold a hypothesis into a single mapping from name to info. This+-- unavoidably will cause duplicate names (things like methods) to shadow one+-- another.+hyByName :: Hypothesis a -> Map OccName (HyInfo a)+hyByName+  = M.fromList+  . fmap (hi_name &&& id)+  . unHypothesis+++------------------------------------------------------------------------------ -- | Only the hypothesis members which are pattern vals jPatHypothesis :: Judgement' a -> Map OccName PatVal-jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis+jPatHypothesis+  = M.mapMaybe (getPatVal . hi_provenance)+  . hyByName+  . jHypothesis   getPatVal :: Provenance-> Maybe PatVal@@ -329,7 +357,7 @@   mkFirstJudgement-    :: M.Map OccName (HyInfo CType)+    :: Hypothesis CType     -> Bool  -- ^ are we in the top level rhs hole?     -> Type     -> Judgement' CType@@ -377,4 +405,3 @@ expandDisallowed :: Provenance -> Provenance expandDisallowed (DisallowedPrv _ prv) = expandDisallowed prv expandDisallowed prv = prv-

@@ -1,5 +1,4 @@ {-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE LambdaCase #-}  module Ide.Plugin.Tactic.KnownStrategies.QuickCheck where @@ -109,4 +108,3 @@                     (n == 1)             @@ arbitrary         False -> arbitrary-

@@ -0,0 +1,212 @@+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Ide.Plugin.Tactic.LanguageServer where++import           Control.Arrow+import           Control.Monad+import           Control.Monad.Trans.Maybe+import           Data.Aeson                           (Value (Object), fromJSON)+import           Data.Aeson.Types                     (Result (Error, Success))+import           Data.Coerce+import           Data.Functor                         ((<&>))+import           Data.Generics.Aliases                (mkQ)+import           Data.Generics.Schemes                (everything)+import           Data.Map                             (Map)+import qualified Data.Map                             as M+import           Data.Maybe+import           Data.Monoid+import qualified Data.Set                             as S+import qualified Data.Text                            as T+import           Data.Traversable+import           Development.IDE                      (ShakeExtras,+                                                       getPluginConfig)+import           Development.IDE.Core.PositionMapping+import           Development.IDE.Core.RuleTypes+import           Development.IDE.Core.Service         (runAction)+import           Development.IDE.Core.Shake           (IdeState (..),+                                                       useWithStale)+import           Development.IDE.GHC.Compat+import           Development.IDE.GHC.Error            (realSrcSpanToRange)+import           Development.IDE.Spans.LocalBindings  (Bindings,+                                                       getDefiningBindings)+import           Development.Shake                    (Action, RuleResult)+import           Development.Shake.Classes+import qualified FastString+import           Ide.Plugin.Config                    (PluginConfig (plcConfig))+import qualified Ide.Plugin.Config                    as Plugin+import           Ide.Plugin.Tactic.Context+import           Ide.Plugin.Tactic.FeatureSet+import           Ide.Plugin.Tactic.GHC+import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Range+import           Ide.Plugin.Tactic.TestTypes          (TacticCommand,+                                                       cfg_feature_set)+import           Ide.Plugin.Tactic.Types+import           Language.LSP.Server                  (MonadLsp)+import           Language.LSP.Types+import           OccName+import           Prelude                              hiding (span)+import           SrcLoc                               (containsSpan)+import           TcRnTypes                            (tcg_binds)+++tacticDesc :: T.Text -> T.Text+tacticDesc name = "fill the hole using the " <> name <> " tactic"+++------------------------------------------------------------------------------+-- | The name of the command for the LS.+tcCommandName :: TacticCommand -> T.Text+tcCommandName = T.pack . show+++runIde :: IdeState -> Action a -> IO a+runIde state = runAction "tactic" state+++runStaleIde+    :: forall a r+     . ( r ~ RuleResult a+       , Eq a , Hashable a , Binary a , Show a , Typeable a , NFData a+       , Show r, Typeable r, NFData r+       )+    => IdeState+    -> NormalizedFilePath+    -> a+    -> MaybeT IO (r, PositionMapping)+runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp+++------------------------------------------------------------------------------+-- | Get the current feature set from the plugin config.+getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet+getFeatureSet extras = do+  pcfg <- getPluginConfig extras "tactics"+  pure $ case fromJSON $ Object $ plcConfig pcfg of+    Success cfg -> cfg_feature_set cfg+    Error _     -> defaultFeatures+++getIdeDynflags+    :: IdeState+    -> NormalizedFilePath+    -> MaybeT IO DynFlags+getIdeDynflags state nfp = do+  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'+  -- which don't change very often.+  ((modsum,_), _) <- runStaleIde state nfp GetModSummaryWithoutTimestamps+  pure $ ms_hspp_opts modsum+++------------------------------------------------------------------------------+-- | Find the last typechecked module, and find the most specific span, as well+-- as the judgement at the given range.+judgementForHole+    :: IdeState+    -> NormalizedFilePath+    -> Range+    -> FeatureSet+    -> MaybeT IO (Range, Judgement, Context, DynFlags)+judgementForHole state nfp range features = do+  (asts, amapping) <- runStaleIde state nfp GetHieAst+  case asts of+    HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"+    HAR _ hf _ _ HieFresh -> do+      (binds, _) <- runStaleIde state nfp GetBindings+      (tcmod, _) <- runStaleIde state nfp TypeCheck+      (rss, g)   <- liftMaybe $ getSpanAndTypeAtHole amapping range hf+      resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss+      let (jdg, ctx) = mkJudgementAndContext features g binds rss tcmod+      dflags <- getIdeDynflags state nfp+      pure (resulting_range, jdg, ctx, dflags)+++mkJudgementAndContext+    :: FeatureSet+    -> Type+    -> Bindings+    -> RealSrcSpan+    -> TcModuleResult+    -> (Judgement, Context)+mkJudgementAndContext features g binds rss tcmod = do+      let tcg  = tmrTypechecked tcmod+          tcs = tcg_binds tcg+          ctx = mkContext features+                  (mapMaybe (sequenceA . (occName *** coerce))+                    $ getDefiningBindings binds rss)+                  tcg+          top_provs = getRhsPosVals rss tcs+          local_hy = spliceProvenance top_provs+                   $ hypothesisFromBindings rss binds+          cls_hy = contextMethodHypothesis ctx+       in ( mkFirstJudgement+              (local_hy <> cls_hy)+              (isRhsHole rss tcs)+              g+          , ctx+          )+++getSpanAndTypeAtHole+    :: PositionMapping+    -> Range+    -> HieASTs b+    -> Maybe (Span, b)+getSpanAndTypeAtHole amapping range hf = do+  range' <- fromCurrentRange amapping range+  join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts hf) $ \fs ast ->+    case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of+      Nothing -> Nothing+      Just ast' -> do+        let info = nodeInfo ast'+        ty <- listToMaybe $ nodeType info+        guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info+        pure (nodeSpan ast', ty)+++liftMaybe :: Monad m => Maybe a -> MaybeT m a+liftMaybe a = MaybeT $ pure a+++spliceProvenance+    :: Map OccName Provenance+    -> Hypothesis a+    -> Hypothesis a+spliceProvenance provs x =+  Hypothesis $ flip fmap (unHypothesis x) $ \hi ->+    overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi+++------------------------------------------------------------------------------+-- | Compute top-level position vals of a function+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance+getRhsPosVals rss tcs+  = M.fromList+  $ join+  $ maybeToList+  $ getFirst+  $ everything (<>) (mkQ mempty $ \case+      TopLevelRHS name ps+          (L (RealSrcSpan span)  -- body with no guards and a single defn+            (HsVar _ (L _ hole)))+        | containsSpan rss span  -- which contains our span+        , isHole $ occName hole  -- and the span is a hole+        -> First $ do+            patnames <- traverse getPatName ps+            pure $ zip patnames $ [0..] <&> TopLevelArgPrv name+      _ -> mempty+  ) tcs+++------------------------------------------------------------------------------+-- | Is this hole immediately to the right of an equals sign?+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool+isRhsHole rss tcs = everything (||) (mkQ False $ \case+  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span+  _                                        -> False+  ) tcs+

@@ -0,0 +1,192 @@+{-# LANGUAGE DeriveAnyClass     #-}+{-# LANGUAGE DeriveGeneric      #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE OverloadedStrings  #-}+{-# LANGUAGE ViewPatterns       #-}++module Ide.Plugin.Tactic.LanguageServer.TacticProviders+  ( commandProvider+  , commandTactic+  , tcCommandId+  , TacticParams (..)+  ) where++import           Control.Monad+import           Control.Monad.Error.Class (MonadError(throwError))+import           Data.Aeson+import           Data.Coerce+import qualified Data.Map as M+import           Data.Maybe+import           Data.Monoid+import qualified Data.Text as T+import           Data.Traversable+import           Development.IDE.GHC.Compat+import           GHC.Generics+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))+import           Ide.Plugin.Tactic.Auto+import           Ide.Plugin.Tactic.FeatureSet+import           Ide.Plugin.Tactic.GHC+import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Tactics+import           Ide.Plugin.Tactic.TestTypes+import           Ide.Plugin.Tactic.Types+import           Ide.PluginUtils+import           Ide.Types+import           Language.LSP.Types+import           OccName+import           Prelude hiding (span)+import           Refinery.Tactic (goal)+++------------------------------------------------------------------------------+-- | A mapping from tactic commands to actual tactics for refinery.+commandTactic :: TacticCommand -> OccName -> TacticsM ()+commandTactic Auto         = const auto+commandTactic Intros       = const intros+commandTactic Destruct     = useNameFromHypothesis destruct+commandTactic Homomorphism = useNameFromHypothesis homo+commandTactic DestructLambdaCase     = const destructLambdaCase+commandTactic HomomorphismLambdaCase = const homoLambdaCase+++------------------------------------------------------------------------------+-- | Mapping from tactic commands to their contextual providers. See 'provide',+-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.+commandProvider :: TacticCommand -> TacticProvider+commandProvider Auto  = provide Auto ""+commandProvider Intros =+  filterGoalType isFunction $+    provide Intros ""+commandProvider Destruct =+  filterBindingType destructFilter $ \occ _ ->+    provide Destruct $ T.pack $ occNameString occ+commandProvider Homomorphism =+  filterBindingType homoFilter $ \occ _ ->+    provide Homomorphism $ T.pack $ occNameString occ+commandProvider DestructLambdaCase =+  requireExtension LambdaCase $+    filterGoalType (isJust . lambdaCaseable) $+      provide DestructLambdaCase ""+commandProvider HomomorphismLambdaCase =+  requireExtension LambdaCase $+    filterGoalType ((== Just True) . lambdaCaseable) $+      provide HomomorphismLambdaCase ""+++------------------------------------------------------------------------------+-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS+-- UI.+type TacticProvider+     = DynFlags+    -> FeatureSet+    -> PluginId+    -> Uri+    -> Range+    -> Judgement+    -> IO [Command |? CodeAction]+++data TacticParams = TacticParams+    { tp_file     :: Uri    -- ^ Uri of the file to fill the hole in+    , tp_range    :: Range  -- ^ The range of the hole+    , tp_var_name :: T.Text+    }+  deriving stock (Show, Eq, Generic)+  deriving anyclass (ToJSON, FromJSON)+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- 'Feature' is in the feature set.+requireFeature :: Feature -> TacticProvider -> TacticProvider+requireFeature f tp dflags fs plId uri range jdg = do+  guard $ hasFeature f fs+  tp dflags fs plId uri range jdg+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- predicate holds for the goal.+requireExtension :: Extension -> TacticProvider -> TacticProvider+requireExtension ext tp dflags fs plId uri range jdg =+  case xopt ext dflags of+    True  -> tp dflags fs plId uri range jdg+    False -> pure []+++------------------------------------------------------------------------------+-- | Restrict a 'TacticProvider', making sure it appears only when the given+-- predicate holds for the goal.+filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider+filterGoalType p tp dflags fs plId uri range jdg =+  case p $ unCType $ jGoal jdg of+    True  -> tp dflags fs plId uri range jdg+    False -> pure []+++------------------------------------------------------------------------------+-- | Multiply a 'TacticProvider' for each binding, making sure it appears only+-- when the given predicate holds over the goal and binding types.+filterBindingType+    :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.+    -> (OccName -> Type -> TacticProvider)+    -> TacticProvider+filterBindingType p tp dflags fs plId uri range jdg =+  let hy = jHypothesis jdg+      g  = jGoal jdg+   in fmap join $ for (unHypothesis hy) $ \hi ->+        let ty = unCType $ hi_type hi+         in case p (unCType g) ty of+              True  -> tp (hi_name hi) ty dflags fs plId uri range jdg+              False -> pure []++++------------------------------------------------------------------------------+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to+-- look it up in the hypothesis.+useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a+useNameFromHypothesis f name = do+  hy <- jHypothesis <$> goal+  case M.lookup name $ hyByName hy of+    Just hi -> f hi+    Nothing -> throwError $ NotInScope name+++------------------------------------------------------------------------------+-- | Terminal constructor for providing context-sensitive tactics. Tactics+-- given by 'provide' are always available.+provide :: TacticCommand -> T.Text -> TacticProvider+provide tc name _ _ plId uri range _ = do+  let title = tacticTitle tc name+      params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }+      cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])+  pure+    $ pure+    $ InR+    $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing Nothing Nothing+    $ Just cmd+++------------------------------------------------------------------------------+-- | Construct a 'CommandId'+tcCommandId :: TacticCommand -> CommandId+tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"++++------------------------------------------------------------------------------+-- | We should show homos only when the goal type is the same as the binding+-- type, and that both are usual algebraic types.+homoFilter :: Type -> Type -> Bool+homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2+homoFilter _ _ = False+++------------------------------------------------------------------------------+-- | We should show destruct for bindings only when those bindings have usual+-- algebraic types.+destructFilter :: Type -> Type -> Bool+destructFilter _ (algebraicTyCon -> Just _) = True+destructFilter _ _ = False+

@@ -1,7 +1,4 @@ {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE DeriveFunctor         #-}-{-# LANGUAGE DeriveGeneric         #-}-{-# LANGUAGE DerivingStrategies    #-} {-# LANGUAGE DerivingVia           #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-}@@ -9,9 +6,7 @@ {-# LANGUAGE MonoLocalBinds        #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards       #-}-{-# LANGUAGE TypeSynonymInstances  #-} {-# LANGUAGE ViewPatterns          #-}-{-# LANGUAGE ViewPatterns          #-} {-# OPTIONS_GHC -fno-warn-orphans  #-}  module Ide.Plugin.Tactic.Machinery@@ -38,6 +33,7 @@ import qualified Data.Set as S import           Development.IDE.GHC.Compat import           Ide.Plugin.Tactic.Judgements+import           Ide.Plugin.Tactic.Simplify (simplify) import           Ide.Plugin.Tactic.Types import           OccName (HasOccName(occName)) import           Refinery.ProofState@@ -79,9 +75,11 @@                 $ (:) (jGoal jdg)                 $ fmap hi_type                 $ toList+                $ hyByName                 $ jHypothesis jdg         unused_topvals = M.keysSet                        $ M.filter (isTopLevel . hi_provenance)+                       $ hyByName                        $ jHypothesis jdg         tacticState =           defaultTacticState@@ -92,18 +90,21 @@           . flip runReader ctx           . unExtractM           $ runTacticT t jdg tacticState of-      (errs, []) -> Left $ take 50 $ errs+      (errs, []) -> Left $ take 50 errs       (_, fmap assoc23 -> solns) -> do         let sorted =               flip sortBy solns $ comparing $ \((_, ext), (jdg, holes)) ->                 Down $ scoreSolution ext jdg holes         case sorted of           (((tr, ext), _) : _) ->-            Right-              . RunTacticResults tr ext-              . reverse-              . fmap fst-              $ take 5 sorted+            Right $+              RunTacticResults+                { rtr_trace = tr+                , rtr_extract = simplify ext+                , rtr_other_solns = reverse . fmap fst $ take 5 sorted+                , rtr_jdg = jdg+                , rtr_ctx = ctx+                }           -- guaranteed to not be empty           _ -> Left [] @@ -174,7 +175,7 @@     , Penalize $ S.size ts_unused_top_vals     , Penalize $ S.size ts_intro_vals     , Reward   $ S.size ts_used_vals-    , Penalize $ ts_recursion_count+    , Penalize ts_recursion_count     , Penalize $ solutionSize ext     ) @@ -223,7 +224,7 @@ ------------------------------------------------------------------------------ -- | Get the class methods of a 'PredType', correctly dealing with -- instantiation of quantified class types.-methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]+methodHypothesis :: PredType -> Maybe [HyInfo CType] methodHypothesis ty = do   (tc, apps) <- splitTyConApp_maybe ty   cls <- tyConClass_maybe tc@@ -235,8 +236,7 @@               $ classSCTheta cls   pure $ mappend sc_methods $ methods <&> \method ->     let (_, _, ty) = tcSplitSigmaTy $ idType method-    in ( occName method-       , HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty+    in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty        )  @@ -251,4 +251,3 @@   case S.size $ vars S.\\ skolems of     0 -> m     _ -> throwError TooPolymorphic-

@@ -7,6 +7,8 @@ import           Data.Char import           Data.Map (Map) import qualified Data.Map as M+import           Data.Set (Set)+import qualified Data.Set as S import           Data.Traversable import           Name import           TcType@@ -22,16 +24,19 @@ mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b))   = "f" ++ mkTyName a ++ mkTyName b -- eg. mkTyName (a -> b -> C) = "f_C"-mkTyName (tcSplitFunTys -> ((_:_), b))+mkTyName (tcSplitFunTys -> (_:_, b))   = "f_" ++ mkTyName b -- eg. mkTyName (Either A B) = "eab" mkTyName (splitTyConApp_maybe -> Just (c, args))   = mkTyConName c ++ foldMap mkTyName args+-- eg. mkTyName (f a) = "fa"+mkTyName (tcSplitAppTys -> (t, args@(_:_)))+  = mkTyName t ++ foldMap mkTyName args -- eg. mkTyName a = "a" mkTyName (getTyVar_maybe -> Just tv)   = occNameString $ occName tv -- eg. mkTyName (forall x. y) = "y"-mkTyName (tcSplitSigmaTy -> ((_:_), _, t))+mkTyName (tcSplitSigmaTy -> (_:_, _, t))   = mkTyName t mkTyName _ = "x" @@ -61,12 +66,12 @@ ------------------------------------------------------------------------------ -- | Produce a unique, good name for a type. mkGoodName-    :: [OccName]  -- ^ Bindings in scope; used to ensure we don't shadow anything+    :: Set OccName  -- ^ Bindings in scope; used to ensure we don't shadow anything     -> Type       -- ^ The type to produce a name for     -> OccName mkGoodName in_scope t =   let tn = mkTyName t-   in mkVarOcc $ case elem (mkVarOcc tn) in_scope of+   in mkVarOcc $ case S.member (mkVarOcc tn) in_scope of         True -> tn ++ show (length in_scope)         False -> tn @@ -75,14 +80,14 @@ -- | Like 'mkGoodName' but creates several apart names. mkManyGoodNames   :: (Traversable t, Monad m)-  => M.Map OccName a+  => Set OccName   -> t Type   -> m (t OccName)-mkManyGoodNames hy args =-  flip evalStateT (getInScope hy) $ for args $ \at -> do+mkManyGoodNames in_scope args =+  flip evalStateT in_scope $ for args $ \at -> do     in_scope <- get     let n = mkGoodName in_scope at-    modify (n :)+    modify $ S.insert n     pure n  @@ -90,4 +95,3 @@ -- | Which names are in scope? getInScope :: Map OccName a -> [OccName] getInScope = M.keys-

@@ -0,0 +1,108 @@+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE OverloadedStrings   #-}+{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns        #-}++module Ide.Plugin.Tactic.Simplify+  ( simplify+  ) where++import Data.Generics (everywhere, mkT, GenericT)+import Data.List.Extra (unsnoc)+import Data.Monoid (Endo (..))+import Development.IDE.GHC.Compat+import GHC.SourceGen (var)+import GHC.SourceGen.Expr (lambda)+import Ide.Plugin.Tactic.CodeGen.Utils+import Ide.Plugin.Tactic.GHC (fromPatCompatPs, containsHsVar)+++------------------------------------------------------------------------------+-- | A pattern over the otherwise (extremely) messy AST for lambdas.+pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs+pattern Lambda pats body <-+  HsLam _+    (MG {mg_alts = L _ [L _+      (Match { m_pats = fmap fromPatCompatPs -> pats+             , m_grhss = GRHSs {grhssGRHSs = [L _ (+                 GRHS _ [] (L _ body))]}+             })]})+  where+    -- If there are no patterns to bind, just stick in the body+    Lambda [] body   = body+    Lambda pats body = lambda pats body+++------------------------------------------------------------------------------+-- | Simlify an expression.+simplify :: LHsExpr GhcPs -> LHsExpr GhcPs+simplify+  = head+  . drop 3   -- Do three passes; this should be good enough for the limited+             -- amount of gas we give to auto+  . iterate (everywhere $ foldEndo+    [ simplifyEtaReduce+    , simplifyRemoveParens+    , simplifyCompose+    ])+++------------------------------------------------------------------------------+-- | Like 'foldMap' but for endomorphisms.+foldEndo :: Foldable t => t (a -> a) -> a -> a+foldEndo = appEndo . foldMap Endo+++------------------------------------------------------------------------------+-- | Perform an eta reduction. For example, transforms @\x -> (f g) x@ into+-- @f g@.+simplifyEtaReduce :: GenericT+simplifyEtaReduce = mkT $ \case+  Lambda+      [VarPat _ (L _ pat)]+      (HsVar _ (L _ a)) | pat == a ->+    var "id"+  Lambda+      (unsnoc -> Just (pats, (VarPat _ (L _ pat))))+      (HsApp _ (L _ f) (L _ (HsVar _ (L _ a))))+      | pat == a+        -- We can only perform this simplifiation if @pat@ is otherwise unused.+      , not (containsHsVar pat f) ->+    Lambda pats f+  x -> x+++------------------------------------------------------------------------------+-- | Perform an eta-reducing function composition. For example, transforms+-- @\x -> f (g (h x))@ into @f . g . h@.+simplifyCompose :: GenericT+simplifyCompose = mkT $ \case+  Lambda+      (unsnoc -> Just (pats, (VarPat _ (L _ pat))))+      (unroll -> (fs@(_:_), (HsVar _ (L _ a))))+      | pat == a+        -- We can only perform this simplifiation if @pat@ is otherwise unused.+      , not (containsHsVar pat fs) ->+    Lambda pats (foldr1 (infixCall ".") fs)+  x -> x+++------------------------------------------------------------------------------+-- | Removes unnecessary parentheses on any token that doesn't need them.+simplifyRemoveParens :: GenericT+simplifyRemoveParens = mkT $ \case+  HsPar _ (L _ x) | isAtomicHsExpr x -> x+  (x :: HsExpr GhcPs) -> x+++------------------------------------------------------------------------------+-- | Unrolls a right-associative function application of the form+-- @HsApp f (HsApp g (HsApp h x))@ into @([f, g, h], x)@.+unroll :: HsExpr GhcPs -> ([HsExpr GhcPs], HsExpr GhcPs)+unroll (HsPar _ (L _ x)) = unroll x+unroll (HsApp _ (L _ f) (L _ a)) =+  let (fs, r) = unroll a+   in (f : fs, r)+unroll x = ([], x)+

@@ -1,12 +1,7 @@ {-# LANGUAGE TupleSections #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE DeriveGeneric         #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-}-{-# LANGUAGE LambdaCase            #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeSynonymInstances  #-} {-# LANGUAGE ViewPatterns          #-}  module Ide.Plugin.Tactic.Tactics@@ -24,6 +19,7 @@ import           Data.List import qualified Data.Map as M import           Data.Maybe+import           Data.Set (Set) import qualified Data.Set as S import           DataCon import           Development.IDE.GHC.Compat@@ -47,7 +43,7 @@ ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM ()-assumption = attemptOn allNames assume+assumption = attemptOn (S.toList . allNames) assume   ------------------------------------------------------------------------------@@ -55,7 +51,7 @@ assume :: OccName -> TacticsM () assume name = rule $ \jdg -> do   let g  = jGoal jdg-  case M.lookup name $ jHypothesis jdg of+  case M.lookup name $ hyByName $ jHypothesis jdg of     Just (hi_type -> ty) -> do       unify ty $ jGoal jdg       for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion@@ -67,10 +63,10 @@ recursion :: TacticsM () recursion = requireConcreteHole $ tracing "recursion" $ do   defs <- getCurrentDefinitions-  attemptOn (const $ fmap fst defs) $ \name -> do+  attemptOn (const defs) $ \(name, ty) -> do     modify $ pushRecursionStack .  countRecursiveCall     ensure guardStructurallySmallerRecursion popRecursionStack $ do-      (localTactic (apply name) $ introducingRecursively defs)+      (localTactic (apply $ HyInfo name RecursivePrv ty) $ introducingRecursively defs)         <@> fmap (localTactic assumption . filterPosition name) [0..]  @@ -84,7 +80,7 @@   case tcSplitFunTys $ unCType g of     ([], _) -> throwError $ GoalMismatch "intros" g     (as, b) -> do-      vs <- mkManyGoodNames (jEntireHypothesis jdg) as+      vs <- mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as       let top_hole = isTopHole ctx jdg           jdg' = introducingLambda top_hole (zip vs $ coerce as)                $ withNewGoal (CType b) jdg@@ -100,35 +96,32 @@  ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches.-destructAuto :: OccName -> TacticsM ()-destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do+destructAuto :: HyInfo CType -> TacticsM ()+destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do   jdg <- goal-  case M.lookup name $ jHypothesis jdg of-    Nothing -> throwError $ NotInScope name-    Just hi ->-      let subtactic = rule $ destruct' (const subgoal) name-      in case isPatternMatch $ hi_provenance hi of-            True ->-              pruning subtactic $ \jdgs ->-                let getHyTypes = S.fromList . fmap hi_type . M.elems . jHypothesis-                    new_hy = foldMap getHyTypes jdgs-                    old_hy = getHyTypes jdg-                in case S.null $ new_hy S.\\ old_hy of-                      True  -> Just $ UnhelpfulDestruct name-                      False -> Nothing-            False -> subtactic+  let subtactic = rule $ destruct' (const subgoal) hi+  case isPatternMatch $ hi_provenance hi of+    True ->+      pruning subtactic $ \jdgs ->+        let getHyTypes = S.fromList . fmap hi_type . unHypothesis . jHypothesis+            new_hy = foldMap getHyTypes jdgs+            old_hy = getHyTypes jdg+        in case S.null $ new_hy S.\\ old_hy of+              True  -> Just $ UnhelpfulDestruct $ hi_name hi+              False -> Nothing+    False -> subtactic   ------------------------------------------------------------------------------ -- | Case split, and leave holes in the matches.-destruct :: OccName -> TacticsM ()-destruct name = requireConcreteHole $ tracing "destruct(user)" $-  rule $ destruct' (const subgoal) name+destruct :: HyInfo CType -> TacticsM ()+destruct hi = requireConcreteHole $ tracing "destruct(user)" $+  rule $ destruct' (const subgoal) hi   ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches.-homo :: OccName -> TacticsM ()+homo :: HyInfo CType -> TacticsM () homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg ->   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) @@ -152,32 +145,30 @@         $ jGoal jdg  -apply :: OccName -> TacticsM ()-apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do+apply :: HyInfo CType -> TacticsM ()+apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do   jdg <- goal   let hy = jHypothesis jdg       g  = jGoal jdg-  case M.lookup func hy of-    Just (hi_type -> CType ty) -> do-      ty' <- freshTyvars ty-      let (_, _, args, ret) = tacticsSplitFunTy ty'-      requireNewHoles $ rule $ \jdg -> do-        unify g (CType ret)-        useOccName jdg func-        (tr, sgs)-            <- fmap unzipTrace-            $ traverse ( newSubgoal-                        . blacklistingDestruct-                        . flip withNewGoal jdg-                        . CType-                        ) args-        pure-          . (tr, )-          . noLoc-          . foldl' (@@) (var' func)-          $ fmap unLoc sgs-    Nothing -> do-      throwError $ GoalMismatch "apply" g+      ty = unCType $ hi_type hi+      func = hi_name hi+  ty' <- freshTyvars ty+  let (_, _, args, ret) = tacticsSplitFunTy ty'+  requireNewHoles $ rule $ \jdg -> do+    unify g (CType ret)+    useOccName jdg func+    (tr, sgs)+        <- fmap unzipTrace+        $ traverse ( newSubgoal+                    . blacklistingDestruct+                    . flip withNewGoal jdg+                    . CType+                    ) args+    pure+      . (tr, )+      . noLoc+      . foldl' (@@) (var' func)+      $ fmap unLoc sgs   ------------------------------------------------------------------------------@@ -272,16 +263,19 @@     , recursion     ] -overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()+overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM () overFunctions =-  attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . jHypothesis+  attemptOn $ filter (isFunction . unCType . hi_type)+           . unHypothesis+           . jHypothesis -overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()+overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM () overAlgebraicTerms =-  attemptOn $-    M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . jHypothesis+  attemptOn $ filter (isJust . algebraicTyCon . unCType . hi_type)+            . unHypothesis+            . jHypothesis  -allNames :: Judgement -> [OccName]-allNames = M.keys . jHypothesis+allNames :: Judgement -> Set OccName+allNames = hyNamesInScope . jHypothesis 

@@ -3,6 +3,8 @@ module Ide.Plugin.Tactic.TestTypes where  import qualified Data.Text as T+import Data.Aeson+import Ide.Plugin.Tactic.FeatureSet  ------------------------------------------------------------------------------ -- | The list of tactics exposed to the outside world. These are attached to@@ -25,3 +27,24 @@ tacticTitle Homomorphism var = "Homomorphic case split on " <> var tacticTitle DestructLambdaCase _ = "Lambda case split" tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"+++------------------------------------------------------------------------------+-- | Plugin configuration for tactics+newtype Config = Config+  { cfg_feature_set :: FeatureSet+  }++emptyConfig :: Config+emptyConfig = Config defaultFeatures++instance ToJSON Config where+  toJSON (Config features) = object+    [ "features" .= prettyFeatureSet features+    ]++instance FromJSON Config where+  parseJSON = withObject "Config" $ \obj -> do+    features <- parseFeatureSet <$> obj .: "features"+    pure $ Config features+

@@ -1,14 +1,12 @@-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DeriveFunctor              #-} {-# LANGUAGE DeriveGeneric              #-}-{-# LANGUAGE DerivingStrategies         #-}+{-# LANGUAGE DerivingVia                #-}+{-# LANGUAGE FlexibleContexts           #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses      #-}-{-# LANGUAGE TypeSynonymInstances       #-}+{-# LANGUAGE OverloadedStrings          #-}+{-# LANGUAGE TypeApplications           #-} {-# OPTIONS_GHC -fno-warn-orphans       #-}  module Ide.Plugin.Tactic.Types@@ -22,13 +20,12 @@   , Range   ) where -import Control.Lens hiding (Context)+import Control.Lens hiding (Context, (.=)) import Control.Monad.Reader import Control.Monad.State import Data.Coerce import Data.Function import Data.Generics.Product (field)-import Data.Map (Map) import Data.Set (Set) import Data.Tree import Development.IDE.GHC.Compat hiding (Node)@@ -36,6 +33,7 @@ import Development.IDE.Types.Location import GHC.Generics import Ide.Plugin.Tactic.Debug+import Ide.Plugin.Tactic.FeatureSet (FeatureSet) import OccName import Refinery.Tactic import System.IO.Unsafe (unsafePerformIO)@@ -72,12 +70,18 @@ instance Show Class where   show  = unsafeRender +instance Show (HsExpr GhcPs) where+  show  = unsafeRender +instance Show (Pat GhcPs) where+  show  = unsafeRender++ ------------------------------------------------------------------------------ data TacticState = TacticState     { ts_skolems   :: !(Set TyVar)       -- ^ The known skolems.-    , ts_unifier   :: !(TCvSubst)+    , ts_unifier   :: !TCvSubst       -- ^ The current substitution of univars.     , ts_used_vals :: !(Set OccName)       -- ^ Set of values used by tactics.@@ -217,10 +221,18 @@   compare = nonDetCmpUnique `on` getUnique . getViaUnique  +newtype Hypothesis a = Hypothesis+  { unHypothesis :: [HyInfo a]+  }+  deriving stock (Functor, Eq, Show, Generic, Ord)+  deriving newtype (Semigroup, Monoid)++ ------------------------------------------------------------------------------ -- | The provenance and type of a hypothesis term. data HyInfo a = HyInfo-  { hi_provenance :: Provenance+  { hi_name       :: OccName+  , hi_provenance :: Provenance   , hi_type       :: a   }   deriving stock (Functor, Eq, Show, Generic, Ord)@@ -229,17 +241,17 @@ ------------------------------------------------------------------------------ -- | Map a function over the provenance. overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a-overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty+overProvenance f (HyInfo name prv ty) = HyInfo name (f prv) ty   ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. data Judgement' a = Judgement-  { _jHypothesis :: !(Map OccName (HyInfo a))-  , _jBlacklistDestruct :: !(Bool)-  , _jWhitelistSplit :: !(Bool)+  { _jHypothesis :: !(Hypothesis a)+  , _jBlacklistDestruct :: !Bool+  , _jWhitelistSplit :: !Bool   , _jIsTopHole    :: !Bool-  , _jGoal         :: !(a)+  , _jGoal         :: !a   }   deriving stock (Eq, Generic, Functor, Show) @@ -325,14 +337,15 @@     -- ^ The functions currently being defined   , ctxModuleFuncs :: [(OccName, CType)]     -- ^ Everything defined in the current module+  , ctxFeatureSet :: FeatureSet   }-  deriving stock (Eq, Ord)+  deriving stock (Eq, Ord, Show)   ------------------------------------------------------------------------------ -- | An empty context emptyContext :: Context-emptyContext  = Context mempty mempty+emptyContext  = Context mempty mempty mempty   newtype Rose a = Rose (Tree a)@@ -363,5 +376,14 @@   { rtr_trace       :: Trace   , rtr_extract     :: LHsExpr GhcPs   , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]+  , rtr_jdg         :: Judgement+  , rtr_ctx         :: Context   } deriving Show+++data AgdaMatch = AgdaMatch+  { amPats :: [Pat GhcPs]+  , amBody :: HsExpr GhcPs+  }+  deriving (Show) 

@@ -1,122 +0,0 @@-{-# LANGUAGE LambdaCase          #-}-{-# LANGUAGE NamedFieldPuns      #-}-{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE RecordWildCards     #-}-{-# LANGUAGE ScopedTypeVariables #-}--module Ide.TreeTransform-  ( Graft, graft, transform, useAnnotatedSource-  ) where--import           BasicTypes (appPrec)-import           Control.Monad-import           Control.Monad.Trans.Class-import qualified Data.Text as T-import           Development.IDE.Core.RuleTypes-import           Development.IDE.Core.Rules-import           Development.IDE.Core.Shake-import           Development.IDE.GHC.Compat  hiding (parseExpr)-import           Development.IDE.Types.Location-import           Generics.SYB-import           Ide.PluginUtils-import           Language.Haskell.GHC.ExactPrint-import           Language.Haskell.GHC.ExactPrint.Parsers-import           Language.Haskell.LSP.Types-import           Language.Haskell.LSP.Types.Capabilities (ClientCapabilities)-import           Outputable-import           Retrie.ExactPrint hiding (parseExpr)------------------------------------------------------------------------------------ | Get the latest version of the annotated parse source.-useAnnotatedSource-    :: String-    -> IdeState-    -> NormalizedFilePath-    -> IO (Maybe (Annotated ParsedSource))-useAnnotatedSource herald state nfp = do-  pm <- runAction herald state $ use GetParsedModule nfp-  pure $ fmap fixAnns pm------------------------------------------------------------------------------------ | A transformation for grafting source trees together. Use the semigroup--- instance to combine 'Graft's, and run them via 'transform'.-newtype Graft a = Graft-  { runGraft :: DynFlags -> a -> TransformT (Either String) a-  }--instance Semigroup (Graft a) where-  Graft a <> Graft b = Graft $ \dflags -> a dflags >=> b dflags--instance Monoid (Graft a) where-  mempty = Graft $ const pure------------------------------------------------------------------------------------ | Convert a 'Graft' into a 'WorkspaceEdit'.-transform-    :: DynFlags-    -> ClientCapabilities-    -> Uri-    -> Graft ParsedSource-    -> Annotated ParsedSource-    -> Either String WorkspaceEdit-transform dflags ccs uri f a = do-  let src = printA a-  a' <- transformA a $ runGraft f dflags-  let res = printA a'-  pure $ diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions------------------------------------------------------------------------------------ | Construct a 'Graft', replacing the node at the given 'SrcSpan' with the--- given 'LHSExpr'. The node at that position must already be a 'LHsExpr', or--- this is a no-op.-graft-    :: forall a-     . Data a-    => SrcSpan-    -> LHsExpr GhcPs-    -> Graft a-graft dst val = Graft $ \dflags a -> do-  (anns, val') <- annotate dflags $ parenthesize val-  modifyAnnsT $ mappend anns-  pure $ everywhere'-    ( mkT $-        \case-          (L src _ :: LHsExpr GhcPs) | src == dst -> val'-          l -> l-    ) a------------------------------------------------------------------------------------ | Dark magic I stole from retrie. No idea what it does.-fixAnns :: ParsedModule -> Annotated ParsedSource-fixAnns ParsedModule {..} =-  let ranns = relativiseApiAnns pm_parsed_source pm_annotations-   in unsafeMkA pm_parsed_source ranns 0------------------------------------------------------------------------------------ | Given an 'LHSExpr', compute its exactprint annotations.-annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs)-annotate dflags expr = do-  uniq <- show <$> uniqueSrcSpanT-  let rendered = render dflags expr-  (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered-  let anns' = setPrecedingLines expr' 0 1 anns-  pure (anns', expr')------------------------------------------------------------------------------------ | Print out something 'Outputable'.-render :: Outputable a => DynFlags -> a -> String-render dflags = showSDoc dflags . ppr------------------------------------------------------------------------------------ | Put parentheses around an expression if required.-parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs-parenthesize = parenthesizeHsExpr appPrec-

@@ -2,23 +2,17 @@  module AutoTupleSpec where -import           Data.Either (isRight)-import qualified Data.Map as M-import           Ide.Plugin.Tactic.Debug-import           Ide.Plugin.Tactic.Judgements (mkFirstJudgement)-import           Ide.Plugin.Tactic.Machinery-import           Ide.Plugin.Tactic.Tactics (auto')-import           Ide.Plugin.Tactic.Types-import           OccName (mkVarOcc)-import           Test.Hspec-import           Test.QuickCheck-import           Type (mkTyVarTy)-import           TysPrim (alphaTyVars)-import           TysWiredIn (mkBoxedTupleTy)---instance Show Type where-  show = unsafeRender+import Data.Either (isRight)+import Ide.Plugin.Tactic.Judgements (mkFirstJudgement)+import Ide.Plugin.Tactic.Machinery+import Ide.Plugin.Tactic.Tactics (auto')+import Ide.Plugin.Tactic.Types+import OccName (mkVarOcc)+import Test.Hspec+import Test.QuickCheck+import Type (mkTyVarTy)+import TysPrim (alphaTyVars)+import TysWiredIn (mkBoxedTupleTy)   spec :: Spec@@ -42,7 +36,7 @@           runTactic             emptyContext             (mkFirstJudgement-              (M.singleton (mkVarOcc "x") $ HyInfo UserPrv $ CType in_type)+              (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type)               True               out_type)             (auto' $ n * 2) `shouldSatisfy` isRight

@@ -0,0 +1,224 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DuplicateRecordFields #-}+{-# LANGUAGE OverloadedStrings     #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE ViewPatterns          #-}++module GoldenSpec where++import           Control.Applicative.Combinators ( skipManyTill )+import           Control.Lens hiding ((<.>), failing)+import           Control.Monad (unless)+import           Control.Monad.IO.Class+import           Data.Aeson+import           Data.Default (Default(def))+import           Data.Foldable+import qualified Data.Map as M+import           Data.Maybe+import           Data.Text (Text)+import qualified Data.Text.IO as T+import qualified Ide.Plugin.Config as Plugin+import           Ide.Plugin.Tactic.FeatureSet (FeatureSet, allFeatures)+import           Ide.Plugin.Tactic.TestTypes+import           Language.LSP.Test+import           Language.LSP.Types+import           Language.LSP.Types.Lens hiding (id, capabilities, message, executeCommand, applyEdit, rename, line, title, name, actions)+import           System.Directory (doesFileExist)+import           System.FilePath+import           Test.Hspec+++spec :: Spec+spec = do+  describe "code action availability" $ do+    mkTest+      "Produces intros code action"+      "T1.hs" 2 14+      [ (id, Intros, "")+      ]+    mkTest+      "Produces destruct and homomorphism code actions"+      "T2.hs" 2 21+      [ (id, Destruct, "eab")+      , (id, Homomorphism, "eab")+      ]+    mkTest+      "Won't suggest homomorphism on the wrong type"+      "T2.hs" 8 8+      [ (not, Homomorphism, "global")+      ]+    mkTest+      "Won't suggest intros on the wrong type"+      "T2.hs" 8 8+      [ (not, Intros, "")+      ]+    mkTest+      "Produces (homomorphic) lambdacase code actions"+      "T3.hs" 4 24+      [ (id, HomomorphismLambdaCase, "")+      , (id, DestructLambdaCase, "")+      ]+    mkTest+      "Produces lambdacase code actions"+      "T3.hs" 7 13+      [ (id, DestructLambdaCase, "")+      ]+    mkTest+      "Doesn't suggest lambdacase without -XLambdaCase"+      "T2.hs" 11 25+      [ (not, DestructLambdaCase, "")+      ]++  describe "golden tests" $ do+    let goldenTest = mkGoldenTest allFeatures+        autoTest = mkGoldenTest allFeatures Auto ""++    goldenTest Intros "" "GoldenIntros.hs" 2 8+    autoTest "GoldenEitherAuto.hs"        2 11+    autoTest "GoldenJoinCont.hs"          4 12+    autoTest "GoldenIdentityFunctor.hs"   3 11+    autoTest "GoldenIdTypeFam.hs"         7 11+    autoTest "GoldenEitherHomomorphic.hs" 2 15+    autoTest "GoldenNote.hs"              2 8+    autoTest "GoldenPureList.hs"          2 12+    autoTest "GoldenListFmap.hs"          2 12+    autoTest "GoldenFromMaybe.hs"         2 13+    autoTest "GoldenFoldr.hs"             2 10+    autoTest "GoldenSwap.hs"              2 8+    autoTest "GoldenFmapTree.hs"          4 11+    goldenTest Destruct "gadt"+             "GoldenGADTDestruct.hs"      7 17+    goldenTest Destruct "gadt"+             "GoldenGADTDestructCoercion.hs" 8 17+    autoTest "GoldenGADTAuto.hs"    7 13+    autoTest "GoldenSwapMany.hs"    2 12+    autoTest "GoldenBigTuple.hs"    4 12+    autoTest "GoldenShow.hs"        2 10+    autoTest "GoldenShowCompose.hs" 2 15+    autoTest "GoldenShowMapChar.hs" 2 8+    autoTest "GoldenSuperclass.hs"  7 8+    failing "flaky in CI" $+      autoTest "GoldenApplicativeThen.hs" 2 11+    autoTest "GoldenSafeHead.hs"  2 12+    failing "not enough auto gas" $+      autoTest "GoldenFish.hs" 5 18+    autoTest "GoldenArbitrary.hs" 25 13+    autoTest "FmapBoth.hs"        2 12+    autoTest "RecordCon.hs"       7  8+    autoTest "FmapJoin.hs"        2 14+    autoTest "Fgmap.hs"           2 9+    autoTest "FmapJoinInLet.hs"   4 19+    goldenTest Destruct "a"+      "SplitPattern.hs"  7 25+++------------------------------------------------------------------------------+-- | Get a range at the given line and column corresponding to having nothing+-- selected.+--+-- NB: These coordinates are in "file space", ie, 1-indexed.+pointRange :: Int -> Int -> Range+pointRange+  (subtract 1 -> line)+  (subtract 1 -> col) =+    Range (Position line col) (Position line $ col + 1)+++------------------------------------------------------------------------------+-- | Get the title of a code action.+codeActionTitle :: (Command |? CodeAction) -> Maybe Text+codeActionTitle InL{} = Nothing+codeActionTitle (InR(CodeAction title _ _ _ _ _ _)) = Just title+++------------------------------------------------------------------------------+-- | Make a tactic unit test.+mkTest+    :: Foldable t+    => String  -- ^ The test name+    -> FilePath  -- ^ The file to load+    -> Int  -- ^ Cursor line+    -> Int  -- ^ Cursor columnn+    -> t ( Bool -> Bool   -- Use 'not' for actions that shouldnt be present+         , TacticCommand  -- An expected command ...+         , Text           -- ... for this variable+         ) -- ^ A collection of (un)expected code actions.+    -> SpecWith (Arg Bool)+mkTest name fp line col ts = it name $ do+  runSession testCommand fullCaps tacticPath $ do+    doc <- openDoc fp "haskell"+    _ <- waitForDiagnostics+    actions <- getCodeActions doc $ pointRange line col+    let titles = mapMaybe codeActionTitle actions+    for_ ts $ \(f, tc, var) -> do+      let title = tacticTitle tc var+      liftIO $+        (title `elem` titles) `shouldSatisfy` f+++setFeatureSet :: FeatureSet -> Session ()+setFeatureSet features = do+  let unObject (Object obj) = obj+      unObject _ = undefined+      def_config = def :: Plugin.Config+      config =+        def_config+          { Plugin.plugins = M.fromList [("tactics",+              def { Plugin.plcConfig = unObject $ toJSON $+                emptyConfig { cfg_feature_set = features }}+          )] <> Plugin.plugins def_config }++  sendNotification SWorkspaceDidChangeConfiguration $+    DidChangeConfigurationParams $+      toJSON config+++mkGoldenTest+    :: FeatureSet+    -> TacticCommand+    -> Text+    -> FilePath+    -> Int+    -> Int+    -> SpecWith ()+mkGoldenTest features tc occ input line col =+  it (input <> " (golden)") $ do+    runSession testCommand fullCaps tacticPath $ do+      setFeatureSet features+      doc <- openDoc input "haskell"+      _ <- waitForDiagnostics+      actions <- getCodeActions doc $ pointRange line col+      Just (InR CodeAction {_command = Just c})+        <- pure $ find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions+      executeCommand c+      _resp <- skipManyTill anyMessage (message SWorkspaceApplyEdit)+      edited <- documentContents doc+      let expected_name = tacticPath </> input <.> "expected"+      -- Write golden tests if they don't already exist+      liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do+        T.writeFile expected_name edited+      expected <- liftIO $ T.readFile expected_name+      liftIO $ edited `shouldBe` expected+++------------------------------------------------------------------------------+-- | Don't run a test.+failing :: Applicative m => String -> b -> m ()+failing _ _ = pure ()+++tacticPath :: FilePath+tacticPath = "test/golden"+++testCommand :: String+testCommand = "test-server"+++executeCommandWithResp :: Command -> Session (ResponseMessage 'WorkspaceExecuteCommand)+executeCommandWithResp cmd = do+  let args = decode $ encode $ fromJust $ cmd ^. arguments+      execParams = ExecuteCommandParams Nothing (cmd ^. command) args+  request SWorkspaceExecuteCommand execParams+

@@ -0,0 +1,19 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ViewPatterns      #-}++module Main(main) where++import           Data.Default+import           Development.IDE.Main+import qualified Development.IDE.Plugin.HLS.GhcIde as Ghcide+import           Ide.Plugin.Tactic as T+import           Ide.PluginUtils++main :: IO ()+main = defaultMain def+  { argsHlsPlugins = pluginDescToIdePlugins $+    [ T.descriptor "tactic"+    ] <>+    Ghcide.descriptors+  }+