Skip to content

Commit b4deb4a

Browse files
isovectormergify[bot]
isovector
and
mergify[bot]
authored
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>
1 parent 68c4a90 commit b4deb4a

File tree

6 files changed

+148
-54
lines changed

6 files changed

+148
-54
lines changed

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs‎

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Data.Bool (bool)
1717
import Data.Coerce
1818
import Data.Maybe
1919
import Data.Monoid
20+
import qualified Data.Set as S
2021
import qualified Data.Text as T
2122
import Data.Traversable
2223
import DataCon (dataConName)
@@ -32,7 +33,7 @@ import Prelude hiding (span)
3233
import Wingman.Auto
3334
import Wingman.GHC
3435
import Wingman.Judgements
35-
import Wingman.Machinery (useNameFromHypothesis)
36+
import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons)
3637
import Wingman.Metaprogramming.Parser (parseMetaprogram)
3738
import Wingman.Tactics
3839
import Wingman.Types
@@ -126,7 +127,7 @@ commandProvider DestructLambdaCase =
126127
commandProvider HomomorphismLambdaCase =
127128
requireHoleSort (== Hole) $
128129
requireExtension LambdaCase $
129-
filterGoalType ((== Just True) . lambdaCaseable) $
130+
filterGoalType (liftLambdaCase False homoFilter) $
130131
provide HomomorphismLambdaCase ""
131132
commandProvider DestructAll =
132133
requireHoleSort (== Hole) $
@@ -313,8 +314,20 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
313314
-- | We should show homos only when the goal type is the same as the binding
314315
-- type, and that both are usual algebraic types.
315316
homoFilter :: Type -> Type -> Bool
316-
homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
317-
homoFilter _ _ = False
317+
homoFilter codomain domain =
318+
case uncoveredDataCons domain codomain of
319+
Just s -> S.null s
320+
_ -> False
321+
322+
323+
------------------------------------------------------------------------------
324+
-- | Lift a function of (codomain, domain) over a lambda case.
325+
liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
326+
liftLambdaCase nil f t =
327+
case tacticsSplitFunTy t of
328+
(_, _, arg : _, res) -> f res arg
329+
_ -> nil
330+
318331

319332

320333
------------------------------------------------------------------------------

‎plugins/hls-tactics-plugin/src/Wingman/Machinery.hs‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ import Refinery.Tactic.Internal
3232
import TcType
3333
import Type (tyCoVarsOfTypeWellScoped)
3434
import Wingman.Context (getInstance)
35-
import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst)
35+
import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons)
3636
import Wingman.Judgements
3737
import Wingman.Simplify (simplify)
3838
import Wingman.Types
@@ -412,3 +412,15 @@ getCurrentDefinitions = do
412412
for ctx_funcs $ \res@(occ, _) ->
413413
pure . maybe res (occ,) =<< lookupNameInContext occ
414414

415+
416+
------------------------------------------------------------------------------
417+
-- | Given two types, see if we can construct a homomorphism by mapping every
418+
-- data constructor in the domain to the same in the codomain. This function
419+
-- returns 'Just' when all the lookups succeeded, and a non-empty value if the
420+
-- homomorphism *is not* possible.
421+
uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon))
422+
uncoveredDataCons domain codomain = do
423+
(g_dcs, _) <- tacticsGetDataCons codomain
424+
(hi_dcs, _) <- tacticsGetDataCons domain
425+
pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs)
426+

‎plugins/hls-tactics-plugin/src/Wingman/Tactics.hs‎

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -198,8 +198,23 @@ destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $
198198
------------------------------------------------------------------------------
199199
-- | Case split, using the same data constructor in the matches.
200200
homo :: HyInfo CType -> TacticsM ()
201-
homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->
202-
buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
201+
homo hi = requireConcreteHole . tracing "homo" $ do
202+
jdg <- goal
203+
let g = jGoal jdg
204+
205+
-- Ensure that every data constructor in the domain type is covered in the
206+
-- codomain; otherwise 'homo' will produce an ill-typed program.
207+
case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of
208+
Just uncovered_dcs ->
209+
unless (S.null uncovered_dcs) $
210+
throwError $ TacticPanic "Can't cover every datacon in domain"
211+
_ -> throwError $ TacticPanic "Unable to fetch datacons"
212+
213+
rule
214+
$ destruct'
215+
False
216+
(\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
217+
$ hi
203218

204219

205220
------------------------------------------------------------------------------

‎plugins/hls-tactics-plugin/test/CodeAction/DestructSpec.hs‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,3 +35,81 @@ spec = do
3535
destructTest "a" 7 17 "LayoutSplitPattern"
3636
destructTest "a" 8 26 "LayoutSplitPatSyn"
3737

38+
describe "providers" $ do
39+
mkTest
40+
"Produces destruct and homomorphism code actions"
41+
"T2" 2 21
42+
[ (id, Destruct, "eab")
43+
, (id, Homomorphism, "eab")
44+
, (not, DestructPun, "eab")
45+
]
46+
47+
mkTest
48+
"Won't suggest homomorphism on the wrong type"
49+
"T2" 8 8
50+
[ (not, Homomorphism, "global")
51+
]
52+
53+
mkTest
54+
"Produces (homomorphic) lambdacase code actions"
55+
"T3" 4 24
56+
[ (id, HomomorphismLambdaCase, "")
57+
, (id, DestructLambdaCase, "")
58+
]
59+
60+
mkTest
61+
"Produces lambdacase code actions"
62+
"T3" 7 13
63+
[ (id, DestructLambdaCase, "")
64+
]
65+
66+
mkTest
67+
"Doesn't suggest lambdacase without -XLambdaCase"
68+
"T2" 11 25
69+
[ (not, DestructLambdaCase, "")
70+
]
71+
72+
mkTest
73+
"Doesn't suggest destruct if already destructed"
74+
"ProvideAlreadyDestructed" 6 18
75+
[ (not, Destruct, "x")
76+
]
77+
78+
mkTest
79+
"...but does suggest destruct if destructed in a different branch"
80+
"ProvideAlreadyDestructed" 9 7
81+
[ (id, Destruct, "x")
82+
]
83+
84+
mkTest
85+
"Doesn't suggest destruct on class methods"
86+
"ProvideLocalHyOnly" 2 12
87+
[ (not, Destruct, "mempty")
88+
]
89+
90+
mkTest
91+
"Suggests homomorphism if the domain is bigger than the codomain"
92+
"ProviderHomomorphism" 12 13
93+
[ (id, Homomorphism, "g")
94+
]
95+
96+
mkTest
97+
"Doesn't suggest homomorphism if the domain is smaller than the codomain"
98+
"ProviderHomomorphism" 15 14
99+
[ (not, Homomorphism, "g")
100+
, (id, Destruct, "g")
101+
]
102+
103+
mkTest
104+
"Suggests lambda homomorphism if the domain is bigger than the codomain"
105+
"ProviderHomomorphism" 18 14
106+
[ (id, HomomorphismLambdaCase, "")
107+
]
108+
109+
mkTest
110+
"Doesn't suggest lambda homomorphism if the domain is smaller than the codomain"
111+
"ProviderHomomorphism" 21 15
112+
[ (not, HomomorphismLambdaCase, "")
113+
, (id, DestructLambdaCase, "")
114+
]
115+

‎plugins/hls-tactics-plugin/test/ProviderSpec.hs‎

Lines changed: 1 addition & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -14,55 +14,9 @@ spec = do
1414
"T1" 2 14
1515
[ (id, Intros, "")
1616
]
17-
mkTest
18-
"Produces destruct and homomorphism code actions"
19-
"T2" 2 21
20-
[ (id, Destruct, "eab")
21-
, (id, Homomorphism, "eab")
22-
, (not, DestructPun, "eab")
23-
]
24-
mkTest
25-
"Won't suggest homomorphism on the wrong type"
26-
"T2" 8 8
27-
[ (not, Homomorphism, "global")
28-
]
17+
2918
mkTest
3019
"Won't suggest intros on the wrong type"
3120
"T2" 8 8
3221
[ (not, Intros, "")
3322
]
34-
mkTest
35-
"Produces (homomorphic) lambdacase code actions"
36-
"T3" 4 24
37-
[ (id, HomomorphismLambdaCase, "")
38-
, (id, DestructLambdaCase, "")
39-
]
40-
mkTest
41-
"Produces lambdacase code actions"
42-
"T3" 7 13
43-
[ (id, DestructLambdaCase, "")
44-
]
45-
mkTest
46-
"Doesn't suggest lambdacase without -XLambdaCase"
47-
"T2" 11 25
48-
[ (not, DestructLambdaCase, "")
49-
]
50-
51-
mkTest
52-
"Doesn't suggest destruct if already destructed"
53-
"ProvideAlreadyDestructed" 6 18
54-
[ (not, Destruct, "x")
55-
]
56-
57-
mkTest
58-
"...but does suggest destruct if destructed in a different branch"
59-
"ProvideAlreadyDestructed" 9 7
60-
[ (id, Destruct, "x")
61-
]
62-
63-
mkTest
64-
"Doesn't suggest destruct on class methods"
65-
"ProvideLocalHyOnly" 2 12
66-
[ (not, Destruct, "mempty")
67-
]
68-

‎plugins/hls-tactics-plugin/test/golden/ProviderHomomorphism.hs‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
{-# LANGUAGE GADTs #-}
2+
{-# LANGUAGE LambdaCase #-}
3+
4+
data GADT a where
5+
B1 :: GADT Bool
6+
B2 :: GADT Bool
7+
Int :: GADT Int
8+
Var :: GADT a
9+
10+
11+
hasHomo :: GADT Bool -> GADT a
12+
hasHomo g = _
13+
14+
cantHomo :: GADT a -> GADT Int
15+
cantHomo g = _
16+
17+
hasHomoLam :: GADT Bool -> GADT a
18+
hasHomoLam = _
19+
20+
cantHomoLam :: GADT a -> GADT Int
21+
cantHomoLam = _
22+

0 commit comments

Comments
 (0)