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 = _ +