Implement Tactic Featuresets (#1398)

* Implement featuresets

* Make Tactics tests run with a full feature set

* Respond to feedback from @wz1000

* Cleanup imports in Types

Co-authored-by: Javier Neira <[email protected]>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

haskell-language-server.cabal

@@ -462,6 +462,7 @@ test-suite func-test
     Splice
     HaddockComments
     Ide.Plugin.Splice.Types
+    Ide.Plugin.Tactic.FeatureSet
     Ide.Plugin.Tactic.TestTypes
     Ide.Plugin.Eval.Types
 

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

@@ -29,6 +29,7 @@ library
     Ide.Plugin.Tactic.CodeGen.Utils
     Ide.Plugin.Tactic.Context
     Ide.Plugin.Tactic.Debug
+    Ide.Plugin.Tactic.FeatureSet
     Ide.Plugin.Tactic.GHC
     Ide.Plugin.Tactic.Judgements
     Ide.Plugin.Tactic.KnownStrategies

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs

@@ -33,6 +33,7 @@ import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
 import           Development.Shake.Classes
 import           Ide.Plugin.Tactic.CaseSplit
+import           Ide.Plugin.Tactic.FeatureSet (hasFeature, Feature (..))
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.LanguageServer
 import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
@@ -66,13 +67,15 @@ descriptor plId = (defaultPluginDescriptor plId)
 
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
-  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
+  | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      features <- getFeatureSet
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range
+        (_, jdg, _, dflags) <- judgementForHole state nfp range features
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound]
             dflags
+            features
             plId
             uri
             range
@@ -84,9 +87,10 @@ codeActionProvider _ _ _ = pure $ Right $ List []
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
 tacticCmd tac state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
+      features <- getFeatureSet
       ccs <- getClientCapabilities
       res <- liftIO $ fromMaybeT (Right Nothing) $ do
-        (range', jdg, ctx, dflags) <- judgementForHole state nfp range
+        (range', jdg, ctx, dflags) <- judgementForHole state nfp range features
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
 

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs

@@ -7,8 +7,6 @@ import           Bag
 import           Control.Arrow
 import           Control.Monad.Reader
 import           Data.List
-import           Data.Map (Map)
-import qualified Data.Map as M
 import           Data.Maybe (mapMaybe)
 import           Data.Set (Set)
 import qualified Data.Set as S
@@ -20,16 +18,18 @@ import           OccName
 import           TcRnTypes
 import           TcType (substTy, tcSplitSigmaTy)
 import           Unify (tcUnifyTy)
+import Ide.Plugin.Tactic.FeatureSet (FeatureSet)
 
 
-mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
-mkContext locals tcg = Context
+mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context
+mkContext features locals tcg = Context
   { ctxDefiningFuncs = locals
   , ctxModuleFuncs = fmap splitId
                    . (getFunBindId =<<)
                    . fmap unLoc
                    . bagToList
                    $ tcg_binds tcg
+  , ctxFeatureSet = features
   }
 
 

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs

@@ -0,0 +1,92 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms   #-}
+{-# LANGUAGE ViewPatterns      #-}
+
+module Ide.Plugin.Tactic.FeatureSet
+  ( Feature (..)
+  , FeatureSet
+  , hasFeature
+  , defaultFeatures
+  , allFeatures
+  , parseFeatureSet
+  , prettyFeatureSet
+  ) where
+
+import           Data.List (intercalate)
+import           Data.Maybe (mapMaybe, listToMaybe)
+import           Data.Set (Set)
+import qualified Data.Set as S
+import qualified Data.Text as T
+
+
+------------------------------------------------------------------------------
+-- | All the available features. A 'FeatureSet' describes the ones currently
+-- available to the user.
+data Feature = CantHaveAnEmptyDataType
+  deriving (Eq, Ord, Show, Read, Enum, Bounded)
+
+
+------------------------------------------------------------------------------
+-- | A collection of enabled features.
+type FeatureSet = Set Feature
+
+
+------------------------------------------------------------------------------
+-- | Parse a feature set.
+parseFeatureSet :: T.Text -> FeatureSet
+parseFeatureSet
+  = mappend defaultFeatures
+  . S.fromList
+  . mapMaybe (readMaybe . mappend featurePrefix . rot13 . T.unpack)
+  . T.split (== '/')
+
+
+------------------------------------------------------------------------------
+-- | Features that are globally enabled for all users.
+defaultFeatures :: FeatureSet
+defaultFeatures = S.fromList
+  [
+  ]
+
+
+------------------------------------------------------------------------------
+-- | All available features.
+allFeatures :: FeatureSet
+allFeatures = S.fromList $ enumFromTo minBound maxBound
+
+
+------------------------------------------------------------------------------
+-- | Pretty print a feature set.
+prettyFeatureSet :: FeatureSet -> String
+prettyFeatureSet
+  = intercalate "/"
+  . fmap (rot13 . drop (length featurePrefix) . show)
+  . S.toList
+
+
+------------------------------------------------------------------------------
+-- | Is a given 'Feature' currently enabled?
+hasFeature :: Feature -> FeatureSet -> Bool
+hasFeature = S.member
+
+
+------------------------------------------------------------------------------
+-- | Like 'read', but not partial.
+readMaybe :: Read a => String -> Maybe a
+readMaybe = fmap fst . listToMaybe . reads
+
+
+featurePrefix :: String
+featurePrefix = "Feature"
+
+
+rot13 :: String -> String
+rot13 = fmap (toEnum . rot13int . fromEnum)
+
+
+rot13int :: Integral a => a -> a
+rot13int x
+  | (fromIntegral x :: Word) - 97 < 26 = 97 + rem (x - 84) 26
+  | (fromIntegral x :: Word) - 65 < 26 = 65 + rem (x - 52) 26
+  | otherwise   = x
+

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE OverloadedStrings   #-}
@@ -8,6 +9,8 @@ module Ide.Plugin.Tactic.LanguageServer where
 import           Control.Arrow
 import           Control.Monad
 import           Control.Monad.Trans.Maybe
+import           Data.Aeson (Value(Object), fromJSON)
+import           Data.Aeson.Types (Result(Success, Error))
 import           Data.Coerce
 import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
@@ -29,12 +32,17 @@ import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
 import           Development.Shake (RuleResult, Action)
 import           Development.Shake.Classes
 import qualified FastString
+import           Ide.Plugin.Config (PluginConfig(plcConfig))
+import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Tactic.Context
+import           Ide.Plugin.Tactic.FeatureSet
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Range
-import           Ide.Plugin.Tactic.TestTypes (TacticCommand)
+import           Ide.Plugin.Tactic.TestTypes (cfg_feature_set, TacticCommand)
 import           Ide.Plugin.Tactic.Types
+import           Ide.PluginUtils (getPluginConfig)
+import           Language.LSP.Server (MonadLsp)
 import           Language.LSP.Types
 import           OccName
 import           Prelude hiding (span)
@@ -69,6 +77,16 @@ runStaleIde
 runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp
 
 
+------------------------------------------------------------------------------
+-- | Get the current feature set from the plugin config.
+getFeatureSet :: MonadLsp Plugin.Config m => m FeatureSet
+getFeatureSet = do
+  pcfg <- getPluginConfig "tactics"
+  pure $ case fromJSON $ Object $ plcConfig pcfg of
+    Success cfg -> cfg_feature_set cfg
+    Error _     -> defaultFeatures
+
+
 getIdeDynflags
     :: IdeState
     -> NormalizedFilePath
@@ -87,8 +105,9 @@ judgementForHole
     :: IdeState
     -> NormalizedFilePath
     -> Range
+    -> FeatureSet
     -> MaybeT IO (Range, Judgement, Context, DynFlags)
-judgementForHole state nfp range = do
+judgementForHole state nfp range features = do
   (asts, amapping) <- runStaleIde state nfp GetHieAst
   case asts of
     HAR _ _  _ _ (HieFromDisk _) -> fail "Need a fresh hie file"
@@ -97,21 +116,22 @@ judgementForHole state nfp range = do
       (tcmod, _) <- runStaleIde state nfp TypeCheck
       (rss, g)   <- liftMaybe $ getSpanAndTypeAtHole amapping range hf
       resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
-      let (jdg, ctx) = mkJudgementAndContext g binds rss tcmod
+      let (jdg, ctx) = mkJudgementAndContext features g binds rss tcmod
       dflags <- getIdeDynflags state nfp
       pure (resulting_range, jdg, ctx, dflags)
 
 
 mkJudgementAndContext
-    :: Type
+    :: FeatureSet
+    -> Type
     -> Bindings
     -> RealSrcSpan
     -> TcModuleResult
     -> (Judgement, Context)
-mkJudgementAndContext g binds rss tcmod = do
+mkJudgementAndContext features g binds rss tcmod = do
       let tcg  = tmrTypechecked tcmod
           tcs = tcg_binds tcg
-          ctx = mkContext
+          ctx = mkContext features
                   (mapMaybe (sequenceA . (occName *** coerce))
                     $ getDefiningBindings binds rss)
                   tcg

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs

@@ -21,9 +21,10 @@ import           Data.Monoid
 import qualified Data.Text as T
 import           Data.Traversable
 import           Development.IDE.GHC.Compat
-import           GHC.Generics (Generic)
+import           GHC.Generics
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin.Tactic.Auto
+import           Ide.Plugin.Tactic.FeatureSet
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Tactics
@@ -77,6 +78,7 @@ commandProvider HomomorphismLambdaCase =
 -- UI.
 type TacticProvider
      = DynFlags
+    -> FeatureSet
     -> PluginId
     -> Uri
     -> Range
@@ -93,23 +95,32 @@ data TacticParams = TacticParams
   deriving anyclass (ToJSON, FromJSON)
 
 
+------------------------------------------------------------------------------
+-- | Restrict a 'TacticProvider', making sure it appears only when the given
+-- 'Feature' is in the feature set.
+requireFeature :: Feature -> TacticProvider -> TacticProvider
+requireFeature f tp dflags fs plId uri range jdg = do
+  guard $ hasFeature f fs
+  tp dflags fs plId uri range jdg
+
+
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 requireExtension :: Extension -> TacticProvider -> TacticProvider
-requireExtension ext tp dflags plId uri range jdg =
+requireExtension ext tp dflags fs plId uri range jdg =
   case xopt ext dflags of
-    True  -> tp dflags plId uri range jdg
+    True  -> tp dflags fs plId uri range jdg
     False -> pure []
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp dflags plId uri range jdg =
+filterGoalType p tp dflags fs plId uri range jdg =
   case p $ unCType $ jGoal jdg of
-    True  -> tp dflags plId uri range jdg
+    True  -> tp dflags fs plId uri range jdg
     False -> pure []
 
 
@@ -120,13 +131,13 @@ filterBindingType
     :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
-filterBindingType p tp dflags plId uri range jdg =
+filterBindingType p tp dflags fs plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
    in fmap join $ for (unHypothesis hy) $ \hi ->
         let ty = unCType $ hi_type hi
          in case p (unCType g) ty of
-              True  -> tp (hi_name hi) ty dflags plId uri range jdg
+              True  -> tp (hi_name hi) ty dflags fs plId uri range jdg
               False -> pure []
 
 
@@ -146,7 +157,7 @@ useNameFromHypothesis f name = do
 -- | Terminal constructor for providing context-sensitive tactics. Tactics
 -- given by 'provide' are always available.
 provide :: TacticCommand -> T.Text -> TacticProvider
-provide tc name _ plId uri range _ = do
+provide tc name _ _ plId uri range _ = do
   let title = tacticTitle tc name
       params = TacticParams { tp_file = uri , tp_range = range , tp_var_name = name }
       cmd = mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])

plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs

@@ -3,6 +3,8 @@
 module Ide.Plugin.Tactic.TestTypes where
 
 import qualified Data.Text as T
+import Data.Aeson
+import Ide.Plugin.Tactic.FeatureSet
 
 ------------------------------------------------------------------------------
 -- | The list of tactics exposed to the outside world. These are attached to
@@ -25,3 +27,24 @@ tacticTitle Destruct var = "Case split on " <> var
 tacticTitle Homomorphism var = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _ = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
+
+
+------------------------------------------------------------------------------
+-- | Plugin configuration for tactics
+newtype Config = Config
+  { cfg_feature_set :: FeatureSet
+  }
+
+emptyConfig :: Config
+emptyConfig = Config defaultFeatures
+
+instance ToJSON Config where
+  toJSON (Config features) = object
+    [ "features" .= prettyFeatureSet features
+    ]
+
+instance FromJSON Config where
+  parseJSON = withObject "Config" $ \obj -> do
+    features <- parseFeatureSet <$> obj .: "features"
+    pure $ Config features
+