Skip to content

Commit c67b233

Browse files
authored
Intelligent derivations of Semigroup and Monoid for Wingman (#1671)
* Derive mempty from in class methods * Derive semigroup too * Add tests * Add tests that check instances defined in the current module * Correctly thread theta and lookup instances * Tidy and haddock * Add a test that already has destructed the args * Add whitespace invariant test machinery * Sort imports
1 parent f31df52 commit c67b233

32 files changed

+508
-48
lines changed

ghcide/src/Development/IDE/Core/UseStale.hs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ module Development.IDE.Core.UseStale
99
, unTrack
1010
, PositionMap
1111
, TrackedStale (..)
12+
, untrackedStaleValue
1213
, unsafeMkStale
1314
, unsafeMkCurrent
1415
, unsafeCopyAge
@@ -85,6 +86,10 @@ instance Functor TrackedStale where
8586
fmap f (TrackedStale t pm) = TrackedStale (fmap f t) pm
8687

8788

89+
untrackedStaleValue :: TrackedStale a -> a
90+
untrackedStaleValue (TrackedStale ta _) = coerce ta
91+
92+
8893
------------------------------------------------------------------------------
8994
-- | A class for which 'Tracked' values can be run across a 'PositionMapping'
9095
-- to change their ages.

plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,8 @@ test-suite tests
142142
, lens
143143
, mtl
144144
, text
145+
, deepseq
146+
, tasty-hunit
145147
build-tool-depends:
146148
hspec-discover:hspec-discover
147149
default-language: Haskell2010

plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ import Control.Monad.State
1616
import Data.Bool (bool)
1717
import Data.Generics.Labels ()
1818
import Data.List
19-
import Data.Maybe (mapMaybe)
2019
import Data.Monoid (Endo(..))
2120
import qualified Data.Set as S
2221
import Data.Traversable
@@ -58,7 +57,7 @@ destructMatches f scrut t jdg = do
5857
[] -> throwError $ GoalMismatch "destruct" g
5958
_ -> fmap unzipTrace $ for dcs $ \dc -> do
6059
let con = RealDataCon dc
61-
ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
60+
ev = concatMap mkEvidence $ dataConInstArgTys dc apps
6261
-- We explicitly do not need to add the method hypothesis to
6362
-- #syn_scoped
6463
method_hy = foldMap evidenceToHypothesis ev
Lines changed: 86 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,46 @@
11
module Wingman.Context where
22

3-
import Bag
4-
import Control.Arrow
5-
import Control.Monad.Reader
6-
import Development.IDE.GHC.Compat
7-
import OccName
8-
import TcRnTypes
9-
import Wingman.FeatureSet (FeatureSet)
10-
import Wingman.Types
11-
12-
13-
mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context
14-
mkContext features locals tcg = Context
3+
import Bag
4+
import Control.Arrow
5+
import Control.Monad.Reader
6+
import Data.Foldable.Extra (allM)
7+
import Data.Maybe (fromMaybe, isJust)
8+
import qualified Data.Set as S
9+
import Development.IDE.GHC.Compat
10+
import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)
11+
import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
12+
import OccName
13+
import TcRnTypes
14+
import TcType (tcSplitTyConApp, tcSplitPhiTy)
15+
import TysPrim (alphaTys)
16+
import Wingman.FeatureSet (FeatureSet)
17+
import Wingman.Judgements.Theta
18+
import Wingman.Types
19+
20+
21+
mkContext
22+
:: FeatureSet
23+
-> [(OccName, CType)]
24+
-> TcGblEnv
25+
-> ExternalPackageState
26+
-> KnownThings
27+
-> [Evidence]
28+
-> Context
29+
mkContext features locals tcg eps kt ev = Context
1530
{ ctxDefiningFuncs = locals
1631
, ctxModuleFuncs = fmap splitId
1732
. (getFunBindId =<<)
1833
. fmap unLoc
1934
. bagToList
2035
$ tcg_binds tcg
2136
, ctxFeatureSet = features
37+
, ctxInstEnvs =
38+
InstEnvs
39+
(eps_inst_env eps)
40+
(tcg_inst_env tcg)
41+
(tcVisibleOrphanMods tcg)
42+
, ctxKnownThings = kt
43+
, ctxTheta = evidenceToThetaType ev
2244
}
2345

2446

@@ -37,3 +59,55 @@ getFunBindId _ = []
3759
getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
3860
getCurrentDefinitions = asks ctxDefiningFuncs
3961

62+
63+
------------------------------------------------------------------------------
64+
-- | Extract something from 'KnownThings'.
65+
getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a
66+
getKnownThing f = asks $ f . ctxKnownThings
67+
68+
69+
------------------------------------------------------------------------------
70+
-- | Like 'getInstance', but uses a class from the 'KnownThings'.
71+
getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))
72+
getKnownInstance f tys = do
73+
cls <- getKnownThing f
74+
getInstance cls tys
75+
76+
77+
------------------------------------------------------------------------------
78+
-- | Determine if there is an instance that exists for the given 'Class' at the
79+
-- specified types. Deeply checks contexts to ensure the instance is actually
80+
-- real.
81+
--
82+
-- If so, this returns a 'PredType' that corresponds to the type of the
83+
-- dictionary.
84+
getInstance :: MonadReader Context m => Class -> [Type] -> m (Maybe (Class, PredType))
85+
getInstance cls tys = do
86+
env <- asks ctxInstEnvs
87+
let (mres, _, _) = lookupInstEnv False env cls tys
88+
case mres of
89+
((inst, mapps) : _) -> do
90+
-- Get the instantiated type of the dictionary
91+
let df = piResultTys (idType $ is_dfun inst) $ zipWith fromMaybe alphaTys mapps
92+
-- pull off its resulting arguments
93+
let (theta, df') = tcSplitPhiTy df
94+
allM hasClassInstance theta >>= \case
95+
True -> pure $ Just (cls, df')
96+
False -> pure Nothing
97+
_ -> pure Nothing
98+
99+
100+
------------------------------------------------------------------------------
101+
-- | Like 'getInstance', but only returns whether or not it succeeded. Can fail
102+
-- fast, and uses a cached Theta from the context.
103+
hasClassInstance :: MonadReader Context m => PredType -> m Bool
104+
hasClassInstance predty = do
105+
theta <- asks ctxTheta
106+
case S.member (CType predty) theta of
107+
True -> pure True
108+
False -> do
109+
let (con, apps) = tcSplitTyConApp predty
110+
case tyConClass_maybe con of
111+
Nothing -> pure False
112+
Just cls -> fmap isJust $ getInstance cls apps
113+

plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ data Feature
2424
= FeatureDestructAll
2525
| FeatureUseDataCon
2626
| FeatureRefineHole
27+
| FeatureKnownMonoid
2728
deriving (Eq, Ord, Show, Read, Enum, Bounded)
2829

2930

plugins/hls-tactics-plugin/src/Wingman/GHC.hs

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,9 @@
44
module Wingman.GHC where
55

66
import ConLike
7+
import Control.Applicative (empty)
78
import Control.Monad.State
9+
import Control.Monad.Trans.Maybe (MaybeT(..))
810
import Data.Function (on)
911
import Data.Functor ((<&>))
1012
import Data.List (isPrefixOf)
@@ -14,10 +16,14 @@ import Data.Set (Set)
1416
import qualified Data.Set as S
1517
import Data.Traversable
1618
import DataCon
19+
import Development.IDE (HscEnvEq (hscEnv))
20+
import Development.IDE.Core.Compile (lookupName)
1721
import Development.IDE.GHC.Compat
1822
import GHC.SourceGen (case', lambda, match)
1923
import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
24+
import GhcPlugins (extractModule, GlobalRdrElt (gre_name))
2025
import OccName
26+
import TcRnMonad
2127
import TcType
2228
import TyCoRep
2329
import Type
@@ -294,3 +300,40 @@ unXPat (XPat (L _ pat)) = unXPat pat
294300
#endif
295301
unXPat pat = pat
296302

303+
304+
------------------------------------------------------------------------------
305+
-- | Build a 'KnownThings'.
306+
knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings
307+
knownThings tcg hscenv= do
308+
let cls = knownClass tcg hscenv
309+
KnownThings
310+
<$> cls (mkClsOcc "Semigroup")
311+
<*> cls (mkClsOcc "Monoid")
312+
313+
314+
------------------------------------------------------------------------------
315+
-- | Like 'knownThing' but specialized to classes.
316+
knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class
317+
knownClass = knownThing $ \case
318+
ATyCon tc -> tyConClass_maybe tc
319+
_ -> Nothing
320+
321+
322+
------------------------------------------------------------------------------
323+
-- | Helper function for defining 'knownThings'.
324+
knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a
325+
knownThing f tcg hscenv occ = do
326+
let modul = extractModule tcg
327+
rdrenv = tcg_rdr_env tcg
328+
329+
case lookupOccEnv rdrenv occ of
330+
Nothing -> empty
331+
Just elts -> do
332+
mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts
333+
case mvar of
334+
Just tt -> liftMaybe $ f tt
335+
_ -> empty
336+
337+
liftMaybe :: Monad m => Maybe a -> MaybeT m a
338+
liftMaybe a = MaybeT $ pure a
339+

plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs

Lines changed: 27 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,22 +7,26 @@ module Wingman.Judgements.Theta
77
, mkEvidence
88
, evidenceToSubst
99
, evidenceToHypothesis
10+
, evidenceToThetaType
1011
) where
1112

12-
import Data.Maybe (fromMaybe, mapMaybe)
13+
import Class (classTyVars)
14+
import Control.Applicative (empty)
15+
import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
1316
import Data.Set (Set)
1417
import qualified Data.Set as S
1518
import Development.IDE.Core.UseStale
1619
import Development.IDE.GHC.Compat
17-
import Generics.SYB hiding (tyConName)
18-
import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe)
20+
import Generics.SYB hiding (tyConName, empty)
21+
import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
1922
#if __GLASGOW_HASKELL__ > 806
2023
import GhcPlugins (eqTyCon)
2124
#else
2225
import GhcPlugins (nameRdrName, tyConName)
2326
import PrelNames (eqTyCon_RDR)
2427
#endif
2528
import TcEvidence
29+
import TcType (substTy)
2630
import TcType (tcTyConAppTyCon_maybe)
2731
import TysPrim (eqPrimTyCon)
2832
import Wingman.Machinery
@@ -41,19 +45,31 @@ data Evidence
4145

4246
------------------------------------------------------------------------------
4347
-- | Given a 'PredType', pull an 'Evidence' out of it.
44-
mkEvidence :: PredType -> Maybe Evidence
48+
mkEvidence :: PredType -> [Evidence]
4549
mkEvidence (getEqualityTheta -> Just (a, b))
46-
= Just $ EqualityOfTypes a b
47-
mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (isClassTyCon -> True))
48-
= Just $ HasInstance inst
49-
mkEvidence _ = Nothing
50+
= pure $ EqualityOfTypes a b
51+
mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (tyConClass_maybe -> Just cls)) = do
52+
(_, apps) <- maybeToList $ splitTyConApp_maybe inst
53+
let tvs = classTyVars cls
54+
subst = zipTvSubst tvs apps
55+
sc_ev <- traverse (mkEvidence . substTy subst) $ classSCTheta cls
56+
HasInstance inst : sc_ev
57+
mkEvidence _ = empty
58+
59+
60+
------------------------------------------------------------------------------
61+
-- | Build a set of 'PredType's from the evidence.
62+
evidenceToThetaType :: [Evidence] -> Set CType
63+
evidenceToThetaType evs = S.fromList $ do
64+
HasInstance t <- evs
65+
pure $ CType t
5066

5167

5268
------------------------------------------------------------------------------
5369
-- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
5470
getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
5571
getEvidenceAtHole (unTrack -> dst)
56-
= mapMaybe mkEvidence
72+
= concatMap mkEvidence
5773
. (everything (<>) $
5874
mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)
5975
. unTrack
@@ -113,6 +129,8 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name
113129
-- show
114130
, "showsPrec"
115131
, "showList"
132+
-- monad
133+
, "return"
116134
]
117135

118136

plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs

Lines changed: 61 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,38 @@ module Wingman.KnownStrategies where
33
import Control.Monad.Error.Class
44
import OccName (mkVarOcc)
55
import Refinery.Tactic
6-
import Wingman.Context (getCurrentDefinitions)
6+
import Wingman.Context (getCurrentDefinitions, getKnownInstance)
77
import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)
88
import Wingman.Machinery (tracing)
99
import Wingman.Tactics
1010
import Wingman.Types
11+
import Wingman.Judgements (jGoal)
12+
import Data.Foldable (for_)
13+
import Wingman.FeatureSet
14+
import Control.Applicative (empty)
15+
import Control.Monad.Reader.Class (asks)
1116

1217

1318
knownStrategies :: TacticsM ()
1419
knownStrategies = choice
1520
[ known "fmap" deriveFmap
21+
, known "mempty" deriveMempty
1622
, known "arbitrary" deriveArbitrary
23+
, featureGuard FeatureKnownMonoid $ known "<>" deriveMappend
24+
, featureGuard FeatureKnownMonoid $ known "mappend" deriveMappend
1725
]
1826

1927

28+
------------------------------------------------------------------------------
29+
-- | Guard a tactic behind a feature.
30+
featureGuard :: Feature -> TacticsM a -> TacticsM a
31+
featureGuard feat t = do
32+
fs <- asks ctxFeatureSet
33+
case hasFeature feat fs of
34+
True -> t
35+
False -> empty
36+
37+
2038
known :: String -> TacticsM () -> TacticsM ()
2139
known name t = do
2240
getCurrentDefinitions >>= \case
@@ -35,3 +53,45 @@ deriveFmap = do
3553
, recursion
3654
]
3755

56+
57+
------------------------------------------------------------------------------
58+
-- | We derive mappend by binding the arguments, introducing the constructor,
59+
-- and then calling mappend recursively. At each recursive call, we filter away
60+
-- any binding that isn't in an analogous position.
61+
--
62+
-- The recursive call first attempts to use an instace in scope. If that fails,
63+
-- it fals back to trying a theta method from the hypothesis with the correct
64+
-- name.
65+
deriveMappend :: TacticsM ()
66+
deriveMappend = do
67+
try intros
68+
destructAll
69+
split
70+
g <- goal
71+
minst <- getKnownInstance kt_semigroup
72+
. pure
73+
. unCType
74+
$ jGoal g
75+
for_ minst $ \(cls, df) -> do
76+
restrictPositionForApplication
77+
(applyMethod cls df $ mkVarOcc "<>")
78+
assumption
79+
try $
80+
restrictPositionForApplication
81+
(applyByName $ mkVarOcc "<>")
82+
assumption
83+
84+
85+
------------------------------------------------------------------------------
86+
-- | We derive mempty by introducing the constructor, and then trying to
87+
-- 'mempty' everywhere. This smaller 'mempty' might come from an instance in
88+
-- scope, or it might come from the hypothesis theta.
89+
deriveMempty :: TacticsM ()
90+
deriveMempty = do
91+
split
92+
g <- goal
93+
minst <- getKnownInstance kt_monoid [unCType $ jGoal g]
94+
for_ minst $ \(cls, df) -> do
95+
applyMethod cls df $ mkVarOcc "mempty"
96+
try assumption
97+

0 commit comments

Comments
 (0)