From c7cc9934c4a19b5b253c65388b9e3ffe51532898 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 6 Sep 2020 11:25:11 -0700 Subject: [PATCH 01/63] Add refinery --- haskell-language-server.cabal | 1 + stack.yaml | 35 +++++++++++++---------------------- 2 files changed, 14 insertions(+), 22 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 509e4d4221..e2f765d11f 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -97,6 +97,7 @@ library , time , transformers , unordered-containers + , refinery include-dirs: include if os(windows) diff --git a/stack.yaml b/stack.yaml index 605591b432..a57e4c4ceb 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-14.27 # Last 8.6.5 +resolver: lts-15.0 # Last 8.8.2 packages: - . @@ -9,53 +9,44 @@ ghc-options: extra-deps: - aeson-1.5.2.0 -- ansi-terminal-0.10.3 -- base-compat-0.10.5 +- apply-refact-0.7.0.0 - github: bubba/brittany commit: c59655f10d5ad295c2481537fc8abf0a297d9d1c -- butcher-1.3.3.1 -- Cabal-3.0.2.0 -- cabal-plan-0.6.2.0 +- butcher-1.3.3.2 +- bytestring-trie-0.2.5.0 - clock-0.7.2 +- constrained-dynamic-0.1.0.0 - extra-1.7.3 - floskell-0.10.4 - fourmolu-0.1.0.0@rev:1 -- fuzzy-0.1.0.0 # - ghcide-0.1.0 - ghc-check-0.5.0.1 -- ghc-exactprint-0.6.2 - ghc-lib-parser-8.10.1.20200523 - ghc-lib-parser-ex-8.10.0.4 -- haddock-api-2.22.0@rev:1 - haddock-library-1.8.0 - haskell-lsp-0.22.0.0 - haskell-lsp-types-0.22.0.0 +- haskell-src-exts-1.21.1 - hie-bios-0.6.1 +- hlint-2.2.8 +- hoogle-5.0.17.11 +- hsimport-0.11.0 - HsYAML-0.2.1.0@rev:1 - HsYAML-aeson-0.2.0.0@rev:2 -- indexed-profunctors-0.1 -- lens-4.18 +- ilist-0.3.1.0 - lsp-test-0.11.0.4 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 -- optics-core-0.2 -- optparse-applicative-0.15.1.0 - ormolu-0.1.2.0 -- parser-combinators-1.2.1 -- primitive-0.7.1.0 -- regex-base-0.94.0.0 -- regex-pcre-builtin-0.95.1.1.8.43 -- regex-tdfa-1.3.1.0 - retrie-0.1.1.1 -- semialign-1.1 +- semigroups-0.18.5 # - github: wz1000/shake # commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef - stylish-haskell-0.11.0.3 -- tasty-rerun-1.1.17 - temporary-1.2.1.1 - these-1.1.1.1 -- type-equality-1 -- topograph-1 +- primitive-0.7.1.0@sha256:6a237bb338bcc43193077ff8e8c0f0ce2de14c652231496a15672e8b563a07e2,2604 +- refinery-0.1.0.0 flags: haskell-language-server: From c81f2eb53eac2ec1361b3b97b35f555ea9dacb0b Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sun, 6 Sep 2020 11:28:29 -0700 Subject: [PATCH 02/63] [WIP] Add Skeleton for Tactic Plugin --- haskell-language-server.cabal | 1 + src/Ide/Plugin/Tactic.hs | 44 +++++++++++++++++++++++++++++++++++ 2 files changed, 45 insertions(+) create mode 100644 src/Ide/Plugin/Tactic.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index e2f765d11f..385b9481a4 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -51,6 +51,7 @@ library Ide.Plugin.Ormolu Ide.Plugin.Pragmas Ide.Plugin.Retrie + Ide.Plugin.Tactic Ide.Plugin.Floskell Ide.Plugin.Formatter Ide.Plugin.StylishHaskell diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs new file mode 100644 index 0000000000..6a3af3498c --- /dev/null +++ b/src/Ide/Plugin/Tactic.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} +-- | A plugin that uses tactics to synthesize code + +module Ide.Plugin.Tactic + ( descriptor + ) where + +import Data.Aeson +import qualified Data.HashMap.Strict as H +import qualified GHC.Generics as Generics +import Ide.Types +import qualified Language.Haskell.LSP.Types as J +import Language.Haskell.LSP.Types + +descriptor :: PluginId -> PluginDescriptor +descriptor plId = (defaultPluginDescriptor plId) + { pluginCommands = [PluginCommand "fillHole" "fill the hole using a tactic" tacticCmd] + , pluginCodeActionProvider = Just codeActionProvider + } + +codeActionProvider :: CodeActionProvider +codeActionProvider _conf _ide _plid (TextDocumentIdentifier uri) range _ctx = _hole + +-- codeAction :: CodeActionProvider +-- codeAction _lf _state _pid _tid _range + +data TacticParams = TacticParams + { file :: J.Uri -- ^ Uri of the file to fill the hole in + , range :: J.Range -- ^ The range of the hole + } + deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) + +tacticCmd :: CommandFunction TacticParams +tacticCmd _lf _ide (TacticParams uri range) = do + let + textEdits = J.List + [J.TextEdit range _solution + ] + res = J.WorkspaceEdit + (Just $ H.singleton uri textEdits) + Nothing + pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) From a31a9f94809f54a096d11ce96041ce32dd836a8b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 6 Sep 2020 11:35:13 -0700 Subject: [PATCH 03/63] Local bindings --- haskell-language-server.cabal | 1 + src/Ide/LocalBindings.hs | 115 ++++++++++++++++++++++++++++++++++ 2 files changed, 116 insertions(+) create mode 100644 src/Ide/LocalBindings.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index e2f765d11f..36cc3c47ee 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -98,6 +98,7 @@ library , transformers , unordered-containers , refinery + , syb include-dirs: include if os(windows) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs new file mode 100644 index 0000000000..009b25ddd1 --- /dev/null +++ b/src/Ide/LocalBindings.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE LambdaCase #-} + +module Ide.LocalBindings where + +import Bag +import Control.Lens +import Data.Data.Lens +import Data.Generics +import qualified Data.Map as M +import qualified Data.Set as S +import GHC (TypecheckedModule (..), GhcTc) +import HsBinds +import HsExpr +import Id +import SrcLoc + + +bindings :: TypecheckedModule -> (S.Set Id, M.Map SrcSpan (S.Set Id)) +bindings = bindsBindings mempty . tm_typechecked_source + + +dataBindings :: Data a => S.Set Id -> a -> M.Map SrcSpan (S.Set Id) +dataBindings in_scope = foldMapOf biplate $ cool collect + where + cool + :: (HsExpr GhcTc -> M.Map SrcSpan (S.Set Id)) + -> LHsExpr GhcTc -> M.Map SrcSpan (S.Set Id) + cool f (L src expr) = M.union (f expr) (M.singleton src in_scope) + + collect :: HsExpr GhcTc -> M.Map SrcSpan (S.Set Id) + collect (HsLam _ matches) = matchGroupBindings in_scope matches + collect (HsLamCase _ matches) = matchGroupBindings in_scope matches + collect (HsCase _ scrutinee matches) = + M.union (dataBindings in_scope scrutinee) $ matchGroupBindings in_scope matches + collect (HsLet _ (L _ binds) expr) = + let (new, res) = localBindsBindings in_scope binds + in_scope' = S.union new in_scope + in M.union (dataBindings in_scope' expr) res + collect (HsVar _ _) = mempty + collect (HsUnboundVar _ _) = mempty + collect (HsConLikeOut _ _) = mempty + collect (HsRecFld _ _) = mempty + collect (HsOverLabel _ _ _) = mempty + collect (HsIPVar _ _) = mempty + collect (HsOverLit _ _) = mempty + collect (HsLit _ _) = mempty + collect (HsApp _ a b) = M.union (dataBindings in_scope a) (dataBindings in_scope b) + collect (HsAppType _ _ a) = dataBindings in_scope a + collect (OpApp _ a b c) = + mconcat + [ dataBindings in_scope a + , dataBindings in_scope b + , dataBindings in_scope c + ] + collect (NegApp _ a _) = dataBindings in_scope a + collect (HsPar _ a) = dataBindings in_scope a + collect (SectionL _ a b) = + mconcat + [ dataBindings in_scope a + , dataBindings in_scope b + ] + collect (SectionR _ a b) = + mconcat + [ dataBindings in_scope a + , dataBindings in_scope b + ] + collect (ExplicitTuple _ a _) = dataBindings in_scope a + collect (ExplicitSum _ _ _ a) = dataBindings in_scope a + collect (HsIf _ _ a b c) = + mconcat + [ dataBindings in_scope a + , dataBindings in_scope b + , dataBindings in_scope c + ] + collect (HsMultiIf _ a) = dataBindings in_scope a + collect (HsDo _ _ a) = dataBindings in_scope a + collect (ExplicitList _ _ a) = dataBindings in_scope a + collect (RecordCon _ _ a) = dataBindings in_scope a + collect (RecordUpd _ _ a) = dataBindings in_scope a + collect (ExprWithTySig _ _ a) = dataBindings in_scope a + collect (ArithSeq _ _ a) = dataBindings in_scope a + collect (HsSCC _ _ _ a) = dataBindings in_scope a + collect (HsBracket _ a) = dataBindings in_scope a + collect (HsStatic _ a) = dataBindings in_scope a + -- TODO(sandy): This doesn't do arrow syntax + collect _ = mempty + + + +matchGroupBindings :: S.Set Id -> MatchGroup GhcTc (LHsExpr GhcTc) -> M.Map SrcSpan (S.Set Id) +matchGroupBindings _ (XMatchGroup _) = M.empty +matchGroupBindings in_scope (MG _ (L _ alts) _) = M.fromList $ do + L _ (Match _ _ pats body) <- alts + let bound = S.filter isId $ everything S.union (mkQ S.empty S.singleton) pats + M.toList $ dataBindings (S.union bound in_scope) body + + +localBindsBindings :: S.Set Id -> HsLocalBindsLR GhcTc GhcTc -> (S.Set Id, M.Map SrcSpan (S.Set Id)) +localBindsBindings in_scope (HsValBinds _ (ValBinds _ binds _sigs)) = bindsBindings in_scope binds +localBindsBindings in_scope (HsValBinds _ (XValBindsLR (NValBinds groups _sigs))) = + flip foldMap groups $ bindsBindings in_scope . snd +localBindsBindings _ _ = (mempty, mempty) + +bindsBindings :: S.Set Id -> Bag (LHsBindLR GhcTc GhcTc) -> (S.Set Id, M.Map SrcSpan (S.Set Id)) +bindsBindings in_scope binds = + -- TODO(sandy): This doesn't do recursive binds + flip foldMap (fmap unLoc $ bagToList binds) $ \case + FunBind _ (L _ name) matches _ _ -> + (S.singleton name, matchGroupBindings (S.insert name in_scope) matches) + PatBind _ pat rhs _ -> + let bound = S.filter isId $ everything S.union (mkQ S.empty S.singleton) pat + in (bound, dataBindings (S.union bound in_scope) rhs) + AbsBinds _ _ _ _ _ binds' _ -> bindsBindings in_scope binds' + _ -> (mempty, mempty) + From b79a23a39f08f36371a3588735db892574445ea1 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 6 Sep 2020 11:48:59 -0700 Subject: [PATCH 04/63] more cases for bindings --- src/Ide/LocalBindings.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 009b25ddd1..0fb3eb12e2 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -86,7 +86,6 @@ dataBindings in_scope = foldMapOf biplate $ cool collect collect _ = mempty - matchGroupBindings :: S.Set Id -> MatchGroup GhcTc (LHsExpr GhcTc) -> M.Map SrcSpan (S.Set Id) matchGroupBindings _ (XMatchGroup _) = M.empty matchGroupBindings in_scope (MG _ (L _ alts) _) = M.fromList $ do @@ -101,9 +100,9 @@ localBindsBindings in_scope (HsValBinds _ (XValBindsLR (NValBinds groups _sigs)) flip foldMap groups $ bindsBindings in_scope . snd localBindsBindings _ _ = (mempty, mempty) + bindsBindings :: S.Set Id -> Bag (LHsBindLR GhcTc GhcTc) -> (S.Set Id, M.Map SrcSpan (S.Set Id)) bindsBindings in_scope binds = - -- TODO(sandy): This doesn't do recursive binds flip foldMap (fmap unLoc $ bagToList binds) $ \case FunBind _ (L _ name) matches _ _ -> (S.singleton name, matchGroupBindings (S.insert name in_scope) matches) @@ -111,5 +110,7 @@ bindsBindings in_scope binds = let bound = S.filter isId $ everything S.union (mkQ S.empty S.singleton) pat in (bound, dataBindings (S.union bound in_scope) rhs) AbsBinds _ _ _ _ _ binds' _ -> bindsBindings in_scope binds' - _ -> (mempty, mempty) + VarBind _ name c _ -> (S.singleton name, dataBindings in_scope c) + PatSynBind _ _ -> mempty + XHsBindsLR _ -> mempty From 2b7040d99318fcc510974dfb55f0b3515afd4b0a Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Sun, 6 Sep 2020 11:56:13 -0700 Subject: [PATCH 05/63] [WIP] Add more to the code action provider --- src/Ide/Plugin/Tactic.hs | 26 ++++++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 6a3af3498c..3bc8fd4854 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -10,21 +10,39 @@ module Ide.Plugin.Tactic import Data.Aeson import qualified Data.HashMap.Strict as H import qualified GHC.Generics as Generics + +import Development.IDE.Core.RuleTypes (GhcSessionDeps (GhcSessionDeps), + TcModuleResult (tmrModule), + TypeCheck (TypeCheck)) +import Development.IDE.Core.Shake (use, IdeState (..)) +import Development.IDE.Core.Service (runAction) +import Development.Shake (Action) + import Ide.Types + import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types +-- import Refinery.Tactic + descriptor :: PluginId -> PluginDescriptor descriptor plId = (defaultPluginDescriptor plId) { pluginCommands = [PluginCommand "fillHole" "fill the hole using a tactic" tacticCmd] , pluginCodeActionProvider = Just codeActionProvider } +runIde :: IdeState -> Action a -> IO a +runIde state = runAction "tactic" state + codeActionProvider :: CodeActionProvider -codeActionProvider _conf _ide _plid (TextDocumentIdentifier uri) range _ctx = _hole +codeActionProvider _conf state _plid (TextDocumentIdentifier uri) range _ctx + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + tmr <- runIde state $ use TypeCheck nfp + hsc <- runIde state $ use GhcSessionDeps nfp + -- TODO Check if we have a hole inside of the range. + -- Go from range -> SrcSpan, then look inside the module contents + _hole --- codeAction :: CodeActionProvider --- codeAction _lf _state _pid _tid _range data TacticParams = TacticParams { file :: J.Uri -- ^ Uri of the file to fill the hole in @@ -36,7 +54,7 @@ tacticCmd :: CommandFunction TacticParams tacticCmd _lf _ide (TacticParams uri range) = do let textEdits = J.List - [J.TextEdit range _solution + [J.TextEdit range ("Howdy Partner!") ] res = J.WorkspaceEdit (Just $ H.singleton uri textEdits) From 945d38a3fbb5b3a33c098a4194bfcdf258331870 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 6 Sep 2020 12:02:37 -0700 Subject: [PATCH 06/63] is it a hole? --- src/Ide/LocalBindings.hs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 0fb3eb12e2..8e865cf23a 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} module Ide.LocalBindings where @@ -13,6 +14,7 @@ import HsBinds import HsExpr import Id import SrcLoc +import Data.Monoid bindings :: TypecheckedModule -> (S.Set Id, M.Map SrcSpan (S.Set Id)) @@ -114,3 +116,13 @@ bindsBindings in_scope binds = PatSynBind _ _ -> mempty XHsBindsLR _ -> mempty + +isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar +isItAHole tcm span = getFirst $ + everything (<>) ( + mkQ mempty $ \case + L span' (HsUnboundVar _ z :: HsExpr GhcTc) + | span == span' -> pure z + _ -> mempty + ) $ tm_typechecked_source tcm + From ae533ebadb07a316a9128a1d587810939d4fc009 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 6 Sep 2020 12:17:39 -0700 Subject: [PATCH 07/63] Beginning of tactics machinery --- src/Ide/Tactics.hs | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 src/Ide/Tactics.hs diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs new file mode 100644 index 0000000000..197b628126 --- /dev/null +++ b/src/Ide/Tactics.hs @@ -0,0 +1,38 @@ +{-# LANGUAGE DeriveGeneric #-} + +module IDE.Tactics where + +import Refinery.Tactic +import GHC +import OccName +import GHC.Generics +import Data.Function +import Type + + +newtype CType = CType { unCType :: Type } + +instance Eq CType where + (==) = eqType `on` unCType + +instance Ord CType where + compare = nonDetCmpType `on` unCType + + +data Judgement = Judgement + { jHoleId :: Integer + , jHypothesis :: [(OccName, CType)] + , jGoal :: CType + } + deriving (Eq, Ord, Generic) + + +data TacticError + = UndefinedHypothesis OccName + | GoalMismatch String CType + | UnsolvedSubgoals [Judgement] + + +type TacticsM = TacticT Judgement (HsType GhcTc) (ProvableT Judgement (Either TacticError)) +type RuleM = RuleT Judgement (HsType GhcTc) (ProvableT Judgement (Either TacticError)) + From ca24aa5f0a69d272db17bf5f12d8a510375dd380 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 10:59:22 -0700 Subject: [PATCH 08/63] tactics machinery --- haskell-language-server.cabal | 2 + src/Ide/Tactics.hs | 109 ++++++++++++++++++++++++++++++++-- 2 files changed, 106 insertions(+), 5 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 135c079c71..3813686881 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -100,6 +100,8 @@ library , unordered-containers , refinery , syb + , mtl + , ghc-source-gen include-dirs: include if os(windows) diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index 197b628126..c7af253161 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -1,13 +1,28 @@ -{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ViewPatterns #-} module IDE.Tactics where +import Control.Arrow +import Data.Char +import Data.List import Refinery.Tactic import GHC import OccName import GHC.Generics import Data.Function import Type +import TcType +import TyCoRep +import Control.Monad.Except (throwError) +import Control.Monad.Trans +import GHC.SourceGen.Expr +import GHC.SourceGen.Binds +import GHC.SourceGen.Overloaded +import GHC.SourceGen.Pat newtype CType = CType { unCType :: Type } @@ -20,8 +35,7 @@ instance Ord CType where data Judgement = Judgement - { jHoleId :: Integer - , jHypothesis :: [(OccName, CType)] + { jHypothesis :: [(OccName, CType)] , jGoal :: CType } deriving (Eq, Ord, Generic) @@ -33,6 +47,91 @@ data TacticError | UnsolvedSubgoals [Judgement] -type TacticsM = TacticT Judgement (HsType GhcTc) (ProvableT Judgement (Either TacticError)) -type RuleM = RuleT Judgement (HsType GhcTc) (ProvableT Judgement (Either TacticError)) +type ProvableM = ProvableT Judgement (Either TacticError) +type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) ProvableM + +assumption :: TacticsM () +assumption = rule $ \(Judgement hy g) -> + case find ((== g) . snd) hy of + Just (v, _) -> pure $ noLoc $ HsVar NoExt $ noLoc $ Unqual v + Nothing -> throwError $ GoalMismatch "assumption" g + + +newSubgoal :: [(OccName, CType)] -> CType -> RuleM (LHsExpr GhcPs) +newSubgoal hy g = subgoal =<< newJudgement hy g + + + +newJudgement + :: ( Monad m) + => [(OccName, CType)] + -> CType + -> m Judgement +newJudgement hy g = do + pure $ Judgement hy g + + + +intro :: TacticsM () +intro = rule $ \(Judgement hy g) -> + case unCType g of + (FunTy a b) -> do + v <- pure $ mkGoodName (getInScope hy) a + sg <- newSubgoal ((v, CType a) : hy) $ CType b + pure $ noLoc $ lambda [VarPat noExt $ noLoc $ Unqual v] $ unLoc sg + _ -> throwError $ GoalMismatch "intro" g + + +mkGoodName :: [OccName] -> Type -> OccName +mkGoodName in_scope t = + let tn = mkTyName t + in mkVarOcc $ case elem (mkVarOcc tn) in_scope of + True -> tn ++ show (length in_scope) + False -> tn + + + +mkTyName :: Type -> String +mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) = "f" ++ mkTyName a ++ mkTyName b +mkTyName (tcSplitFunTys -> ((_:_), b)) = "f_" ++ mkTyName b +mkTyName (splitTyConApp_maybe -> Just (c, args)) = mkTyConName c ++ foldMap mkTyName args +mkTyName (getTyVar_maybe-> Just tv) = occNameString $ occName tv +mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) = mkTyName t +mkTyName _ = "x" + + +mkTyConName :: TyCon -> String +mkTyConName = fmap toLower . take 1 . occNameString . getOccName + + +tacticActual + :: TacticsM () + -> Judgement + -> Either TacticError (LHsExpr GhcPs) +tacticActual t = fmap fst . runProvableT . runTacticT t + +runTactic + :: Type + -> [(OccName, Type)] + -> TacticsM () + -> Maybe (LHsExpr GhcPs) +runTactic ty hy t + = hush + . tacticActual t + . Judgement (fmap (second CType) hy) + $ CType ty + + +hush :: Either a b -> Maybe b +hush = either (const Nothing) Just + + +instance MonadExtract (LHsExpr GhcPs) ProvableM where + hole = pure $ noLoc $ HsUnboundVar NoExt $ TrueExprHole $ mkVarOcc "_" + + + +getInScope :: [(OccName, a)] -> [OccName] +getInScope = fmap fst From 7128ed02896da0c056af6d929d33a10ea9e03821 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 11:14:00 -0700 Subject: [PATCH 09/63] split out tactics machinery; finish porting tactics --- src/Ide/LocalBindings.hs | 2 +- src/Ide/TacticMachinery.hs | 132 +++++++++++++++++++++++++ src/Ide/Tactics.hs | 193 +++++++++++++++++-------------------- 3 files changed, 221 insertions(+), 106 deletions(-) create mode 100644 src/Ide/TacticMachinery.hs diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 8e865cf23a..4d8fc6b54f 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -8,13 +8,13 @@ import Control.Lens import Data.Data.Lens import Data.Generics import qualified Data.Map as M +import Data.Monoid import qualified Data.Set as S import GHC (TypecheckedModule (..), GhcTc) import HsBinds import HsExpr import Id import SrcLoc -import Data.Monoid bindings :: TypecheckedModule -> (S.Set Id, M.Map SrcSpan (S.Set Id)) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs new file mode 100644 index 0000000000..54909c2b5f --- /dev/null +++ b/src/Ide/TacticMachinery.hs @@ -0,0 +1,132 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.TacticMachinery where + +import Control.Arrow +import Data.Char +import Data.Function +import Data.List +import DataCon +import GHC +import GHC.Generics +import GHC.SourceGen.Overloaded +import Name +import Refinery.Tactic +import TcType +import Type + + +newtype CType = CType { unCType :: Type } + +instance Eq CType where + (==) = eqType `on` unCType + +instance Ord CType where + compare = nonDetCmpType `on` unCType + + +data Judgement = Judgement + { jHypothesis :: [(OccName, CType)] + , jGoal :: CType + } + deriving (Eq, Ord, Generic) + + +data TacticError + = UndefinedHypothesis OccName + | GoalMismatch String CType + | UnsolvedSubgoals [Judgement] + + +type ProvableM = ProvableT Judgement (Either TacticError) +type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) ProvableM +type Rule = RuleM (LHsExpr GhcPs) + + +newSubgoal :: [(OccName, CType)] -> CType -> RuleM (LHsExpr GhcPs) +newSubgoal hy g = subgoal =<< newJudgement hy g + + +newJudgement + :: ( Monad m) + => [(OccName, CType)] + -> CType + -> m Judgement +newJudgement hy g = do + pure $ Judgement hy g + + +mkGoodName :: [OccName] -> Type -> OccName +mkGoodName in_scope t = + let tn = mkTyName t + in mkVarOcc $ case elem (mkVarOcc tn) in_scope of + True -> tn ++ show (length in_scope) + False -> tn + + +mkTyName :: Type -> String +mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) + = "f" ++ mkTyName a ++ mkTyName b +mkTyName (tcSplitFunTys -> ((_:_), b)) + = "f_" ++ mkTyName b +mkTyName (splitTyConApp_maybe -> Just (c, args)) + = mkTyConName c ++ foldMap mkTyName args +mkTyName (getTyVar_maybe-> Just tv) + = occNameString $ occName tv +mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) + = mkTyName t +mkTyName _ = "x" + + +mkTyConName :: TyCon -> String +mkTyConName = fmap toLower . take 1 . occNameString . getOccName + + +tacticActual + :: TacticsM () + -> Judgement + -> Either TacticError (LHsExpr GhcPs) +tacticActual t = fmap fst . runProvableT . runTacticT t + + +runTactic + :: Type + -> [(OccName, Type)] + -> TacticsM () + -> Maybe (LHsExpr GhcPs) +runTactic ty hy t + = hush + . tacticActual t + . Judgement (fmap (second CType) hy) + $ CType ty + + +hush :: Either a b -> Maybe b +hush = either (const Nothing) Just + + +instance MonadExtract (LHsExpr GhcPs) ProvableM where + hole = pure $ noLoc $ HsUnboundVar NoExt $ TrueExprHole $ mkVarOcc "_" + + +getInScope :: [(OccName, a)] -> [OccName] +getInScope = fmap fst + + +buildDataCon + :: [(OccName, CType)] + -> DataCon + -> [Type] + -> RuleM (LHsExpr GhcPs) +buildDataCon hy dc apps = do + let args = dataConInstArgTys dc apps + sgs <- traverse (newSubgoal hy . CType) args + pure . noLoc + . foldl' (@@) (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) + $ fmap unLoc sgs + diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index c7af253161..62c0e04ae8 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -4,53 +4,29 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} -module IDE.Tactics where +module Ide.Tactics + ( module Ide.Tactics + , runTactic + ) where -import Control.Arrow -import Data.Char +import Control.Monad.Except (throwError) +import Control.Monad.State import Data.List -import Refinery.Tactic +import Data.Traversable +import DataCon import GHC -import OccName -import GHC.Generics -import Data.Function -import Type -import TcType -import TyCoRep -import Control.Monad.Except (throwError) -import Control.Monad.Trans -import GHC.SourceGen.Expr +import GHC.Exts import GHC.SourceGen.Binds +import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat +import Ide.TacticMachinery +import Name +import Refinery.Tactic +import TyCoRep +import Type -newtype CType = CType { unCType :: Type } - -instance Eq CType where - (==) = eqType `on` unCType - -instance Ord CType where - compare = nonDetCmpType `on` unCType - - -data Judgement = Judgement - { jHypothesis :: [(OccName, CType)] - , jGoal :: CType - } - deriving (Eq, Ord, Generic) - - -data TacticError - = UndefinedHypothesis OccName - | GoalMismatch String CType - | UnsolvedSubgoals [Judgement] - - -type ProvableM = ProvableT Judgement (Either TacticError) -type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM -type RuleM = RuleT Judgement (LHsExpr GhcPs) ProvableM - assumption :: TacticsM () assumption = rule $ \(Judgement hy g) -> case find ((== g) . snd) hy of @@ -58,21 +34,6 @@ assumption = rule $ \(Judgement hy g) -> Nothing -> throwError $ GoalMismatch "assumption" g -newSubgoal :: [(OccName, CType)] -> CType -> RuleM (LHsExpr GhcPs) -newSubgoal hy g = subgoal =<< newJudgement hy g - - - -newJudgement - :: ( Monad m) - => [(OccName, CType)] - -> CType - -> m Judgement -newJudgement hy g = do - pure $ Judgement hy g - - - intro :: TacticsM () intro = rule $ \(Judgement hy g) -> case unCType g of @@ -83,55 +44,77 @@ intro = rule $ \(Judgement hy g) -> _ -> throwError $ GoalMismatch "intro" g -mkGoodName :: [OccName] -> Type -> OccName -mkGoodName in_scope t = - let tn = mkTyName t - in mkVarOcc $ case elem (mkVarOcc tn) in_scope of - True -> tn ++ show (length in_scope) - False -> tn - - - -mkTyName :: Type -> String -mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) = "f" ++ mkTyName a ++ mkTyName b -mkTyName (tcSplitFunTys -> ((_:_), b)) = "f_" ++ mkTyName b -mkTyName (splitTyConApp_maybe -> Just (c, args)) = mkTyConName c ++ foldMap mkTyName args -mkTyName (getTyVar_maybe-> Just tv) = occNameString $ occName tv -mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) = mkTyName t -mkTyName _ = "x" - - -mkTyConName :: TyCon -> String -mkTyConName = fmap toLower . take 1 . occNameString . getOccName - - -tacticActual - :: TacticsM () - -> Judgement - -> Either TacticError (LHsExpr GhcPs) -tacticActual t = fmap fst . runProvableT . runTacticT t - -runTactic - :: Type - -> [(OccName, Type)] - -> TacticsM () - -> Maybe (LHsExpr GhcPs) -runTactic ty hy t - = hush - . tacticActual t - . Judgement (fmap (second CType) hy) - $ CType ty - - -hush :: Either a b -> Maybe b -hush = either (const Nothing) Just - - -instance MonadExtract (LHsExpr GhcPs) ProvableM where - hole = pure $ noLoc $ HsUnboundVar NoExt $ TrueExprHole $ mkVarOcc "_" - - - -getInScope :: [(OccName, a)] -> [OccName] -getInScope = fmap fst +destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM () +destruct' f term = rule $ \(Judgement hy g) -> do + case find ((== term) . fst) hy of + Nothing -> throwError $ UndefinedHypothesis term + Just (_, t) -> + case splitTyConApp_maybe $ unCType t of + Nothing -> throwError $ GoalMismatch "destruct" g + Just (tc, apps) -> do + fmap noLoc + $ case' (HsVar NoExt $ noLoc $ Unqual term) + <$> do + for (tyConDataCons tc) $ \dc -> do + let args = dataConInstArgTys dc apps + names <- flip evalStateT (getInScope hy) $ for args $ \at -> do + in_scope <- Control.Monad.State.get + let n = mkGoodName in_scope at + modify (n :) + pure n + + let pat :: Pat GhcPs + pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) + $ fmap (bvar . fromString . occNameString) names + + j <- newJudgement (zip names (fmap CType args) ++ hy) g + sg <- f dc j + pure $ match [pat] $ unLoc sg + + +destruct :: OccName -> TacticsM () +destruct = destruct' $ const subgoal + +homo :: OccName -> TacticsM () +homo = destruct' $ \dc (Judgement hy (CType g)) -> + buildDataCon hy dc (snd $ splitAppTys g) + + +apply :: TacticsM () +apply = rule $ \(Judgement hy g) -> do + case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) hy of + Just (func, CType ty) -> do + let (args, _) = splitFunTys ty + sgs <- traverse (newSubgoal hy . CType) args + pure . noLoc + . foldl' (@@) (HsVar NoExt $ noLoc $ Unqual func) + $ fmap unLoc sgs + Nothing -> throwError $ GoalMismatch "apply" g + + +split :: TacticsM () +split = rule $ \(Judgement hy g) -> + case splitTyConApp_maybe $ unCType g of + Just (tc, apps) -> + case tyConDataCons tc of + [dc] -> buildDataCon hy dc apps + _ -> throwError $ GoalMismatch "split" g + Nothing -> throwError $ GoalMismatch "split" g + + +deepen :: Int -> TacticsM () +deepen 0 = pure () +deepen depth = do + one + deepen $ depth - 1 + +auto :: TacticsM () +auto = (intro >> auto) + (assumption >> auto) + (split >> auto) + (apply >> auto) + pure () + +one :: TacticsM () +one = intro assumption split apply pure () From b82ea25da050d42acc093d2f10f79f8f69318b14 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 11:26:53 -0700 Subject: [PATCH 10/63] Haddock for tactics machinery --- src/Ide/TacticMachinery.hs | 85 +++++++++++++++++++++++++------------- 1 file changed, 56 insertions(+), 29 deletions(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 54909c2b5f..d436fd692a 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -20,6 +20,8 @@ import TcType import Type +------------------------------------------------------------------------------ +-- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type } instance Eq CType where @@ -29,6 +31,8 @@ instance Ord CType where compare = nonDetCmpType `on` unCType +------------------------------------------------------------------------------ +-- | The current bindings and goal for a hole to be filled by refinery. data Judgement = Judgement { jHypothesis :: [(OccName, CType)] , jGoal :: CType @@ -36,6 +40,8 @@ data Judgement = Judgement deriving (Eq, Ord, Generic) +------------------------------------------------------------------------------ +-- | Reasons a tactic might fail. data TacticError = UndefinedHypothesis OccName | GoalMismatch String CType @@ -45,23 +51,36 @@ data TacticError type ProvableM = ProvableT Judgement (Either TacticError) type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM type RuleM = RuleT Judgement (LHsExpr GhcPs) ProvableM -type Rule = RuleM (LHsExpr GhcPs) +type Rule = RuleM (LHsExpr GhcPs) -newSubgoal :: [(OccName, CType)] -> CType -> RuleM (LHsExpr GhcPs) +------------------------------------------------------------------------------ +-- | Produce a subgoal that must be solved before we can solve the original +-- goal. +newSubgoal + :: [(OccName, CType)] -- ^ Available bindings + -> CType -- ^ Sub-goal type + -> RuleM (LHsExpr GhcPs) newSubgoal hy g = subgoal =<< newJudgement hy g +------------------------------------------------------------------------------ +-- | Create a new judgment newJudgement - :: ( Monad m) - => [(OccName, CType)] - -> CType + :: Monad m + => [(OccName, CType)] -- ^ Available bindings + -> CType -- ^ Sub-goal type -> m Judgement newJudgement hy g = do pure $ Judgement hy g -mkGoodName :: [OccName] -> Type -> OccName +------------------------------------------------------------------------------ +-- | Produce a unique, good name for a type. +mkGoodName + :: [OccName] -- ^ Bindings in scope; used to ensure we don't shadow anything + -> Type -- ^ The type to produce a name for + -> OccName mkGoodName in_scope t = let tn = mkTyName t in mkVarOcc $ case elem (mkVarOcc tn) in_scope of @@ -69,64 +88,72 @@ mkGoodName in_scope t = False -> tn +------------------------------------------------------------------------------ +-- | Use type information to create a reasonable name. mkTyName :: Type -> String +-- eg. mkTyName (a -> B) = "fab" mkTyName (tcSplitFunTys -> ([a@(isFunTy -> False)], b)) = "f" ++ mkTyName a ++ mkTyName b +-- eg. mkTyName (a -> b -> C) = "f_C" mkTyName (tcSplitFunTys -> ((_:_), b)) = "f_" ++ mkTyName b +-- eg. mkTyName (Either A B) = "eab" mkTyName (splitTyConApp_maybe -> Just (c, args)) = mkTyConName c ++ foldMap mkTyName args +-- eg. mkTyName a = "a" mkTyName (getTyVar_maybe-> Just tv) = occNameString $ occName tv +-- eg. mkTyName (forall x. y) = "y" mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) = mkTyName t mkTyName _ = "x" +------------------------------------------------------------------------------ +-- | Get a good name for a type constructor. mkTyConName :: TyCon -> String mkTyConName = fmap toLower . take 1 . occNameString . getOccName -tacticActual - :: TacticsM () - -> Judgement - -> Either TacticError (LHsExpr GhcPs) -tacticActual t = fmap fst . runProvableT . runTacticT t - - +------------------------------------------------------------------------------ +-- | Attempt to generate a term of the right type using in-scope bindings, and +-- a given tactic. runTactic - :: Type - -> [(OccName, Type)] - -> TacticsM () - -> Maybe (LHsExpr GhcPs) + :: Type -- ^ Desired type + -> [(OccName, Type)] -- ^ In-scope bindings + -> TacticsM () -- ^ Tactic to use + -> Either TacticError (LHsExpr GhcPs) runTactic ty hy t - = hush - . tacticActual t + = fmap fst + . runProvableT + . runTacticT t . Judgement (fmap (second CType) hy) $ CType ty -hush :: Either a b -> Maybe b -hush = either (const Nothing) Just - - instance MonadExtract (LHsExpr GhcPs) ProvableM where hole = pure $ noLoc $ HsUnboundVar NoExt $ TrueExprHole $ mkVarOcc "_" +------------------------------------------------------------------------------ +-- | Which names are in scope? getInScope :: [(OccName, a)] -> [OccName] getInScope = fmap fst +------------------------------------------------------------------------------ +-- | Construct a data con with subgoals for each field. buildDataCon - :: [(OccName, CType)] - -> DataCon - -> [Type] + :: [(OccName, CType)] -- ^ In-scope bindings + -> DataCon -- ^ The data con to build + -> [Type] -- ^ Type arguments for the data con -> RuleM (LHsExpr GhcPs) buildDataCon hy dc apps = do let args = dataConInstArgTys dc apps sgs <- traverse (newSubgoal hy . CType) args - pure . noLoc - . foldl' (@@) (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) - $ fmap unLoc sgs + pure + . noLoc + . foldl' (@@) + (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) + $ fmap unLoc sgs From 5e6454b9606d2d386e823ba2fc8326da1d213ff7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 11:32:23 -0700 Subject: [PATCH 11/63] Use a map for hypothesis --- src/Ide/TacticMachinery.hs | 53 +++++++++++++++++++------------------- src/Ide/Tactics.hs | 43 ++++++++++++++++--------------- 2 files changed, 49 insertions(+), 47 deletions(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index d436fd692a..318b4ff0b4 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -6,18 +6,19 @@ module Ide.TacticMachinery where -import Control.Arrow -import Data.Char -import Data.Function -import Data.List -import DataCon -import GHC -import GHC.Generics -import GHC.SourceGen.Overloaded -import Name -import Refinery.Tactic -import TcType -import Type +import Data.Char +import Data.Function +import Data.List +import Data.Map (Map) +import qualified Data.Map as M +import DataCon +import GHC +import GHC.Generics +import GHC.SourceGen.Overloaded +import Name +import Refinery.Tactic +import TcType +import Type ------------------------------------------------------------------------------ @@ -34,7 +35,7 @@ instance Ord CType where ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. data Judgement = Judgement - { jHypothesis :: [(OccName, CType)] + { jHypothesis :: Map OccName CType , jGoal :: CType } deriving (Eq, Ord, Generic) @@ -58,8 +59,8 @@ type Rule = RuleM (LHsExpr GhcPs) -- | Produce a subgoal that must be solved before we can solve the original -- goal. newSubgoal - :: [(OccName, CType)] -- ^ Available bindings - -> CType -- ^ Sub-goal type + :: Map OccName CType -- ^ Available bindings + -> CType -- ^ Sub-goal type -> RuleM (LHsExpr GhcPs) newSubgoal hy g = subgoal =<< newJudgement hy g @@ -68,8 +69,8 @@ newSubgoal hy g = subgoal =<< newJudgement hy g -- | Create a new judgment newJudgement :: Monad m - => [(OccName, CType)] -- ^ Available bindings - -> CType -- ^ Sub-goal type + => Map OccName CType -- ^ Available bindings + -> CType -- ^ Sub-goal type -> m Judgement newJudgement hy g = do pure $ Judgement hy g @@ -119,15 +120,15 @@ mkTyConName = fmap toLower . take 1 . occNameString . getOccName -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. runTactic - :: Type -- ^ Desired type - -> [(OccName, Type)] -- ^ In-scope bindings - -> TacticsM () -- ^ Tactic to use + :: Type -- ^ Desired type + -> Map OccName Type -- ^ In-scope bindings + -> TacticsM () -- ^ Tactic to use -> Either TacticError (LHsExpr GhcPs) runTactic ty hy t = fmap fst . runProvableT . runTacticT t - . Judgement (fmap (second CType) hy) + . Judgement (fmap CType hy) $ CType ty @@ -137,16 +138,16 @@ instance MonadExtract (LHsExpr GhcPs) ProvableM where ------------------------------------------------------------------------------ -- | Which names are in scope? -getInScope :: [(OccName, a)] -> [OccName] -getInScope = fmap fst +getInScope :: Map OccName a -> [OccName] +getInScope = M.keys ------------------------------------------------------------------------------ -- | Construct a data con with subgoals for each field. buildDataCon - :: [(OccName, CType)] -- ^ In-scope bindings - -> DataCon -- ^ The data con to build - -> [Type] -- ^ Type arguments for the data con + :: Map OccName CType -- ^ In-scope bindings + -> DataCon -- ^ The data con to build + -> [Type] -- ^ Type arguments for the data con -> RuleM (LHsExpr GhcPs) buildDataCon hy dc apps = do let args = dataConInstArgTys dc apps diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index 62c0e04ae8..e2820cb4e2 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -9,27 +9,28 @@ module Ide.Tactics , runTactic ) where -import Control.Monad.Except (throwError) -import Control.Monad.State -import Data.List -import Data.Traversable -import DataCon -import GHC -import GHC.Exts -import GHC.SourceGen.Binds -import GHC.SourceGen.Expr -import GHC.SourceGen.Overloaded -import GHC.SourceGen.Pat -import Ide.TacticMachinery -import Name -import Refinery.Tactic -import TyCoRep -import Type +import Control.Monad.Except (throwError) +import Control.Monad.State +import Data.List +import qualified Data.Map as M +import Data.Traversable +import DataCon +import GHC +import GHC.Exts +import GHC.SourceGen.Binds +import GHC.SourceGen.Expr +import GHC.SourceGen.Overloaded +import GHC.SourceGen.Pat +import Ide.TacticMachinery +import Name +import Refinery.Tactic +import TyCoRep +import Type assumption :: TacticsM () assumption = rule $ \(Judgement hy g) -> - case find ((== g) . snd) hy of + case find ((== g) . snd) $ toList hy of Just (v, _) -> pure $ noLoc $ HsVar NoExt $ noLoc $ Unqual v Nothing -> throwError $ GoalMismatch "assumption" g @@ -39,14 +40,14 @@ intro = rule $ \(Judgement hy g) -> case unCType g of (FunTy a b) -> do v <- pure $ mkGoodName (getInScope hy) a - sg <- newSubgoal ((v, CType a) : hy) $ CType b + sg <- newSubgoal (M.singleton v (CType a) <> hy) $ CType b pure $ noLoc $ lambda [VarPat noExt $ noLoc $ Unqual v] $ unLoc sg _ -> throwError $ GoalMismatch "intro" g destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM () destruct' f term = rule $ \(Judgement hy g) -> do - case find ((== term) . fst) hy of + case find ((== term) . fst) $ toList hy of Nothing -> throwError $ UndefinedHypothesis term Just (_, t) -> case splitTyConApp_maybe $ unCType t of @@ -67,7 +68,7 @@ destruct' f term = rule $ \(Judgement hy g) -> do pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) $ fmap (bvar . fromString . occNameString) names - j <- newJudgement (zip names (fmap CType args) ++ hy) g + j <- newJudgement (M.fromList (zip names (fmap CType args)) <> hy) g sg <- f dc j pure $ match [pat] $ unLoc sg @@ -82,7 +83,7 @@ homo = destruct' $ \dc (Judgement hy (CType g)) -> apply :: TacticsM () apply = rule $ \(Judgement hy g) -> do - case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) hy of + case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of Just (func, CType ty) -> do let (args, _) = splitFunTys ty sgs <- traverse (newSubgoal hy . CType) args From e434f6c242749ec2518592d6f010e971c23c4d5e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 11:37:05 -0700 Subject: [PATCH 12/63] Better types on LocalBindings --- src/Ide/LocalBindings.hs | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 4d8fc6b54f..691367e9c4 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -1,15 +1,21 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} -module Ide.LocalBindings where +module Ide.LocalBindings + ( Bindings (..) + , bindings + , isItAHole + ) where +import qualified Data.Set as S +import Data.Set (Set) +import qualified Data.Map as M +import Data.Map (Map) import Bag import Control.Lens import Data.Data.Lens import Data.Generics -import qualified Data.Map as M import Data.Monoid -import qualified Data.Set as S import GHC (TypecheckedModule (..), GhcTc) import HsBinds import HsExpr @@ -17,8 +23,20 @@ import Id import SrcLoc -bindings :: TypecheckedModule -> (S.Set Id, M.Map SrcSpan (S.Set Id)) -bindings = bindsBindings mempty . tm_typechecked_source +data Bindings = Bindings + { bGlobalBinds :: Set Id + , bLocalBinds :: Map SrcSpan (Set Id) + } deriving (Eq, Ord) + +instance Semigroup Bindings where + Bindings g1 l1 <> Bindings g2 l2 = Bindings (g1 <> g2) (l1 <> l2) + +instance Monoid Bindings where + mempty = Bindings mempty mempty + + +bindings :: TypecheckedModule -> Bindings +bindings = uncurry Bindings . bindsBindings mempty . tm_typechecked_source dataBindings :: Data a => S.Set Id -> a -> M.Map SrcSpan (S.Set Id) From 979dc53092d04236638aae0b469502ae5031d0ca Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 11:43:11 -0700 Subject: [PATCH 13/63] render the result of running a tactic --- src/Ide/TacticMachinery.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 318b4ff0b4..5ce8b0618a 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -19,6 +19,7 @@ import Name import Refinery.Tactic import TcType import Type +import Outputable ------------------------------------------------------------------------------ @@ -120,12 +121,13 @@ mkTyConName = fmap toLower . take 1 . occNameString . getOccName -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. runTactic - :: Type -- ^ Desired type + :: DynFlags + -> Type -- ^ Desired type -> Map OccName Type -- ^ In-scope bindings -> TacticsM () -- ^ Tactic to use - -> Either TacticError (LHsExpr GhcPs) -runTactic ty hy t - = fmap fst + -> Either TacticError String +runTactic dflags ty hy t + = fmap (showSDoc dflags . ppr . fst) . runProvableT . runTacticT t . Judgement (fmap CType hy) From 03f04f6a2e2d7a2deb93fa2f8b19ccfcff807f73 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 11:56:12 -0700 Subject: [PATCH 14/63] Hypothesis from bindings --- src/Ide/LocalBindings.hs | 8 ++++---- src/Ide/TacticMachinery.hs | 21 ++++++++++++++++++++- 2 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 691367e9c4..824f648375 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -7,15 +7,15 @@ module Ide.LocalBindings , isItAHole ) where -import qualified Data.Set as S -import Data.Set (Set) -import qualified Data.Map as M -import Data.Map (Map) import Bag import Control.Lens import Data.Data.Lens import Data.Generics +import Data.Map (Map) +import qualified Data.Map as M import Data.Monoid +import Data.Set (Set) +import qualified Data.Set as S import GHC (TypecheckedModule (..), GhcTc) import HsBinds import HsExpr diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 5ce8b0618a..c899191d36 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -6,20 +6,25 @@ module Ide.TacticMachinery where +import Control.Arrow import Data.Char import Data.Function import Data.List import Data.Map (Map) import qualified Data.Map as M +import Data.Set (Set) +import qualified Data.Set as S import DataCon import GHC import GHC.Generics import GHC.SourceGen.Overloaded +import Ide.LocalBindings import Name +import Outputable (ppr, showSDoc) +import Data.Maybe import Refinery.Tactic import TcType import Type -import Outputable ------------------------------------------------------------------------------ @@ -33,6 +38,20 @@ instance Ord CType where compare = nonDetCmpType `on` unCType +------------------------------------------------------------------------------ +-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. +hypothesisFromBindings :: SrcSpan -> Bindings -> Map OccName CType +hypothesisFromBindings span (Bindings global local) = + buildHypothesis global + <> buildHypothesis (fromMaybe mempty $ M.lookup span local) + + +------------------------------------------------------------------------------ +-- | Convert a @Set Id@ into a hypothesis. +buildHypothesis :: Set Id -> Map OccName CType +buildHypothesis s = M.fromList $ fmap (occName &&& CType . varType) $ S.toList s + + ------------------------------------------------------------------------------ -- | The current bindings and goal for a hole to be filled by refinery. data Judgement = Judgement From 5aacafc34d05ccee38a0cf204a7a0419cd06a360 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 12:04:35 -0700 Subject: [PATCH 15/63] Sort types --- src/Ide/TacticMachinery.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index c899191d36..79f7fcc104 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -12,6 +12,7 @@ import Data.Function import Data.List import Data.Map (Map) import qualified Data.Map as M +import Data.Maybe import Data.Set (Set) import qualified Data.Set as S import DataCon @@ -21,7 +22,6 @@ import GHC.SourceGen.Overloaded import Ide.LocalBindings import Name import Outputable (ppr, showSDoc) -import Data.Maybe import Refinery.Tactic import TcType import Type From c7bb9914de3b6c03874d5d4ab9c824df424b3e20 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 12:28:49 -0700 Subject: [PATCH 16/63] mostSpecificSpan --- src/Ide/LocalBindings.hs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 824f648375..33d40d4ba9 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -4,15 +4,19 @@ module Ide.LocalBindings ( Bindings (..) , bindings + , mostSpecificSpan , isItAHole ) where import Bag import Control.Lens import Data.Data.Lens +import Data.Function import Data.Generics +import Data.List import Data.Map (Map) import qualified Data.Map as M +import Data.Maybe import Data.Monoid import Data.Set (Set) import qualified Data.Set as S @@ -135,6 +139,16 @@ bindsBindings in_scope binds = XHsBindsLR _ -> mempty +mostSpecificSpan :: (Data a, Typeable pass) => SrcSpan -> a -> Maybe (LHsExpr pass) +mostSpecificSpan span z + = listToMaybe + $ sortBy (leftmost_smallest `on` getLoc) + $ everything (<>) (mkQ mempty $ \case + L span' a | span `isSubspanOf` span' -> [a] + _ -> []) + $ z + + isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar isItAHole tcm span = getFirst $ everything (<>) ( From 0078219d88f425ad2600f0ee94a6a197c6a310c5 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 12:31:29 -0700 Subject: [PATCH 17/63] Render --- src/Ide/TacticMachinery.hs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 79f7fcc104..59162f4b35 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -1,5 +1,7 @@ {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} @@ -21,7 +23,7 @@ import GHC.Generics import GHC.SourceGen.Overloaded import Ide.LocalBindings import Name -import Outputable (ppr, showSDoc) +import Outputable (ppr, showSDoc, Outputable) import Refinery.Tactic import TcType import Type @@ -146,7 +148,7 @@ runTactic -> TacticsM () -- ^ Tactic to use -> Either TacticError String runTactic dflags ty hy t - = fmap (showSDoc dflags . ppr . fst) + = fmap (render dflags . fst) . runProvableT . runTacticT t . Judgement (fmap CType hy) @@ -179,3 +181,7 @@ buildDataCon hy dc apps = do (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs + +render :: Outputable (LHsExpr pass) => DynFlags -> LHsExpr pass -> String +render dflags = showSDoc dflags . ppr + From 6c1ea41b96aceb043c43afe0499bb6f725dd5e0e Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 12:52:07 -0700 Subject: [PATCH 18/63] slightly better span --- src/Ide/LocalBindings.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 33d40d4ba9..d43098a581 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -144,8 +144,8 @@ mostSpecificSpan span z = listToMaybe $ sortBy (leftmost_smallest `on` getLoc) $ everything (<>) (mkQ mempty $ \case - L span' a | span `isSubspanOf` span' -> [a] - _ -> []) + l@(L span' _) | span `isSubspanOf` span' -> [l] + _ -> []) $ z From edae73607debe8e1b1b766ed5073dee666066534 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 12:58:52 -0700 Subject: [PATCH 19/63] better sorting for specific spans --- src/Ide/LocalBindings.hs | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index d43098a581..9259f6957d 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -8,6 +8,7 @@ module Ide.LocalBindings , isItAHole ) where +import Data.Ord import Bag import Control.Lens import Data.Data.Lens @@ -139,10 +140,20 @@ bindsBindings in_scope binds = XHsBindsLR _ -> mempty +size :: SrcSpan -> Int +size (UnhelpfulSpan _) = maxBound +size (RealSrcSpan span) = + (srcSpanEndLine span - srcSpanStartLine span) * 1000 - + (srcSpanEndCol span - srcSpanStartCol span) + +smallest :: SrcSpan -> SrcSpan -> Ordering +smallest = comparing size + + mostSpecificSpan :: (Data a, Typeable pass) => SrcSpan -> a -> Maybe (LHsExpr pass) mostSpecificSpan span z = listToMaybe - $ sortBy (leftmost_smallest `on` getLoc) + $ sortBy (smallest `on` getLoc) $ everything (<>) (mkQ mempty $ \case l@(L span' _) | span `isSubspanOf` span' -> [l] _ -> []) From 5bb8c66daa204a88cc889593b468bf7f9a0081a5 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 7 Sep 2020 13:00:10 -0700 Subject: [PATCH 20/63] Actually add the tactic plugin :) --- exe/Main.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/exe/Main.hs b/exe/Main.hs index 7a5bd8e44e..58745e9793 100644 --- a/exe/Main.hs +++ b/exe/Main.hs @@ -73,6 +73,7 @@ import Ide.Plugin.ImportLens as ImportLens import Ide.Plugin.Ormolu as Ormolu import Ide.Plugin.StylishHaskell as StylishHaskell import Ide.Plugin.Retrie as Retrie +import Ide.Plugin.Tactic as Tactic #if AGPL import Ide.Plugin.Brittany as Brittany #endif @@ -106,6 +107,7 @@ idePlugins includeExamples = pluginDescToIdePlugins allPlugins , Pragmas.descriptor "pragmas" , Floskell.descriptor "floskell" , Fourmolu.descriptor "fourmolu" + , Tactic.descriptor "tactic" -- , genericDescriptor "generic" -- , ghcmodDescriptor "ghcmod" , Ormolu.descriptor "ormolu" From a78b440c312fd305cb4c37a33f3f0d21174f0955 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 7 Sep 2020 13:05:50 -0700 Subject: [PATCH 21/63] [WIP] Do stuff --- haskell-language-server.cabal | 3 +++ src/Ide/LocalBindings.hs | 5 ++--- src/Ide/Plugin/Tactic.hs | 41 ++++++++++++++++++++++++++++++----- 3 files changed, 40 insertions(+), 9 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 3813686881..b488bd0c18 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -39,6 +39,7 @@ common agpl library import: agpl exposed-modules: + Ide.LocalBindings Ide.Logger Ide.Plugin Ide.Plugin.Config @@ -56,6 +57,8 @@ library Ide.Plugin.Formatter Ide.Plugin.StylishHaskell Ide.PluginUtils + Ide.TacticMachinery + Ide.Tactics Ide.Types Ide.Version other-modules: diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 33d40d4ba9..cbfbc71f67 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -144,11 +144,10 @@ mostSpecificSpan span z = listToMaybe $ sortBy (leftmost_smallest `on` getLoc) $ everything (<>) (mkQ mempty $ \case - L span' a | span `isSubspanOf` span' -> [a] - _ -> []) + l@(L span' _) | span `isSubspanOf` span' -> [l] + _ -> []) $ z - isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar isItAHole tcm span = getFirst $ everything (<>) ( diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 3bc8fd4854..02d14ef56e 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} -- | A plugin that uses tactics to synthesize code @@ -8,7 +9,10 @@ module Ide.Plugin.Tactic ) where import Data.Aeson +import Data.Coerce +import Data.Maybe import qualified Data.HashMap.Strict as H +import qualified Data.Text as T import qualified GHC.Generics as Generics import Development.IDE.Core.RuleTypes (GhcSessionDeps (GhcSessionDeps), @@ -17,31 +21,56 @@ import Development.IDE.Core.RuleTypes (GhcSessionDeps (GhcSessionDeps) import Development.IDE.Core.Shake (use, IdeState (..)) import Development.IDE.Core.Service (runAction) import Development.Shake (Action) +import Development.IDE.GHC.Util import Ide.Types +import Ide.TacticMachinery +import Ide.Plugin +import Ide.LocalBindings import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types +import FastString +import HsBinds +import HsExpr +import GHC +import SrcLoc +import DynFlags + + +import System.IO -- import Refinery.Tactic descriptor :: PluginId -> PluginDescriptor descriptor plId = (defaultPluginDescriptor plId) - { pluginCommands = [PluginCommand "fillHole" "fill the hole using a tactic" tacticCmd] + { pluginCommands = [PluginCommand (coerce tacticCommandName) "fill the hole using a tactic" tacticCmd] , pluginCodeActionProvider = Just codeActionProvider } +tacticCommandName :: T.Text +tacticCommandName = "tacticCommand" + runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state +rangeToSrcSpan :: String -> Range -> SrcSpan +rangeToSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = + mkSrcSpan (mkSrcLoc (fsLit file) (startLn + 1) (startCh + 1)) (mkSrcLoc (fsLit file) (endLn + 1) (endCh + 1)) + codeActionProvider :: CodeActionProvider -codeActionProvider _conf state _plid (TextDocumentIdentifier uri) range _ctx +codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - tmr <- runIde state $ use TypeCheck nfp + Just tmr <- runIde state $ use TypeCheck nfp + -- FIXME Get the dynflags from this? hsc <- runIde state $ use GhcSessionDeps nfp - -- TODO Check if we have a hole inside of the range. - -- Go from range -> SrcSpan, then look inside the module contents - _hole + let title = "Fill Hole" + let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range + let mod = tmrModule tmr + cmd <- mkLspCommand plId (coerce tacticCommandName) title Nothing + case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of + Just hole -> pure (Right (List [ CACodeAction $ CodeAction (title <> " " <> (T.pack $ render unsafeGlobalDynFlags hole)) (Just CodeActionQuickFix) Nothing Nothing (Just cmd) ])) + Nothing -> pure (Right (List [ CACodeAction $ CodeAction ("Broken: " <> " ") (Just CodeActionQuickFix) Nothing Nothing (Just cmd) ])) data TacticParams = TacticParams From 65e59fc6304c1403c368a46d1b498e8ca9606274 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 13:15:53 -0700 Subject: [PATCH 22/63] Fix size --- src/Ide/LocalBindings.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 9259f6957d..106899433a 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -140,11 +140,12 @@ bindsBindings in_scope binds = XHsBindsLR _ -> mempty -size :: SrcSpan -> Int +size :: SrcSpan -> (Int, Int) size (UnhelpfulSpan _) = maxBound size (RealSrcSpan span) = - (srcSpanEndLine span - srcSpanStartLine span) * 1000 - - (srcSpanEndCol span - srcSpanStartCol span) + ( srcSpanEndLine span - srcSpanStartLine span + , srcSpanEndCol span - srcSpanStartCol span + ) smallest :: SrcSpan -> SrcSpan -> Ordering smallest = comparing size From ccb799da32eca91f8d0aa221dc4c36b254bb6918 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 7 Sep 2020 13:33:35 -0700 Subject: [PATCH 23/63] [WIP] It does the thing!! --- src/Ide/Plugin/Tactic.hs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 02d14ef56e..56f7450d99 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -21,6 +21,7 @@ import Development.IDE.Core.RuleTypes (GhcSessionDeps (GhcSessionDeps) import Development.IDE.Core.Shake (use, IdeState (..)) import Development.IDE.Core.Service (runAction) import Development.Shake (Action) +import Development.IDE.GHC.Error import Development.IDE.GHC.Util import Ide.Types @@ -67,10 +68,16 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx let title = "Fill Hole" let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range let mod = tmrModule tmr - cmd <- mkLspCommand plId (coerce tacticCommandName) title Nothing case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of - Just hole -> pure (Right (List [ CACodeAction $ CodeAction (title <> " " <> (T.pack $ render unsafeGlobalDynFlags hole)) (Just CodeActionQuickFix) Nothing Nothing (Just cmd) ])) - Nothing -> pure (Right (List [ CACodeAction $ CodeAction ("Broken: " <> " ") (Just CodeActionQuickFix) Nothing Nothing (Just cmd) ])) + -- FIXME For some reason we get an HsVar instead of an HsUnboundVar. We should + -- check if this is a hole somehow?? + Just (L span' (HsVar _ _)) -> do + -- FIXME What happens if the range is unhelpful? + let params = TacticParams { file = uri, range = fromJust $ srcSpanToRange span' } + cmd <- mkLspCommand plId (coerce tacticCommandName) title (Just [toJSON params]) + pure (Right (List [ CACodeAction $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing (Just cmd) ])) + Just e -> pure (Right (List [ CACodeAction $ CodeAction (T.pack (render unsafeGlobalDynFlags e)) (Just CodeActionQuickFix) Nothing Nothing Nothing ])) + Nothing -> pure (Right (List [])) data TacticParams = TacticParams From 425e9bcca121672cb27535e160ec775e8e3c7ddb Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 14:11:36 -0700 Subject: [PATCH 24/63] Parenthesize if necessary --- src/Ide/TacticMachinery.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 59162f4b35..724897f1f3 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -148,7 +148,7 @@ runTactic -> TacticsM () -- ^ Tactic to use -> Either TacticError String runTactic dflags ty hy t - = fmap (render dflags . fst) + = fmap (render dflags . noLoc . HsPar NoExt . fst) . runProvableT . runTacticT t . Judgement (fmap CType hy) From 385ee7ecc09207b2127c88e5a84c6c29c55c572e Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 7 Sep 2020 14:12:59 -0700 Subject: [PATCH 25/63] Multiple tactic actions --- src/Ide/Plugin/Tactic.hs | 60 ++++++++++++++++++++++++++------------ src/Ide/TacticMachinery.hs | 5 ++-- 2 files changed, 44 insertions(+), 21 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 56f7450d99..4aa1e0b822 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -11,6 +11,8 @@ module Ide.Plugin.Tactic import Data.Aeson import Data.Coerce import Data.Maybe +import Data.Traversable +import qualified Data.Map as Map import qualified Data.HashMap.Strict as H import qualified Data.Text as T import qualified GHC.Generics as Generics @@ -26,6 +28,7 @@ import Development.IDE.GHC.Util import Ide.Types import Ide.TacticMachinery +import Ide.Tactics import Ide.Plugin import Ide.LocalBindings @@ -38,6 +41,7 @@ import HsExpr import GHC import SrcLoc import DynFlags +import Type import System.IO @@ -45,12 +49,18 @@ import System.IO descriptor :: PluginId -> PluginDescriptor descriptor plId = (defaultPluginDescriptor plId) - { pluginCommands = [PluginCommand (coerce tacticCommandName) "fill the hole using a tactic" tacticCmd] + { pluginCommands = fmap (\(name, tac) -> PluginCommand (coerce $ name <> "Command") (tacticDesc name) (tacticCmd tac)) $ Map.toList tacticCommands , pluginCodeActionProvider = Just codeActionProvider } +tacticDesc :: T.Text -> T.Text +tacticDesc name = "fill the hole using the " <> name <> " tactic" -tacticCommandName :: T.Text -tacticCommandName = "tacticCommand" +tacticCommands :: Map.Map T.Text (TacticsM ()) +tacticCommands = Map.fromList + [ ("auto", auto) + , ("split", split) + , ("intro", intro) + ] runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state @@ -63,9 +73,6 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do Just tmr <- runIde state $ use TypeCheck nfp - -- FIXME Get the dynflags from this? - hsc <- runIde state $ use GhcSessionDeps nfp - let title = "Fill Hole" let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range let mod = tmrModule tmr case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of @@ -74,8 +81,11 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx Just (L span' (HsVar _ _)) -> do -- FIXME What happens if the range is unhelpful? let params = TacticParams { file = uri, range = fromJust $ srcSpanToRange span' } - cmd <- mkLspCommand plId (coerce tacticCommandName) title (Just [toJSON params]) - pure (Right (List [ CACodeAction $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing (Just cmd) ])) + let names = Map.keys tacticCommands + actions <- for names $ \name -> do + cmd <- mkLspCommand plId (coerce $ name <> "Command") name (Just [toJSON params]) + pure $ CACodeAction $ CodeAction name (Just CodeActionQuickFix) Nothing Nothing (Just cmd) + pure $ Right $ List actions Just e -> pure (Right (List [ CACodeAction $ CodeAction (T.pack (render unsafeGlobalDynFlags e)) (Just CodeActionQuickFix) Nothing Nothing Nothing ])) Nothing -> pure (Right (List [])) @@ -86,13 +96,27 @@ data TacticParams = TacticParams } deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) -tacticCmd :: CommandFunction TacticParams -tacticCmd _lf _ide (TacticParams uri range) = do - let - textEdits = J.List - [J.TextEdit range ("Howdy Partner!") - ] - res = J.WorkspaceEdit - (Just $ H.singleton uri textEdits) - Nothing - pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) +tacticCmd :: TacticsM () -> CommandFunction TacticParams +tacticCmd tac _lf state (TacticParams uri range) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + Just tmr <- runIde state $ use TypeCheck nfp + let + span = rangeToSrcSpan (fromNormalizedFilePath nfp) range + mod = tmrModule tmr + hyps = hypothesisFromBindings span $ bindings mod + Just (L _ (HsVar _ (L _ v))) = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) + goal = varType v + case runTactic unsafeGlobalDynFlags goal hyps tac of + Left err -> pure (Right Null, Nothing) + Right res -> + let edit = J.List [ J.TextEdit range (T.pack res) ] + response = J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing + in pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response)) + -- result = runTactic unsafeGlobalDynFlags goal hyps _tac + -- textEdits = J.List + -- [J.TextEdit range ("Howdy Partner!") + -- ] + -- res = J.WorkspaceEdit + -- (Just $ H.singleton uri textEdits) + -- Nothing + -- pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 59162f4b35..929bf48532 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -144,14 +144,14 @@ mkTyConName = fmap toLower . take 1 . occNameString . getOccName runTactic :: DynFlags -> Type -- ^ Desired type - -> Map OccName Type -- ^ In-scope bindings + -> Map OccName CType -- ^ In-scope bindings -> TacticsM () -- ^ Tactic to use -> Either TacticError String runTactic dflags ty hy t = fmap (render dflags . fst) . runProvableT . runTacticT t - . Judgement (fmap CType hy) + . Judgement hy $ CType ty @@ -181,7 +181,6 @@ buildDataCon hy dc apps = do (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs - render :: Outputable (LHsExpr pass) => DynFlags -> LHsExpr pass -> String render dflags = showSDoc dflags . ppr From 1fcc5d822df9de423d472bb7903fbd316be551c9 Mon Sep 17 00:00:00 2001 From: TOTBWF Date: Mon, 7 Sep 2020 14:29:14 -0700 Subject: [PATCH 26/63] [WIP] Home on the 'Range' --- src/Ide/Plugin/Tactic.hs | 26 +++++++++----------------- src/Ide/TacticMachinery.hs | 5 +++++ 2 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 4aa1e0b822..d854db5502 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -20,7 +20,8 @@ import qualified GHC.Generics as Generics import Development.IDE.Core.RuleTypes (GhcSessionDeps (GhcSessionDeps), TcModuleResult (tmrModule), TypeCheck (TypeCheck)) -import Development.IDE.Core.Shake (use, IdeState (..)) +import Development.IDE.Core.Shake (useWithStale, IdeState (..)) +import Development.IDE.Core.PositionMapping import Development.IDE.Core.Service (runAction) import Development.Shake (Action) import Development.IDE.GHC.Error @@ -72,15 +73,14 @@ rangeToSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - Just tmr <- runIde state $ use TypeCheck nfp - let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range + Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp + let span = rangeToSrcSpan (fromNormalizedFilePath nfp) $ fromMaybe (error "bummer") $ fromCurrentRange pos range let mod = tmrModule tmr case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of -- FIXME For some reason we get an HsVar instead of an HsUnboundVar. We should -- check if this is a hole somehow?? Just (L span' (HsVar _ _)) -> do - -- FIXME What happens if the range is unhelpful? - let params = TacticParams { file = uri, range = fromJust $ srcSpanToRange span' } + let params = TacticParams { file = uri, range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' } let names = Map.keys tacticCommands actions <- for names $ \name -> do cmd <- mkLspCommand plId (coerce $ name <> "Command") name (Just [toJSON params]) @@ -99,24 +99,16 @@ data TacticParams = TacticParams tacticCmd :: TacticsM () -> CommandFunction TacticParams tacticCmd tac _lf state (TacticParams uri range) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - Just tmr <- runIde state $ use TypeCheck nfp + Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp let - span = rangeToSrcSpan (fromNormalizedFilePath nfp) range + span = rangeToSrcSpan (fromNormalizedFilePath nfp) $ fromMaybe (error "Oh shucks") $ fromCurrentRange pos range mod = tmrModule tmr hyps = hypothesisFromBindings span $ bindings mod Just (L _ (HsVar _ (L _ v))) = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) goal = varType v case runTactic unsafeGlobalDynFlags goal hyps tac of - Left err -> pure (Right Null, Nothing) + Left err -> pure (Left (ResponseError InvalidRequest (T.pack $ show err) Nothing), Nothing) Right res -> - let edit = J.List [ J.TextEdit range (T.pack res) ] + let edit = J.List [ J.TextEdit (fromMaybe (error "Fiddlesticks" ) $ toCurrentRange pos range) (T.pack res) ] response = J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing in pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response)) - -- result = runTactic unsafeGlobalDynFlags goal hyps _tac - -- textEdits = J.List - -- [J.TextEdit range ("Howdy Partner!") - -- ] - -- res = J.WorkspaceEdit - -- (Just $ H.singleton uri textEdits) - -- Nothing - -- pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 019889e725..40fa7929b3 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -70,6 +70,11 @@ data TacticError | GoalMismatch String CType | UnsolvedSubgoals [Judgement] +instance Show TacticError where + show (UndefinedHypothesis name) = "undefined is not a function" + show (GoalMismatch str typ) = "oh no" + show (UnsolvedSubgoals jdgs) = "so sad" + type ProvableM = ProvableT Judgement (Either TacticError) type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM From 9b567e658f96c6721a9b4d5e86738e24882e2b26 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 14:34:53 -0700 Subject: [PATCH 27/63] destruct and homo --- src/Ide/Plugin/Tactic.hs | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index d854db5502..a7dce07940 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -36,6 +36,7 @@ import Ide.LocalBindings import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types +import OccName import FastString import HsBinds import HsExpr @@ -56,11 +57,13 @@ descriptor plId = (defaultPluginDescriptor plId) tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" -tacticCommands :: Map.Map T.Text (TacticsM ()) +tacticCommands :: Map.Map T.Text (OccName -> TacticsM ()) tacticCommands = Map.fromList - [ ("auto", auto) - , ("split", split) - , ("intro", intro) + [ ("auto", const auto) + , ("split", const split) + , ("intro", const intro) + , ("destruct", destruct) + , ("homo", homo) ] runIde :: IdeState -> Action a -> IO a @@ -79,8 +82,12 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of -- FIXME For some reason we get an HsVar instead of an HsUnboundVar. We should -- check if this is a hole somehow?? - Just (L span' (HsVar _ _)) -> do - let params = TacticParams { file = uri, range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' } + Just (L span' (HsVar _ (L _ var))) -> do + let params = TacticParams + { file = uri + , range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' + , var_name = T.pack $ occNameString $ occName var + } let names = Map.keys tacticCommands actions <- for names $ \name -> do cmd <- mkLspCommand plId (coerce $ name <> "Command") name (Just [toJSON params]) @@ -93,11 +100,12 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx data TacticParams = TacticParams { file :: J.Uri -- ^ Uri of the file to fill the hole in , range :: J.Range -- ^ The range of the hole + , var_name :: T.Text } deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) -tacticCmd :: TacticsM () -> CommandFunction TacticParams -tacticCmd tac _lf state (TacticParams uri range) +tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams +tacticCmd tac _lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp let @@ -106,7 +114,7 @@ tacticCmd tac _lf state (TacticParams uri range) hyps = hypothesisFromBindings span $ bindings mod Just (L _ (HsVar _ (L _ v))) = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) goal = varType v - case runTactic unsafeGlobalDynFlags goal hyps tac of + case runTactic unsafeGlobalDynFlags goal hyps (tac $ mkVarOcc $ T.unpack var_name) of Left err -> pure (Left (ResponseError InvalidRequest (T.pack $ show err) Nothing), Nothing) Right res -> let edit = J.List [ J.TextEdit (fromMaybe (error "Fiddlesticks" ) $ toCurrentRange pos range) (T.pack res) ] From 4de1ab24a600df4c858a12d014e6545c051673fa Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 14:49:53 -0700 Subject: [PATCH 28/63] fix naming and parens --- src/Ide/TacticMachinery.hs | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 40fa7929b3..27c6087b1a 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -27,6 +27,7 @@ import Outputable (ppr, showSDoc, Outputable) import Refinery.Tactic import TcType import Type +import TysWiredIn (listTyCon, pairTyCon) ------------------------------------------------------------------------------ @@ -140,7 +141,10 @@ mkTyName _ = "x" ------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String -mkTyConName = fmap toLower . take 1 . occNameString . getOccName +mkTyConName tc + | tc == listTyCon = "l_" + | tc == pairTyCon = "p_" + | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc ------------------------------------------------------------------------------ @@ -153,13 +157,25 @@ runTactic -> TacticsM () -- ^ Tactic to use -> Either TacticError String runTactic dflags ty hy t - = fmap (render dflags . noLoc . HsPar NoExt . fst) + = fmap (render dflags . parenthesize . fst) . runProvableT . runTacticT t . Judgement hy $ CType ty +------------------------------------------------------------------------------ +-- | Put parentheses around an expression if required. +parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs +parenthesize a@(L _ HsVar{}) = a +parenthesize a@(L _ HsUnboundVar{}) = a +parenthesize a@(L _ HsOverLabel{}) = a +parenthesize a@(L _ HsOverLit{}) = a +parenthesize a@(L _ HsIPVar{}) = a +parenthesize a@(L _ HsLit{}) = a +parenthesize a = noLoc $ HsPar NoExt a + + instance MonadExtract (LHsExpr GhcPs) ProvableM where hole = pure $ noLoc $ HsUnboundVar NoExt $ TrueExprHole $ mkVarOcc "_" From ca6ef7a4e78668aacd4900ff67f1a6287d080186 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 15:19:39 -0700 Subject: [PATCH 29/63] Cleanup Plugin Tactic --- ghcide | 2 +- haskell-language-server.cabal | 126 ++++++++++++++-------------- src/Ide/Plugin/Tactic.hs | 150 ++++++++++++++++++++++------------ stack.yaml | 2 +- 4 files changed, 161 insertions(+), 119 deletions(-) diff --git a/ghcide b/ghcide index 078e3d3c0d..26517c6af0 160000 --- a/ghcide +++ b/ghcide @@ -1 +1 @@ -Subproject commit 078e3d3c0d319f83841ccbcdc60ff5f0e243f6be +Subproject commit 26517c6af0bc83181de248406e8e570351748331 diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index b488bd0c18..2675cf80f3 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -246,67 +246,67 @@ common hls-test-utils ghc-options: -Werror default-language: Haskell2010 -test-suite func-test - import: agpl, hls-test-utils - type: exitcode-stdio-1.0 - default-language: Haskell2010 - build-tool-depends: haskell-language-server:haskell-language-server - , ghcide:ghcide-test-preprocessor - build-depends: base >=4.7 && <5 - , aeson - , bytestring - , data-default - , directory - , filepath - , haskell-language-server - , haskell-lsp - , haskell-lsp-types - , lens - , lsp-test >= 0.11.0.4 - , tasty - , tasty-ant-xml >= 1.1.6 - , tasty-expected-failure - , tasty-golden - , tasty-hunit - , tasty-rerun - , text - , unordered-containers - hs-source-dirs: test/functional - main-is: Main.hs - other-modules: Command - , Completion - , Deferred - , Definition - , Diagnostic - , Eval - , Format - , FunctionalBadProject - , FunctionalCodeAction - , FunctionalLiquid - , HieBios - , Highlight - , Progress - , Reference - , Rename - , Symbol - , TypeDefinition - ghc-options: -Wall - -Wno-name-shadowing - -threaded -rtsopts -with-rtsopts=-N - if flag(pedantic) - ghc-options: -Werror -Wredundant-constraints +-- test-suite func-test +-- import: agpl, hls-test-utils +-- type: exitcode-stdio-1.0 +-- default-language: Haskell2010 +-- build-tool-depends: haskell-language-server:haskell-language-server +-- , ghcide:ghcide-test-preprocessor +-- build-depends: base >=4.7 && <5 +-- , aeson +-- , bytestring +-- , data-default +-- , directory +-- , filepath +-- , haskell-language-server +-- , haskell-lsp +-- , haskell-lsp-types +-- , lens +-- , lsp-test >= 0.11.0.4 +-- , tasty +-- , tasty-ant-xml >= 1.1.6 +-- , tasty-expected-failure +-- , tasty-golden +-- , tasty-hunit +-- , tasty-rerun +-- , text +-- , unordered-containers +-- hs-source-dirs: test/functional +-- main-is: Main.hs +-- other-modules: Command +-- , Completion +-- , Deferred +-- , Definition +-- , Diagnostic +-- , Eval +-- , Format +-- , FunctionalBadProject +-- , FunctionalCodeAction +-- , FunctionalLiquid +-- , HieBios +-- , Highlight +-- , Progress +-- , Reference +-- , Rename +-- , Symbol +-- , TypeDefinition +-- ghc-options: -Wall +-- -Wno-name-shadowing +-- -threaded -rtsopts -with-rtsopts=-N +-- if flag(pedantic) +-- ghc-options: -Werror -Wredundant-constraints -test-suite wrapper-test - import: agpl, hls-test-utils - type: exitcode-stdio-1.0 - build-tool-depends: haskell-language-server:haskell-language-server-wrapper - default-language: Haskell2010 - build-depends: base == 4.* - , directory - , process - , tasty - , tasty-hunit - , tasty-ant-xml >= 1.1.6 - hs-source-dirs: test/wrapper - main-is: Main.hs - ghc-options: -Wall +-- test-suite wrapper-test +-- import: agpl, hls-test-utils +-- type: exitcode-stdio-1.0 +-- build-tool-depends: haskell-language-server:haskell-language-server-wrapper +-- default-language: Haskell2010 +-- build-depends: base == 4.* +-- , directory +-- , process +-- , tasty +-- , tasty-hunit +-- , tasty-ant-xml >= 1.1.6 +-- hs-source-dirs: test/wrapper +-- main-is: Main.hs +-- ghc-options: -Wall diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index a7dce07940..b2e9c02315 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,8 +1,9 @@ +-- | A plugin that uses tactics to synthesize code {-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} --- | A plugin that uses tactics to synthesize code +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} module Ide.Plugin.Tactic ( descriptor @@ -17,15 +18,13 @@ import qualified Data.HashMap.Strict as H import qualified Data.Text as T import qualified GHC.Generics as Generics -import Development.IDE.Core.RuleTypes (GhcSessionDeps (GhcSessionDeps), - TcModuleResult (tmrModule), +import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (TypeCheck)) import Development.IDE.Core.Shake (useWithStale, IdeState (..)) import Development.IDE.Core.PositionMapping import Development.IDE.Core.Service (runAction) import Development.Shake (Action) import Development.IDE.GHC.Error -import Development.IDE.GHC.Util import Ide.Types import Ide.TacticMachinery @@ -37,21 +36,21 @@ import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types import OccName -import FastString -import HsBinds import HsExpr import GHC -import SrcLoc import DynFlags import Type -import System.IO --- import Refinery.Tactic - descriptor :: PluginId -> PluginDescriptor descriptor plId = (defaultPluginDescriptor plId) - { pluginCommands = fmap (\(name, tac) -> PluginCommand (coerce $ name <> "Command") (tacticDesc name) (tacticCmd tac)) $ Map.toList tacticCommands + { pluginCommands + = fmap (\(name, tac) -> + PluginCommand + (coerce $ name <> "Command") + (tacticDesc name) + (tacticCmd tac)) $ + Map.toList tacticCommands , pluginCodeActionProvider = Just codeActionProvider } tacticDesc :: T.Text -> T.Text @@ -59,42 +58,57 @@ tacticDesc name = "fill the hole using the " <> name <> " tactic" tacticCommands :: Map.Map T.Text (OccName -> TacticsM ()) tacticCommands = Map.fromList - [ ("auto", const auto) - , ("split", const split) - , ("intro", const intro) + [ ("auto", const auto) + , ("split", const split) + , ("intro", const intro) , ("destruct", destruct) - , ("homo", homo) + , ("homo", homo) ] runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state -rangeToSrcSpan :: String -> Range -> SrcSpan -rangeToSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = - mkSrcSpan (mkSrcLoc (fsLit file) (startLn + 1) (startCh + 1)) (mkSrcLoc (fsLit file) (endLn + 1) (endCh + 1)) - codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp - let span = rangeToSrcSpan (fromNormalizedFilePath nfp) $ fromMaybe (error "bummer") $ fromCurrentRange pos range - let mod = tmrModule tmr - case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of - -- FIXME For some reason we get an HsVar instead of an HsUnboundVar. We should - -- check if this is a hole somehow?? - Just (L span' (HsVar _ (L _ var))) -> do - let params = TacticParams - { file = uri - , range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - , var_name = T.pack $ occNameString $ occName var - } - let names = Map.keys tacticCommands - actions <- for names $ \name -> do - cmd <- mkLspCommand plId (coerce $ name <> "Command") name (Just [toJSON params]) - pure $ CACodeAction $ CodeAction name (Just CodeActionQuickFix) Nothing Nothing (Just cmd) - pure $ Right $ List actions - Just e -> pure (Right (List [ CACodeAction $ CodeAction (T.pack (render unsafeGlobalDynFlags e)) (Just CodeActionQuickFix) Nothing Nothing Nothing ])) - Nothing -> pure (Right (List [])) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp + let span = rangeToSrcSpan (fromNormalizedFilePath nfp) + $ fromMaybe (error "bummer") + $ fromCurrentRange pos range + let mod = tmrModule tmr + case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of + -- FIXME For some reason we get an HsVar instead of an + -- HsUnboundVar. We should check if this is a hole somehow?? + Just (L span' (HsVar _ (L _ var))) -> do + let params = TacticParams + { file = uri + , range + = fromMaybe (error "that is not great") + $ toCurrentRange pos =<< srcSpanToRange span' + , var_name = T.pack $ occNameString $ occName var + } + let names = Map.keys tacticCommands + actions <- for names $ \name -> do + cmd <- + mkLspCommand + plId + (coerce $ name <> "Command") + name + (Just [toJSON params]) + pure + $ CACodeAction + $ CodeAction + name + (Just CodeActionQuickFix) + Nothing + Nothing + $ Just cmd + pure $ Right $ List actions + _ -> pure $ Right $ codeActions [] +codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] + +codeActions :: [CodeAction] -> List CAResult +codeActions = List . fmap CACodeAction data TacticParams = TacticParams @@ -106,17 +120,45 @@ data TacticParams = TacticParams tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac _lf state (TacticParams uri range var_name) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp - let - span = rangeToSrcSpan (fromNormalizedFilePath nfp) $ fromMaybe (error "Oh shucks") $ fromCurrentRange pos range - mod = tmrModule tmr - hyps = hypothesisFromBindings span $ bindings mod - Just (L _ (HsVar _ (L _ v))) = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) - goal = varType v - case runTactic unsafeGlobalDynFlags goal hyps (tac $ mkVarOcc $ T.unpack var_name) of - Left err -> pure (Left (ResponseError InvalidRequest (T.pack $ show err) Nothing), Nothing) - Right res -> - let edit = J.List [ J.TextEdit (fromMaybe (error "Fiddlesticks" ) $ toCurrentRange pos range) (T.pack res) ] - response = J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing - in pure (Right Null, Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response)) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do + Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp + let + span + = rangeToSrcSpan (fromNormalizedFilePath nfp) + $ fromMaybe (error "Oh shucks") + $ fromCurrentRange pos range + mod = tmrModule tmr + hyps = hypothesisFromBindings span $ bindings mod + Just (L _ (HsVar _ (L _ v))) + = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) + goal = varType v + + pure $ + case runTactic + unsafeGlobalDynFlags + goal + hyps + $ tac + $ mkVarOcc + $ T.unpack var_name of + Left err -> + (, Nothing) + $ Left + $ ResponseError InvalidRequest (T.pack $ show err) Nothing + Right res -> + let edit + = J.List + $ pure + $ J.TextEdit + ( fromMaybe (error "Fiddlesticks") + $ toCurrentRange pos range + ) + $ T.pack res + + response = J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing + in ( Right Null + , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) + ) +tacticCmd _ _ _ _ = + pure (Left $ ResponseError InvalidRequest (T.pack "nah") Nothing, Nothing) + diff --git a/stack.yaml b/stack.yaml index a57e4c4ceb..8fd265622a 100644 --- a/stack.yaml +++ b/stack.yaml @@ -50,7 +50,7 @@ extra-deps: flags: haskell-language-server: - pedantic: true + pedantic: false retrie: BuildExecutable: false From 73854c7bf87596f8fc8ca1819e35ac8bac510857 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 17:05:21 -0700 Subject: [PATCH 30/63] context dependent destruct and homo --- src/Ide/Plugin/Tactic.hs | 165 ++++++++++++++++++++++++++++--------- src/Ide/TacticMachinery.hs | 31 +++++-- 2 files changed, 148 insertions(+), 48 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index b2e9c02315..b277dd1ad6 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -9,6 +9,7 @@ module Ide.Plugin.Tactic ( descriptor ) where +import Control.Monad import Data.Aeson import Data.Coerce import Data.Maybe @@ -49,15 +50,16 @@ descriptor plId = (defaultPluginDescriptor plId) PluginCommand (coerce $ name <> "Command") (tacticDesc name) - (tacticCmd tac)) $ - Map.toList tacticCommands + (tacticCmd tac)) + (Map.toList registeredCommands) , pluginCodeActionProvider = Just codeActionProvider } + tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" -tacticCommands :: Map.Map T.Text (OccName -> TacticsM ()) -tacticCommands = Map.fromList +registeredCommands :: Map.Map T.Text (OccName -> TacticsM ()) +registeredCommands = Map.fromList [ ("auto", const auto) , ("split", const split) , ("intro", const intro) @@ -65,29 +67,33 @@ tacticCommands = Map.fromList , ("homo", homo) ] +alwaysCommands :: [T.Text] +alwaysCommands = + [ "auto" + , "split" + , "intro" + ] + runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp - let span = rangeToSrcSpan (fromNormalizedFilePath nfp) - $ fromMaybe (error "bummer") - $ fromCurrentRange pos range - let mod = tmrModule tmr - case mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) of + (pos, mss, jdg) <- judgmentForHole state nfp range + case mss of -- FIXME For some reason we get an HsVar instead of an -- HsUnboundVar. We should check if this is a hole somehow?? - Just (L span' (HsVar _ (L _ var))) -> do + L span' (HsVar _ (L _ var)) -> do + let resulting_range + = fromMaybe (error "that is not great") + $ toCurrentRange pos =<< srcSpanToRange span' let params = TacticParams { file = uri - , range - = fromMaybe (error "that is not great") - $ toCurrentRange pos =<< srcSpanToRange span' + , range = resulting_range , var_name = T.pack $ occNameString $ occName var } - let names = Map.keys tacticCommands + let names = alwaysCommands actions <- for names $ \name -> do cmd <- mkLspCommand @@ -103,14 +109,85 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx Nothing Nothing $ Just cmd - pure $ Right $ List actions + split_actions <- mkSplits plId uri resulting_range jdg + homo_actions <- mkHomos plId uri resulting_range jdg + pure $ Right $ List $ mconcat + [ actions + , split_actions + , homo_actions + ] _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] + codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction +mkSplits :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkSplits plId uri range (Judgement hys _) = + fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> + case algebraicTyCon ty of + Nothing -> pure [] + Just _ -> do + let name = T.pack $ occNameString occ + let params = TacticParams + { file = uri + , range = range + , var_name = name + } + cmd <- + mkLspCommand + plId + ("destructCommand") + name + (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction + ("destruct " <> name) + (Just CodeActionQuickFix) + Nothing + Nothing + $ Just cmd + + +mkHomos :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkHomos plId uri range (Judgement hys (CType g)) = + case algebraicTyCon g of + Nothing -> pure [] + Just tycon -> + fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> + case algebraicTyCon ty of + Just tycon2 | tycon == tycon2 -> do + let name = T.pack $ occNameString occ + let params = TacticParams + { file = uri + , range = range + , var_name = name + } + cmd <- + mkLspCommand + plId + ("homoCommand") + name + (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction + ("homo " <> name) + (Just CodeActionQuickFix) + Nothing + Nothing + $ Just cmd + _ -> pure [] + + + + + data TacticParams = TacticParams { file :: J.Uri -- ^ Uri of the file to fill the hole in , range :: J.Range -- ^ The range of the hole @@ -118,26 +195,33 @@ data TacticParams = TacticParams } deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) + +judgmentForHole + :: IdeState + -> NormalizedFilePath + -> Range + -> IO (PositionMapping, LHsExpr GhcTc, Judgement) +judgmentForHole state nfp range = do + Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp + let span = rangeToSrcSpan (fromNormalizedFilePath nfp) + $ fromMaybe (error "Oh shucks") + $ fromCurrentRange pos range + mod = tmrModule tmr + Just (mss@(L span' (HsVar _ (L _ v)))) + = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) + goal = varType v + hyps = hypothesisFromBindings span' $ bindings mod + pure (pos, mss, Judgement hyps $ CType goal) + + tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac _lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp - let - span - = rangeToSrcSpan (fromNormalizedFilePath nfp) - $ fromMaybe (error "Oh shucks") - $ fromCurrentRange pos range - mod = tmrModule tmr - hyps = hypothesisFromBindings span $ bindings mod - Just (L _ (HsVar _ (L _ v))) - = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) - goal = varType v - + (pos, _, jdg) <- judgmentForHole state nfp range pure $ case runTactic unsafeGlobalDynFlags - goal - hyps + jdg $ tac $ mkVarOcc $ T.unpack var_name of @@ -146,16 +230,17 @@ tacticCmd tac _lf state (TacticParams uri range var_name) $ Left $ ResponseError InvalidRequest (T.pack $ show err) Nothing Right res -> - let edit - = J.List - $ pure - $ J.TextEdit - ( fromMaybe (error "Fiddlesticks") - $ toCurrentRange pos range - ) - $ T.pack res - - response = J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing + let edit = + J.List + $ pure + $ J.TextEdit + ( fromMaybe (error "Fiddlesticks") + $ toCurrentRange pos range + ) + $ T.pack res + + response = + J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing in ( Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) ) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 27c6087b1a..028947b88b 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -27,7 +27,7 @@ import Outputable (ppr, showSDoc, Outputable) import Refinery.Tactic import TcType import Type -import TysWiredIn (listTyCon, pairTyCon) +import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) ------------------------------------------------------------------------------ @@ -52,7 +52,11 @@ hypothesisFromBindings span (Bindings global local) = ------------------------------------------------------------------------------ -- | Convert a @Set Id@ into a hypothesis. buildHypothesis :: Set Id -> Map OccName CType -buildHypothesis s = M.fromList $ fmap (occName &&& CType . varType) $ S.toList s +buildHypothesis + = M.fromList + . fmap (occName &&& CType . varType) + . filter (isAlpha . head . occNameString . occName) + . S.toList ------------------------------------------------------------------------------ @@ -138,6 +142,20 @@ mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) mkTyName _ = "x" +------------------------------------------------------------------------------ +-- | Is this an algebraic type? +algebraicTyCon :: Type -> Maybe TyCon +algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) + | tycon == intTyCon = Nothing + | tycon == floatTyCon = Nothing + | tycon == doubleTyCon = Nothing + | tycon == charTyCon = Nothing + | tycon == funTyCon = Nothing + | otherwise = Just tycon +algebraicTyCon _ = Nothing + + + ------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String @@ -152,16 +170,13 @@ mkTyConName tc -- a given tactic. runTactic :: DynFlags - -> Type -- ^ Desired type - -> Map OccName CType -- ^ In-scope bindings + -> Judgement -> TacticsM () -- ^ Tactic to use -> Either TacticError String -runTactic dflags ty hy t +runTactic dflags jdg t = fmap (render dflags . parenthesize . fst) . runProvableT - . runTacticT t - . Judgement hy - $ CType ty + $ runTacticT t jdg ------------------------------------------------------------------------------ From 26df332703cafe265c56daff841613da26718355 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 17:35:29 -0700 Subject: [PATCH 31/63] Generalized interface --- src/Ide/Plugin/Tactic.hs | 195 ++++++++++++++++++++------------------- 1 file changed, 102 insertions(+), 93 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index b277dd1ad6..3af846a53d 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,10 +1,11 @@ --- | A plugin that uses tactics to synthesize code {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} +-- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic ( descriptor ) where @@ -46,33 +47,69 @@ import Type descriptor :: PluginId -> PluginDescriptor descriptor plId = (defaultPluginDescriptor plId) { pluginCommands - = fmap (\(name, tac) -> + = fmap (\tc -> PluginCommand - (coerce $ name <> "Command") - (tacticDesc name) - (tacticCmd tac)) - (Map.toList registeredCommands) + (tcCommandId tc) + (tacticDesc $ tcCommandName tc) + (tacticCmd $ commandTactic tc)) + [minBound .. maxBound] , pluginCodeActionProvider = Just codeActionProvider } tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" -registeredCommands :: Map.Map T.Text (OccName -> TacticsM ()) -registeredCommands = Map.fromList - [ ("auto", const auto) - , ("split", const split) - , ("intro", const intro) - , ("destruct", destruct) - , ("homo", homo) - ] - -alwaysCommands :: [T.Text] -alwaysCommands = - [ "auto" - , "split" - , "intro" - ] +data TacticCommand + = Auto + | Split + | Intro + | Destruct + | Homo + deriving (Eq, Ord, Show, Enum, Bounded) + +data TacticVariety + = PerHole + | PerBinding + deriving (Eq, Ord, Show, Enum, Bounded) + +tcCommandId :: TacticCommand -> CommandId +tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" + +tcCommandName :: TacticCommand -> T.Text +tcCommandName = T.pack . show + +tcCommandTitle :: TacticCommand -> OccName -> T.Text +tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ + +commandVariety :: TacticCommand -> TacticVariety +commandVariety Auto = PerHole +commandVariety Split = PerHole +commandVariety Intro = PerHole +commandVariety Destruct = PerBinding +commandVariety Homo = PerBinding + +commandTactic :: TacticCommand -> OccName -> TacticsM () +commandTactic Auto = const auto +commandTactic Split = const split +commandTactic Intro = const intro +commandTactic Destruct = destruct +commandTactic Homo = homo + +commandHoleFilter + :: TacticCommand + -> Type -- ^ goal type + -> Bool +commandHoleFilter _ _ = True + +commandBindingFilter + :: TacticCommand + -> Type -- ^ goal type + -> Type -- ^ binding type + -> Bool +commandBindingFilter Homo (algebraicTyCon -> Just t1) + (algebraicTyCon -> Just t2) = t1 == t2 +commandBindingFilter Destruct (algebraicTyCon -> Just _) _ = True +commandBindingFilter _ _ _ = False runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state @@ -84,38 +121,12 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx case mss of -- FIXME For some reason we get an HsVar instead of an -- HsUnboundVar. We should check if this is a hole somehow?? - L span' (HsVar _ (L _ var)) -> do + L span' (HsVar _ (L _ _)) -> do let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - let params = TacticParams - { file = uri - , range = resulting_range - , var_name = T.pack $ occNameString $ occName var - } - let names = alwaysCommands - actions <- for names $ \name -> do - cmd <- - mkLspCommand - plId - (coerce $ name <> "Command") - name - (Just [toJSON params]) - pure - $ CACodeAction - $ CodeAction - name - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd - split_actions <- mkSplits plId uri resulting_range jdg - homo_actions <- mkHomos plId uri resulting_range jdg - pure $ Right $ List $ mconcat - [ actions - , split_actions - , homo_actions - ] + actions <- mkTactics plId uri resulting_range jdg + pure $ Right $ List actions _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -123,13 +134,46 @@ codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction +mkTactics :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkTactics = flip foldMap [minBound .. maxBound] $ \tc -> + case commandVariety tc of + PerHole -> mkGoalTactic tc + PerBinding -> mkBindingTactic tc + -mkSplits :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkSplits plId uri range (Judgement hys _) = +mkGoalTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkGoalTactic tc plId uri range (Judgement _ (CType g)) = + case commandHoleFilter tc g of + False -> pure [] + True -> do + let params = TacticParams + { file = uri + , range = range + -- TODO(sandy): this should be Nothing + , var_name = "" + } + cmd <- + mkLspCommand + plId + (tcCommandId tc) + (tcCommandName tc) + (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction + (tcCommandName tc) + (Just CodeActionQuickFix) + Nothing + Nothing + $ Just cmd + +mkBindingTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkBindingTactic tc plId uri range (Judgement hys (CType g)) = fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> - case algebraicTyCon ty of - Nothing -> pure [] - Just _ -> do + case commandBindingFilter tc g ty of + False -> pure [] + True -> do let name = T.pack $ occNameString occ let params = TacticParams { file = uri @@ -139,55 +183,20 @@ mkSplits plId uri range (Judgement hys _) = cmd <- mkLspCommand plId - ("destructCommand") - name + (tcCommandId tc) + (tcCommandTitle tc occ) (Just [toJSON params]) pure $ pure $ CACodeAction $ CodeAction - ("destruct " <> name) + (tcCommandTitle tc occ) (Just CodeActionQuickFix) Nothing Nothing $ Just cmd -mkHomos :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkHomos plId uri range (Judgement hys (CType g)) = - case algebraicTyCon g of - Nothing -> pure [] - Just tycon -> - fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> - case algebraicTyCon ty of - Just tycon2 | tycon == tycon2 -> do - let name = T.pack $ occNameString occ - let params = TacticParams - { file = uri - , range = range - , var_name = name - } - cmd <- - mkLspCommand - plId - ("homoCommand") - name - (Just [toJSON params]) - pure - $ pure - $ CACodeAction - $ CodeAction - ("homo " <> name) - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd - _ -> pure [] - - - - - data TacticParams = TacticParams { file :: J.Uri -- ^ Uri of the file to fill the hole in , range :: J.Range -- ^ The range of the hole From 7475f3fb2ec7e58ac64ee73610c406730f66bd64 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 08:56:52 -0700 Subject: [PATCH 32/63] More composable --- src/Ide/Plugin/Tactic.hs | 125 +++++++++++++------------------------ src/Ide/TacticMachinery.hs | 7 ++- 2 files changed, 51 insertions(+), 81 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 3af846a53d..4bd8ac2054 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -81,12 +81,18 @@ tcCommandName = T.pack . show tcCommandTitle :: TacticCommand -> OccName -> T.Text tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ -commandVariety :: TacticCommand -> TacticVariety -commandVariety Auto = PerHole -commandVariety Split = PerHole -commandVariety Intro = PerHole -commandVariety Destruct = PerBinding -commandVariety Homo = PerBinding +commandProvider :: TacticCommand -> TacticProvider +commandProvider Auto = provide Auto "Auto" "" +commandProvider Split = provide Split "Split" "" +commandProvider Intro = + filterGoalType isFunction $ + provide Intro "Intro" "" +commandProvider Destruct = + filterBindingType destructFilter $ \occ _ -> + provide Destruct (tcCommandTitle Destruct occ) $ T.pack $ occNameString occ +commandProvider Homo = + filterBindingType homoFilter $ \occ _ -> + provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto @@ -95,21 +101,13 @@ commandTactic Intro = const intro commandTactic Destruct = destruct commandTactic Homo = homo -commandHoleFilter - :: TacticCommand - -> Type -- ^ goal type - -> Bool -commandHoleFilter _ _ = True - -commandBindingFilter - :: TacticCommand - -> Type -- ^ goal type - -> Type -- ^ binding type - -> Bool -commandBindingFilter Homo (algebraicTyCon -> Just t1) - (algebraicTyCon -> Just t2) = t1 == t2 -commandBindingFilter Destruct (algebraicTyCon -> Just _) _ = True -commandBindingFilter _ _ _ = False +homoFilter :: Type -> Type -> Bool +homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2 +homoFilter _ _ = False + +destructFilter :: Type -> Type -> Bool +destructFilter _ (algebraicTyCon -> Just _) = True +destructFilter _ _ = False runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state @@ -125,7 +123,7 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - actions <- mkTactics plId uri resulting_range jdg + actions <- (foldMap commandProvider [minBound .. maxBound]) plId uri resulting_range jdg pure $ Right $ List actions _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -134,67 +132,34 @@ codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction -mkTactics :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkTactics = flip foldMap [minBound .. maxBound] $ \tc -> - case commandVariety tc of - PerHole -> mkGoalTactic tc - PerBinding -> mkBindingTactic tc - -mkGoalTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkGoalTactic tc plId uri range (Judgement _ (CType g)) = - case commandHoleFilter tc g of - False -> pure [] - True -> do - let params = TacticParams - { file = uri - , range = range - -- TODO(sandy): this should be Nothing - , var_name = "" - } - cmd <- - mkLspCommand - plId - (tcCommandId tc) - (tcCommandName tc) - (Just [toJSON params]) - pure - $ pure - $ CACodeAction - $ CodeAction - (tcCommandName tc) - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd - -mkBindingTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkBindingTactic tc plId uri range (Judgement hys (CType g)) = +type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] + +provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider +provide tc title name plId uri range _ = do + let params = TacticParams { file = uri , range = range , var_name = name } + cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing + $ Just cmd + +filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider +filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) = + case p g of + True -> tp plId uri range jdg + False -> pure [] + +filterBindingType + :: (Type -> Type -> Bool) + -> (OccName -> Type -> TacticProvider) + -> TacticProvider +filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> - case commandBindingFilter tc g ty of + case p g ty of + True -> tp occ ty plId uri range jdg False -> pure [] - True -> do - let name = T.pack $ occNameString occ - let params = TacticParams - { file = uri - , range = range - , var_name = name - } - cmd <- - mkLspCommand - plId - (tcCommandId tc) - (tcCommandTitle tc occ) - (Just [toJSON params]) - pure - $ pure - $ CACodeAction - $ CodeAction - (tcCommandTitle tc occ) - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd data TacticParams = TacticParams diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 028947b88b..975a1b41c2 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -142,6 +142,12 @@ mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) mkTyName _ = "x" +------------------------------------------------------------------------------ +-- | Is this a function type? +isFunction :: Type -> Bool +isFunction (tcSplitFunTys -> ((_:_), _)) = True +isFunction _ = False + ------------------------------------------------------------------------------ -- | Is this an algebraic type? algebraicTyCon :: Type -> Maybe TyCon @@ -155,7 +161,6 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) algebraicTyCon _ = Nothing - ------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String From 42d16be9c97682cdd36d6bc0d83f543288de79a7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 09:01:15 -0700 Subject: [PATCH 33/63] Remove TacticVariety --- src/Ide/Plugin/Tactic.hs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 4bd8ac2054..13c6fdde79 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -67,11 +67,6 @@ data TacticCommand | Homo deriving (Eq, Ord, Show, Enum, Bounded) -data TacticVariety - = PerHole - | PerBinding - deriving (Eq, Ord, Show, Enum, Bounded) - tcCommandId :: TacticCommand -> CommandId tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" From 83ef2143075c0351a0c341fb57681102bade5930 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 09:11:27 -0700 Subject: [PATCH 34/63] Haddock --- src/Ide/Plugin/Tactic.hs | 47 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 44 insertions(+), 3 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 13c6fdde79..81ad50162c 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -59,6 +59,10 @@ descriptor plId = (defaultPluginDescriptor plId) tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" +------------------------------------------------------------------------------ +-- | The list of tactics exposed to the outside world. These are attached to +-- actual tactics via 'commandTactic' and are contextually provided to the +-- editor via 'commandProvider'. data TacticCommand = Auto | Split @@ -67,15 +71,32 @@ data TacticCommand | Homo deriving (Eq, Ord, Show, Enum, Bounded) + +------------------------------------------------------------------------------ +-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS +-- UI. +type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] + + +------------------------------------------------------------------------------ +-- | Construct a 'CommandId' tcCommandId :: TacticCommand -> CommandId tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" + +------------------------------------------------------------------------------ +-- | The name of the command for the LS. tcCommandName :: TacticCommand -> T.Text tcCommandName = T.pack . show +------------------------------------------------------------------------------ +-- | Construct a title for a command. tcCommandTitle :: TacticCommand -> OccName -> T.Text tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ +------------------------------------------------------------------------------ +-- | Mapping from tactic commands to their contextual providers. See 'provide', +-- 'filterGoalType' and 'filterBindingType' for the nitty gritty. commandProvider :: TacticCommand -> TacticProvider commandProvider Auto = provide Auto "Auto" "" commandProvider Split = provide Split "Split" "" @@ -89,6 +110,8 @@ commandProvider Homo = filterBindingType homoFilter $ \occ _ -> provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ +------------------------------------------------------------------------------ +-- | A mapping from tactic commands to actual tactics for refinery. commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto commandTactic Split = const split @@ -96,10 +119,16 @@ commandTactic Intro = const intro commandTactic Destruct = destruct commandTactic Homo = homo +------------------------------------------------------------------------------ +-- | We should show homos only when the goal type is the same as the binding +-- type, and that both are usual algebraic types. homoFilter :: Type -> Type -> Bool homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2 homoFilter _ _ = False +------------------------------------------------------------------------------ +-- | We should show destruct for bindings only when those bindings have usual +-- algebraic types. destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _ = False @@ -128,8 +157,9 @@ codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction -type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] - +------------------------------------------------------------------------------ +-- | Terminal constructor for providing context-sensitive tactics. Tactics +-- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider provide tc title name plId uri range _ = do let params = TacticParams { file = uri , range = range , var_name = name } @@ -140,14 +170,22 @@ provide tc title name plId uri range _ = do $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing $ Just cmd + +------------------------------------------------------------------------------ +-- | 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@(Judgement _ (CType g)) = case p g of True -> tp plId uri range jdg False -> pure [] + +------------------------------------------------------------------------------ +-- | Multiply a 'TacticProvider' for each binding, making sure it appears only +-- when the given predicate holds over the goal and binding types. filterBindingType - :: (Type -> Type -> Bool) + :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = @@ -165,6 +203,9 @@ data TacticParams = TacticParams deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) +------------------------------------------------------------------------------ +-- | Find the last typechecked module, and find the most specific span, as well +-- as the judgement at the given range. judgmentForHole :: IdeState -> NormalizedFilePath From 405fec271a9218c637b15214a0bde10158c1a271 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 09:12:54 -0700 Subject: [PATCH 35/63] Describe spooky monoidal behavior --- src/Ide/Plugin/Tactic.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 81ad50162c..8e89bf3259 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -147,7 +147,13 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - actions <- (foldMap commandProvider [minBound .. maxBound]) plId uri resulting_range jdg + actions <- + -- This foldMap is over the function monoid. + foldMap commandProvider [minBound .. maxBound] + plId + uri + resulting_range + jdg pure $ Right $ List actions _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] From 964354ef9e2703a64ace64417747e5157040fa79 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 10:01:11 -0700 Subject: [PATCH 36/63] Only look at actual holes --- src/Ide/LocalBindings.hs | 28 +++++++++++++++------------- src/Ide/Plugin/Tactic.hs | 9 ++++----- 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 120351e410..a532f4228b 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -5,10 +5,9 @@ module Ide.LocalBindings ( Bindings (..) , bindings , mostSpecificSpan - , isItAHole + , holify ) where -import Data.Ord import Bag import Control.Lens import Data.Data.Lens @@ -18,16 +17,16 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import Data.Monoid +import Data.Ord import Data.Set (Set) import qualified Data.Set as S -import GHC (TypecheckedModule (..), GhcTc) +import GHC (TypecheckedModule (..), GhcTc, NoExt (..)) import HsBinds import HsExpr import Id +import OccName import SrcLoc - data Bindings = Bindings { bGlobalBinds :: Set Id , bLocalBinds :: Map SrcSpan (Set Id) @@ -160,12 +159,15 @@ mostSpecificSpan span z _ -> []) $ z -isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar -isItAHole tcm span = getFirst $ - everything (<>) ( - mkQ mempty $ \case - L span' (HsUnboundVar _ z :: HsExpr GhcTc) - | span == span' -> pure z - _ -> mempty - ) $ tm_typechecked_source tcm +------------------------------------------------------------------------------ +-- | Convert an HsVar back into an HsUnboundVar if it isn't actually in scope. +holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc +holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) = + case M.lookup span local of + Nothing -> v + Just binds -> + case S.member var binds of + True -> v + False -> L span $ HsUnboundVar NoExt $ TrueExprHole $ occName var +holify _ v = v diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 8e89bf3259..c3e75a538e 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -141,9 +141,7 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do (pos, mss, jdg) <- judgmentForHole state nfp range case mss of - -- FIXME For some reason we get an HsVar instead of an - -- HsUnboundVar. We should check if this is a hole somehow?? - L span' (HsVar _ (L _ _)) -> do + L span' (HsUnboundVar _ _) -> do let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' @@ -226,8 +224,9 @@ judgmentForHole state nfp range = do Just (mss@(L span' (HsVar _ (L _ v)))) = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) goal = varType v - hyps = hypothesisFromBindings span' $ bindings mod - pure (pos, mss, Judgement hyps $ CType goal) + binds = bindings mod + hyps = hypothesisFromBindings span' binds + pure (pos, holify binds mss, Judgement hyps $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams From e1617bb273bdf46bbf255cec193c1df1e931d505 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 10:14:09 -0700 Subject: [PATCH 37/63] Auto if possible --- src/Ide/Plugin/Tactic.hs | 4 ++-- src/Ide/TacticMachinery.hs | 2 ++ src/Ide/Tactics.hs | 9 +++++++++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index c3e75a538e..47547e8ac9 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -116,8 +116,8 @@ commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto commandTactic Split = const split commandTactic Intro = const intro -commandTactic Destruct = destruct -commandTactic Homo = homo +commandTactic Destruct = autoIfPossible . destruct +commandTactic Homo = autoIfPossible . homo ------------------------------------------------------------------------------ -- | We should show homos only when the goal type is the same as the binding diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 975a1b41c2..f819343418 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -74,11 +74,13 @@ data TacticError = UndefinedHypothesis OccName | GoalMismatch String CType | UnsolvedSubgoals [Judgement] + | NoProgress instance Show TacticError where show (UndefinedHypothesis name) = "undefined is not a function" show (GoalMismatch str typ) = "oh no" show (UnsolvedSubgoals jdgs) = "so sad" + show NoProgress = "No Progress" type ProvableM = ProvableT Judgement (Either TacticError) diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index e2820cb4e2..a9c09b8bc1 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -81,6 +81,10 @@ homo = destruct' $ \dc (Judgement hy (CType g)) -> buildDataCon hy dc (snd $ splitAppTys g) +solve :: TacticsM () -> TacticsM () +solve t = t >> throwError NoProgress + + apply :: TacticsM () apply = rule $ \(Judgement hy g) -> do case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of @@ -116,6 +120,11 @@ auto = (intro >> auto) (apply >> auto) pure () + +autoIfPossible :: TacticsM () -> TacticsM () +autoIfPossible t = t >> (solve auto pure ()) + + one :: TacticsM () one = intro assumption split apply pure () From 44528b0ee6e3d2154f8ef62c789da3534c28f0fc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 12:58:37 -0700 Subject: [PATCH 38/63] debugging --- src/Ide/LocalBindings.hs | 1 + src/Ide/Plugin/Tactic.hs | 3 +++ src/Ide/TacticMachinery.hs | 2 +- src/Ide/Tactics.hs | 2 +- 4 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index a532f4228b..94fee414e2 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -161,6 +161,7 @@ mostSpecificSpan span z ------------------------------------------------------------------------------ -- | Convert an HsVar back into an HsUnboundVar if it isn't actually in scope. +-- TODO(sandy): this will throw away the type >:( holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) = case M.lookup span local of diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 47547e8ac9..01b083e105 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -37,11 +37,13 @@ import Ide.LocalBindings import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types +import Data.List (intercalate) import OccName import HsExpr import GHC import DynFlags import Type +import System.IO descriptor :: PluginId -> PluginDescriptor @@ -233,6 +235,7 @@ tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac _lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do (pos, _, jdg) <- judgmentForHole state nfp range + hPutStrLn stderr $ intercalate "; " $ fmap (\(occ, CType ty) -> occNameString occ <> " :: " <> render unsafeGlobalDynFlags ty) $ Map.toList $ jHypothesis jdg pure $ case runTactic unsafeGlobalDynFlags diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index f819343418..d04d86c5e3 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -224,6 +224,6 @@ buildDataCon hy dc apps = do (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs -render :: Outputable (LHsExpr pass) => DynFlags -> LHsExpr pass -> String +render :: Outputable a => DynFlags -> a -> String render dflags = showSDoc dflags . ppr diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index a9c09b8bc1..abc78351f6 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -122,7 +122,7 @@ auto = (intro >> auto) autoIfPossible :: TacticsM () -> TacticsM () -autoIfPossible t = t >> (solve auto pure ()) +autoIfPossible t = (t >> solve auto) t one :: TacticsM () From 9115e1095d4fb97f1511582061fba1b26836d4e2 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 15:08:30 -0700 Subject: [PATCH 39/63] Maybe grafting works now --- haskell-language-server.cabal | 131 ++++++++++++++++++---------------- src/Ide/TreeTransform.hs | 78 ++++++++++++++++++++ stack.yaml | 37 ++++------ 3 files changed, 160 insertions(+), 86 deletions(-) create mode 100644 src/Ide/TreeTransform.hs diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 509e4d4221..a9478b02d9 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -97,6 +97,11 @@ library , time , transformers , unordered-containers + , refinery + , syb + , mtl + , ghc-source-gen + , ghc-exactprint include-dirs: include if os(windows) @@ -238,67 +243,67 @@ common hls-test-utils ghc-options: -Werror default-language: Haskell2010 -test-suite func-test - import: agpl, hls-test-utils - type: exitcode-stdio-1.0 - default-language: Haskell2010 - build-tool-depends: haskell-language-server:haskell-language-server - , ghcide:ghcide-test-preprocessor - build-depends: base >=4.7 && <5 - , aeson - , bytestring - , data-default - , directory - , filepath - , haskell-language-server - , haskell-lsp - , haskell-lsp-types - , lens - , lsp-test >= 0.11.0.4 - , tasty - , tasty-ant-xml >= 1.1.6 - , tasty-expected-failure - , tasty-golden - , tasty-hunit - , tasty-rerun - , text - , unordered-containers - hs-source-dirs: test/functional - main-is: Main.hs - other-modules: Command - , Completion - , Deferred - , Definition - , Diagnostic - , Eval - , Format - , FunctionalBadProject - , FunctionalCodeAction - , FunctionalLiquid - , HieBios - , Highlight - , Progress - , Reference - , Rename - , Symbol - , TypeDefinition - ghc-options: -Wall - -Wno-name-shadowing - -threaded -rtsopts -with-rtsopts=-N - if flag(pedantic) - ghc-options: -Werror -Wredundant-constraints +-- test-suite func-test +-- import: agpl, hls-test-utils +-- type: exitcode-stdio-1.0 +-- default-language: Haskell2010 +-- build-tool-depends: haskell-language-server:haskell-language-server +-- , ghcide:ghcide-test-preprocessor +-- build-depends: base >=4.7 && <5 +-- , aeson +-- , bytestring +-- , data-default +-- , directory +-- , filepath +-- , haskell-language-server +-- , haskell-lsp +-- , haskell-lsp-types +-- , lens +-- , lsp-test >= 0.11.0.4 +-- , tasty +-- , tasty-ant-xml >= 1.1.6 +-- , tasty-expected-failure +-- , tasty-golden +-- , tasty-hunit +-- , tasty-rerun +-- , text +-- , unordered-containers +-- hs-source-dirs: test/functional +-- main-is: Main.hs +-- other-modules: Command +-- , Completion +-- , Deferred +-- , Definition +-- , Diagnostic +-- , Eval +-- , Format +-- , FunctionalBadProject +-- , FunctionalCodeAction +-- , FunctionalLiquid +-- , HieBios +-- , Highlight +-- , Progress +-- , Reference +-- , Rename +-- , Symbol +-- , TypeDefinition +-- ghc-options: -Wall +-- -Wno-name-shadowing +-- -threaded -rtsopts -with-rtsopts=-N +-- if flag(pedantic) +-- ghc-options: -Werror -Wredundant-constraints -test-suite wrapper-test - import: agpl, hls-test-utils - type: exitcode-stdio-1.0 - build-tool-depends: haskell-language-server:haskell-language-server-wrapper - default-language: Haskell2010 - build-depends: base == 4.* - , directory - , process - , tasty - , tasty-hunit - , tasty-ant-xml >= 1.1.6 - hs-source-dirs: test/wrapper - main-is: Main.hs - ghc-options: -Wall +-- test-suite wrapper-test +-- import: agpl, hls-test-utils +-- type: exitcode-stdio-1.0 +-- build-tool-depends: haskell-language-server:haskell-language-server-wrapper +-- default-language: Haskell2010 +-- build-depends: base == 4.* +-- , directory +-- , process +-- , tasty +-- , tasty-hunit +-- , tasty-ant-xml >= 1.1.6 +-- hs-source-dirs: test/wrapper +-- main-is: Main.hs +-- ghc-options: -Wall diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs new file mode 100644 index 0000000000..0a295145d0 --- /dev/null +++ b/src/Ide/TreeTransform.hs @@ -0,0 +1,78 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ide.TreeTransform + ( Graft, graft, transform, useAnnotatedSource + ) where + +import Control.Monad +import Data.Functor.Identity +import Development.IDE.Core.RuleTypes +import Development.IDE.Core.Rules +import Development.IDE.Core.Shake +import Development.IDE.Types.Location +import GHC +import Generics.SYB +import Ide.PluginUtils +import Language.Haskell.GHC.ExactPrint +import Language.Haskell.LSP.Types +import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) +import Retrie.ExactPrint +import Text.Regex.TDFA.Text() +import qualified Data.Text as T + + +useAnnotatedSource :: String -> IdeState -> NormalizedFilePath -> IO (Annotated ParsedSource) +useAnnotatedSource herald state nfp = do + Just pm <- runAction herald state $ use GetParsedModule nfp + pure $ fixAnns pm + + +newtype Graft a = Graft + { runGraft :: a -> Transform a + } + +instance Semigroup (Graft a) where + Graft a <> Graft b = Graft $ a >=> b + +instance Monoid (Graft a) where + mempty = Graft pure + + +transform + :: ClientCapabilities + -> Uri + -> Graft ParsedSource + -> Annotated ParsedSource + -> WorkspaceEdit +transform ccs uri f a = + let src = printA a + a' = runIdentity $ transformA a $ runGraft f + res = printA a' + in diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions + + +graft + :: forall a b + . (Data a, Annotate b) + => SrcSpan + -> Located b + -> Graft a +graft dst (L _ val) = Graft $ \a -> do + span <- uniqueSrcSpanT + let val' = L span val + modifyAnnsT $ addAnnotationsForPretty [] val' + pure $ everywhere ( mkT $ \case + L src (_ :: b) | src == dst -> val' + l -> l) a + + +fixAnns :: ParsedModule -> Annotated ParsedSource +fixAnns ParsedModule {..} = + let ranns = relativiseApiAnns pm_parsed_source pm_annotations + in unsafeMkA pm_parsed_source ranns 0 + + + diff --git a/stack.yaml b/stack.yaml index 605591b432..8fd265622a 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-14.27 # Last 8.6.5 +resolver: lts-15.0 # Last 8.8.2 packages: - . @@ -9,57 +9,48 @@ ghc-options: extra-deps: - aeson-1.5.2.0 -- ansi-terminal-0.10.3 -- base-compat-0.10.5 +- apply-refact-0.7.0.0 - github: bubba/brittany commit: c59655f10d5ad295c2481537fc8abf0a297d9d1c -- butcher-1.3.3.1 -- Cabal-3.0.2.0 -- cabal-plan-0.6.2.0 +- butcher-1.3.3.2 +- bytestring-trie-0.2.5.0 - clock-0.7.2 +- constrained-dynamic-0.1.0.0 - extra-1.7.3 - floskell-0.10.4 - fourmolu-0.1.0.0@rev:1 -- fuzzy-0.1.0.0 # - ghcide-0.1.0 - ghc-check-0.5.0.1 -- ghc-exactprint-0.6.2 - ghc-lib-parser-8.10.1.20200523 - ghc-lib-parser-ex-8.10.0.4 -- haddock-api-2.22.0@rev:1 - haddock-library-1.8.0 - haskell-lsp-0.22.0.0 - haskell-lsp-types-0.22.0.0 +- haskell-src-exts-1.21.1 - hie-bios-0.6.1 +- hlint-2.2.8 +- hoogle-5.0.17.11 +- hsimport-0.11.0 - HsYAML-0.2.1.0@rev:1 - HsYAML-aeson-0.2.0.0@rev:2 -- indexed-profunctors-0.1 -- lens-4.18 +- ilist-0.3.1.0 - lsp-test-0.11.0.4 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 -- optics-core-0.2 -- optparse-applicative-0.15.1.0 - ormolu-0.1.2.0 -- parser-combinators-1.2.1 -- primitive-0.7.1.0 -- regex-base-0.94.0.0 -- regex-pcre-builtin-0.95.1.1.8.43 -- regex-tdfa-1.3.1.0 - retrie-0.1.1.1 -- semialign-1.1 +- semigroups-0.18.5 # - github: wz1000/shake # commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef - stylish-haskell-0.11.0.3 -- tasty-rerun-1.1.17 - temporary-1.2.1.1 - these-1.1.1.1 -- type-equality-1 -- topograph-1 +- primitive-0.7.1.0@sha256:6a237bb338bcc43193077ff8e8c0f0ce2de14c652231496a15672e8b563a07e2,2604 +- refinery-0.1.0.0 flags: haskell-language-server: - pedantic: true + pedantic: false retrie: BuildExecutable: false From 9d28b43aa67ef37a0ac6f4bfb47b5619c134c3df Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 15:44:27 -0700 Subject: [PATCH 40/63] Transformation works; tree doesnt --- ghcide | 2 +- haskell-language-server.cabal | 72 +++++++++++++++++------------------ src/Ide/Plugin/Tactic.hs | 52 ++++++++++++------------- src/Ide/TacticMachinery.hs | 16 ++++++-- src/Ide/TreeTransform.hs | 15 +++++--- 5 files changed, 85 insertions(+), 72 deletions(-) diff --git a/ghcide b/ghcide index 26517c6af0..078e3d3c0d 160000 --- a/ghcide +++ b/ghcide @@ -1 +1 @@ -Subproject commit 26517c6af0bc83181de248406e8e570351748331 +Subproject commit 078e3d3c0d319f83841ccbcdc60ff5f0e243f6be diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index f59684a942..b8ecd111ed 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -178,42 +178,42 @@ executable haskell-language-server , unordered-containers default-language: Haskell2010 -executable haskell-language-server-wrapper - import: agpl - main-is: Wrapper.hs - hs-source-dirs: - exe - other-modules: - Arguments - Paths_haskell_language_server - autogen-modules: - Paths_haskell_language_server - ghc-options: - -threaded - -Wall - -Wno-name-shadowing - -Wredundant-constraints - -- allow user RTS overrides - -rtsopts - -- disable idle GC - -- disable parallel GC - -- increase nursery size - "-with-rtsopts=-I0 -qg -A128M" - if flag(pedantic) - ghc-options: -Werror - build-depends: - base - , directory - , extra - , filepath - , gitrev - , ghc - , ghc-paths - , hie-bios - , haskell-language-server - , optparse-applicative - , process - default-language: Haskell2010 +-- executable haskell-language-server-wrapper +-- import: agpl +-- main-is: Wrapper.hs +-- hs-source-dirs: +-- exe +-- other-modules: +-- Arguments +-- Paths_haskell_language_server +-- autogen-modules: +-- Paths_haskell_language_server +-- ghc-options: +-- -threaded +-- -Wall +-- -Wno-name-shadowing +-- -Wredundant-constraints +-- -- allow user RTS overrides +-- -rtsopts +-- -- disable idle GC +-- -- disable parallel GC +-- -- increase nursery size +-- "-with-rtsopts=-I0 -qg -A128M" +-- if flag(pedantic) +-- ghc-options: -Werror +-- build-depends: +-- base +-- , directory +-- , extra +-- , filepath +-- , gitrev +-- , ghc +-- , ghc-paths +-- , hie-bios +-- , haskell-language-server +-- , optparse-applicative +-- , process +-- default-language: Haskell2010 -- This common stanza simulates a previous private lib -- We removed it due to issues with stack when loading the project using a stack based hie.yaml diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 01b083e105..c11a61d160 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -10,6 +10,7 @@ module Ide.Plugin.Tactic ( descriptor ) where +import GHC.Generics import Control.Monad import Data.Aeson import Data.Coerce @@ -34,6 +35,7 @@ import Ide.Tactics import Ide.Plugin import Ide.LocalBindings +import qualified Language.Haskell.LSP.Core as LSP import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types @@ -44,6 +46,7 @@ import GHC import DynFlags import Type import System.IO +import Ide.TreeTransform descriptor :: PluginId -> PluginDescriptor @@ -232,36 +235,31 @@ judgmentForHole state nfp range = do tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams -tacticCmd tac _lf state (TacticParams uri range var_name) +tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do (pos, _, jdg) <- judgmentForHole state nfp range + pm <- useAnnotatedSource "tacticsCmd" state nfp hPutStrLn stderr $ intercalate "; " $ fmap (\(occ, CType ty) -> occNameString occ <> " :: " <> render unsafeGlobalDynFlags ty) $ Map.toList $ jHypothesis jdg - pure $ - case runTactic - unsafeGlobalDynFlags - jdg - $ tac - $ mkVarOcc - $ T.unpack var_name of - Left err -> - (, Nothing) - $ Left - $ ResponseError InvalidRequest (T.pack $ show err) Nothing - Right res -> - let edit = - J.List - $ pure - $ J.TextEdit - ( fromMaybe (error "Fiddlesticks") - $ toCurrentRange pos range - ) - $ T.pack res - - response = - J.WorkspaceEdit (Just $ H.singleton uri edit) Nothing - in ( Right Null - , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) - ) + case runTactic + unsafeGlobalDynFlags + jdg + $ tac + $ mkVarOcc + $ T.unpack var_name of + Left err -> + pure $ (, Nothing) + $ Left + $ ResponseError InvalidRequest (T.pack $ show err) Nothing + Right res -> do + let range' = + fromMaybe (error "Fiddlesticks") $ toCurrentRange pos range + span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' + g = graft span res + hPutStrLn stderr $ show span + let response = transform (LSP.clientCapabilities lf) uri g pm + pure $ ( Right Null + , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) + ) tacticCmd _ _ _ _ = pure (Left $ ResponseError InvalidRequest (T.pack "nah") Nothing, Nothing) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index d04d86c5e3..b092f4f4df 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -18,6 +18,8 @@ import Data.Maybe import Data.Set (Set) import qualified Data.Set as S import DataCon +import Development.IDE.Types.Location +import qualified FastString as FS import GHC import GHC.Generics import GHC.SourceGen.Overloaded @@ -179,9 +181,9 @@ runTactic :: DynFlags -> Judgement -> TacticsM () -- ^ Tactic to use - -> Either TacticError String + -> Either TacticError (LHsExpr GhcPs) runTactic dflags jdg t - = fmap (render dflags . parenthesize . fst) + = fmap (parenthesize . fst) . runProvableT $ runTacticT t jdg @@ -199,7 +201,7 @@ parenthesize a = noLoc $ HsPar NoExt a instance MonadExtract (LHsExpr GhcPs) ProvableM where - hole = pure $ noLoc $ HsUnboundVar NoExt $ TrueExprHole $ mkVarOcc "_" + hole = pure $ noLoc $ HsVar NoExt $ noLoc $ Unqual $ mkVarOcc "_" ------------------------------------------------------------------------------ @@ -227,3 +229,11 @@ buildDataCon hy dc apps = do render :: Outputable a => DynFlags -> a -> String render dflags = showSDoc dflags . ppr +-- TODO(sandy): this doesn't belong here +-- | Convert a DAML compiler Range to a GHC SrcSpan +rangeToSrcSpan :: String -> Range -> SrcSpan +rangeToSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = + mkSrcSpan + (mkSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) + (mkSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) + diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs index 0a295145d0..ca0e44336a 100644 --- a/src/Ide/TreeTransform.hs +++ b/src/Ide/TreeTransform.hs @@ -22,6 +22,9 @@ import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) import Retrie.ExactPrint import Text.Regex.TDFA.Text() import qualified Data.Text as T +import Debug.Trace +import Ide.TacticMachinery +import DynFlags useAnnotatedSource :: String -> IdeState -> NormalizedFilePath -> IO (Annotated ParsedSource) @@ -48,9 +51,9 @@ transform -> Annotated ParsedSource -> WorkspaceEdit transform ccs uri f a = - let src = printA a + let src = traceShowId $ printA a a' = runIdentity $ transformA a $ runGraft f - res = printA a' + res = trace (render unsafeGlobalDynFlags $ astA a') $ printA a' in diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions @@ -64,9 +67,11 @@ graft dst (L _ val) = Graft $ \a -> do span <- uniqueSrcSpanT let val' = L span val modifyAnnsT $ addAnnotationsForPretty [] val' - pure $ everywhere ( mkT $ \case - L src (_ :: b) | src == dst -> val' - l -> l) a + pure $ everywhere + ( mkT $ \case + L src (_ :: b) | src == dst -> val' + l -> l + ) a fixAnns :: ParsedModule -> Annotated ParsedSource From 87f23eef004ec545a0a529963920059b14a4442c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 17:01:54 -0700 Subject: [PATCH 41/63] Remove debugging --- src/Ide/Plugin/Tactic.hs | 10 +++------- src/Ide/TacticMachinery.hs | 2 +- src/Ide/TreeTransform.hs | 9 +++------ 3 files changed, 7 insertions(+), 14 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index c11a61d160..71a843c243 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -10,15 +10,13 @@ module Ide.Plugin.Tactic ( descriptor ) where -import GHC.Generics -import Control.Monad +import Control.Monad import Data.Aeson import Data.Coerce -import Data.Maybe -import Data.Traversable import qualified Data.Map as Map -import qualified Data.HashMap.Strict as H +import Data.Maybe import qualified Data.Text as T +import Data.Traversable import qualified GHC.Generics as Generics import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), @@ -239,7 +237,6 @@ tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do (pos, _, jdg) <- judgmentForHole state nfp range pm <- useAnnotatedSource "tacticsCmd" state nfp - hPutStrLn stderr $ intercalate "; " $ fmap (\(occ, CType ty) -> occNameString occ <> " :: " <> render unsafeGlobalDynFlags ty) $ Map.toList $ jHypothesis jdg case runTactic unsafeGlobalDynFlags jdg @@ -255,7 +252,6 @@ tacticCmd tac lf state (TacticParams uri range var_name) fromMaybe (error "Fiddlesticks") $ toCurrentRange pos range span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' g = graft span res - hPutStrLn stderr $ show span let response = transform (LSP.clientCapabilities lf) uri g pm pure $ ( Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index b092f4f4df..4ca0c4ca3f 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -183,7 +183,7 @@ runTactic -> TacticsM () -- ^ Tactic to use -> Either TacticError (LHsExpr GhcPs) runTactic dflags jdg t - = fmap (parenthesize . fst) + = fmap (fst) . runProvableT $ runTacticT t jdg diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs index ca0e44336a..2eb6e4736a 100644 --- a/src/Ide/TreeTransform.hs +++ b/src/Ide/TreeTransform.hs @@ -22,9 +22,6 @@ import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) import Retrie.ExactPrint import Text.Regex.TDFA.Text() import qualified Data.Text as T -import Debug.Trace -import Ide.TacticMachinery -import DynFlags useAnnotatedSource :: String -> IdeState -> NormalizedFilePath -> IO (Annotated ParsedSource) @@ -51,9 +48,9 @@ transform -> Annotated ParsedSource -> WorkspaceEdit transform ccs uri f a = - let src = traceShowId $ printA a + let src = printA a a' = runIdentity $ transformA a $ runGraft f - res = trace (render unsafeGlobalDynFlags $ astA a') $ printA a' + res = printA a' in diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions @@ -66,7 +63,7 @@ graft graft dst (L _ val) = Graft $ \a -> do span <- uniqueSrcSpanT let val' = L span val - modifyAnnsT $ addAnnotationsForPretty [] val' + modifyAnnsT $ mappend $ addAnnotationsForPretty [] val' mempty pure $ everywhere ( mkT $ \case L src (_ :: b) | src == dst -> val' From 64a30b3656be302caa9a6d1f9783b02a9cc93a88 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 12:37:58 -0700 Subject: [PATCH 42/63] Proper indentation and parenthesizing --- src/Ide/Plugin/Tactic.hs | 2 +- src/Ide/TacticMachinery.hs | 11 ----- src/Ide/TreeTransform.hs | 98 ++++++++++++++++++++++++++------------ 3 files changed, 68 insertions(+), 43 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 71a843c243..31ac58b852 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -252,7 +252,7 @@ tacticCmd tac lf state (TacticParams uri range var_name) fromMaybe (error "Fiddlesticks") $ toCurrentRange pos range span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' g = graft span res - let response = transform (LSP.clientCapabilities lf) uri g pm + let response = transform unsafeGlobalDynFlags (LSP.clientCapabilities lf) uri g pm pure $ ( Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) ) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 4ca0c4ca3f..96d70c420e 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -188,17 +188,6 @@ runTactic dflags jdg t $ runTacticT t jdg ------------------------------------------------------------------------------- --- | Put parentheses around an expression if required. -parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs -parenthesize a@(L _ HsVar{}) = a -parenthesize a@(L _ HsUnboundVar{}) = a -parenthesize a@(L _ HsOverLabel{}) = a -parenthesize a@(L _ HsOverLit{}) = a -parenthesize a@(L _ HsIPVar{}) = a -parenthesize a@(L _ HsLit{}) = a -parenthesize a = noLoc $ HsPar NoExt a - instance MonadExtract (LHsExpr GhcPs) ProvableM where hole = pure $ noLoc $ HsVar NoExt $ noLoc $ Unqual $ mkVarOcc "_" diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs index 2eb6e4736a..f927b5b5cd 100644 --- a/src/Ide/TreeTransform.hs +++ b/src/Ide/TreeTransform.hs @@ -1,5 +1,6 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -7,21 +8,25 @@ module Ide.TreeTransform ( Graft, graft, transform, useAnnotatedSource ) where -import Control.Monad -import Data.Functor.Identity -import Development.IDE.Core.RuleTypes -import Development.IDE.Core.Rules -import Development.IDE.Core.Shake -import Development.IDE.Types.Location -import GHC -import Generics.SYB -import Ide.PluginUtils -import Language.Haskell.GHC.ExactPrint -import Language.Haskell.LSP.Types -import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) -import Retrie.ExactPrint -import Text.Regex.TDFA.Text() +import Control.Monad +import Data.Bool +import Data.Functor.Identity import qualified Data.Text as T +import Debug.Trace +import Development.IDE.Core.RuleTypes +import Development.IDE.Core.Rules +import Development.IDE.Core.Shake +import Development.IDE.Types.Location +import GHC hiding (parseExpr) +import Generics.SYB +import Ide.PluginUtils +import Language.Haskell.GHC.ExactPrint +import Language.Haskell.GHC.ExactPrint.Parsers +import Language.Haskell.LSP.Types +import Language.Haskell.LSP.Types.Capabilities (ClientCapabilities) +import Outputable +import Retrie.ExactPrint hiding (parseExpr) +import Text.Regex.TDFA.Text() useAnnotatedSource :: String -> IdeState -> NormalizedFilePath -> IO (Annotated ParsedSource) @@ -31,43 +36,53 @@ useAnnotatedSource herald state nfp = do newtype Graft a = Graft - { runGraft :: a -> Transform a + { runGraft :: DynFlags -> a -> Transform a } instance Semigroup (Graft a) where - Graft a <> Graft b = Graft $ a >=> b + Graft a <> Graft b = Graft $ \dflags -> a dflags >=> b dflags instance Monoid (Graft a) where - mempty = Graft pure + mempty = Graft $ const pure transform - :: ClientCapabilities + :: DynFlags + -> ClientCapabilities -> Uri -> Graft ParsedSource -> Annotated ParsedSource -> WorkspaceEdit -transform ccs uri f a = +transform dflags ccs uri f a = let src = printA a - a' = runIdentity $ transformA a $ runGraft f + a' = runIdentity $ transformA a $ runGraft f dflags res = printA a' in diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions graft - :: forall a b - . (Data a, Annotate b) + :: forall a + . (Data a) => SrcSpan - -> Located b + -> Located (HsExpr GhcPs) -> Graft a -graft dst (L _ val) = Graft $ \a -> do - span <- uniqueSrcSpanT - let val' = L span val - modifyAnnsT $ mappend $ addAnnotationsForPretty [] val' mempty - pure $ everywhere - ( mkT $ \case - L src (_ :: b) | src == dst -> val' - l -> l +graft dst val = Graft $ \dflags a -> do + let inside_app = + everything (||) + (mkQ False $ \case + (L _ (HsApp _ (L src _) _) :: LHsExpr GhcPs) + | src == dst -> True + (L _ (HsApp _ _ (L src _)) :: LHsExpr GhcPs) + | src == dst -> True + _ -> False + ) a + (anns, val') <- annotate dflags $ bool val (parenthesize val) inside_app + modifyAnnsT $ mappend anns + pure $ everywhere' + ( mkT $ + \case + (L src _ :: LHsExpr GhcPs) | src == dst -> val' + l -> l ) a @@ -77,4 +92,25 @@ fixAnns ParsedModule {..} = in unsafeMkA pm_parsed_source ranns 0 +annotate :: DynFlags -> LHsExpr GhcPs -> Transform (Anns, LHsExpr GhcPs) +annotate dflags expr = do + uniq <- show <$> uniqueSrcSpanT + let rendered = traceId $ render dflags expr + Right (anns, expr') = parseExpr dflags uniq rendered + anns' = setPrecedingLines expr' 0 1 anns + pure (anns', expr') + +render :: Outputable a => DynFlags -> a -> String +render dflags = showSDoc dflags . ppr + +------------------------------------------------------------------------------ +-- | Put parentheses around an expression if required. +parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs +parenthesize a@(L _ HsVar{}) = a +parenthesize a@(L _ HsUnboundVar{}) = a +parenthesize a@(L _ HsOverLabel{}) = a +parenthesize a@(L _ HsOverLit{}) = a +parenthesize a@(L _ HsIPVar{}) = a +parenthesize a@(L _ HsLit{}) = a +parenthesize a = noLoc $ HsPar NoExt a From 2f49670adbb081d2177cdc1a2bf1e6d46f69cd7d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 12:49:14 -0700 Subject: [PATCH 43/63] Less fancy parenthesizing --- src/Ide/TreeTransform.hs | 20 +++----------------- 1 file changed, 3 insertions(+), 17 deletions(-) diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs index f927b5b5cd..926120a393 100644 --- a/src/Ide/TreeTransform.hs +++ b/src/Ide/TreeTransform.hs @@ -8,6 +8,7 @@ module Ide.TreeTransform ( Graft, graft, transform, useAnnotatedSource ) where +import BasicTypes (appPrec) import Control.Monad import Data.Bool import Data.Functor.Identity @@ -67,16 +68,7 @@ graft -> Located (HsExpr GhcPs) -> Graft a graft dst val = Graft $ \dflags a -> do - let inside_app = - everything (||) - (mkQ False $ \case - (L _ (HsApp _ (L src _) _) :: LHsExpr GhcPs) - | src == dst -> True - (L _ (HsApp _ _ (L src _)) :: LHsExpr GhcPs) - | src == dst -> True - _ -> False - ) a - (anns, val') <- annotate dflags $ bool val (parenthesize val) inside_app + (anns, val') <- annotate dflags $ parenthesize val modifyAnnsT $ mappend anns pure $ everywhere' ( mkT $ @@ -106,11 +98,5 @@ render dflags = showSDoc dflags . ppr ------------------------------------------------------------------------------ -- | Put parentheses around an expression if required. parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs -parenthesize a@(L _ HsVar{}) = a -parenthesize a@(L _ HsUnboundVar{}) = a -parenthesize a@(L _ HsOverLabel{}) = a -parenthesize a@(L _ HsOverLit{}) = a -parenthesize a@(L _ HsIPVar{}) = a -parenthesize a@(L _ HsLit{}) = a -parenthesize a = noLoc $ HsPar NoExt a +parenthesize = parenthesizeHsExpr appPrec From 56e1bed04651aaa0022117a3e0b267c87af9768c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 13:18:46 -0700 Subject: [PATCH 44/63] Don't crash if we can't lookup things --- src/Ide/Plugin/Tactic.hs | 151 ++++++++++++++++++++------------------- 1 file changed, 77 insertions(+), 74 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 31ac58b852..0670db4f11 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} @@ -11,40 +12,33 @@ module Ide.Plugin.Tactic ) where import Control.Monad +import Control.Monad.Trans +import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce -import qualified Data.Map as Map +import qualified Data.Map as M import Data.Maybe -import qualified Data.Text as T +import qualified Data.Text as T import Data.Traversable -import qualified GHC.Generics as Generics - -import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), - TypeCheck (TypeCheck)) -import Development.IDE.Core.Shake (useWithStale, IdeState (..)) import Development.IDE.Core.PositionMapping +import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (TypeCheck)) import Development.IDE.Core.Service (runAction) +import Development.IDE.Core.Shake (useWithStale, IdeState (..)) +import Development.IDE.GHC.Error (srcSpanToRange) import Development.Shake (Action) -import Development.IDE.GHC.Error - -import Ide.Types +import DynFlags (unsafeGlobalDynFlags) +import GHC +import GHC.Generics (Generic) +import Ide.LocalBindings (bindings, mostSpecificSpan, holify) +import Ide.Plugin (mkLspCommand) import Ide.TacticMachinery import Ide.Tactics -import Ide.Plugin -import Ide.LocalBindings - -import qualified Language.Haskell.LSP.Core as LSP -import qualified Language.Haskell.LSP.Types as J +import Ide.TreeTransform (transform, graft, useAnnotatedSource) +import Ide.Types +import Language.Haskell.LSP.Core (clientCapabilities) import Language.Haskell.LSP.Types - -import Data.List (intercalate) -import OccName -import HsExpr -import GHC -import DynFlags +import OccName import Type -import System.IO -import Ide.TreeTransform descriptor :: PluginId -> PluginDescriptor @@ -141,25 +135,26 @@ runIde state = runAction "tactic" state codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - (pos, mss, jdg) <- judgmentForHole state nfp range - case mss of - L span' (HsUnboundVar _ _) -> do - let resulting_range - = fromMaybe (error "that is not great") - $ toCurrentRange pos =<< srcSpanToRange span' - actions <- - -- This foldMap is over the function monoid. - foldMap commandProvider [minBound .. maxBound] - plId - uri - resulting_range - jdg - pure $ Right $ List actions - _ -> pure $ Right $ codeActions [] + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = + fromMaybeT (Right $ List []) $ do + (pos, mss, jdg) <- MaybeT $ judgmentForHole state nfp range + case mss of + L span' (HsUnboundVar _ _) -> do + resulting_range <- + liftMaybe $ toCurrentRange pos =<< srcSpanToRange span' + actions <- lift $ + -- This foldMap is over the function monoid. + foldMap commandProvider [minBound .. maxBound] + plId + uri + resulting_range + jdg + pure $ Right $ List actions + _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] + codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction @@ -196,18 +191,18 @@ filterBindingType -> (OccName -> Type -> TacticProvider) -> TacticProvider filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = - fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> + fmap join $ for (M.toList hys) $ \(occ, CType ty) -> case p g ty of True -> tp occ ty plId uri range jdg False -> pure [] data TacticParams = TacticParams - { file :: J.Uri -- ^ Uri of the file to fill the hole in - , range :: J.Range -- ^ The range of the hole + { file :: Uri -- ^ Uri of the file to fill the hole in + , range :: Range -- ^ The range of the hole , var_name :: T.Text } - deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) + deriving (Show, Eq, Generic, ToJSON, FromJSON) ------------------------------------------------------------------------------ @@ -217,16 +212,17 @@ judgmentForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (PositionMapping, LHsExpr GhcTc, Judgement) -judgmentForHole state nfp range = do - Just (tmr, pos) <- runIde state $ useWithStale TypeCheck nfp - let span = rangeToSrcSpan (fromNormalizedFilePath nfp) - $ fromMaybe (error "Oh shucks") - $ fromCurrentRange pos range + -> IO (Maybe (PositionMapping, LHsExpr GhcTc, Judgement)) +judgmentForHole state nfp range = runMaybeT $ do + (tmr, pos) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp + range' <- liftMaybe $ fromCurrentRange pos range + let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' mod = tmrModule tmr - Just (mss@(L span' (HsVar _ (L _ v)))) - = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) - goal = varType v + + (mss@(L span' (HsVar _ (L _ v)))) + <- liftMaybe $ mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) + + let goal = varType v binds = bindings mod hyps = hypothesisFromBindings span' binds pure (pos, holify binds mss, Judgement hyps $ CType goal) @@ -234,28 +230,35 @@ judgmentForHole state nfp range = do tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) - | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do - (pos, _, jdg) <- judgmentForHole state nfp range - pm <- useAnnotatedSource "tacticsCmd" state nfp - case runTactic - unsafeGlobalDynFlags - jdg - $ tac - $ mkVarOcc - $ T.unpack var_name of - Left err -> - pure $ (, Nothing) - $ Left - $ ResponseError InvalidRequest (T.pack $ show err) Nothing - Right res -> do - let range' = - fromMaybe (error "Fiddlesticks") $ toCurrentRange pos range - span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' - g = graft span res - let response = transform unsafeGlobalDynFlags (LSP.clientCapabilities lf) uri g pm - pure $ ( Right Null - , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) - ) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = + fromMaybeT (Right Null, Nothing) $ do + (pos, _, jdg) <- MaybeT $ judgmentForHole state nfp range + let dflags = unsafeGlobalDynFlags + pm <- lift $ useAnnotatedSource "tacticsCmd" state nfp + case runTactic dflags jdg + $ tac + $ mkVarOcc + $ T.unpack var_name of + Left err -> + pure $ (, Nothing) + $ Left + $ ResponseError InvalidRequest (T.pack $ show err) Nothing + Right res -> do + range' <- liftMaybe $ toCurrentRange pos range + let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' + g = graft span res + let response = transform dflags (clientCapabilities lf) uri g pm + pure + ( Right Null + , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) + ) tacticCmd _ _ _ _ = pure (Left $ ResponseError InvalidRequest (T.pack "nah") Nothing, Nothing) + +fromMaybeT :: Functor m => a -> MaybeT m a -> m a +fromMaybeT def = fmap (fromMaybe def) . runMaybeT + +liftMaybe :: Monad m => Maybe a -> MaybeT m a +liftMaybe a = MaybeT $ pure a + From 9e10c922abdba214aaa587a82e74c18bcf096f94 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 13:23:23 -0700 Subject: [PATCH 45/63] Holes must start with an underscore --- src/Ide/LocalBindings.hs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 94fee414e2..8dc5adc996 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -164,11 +164,14 @@ mostSpecificSpan span z -- TODO(sandy): this will throw away the type >:( holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) = - case M.lookup span local of - Nothing -> v - Just binds -> - case S.member var binds of - True -> v - False -> L span $ HsUnboundVar NoExt $ TrueExprHole $ occName var + let occ = occName var + in case M.lookup span local of + Nothing -> v + Just binds -> + -- Make sure the binding is not in scope and that it begins with an + -- underscore + case not (S.member var binds) && take 1 (occNameString occ) == "_" of + True -> L span $ HsUnboundVar NoExt $ TrueExprHole occ + False -> v holify _ v = v From 8aa89838bb6bbd1788518063360635a9895abc3b Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 13:45:34 -0700 Subject: [PATCH 46/63] Haddock pass --- src/Ide/LocalBindings.hs | 34 ++++++++++++++++++++++------ src/Ide/Plugin/Tactic.hs | 2 +- src/Ide/TacticMachinery.hs | 46 +++++++++++++++++++++++++------------- src/Ide/Tactics.hs | 32 +++++++++++++++++++++++++- src/Ide/TreeTransform.hs | 30 +++++++++++++++++++++---- 5 files changed, 115 insertions(+), 29 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 8dc5adc996..1d08ff5c03 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -27,6 +27,8 @@ import Id import OccName import SrcLoc +------------------------------------------------------------------------------ +-- | The available bindings at every point in a Haskell tree. data Bindings = Bindings { bGlobalBinds :: Set Id , bLocalBinds :: Map SrcSpan (Set Id) @@ -39,10 +41,20 @@ instance Monoid Bindings where mempty = Bindings mempty mempty +------------------------------------------------------------------------------ +-- | Determine what bindings are in scope at every point in a program. +-- +-- **WARNING:** This doesn't find bindings inside of TH splices or arrow syntax +-- --- and possibly other obscure pieces of the AST. bindings :: TypecheckedModule -> Bindings bindings = uncurry Bindings . bindsBindings mempty . tm_typechecked_source +------------------------------------------------------------------------------ +-- | Helper function for implementing 'binding'. +-- +-- **WARNING:** This doesn't yet work over TH splices or arrow syntax --- and +-- possibly other obscure pieces of the AST. dataBindings :: Data a => S.Set Id -> a -> M.Map SrcSpan (S.Set Id) dataBindings in_scope = foldMapOf biplate $ cool collect where @@ -110,6 +122,8 @@ dataBindings in_scope = foldMapOf biplate $ cool collect collect _ = mempty +------------------------------------------------------------------------------ +-- | Map the binds from a match group into over their containing spans. matchGroupBindings :: S.Set Id -> MatchGroup GhcTc (LHsExpr GhcTc) -> M.Map SrcSpan (S.Set Id) matchGroupBindings _ (XMatchGroup _) = M.empty matchGroupBindings in_scope (MG _ (L _ alts) _) = M.fromList $ do @@ -118,6 +132,8 @@ matchGroupBindings in_scope (MG _ (L _ alts) _) = M.fromList $ do M.toList $ dataBindings (S.union bound in_scope) body +------------------------------------------------------------------------------ +-- | Map the binds from a local binds into over their containing spans. localBindsBindings :: S.Set Id -> HsLocalBindsLR GhcTc GhcTc -> (S.Set Id, M.Map SrcSpan (S.Set Id)) localBindsBindings in_scope (HsValBinds _ (ValBinds _ binds _sigs)) = bindsBindings in_scope binds localBindsBindings in_scope (HsValBinds _ (XValBindsLR (NValBinds groups _sigs))) = @@ -125,6 +141,8 @@ localBindsBindings in_scope (HsValBinds _ (XValBindsLR (NValBinds groups _sigs)) localBindsBindings _ _ = (mempty, mempty) +------------------------------------------------------------------------------ +-- | Map the binds from a hsbindlr into over their containing spans. bindsBindings :: S.Set Id -> Bag (LHsBindLR GhcTc GhcTc) -> (S.Set Id, M.Map SrcSpan (S.Set Id)) bindsBindings in_scope binds = flip foldMap (fmap unLoc $ bagToList binds) $ \case @@ -139,21 +157,23 @@ bindsBindings in_scope binds = XHsBindsLR _ -> mempty -size :: SrcSpan -> (Int, Int) -size (UnhelpfulSpan _) = maxBound -size (RealSrcSpan span) = +------------------------------------------------------------------------------ +-- | How many lines and columns does a SrcSpan span? +srcSpanSize :: SrcSpan -> (Int, Int) +srcSpanSize (UnhelpfulSpan _) = maxBound +srcSpanSize (RealSrcSpan span) = ( srcSpanEndLine span - srcSpanStartLine span , srcSpanEndCol span - srcSpanStartCol span ) -smallest :: SrcSpan -> SrcSpan -> Ordering -smallest = comparing size - +------------------------------------------------------------------------------ +-- | Given a SrcSpan, find the smallest LHsExpr that entirely contains that +-- span. Useful for determining what node in the tree your cursor is hovering over. mostSpecificSpan :: (Data a, Typeable pass) => SrcSpan -> a -> Maybe (LHsExpr pass) mostSpecificSpan span z = listToMaybe - $ sortBy (smallest `on` getLoc) + $ sortBy (comparing srcSpanSize `on` getLoc) $ everything (<>) (mkQ mempty $ \case l@(L span' _) | span `isSubspanOf` span' -> [l] _ -> []) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 0670db4f11..5e4839a138 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -235,7 +235,7 @@ tacticCmd tac lf state (TacticParams uri range var_name) (pos, _, jdg) <- MaybeT $ judgmentForHole state nfp range let dflags = unsafeGlobalDynFlags pm <- lift $ useAnnotatedSource "tacticsCmd" state nfp - case runTactic dflags jdg + case runTactic jdg $ tac $ mkVarOcc $ T.unpack var_name of diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 96d70c420e..601fd51566 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -19,19 +19,26 @@ import Data.Set (Set) import qualified Data.Set as S import DataCon import Development.IDE.Types.Location +import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC import GHC.Generics import GHC.SourceGen.Overloaded import Ide.LocalBindings import Name -import Outputable (ppr, showSDoc, Outputable) +import Outputable hiding ((<>)) import Refinery.Tactic import TcType import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) +------------------------------------------------------------------------------ +-- | Orphan instance for producing holes when attempting to solve tactics. +instance MonadExtract (LHsExpr GhcPs) ProvableM where + hole = pure $ noLoc $ HsVar NoExt $ noLoc $ Unqual $ mkVarOcc "_" + + ------------------------------------------------------------------------------ -- | A wrapper around 'Type' which supports equality and ordering. newtype CType = CType { unCType :: Type } @@ -79,10 +86,19 @@ data TacticError | NoProgress instance Show TacticError where - show (UndefinedHypothesis name) = "undefined is not a function" - show (GoalMismatch str typ) = "oh no" - show (UnsolvedSubgoals jdgs) = "so sad" - show NoProgress = "No Progress" + show (UndefinedHypothesis name) = + occNameString name <> " is not available in the hypothesis." + show (GoalMismatch tac (CType typ)) = + mconcat + [ "The tactic " + , tac + , " doesn't apply to goal type " + , unsafeRender typ + ] + show (UnsolvedSubgoals _) = + "There were unsolved subgoals" + show NoProgress = + "Unable to make progress" type ProvableM = ProvableT Judgement (Either TacticError) @@ -178,21 +194,15 @@ mkTyConName tc -- | Attempt to generate a term of the right type using in-scope bindings, and -- a given tactic. runTactic - :: DynFlags - -> Judgement + :: Judgement -> TacticsM () -- ^ Tactic to use -> Either TacticError (LHsExpr GhcPs) -runTactic dflags jdg t +runTactic jdg t = fmap (fst) . runProvableT $ runTacticT t jdg - -instance MonadExtract (LHsExpr GhcPs) ProvableM where - hole = pure $ noLoc $ HsVar NoExt $ noLoc $ Unqual $ mkVarOcc "_" - - ------------------------------------------------------------------------------ -- | Which names are in scope? getInScope :: Map OccName a -> [OccName] @@ -215,14 +225,18 @@ buildDataCon hy dc apps = do (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs -render :: Outputable a => DynFlags -> a -> String -render dflags = showSDoc dflags . ppr --- TODO(sandy): this doesn't belong here +------------------------------------------------------------------------------ -- | Convert a DAML compiler Range to a GHC SrcSpan +-- TODO(sandy): this doesn't belong here rangeToSrcSpan :: String -> Range -> SrcSpan rangeToSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = mkSrcSpan (mkSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) (mkSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) +------------------------------------------------------------------------------ +-- | Print something +unsafeRender :: Outputable a => a -> String +unsafeRender = showSDoc unsafeGlobalDynFlags . ppr + diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index abc78351f6..86c6f27678 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -28,6 +28,8 @@ import TyCoRep import Type +------------------------------------------------------------------------------ +-- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () assumption = rule $ \(Judgement hy g) -> case find ((== g) . snd) $ toList hy of @@ -35,6 +37,8 @@ assumption = rule $ \(Judgement hy g) -> Nothing -> throwError $ GoalMismatch "assumption" g +------------------------------------------------------------------------------ +-- | Introduce a lambda. intro :: TacticsM () intro = rule $ \(Judgement hy g) -> case unCType g of @@ -45,6 +49,9 @@ intro = rule $ \(Judgement hy g) -> _ -> throwError $ GoalMismatch "intro" g +------------------------------------------------------------------------------ +-- | Combinator for performign case splitting, and running sub-rules on the +-- resulting matches. destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> TacticsM () destruct' f term = rule $ \(Judgement hy g) -> do case find ((== term) . fst) $ toList hy of @@ -73,18 +80,28 @@ destruct' f term = rule $ \(Judgement hy g) -> do pure $ match [pat] $ unLoc sg +------------------------------------------------------------------------------ +-- | Case split, and leave holes in the matches. destruct :: OccName -> TacticsM () destruct = destruct' $ const subgoal + +------------------------------------------------------------------------------ +-- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () homo = destruct' $ \dc (Judgement hy (CType g)) -> - buildDataCon hy dc (snd $ splitAppTys g) + buildDatctiaCon hy dc (snd $ splitAppTys g) +------------------------------------------------------------------------------ +-- | Ensure a tactic produces no subgoals. Useful when working with +-- backtracking. solve :: TacticsM () -> TacticsM () solve t = t >> throwError NoProgress +------------------------------------------------------------------------------ +-- | Apply a function from the hypothesis. apply :: TacticsM () apply = rule $ \(Judgement hy g) -> do case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of @@ -97,6 +114,9 @@ apply = rule $ \(Judgement hy g) -> do Nothing -> throwError $ GoalMismatch "apply" g +------------------------------------------------------------------------------ +-- | Introduce a data constructor, splitting a goal into the datacon's +-- constituent sub-goals. split :: TacticsM () split = rule $ \(Judgement hy g) -> case splitTyConApp_maybe $ unCType g of @@ -107,12 +127,17 @@ split = rule $ \(Judgement hy g) -> Nothing -> throwError $ GoalMismatch "split" g +------------------------------------------------------------------------------ +-- | Run 'one' many times. deepen :: Int -> TacticsM () deepen 0 = pure () deepen depth = do one deepen $ depth - 1 + +------------------------------------------------------------------------------ +-- | Automatically solve a goal. auto :: TacticsM () auto = (intro >> auto) (assumption >> auto) @@ -121,10 +146,15 @@ auto = (intro >> auto) pure () +------------------------------------------------------------------------------ +-- | Run a tactic, and subsequently apply auto if it completes. If not, just +-- run the first tactic, leaving its subgoals as holes. autoIfPossible :: TacticsM () -> TacticsM () autoIfPossible t = (t >> solve auto) t +------------------------------------------------------------------------------ +-- | Do one obvious thing. one :: TacticsM () one = intro assumption split apply pure () diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs index 926120a393..0aa2d4cec6 100644 --- a/src/Ide/TreeTransform.hs +++ b/src/Ide/TreeTransform.hs @@ -10,7 +10,6 @@ module Ide.TreeTransform import BasicTypes (appPrec) import Control.Monad -import Data.Bool import Data.Functor.Identity import qualified Data.Text as T import Debug.Trace @@ -30,12 +29,21 @@ import Retrie.ExactPrint hiding (parseExpr) import Text.Regex.TDFA.Text() -useAnnotatedSource :: String -> IdeState -> NormalizedFilePath -> IO (Annotated ParsedSource) +------------------------------------------------------------------------------ +-- | Get the latest version of the annotated parse source. +useAnnotatedSource + :: String + -> IdeState + -> NormalizedFilePath + -> IO (Annotated ParsedSource) useAnnotatedSource herald state nfp = do Just pm <- runAction herald state $ use GetParsedModule nfp pure $ fixAnns pm +------------------------------------------------------------------------------ +-- | A transformation for grafting source trees together. Use the semigroup +-- instance to combine 'Graft's, and run them via 'transform'. newtype Graft a = Graft { runGraft :: DynFlags -> a -> Transform a } @@ -47,6 +55,8 @@ instance Monoid (Graft a) where mempty = Graft $ const pure +------------------------------------------------------------------------------ +-- | Convert a 'Graft' into a 'WorkspaceEdit'. transform :: DynFlags -> ClientCapabilities @@ -61,11 +71,15 @@ transform dflags ccs uri f a = in diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions +------------------------------------------------------------------------------ +-- | Construct a 'Graft', replacing the node at the given 'SrcSpan' with the +-- given 'LHSExpr'. The node at that position must already be a 'LHsExpr', or +-- this is a no-op. graft :: forall a - . (Data a) + . Data a => SrcSpan - -> Located (HsExpr GhcPs) + -> LHsExpr GhcPs -> Graft a graft dst val = Graft $ \dflags a -> do (anns, val') <- annotate dflags $ parenthesize val @@ -78,12 +92,16 @@ graft dst val = Graft $ \dflags a -> do ) a +------------------------------------------------------------------------------ +-- | Dark magic I stole from retrie. No idea what it does. fixAnns :: ParsedModule -> Annotated ParsedSource fixAnns ParsedModule {..} = let ranns = relativiseApiAnns pm_parsed_source pm_annotations in unsafeMkA pm_parsed_source ranns 0 +------------------------------------------------------------------------------ +-- | Given an 'LHSExpr', compute its exactprint annotations. annotate :: DynFlags -> LHsExpr GhcPs -> Transform (Anns, LHsExpr GhcPs) annotate dflags expr = do uniq <- show <$> uniqueSrcSpanT @@ -92,9 +110,13 @@ annotate dflags expr = do anns' = setPrecedingLines expr' 0 1 anns pure (anns', expr') + +------------------------------------------------------------------------------ +-- | Print out something 'Outputable'. render :: Outputable a => DynFlags -> a -> String render dflags = showSDoc dflags . ppr + ------------------------------------------------------------------------------ -- | Put parentheses around an expression if required. parenthesize :: LHsExpr GhcPs -> LHsExpr GhcPs From d698b8885d4a270aa3f1d768f59acffc6594d603 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 13:50:58 -0700 Subject: [PATCH 47/63] Module restructuring --- haskell-language-server.cabal | 4 ++-- src/Ide/Plugin/Tactic.hs | 4 ++-- .../{TacticMachinery.hs => Plugin/Tactic/Machinery.hs} | 2 +- src/Ide/{ => Plugin/Tactic}/Tactics.hs | 8 ++++---- 4 files changed, 9 insertions(+), 9 deletions(-) rename src/Ide/{TacticMachinery.hs => Plugin/Tactic/Machinery.hs} (99%) rename src/Ide/{ => Plugin/Tactic}/Tactics.hs (97%) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index b8ecd111ed..e0fb739211 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -53,12 +53,12 @@ library Ide.Plugin.Pragmas Ide.Plugin.Retrie Ide.Plugin.Tactic + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Tactics Ide.Plugin.Floskell Ide.Plugin.Formatter Ide.Plugin.StylishHaskell Ide.PluginUtils - Ide.TacticMachinery - Ide.Tactics Ide.Types Ide.Version Ide.TreeTransform diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 5e4839a138..cffeb086bc 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -31,8 +31,8 @@ import GHC import GHC.Generics (Generic) import Ide.LocalBindings (bindings, mostSpecificSpan, holify) import Ide.Plugin (mkLspCommand) -import Ide.TacticMachinery -import Ide.Tactics +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Tactics import Ide.TreeTransform (transform, graft, useAnnotatedSource) import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/Plugin/Tactic/Machinery.hs similarity index 99% rename from src/Ide/TacticMachinery.hs rename to src/Ide/Plugin/Tactic/Machinery.hs index 601fd51566..ffc9273e7a 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/Plugin/Tactic/Machinery.hs @@ -6,7 +6,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} -module Ide.TacticMachinery where +module Ide.Plugin.Tactic.Machinery where import Control.Arrow import Data.Char diff --git a/src/Ide/Tactics.hs b/src/Ide/Plugin/Tactic/Tactics.hs similarity index 97% rename from src/Ide/Tactics.hs rename to src/Ide/Plugin/Tactic/Tactics.hs index 86c6f27678..1baf28e089 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Plugin/Tactic/Tactics.hs @@ -4,8 +4,8 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} -module Ide.Tactics - ( module Ide.Tactics +module Ide.Plugin.Tactic.Tactics + ( module Ide.Plugin.Tactic.Tactics , runTactic ) where @@ -21,7 +21,7 @@ import GHC.SourceGen.Binds import GHC.SourceGen.Expr import GHC.SourceGen.Overloaded import GHC.SourceGen.Pat -import Ide.TacticMachinery +import Ide.Plugin.Tactic.Machinery import Name import Refinery.Tactic import TyCoRep @@ -90,7 +90,7 @@ destruct = destruct' $ const subgoal -- | Case split, using the same data constructor in the matches. homo :: OccName -> TacticsM () homo = destruct' $ \dc (Judgement hy (CType g)) -> - buildDatctiaCon hy dc (snd $ splitAppTys g) + buildDataCon hy dc (snd $ splitAppTys g) ------------------------------------------------------------------------------ From a5ee18ae543d69568a392a59840786ad08eca72c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 14:01:03 -0700 Subject: [PATCH 48/63] Fix the cabal file --- haskell-language-server.cabal | 210 +++++++++++++++++----------------- 1 file changed, 105 insertions(+), 105 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index e0fb739211..b9e43c1e93 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -59,9 +59,9 @@ library Ide.Plugin.Formatter Ide.Plugin.StylishHaskell Ide.PluginUtils + Ide.TreeTransform Ide.Types Ide.Version - Ide.TreeTransform other-modules: Paths_haskell_language_server hs-source-dirs: @@ -82,6 +82,8 @@ library , fourmolu ^>= 0.1 , ghc , ghc-boot-th + , ghc-exactprint + , ghc-source-gen , ghcide >= 0.1 , gitrev , hashable @@ -89,24 +91,22 @@ library , hie-bios >= 0.6.1 && < 0.8 , hslogger , lens + , mtl , ormolu ^>= 0.1.2 , optparse-simple , process , regex-tdfa >= 1.3.1.0 + , refinery , retrie >= 0.1.1.0 , safe-exceptions , shake >= 0.17.5 , stylish-haskell == 0.11.* + , syb , temporary , text , time , transformers , unordered-containers - , refinery - , syb - , mtl - , ghc-source-gen - , ghc-exactprint include-dirs: include if os(windows) @@ -178,42 +178,42 @@ executable haskell-language-server , unordered-containers default-language: Haskell2010 --- executable haskell-language-server-wrapper --- import: agpl --- main-is: Wrapper.hs --- hs-source-dirs: --- exe --- other-modules: --- Arguments --- Paths_haskell_language_server --- autogen-modules: --- Paths_haskell_language_server --- ghc-options: --- -threaded --- -Wall --- -Wno-name-shadowing --- -Wredundant-constraints --- -- allow user RTS overrides --- -rtsopts --- -- disable idle GC --- -- disable parallel GC --- -- increase nursery size --- "-with-rtsopts=-I0 -qg -A128M" --- if flag(pedantic) --- ghc-options: -Werror --- build-depends: --- base --- , directory --- , extra --- , filepath --- , gitrev --- , ghc --- , ghc-paths --- , hie-bios --- , haskell-language-server --- , optparse-applicative --- , process --- default-language: Haskell2010 +executable haskell-language-server-wrapper + import: agpl + main-is: Wrapper.hs + hs-source-dirs: + exe + other-modules: + Arguments + Paths_haskell_language_server + autogen-modules: + Paths_haskell_language_server + ghc-options: + -threaded + -Wall + -Wno-name-shadowing + -Wredundant-constraints + -- allow user RTS overrides + -rtsopts + -- disable idle GC + -- disable parallel GC + -- increase nursery size + "-with-rtsopts=-I0 -qg -A128M" + if flag(pedantic) + ghc-options: -Werror + build-depends: + base + , directory + , extra + , filepath + , gitrev + , ghc + , ghc-paths + , hie-bios + , haskell-language-server + , optparse-applicative + , process + default-language: Haskell2010 -- This common stanza simulates a previous private lib -- We removed it due to issues with stack when loading the project using a stack based hie.yaml @@ -248,67 +248,67 @@ common hls-test-utils ghc-options: -Werror default-language: Haskell2010 --- test-suite func-test --- import: agpl, hls-test-utils --- type: exitcode-stdio-1.0 --- default-language: Haskell2010 --- build-tool-depends: haskell-language-server:haskell-language-server --- , ghcide:ghcide-test-preprocessor --- build-depends: base >=4.7 && <5 --- , aeson --- , bytestring --- , data-default --- , directory --- , filepath --- , haskell-language-server --- , haskell-lsp --- , haskell-lsp-types --- , lens --- , lsp-test >= 0.11.0.4 --- , tasty --- , tasty-ant-xml >= 1.1.6 --- , tasty-expected-failure --- , tasty-golden --- , tasty-hunit --- , tasty-rerun --- , text --- , unordered-containers --- hs-source-dirs: test/functional --- main-is: Main.hs --- other-modules: Command --- , Completion --- , Deferred --- , Definition --- , Diagnostic --- , Eval --- , Format --- , FunctionalBadProject --- , FunctionalCodeAction --- , FunctionalLiquid --- , HieBios --- , Highlight --- , Progress --- , Reference --- , Rename --- , Symbol --- , TypeDefinition --- ghc-options: -Wall --- -Wno-name-shadowing --- -threaded -rtsopts -with-rtsopts=-N --- if flag(pedantic) --- ghc-options: -Werror -Wredundant-constraints +test-suite func-test + import: agpl, hls-test-utils + type: exitcode-stdio-1.0 + default-language: Haskell2010 + build-tool-depends: haskell-language-server:haskell-language-server + , ghcide:ghcide-test-preprocessor + build-depends: base >=4.7 && <5 + , aeson + , bytestring + , data-default + , directory + , filepath + , haskell-language-server + , haskell-lsp + , haskell-lsp-types + , lens + , lsp-test >= 0.11.0.4 + , tasty + , tasty-ant-xml >= 1.1.6 + , tasty-expected-failure + , tasty-golden + , tasty-hunit + , tasty-rerun + , text + , unordered-containers + hs-source-dirs: test/functional + main-is: Main.hs + other-modules: Command + , Completion + , Deferred + , Definition + , Diagnostic + , Eval + , Format + , FunctionalBadProject + , FunctionalCodeAction + , FunctionalLiquid + , HieBios + , Highlight + , Progress + , Reference + , Rename + , Symbol + , TypeDefinition + ghc-options: -Wall + -Wno-name-shadowing + -threaded -rtsopts -with-rtsopts=-N + if flag(pedantic) + ghc-options: -Werror -Wredundant-constraints --- test-suite wrapper-test --- import: agpl, hls-test-utils --- type: exitcode-stdio-1.0 --- build-tool-depends: haskell-language-server:haskell-language-server-wrapper --- default-language: Haskell2010 --- build-depends: base == 4.* --- , directory --- , process --- , tasty --- , tasty-hunit --- , tasty-ant-xml >= 1.1.6 --- hs-source-dirs: test/wrapper --- main-is: Main.hs --- ghc-options: -Wall +test-suite wrapper-test + import: agpl, hls-test-utils + type: exitcode-stdio-1.0 + build-tool-depends: haskell-language-server:haskell-language-server-wrapper + default-language: Haskell2010 + build-depends: base == 4.* + , directory + , process + , tasty + , tasty-hunit + , tasty-ant-xml >= 1.1.6 + hs-source-dirs: test/wrapper + main-is: Main.hs + ghc-options: -Wall From bf2e93d42ab380ba35d78e8269b50db7180afe30 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 14:20:59 -0700 Subject: [PATCH 49/63] Intros, and disable some of the unpolished tactics --- src/Ide/Plugin/Tactic.hs | 49 ++++++++++++++++++++---------- src/Ide/Plugin/Tactic/Machinery.hs | 17 +++++++++++ src/Ide/Plugin/Tactic/Tactics.hs | 22 ++++++++++---- 3 files changed, 66 insertions(+), 22 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index cffeb086bc..ddfa4d76c9 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -49,7 +49,7 @@ descriptor plId = (defaultPluginDescriptor plId) (tcCommandId tc) (tacticDesc $ tcCommandName tc) (tacticCmd $ commandTactic tc)) - [minBound .. maxBound] + enabledTactics , pluginCodeActionProvider = Just codeActionProvider } @@ -64,11 +64,16 @@ data TacticCommand = Auto | Split | Intro + | Intros | Destruct - | Homo + | Homomorphism deriving (Eq, Ord, Show, Enum, Bounded) +enabledTactics :: [TacticCommand] +enabledTactics = [Intros, Destruct, Homomorphism] + + ------------------------------------------------------------------------------ -- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS -- UI. @@ -86,10 +91,6 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" tcCommandName :: TacticCommand -> T.Text tcCommandName = T.pack . show ------------------------------------------------------------------------------- --- | Construct a title for a command. -tcCommandTitle :: TacticCommand -> OccName -> T.Text -tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ ------------------------------------------------------------------------------ -- | Mapping from tactic commands to their contextual providers. See 'provide', @@ -100,21 +101,35 @@ commandProvider Split = provide Split "Split" "" commandProvider Intro = filterGoalType isFunction $ provide Intro "Intro" "" +commandProvider Intros = + filterGoalType isFunction $ + provide Intros "Introduce lambda" "" commandProvider Destruct = filterBindingType destructFilter $ \occ _ -> - provide Destruct (tcCommandTitle Destruct occ) $ T.pack $ occNameString occ -commandProvider Homo = + provide + Destruct + ("Case split on " <> T.pack (occNameString occ)) + . T.pack + $ occNameString occ +commandProvider Homomorphism = filterBindingType homoFilter $ \occ _ -> - provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ + provide + Homomorphism + ("Homomorphic case split on " <> T.pack (occNameString occ)) + . T.pack + $ occNameString occ + ------------------------------------------------------------------------------ -- | 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 Destruct = autoIfPossible . destruct -commandTactic Homo = autoIfPossible . homo +commandTactic Auto = const auto +commandTactic Split = const split +commandTactic Intro = const intro +commandTactic Intros = const intros +commandTactic Destruct = autoIfPossible . destruct +commandTactic Homomorphism = autoIfPossible . homo + ------------------------------------------------------------------------------ -- | We should show homos only when the goal type is the same as the binding @@ -123,6 +138,7 @@ homoFilter :: Type -> Type -> Bool homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2 homoFilter _ _ = False + ------------------------------------------------------------------------------ -- | We should show destruct for bindings only when those bindings have usual -- algebraic types. @@ -130,9 +146,11 @@ destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _ = False + runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state + codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = @@ -144,7 +162,7 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx liftMaybe $ toCurrentRange pos =<< srcSpanToRange span' actions <- lift $ -- This foldMap is over the function monoid. - foldMap commandProvider [minBound .. maxBound] + foldMap commandProvider enabledTactics plId uri resulting_range @@ -154,7 +172,6 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] - codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction diff --git a/src/Ide/Plugin/Tactic/Machinery.hs b/src/Ide/Plugin/Tactic/Machinery.hs index ffc9273e7a..5e9769eeff 100644 --- a/src/Ide/Plugin/Tactic/Machinery.hs +++ b/src/Ide/Plugin/Tactic/Machinery.hs @@ -9,6 +9,7 @@ module Ide.Plugin.Tactic.Machinery where import Control.Arrow +import Control.Monad.State (get, modify, evalStateT) import Data.Char import Data.Function import Data.List @@ -17,6 +18,7 @@ import qualified Data.Map as M import Data.Maybe import Data.Set (Set) import qualified Data.Set as S +import Data.Traversable import DataCon import Development.IDE.Types.Location import DynFlags (unsafeGlobalDynFlags) @@ -141,6 +143,21 @@ mkGoodName in_scope t = False -> tn +------------------------------------------------------------------------------ +-- | Like 'mkGoodName' but creates several apart names. +mkManyGoodNames + :: (Traversable t, Monad m) + => M.Map OccName a + -> t Type + -> m (t OccName) +mkManyGoodNames hy args = + flip evalStateT (getInScope hy) $ for args $ \at -> do + in_scope <- Control.Monad.State.get + let n = mkGoodName in_scope at + modify (n :) + pure n + + ------------------------------------------------------------------------------ -- | Use type information to create a reasonable name. mkTyName :: Type -> String diff --git a/src/Ide/Plugin/Tactic/Tactics.hs b/src/Ide/Plugin/Tactic/Tactics.hs index 1baf28e089..847d7ffd9a 100644 --- a/src/Ide/Plugin/Tactic/Tactics.hs +++ b/src/Ide/Plugin/Tactic/Tactics.hs @@ -10,7 +10,6 @@ module Ide.Plugin.Tactic.Tactics ) where import Control.Monad.Except (throwError) -import Control.Monad.State import Data.List import qualified Data.Map as M import Data.Traversable @@ -24,6 +23,7 @@ import GHC.SourceGen.Pat import Ide.Plugin.Tactic.Machinery import Name import Refinery.Tactic +import TcType import TyCoRep import Type @@ -48,6 +48,20 @@ intro = rule $ \(Judgement hy g) -> pure $ noLoc $ lambda [VarPat noExt $ noLoc $ Unqual v] $ unLoc sg _ -> throwError $ GoalMismatch "intro" g +------------------------------------------------------------------------------ +-- | Introduce a lambda binding every variable. +intros :: TacticsM () +intros = rule $ \(Judgement hy g) -> + case tcSplitFunTys $ unCType g of + ([], _) -> throwError $ GoalMismatch "intro" g + (as, b) -> do + vs <- mkManyGoodNames hy as + sg <- newSubgoal (M.fromList (zip vs $ fmap CType as) <> hy) $ CType b + pure + . noLoc + . lambda (fmap (bvar . fromString . occNameString) vs) + $ unLoc sg + ------------------------------------------------------------------------------ -- | Combinator for performign case splitting, and running sub-rules on the @@ -65,11 +79,7 @@ destruct' f term = rule $ \(Judgement hy g) -> do <$> do for (tyConDataCons tc) $ \dc -> do let args = dataConInstArgTys dc apps - names <- flip evalStateT (getInScope hy) $ for args $ \at -> do - in_scope <- Control.Monad.State.get - let n = mkGoodName in_scope at - modify (n :) - pure n + names <- mkManyGoodNames hy args let pat :: Pat GhcPs pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) From e0ecbb537fdf3292b282fac4d7767ac1ea3b0b78 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 14:21:43 -0700 Subject: [PATCH 50/63] Disable autoIfPossible --- src/Ide/Plugin/Tactic.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index ddfa4d76c9..d3ed3cd94d 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -127,8 +127,8 @@ commandTactic Auto = const auto commandTactic Split = const split commandTactic Intro = const intro commandTactic Intros = const intros -commandTactic Destruct = autoIfPossible . destruct -commandTactic Homomorphism = autoIfPossible . homo +commandTactic Destruct = destruct +commandTactic Homomorphism = homo ------------------------------------------------------------------------------ From 4967997d062058c51a712e5d783b898a9caffe09 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Wed, 9 Sep 2020 14:23:02 -0700 Subject: [PATCH 51/63] Fix stack.yaml --- stack.yaml | 37 +++++++++++++++++++++++-------------- 1 file changed, 23 insertions(+), 14 deletions(-) diff --git a/stack.yaml b/stack.yaml index 8fd265622a..605591b432 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-15.0 # Last 8.8.2 +resolver: lts-14.27 # Last 8.6.5 packages: - . @@ -9,48 +9,57 @@ ghc-options: extra-deps: - aeson-1.5.2.0 -- apply-refact-0.7.0.0 +- ansi-terminal-0.10.3 +- base-compat-0.10.5 - github: bubba/brittany commit: c59655f10d5ad295c2481537fc8abf0a297d9d1c -- butcher-1.3.3.2 -- bytestring-trie-0.2.5.0 +- butcher-1.3.3.1 +- Cabal-3.0.2.0 +- cabal-plan-0.6.2.0 - clock-0.7.2 -- constrained-dynamic-0.1.0.0 - extra-1.7.3 - floskell-0.10.4 - fourmolu-0.1.0.0@rev:1 +- fuzzy-0.1.0.0 # - ghcide-0.1.0 - ghc-check-0.5.0.1 +- ghc-exactprint-0.6.2 - ghc-lib-parser-8.10.1.20200523 - ghc-lib-parser-ex-8.10.0.4 +- haddock-api-2.22.0@rev:1 - haddock-library-1.8.0 - haskell-lsp-0.22.0.0 - haskell-lsp-types-0.22.0.0 -- haskell-src-exts-1.21.1 - hie-bios-0.6.1 -- hlint-2.2.8 -- hoogle-5.0.17.11 -- hsimport-0.11.0 - HsYAML-0.2.1.0@rev:1 - HsYAML-aeson-0.2.0.0@rev:2 -- ilist-0.3.1.0 +- indexed-profunctors-0.1 +- lens-4.18 - lsp-test-0.11.0.4 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 +- optics-core-0.2 +- optparse-applicative-0.15.1.0 - ormolu-0.1.2.0 +- parser-combinators-1.2.1 +- primitive-0.7.1.0 +- regex-base-0.94.0.0 +- regex-pcre-builtin-0.95.1.1.8.43 +- regex-tdfa-1.3.1.0 - retrie-0.1.1.1 -- semigroups-0.18.5 +- semialign-1.1 # - github: wz1000/shake # commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef - stylish-haskell-0.11.0.3 +- tasty-rerun-1.1.17 - temporary-1.2.1.1 - these-1.1.1.1 -- primitive-0.7.1.0@sha256:6a237bb338bcc43193077ff8e8c0f0ce2de14c652231496a15672e8b563a07e2,2604 -- refinery-0.1.0.0 +- type-equality-1 +- topograph-1 flags: haskell-language-server: - pedantic: false + pedantic: true retrie: BuildExecutable: false From 670bcdc883adeab9647fedba63124992c7e99624 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 21:27:46 -0700 Subject: [PATCH 52/63] Respond to simple PR comments. --- src/Ide/LocalBindings.hs | 3 ++- src/Ide/Plugin/Tactic.hs | 8 +++++--- src/Ide/Plugin/Tactic/Machinery.hs | 2 +- src/Ide/Plugin/Tactic/Tactics.hs | 14 ++++++++++---- src/Ide/TreeTransform.hs | 8 ++++---- 5 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 1d08ff5c03..4d9fac5360 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -20,13 +20,14 @@ import Data.Maybe import Data.Ord import Data.Set (Set) import qualified Data.Set as S -import GHC (TypecheckedModule (..), GhcTc, NoExt (..)) +import Development.IDE.GHC.Compat (TypecheckedModule (..), GhcTc, NoExt (..)) import HsBinds import HsExpr import Id import OccName import SrcLoc + ------------------------------------------------------------------------------ -- | The available bindings at every point in a Haskell tree. data Bindings = Bindings diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index d3ed3cd94d..8a20ef0fbd 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -24,10 +24,10 @@ import Development.IDE.Core.PositionMapping import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (TypeCheck)) import Development.IDE.Core.Service (runAction) import Development.IDE.Core.Shake (useWithStale, IdeState (..)) +import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (srcSpanToRange) import Development.Shake (Action) import DynFlags (unsafeGlobalDynFlags) -import GHC import GHC.Generics (Generic) import Ide.LocalBindings (bindings, mostSpecificSpan, holify) import Ide.Plugin (mkLspCommand) @@ -251,7 +251,7 @@ tacticCmd tac lf state (TacticParams uri range var_name) fromMaybeT (Right Null, Nothing) $ do (pos, _, jdg) <- MaybeT $ judgmentForHole state nfp range let dflags = unsafeGlobalDynFlags - pm <- lift $ useAnnotatedSource "tacticsCmd" state nfp + pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic jdg $ tac $ mkVarOcc @@ -270,7 +270,9 @@ tacticCmd tac lf state (TacticParams uri range var_name) , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams response) ) tacticCmd _ _ _ _ = - pure (Left $ ResponseError InvalidRequest (T.pack "nah") Nothing, Nothing) + pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing + , Nothing + ) fromMaybeT :: Functor m => a -> MaybeT m a -> m a diff --git a/src/Ide/Plugin/Tactic/Machinery.hs b/src/Ide/Plugin/Tactic/Machinery.hs index 5e9769eeff..a0e64f08d3 100644 --- a/src/Ide/Plugin/Tactic/Machinery.hs +++ b/src/Ide/Plugin/Tactic/Machinery.hs @@ -20,10 +20,10 @@ import Data.Set (Set) import qualified Data.Set as S import Data.Traversable import DataCon +import Development.IDE.GHC.Compat import Development.IDE.Types.Location import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS -import GHC import GHC.Generics import GHC.SourceGen.Overloaded import Ide.LocalBindings diff --git a/src/Ide/Plugin/Tactic/Tactics.hs b/src/Ide/Plugin/Tactic/Tactics.hs index 847d7ffd9a..308b867918 100644 --- a/src/Ide/Plugin/Tactic/Tactics.hs +++ b/src/Ide/Plugin/Tactic/Tactics.hs @@ -14,7 +14,7 @@ import Data.List import qualified Data.Map as M import Data.Traversable import DataCon -import GHC +import Development.IDE.GHC.Compat import GHC.Exts import GHC.SourceGen.Binds import GHC.SourceGen.Expr @@ -28,6 +28,12 @@ import TyCoRep import Type +------------------------------------------------------------------------------ +-- | Like 'bvar', but works over standard GHC 'OccName's. +bvar' :: BVar a => OccName -> a +bvar' = bvar . fromString . occNameString + + ------------------------------------------------------------------------------ -- | Use something in the hypothesis to fill the hole. assumption :: TacticsM () @@ -45,7 +51,7 @@ intro = rule $ \(Judgement hy g) -> (FunTy a b) -> do v <- pure $ mkGoodName (getInScope hy) a sg <- newSubgoal (M.singleton v (CType a) <> hy) $ CType b - pure $ noLoc $ lambda [VarPat noExt $ noLoc $ Unqual v] $ unLoc sg + pure $ noLoc $ lambda [bvar' v] $ unLoc sg _ -> throwError $ GoalMismatch "intro" g ------------------------------------------------------------------------------ @@ -59,7 +65,7 @@ intros = rule $ \(Judgement hy g) -> sg <- newSubgoal (M.fromList (zip vs $ fmap CType as) <> hy) $ CType b pure . noLoc - . lambda (fmap (bvar . fromString . occNameString) vs) + . lambda (fmap bvar' vs) $ unLoc sg @@ -83,7 +89,7 @@ destruct' f term = rule $ \(Judgement hy g) -> do let pat :: Pat GhcPs pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) - $ fmap (bvar . fromString . occNameString) names + $ fmap bvar' names j <- newJudgement (M.fromList (zip names (fmap CType args)) <> hy) g sg <- f dc j diff --git a/src/Ide/TreeTransform.hs b/src/Ide/TreeTransform.hs index 0aa2d4cec6..6c98c12393 100644 --- a/src/Ide/TreeTransform.hs +++ b/src/Ide/TreeTransform.hs @@ -16,8 +16,8 @@ import Debug.Trace import Development.IDE.Core.RuleTypes import Development.IDE.Core.Rules import Development.IDE.Core.Shake +import Development.IDE.GHC.Compat hiding (parseExpr) import Development.IDE.Types.Location -import GHC hiding (parseExpr) import Generics.SYB import Ide.PluginUtils import Language.Haskell.GHC.ExactPrint @@ -35,10 +35,10 @@ useAnnotatedSource :: String -> IdeState -> NormalizedFilePath - -> IO (Annotated ParsedSource) + -> IO (Maybe (Annotated ParsedSource)) useAnnotatedSource herald state nfp = do - Just pm <- runAction herald state $ use GetParsedModule nfp - pure $ fixAnns pm + pm <- runAction herald state $ use GetParsedModule nfp + pure $ fmap fixAnns pm ------------------------------------------------------------------------------ From 9b0544125589bb8f6e16b6783732313547b5bab0 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 21:43:35 -0700 Subject: [PATCH 53/63] Get a proper dflags --- src/Ide/Plugin/Tactic.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 8a20ef0fbd..41b43e68b4 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -21,13 +21,12 @@ import Data.Maybe import qualified Data.Text as T import Data.Traversable import Development.IDE.Core.PositionMapping -import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (TypeCheck)) +import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (..), GetModIface(..), hirModSummary) import Development.IDE.Core.Service (runAction) -import Development.IDE.Core.Shake (useWithStale, IdeState (..)) +import Development.IDE.Core.Shake (use, useWithStale, IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (srcSpanToRange) import Development.Shake (Action) -import DynFlags (unsafeGlobalDynFlags) import GHC.Generics (Generic) import Ide.LocalBindings (bindings, mostSpecificSpan, holify) import Ide.Plugin (mkLspCommand) @@ -250,7 +249,10 @@ tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do (pos, _, jdg) <- MaybeT $ judgmentForHole state nfp range - let dflags = unsafeGlobalDynFlags + -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' + -- which don't change very often. + (mod_iface, _) <- MaybeT $ runIde state $ useWithStale GetModIface nfp + let dflags = ms_hspp_opts $ hirModSummary mod_iface pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic jdg $ tac From 67b94af027c109d5bd6be188fc0755594a723280 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 22:19:21 -0700 Subject: [PATCH 54/63] WIP on a better bindings interface --- src/Ide/LocalBindings.hs | 18 +++++++++++++++++- src/Ide/Plugin/Tactic.hs | 2 +- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 4d9fac5360..c146a21ffd 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -10,6 +10,7 @@ module Ide.LocalBindings import Bag import Control.Lens +import Control.Monad import Data.Data.Lens import Data.Function import Data.Generics @@ -20,7 +21,7 @@ import Data.Maybe import Data.Ord import Data.Set (Set) import qualified Data.Set as S -import Development.IDE.GHC.Compat (TypecheckedModule (..), GhcTc, NoExt (..)) +import Development.IDE.GHC.Compat (TypecheckedModule (..), GhcTc, NoExt (..), RefMap, identType) import HsBinds import HsExpr import Id @@ -28,6 +29,21 @@ import OccName import SrcLoc +------------------------------------------------------------------------------ +-- | WIP function for getting 'bindings' from HIE, rather than stupidly +-- traversing the entire AST. +_bindigsHIE :: RefMap -> SrcSpan -> Set Id +_bindigsHIE _ (UnhelpfulSpan _) = mempty +_bindigsHIE refmap (RealSrcSpan span) = S.fromList $ do + (ident, refs) <- M.toList refmap + Right _name <- pure ident + (ref_span, ident_details) <- refs + Just _ty <- pure $ identType ident_details + guard $ ref_span `containsSpan` span + mempty + + + ------------------------------------------------------------------------------ -- | The available bindings at every point in a Haskell tree. data Bindings = Bindings diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 41b43e68b4..d71cb68200 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -23,7 +23,7 @@ import Data.Traversable import Development.IDE.Core.PositionMapping import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (..), GetModIface(..), hirModSummary) import Development.IDE.Core.Service (runAction) -import Development.IDE.Core.Shake (use, useWithStale, IdeState (..)) +import Development.IDE.Core.Shake (useWithStale, IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (srcSpanToRange) import Development.Shake (Action) From a45fde6e3f2d1c1c96cf8e787b48126a662a8c43 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 23:33:49 -0700 Subject: [PATCH 55/63] Simplify dflags lookup and expose titles --- src/Ide/Plugin/Tactic.hs | 48 +++++++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 20 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index d71cb68200..8be4c7bbbd 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -9,6 +9,8 @@ -- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic ( descriptor + , tacticTitle + , TacticCommand (..) ) where import Control.Monad @@ -21,13 +23,15 @@ import Data.Maybe import qualified Data.Text as T import Data.Traversable import Development.IDE.Core.PositionMapping -import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (..), GetModIface(..), hirModSummary) +import Development.IDE.Core.RuleTypes (TcModuleResult (tmrModule), TypeCheck (..), GhcSession(..)) import Development.IDE.Core.Service (runAction) import Development.IDE.Core.Shake (useWithStale, IdeState (..)) import Development.IDE.GHC.Compat import Development.IDE.GHC.Error (srcSpanToRange) +import Development.IDE.GHC.Util (hscEnv) import Development.Shake (Action) import GHC.Generics (Generic) +import HscTypes (hsc_dflags) import Ide.LocalBindings (bindings, mostSpecificSpan, holify) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.Machinery @@ -91,32 +95,35 @@ tcCommandName :: TacticCommand -> T.Text tcCommandName = T.pack . show +------------------------------------------------------------------------------ +-- | 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 + + ------------------------------------------------------------------------------ -- | Mapping from tactic commands to their contextual providers. See 'provide', -- 'filterGoalType' and 'filterBindingType' for the nitty gritty. commandProvider :: TacticCommand -> TacticProvider -commandProvider Auto = provide Auto "Auto" "" -commandProvider Split = provide Split "Split" "" +commandProvider Auto = provide Auto "" +commandProvider Split = provide Split "" commandProvider Intro = filterGoalType isFunction $ - provide Intro "Intro" "" + provide Intro "" commandProvider Intros = filterGoalType isFunction $ - provide Intros "Introduce lambda" "" + provide Intros "" commandProvider Destruct = filterBindingType destructFilter $ \occ _ -> - provide - Destruct - ("Case split on " <> T.pack (occNameString occ)) - . T.pack - $ occNameString occ + provide Destruct $ T.pack $ occNameString occ commandProvider Homomorphism = filterBindingType homoFilter $ \occ _ -> - provide - Homomorphism - ("Homomorphic case split on " <> T.pack (occNameString occ)) - . T.pack - $ occNameString occ + provide Homomorphism $ T.pack $ occNameString occ ------------------------------------------------------------------------------ @@ -178,9 +185,10 @@ codeActions = List . fmap CACodeAction ------------------------------------------------------------------------------ -- | Terminal constructor for providing context-sensitive tactics. Tactics -- given by 'provide' are always available. -provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider -provide tc title name plId uri range _ = do - let params = TacticParams { file = uri , range = range , var_name = name } +provide :: TacticCommand -> T.Text -> TacticProvider +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]) pure $ pure @@ -251,8 +259,8 @@ tacticCmd tac lf state (TacticParams uri range var_name) (pos, _, jdg) <- MaybeT $ judgmentForHole state nfp range -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. - (mod_iface, _) <- MaybeT $ runIde state $ useWithStale GetModIface nfp - let dflags = ms_hspp_opts $ hirModSummary mod_iface + (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp + let dflags = hsc_dflags $ hscEnv hscenv pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp case runTactic jdg $ tac From 75cb381f25aca1a33badcfff752fccee15210d04 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 23:38:47 -0700 Subject: [PATCH 56/63] Tactic tests --- haskell-language-server.cabal | 1 + test/functional/Main.hs | 2 + test/functional/Tactic.hs | 88 +++++++++++++++++++++++++++++++++ test/testdata/tactic/T1.hs | 3 ++ test/testdata/tactic/T2.hs | 2 + test/testdata/tactic/test.cabal | 17 +++++++ 6 files changed, 113 insertions(+) create mode 100644 test/functional/Tactic.hs create mode 100644 test/testdata/tactic/T1.hs create mode 100644 test/testdata/tactic/T2.hs create mode 100644 test/testdata/tactic/test.cabal diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index b9e43c1e93..4c46aaf211 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -291,6 +291,7 @@ test-suite func-test , Reference , Rename , Symbol + , Tactic , TypeDefinition ghc-options: -Wall -Wno-name-shadowing diff --git a/test/functional/Main.hs b/test/functional/Main.hs index 328a0e502f..d499adc3f5 100644 --- a/test/functional/Main.hs +++ b/test/functional/Main.hs @@ -21,6 +21,7 @@ import Progress import Reference import Rename import Symbol +import Tactic import TypeDefinition main :: IO () @@ -48,5 +49,6 @@ main = , Reference.tests , Rename.tests , Symbol.tests + , Tactic.tests , TypeDefinition.tests ] diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs new file mode 100644 index 0000000000..55886c2792 --- /dev/null +++ b/test/functional/Tactic.hs @@ -0,0 +1,88 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} + +module Tactic + ( tests + ) +where + +import Debug.Trace +import Data.Foldable +import Data.Text (Text) +import qualified Data.Text as T +import Control.Applicative.Combinators + ( skipManyTill ) +import Control.Monad.IO.Class ( MonadIO(liftIO) ) +import qualified Data.Text.IO as T +import Language.Haskell.LSP.Test +import Language.Haskell.LSP.Types ( ApplyWorkspaceEditRequest + , CodeLens + , Command(_title) + , Position(..) + , Range(..) + , Location(Location) + , CAResult(..) + , CodeAction(..) + , Uri + ) +import System.FilePath +import Test.Hls.Util +import Test.Tasty +import Test.Tasty.ExpectedFailure (expectFailBecause) +import Test.Tasty.HUnit +import Data.List +import Data.Maybe (listToMaybe, mapMaybe) +import Ide.Plugin.Tactic (tacticTitle, TacticCommand (..)) + + +pointRange :: Int -> Int -> Range +pointRange + (subtract 1 -> line) + (subtract 1 -> col) = + Range (Position line col) (Position line $ col + 1) + +codeActionTitle :: CAResult -> Maybe Text +codeActionTitle CACommand{} = Nothing +codeActionTitle (CACodeAction(CodeAction title _ _ _ _)) = Just title + +tests :: TestTree +tests = testGroup + "tactic" + [ mkTest + "Produces intros code action" + "T1.hs" 2 14 + [ (Intros, "") + ] + , mkTest + "Produces destruct and homomorphism code actions" + "T2.hs" 2 21 + [ (Destruct, "eab") + , (Homomorphism, "eab") + ] + ] + +mkTest + :: Foldable t + => String + -> FilePath + -> Int + -> Int + -> t (TacticCommand, Text) + -> TestTree +mkTest name fp line col ts = + testCase name $ do + runSession hieCommand fullCaps tacticPath $ do + doc <- openDoc fp "haskell" + actions <- getCodeActions doc $ pointRange line col + let titles = mapMaybe codeActionTitle actions + for_ ts $ \(tc, var) -> do + let title = tacticTitle tc var + liftIO $ + elem title titles + @? ("Expected a code action with title " <> T.unpack title) + +tacticPath :: FilePath +tacticPath = "test/testdata/tactic" + diff --git a/test/testdata/tactic/T1.hs b/test/testdata/tactic/T1.hs new file mode 100644 index 0000000000..7ab382d69f --- /dev/null +++ b/test/testdata/tactic/T1.hs @@ -0,0 +1,3 @@ +fmapEither :: (a -> b) -> Either c a -> Either c b +fmapEither = _lalala + diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs new file mode 100644 index 0000000000..83bdc32580 --- /dev/null +++ b/test/testdata/tactic/T2.hs @@ -0,0 +1,2 @@ +eitherFmap :: (a -> b) -> Either e a -> Either e b +eitherFmap fa eab = _ diff --git a/test/testdata/tactic/test.cabal b/test/testdata/tactic/test.cabal new file mode 100644 index 0000000000..845edafa26 --- /dev/null +++ b/test/testdata/tactic/test.cabal @@ -0,0 +1,17 @@ +name: test +version: 0.1.0.0 +-- synopsis: +-- description: +license: BSD3 +author: Author name here +maintainer: example@example.com +copyright: 2017 Author name here +category: Web +build-type: Simple +cabal-version: >=1.10 + +library + exposed-modules: T1, T2 + build-depends: base >= 4.7 && < 5 + default-language: Haskell2010 + ghc-options: -Wall -fwarn-unused-imports From a41fa2d5f460ae4a4e8ea7387c979a040f158f42 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 23:53:05 -0700 Subject: [PATCH 57/63] Add a few more tests --- test/functional/Tactic.hs | 30 ++++++++++++++++++++++++------ test/testdata/tactic/T2.hs | 7 +++++++ 2 files changed, 31 insertions(+), 6 deletions(-) diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 55886c2792..a636e8c3fa 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -53,13 +53,28 @@ tests = testGroup [ mkTest "Produces intros code action" "T1.hs" 2 14 - [ (Intros, "") + [ (id, Intros, "") ] , mkTest "Produces destruct and homomorphism code actions" "T2.hs" 2 21 - [ (Destruct, "eab") - , (Homomorphism, "eab") + [ (id, Destruct, "eab") + , (id, Homomorphism, "eab") + ] + , mkTest + "Can destruct globals" + "T2.hs" 8 8 + [ (id, Destruct, "global") + ] + , mkTest + "Won't suggest homomorphism on the wrong type" + "T2.hs" 8 8 + [ (not, Homomorphism, "global") + ] + , mkTest + "Won't suggest intros on the wrong type" + "T2.hs" 8 8 + [ (not, Intros, "") ] ] @@ -69,7 +84,10 @@ mkTest -> FilePath -> Int -> Int - -> t (TacticCommand, Text) + -> t ( Bool -> Bool -- Use 'not' for actions that shouldnt be present + , TacticCommand + , Text + ) -> TestTree mkTest name fp line col ts = testCase name $ do @@ -77,10 +95,10 @@ mkTest name fp line col ts = doc <- openDoc fp "haskell" actions <- getCodeActions doc $ pointRange line col let titles = mapMaybe codeActionTitle actions - for_ ts $ \(tc, var) -> do + for_ ts $ \(f, tc, var) -> do let title = tacticTitle tc var liftIO $ - elem title titles + f (elem title titles) @? ("Expected a code action with title " <> T.unpack title) tacticPath :: FilePath diff --git a/test/testdata/tactic/T2.hs b/test/testdata/tactic/T2.hs index 83bdc32580..a81756abbb 100644 --- a/test/testdata/tactic/T2.hs +++ b/test/testdata/tactic/T2.hs @@ -1,2 +1,9 @@ eitherFmap :: (a -> b) -> Either e a -> Either e b eitherFmap fa eab = _ + +global :: Bool +global = True + +foo :: Int +foo = _ + From 30d214a20521024572425f9d3dc09662338e68af Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Thu, 10 Sep 2020 23:56:00 -0700 Subject: [PATCH 58/63] Cleanup imports --- test/functional/Tactic.hs | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index a636e8c3fa..6a900b5517 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -8,32 +8,20 @@ module Tactic ) where -import Debug.Trace import Data.Foldable import Data.Text (Text) import qualified Data.Text as T -import Control.Applicative.Combinators - ( skipManyTill ) import Control.Monad.IO.Class ( MonadIO(liftIO) ) -import qualified Data.Text.IO as T import Language.Haskell.LSP.Test -import Language.Haskell.LSP.Types ( ApplyWorkspaceEditRequest - , CodeLens - , Command(_title) - , Position(..) +import Language.Haskell.LSP.Types ( Position(..) , Range(..) - , Location(Location) , CAResult(..) , CodeAction(..) - , Uri ) -import System.FilePath import Test.Hls.Util import Test.Tasty -import Test.Tasty.ExpectedFailure (expectFailBecause) import Test.Tasty.HUnit -import Data.List -import Data.Maybe (listToMaybe, mapMaybe) +import Data.Maybe (mapMaybe) import Ide.Plugin.Tactic (tacticTitle, TacticCommand (..)) From bb148441f206f38151aafdfc4ec89749510d1e0c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 11 Sep 2020 00:00:21 -0700 Subject: [PATCH 59/63] Haddock the tests --- test/functional/Tactic.hs | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 6a900b5517..6141ad41f8 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -25,16 +25,25 @@ import Data.Maybe (mapMaybe) import Ide.Plugin.Tactic (tacticTitle, TacticCommand (..)) +------------------------------------------------------------------------------ +-- | Get a range at the given line and column corresponding to having nothing +-- selected. +-- +-- NB: These coordinates are in "file space", ie, 1-indexed. pointRange :: Int -> Int -> Range pointRange (subtract 1 -> line) (subtract 1 -> col) = Range (Position line col) (Position line $ col + 1) + +------------------------------------------------------------------------------ +-- | Get the title of a code action. codeActionTitle :: CAResult -> Maybe Text codeActionTitle CACommand{} = Nothing codeActionTitle (CACodeAction(CodeAction title _ _ _ _)) = Just title + tests :: TestTree tests = testGroup "tactic" @@ -66,16 +75,19 @@ tests = testGroup ] ] + +------------------------------------------------------------------------------ +-- | Make a tactic unit test. mkTest :: Foldable t - => String - -> FilePath - -> Int - -> Int + => String -- ^ The test name + -> FilePath -- ^ The file to load + -> Int -- ^ Cursor line + -> Int -- ^ Cursor columnn -> t ( Bool -> Bool -- Use 'not' for actions that shouldnt be present - , TacticCommand - , Text - ) + , TacticCommand -- An expected command ... + , Text -- ... for this variable + ) -- ^ A collection of (un)expected code actions. -> TestTree mkTest name fp line col ts = testCase name $ do From 716b8efc5fc722339f73cc6ef1feda35e24b186c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 11 Sep 2020 11:08:00 -0700 Subject: [PATCH 60/63] Move tactic plugin --- {src => plugins/default/src}/Ide/LocalBindings.hs | 0 {src => plugins/default/src}/Ide/Plugin/Tactic.hs | 0 {src => plugins/default/src}/Ide/Plugin/Tactic/Machinery.hs | 0 {src => plugins/default/src}/Ide/Plugin/Tactic/Tactics.hs | 0 {src => plugins/default/src}/Ide/TreeTransform.hs | 0 5 files changed, 0 insertions(+), 0 deletions(-) rename {src => plugins/default/src}/Ide/LocalBindings.hs (100%) rename {src => plugins/default/src}/Ide/Plugin/Tactic.hs (100%) rename {src => plugins/default/src}/Ide/Plugin/Tactic/Machinery.hs (100%) rename {src => plugins/default/src}/Ide/Plugin/Tactic/Tactics.hs (100%) rename {src => plugins/default/src}/Ide/TreeTransform.hs (100%) diff --git a/src/Ide/LocalBindings.hs b/plugins/default/src/Ide/LocalBindings.hs similarity index 100% rename from src/Ide/LocalBindings.hs rename to plugins/default/src/Ide/LocalBindings.hs diff --git a/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs similarity index 100% rename from src/Ide/Plugin/Tactic.hs rename to plugins/default/src/Ide/Plugin/Tactic.hs diff --git a/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs similarity index 100% rename from src/Ide/Plugin/Tactic/Machinery.hs rename to plugins/default/src/Ide/Plugin/Tactic/Machinery.hs diff --git a/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs similarity index 100% rename from src/Ide/Plugin/Tactic/Tactics.hs rename to plugins/default/src/Ide/Plugin/Tactic/Tactics.hs diff --git a/src/Ide/TreeTransform.hs b/plugins/default/src/Ide/TreeTransform.hs similarity index 100% rename from src/Ide/TreeTransform.hs rename to plugins/default/src/Ide/TreeTransform.hs From d452bf3dcbdc017398dc729210bd940d8747a468 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 11 Sep 2020 11:25:41 -0700 Subject: [PATCH 61/63] Almost there! --- ghcide | 2 +- haskell-language-server.cabal | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/ghcide b/ghcide index 078e3d3c0d..96cf8c53d0 160000 --- a/ghcide +++ b/ghcide @@ -1 +1 @@ -Subproject commit 078e3d3c0d319f83841ccbcdc60ff5f0e243f6be +Subproject commit 96cf8c53d0bdc16d3d2cd0559b74962593ce6dc5 diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 2923a0cdc2..6a3a94c69d 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -127,6 +127,7 @@ executable haskell-language-server , haskell-lsp ^>=0.22 , hls-plugin-api , lens + , mtl , ormolu ^>=0.1.2 , refinery , regex-tdfa @@ -134,6 +135,7 @@ executable haskell-language-server , safe-exceptions , shake >=0.17.5 , stylish-haskell ^>=0.11 + , syb , temporary , time , transformers From f0728818eae841b517ecbc2b5ffc84b8d0151a2c Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Fri, 11 Sep 2020 20:18:09 -0700 Subject: [PATCH 62/63] Get the tests running again --- haskell-language-server.cabal | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 6a3a94c69d..6096ebe623 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -222,13 +222,23 @@ test-suite func-test , bytestring , data-default , lens + , ghc + , ghc-source-gen + , ghc-exactprint + , ghcide + , mtl + , refinery + , regex-tdfa + , retrie + , shake + , syb , tasty , tasty-ant-xml >=1.1.6 , tasty-expected-failure , tasty-golden , tasty-rerun - hs-source-dirs: test/functional + hs-source-dirs: test/functional plugins/default/src main-is: Main.hs other-modules: Command @@ -249,6 +259,11 @@ test-suite func-test Symbol Tactic TypeDefinition + Ide.LocalBindings + Ide.Plugin.Tactic + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Tactics + Ide.TreeTransform ghc-options: -Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N From 54cd86acc1d8804fb542f41adfec119c0b0e4c0d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sat, 12 Sep 2020 23:08:22 -0700 Subject: [PATCH 63/63] Empty commit for CI