Skip to content

Commit

Permalink
implement isovector#21 : splitting on datatypeOne code action per dat…
Browse files Browse the repository at this point in the history
…atype constructor is produced.test cases for splittingdon't suggest constructors with hash by defaultsuggesting I# for Int probably is not what you want99% of the timealso reuse tyDataCons, tacnameuse 'algebraicTyCon' as filter for now
  • Loading branch information
WorldSEnder committed Oct 20, 2020
1 parent de4e387 commit 43b97cd
Show file tree
Hide file tree
Showing 10 changed files with 102 additions and 22 deletions.
47 changes: 30 additions & 17 deletions plugins/tactics/src/Ide/Plugin/Tactic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ import Data.Coerce
import Data.Generics.Aliases (mkQ)
import Data.Generics.Schemes (everything)
import Data.List
import qualified Data.Foldable as F
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid
Expand Down Expand Up @@ -101,6 +102,10 @@ commandProvider Auto = provide Auto ""
commandProvider Intros =
filterGoalType isFunction $
provide Intros ""
commandProvider Split =
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
Expand All @@ -119,11 +124,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

Expand Down Expand Up @@ -194,6 +200,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.
Expand Down Expand Up @@ -280,7 +294,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
Expand All @@ -289,19 +303,18 @@ tacticCmd tac lf state (TacticParams uri range var_name)
pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
x <- lift $ timeout 2e8 $
case runTactic ctx jdg
$ tac
$ mkVarOcc
$ T.unpack var_name of
Left err ->
pure $ (, Nothing)
$ Left
$ ResponseError InvalidRequest (T.pack $ show err) Nothing
Right (_, ext) -> do
let g = graft (RealSrcSpan span) ext
response = transform dflags (clientCapabilities lf) uri g pm
pure $ case response of
Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
$ tac
$ T.unpack var_name of
Left err ->
pure $ (, Nothing)
$ Left
$ ResponseError InvalidRequest (T.pack $ show err) Nothing
Right (_, ext) -> do
let g = graft (RealSrcSpan span) ext
response = transform dflags (clientCapabilities lf) uri g pm
pure $ case response of
Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
pure $ case x of
Just y -> y
Nothing -> (, Nothing)
Expand Down
8 changes: 8 additions & 0 deletions plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module Ide.Plugin.Tactic.GHC where
import Data.Maybe (isJust)
import Development.IDE.GHC.Compat
import OccName
import DataCon
import TcType
import TyCoRep
import Type
Expand Down Expand Up @@ -106,3 +107,10 @@ getPatName (fromPatCompat -> p0) =
#endif
_ -> Nothing

------------------------------------------------------------------------------
-- | What data-constructor, if any, does the type have?
tyDataCons :: Type -> Maybe [DataCon]
tyDataCons g = do
(tc, _) <- splitTyConApp_maybe g
pure $ tyConDataCons tc

23 changes: 19 additions & 4 deletions plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
Original file line number Diff line number Diff line change
Expand Up @@ -194,10 +194,9 @@ split :: TacticsM ()
split = tracing "split(user)" $ do
jdg <- goal
let g = jGoal jdg
case splitTyConApp_maybe $ unCType g of
Nothing -> throwError $ GoalMismatch "split" g
Just (tc, _) -> do
let dcs = tyConDataCons tc
case tyDataCons $ unCType g of
Nothing -> throwError $ GoalMismatch "split(user)" g
Just dcs -> do
choice $ fmap splitDataCon dcs


Expand Down Expand Up @@ -235,6 +234,22 @@ splitDataCon dc = tracing ("splitDataCon:" <> show 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
let tacname = "splitDataCon'(" ++ unsafeRender dcn ++ ")"
jdg <- goal
let g = jGoal jdg
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 tacname g
Just dc -> splitDataCon dc


------------------------------------------------------------------------------
-- | @matching f@ takes a function from a judgement to a @Tactic@, and
-- then applies the resulting @Tactic@.
Expand Down
2 changes: 2 additions & 0 deletions plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import qualified Data.Text as T
data TacticCommand
= Auto
| Intros
| Split
| Destruct
| Homomorphism
| DestructLambdaCase
Expand All @@ -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"
Expand Down
1 change: 1 addition & 0 deletions stack.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ packages:
- .
- ./ghcide/
- ./hls-plugin-api
- ./plugins/tactics

ghc-options:
"$everything": -haddock
Expand Down
23 changes: 23 additions & 0 deletions test/functional/Tactic.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -80,6 +81,27 @@ tests = testGroup
"T3.hs" 7 13
[ (id, DestructLambdaCase, "")
]
, ignoreTestBecause "Not implemented, see isovector/haskell-language-server#31" $ mkTest
"Splits Int with I# when -XMagicHash is enabled"
"T3.hs" 10 14
[ (id, Split, "I#")
]
, mkTest
"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 MagicHash constructors without -XMagicHash"
"T2.hs" 24 14
[ (not, Split, "I#")
]
, mkTest
"Doesn't suggest lambdacase without -XLambdaCase"
"T2.hs" 11 25
Expand All @@ -101,6 +123,7 @@ tests = testGroup
, goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt"
, goldenTest "GoldenGADTAuto.hs" 7 13 Auto ""
, goldenTest "GoldenSwapMany.hs" 2 12 Auto ""
, goldenTest "GoldenSplitPair.hs" 2 11 Split "(,)"
]


Expand Down
2 changes: 2 additions & 0 deletions test/testdata/tactic/GoldenSplitPair.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
thePair :: (Int, Int)
thePair = _
2 changes: 2 additions & 0 deletions test/testdata/tactic/GoldenSplitPair.hs.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
thePair :: (Int, Int)
thePair = (_, _)
12 changes: 12 additions & 0 deletions test/testdata/tactic/T2.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,15 @@ foo = _
dontSuggestLambdaCase :: Either a b -> Int
dontSuggestLambdaCase = _

data T = T !(Int, Int)

suggestCon :: T
suggestCon = _

data T2 = T21 Int | T22 Int Int

suggestCons :: T2
suggestCons = _

suggestInt :: Int
suggestInt = _
4 changes: 3 additions & 1 deletion test/testdata/tactic/T3.hs
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE LambdaCase, MagicHash #-}

suggestHomomorphicLC :: Either a b -> Either a b
suggestHomomorphicLC = _

suggestLC :: Either a b -> Int
suggestLC = _

suggestInt :: Int
suggestInt = _

0 comments on commit 43b97cd

Please sign in to comment.