Intelligent derivations of Semigroup and Monoid for Wingman

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

@@ -9,6 +9,7 @@ module Development.IDE.Core.UseStale
   , unTrack
   , PositionMap
   , TrackedStale (..)
+  , untrackedStaleValue
   , unsafeMkStale
   , unsafeMkCurrent
   , unsafeCopyAge
@@ -85,6 +86,10 @@ instance Functor TrackedStale where
   fmap f (TrackedStale t pm) = TrackedStale (fmap f t) pm
 
 
+untrackedStaleValue :: TrackedStale a -> a
+untrackedStaleValue (TrackedStale ta _) = coerce ta
+
+
 ------------------------------------------------------------------------------
 -- | A class for which 'Tracked' values can be run across a 'PositionMapping'
 -- to change their ages.

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

@@ -142,6 +142,8 @@ test-suite tests
     , lens
     , mtl
     , text
+    , deepseq
+    , tasty-hunit
   build-tool-depends:
       hspec-discover:hspec-discover
   default-language: Haskell2010

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

@@ -16,7 +16,6 @@ import           Control.Monad.State
 import           Data.Bool (bool)
 import           Data.Generics.Labels ()
 import           Data.List
-import           Data.Maybe (mapMaybe)
 import           Data.Monoid (Endo(..))
 import qualified Data.Set as S
 import           Data.Traversable
@@ -58,7 +57,7 @@ destructMatches f scrut t jdg = do
         [] -> throwError $ GoalMismatch "destruct" g
         _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let con = RealDataCon dc
-              ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
+              ev = concatMap mkEvidence $ dataConInstArgTys dc apps
               -- We explicitly do not need to add the method hypothesis to
               -- #syn_scoped
               method_hy = foldMap evidenceToHypothesis ev

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

@@ -1,24 +1,46 @@
 module Wingman.Context where
 
-import Bag
-import Control.Arrow
-import Control.Monad.Reader
-import Development.IDE.GHC.Compat
-import OccName
-import TcRnTypes
-import Wingman.FeatureSet (FeatureSet)
-import Wingman.Types
-
-
-mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context
-mkContext features locals tcg = Context
+import           Bag
+import           Control.Arrow
+import           Control.Monad.Reader
+import           Data.Foldable.Extra (allM)
+import           Data.Maybe (fromMaybe, isJust)
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)
+import           InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
+import           OccName
+import           TcRnTypes
+import           TcType (tcSplitTyConApp, tcSplitPhiTy)
+import           TysPrim (alphaTys)
+import           Wingman.FeatureSet (FeatureSet)
+import           Wingman.Judgements.Theta
+import           Wingman.Types
+
+
+mkContext
+    :: FeatureSet
+    -> [(OccName, CType)]
+    -> TcGblEnv
+    -> ExternalPackageState
+    -> KnownThings
+    -> [Evidence]
+    -> Context
+mkContext features locals tcg eps kt ev = Context
   { ctxDefiningFuncs = locals
   , ctxModuleFuncs = fmap splitId
                    . (getFunBindId =<<)
                    . fmap unLoc
                    . bagToList
                    $ tcg_binds tcg
   , ctxFeatureSet = features
+  , ctxInstEnvs =
+      InstEnvs
+        (eps_inst_env eps)
+        (tcg_inst_env tcg)
+        (tcVisibleOrphanMods tcg)
+  , ctxKnownThings = kt
+  , ctxTheta = evidenceToThetaType ev
   }
 
 
@@ -37,3 +59,55 @@ getFunBindId _ = []
 getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
 getCurrentDefinitions = asks ctxDefiningFuncs
 
+
+------------------------------------------------------------------------------
+-- | Extract something from 'KnownThings'.
+getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a
+getKnownThing f = asks $ f . ctxKnownThings
+
+
+------------------------------------------------------------------------------
+-- | Like 'getInstance', but uses a class from the 'KnownThings'.
+getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))
+getKnownInstance f tys = do
+  cls <- getKnownThing f
+  getInstance cls tys
+
+
+------------------------------------------------------------------------------
+-- | Determine if there is an instance that exists for the given 'Class' at the
+-- specified types. Deeply checks contexts to ensure the instance is actually
+-- real.
+--
+-- If so, this returns a 'PredType' that corresponds to the type of the
+-- dictionary.
+getInstance :: MonadReader Context m => Class -> [Type] -> m (Maybe (Class, PredType))
+getInstance cls tys = do
+  env <- asks ctxInstEnvs
+  let (mres, _, _) = lookupInstEnv False env cls tys
+  case mres of
+    ((inst, mapps) : _) -> do
+      -- Get the instantiated type of the dictionary
+      let df = piResultTys (idType $ is_dfun inst) $ zipWith fromMaybe alphaTys mapps
+      -- pull off its resulting arguments
+      let (theta, df') = tcSplitPhiTy df
+      allM hasClassInstance theta >>= \case
+        True -> pure $ Just (cls, df')
+        False -> pure Nothing
+    _ -> pure Nothing
+
+
+------------------------------------------------------------------------------
+-- | Like 'getInstance', but only returns whether or not it succeeded. Can fail
+-- fast, and uses a cached Theta from the context.
+hasClassInstance :: MonadReader Context m => PredType -> m Bool
+hasClassInstance predty = do
+  theta <- asks ctxTheta
+  case S.member (CType predty) theta of
+    True -> pure True
+    False -> do
+      let (con, apps) = tcSplitTyConApp predty
+      case tyConClass_maybe con of
+        Nothing -> pure False
+        Just cls -> fmap isJust $ getInstance cls apps
+

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

@@ -24,6 +24,7 @@ data Feature
   = FeatureDestructAll
   | FeatureUseDataCon
   | FeatureRefineHole
+  | FeatureKnownMonoid
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 

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

@@ -4,7 +4,9 @@
 module Wingman.GHC where
 
 import           ConLike
+import           Control.Applicative (empty)
 import           Control.Monad.State
+import           Control.Monad.Trans.Maybe (MaybeT(..))
 import           Data.Function (on)
 import           Data.Functor ((<&>))
 import           Data.List (isPrefixOf)
@@ -14,10 +16,14 @@ import           Data.Set (Set)
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
+import           Development.IDE (HscEnvEq (hscEnv))
+import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat
 import           GHC.SourceGen (case', lambda, match)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
+import           GhcPlugins (extractModule, GlobalRdrElt (gre_name))
 import           OccName
+import           TcRnMonad
 import           TcType
 import           TyCoRep
 import           Type
@@ -294,3 +300,40 @@ unXPat (XPat (L _ pat)) = unXPat pat
 #endif
 unXPat pat              = pat
 
+
+------------------------------------------------------------------------------
+-- | Build a 'KnownThings'.
+knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings
+knownThings tcg hscenv= do
+  let cls = knownClass tcg hscenv
+  KnownThings
+    <$> cls (mkClsOcc "Semigroup")
+    <*> cls (mkClsOcc "Monoid")
+
+
+------------------------------------------------------------------------------
+-- | Like 'knownThing' but specialized to classes.
+knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class
+knownClass = knownThing $ \case
+  ATyCon tc -> tyConClass_maybe tc
+  _         -> Nothing
+
+
+------------------------------------------------------------------------------
+-- | Helper function for defining 'knownThings'.
+knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a
+knownThing f tcg hscenv occ = do
+  let modul = extractModule tcg
+      rdrenv = tcg_rdr_env tcg
+
+  case lookupOccEnv rdrenv occ of
+    Nothing -> empty
+    Just elts -> do
+      mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts
+      case mvar of
+        Just tt -> liftMaybe $ f tt
+        _ -> empty
+
+liftMaybe :: Monad m => Maybe a -> MaybeT m a
+liftMaybe a = MaybeT $ pure a
+

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

@@ -7,22 +7,26 @@ module Wingman.Judgements.Theta
   , mkEvidence
   , evidenceToSubst
   , evidenceToHypothesis
+  , evidenceToThetaType
   ) where
 
-import           Data.Maybe (fromMaybe, mapMaybe)
+import           Class (classTyVars)
+import           Control.Applicative (empty)
+import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)
 import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           Generics.SYB hiding (tyConName)
-import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe)
+import           Generics.SYB hiding (tyConName, empty)
+import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
 #if __GLASGOW_HASKELL__ > 806
 import           GhcPlugins (eqTyCon)
 #else
 import           GhcPlugins (nameRdrName, tyConName)
 import           PrelNames (eqTyCon_RDR)
 #endif
 import           TcEvidence
+import           TcType (substTy)
 import           TcType (tcTyConAppTyCon_maybe)
 import           TysPrim (eqPrimTyCon)
 import           Wingman.Machinery
@@ -41,19 +45,31 @@ data Evidence
 
 ------------------------------------------------------------------------------
 -- | Given a 'PredType', pull an 'Evidence' out of it.
-mkEvidence :: PredType -> Maybe Evidence
+mkEvidence :: PredType -> [Evidence]
 mkEvidence (getEqualityTheta -> Just (a, b))
-  = Just $ EqualityOfTypes a b
-mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (isClassTyCon -> True))
-  = Just $ HasInstance inst
-mkEvidence _ = Nothing
+  = pure $ EqualityOfTypes a b
+mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (tyConClass_maybe -> Just cls)) = do
+  (_, apps) <- maybeToList $ splitTyConApp_maybe inst
+  let tvs     = classTyVars cls
+      subst   = zipTvSubst tvs apps
+  sc_ev <- traverse (mkEvidence . substTy subst) $ classSCTheta cls
+  HasInstance inst : sc_ev
+mkEvidence _ = empty
+
+
+------------------------------------------------------------------------------
+-- | Build a set of 'PredType's from the evidence.
+evidenceToThetaType :: [Evidence] -> Set CType
+evidenceToThetaType evs = S.fromList $ do
+  HasInstance t <- evs
+  pure $ CType t
 
 
 ------------------------------------------------------------------------------
 -- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
 getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
 getEvidenceAtHole (unTrack -> dst)
-  = mapMaybe mkEvidence
+  = concatMap mkEvidence
   . (everything (<>) $
         mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)
   . unTrack
@@ -113,6 +129,8 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name
         -- show
       , "showsPrec"
       , "showList"
+        -- monad
+      , "return"
       ]
 
 

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

@@ -3,20 +3,38 @@ module Wingman.KnownStrategies where
 import Control.Monad.Error.Class
 import OccName (mkVarOcc)
 import Refinery.Tactic
-import Wingman.Context (getCurrentDefinitions)
+import Wingman.Context (getCurrentDefinitions, getKnownInstance)
 import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)
 import Wingman.Machinery (tracing)
 import Wingman.Tactics
 import Wingman.Types
+import Wingman.Judgements (jGoal)
+import Data.Foldable (for_)
+import Wingman.FeatureSet
+import Control.Applicative (empty)
+import Control.Monad.Reader.Class (asks)
 
 
 knownStrategies :: TacticsM ()
 knownStrategies = choice
   [ known "fmap" deriveFmap
+  , known "mempty" deriveMempty
   , known "arbitrary" deriveArbitrary
+  , featureGuard FeatureKnownMonoid $ known "<>" deriveMappend
+  , featureGuard FeatureKnownMonoid $ known "mappend" deriveMappend
   ]
 
 
+------------------------------------------------------------------------------
+-- | Guard a tactic behind a feature.
+featureGuard :: Feature -> TacticsM a -> TacticsM a
+featureGuard feat t = do
+  fs <- asks ctxFeatureSet
+  case hasFeature feat fs of
+    True -> t
+    False -> empty
+
+
 known :: String -> TacticsM () -> TacticsM ()
 known name t = do
   getCurrentDefinitions >>= \case
@@ -35,3 +53,45 @@ deriveFmap = do
     , recursion
     ]
 
+
+------------------------------------------------------------------------------
+-- | We derive mappend by binding the arguments, introducing the constructor,
+-- and then calling mappend recursively. At each recursive call, we filter away
+-- any binding that isn't in an analogous position.
+--
+-- The recursive call first attempts to use an instace in scope. If that fails,
+-- it fals back to trying a theta method from the hypothesis with the correct
+-- name.
+deriveMappend :: TacticsM ()
+deriveMappend = do
+  try intros
+  destructAll
+  split
+  g <- goal
+  minst <- getKnownInstance kt_semigroup
+         . pure
+         . unCType
+         $ jGoal g
+  for_ minst $ \(cls, df) -> do
+    restrictPositionForApplication
+      (applyMethod cls df $ mkVarOcc "<>")
+      assumption
+  try $
+    restrictPositionForApplication
+      (applyByName $ mkVarOcc "<>")
+      assumption
+
+
+------------------------------------------------------------------------------
+-- | We derive mempty by introducing the constructor, and then trying to
+-- 'mempty' everywhere. This smaller 'mempty' might come from an instance in
+-- scope, or it might come from the hypothesis theta.
+deriveMempty :: TacticsM ()
+deriveMempty = do
+  split
+  g <- goal
+  minst <- getKnownInstance kt_monoid [unCType $ jGoal g]
+  for_ minst $ \(cls, df) -> do
+    applyMethod cls df $ mkVarOcc "mempty"
+  try assumption
+