From d8d7f4c74c8925dcf70e5ac92e05056b8e60ce1b Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Wed, 7 Oct 2020 11:28:01 +0900 Subject: [PATCH 1/6] Use `dataConInstOrigArgTys` instaed of `dataConInstArgTys` --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- test/functional/Tactic.hs | 1 + test/testdata/tactic/GoldenGADTDestruct.hs | 7 +++++++ test/testdata/tactic/GoldenGADTDestruct.hs.expected | 7 +++++++ 4 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 test/testdata/tactic/GoldenGADTDestruct.hs create mode 100644 test/testdata/tactic/GoldenGADTDestruct.hs.expected diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 1f1f3ea449..cdf2549fdd 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -38,7 +38,7 @@ destructMatches f f2 t jdg = do case dcs of [] -> throwError $ GoalMismatch "destruct" g _ -> for dcs $ \dc -> do - let args = dataConInstArgTys dc apps + let args = dataConInstOrigArgTys dc apps names <- mkManyGoodNames hy args let pat :: Pat GhcPs diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index e770ad8a41..08184c441c 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -93,6 +93,7 @@ tests = testGroup , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto "" , goldenTest "GoldenNote.hs" 2 8 Auto "" , goldenTest "GoldenPureList.hs" 2 12 Auto "" + , goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt" ] diff --git a/test/testdata/tactic/GoldenGADTDestruct.hs b/test/testdata/tactic/GoldenGADTDestruct.hs new file mode 100644 index 0000000000..588cf362a2 --- /dev/null +++ b/test/testdata/tactic/GoldenGADTDestruct.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module GoldenGADTDestruct where +data CtxGADT where + MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT + +ctxGADT :: CtxGADT -> String +ctxGADT gadt = _decons diff --git a/test/testdata/tactic/GoldenGADTDestruct.hs.expected b/test/testdata/tactic/GoldenGADTDestruct.hs.expected new file mode 100644 index 0000000000..2243aafdf6 --- /dev/null +++ b/test/testdata/tactic/GoldenGADTDestruct.hs.expected @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module GoldenGADTDestruct where +data CtxGADT where + MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT + +ctxGADT :: CtxGADT -> String +ctxGADT gadt = (case gadt of { (MkCtxGADT a) -> _ }) From 7fd17e6bd1940c7223e7065ef6326de131ccc8a9 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Wed, 7 Oct 2020 11:33:33 +0900 Subject: [PATCH 2/6] Use `dataConInstOrigArgTys` instead also in buildDataCon --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index cdf2549fdd..29ecec9e57 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -85,7 +85,7 @@ buildDataCon -> [Type] -- ^ Type arguments for the data con -> RuleM (LHsExpr GhcPs) buildDataCon jdg dc apps = do - let args = dataConInstArgTys dc apps + let args = dataConInstOrigArgTys dc apps sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args pure . noLoc From 6c0767ba79e44f36bf34801b44608732ecb8859a Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Wed, 7 Oct 2020 17:44:20 +0900 Subject: [PATCH 3/6] Updates hie.yaml to make tactics plugin sources compatible with hls itself --- hie.yaml.cbl | 3 +++ hie.yaml.stack | 2 ++ 2 files changed, 5 insertions(+) diff --git a/hie.yaml.cbl b/hie.yaml.cbl index e30fd51d61..46730ab9d9 100644 --- a/hie.yaml.cbl +++ b/hie.yaml.cbl @@ -25,6 +25,9 @@ cradle: - path: "./plugins/default/src" component: "haskell-language-server:exe:haskell-language-server" + - path: "./plugins/tactics/src" + component: "haskell-language-server:exe:haskell-language-server" + - path: "./exe/Wrapper.hs" component: "haskell-language-server:exe:haskell-language-server-wrapper" diff --git a/hie.yaml.stack b/hie.yaml.stack index 18be9ff283..f9400d0914 100644 --- a/hie.yaml.stack +++ b/hie.yaml.stack @@ -21,6 +21,8 @@ cradle: - path: "./plugins/default/src" component: "haskell-language-server:exe:haskell-language-server" + - path: "./plugins/tactics/src" + component: "haskell-language-server:exe:haskell-language-server" - path: "./exe/Arguments.hs" component: "haskell-language-server:exe:haskell-language-server" From 79b98f000c090872c75152557d540dc5c19f1385 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Wed, 7 Oct 2020 17:51:39 +0900 Subject: [PATCH 4/6] Introduces compatibility function `dataConInstOrigArgTys'`, which calls `dataConInstArgTys` and selecting only non-class types --- plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs index 29ecec9e57..156673f5fe 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs @@ -38,7 +38,7 @@ destructMatches f f2 t jdg = do case dcs of [] -> throwError $ GoalMismatch "destruct" g _ -> for dcs $ \dc -> do - let args = dataConInstOrigArgTys dc apps + let args = dataConInstOrigArgTys' dc apps names <- mkManyGoodNames hy args let pat :: Pat GhcPs @@ -51,9 +51,19 @@ destructMatches f f2 t jdg = do pure $ match [pat] $ unLoc sg +-- | Essentially same as 'dataConInstOrigArgTys' in GHC, +-- but we need some tweaks in GHC >= 8.8. +-- Since old 'dataConInstArgTys' seems working with >= 8.8, +-- we just filter out non-class types in the result. +dataConInstOrigArgTys' :: DataCon -> [Type] -> [Type] +dataConInstOrigArgTys' con ty = + let tys0 = dataConInstArgTys con ty + in filter (maybe True (not . isClassTyCon) . tyConAppTyCon_maybe) tys0 + ------------------------------------------------------------------------------ -- | Combinator for performing 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 @@ -85,7 +95,7 @@ buildDataCon -> [Type] -- ^ Type arguments for the data con -> RuleM (LHsExpr GhcPs) buildDataCon jdg dc apps = do - let args = dataConInstOrigArgTys dc apps + let args = dataConInstOrigArgTys' dc apps sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args pure . noLoc From c1d47b94f88afea387f0c5b664f39595c09ba996 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Wed, 7 Oct 2020 18:34:47 +0900 Subject: [PATCH 5/6] Adds dependency `data-tree-print-0.1.0.2` --- stack-8.10.2.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index c052b7fa0b..eb00a542bb 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -14,6 +14,7 @@ extra-deps: commit: c59655f10d5ad295c2481537fc8abf0a297d9d1c - Cabal-3.0.2.0 - clock-0.7.2 +- data-tree-print-0.1.0.2 - floskell-0.10.4 - fourmolu-0.2.0.0 - monad-dijkstra-0.1.1.2 From 58631276d9780d97190478954b5ceb7411529301 Mon Sep 17 00:00:00 2001 From: Hiromi ISHII Date: Wed, 7 Oct 2020 20:40:02 +0900 Subject: [PATCH 6/6] Adds test-case for GADT introduction --- test/functional/Tactic.hs | 1 + test/testdata/tactic/GoldenGADTAuto.hs | 7 +++++++ test/testdata/tactic/GoldenGADTAuto.hs.expected | 7 +++++++ 3 files changed, 15 insertions(+) create mode 100644 test/testdata/tactic/GoldenGADTAuto.hs create mode 100644 test/testdata/tactic/GoldenGADTAuto.hs.expected diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 08184c441c..bcef3e3951 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -94,6 +94,7 @@ tests = testGroup , goldenTest "GoldenNote.hs" 2 8 Auto "" , goldenTest "GoldenPureList.hs" 2 12 Auto "" , goldenTest "GoldenGADTDestruct.hs" 7 17 Destruct "gadt" + , goldenTest "GoldenGADTAuto.hs" 7 13 Auto "" ] diff --git a/test/testdata/tactic/GoldenGADTAuto.hs b/test/testdata/tactic/GoldenGADTAuto.hs new file mode 100644 index 0000000000..1c47dd0e07 --- /dev/null +++ b/test/testdata/tactic/GoldenGADTAuto.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module GoldenGADTAuto where +data CtxGADT a where + MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a + +ctxGADT :: CtxGADT () +ctxGADT = _auto diff --git a/test/testdata/tactic/GoldenGADTAuto.hs.expected b/test/testdata/tactic/GoldenGADTAuto.hs.expected new file mode 100644 index 0000000000..2159d09f3b --- /dev/null +++ b/test/testdata/tactic/GoldenGADTAuto.hs.expected @@ -0,0 +1,7 @@ +{-# LANGUAGE GADTs #-} +module GoldenGADTAuto where +data CtxGADT a where + MkCtxGADT :: (Show a, Eq a) => a -> CtxGADT a + +ctxGADT :: CtxGADT () +ctxGADT = (MkCtxGADT ())