Lambda case destruct tactics

Author: isovector

plugins/tactics/src/Ide/Plugin/Tactic.hs

@@ -31,11 +31,11 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
-import           Development.IDE.GHC.Util (hscEnv)
 import           Development.Shake (Action)
+import           DynFlags (xopt)
 import qualified FastString
 import           GHC.Generics (Generic)
-import           HscTypes (hsc_dflags)
+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin (mkLspCommand)
 import           Ide.Plugin.Tactic.BindSites
 import           Ide.Plugin.Tactic.Context
@@ -59,22 +59,17 @@ descriptor plId = (defaultPluginDescriptor plId)
               (tcCommandId tc)
               (tacticDesc $ tcCommandName tc)
               (tacticCmd $ commandTactic tc))
-              enabledTactics
+              [minBound .. maxBound]
     , pluginCodeActionProvider = Just codeActionProvider
     }
 
 tacticDesc :: T.Text -> T.Text
 tacticDesc name = "fill the hole using the " <> name <> " tactic"
 
-------------------------------------------------------------------------------
-
-enabledTactics :: [TacticCommand]
-enabledTactics = [Intros, Destruct, Homomorphism, Auto]
-
 ------------------------------------------------------------------------------
 -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
 -- UI.
-type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
+type TacticProvider = DynFlags -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
 
 
 ------------------------------------------------------------------------------
@@ -93,10 +88,6 @@ tcCommandName = T.pack . show
 -- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
 commandProvider :: TacticCommand -> TacticProvider
 commandProvider Auto  = provide Auto ""
-commandProvider Split = provide Split ""
-commandProvider Intro =
-  filterGoalType isFunction $
-    provide Intro ""
 commandProvider Intros =
   filterGoalType isFunction $
     provide Intros ""
@@ -106,17 +97,25 @@ commandProvider Destruct =
 commandProvider Homomorphism =
   filterBindingType homoFilter $ \occ _ ->
     provide Homomorphism $ T.pack $ occNameString occ
+commandProvider DestructLambdaCase =
+  requireExtension LambdaCase $
+    filterGoalType (isJust . lambdaCaseable) $
+      provide DestructLambdaCase ""
+commandProvider HomomorphismLambdaCase =
+  requireExtension LambdaCase $
+    filterGoalType ((== Just True) . lambdaCaseable) $
+      provide HomomorphismLambdaCase ""
 
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
 commandTactic :: TacticCommand -> OccName -> TacticsM ()
 commandTactic Auto         = const auto
-commandTactic Split        = const split
-commandTactic Intro        = const intro
 commandTactic Intros       = const intros
 commandTactic Destruct     = destruct
 commandTactic Homomorphism = homo
+commandTactic DestructLambdaCase     = const destructLambdaCase
+commandTactic HomomorphismLambdaCase = const homoLambdaCase
 
 
 ------------------------------------------------------------------------------
@@ -143,10 +142,11 @@ codeActionProvider :: CodeActionProvider
 codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right $ List []) $ do
-        (_, _, span, jdg) <- MaybeT $ judgementForHole state nfp range
+        (_, _, span, jdg, dflags) <- MaybeT $ judgementForHole state nfp range
         actions <- lift $
           -- This foldMap is over the function monoid.
-          foldMap commandProvider enabledTactics
+          foldMap commandProvider [minBound .. maxBound]
+            dflags
             plId
             uri
             span
@@ -163,7 +163,7 @@ codeActions = List . fmap CACodeAction
 -- | 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 { file = uri , range = range , var_name = name }
   cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
@@ -174,13 +174,23 @@ provide tc name plId uri range _ = do
     $ Just cmd
 
 
+------------------------------------------------------------------------------
+-- | 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 =
+  case xopt ext dflags of
+    True  -> tp dflags 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 plId uri range jdg =
+filterGoalType p tp dflags plId uri range jdg =
   case p $ unCType $ jGoal jdg of
-    True  -> tp plId uri range jdg
+    True  -> tp dflags plId uri range jdg
     False -> pure []
 
 
@@ -191,12 +201,12 @@ filterBindingType
     :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
-filterBindingType p tp plId uri range jdg =
+filterBindingType p tp dflags plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
    in fmap join $ for (M.toList hy) $ \(occ, CType ty) ->
         case p (unCType g) ty of
-          True  -> tp occ ty plId uri range jdg
+          True  -> tp occ ty dflags plId uri range jdg
           False -> pure []
 
 
@@ -215,14 +225,19 @@ judgementForHole
     :: IdeState
     -> NormalizedFilePath
     -> Range
-    -> IO (Maybe (PositionMapping, BindSites, Range, Judgement))
+    -> IO (Maybe (PositionMapping, BindSites, Range, Judgement, DynFlags))
 judgementForHole state nfp range = runMaybeT $ do
   (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp
   range' <- liftMaybe $ fromCurrentRange amapping range
 
   (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp
   let b2 = bindSites $ refMap asts
 
+  -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
+  -- which don't change very often.
+  (modsum, _) <- MaybeT $ runIde state $ useWithStale GetModSummaryWithoutTimestamps nfp
+  let dflags = ms_hspp_opts modsum
+
   (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast ->
       case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of
         Nothing -> Nothing
@@ -235,24 +250,20 @@ judgementForHole state nfp range = runMaybeT $ do
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
 
   let hyps = hypothesisFromBindings rss binds
-  pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal)
+  pure (amapping, b2, resulting_range, mkFirstJudgement hyps goal, dflags)
 
 
 
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
 tacticCmd tac lf state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri =
       fromMaybeT (Right Null, Nothing) $ do
-        (pos, b2, _, jdg) <- MaybeT $ judgementForHole state nfp range
-        -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags'
-        -- which don't change very often.
-        (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp
+        (pos, b2, _, jdg, dflags) <- MaybeT $ judgementForHole state nfp range
         range' <- liftMaybe $ toCurrentRange pos range
         (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
             -- TODO(sandy): unclear if this span is correct; might be
             -- pointing to the wrong version of the file
-            dflags = hsc_dflags $ hscEnv hscenv
             tcg = fst $ tm_internals_ $ tmrModule tcmod
             ctx = mkContext
                     (mapMaybe (sequenceA . (occName *** coerce)) $ getDefiningBindings b2 span)

plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 module Ide.Plugin.Tactic.CodeGen where
 
 import Control.Monad.Except
@@ -18,35 +19,62 @@ import Name
 import Type hiding (Var)
 
 
+destructMatches
+    :: (DataCon -> Judgement -> Rule)
+       -- ^ How to construct each match
+    -> (Judgement -> Judgement)
+       -- ^ How to derive each match judgement
+    -> CType
+       -- ^ Type being destructed
+    -> Judgement
+    -> RuleM [RawMatch]
+destructMatches f f2 t jdg = do
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case splitTyConApp_maybe $ unCType t of
+    Nothing -> throwError $ GoalMismatch "destruct" g
+    Just (tc, apps) -> do
+      let dcs = tyConDataCons tc
+      case dcs of
+        [] -> throwError $ GoalMismatch "destruct" g
+        _ -> for dcs $ \dc -> do
+          let args = dataConInstArgTys dc apps
+          names <- mkManyGoodNames hy args
+
+          let pat :: Pat GhcPs
+              pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
+                  $ fmap bvar' names
+              j = f2
+                $ introducingPat (zip names $ coerce args)
+                $ withNewGoal g jdg
+          sg <- f dc j
+          pure $ match [pat] $ unLoc sg
+
+
 ------------------------------------------------------------------------------
 -- | Combinator for performign case splitting, and running sub-rules on the
 -- resulting matches.
 destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
 destruct' f term jdg = do
   let hy = jHypothesis jdg
-      g  = jGoal jdg
   case find ((== term) . fst) $ toList hy of
     Nothing -> throwError $ UndefinedHypothesis term
     Just (_, t) ->
-      case splitTyConApp_maybe $ unCType t of
-        Nothing -> throwError $ GoalMismatch "destruct" g
-        Just (tc, apps) ->
-          fmap noLoc $ case' (var' term) <$> do
-            let dcs = tyConDataCons tc
-            case dcs of
-              [] -> throwError $ GoalMismatch "destruct" g
-              _ -> for dcs $ \dc -> do
-                let args = dataConInstArgTys dc apps
-                names <- mkManyGoodNames hy args
+      fmap noLoc $ case' (var' term) <$>
+        destructMatches f (destructing term) t jdg
+
 
-                let pat :: Pat GhcPs
-                    pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
-                        $ fmap bvar' names
-                    j = destructing term
-                      $ introducingPat (zip names $ coerce args)
-                      $ withNewGoal g jdg
-                sg <- f dc j
-                pure $ match [pat] $ unLoc sg
+------------------------------------------------------------------------------
+-- | Combinator for performign case splitting, and running sub-rules on the
+-- resulting matches.
+destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
+destructLambdaCase' f jdg = do
+  let g  = jGoal jdg
+  case splitFunTy_maybe (unCType g) of
+    Just (arg, _) | isAlgType arg ->
+      fmap noLoc $ lambdaCase <$>
+        destructMatches f id (CType arg) jdg
+    _ -> throwError $ GoalMismatch "destructLambdaCase'" g
 
 
 ------------------------------------------------------------------------------

plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs

@@ -2,6 +2,7 @@
 
 module Ide.Plugin.Tactic.GHC where
 
+import Data.Maybe (isJust)
 import TcType
 import TyCoRep
 import TyCon
@@ -54,3 +55,15 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))
   | otherwise = Just tycon
 algebraicTyCon _ = Nothing
 
+------------------------------------------------------------------------------
+-- | Can ths type be lambda-cased?
+--
+-- Return: 'Nothing' if no
+--         @Just False@ if it can't be homomorphic
+--         @Just True@ if it can
+lambdaCaseable :: Type -> Maybe Bool
+lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
+  | isJust (algebraicTyCon arg)
+  = Just $ isJust $ algebraicTyCon res
+lambdaCaseable _ = Nothing
+

plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs

@@ -110,6 +110,19 @@ homo = rule . destruct' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
+------------------------------------------------------------------------------
+-- | LambdaCase split, and leave holes in the matches.
+destructLambdaCase :: TacticsM ()
+destructLambdaCase = rule $ destructLambdaCase' (const subgoal)
+
+
+------------------------------------------------------------------------------
+-- | LambdaCase split, using the same data constructor in the matches.
+homoLambdaCase :: TacticsM ()
+homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
+  buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+
+
 apply' :: OccName -> TacticsM ()
 apply' func = rule $ \jdg -> do
   let hy = jHypothesis jdg

plugins/tactics/src/Ide/Plugin/Tactic/Types.hs

@@ -37,21 +37,21 @@ import           Type
 -- editor via 'commandProvider'.
 data TacticCommand
   = Auto
-  | Split
-  | Intro
   | Intros
   | Destruct
   | Homomorphism
+  | DestructLambdaCase
+  | HomomorphismLambdaCase
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
 tacticTitle :: TacticCommand -> T.Text -> T.Text
 tacticTitle Auto _ = "Auto"
-tacticTitle Split _ = "Auto"
-tacticTitle Intro _ = "Intro"
 tacticTitle Intros _ = "Introduce lambda"
 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"
 
 ------------------------------------------------------------------------------
 -- | A wrapper around 'Type' which supports equality and ordering.