From 68c4a90a68feb8898f5402a889fbb16affcc8ea8 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 24 Jun 2021 11:36:08 -0700 Subject: [PATCH 1/5] Fix nix.yaml (#1974) Our old cachix install URL got garbage collected. --- .github/workflows/nix.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 4e16290ecf4..3bc009c411d 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -44,7 +44,7 @@ jobs: - if: ${{ needs.pre_job.outputs.should_skip_develop != 'true' }} uses: cachix/install-nix-action@v13 with: - install_url: https://nixos-nix-install-tests.cachix.org/serve/lb41az54kzk6j12p81br4bczary7m145/install + install_url: https://nixos-nix-install-tests.cachix.org/serve/i6laym9jw3wg9mw6ncyrk6gjx4l34vvx/install install_options: '--tarball-url-prefix https://nixos-nix-install-tests.cachix.org/serve' extra_nix_config: | experimental-features = nix-command flakes @@ -81,7 +81,7 @@ jobs: submodules: true - uses: cachix/install-nix-action@v13 with: - install_url: https://nixos-nix-install-tests.cachix.org/serve/lb41az54kzk6j12p81br4bczary7m145/install + install_url: https://nixos-nix-install-tests.cachix.org/serve/i6laym9jw3wg9mw6ncyrk6gjx4l34vvx/install install_options: '--tarball-url-prefix https://nixos-nix-install-tests.cachix.org/serve' extra_nix_config: | experimental-features = nix-command flakes From b4deb4aac85f4c468d038e5390ad96cbb7afc2db Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 24 Jun 2021 17:10:26 -0700 Subject: [PATCH 2/5] Wingman: Ensure homomorphic destruct covers all constructors in the domain (#1968) * Ensure homomorphism covers the entire codomain * Add tests * Add the same logic to lambda case homomorphism Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- .../Wingman/LanguageServer/TacticProviders.hs | 21 ++++- .../src/Wingman/Machinery.hs | 14 +++- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 19 ++++- .../test/CodeAction/DestructSpec.hs | 78 +++++++++++++++++++ .../hls-tactics-plugin/test/ProviderSpec.hs | 48 +----------- .../test/golden/ProviderHomomorphism.hs | 22 ++++++ 6 files changed, 148 insertions(+), 54 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index 414388e79ef..656f1d3fa65 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -17,6 +17,7 @@ import Data.Bool (bool) import Data.Coerce import Data.Maybe import Data.Monoid +import qualified Data.Set as S import qualified Data.Text as T import Data.Traversable import DataCon (dataConName) @@ -32,7 +33,7 @@ import Prelude hiding (span) import Wingman.Auto import Wingman.GHC import Wingman.Judgements -import Wingman.Machinery (useNameFromHypothesis) +import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons) import Wingman.Metaprogramming.Parser (parseMetaprogram) import Wingman.Tactics import Wingman.Types @@ -126,7 +127,7 @@ commandProvider DestructLambdaCase = commandProvider HomomorphismLambdaCase = requireHoleSort (== Hole) $ requireExtension LambdaCase $ - filterGoalType ((== Just True) . lambdaCaseable) $ + filterGoalType (liftLambdaCase False homoFilter) $ provide HomomorphismLambdaCase "" commandProvider DestructAll = requireHoleSort (== Hole) $ @@ -313,8 +314,20 @@ 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 +homoFilter codomain domain = + case uncoveredDataCons domain codomain of + Just s -> S.null s + _ -> False + + +------------------------------------------------------------------------------ +-- | Lift a function of (codomain, domain) over a lambda case. +liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r +liftLambdaCase nil f t = + case tacticsSplitFunTy t of + (_, _, arg : _, res) -> f res arg + _ -> nil + ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index ef5dcaae293..2f9c4bbb185 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs @@ -32,7 +32,7 @@ import Refinery.Tactic.Internal import TcType import Type (tyCoVarsOfTypeWellScoped) import Wingman.Context (getInstance) -import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst) +import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons) import Wingman.Judgements import Wingman.Simplify (simplify) import Wingman.Types @@ -412,3 +412,15 @@ getCurrentDefinitions = do for ctx_funcs $ \res@(occ, _) -> pure . maybe res (occ,) =<< lookupNameInContext occ + +------------------------------------------------------------------------------ +-- | Given two types, see if we can construct a homomorphism by mapping every +-- data constructor in the domain to the same in the codomain. This function +-- returns 'Just' when all the lookups succeeded, and a non-empty value if the +-- homomorphism *is not* possible. +uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon)) +uncoveredDataCons domain codomain = do + (g_dcs, _) <- tacticsGetDataCons codomain + (hi_dcs, _) <- tacticsGetDataCons domain + pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs) + diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index 81b429e1cf9..b2893e043cc 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -198,8 +198,23 @@ destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $ ------------------------------------------------------------------------------ -- | Case split, using the same data constructor in the matches. homo :: HyInfo CType -> TacticsM () -homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg -> - buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) +homo hi = requireConcreteHole . tracing "homo" $ do + jdg <- goal + let g = jGoal jdg + + -- Ensure that every data constructor in the domain type is covered in the + -- codomain; otherwise 'homo' will produce an ill-typed program. + case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of + Just uncovered_dcs -> + unless (S.null uncovered_dcs) $ + throwError $ TacticPanic "Can't cover every datacon in domain" + _ -> throwError $ TacticPanic "Unable to fetch datacons" + + rule + $ destruct' + False + (\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg) + $ hi ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs index 31251309a37..472f8e8e5c6 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs @@ -35,3 +35,81 @@ spec = do destructTest "a" 7 17 "LayoutSplitPattern" destructTest "a" 8 26 "LayoutSplitPatSyn" + describe "providers" $ do + mkTest + "Produces destruct and homomorphism code actions" + "T2" 2 21 + [ (id, Destruct, "eab") + , (id, Homomorphism, "eab") + , (not, DestructPun, "eab") + ] + + mkTest + "Won't suggest homomorphism on the wrong type" + "T2" 8 8 + [ (not, Homomorphism, "global") + ] + + mkTest + "Produces (homomorphic) lambdacase code actions" + "T3" 4 24 + [ (id, HomomorphismLambdaCase, "") + , (id, DestructLambdaCase, "") + ] + + mkTest + "Produces lambdacase code actions" + "T3" 7 13 + [ (id, DestructLambdaCase, "") + ] + + mkTest + "Doesn't suggest lambdacase without -XLambdaCase" + "T2" 11 25 + [ (not, DestructLambdaCase, "") + ] + + mkTest + "Doesn't suggest destruct if already destructed" + "ProvideAlreadyDestructed" 6 18 + [ (not, Destruct, "x") + ] + + mkTest + "...but does suggest destruct if destructed in a different branch" + "ProvideAlreadyDestructed" 9 7 + [ (id, Destruct, "x") + ] + + mkTest + "Doesn't suggest destruct on class methods" + "ProvideLocalHyOnly" 2 12 + [ (not, Destruct, "mempty") + ] + + mkTest + "Suggests homomorphism if the domain is bigger than the codomain" + "ProviderHomomorphism" 12 13 + [ (id, Homomorphism, "g") + ] + + mkTest + "Doesn't suggest homomorphism if the domain is smaller than the codomain" + "ProviderHomomorphism" 15 14 + [ (not, Homomorphism, "g") + , (id, Destruct, "g") + ] + + mkTest + "Suggests lambda homomorphism if the domain is bigger than the codomain" + "ProviderHomomorphism" 18 14 + [ (id, HomomorphismLambdaCase, "") + ] + + mkTest + "Doesn't suggest lambda homomorphism if the domain is smaller than the codomain" + "ProviderHomomorphism" 21 15 + [ (not, HomomorphismLambdaCase, "") + , (id, DestructLambdaCase, "") + ] + diff --git a/plugins/hls-tactics-plugin/test/ProviderSpec.hs b/plugins/hls-tactics-plugin/test/ProviderSpec.hs index 0c70b8d9af0..7d6d0fcfe6b 100644 --- a/plugins/hls-tactics-plugin/test/ProviderSpec.hs +++ b/plugins/hls-tactics-plugin/test/ProviderSpec.hs @@ -14,55 +14,9 @@ spec = do "T1" 2 14 [ (id, Intros, "") ] - mkTest - "Produces destruct and homomorphism code actions" - "T2" 2 21 - [ (id, Destruct, "eab") - , (id, Homomorphism, "eab") - , (not, DestructPun, "eab") - ] - mkTest - "Won't suggest homomorphism on the wrong type" - "T2" 8 8 - [ (not, Homomorphism, "global") - ] + mkTest "Won't suggest intros on the wrong type" "T2" 8 8 [ (not, Intros, "") ] - mkTest - "Produces (homomorphic) lambdacase code actions" - "T3" 4 24 - [ (id, HomomorphismLambdaCase, "") - , (id, DestructLambdaCase, "") - ] - mkTest - "Produces lambdacase code actions" - "T3" 7 13 - [ (id, DestructLambdaCase, "") - ] - mkTest - "Doesn't suggest lambdacase without -XLambdaCase" - "T2" 11 25 - [ (not, DestructLambdaCase, "") - ] - - mkTest - "Doesn't suggest destruct if already destructed" - "ProvideAlreadyDestructed" 6 18 - [ (not, Destruct, "x") - ] - - mkTest - "...but does suggest destruct if destructed in a different branch" - "ProvideAlreadyDestructed" 9 7 - [ (id, Destruct, "x") - ] - - mkTest - "Doesn't suggest destruct on class methods" - "ProvideLocalHyOnly" 2 12 - [ (not, Destruct, "mempty") - ] - diff --git a/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs b/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs new file mode 100644 index 00000000000..dc096f38f1a --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} + +data GADT a where + B1 :: GADT Bool + B2 :: GADT Bool + Int :: GADT Int + Var :: GADT a + + +hasHomo :: GADT Bool -> GADT a +hasHomo g = _ + +cantHomo :: GADT a -> GADT Int +cantHomo g = _ + +hasHomoLam :: GADT Bool -> GADT a +hasHomoLam = _ + +cantHomoLam :: GADT a -> GADT Int +cantHomoLam = _ + From 505f777c3a65b70636ed81b08c94e193d42d4dae Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 24 Jun 2021 19:25:18 -0700 Subject: [PATCH 3/5] Add the correct file offset to metaprogram parse errors (#1967) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- .../src/Wingman/LanguageServer/Metaprogram.hs | 5 +++-- .../src/Wingman/Metaprogramming/Parser.hs | 21 ++++++++++++++++--- 2 files changed, 21 insertions(+), 5 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs index 6b924a80608..915724f1aa4 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs @@ -22,7 +22,7 @@ import Development.IDE.Core.RuleTypes import Development.IDE.Core.Shake (IdeState (..)) import Development.IDE.Core.UseStale import Development.IDE.GHC.Compat -import GhcPlugins (containsSpan, realSrcLocSpan) +import GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart) import Ide.Types import Language.LSP.Types import Prelude hiding (span) @@ -50,8 +50,9 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of Just (trss, program) -> do let tr_range = fmap realSrcSpanToRange trss + rsl = realSrcSpanStart $ unTrack trss HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg - z <- liftIO $ attempt_it ctx jdg $ T.unpack program + z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program pure $ Hover { _contents = HoverContents $ MarkupContent MkMarkdown diff --git a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs index b03ea3f0e04..8ebf7a9d150 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs @@ -21,6 +21,8 @@ import Wingman.Metaprogramming.Parser.Documentation import Wingman.Metaprogramming.ProofState (proofState, layout) import Wingman.Tactics import Wingman.Types +import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile) +import FastString (unpackFS) nullary :: T.Text -> TacticsM () -> Parser (TacticsM ()) @@ -421,17 +423,30 @@ wrapError :: String -> String wrapError err = "```\n" <> err <> "\n```\n" +fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b +fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s)) + = P.ParseErrorBundle ne + $ P.PosState a n + (P.SourcePos + (unpackFS $ srcLocFile rsl) + ((<>) line $ P.mkPos $ srcLocLine rsl - 1) + ((<>) col $ P.mkPos $ srcLocCol rsl - 1 + length @[] "[wingman|") + ) + pos + s + ------------------------------------------------------------------------------ -- | Attempt to run a metaprogram tactic, returning the proof state, or the -- errors. attempt_it - :: Context + :: RealSrcLoc + -> Context -> Judgement -> String -> IO (Either String String) -attempt_it ctx jdg program = +attempt_it rsl ctx jdg program = case P.runParser tacticProgram "" (T.pack program) of - Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty peb + Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb Right tt -> do res <- runTactic ctx From cea1d7936b5c1d0a1e903e315940e500aed22a0c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 24 Jun 2021 21:10:02 -0700 Subject: [PATCH 4/5] Don't introduce too many variables (#1961) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 16 +++++++++------- .../test/CodeAction/RunMetaprogramSpec.hs | 1 + .../test/golden/IntrosTooMany.expected.hs | 2 ++ .../test/golden/IntrosTooMany.hs | 2 ++ 4 files changed, 14 insertions(+), 7 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs index b2893e043cc..a78d0c4f05a 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs @@ -127,21 +127,23 @@ intros' names = rule $ \jdg -> do let g = jGoal jdg case tacticsSplitFunTy $ unCType g of (_, _, [], _) -> throwError $ GoalMismatch "intros" g - (_, _, as, b) -> do + (_, _, args, res) -> do ctx <- ask - let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names - num_args = length vs + let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names + num_occs = length occs top_hole = isTopHole ctx jdg - hy' = lambdaHypothesis top_hole $ zip vs $ coerce as + bindings = zip occs $ coerce args + bound_occs = fmap fst bindings + hy' = lambdaHypothesis top_hole bindings jdg' = introduce ctx hy' - $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg + $ withNewGoal (CType $ mkFunTys' (drop num_occs args) res) jdg ext <- newSubgoal jdg' pure $ ext - & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") + & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show bound_occs) <> "}") . pure & #syn_scoped <>~ hy' - & #syn_val %~ noLoc . lambda (fmap bvar' vs) . unLoc + & #syn_val %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs index 03efe5c2660..2c0e44b5bc7 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs @@ -38,4 +38,5 @@ spec = do metaTest 4 28 "MetaUseSymbol" metaTest 7 53 "MetaDeepOf" metaTest 2 34 "MetaWithArg" + metaTest 2 12 "IntrosTooMany" diff --git a/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs new file mode 100644 index 00000000000..0deb964ab6d --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs @@ -0,0 +1,2 @@ +too_many :: a -> b -> c +too_many a b = _ diff --git a/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs new file mode 100644 index 00000000000..066f123a478 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs @@ -0,0 +1,2 @@ +too_many :: a -> b -> c +too_many = [wingman| intros a b c d e f g h i j k l m n o p q r s t u v w x y z |] From a1e719356337a0398a9841b61aa363a6f208246c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 24 Jun 2021 22:39:03 -0700 Subject: [PATCH 5/5] Don't suggest empty case lenses for case exprs with no data cons (#1962) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com> --- .../hls-tactics-plugin/src/Wingman/EmptyCase.hs | 15 +++++++++------ .../test/CodeLens/EmptyCaseSpec.hs | 4 ++++ plugins/hls-tactics-plugin/test/Utils.hs | 16 ++++++++++++++-- .../test/golden/EmptyCaseSpuriousGADT.hs | 8 ++++++++ 4 files changed, 35 insertions(+), 8 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/EmptyCaseSpuriousGADT.hs diff --git a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs index 70877096073..8335642a4eb 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs @@ -150,16 +150,19 @@ emptyCaseScrutinees state nfp = do hscenv <- stale GhcSessionDeps let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg - for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do + fmap catMaybes $ for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do ty <- MaybeT . fmap (scrutinzedType <=< sequence) . traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg') $ scrutinee - case ss of - RealSrcSpan r -> do - rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r - pure (rss', ty) - UnhelpfulSpan _ -> empty + case null $ tacticsGetDataCons ty of + True -> pure empty + False -> + case ss of + RealSrcSpan r -> do + rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r + pure $ Just (rss', ty) + UnhelpfulSpan _ -> empty data EmptyCaseSort a = EmptyCase a diff --git a/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs b/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs index ce7a6b60df4..9ebf7d5043a 100644 --- a/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs @@ -9,6 +9,7 @@ import Utils spec :: Spec spec = do let test = mkCodeLensTest + noTest = mkNoCodeLensTest describe "golden" $ do test "EmptyCaseADT" @@ -19,3 +20,6 @@ spec = do test "EmptyCaseGADT" test "EmptyCaseLamCase" + describe "no code lenses" $ do + noTest "EmptyCaseSpuriousGADT" + diff --git a/plugins/hls-tactics-plugin/test/Utils.hs b/plugins/hls-tactics-plugin/test/Utils.hs index c1832503a63..26cfc343d1f 100644 --- a/plugins/hls-tactics-plugin/test/Utils.hs +++ b/plugins/hls-tactics-plugin/test/Utils.hs @@ -15,12 +15,10 @@ import Control.Monad.IO.Class import Data.Aeson import Data.Foldable import Data.Function (on) -import qualified Data.Map as M import Data.Maybe import Data.Text (Text) import qualified Data.Text as T import qualified Data.Text.IO as T -import qualified Ide.Plugin.Config as Plugin import Ide.Plugin.Tactic as Tactic import Language.LSP.Types import Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title) @@ -129,6 +127,20 @@ mkCodeLensTest input = liftIO $ edited `shouldBe` expected +------------------------------------------------------------------------------ +-- | A test that no code lenses can be run in the file +mkNoCodeLensTest + :: FilePath + -> SpecWith () +mkNoCodeLensTest input = + it (input <> " (no code lenses)") $ do + runSessionWithServer plugin tacticPath $ do + doc <- openDoc (input <.> "hs") "haskell" + _ <- waitForDiagnostics + lenses <- fmap (reverse . filter isWingmanLens) $ getCodeLenses doc + liftIO $ lenses `shouldBe` [] + + isWingmanLens :: CodeLens -> Bool isWingmanLens (CodeLens _ (Just (Command _ cmd _)) _) diff --git a/plugins/hls-tactics-plugin/test/golden/EmptyCaseSpuriousGADT.hs b/plugins/hls-tactics-plugin/test/golden/EmptyCaseSpuriousGADT.hs new file mode 100644 index 00000000000..25906fe536e --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/EmptyCaseSpuriousGADT.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE GADTs #-} + +data Foo a where + Foo :: Foo Int + +foo :: Foo Bool -> () +foo x = case x of +