diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,54 @@ +

+Wingman for Haskell +

+ +

 

+ +# 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 " 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 + diff --git a/hls-tactics-plugin.cabal b/hls-tactics-plugin.cabal --- a/hls-tactics-plugin.cabal +++ b/hls-tactics-plugin.cabal @@ -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 diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -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 diff --git a/src/Ide/Plugin/Tactic/CaseSplit.hs b/src/Ide/Plugin/Tactic/CaseSplit.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/CaseSplit.hs @@ -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 + diff --git a/src/Ide/Plugin/Tactic/CodeGen.hs b/src/Ide/Plugin/Tactic/CodeGen.hs --- a/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/src/Ide/Plugin/Tactic/CodeGen.hs @@ -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 "$" diff --git a/src/Ide/Plugin/Tactic/CodeGen/Utils.hs b/src/Ide/Plugin/Tactic/CodeGen/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/CodeGen/Utils.hs @@ -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 "$" + diff --git a/src/Ide/Plugin/Tactic/Context.hs b/src/Ide/Plugin/Tactic/Context.hs --- a/src/Ide/Plugin/Tactic/Context.hs +++ b/src/Ide/Plugin/Tactic/Context.hs @@ -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 - diff --git a/src/Ide/Plugin/Tactic/Debug.hs b/src/Ide/Plugin/Tactic/Debug.hs --- a/src/Ide/Plugin/Tactic/Debug.hs +++ b/src/Ide/Plugin/Tactic/Debug.hs @@ -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 diff --git a/src/Ide/Plugin/Tactic/FeatureSet.hs b/src/Ide/Plugin/Tactic/FeatureSet.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/FeatureSet.hs @@ -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 + diff --git a/src/Ide/Plugin/Tactic/GHC.hs b/src/Ide/Plugin/Tactic/GHC.hs --- a/src/Ide/Plugin/Tactic/GHC.hs +++ b/src/Ide/Plugin/Tactic/GHC.hs @@ -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 + diff --git a/src/Ide/Plugin/Tactic/Judgements.hs b/src/Ide/Plugin/Tactic/Judgements.hs --- a/src/Ide/Plugin/Tactic/Judgements.hs +++ b/src/Ide/Plugin/Tactic/Judgements.hs @@ -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 - diff --git a/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs b/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs --- a/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs +++ b/src/Ide/Plugin/Tactic/KnownStrategies/QuickCheck.hs @@ -1,5 +1,4 @@ {-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE LambdaCase #-} module Ide.Plugin.Tactic.KnownStrategies.QuickCheck where @@ -109,4 +108,3 @@ (n == 1) @@ arbitrary False -> arbitrary - diff --git a/src/Ide/Plugin/Tactic/LanguageServer.hs b/src/Ide/Plugin/Tactic/LanguageServer.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -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 + diff --git a/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs @@ -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 + diff --git a/src/Ide/Plugin/Tactic/Machinery.hs b/src/Ide/Plugin/Tactic/Machinery.hs --- a/src/Ide/Plugin/Tactic/Machinery.hs +++ b/src/Ide/Plugin/Tactic/Machinery.hs @@ -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 - diff --git a/src/Ide/Plugin/Tactic/Naming.hs b/src/Ide/Plugin/Tactic/Naming.hs --- a/src/Ide/Plugin/Tactic/Naming.hs +++ b/src/Ide/Plugin/Tactic/Naming.hs @@ -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 - diff --git a/src/Ide/Plugin/Tactic/Simplify.hs b/src/Ide/Plugin/Tactic/Simplify.hs new file mode 100644 --- /dev/null +++ b/src/Ide/Plugin/Tactic/Simplify.hs @@ -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) + diff --git a/src/Ide/Plugin/Tactic/Tactics.hs b/src/Ide/Plugin/Tactic/Tactics.hs --- a/src/Ide/Plugin/Tactic/Tactics.hs +++ b/src/Ide/Plugin/Tactic/Tactics.hs @@ -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 diff --git a/src/Ide/Plugin/Tactic/TestTypes.hs b/src/Ide/Plugin/Tactic/TestTypes.hs --- a/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/src/Ide/Plugin/Tactic/TestTypes.hs @@ -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 + diff --git a/src/Ide/Plugin/Tactic/Types.hs b/src/Ide/Plugin/Tactic/Types.hs --- a/src/Ide/Plugin/Tactic/Types.hs +++ b/src/Ide/Plugin/Tactic/Types.hs @@ -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) diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs deleted file mode 100644 --- a/src/Ide/TreeTransform.hs +++ /dev/null @@ -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 - diff --git a/test/AutoTupleSpec.hs b/test/AutoTupleSpec.hs --- a/test/AutoTupleSpec.hs +++ b/test/AutoTupleSpec.hs @@ -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 diff --git a/test/GoldenSpec.hs b/test/GoldenSpec.hs new file mode 100644 --- /dev/null +++ b/test/GoldenSpec.hs @@ -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 + diff --git a/test/Server.hs b/test/Server.hs new file mode 100644 --- /dev/null +++ b/test/Server.hs @@ -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 + } +