From 5ab841911d54499067f05ca4cb12f4190369cd9e Mon Sep 17 00:00:00 2001 From: WorldSEnder Date: Thu, 15 Oct 2020 15:05:05 +0200 Subject: [PATCH 1/4] implement #21 : splitting on datatype One code action per datatype constructor is produced. --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 22 ++++++++++++++----- plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 9 ++++++++ .../tactics/src/Ide/Plugin/Tactic/Tactics.hs | 21 +++++++++++++++--- .../src/Ide/Plugin/Tactic/TestTypes.hs | 2 ++ test/functional/Tactic.hs | 5 +++++ test/testdata/tactic/T2.hs | 4 ++++ 6 files changed, 55 insertions(+), 8 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 199cc1a609..9ebd450d25 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -20,6 +20,7 @@ import Control.Monad.Trans import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce +import qualified Data.Foldable as F import qualified Data.Map as M import Data.Maybe import qualified Data.Set as S @@ -92,6 +93,9 @@ commandProvider Auto = provide Auto "" commandProvider Intros = filterGoalType isFunction $ provide Intros "" +commandProvider Split = + foldMapGoalType (F.fold . tyDataCons) $ \dc -> + provide Split $ T.pack $ occNameString $ getOccName dc commandProvider Destruct = filterBindingType destructFilter $ \occ _ -> provide Destruct $ T.pack $ occNameString occ @@ -110,11 +114,12 @@ commandProvider HomomorphismLambdaCase = ------------------------------------------------------------------------------ -- | A mapping from tactic commands to actual tactics for refinery. -commandTactic :: TacticCommand -> OccName -> TacticsM () +commandTactic :: TacticCommand -> String -> TacticsM () commandTactic Auto = const auto commandTactic Intros = const intros -commandTactic Destruct = destruct -commandTactic Homomorphism = homo +commandTactic Split = splitDataCon' . mkDataOcc +commandTactic Destruct = destruct . mkVarOcc +commandTactic Homomorphism = homo . mkVarOcc commandTactic DestructLambdaCase = const destructLambdaCase commandTactic HomomorphismLambdaCase = const homoLambdaCase @@ -185,6 +190,14 @@ requireExtension ext tp dflags plId uri range jdg = False -> pure [] +------------------------------------------------------------------------------ +-- | Create a 'TacticProvider' for each occurance of an 'a' in the foldable container +-- extracted from the goal type. Useful instantiations for 't' include 'Maybe' or '[]'. +foldMapGoalType :: Foldable t => (Type -> t a) -> (a -> TacticProvider) -> TacticProvider +foldMapGoalType f tpa dflags plId uri range jdg = + foldMap tpa (f $ unCType $ jGoal jdg) dflags plId uri range jdg + + ------------------------------------------------------------------------------ -- | Restrict a 'TacticProvider', making sure it appears only when the given -- predicate holds for the goal. @@ -259,7 +272,7 @@ judgementForHole state nfp range = do -tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams +tacticCmd :: (String -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do @@ -268,7 +281,6 @@ tacticCmd tac lf state (TacticParams uri range var_name) pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic ctx jdg $ tac - $ mkVarOcc $ T.unpack var_name of Left err -> pure $ (, Nothing) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs index 9d1c34851b..165e927e39 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs @@ -3,6 +3,7 @@ module Ide.Plugin.Tactic.GHC where import Data.Maybe (isJust) +import DataCon import TcType import TyCoRep import TyCon @@ -67,3 +68,11 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res)) = Just $ isJust $ algebraicTyCon res lambdaCaseable _ = Nothing + +------------------------------------------------------------------------------ +-- | What data-constructor, if any, does the type have? +tyDataCons :: Type -> Maybe [DataCon] +tyDataCons g = do + (tc, _) <- splitTyConApp_maybe g + pure $ tyConDataCons tc + diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 89cb181275..674d88448d 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -155,10 +155,9 @@ split :: TacticsM () split = do jdg <- goal let g = jGoal jdg - case splitTyConApp_maybe $ unCType g of + case tyDataCons $ unCType g of Nothing -> throwError $ GoalMismatch "getGoalTyCon" g - Just (tc, _) -> do - let dcs = tyConDataCons tc + Just dcs -> do choice $ fmap splitDataCon dcs @@ -175,6 +174,22 @@ splitDataCon dc = rule $ \jdg -> do Nothing -> throwError $ GoalMismatch "splitDataCon" g +------------------------------------------------------------------------------ +-- | Attempt to instantiate the named data constructor to solve the goal. +splitDataCon' :: OccName -> TacticsM () +splitDataCon' dcn = do + jdg <- goal + let g = jGoal jdg + case splitTyConApp_maybe $ unCType g of + Nothing -> throwError $ GoalMismatch ("splitDataCon'" ++ unsafeRender dcn) g + Just (tc, _) -> do + let dcs = tyConDataCons tc + mdc = find ((== dcn) . getOccName) dcs + case mdc of + Nothing -> throwError $ GoalMismatch ("splitDataCon'" ++ unsafeRender dcn) g + Just dc -> splitDataCon dc + + ------------------------------------------------------------------------------ -- | @matching f@ takes a function from a judgement to a @Tactic@, and -- then applies the resulting @Tactic@. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs index 2ea4b8d06c..431e71c4d1 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs @@ -11,6 +11,7 @@ import qualified Data.Text as T data TacticCommand = Auto | Intros + | Split | Destruct | Homomorphism | DestructLambdaCase @@ -21,6 +22,7 @@ data TacticCommand tacticTitle :: TacticCommand -> T.Text -> T.Text tacticTitle Auto _ = "Attempt to fill hole" tacticTitle Intros _ = "Introduce lambda" +tacticTitle Split cname = "Introduce constructor " <> cname tacticTitle Destruct var = "Case split on " <> var tacticTitle Homomorphism var = "Homomorphic case split on " <> var tacticTitle DestructLambdaCase _ = "Lambda case split" diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index bcef3e3951..133e202beb 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -80,6 +80,11 @@ tests = testGroup "T3.hs" 7 13 [ (id, DestructLambdaCase, "") ] + , mkTest + "Produces datatype split actions" + "T2.hs" 16 14 + [ (id, Split, "T") + ] , mkTest "Doesn't suggest lambdacase without -XLambdaCase" "T2.hs" 11 25 diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs index 20b1644a8f..d3d5e2b397 100644 --- a/test/testdata/tactic/T2.hs +++ b/test/testdata/tactic/T2.hs @@ -10,3 +10,7 @@ foo = _ dontSuggestLambdaCase :: Either a b -> Int dontSuggestLambdaCase = _ +data T = T !(Int, Int) + +suggestCon :: T +suggestCon = _ From a08705a5c10286531b4c2710ae96cb18317c3cae Mon Sep 17 00:00:00 2001 From: WorldSEnder Date: Thu, 15 Oct 2020 15:23:29 +0200 Subject: [PATCH 2/4] test cases for splitting --- test/functional/Tactic.hs | 9 ++++++++- test/testdata/tactic/GoldenSplitPair.hs | 2 ++ test/testdata/tactic/GoldenSplitPair.hs.expected | 2 ++ test/testdata/tactic/T2.hs | 5 +++++ 4 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 test/testdata/tactic/GoldenSplitPair.hs create mode 100644 test/testdata/tactic/GoldenSplitPair.hs.expected diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 133e202beb..a79d855fc5 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -81,10 +81,16 @@ tests = testGroup [ (id, DestructLambdaCase, "") ] , mkTest - "Produces datatype split actions" + "Produces datatype split action for single-constructor types" "T2.hs" 16 14 [ (id, Split, "T") ] + , mkTest + "Produces datatype split action for multiple constructors" + "T2.hs" 21 15 + [ (id, Split, "T21") + , (id, Split, "T22") + ] , mkTest "Doesn't suggest lambdacase without -XLambdaCase" "T2.hs" 11 25 @@ -100,6 +106,7 @@ tests = testGroup , goldenTest "GoldenPureList.hs" 2 12 Auto "" , goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt" , goldenTest "GoldenGADTAuto.hs" 7 13 Auto "" + , goldenTest "GoldenSplitPair.hs" 2 11 Split "(,)" ] diff --git a/test/testdata/tactic/GoldenSplitPair.hs b/test/testdata/tactic/GoldenSplitPair.hs new file mode 100644 index 0000000000..826c7a6609 --- /dev/null +++ b/test/testdata/tactic/GoldenSplitPair.hs @@ -0,0 +1,2 @@ +thePair :: (Int, Int) +thePair = _ diff --git a/test/testdata/tactic/GoldenSplitPair.hs.expected b/test/testdata/tactic/GoldenSplitPair.hs.expected new file mode 100644 index 0000000000..954b583dbb --- /dev/null +++ b/test/testdata/tactic/GoldenSplitPair.hs.expected @@ -0,0 +1,2 @@ +thePair :: (Int, Int) +thePair = ((,) _ _) diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs index d3d5e2b397..7c81a5ec6a 100644 --- a/test/testdata/tactic/T2.hs +++ b/test/testdata/tactic/T2.hs @@ -14,3 +14,8 @@ data T = T !(Int, Int) suggestCon :: T suggestCon = _ + +data T2 = T21 Int | T22 Int Int + +suggestCons :: T2 +suggestCons = _ From 171888e3f3a7f96989363109855f1014caae01d7 Mon Sep 17 00:00:00 2001 From: WorldSEnder Date: Thu, 15 Oct 2020 19:04:01 +0200 Subject: [PATCH 3/4] don't suggest constructors with hash by default suggesting I# for Int probably is not what you want 99% of the time also reuse tyDataCons, tacname --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 14 ++++++++++++-- plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 12 ++++++------ test/functional/Tactic.hs | 10 ++++++++++ test/testdata/tactic/T2.hs | 3 +++ test/testdata/tactic/T3.hs | 4 +++- 5 files changed, 34 insertions(+), 9 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 9ebd450d25..8c96b95879 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -21,6 +21,7 @@ import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce import qualified Data.Foldable as F +import qualified Data.List as L import qualified Data.Map as M import Data.Maybe import qualified Data.Set as S @@ -37,7 +38,7 @@ import Development.Shake (Action) import DynFlags (xopt) import qualified FastString import GHC.Generics (Generic) -import GHC.LanguageExtensions.Type (Extension (LambdaCase)) +import GHC.LanguageExtensions.Type (Extension (LambdaCase, MagicHash)) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.GHC @@ -95,7 +96,9 @@ commandProvider Intros = provide Intros "" commandProvider Split = foldMapGoalType (F.fold . tyDataCons) $ \dc -> - provide Split $ T.pack $ occNameString $ getOccName dc + let cname = occNameString $ getOccName dc + in requireExtensionWhen MagicHash ("#" `L.isSuffixOf` cname) $ + provide Split $ T.pack cname commandProvider Destruct = filterBindingType destructFilter $ \occ _ -> provide Destruct $ T.pack $ occNameString occ @@ -190,6 +193,13 @@ requireExtension ext tp dflags plId uri range jdg = False -> pure [] +------------------------------------------------------------------------------ +-- | Like 'requireExtension' but only check if the bool is @True@. +requireExtensionWhen :: Extension -> Bool -> TacticProvider -> TacticProvider +requireExtensionWhen ext True = requireExtension ext +requireExtensionWhen _ False = id + + ------------------------------------------------------------------------------ -- | Create a 'TacticProvider' for each occurance of an 'a' in the foldable container -- extracted from the goal type. Useful instantiations for 't' include 'Maybe' or '[]'. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs index 674d88448d..ff79d5efd8 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs @@ -178,15 +178,15 @@ splitDataCon dc = rule $ \jdg -> do -- | Attempt to instantiate the named data constructor to solve the goal. splitDataCon' :: OccName -> TacticsM () splitDataCon' dcn = do + let tacname = "splitDataCon'(" ++ unsafeRender dcn ++ ")" jdg <- goal let g = jGoal jdg - case splitTyConApp_maybe $ unCType g of - Nothing -> throwError $ GoalMismatch ("splitDataCon'" ++ unsafeRender dcn) g - Just (tc, _) -> do - let dcs = tyConDataCons tc - mdc = find ((== dcn) . getOccName) dcs + case tyDataCons $ unCType g of + Nothing -> throwError $ GoalMismatch tacname g + Just dcs -> do + let mdc = find ((== dcn) . getOccName) dcs case mdc of - Nothing -> throwError $ GoalMismatch ("splitDataCon'" ++ unsafeRender dcn) g + Nothing -> throwError $ GoalMismatch tacname g Just dc -> splitDataCon dc diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index a79d855fc5..fb3d8bc6bf 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -80,6 +80,11 @@ tests = testGroup "T3.hs" 7 13 [ (id, DestructLambdaCase, "") ] + , mkTest + "Produces I# with -XMagicHash" + "T3.hs" 10 14 + [ (id, Split, "I#") + ] , mkTest "Produces datatype split action for single-constructor types" "T2.hs" 16 14 @@ -91,6 +96,11 @@ tests = testGroup [ (id, Split, "T21") , (id, Split, "T22") ] + , mkTest + "Doesn't suggest MagicHash constructors without -XMagicHash" + "T2.hs" 24 14 + [ (not, Split, "I#") + ] , mkTest "Doesn't suggest lambdacase without -XLambdaCase" "T2.hs" 11 25 diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs index 7c81a5ec6a..c42d50d8da 100644 --- a/test/testdata/tactic/T2.hs +++ b/test/testdata/tactic/T2.hs @@ -19,3 +19,6 @@ data T2 = T21 Int | T22 Int Int suggestCons :: T2 suggestCons = _ + +suggestInt :: Int +suggestInt = _ diff --git a/test/testdata/tactic/T3.hs b/test/testdata/tactic/T3.hs index 1bb42a9b02..f6f46a6aff 100644 --- a/test/testdata/tactic/T3.hs +++ b/test/testdata/tactic/T3.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase, MagicHash #-} suggestHomomorphicLC :: Either a b -> Either a b suggestHomomorphicLC = _ @@ -6,3 +6,5 @@ suggestHomomorphicLC = _ suggestLC :: Either a b -> Int suggestLC = _ +suggestInt :: Int +suggestInt = _ From e8c1c0343ff496c8f60aa1f12af7a874a84c0960 Mon Sep 17 00:00:00 2001 From: WorldSEnder Date: Thu, 15 Oct 2020 20:29:05 +0200 Subject: [PATCH 4/4] use 'algebraicTyCon' as filter for now --- plugins/tactics/src/Ide/Plugin/Tactic.hs | 17 ++++------------- test/functional/Tactic.hs | 5 +++-- 2 files changed, 7 insertions(+), 15 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs index 8c96b95879..18c0a582c3 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs @@ -21,7 +21,6 @@ import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce import qualified Data.Foldable as F -import qualified Data.List as L import qualified Data.Map as M import Data.Maybe import qualified Data.Set as S @@ -38,7 +37,7 @@ import Development.Shake (Action) import DynFlags (xopt) import qualified FastString import GHC.Generics (Generic) -import GHC.LanguageExtensions.Type (Extension (LambdaCase, MagicHash)) +import GHC.LanguageExtensions.Type (Extension (LambdaCase)) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.GHC @@ -95,10 +94,9 @@ commandProvider Intros = filterGoalType isFunction $ provide Intros "" commandProvider Split = - foldMapGoalType (F.fold . tyDataCons) $ \dc -> - let cname = occNameString $ getOccName dc - in requireExtensionWhen MagicHash ("#" `L.isSuffixOf` cname) $ - provide Split $ T.pack cname + filterGoalType (isJust . algebraicTyCon) $ + foldMapGoalType (F.fold . tyDataCons) $ \dc -> + provide Split $ T.pack $ occNameString $ getOccName dc commandProvider Destruct = filterBindingType destructFilter $ \occ _ -> provide Destruct $ T.pack $ occNameString occ @@ -193,13 +191,6 @@ requireExtension ext tp dflags plId uri range jdg = False -> pure [] ------------------------------------------------------------------------------- --- | Like 'requireExtension' but only check if the bool is @True@. -requireExtensionWhen :: Extension -> Bool -> TacticProvider -> TacticProvider -requireExtensionWhen ext True = requireExtension ext -requireExtensionWhen _ False = id - - ------------------------------------------------------------------------------ -- | Create a 'TacticProvider' for each occurance of an 'a' in the foldable container -- extracted from the goal type. Useful instantiations for 't' include 'Maybe' or '[]'. diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index fb3d8bc6bf..d9adc6f9e7 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -21,6 +21,7 @@ import Language.Haskell.LSP.Types (ApplyWorkspaceEditRequest, Position import Test.Hls.Util import Test.Tasty import Test.Tasty.HUnit +import Test.Tasty.ExpectedFailure (ignoreTestBecause) import System.FilePath import System.Directory (doesFileExist) import Control.Monad (unless) @@ -80,8 +81,8 @@ tests = testGroup "T3.hs" 7 13 [ (id, DestructLambdaCase, "") ] - , mkTest - "Produces I# with -XMagicHash" + , ignoreTestBecause "Not implemented, see #31" $ mkTest + "Splits Int with I# when -XMagicHash is enabled" "T3.hs" 10 14 [ (id, Split, "I#") ]