From ab4cdb371bb58f49c4a73572a3249edf82ab0536 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 22 Jun 2021 13:53:04 -0700 Subject: [PATCH 1/3] Ensure homomorphism covers the entire codomain --- .../Wingman/LanguageServer/TacticProviders.hs | 10 +++++++--- .../src/Wingman/Machinery.hs | 14 +++++++++++++- .../hls-tactics-plugin/src/Wingman/Tactics.hs | 19 +++++++++++++++++-- 3 files changed, 37 insertions(+), 6 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index 414388e79e..ba88520900 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 @@ -125,6 +126,7 @@ commandProvider DestructLambdaCase = provide DestructLambdaCase "" commandProvider HomomorphismLambdaCase = requireHoleSort (== Hole) $ + -- TODO(sandy): Needs the new test requireExtension LambdaCase $ filterGoalType ((== Just True) . lambdaCaseable) $ provide HomomorphismLambdaCase "" @@ -313,8 +315,10 @@ 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 ------------------------------------------------------------------------------ diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs index ef5dcaae29..2f9c4bbb18 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 81b429e1cf..b2893e043c 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 ------------------------------------------------------------------------------ From 0907ff2504f85240d76eb79241f0f35fb3d4f455 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 22 Jun 2021 16:22:20 -0700 Subject: [PATCH 2/3] Add tests --- .../test/CodeAction/DestructSpec.hs | 66 +++++++++++++++++++ .../hls-tactics-plugin/test/ProviderSpec.hs | 48 +------------- .../test/golden/ProviderHomomorphism.hs | 15 +++++ 3 files changed, 82 insertions(+), 47 deletions(-) create mode 100644 plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs diff --git a/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs index 31251309a3..3c16d631dd 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs @@ -35,3 +35,69 @@ 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" 11 13 + [ (id, Homomorphism, "g") + ] + + mkTest + "Doesn't suggest homomorphism if the domain is smaller than the codomain" + "ProviderHomomorphism" 14 14 + [ (not, Homomorphism, "g") + , (id, Destruct, "g") + ] + + diff --git a/plugins/hls-tactics-plugin/test/ProviderSpec.hs b/plugins/hls-tactics-plugin/test/ProviderSpec.hs index 0c70b8d9af..7d6d0fcfe6 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 0000000000..5a6b15dd73 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} + +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 = _ + From 3ac810c024702c0a77973b6694ef1a8df6c4cd8b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 22 Jun 2021 16:30:10 -0700 Subject: [PATCH 3/3] Add the same logic to lambda case homomorphism --- .../Wingman/LanguageServer/TacticProviders.hs | 13 +++++++++++-- .../test/CodeAction/DestructSpec.hs | 16 ++++++++++++++-- .../test/golden/ProviderHomomorphism.hs | 9 ++++++++- 3 files changed, 33 insertions(+), 5 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs index ba88520900..656f1d3fa6 100644 --- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs +++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs @@ -126,9 +126,8 @@ commandProvider DestructLambdaCase = provide DestructLambdaCase "" commandProvider HomomorphismLambdaCase = requireHoleSort (== Hole) $ - -- TODO(sandy): Needs the new test requireExtension LambdaCase $ - filterGoalType ((== Just True) . lambdaCaseable) $ + filterGoalType (liftLambdaCase False homoFilter) $ provide HomomorphismLambdaCase "" commandProvider DestructAll = requireHoleSort (== Hole) $ @@ -321,6 +320,16 @@ homoFilter codomain domain = _ -> 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 + + + ------------------------------------------------------------------------------ -- | We should show destruct for bindings only when those bindings have usual -- algebraic types. diff --git a/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs index 3c16d631dd..472f8e8e5c 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs @@ -89,15 +89,27 @@ spec = do mkTest "Suggests homomorphism if the domain is bigger than the codomain" - "ProviderHomomorphism" 11 13 + "ProviderHomomorphism" 12 13 [ (id, Homomorphism, "g") ] mkTest "Doesn't suggest homomorphism if the domain is smaller than the codomain" - "ProviderHomomorphism" 14 14 + "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/golden/ProviderHomomorphism.hs b/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs index 5a6b15dd73..dc096f38f1 100644 --- a/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs +++ b/plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE GADTs #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} data GADT a where B1 :: GADT Bool @@ -13,3 +14,9 @@ hasHomo g = _ cantHomo :: GADT a -> GADT Int cantHomo g = _ +hasHomoLam :: GADT Bool -> GADT a +hasHomoLam = _ + +cantHomoLam :: GADT a -> GADT Int +cantHomoLam = _ +