From 6e3682b8b9618d4f775b4679ff7503719b9e603d Mon Sep 17 00:00:00 2001 From: WorldSEnder Date: Thu, 15 Oct 2020 15:05:05 +0200 Subject: [PATCH 1/2] implement #21 : splitting on datatype One code action per datatype constructor is produced. test cases for splitting don't suggest constructors with hash by default suggesting I# for Int probably is not what you want 99% of the time also reuse tyDataCons, tacname use 'algebraicTyCon' as filter for now --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 49 ++++++++++++------- plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 8 +++ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 23 +++++++-- .../src/Ide/Plugin/Tactic/TestTypes.hs | 2 + test/functional/Tactic.hs | 22 +++++++++ test/testdata/tactic/GoldenSplitPair.hs | 2 + .../tactic/GoldenSplitPair.hs.expected | 2 + test/testdata/tactic/T2.hs | 12 +++++ test/testdata/tactic/T3.hs | 4 +- 9 files changed, 101 insertions(+), 23 deletions(-) create mode 100644 test/testdata/tactic/GoldenSplitPair.hs create mode 100644 test/testdata/tactic/GoldenSplitPair.hs.expected diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index c5744e811a..4458870580 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -26,6 +26,7 @@ import Data.Functor ((<&>)) import Data.Generics.Aliases (mkQ) import Data.Generics.Schemes (everything) import Data.List +import qualified Data.Foldable as F import Data.Map (Map) import qualified Data.Map as M import Data.Maybe @@ -103,6 +104,10 @@ commandProvider Auto = provide Auto "" commandProvider Intros = filterGoalType isFunction $ provide Intros "" +commandProvider Split = + filterGoalType (isJust . algebraicTyCon) $ + foldMapGoalType (F.fold . tyDataCons) $ \dc -> + provide Split $ T.pack $ occNameString $ getOccName dc commandProvider Destruct = filterBindingType destructFilter $ \occ _ -> provide Destruct $ T.pack $ occNameString occ @@ -121,11 +126,12 @@ commandProvider HomomorphismLambdaCase = ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. -commandTactic :: TacticCommand -> OccName -> TacticsM () +commandTactic :: TacticCommand -> String -> TacticsM () commandTactic Auto = const auto commandTactic Intros = const intros -commandTactic Destruct = destruct -commandTactic Homomorphism = homo +commandTactic Split = splitDataCon' . mkDataOcc +commandTactic Destruct = destruct . mkVarOcc +commandTactic Homomorphism = homo . mkVarOcc commandTactic DestructLambdaCase = const destructLambdaCase commandTactic HomomorphismLambdaCase = const homoLambdaCase @@ -196,6 +202,14 @@ requireExtension ext tp dflags plId uri range jdg = False -> pure [] +------------------------------------------------------------------------------ +-- | Create a 'TacticProvider' for each occurance of an 'a' in the foldable container +-- extracted from the goal type. Useful instantiations for 't' include 'Maybe' or '[]'. +foldMapGoalType :: Foldable t => (Type -> t a) -> (a -> TacticProvider) -> TacticProvider +foldMapGoalType f tpa dflags plId uri range jdg = + foldMap tpa (f $ unCType $ jGoal jdg) dflags plId uri range jdg + + ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. @@ -289,7 +303,7 @@ spliceProvenance provs = overProvenance (maybe id const $ M.lookup name provs) hi -tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams +tacticCmd :: (String -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do @@ -298,20 +312,19 @@ tacticCmd tac lf state (TacticParams uri range var_name) 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) + $ tac + $ 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) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index 3b66956257..d267f9497a 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -6,6 +6,7 @@ module Ide.Plugin.Tactic.GHC where import Control.Monad.State +import DataCon import qualified Data.Map as M import Data.Maybe (isJust) import Data.Traversable @@ -148,3 +149,10 @@ getPatName (fromPatCompat -> p0) = #endif _ -> Nothing +------------------------------------------------------------------------------ +-- | What data-constructor, if any, does the type have? +tyDataCons :: Type -> Maybe [DataCon] +tyDataCons g = do + (tc, _) <- splitTyConApp_maybe g + pure $ tyConDataCons tc + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 8f6de3ebce..b9a8f3f785 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -186,10 +186,9 @@ split :: TacticsM () split = tracing "split(user)" $ do jdg <- goal let g = jGoal jdg - case splitTyConApp_maybe $ unCType g of - Nothing -> throwError $ GoalMismatch "split" g - Just (tc, _) -> do - let dcs = tyConDataCons tc + case tyDataCons $ unCType g of + Nothing -> throwError $ GoalMismatch "split(user)" g + Just dcs -> do choice $ fmap splitDataCon dcs @@ -238,6 +237,22 @@ splitDataCon dc = Nothing -> throwError $ GoalMismatch "splitDataCon" g +------------------------------------------------------------------------------ +-- | Attempt to instantiate the named data constructor to solve the goal. +splitDataCon' :: OccName -> TacticsM () +splitDataCon' dcn = do + let tacname = "splitDataCon'(" ++ unsafeRender dcn ++ ")" + jdg <- goal + let g = jGoal jdg + case tyDataCons $ unCType g of + Nothing -> throwError $ GoalMismatch tacname g + Just dcs -> do + let mdc = find ((== dcn) . getOccName) dcs + case mdc of + Nothing -> throwError $ GoalMismatch tacname g + Just dc -> splitDataCon dc + + ------------------------------------------------------------------------------ -- | @matching f@ takes a function from a judgement to a @Tactic@, and -- then applies the resulting @Tactic@. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs index 2ea4b8d06c..431e71c4d1 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs @@ -11,6 +11,7 @@ import qualified Data.Text as T data TacticCommand = Auto | Intros + | Split | Destruct | Homomorphism | DestructLambdaCase @@ -21,6 +22,7 @@ data TacticCommand tacticTitle :: TacticCommand -> T.Text -> T.Text tacticTitle Auto _ = "Attempt to fill hole" tacticTitle Intros _ = "Introduce lambda" +tacticTitle Split cname = "Introduce constructor " <> cname tacticTitle Destruct var = "Case split on " <> var tacticTitle Homomorphism var = "Homomorphic case split on " <> var tacticTitle DestructLambdaCase _ = "Lambda case split" diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index a37474771b..541b6deb4b 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -85,6 +85,27 @@ tests = testGroup "T3.hs" 7 13 [ (id, DestructLambdaCase, "") ] + , ignoreTestBecause "Not implemented, see isovector/haskell-language-server#31" $ mkTest + "Splits Int with I# when -XMagicHash is enabled" + "T3.hs" 10 14 + [ (id, Split, "I#") + ] + , mkTest + "Produces datatype split action for single-constructor types" + "T2.hs" 16 14 + [ (id, Split, "T") + ] + , mkTest + "Produces datatype split action for multiple constructors" + "T2.hs" 21 15 + [ (id, Split, "T21") + , (id, Split, "T22") + ] + , mkTest + "Doesn't suggest MagicHash constructors without -XMagicHash" + "T2.hs" 24 14 + [ (not, Split, "I#") + ] , mkTest "Doesn't suggest lambdacase without -XLambdaCase" "T2.hs" 11 25 @@ -115,6 +136,7 @@ tests = testGroup $ goldenTest "GoldenApplicativeThen.hs" 2 11 Auto "" , goldenTest "GoldenSafeHead.hs" 2 12 Auto "" , expectFail "GoldenFish.hs" 5 18 Auto "" + , goldenTest "GoldenSplitPair.hs" 2 11 Split "(,)" ] diff --git a/test/testdata/tactic/GoldenSplitPair.hs b/test/testdata/tactic/GoldenSplitPair.hs new file mode 100644 index 0000000000..826c7a6609 --- /dev/null +++ b/test/testdata/tactic/GoldenSplitPair.hs @@ -0,0 +1,2 @@ +thePair :: (Int, Int) +thePair = _ diff --git a/test/testdata/tactic/GoldenSplitPair.hs.expected b/test/testdata/tactic/GoldenSplitPair.hs.expected new file mode 100644 index 0000000000..7c6501413c --- /dev/null +++ b/test/testdata/tactic/GoldenSplitPair.hs.expected @@ -0,0 +1,2 @@ +thePair :: (Int, Int) +thePair = (_, _) diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs index 20b1644a8f..c42d50d8da 100644 --- a/test/testdata/tactic/T2.hs +++ b/test/testdata/tactic/T2.hs @@ -10,3 +10,15 @@ foo = _ dontSuggestLambdaCase :: Either a b -> Int dontSuggestLambdaCase = _ +data T = T !(Int, Int) + +suggestCon :: T +suggestCon = _ + +data T2 = T21 Int | T22 Int Int + +suggestCons :: T2 +suggestCons = _ + +suggestInt :: Int +suggestInt = _ diff --git a/test/testdata/tactic/T3.hs b/test/testdata/tactic/T3.hs index 1bb42a9b02..f6f46a6aff 100644 --- a/test/testdata/tactic/T3.hs +++ b/test/testdata/tactic/T3.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase, MagicHash #-} suggestHomomorphicLC :: Either a b -> Either a b suggestHomomorphicLC = _ @@ -6,3 +6,5 @@ suggestHomomorphicLC = _ suggestLC :: Either a b -> Int suggestLC = _ +suggestInt :: Int +suggestInt = _ From e2cc32529a444d071582e370a6cf5736fce0c428 Mon Sep 17 00:00:00 2001 From: WorldSEnder Date: Mon, 26 Oct 2020 00:53:51 +0100 Subject: [PATCH 2/2] fix stack hie --- hie.yaml.stack | 2 +- stack.yaml | 82 +------------------------------------------------- 2 files changed, 2 insertions(+), 82 deletions(-) mode change 100644 => 120000 stack.yaml diff --git a/hie.yaml.stack b/hie.yaml.stack index e9aaa75c39..c406d31a56 100644 --- a/hie.yaml.stack +++ b/hie.yaml.stack @@ -23,7 +23,7 @@ cradle: component: "haskell-language-server:exe:haskell-language-server" - path: "./plugins/tactics/src" - component: "hls-tactics-plugin:lib:hls-tactics-plugin" + component: "hls-tactics-plugin:lib" - path: "./plugins/tactics/test" component: "hls-tactics-plugin:test:tests" diff --git a/stack.yaml b/stack.yaml deleted file mode 100644 index 89fd3d2f96..0000000000 --- a/stack.yaml +++ /dev/null @@ -1,81 +0,0 @@ -resolver: lts-14.27 # Last 8.6.5 - -packages: -- . -- ./ghcide/ -- ./hls-plugin-api -- ./plugins/tactics -- ./plugins/hls-hlint-plugin - -ghc-options: - "$everything": -haddock - -extra-deps: -- aeson-1.5.2.0 -- apply-refact-0.8.2.1 -- ansi-terminal-0.10.3 -- base-compat-0.10.5 -- github: bubba/brittany - commit: c59655f10d5ad295c2481537fc8abf0a297d9d1c -- butcher-1.3.3.1 -- Cabal-3.0.2.0 -- cabal-plan-0.6.2.0 -- clock-0.7.2 -- extra-1.7.3 -- floskell-0.10.4 -- fourmolu-0.2.0.0 -- fuzzy-0.1.0.0 -# - ghcide-0.1.0 -- ghc-check-0.5.0.1 -- ghc-exactprint-0.6.3.2 -- ghc-lib-8.10.2.20200808 -- ghc-lib-parser-8.10.2.20200808 -- ghc-lib-parser-ex-8.10.0.16 -- ghc-source-gen-0.4.0.0 -- haddock-api-2.22.0@rev:1 -- haddock-library-1.8.0 -- haskell-lsp-0.22.0.0 -- haskell-lsp-types-0.22.0.0 -- hie-bios-0.7.1 -- hlint-3.2 -- HsYAML-0.2.1.0@rev:1 -- HsYAML-aeson-0.2.0.0@rev:2 -- implicit-hie-cradle-0.2.0.1 -- implicit-hie-0.1.1.0 -- indexed-profunctors-0.1 -- lens-4.18 -- lsp-test-0.11.0.6 -- monad-dijkstra-0.1.1.2 -- opentelemetry-0.4.2 -- optics-core-0.2 -- optparse-applicative-0.15.1.0 -- ormolu-0.1.3.0 -- parser-combinators-1.2.1 -- primitive-0.7.1.0 -- refinery-0.3.0.0 -- regex-base-0.94.0.0 -- regex-pcre-builtin-0.95.1.1.8.43 -- regex-tdfa-1.3.1.0 -- retrie-0.1.1.1 -- semialign-1.1 -# - github: wz1000/shake -# commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef -- stylish-haskell-0.12.2.0 -- tasty-rerun-1.1.17 -- temporary-1.2.1.1 -- these-1.1.1.1 -- type-equality-1 -- topograph-1 - -flags: - haskell-language-server: - pedantic: true - retrie: - BuildExecutable: false - -# allow-newer: true - -nix: - packages: [ icu libcxx zlib ] - -concurrent-tests: false diff --git a/stack.yaml b/stack.yaml new file mode 120000 index 0000000000..917ab78b91 --- /dev/null +++ b/stack.yaml @@ -0,0 +1 @@ +stack-8.6.5.yaml \ No newline at end of file