From 9cf7d5bb41db0eae8e38d945c3e259c7493f6101 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 6 Sep 2020 11:25:11 -0700 Subject: [PATCH 01/10] Add refinery [WIP] Add Skeleton for Tactic Plugin Local bindings [WIP] Add more to the code action provider more cases for bindings is it a hole? Beginning of tactics machinery tactics machinery split out tactics machinery; finish porting tactics Haddock for tactics machinery Use a map for hypothesis Better types on LocalBindings render the result of running a tactic Hypothesis from bindings Sort types mostSpecificSpan Render Actually add the tactic plugin :) [WIP] Do stuff slightly better span better sorting for specific spans Fix size [WIP] It does the thing!! Multiple tactic actions Parenthesize if necessary [WIP] Home on the 'Range' destruct and homo fix naming and parens Cleanup Plugin Tactic context dependent destruct and homo Generalized interface More composable Remove TacticVariety Haddock Describe spooky monoidal behavior Only look at actual holes Auto if possible debugging Maybe grafting works now Transformation works; tree doesnt Remove debugging Proper indentation and parenthesizing Less fancy parenthesizing Don't crash if we can't lookup things Holes must start with an underscore Haddock pass Module restructuring Fix the cabal file Intros, and disable some of the unpolished tactics Disable autoIfPossible Fix stack.yaml Respond to simple PR comments. Get a proper dflags WIP on a better bindings interface Simplify dflags lookup and expose titles Tactic tests Add a few more tests Cleanup imports Haddock the tests Rebase on ghcide HEAD (#378) * Rebase on top of ghcide HEAD * use Development.IDE to trim imports * Fix Eval plugin to use GhcSessionDeps Use stale data in explicit imports lens (#383) This prevents the lenses from disappearing while editing, which causes lots of unpleasant jumping Create hls-plugin-api and move plugins to exe Keep current version Add hls-plugin-api component to cradle Move exe modules to main library Format .cabal files with `cabal-fmt --ident 2` Restore ghcide ref Fix cradles Move tactic plugin Almost there! Get the tests running again Empty commit for CI Add refinery to stack more stack woes Duplicate NoExt and less dependency on ghc Cradle is necessary bump ghcide submodule (#396) * Bump ghcide submodule * Update stack descriptors Co-authored-by: Pepe Iborra Update ghcide Compute an interval map of what's in scope Fix 'binding' --- exe/Main.hs | 4 + haskell-language-server.cabal | 12 + plugins/default/src/Ide/LocalBindings.hs | 115 +++++++ plugins/default/src/Ide/Plugin/Tactic.hs | 300 ++++++++++++++++++ .../src/Ide/Plugin/Tactic/Machinery.hs | 256 +++++++++++++++ .../default/src/Ide/Plugin/Tactic/Tactics.hs | 181 +++++++++++ plugins/default/src/Ide/TreeTransform.hs | 124 ++++++++ stack-8.10.1.yaml | 1 + stack-8.10.2.yaml | 1 + stack-8.6.4.yaml | 2 + stack-8.6.5.yaml | 2 + stack-8.8.2.yaml | 1 + stack-8.8.3.yaml | 1 + stack-8.8.4.yaml | 1 + stack.yaml | 22 +- test/functional/Main.hs | 2 + test/functional/Tactic.hs | 106 +++++++ test/testdata/tactic/T1.hs | 3 + test/testdata/tactic/T2.hs | 9 + test/testdata/tactic/hie.yaml | 1 + test/testdata/tactic/test.cabal | 17 + 21 files changed, 1146 insertions(+), 15 deletions(-) create mode 100644 plugins/default/src/Ide/LocalBindings.hs create mode 100644 plugins/default/src/Ide/Plugin/Tactic.hs create mode 100644 plugins/default/src/Ide/Plugin/Tactic/Machinery.hs create mode 100644 plugins/default/src/Ide/Plugin/Tactic/Tactics.hs create mode 100644 plugins/default/src/Ide/TreeTransform.hs 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/hie.yaml create mode 100644 test/testdata/tactic/test.cabal diff --git a/exe/Main.hs b/exe/Main.hs index dfecd730ad..c6911722db 100644 --- a/exe/Main.hs +++ b/exe/Main.hs @@ -20,6 +20,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 @@ -45,6 +46,9 @@ idePlugins includeExamples = pluginDescToIdePlugins allPlugins , Pragmas.descriptor "pragmas" , Floskell.descriptor "floskell" , Fourmolu.descriptor "fourmolu" + , Tactic.descriptor "tactic" + -- , genericDescriptor "generic" + -- , ghcmodDescriptor "ghcmod" , Ormolu.descriptor "ormolu" , StylishHaskell.descriptor "stylish-haskell" , Retrie.descriptor "retrie" diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 8ead3a824c..d728cd3b22 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -112,6 +112,7 @@ executable haskell-language-server , deepseq , floskell ^>=0.10 , fourmolu ^>=0.1 + , fingertree , ghc , ghc-boot-th , ghcide >=0.1 @@ -123,10 +124,21 @@ executable haskell-language-server , ormolu ^>=0.1.2 , regex-tdfa , retrie >=0.1.1.0 + , hslogger + , optparse-applicative + , haskell-lsp ^>=0.22 + , hls-plugin-api + , lens + , mtl + , ormolu ^>=0.1.2 + , regex-tdfa + , retrie >=0.1.1.0 , safe-exceptions , shake >=0.17.5 , stylish-haskell ^>=0.11 , temporary + , text + , syb , time , transformers , unordered-containers diff --git a/plugins/default/src/Ide/LocalBindings.hs b/plugins/default/src/Ide/LocalBindings.hs new file mode 100644 index 0000000000..6bd57400a6 --- /dev/null +++ b/plugins/default/src/Ide/LocalBindings.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ide.LocalBindings + ( Bindings + , getLocalScope + , mostSpecificSpan + , holify + , bindings + ) where + +import Data.Function +import Data.Generics +import Data.IntervalMap.FingerTree (IntervalMap, Interval (..)) +import qualified Data.IntervalMap.FingerTree as IM +import Data.List +import qualified Data.Map as M +import Data.Maybe +import Data.Ord +import Data.Set (Set) +import qualified Data.Set as S +import Development.IDE.GHC.Compat (GhcTc, RefMap, identType, identInfo, noExt, getScopeFromContext, Scope(..)) +import HsExpr +import Id +import OccName +import SrcLoc + +------------------------------------------------------------------------------ +-- | Turn a 'RealSrcSpan' into an 'Interval'. +realSrcSpanToInterval :: RealSrcSpan -> Interval RealSrcLoc +realSrcSpanToInterval rss = + Interval + (realSrcSpanStart rss) + (realSrcSpanEnd rss) + + +------------------------------------------------------------------------------ +-- | Compute which identifiers are in scpoe at every point in the AST. Use +-- 'getLocalScope' to find the results. +bindings :: RefMap -> Bindings +bindings refmap = Bindings $ foldr (uncurry IM.insert) mempty $ do + (ident, refs) <- M.toList refmap + Right name <- pure ident + (ref_span, ident_details) <- refs + Just ty <- pure $ identType ident_details + info <- S.toList $ identInfo ident_details + Just scopes <- pure $ getScopeFromContext info + scope <- scopes >>= \case + ModuleScope -> pure $ + let file = srcSpanFile ref_span + in Interval + (mkRealSrcLoc file minBound minBound) + (mkRealSrcLoc file maxBound maxBound) + LocalScope scope -> pure $ realSrcSpanToInterval scope + NoScope -> [] + pure ( scope + , S.singleton $ mkVanillaGlobal name ty + ) + +------------------------------------------------------------------------------ +-- | The available bindings at every point in a Haskell tree. +newtype Bindings = Bindings + { getBindings :: IntervalMap RealSrcLoc (Set Id) + } deriving newtype (Eq, Ord, Semigroup, Monoid) + + +------------------------------------------------------------------------------ +-- | Given a 'Bindings' get every identifier in scope at the given +-- 'RealSrcSpan', +getLocalScope :: Bindings -> RealSrcSpan -> Set Id +getLocalScope bs rss + = foldMap snd + $ IM.dominators (realSrcSpanToInterval rss) + $ getBindings bs + + +------------------------------------------------------------------------------ +-- | 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 + ) + + +------------------------------------------------------------------------------ +-- | 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 (comparing srcSpanSize `on` getLoc) + $ everything (<>) (mkQ mempty $ \case + l@(L span' _) | span `isSubspanOf` span' -> [l] + _ -> []) + $ 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 bs v@(L s@(RealSrcSpan span) (HsVar _ (L _ var))) = + let occ = occName var + binds = getLocalScope bs span + in -- 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 s $ HsUnboundVar noExt $ TrueExprHole occ + False -> v +holify _ v = v + diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs new file mode 100644 index 0000000000..4b8ee366f2 --- /dev/null +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -0,0 +1,300 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +-- | A plugin that uses tactics to synthesize code +module Ide.Plugin.Tactic + ( descriptor + , tacticTitle + , TacticCommand (..) + ) where + +import Control.Monad +import Control.Monad.Trans +import Control.Monad.Trans.Maybe +import Data.Aeson +import Data.Coerce +import qualified Data.Map as M +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 (..), GhcSession(..), GetHieAst (..), refMap) +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 +import Ide.Plugin.Tactic.Tactics +import Ide.TreeTransform (transform, graft, useAnnotatedSource) +import Ide.Types +import Language.Haskell.LSP.Core (clientCapabilities) +import Language.Haskell.LSP.Types +import OccName +import Type + + +descriptor :: PluginId -> PluginDescriptor +descriptor plId = (defaultPluginDescriptor plId) + { pluginCommands + = fmap (\tc -> + PluginCommand + (tcCommandId tc) + (tacticDesc $ tcCommandName tc) + (tacticCmd $ commandTactic tc)) + enabledTactics + , pluginCodeActionProvider = Just codeActionProvider + } + +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 + | Intro + | Intros + | Destruct + | 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. +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 + + +------------------------------------------------------------------------------ +-- | 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 "" +commandProvider Split = provide Split "" +commandProvider Intro = + filterGoalType isFunction $ + provide Intro "" +commandProvider Intros = + filterGoalType isFunction $ + provide Intros "" +commandProvider Destruct = + filterBindingType destructFilter $ \occ _ -> + provide Destruct $ T.pack $ occNameString occ +commandProvider Homomorphism = + filterBindingType homoFilter $ \occ _ -> + provide Homomorphism $ 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 Intros = const intros +commandTactic Destruct = destruct +commandTactic Homomorphism = 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 + + +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 = + 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 enabledTactics + plId + uri + resulting_range + jdg + pure $ Right $ List actions + _ -> pure $ Right $ codeActions [] +codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] + + +codeActions :: [CodeAction] -> List CAResult +codeActions = List . fmap CACodeAction + + +------------------------------------------------------------------------------ +-- | Terminal constructor for providing context-sensitive tactics. Tactics +-- given by 'provide' are always available. +provide :: TacticCommand -> T.Text -> TacticProvider +provide tc name plId uri range _ = do + 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 + $ CACodeAction + $ 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) -- ^ Goal and then binding types. + -> (OccName -> Type -> TacticProvider) + -> TacticProvider +filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = + 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 :: Uri -- ^ Uri of the file to fill the hole in + , range :: Range -- ^ The range of the hole + , var_name :: T.Text + } + deriving (Show, Eq, 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 + -> 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 + + (mss@(L span' (HsVar _ (L _ v)))) + <- liftMaybe $ mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) + rss <- + liftMaybe $ case span' of + RealSrcSpan rss -> Just rss + _ -> Nothing + + (har, _) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp + let refs = refMap har + binds2 = bindings refs + + let goal = varType v + hyps = hypothesisFromBindings rss binds2 + pure (pos, holify binds2 mss, Judgement hyps $ CType goal) + + +tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams +tacticCmd tac lf state (TacticParams uri range var_name) + | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = + fromMaybeT (Right Null, Nothing) $ do + (pos, _, 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. + (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp + let dflags = hsc_dflags $ hscEnv hscenv + pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp + case runTactic 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 "Bad URI") 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 + diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs new file mode 100644 index 0000000000..6bb92bea25 --- /dev/null +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -0,0 +1,256 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ViewPatterns #-} + +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 +import Data.Map (Map) +import qualified Data.Map as M +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.Generics +import GHC.SourceGen.Overloaded +import Ide.LocalBindings +import Name +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 } + +instance Eq CType where + (==) = eqType `on` unCType + +instance Ord CType where + compare = nonDetCmpType `on` unCType + + +------------------------------------------------------------------------------ +-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis. +hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName CType +hypothesisFromBindings span bs = buildHypothesis (getLocalScope bs span) + + +------------------------------------------------------------------------------ +-- | Convert a @Set Id@ into a hypothesis. +buildHypothesis :: Set Id -> Map OccName CType +buildHypothesis + = M.fromList + . fmap (occName &&& CType . varType) + . filter (isAlpha . head . occNameString . occName) + . S.toList + + +------------------------------------------------------------------------------ +-- | The current bindings and goal for a hole to be filled by refinery. +data Judgement = Judgement + { jHypothesis :: Map OccName CType + , jGoal :: CType + } + deriving (Eq, Ord, Generic) + + +------------------------------------------------------------------------------ +-- | Reasons a tactic might fail. +data TacticError + = UndefinedHypothesis OccName + | GoalMismatch String CType + | UnsolvedSubgoals [Judgement] + | NoProgress + +instance Show TacticError where + 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) +type TacticsM = TacticT Judgement (LHsExpr GhcPs) ProvableM +type RuleM = RuleT Judgement (LHsExpr GhcPs) ProvableM +type Rule = RuleM (LHsExpr GhcPs) + + +------------------------------------------------------------------------------ +-- | Produce a subgoal that must be solved before we can solve the original +-- goal. +newSubgoal + :: Map 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 + => Map OccName CType -- ^ Available bindings + -> CType -- ^ Sub-goal type + -> m Judgement +newJudgement hy g = do + pure $ Judgement hy g + + +------------------------------------------------------------------------------ +-- | 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 + True -> tn ++ show (length in_scope) + 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 +-- 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" + + +------------------------------------------------------------------------------ +-- | Is this a function type? +isFunction :: Type -> Bool +isFunction (tcSplitFunTys -> ((_:_), _)) = True +isFunction _ = False + +------------------------------------------------------------------------------ +-- | 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 +mkTyConName tc + | tc == listTyCon = "l_" + | tc == pairTyCon = "p_" + | otherwise = fmap toLower . take 1 . occNameString $ getOccName tc + + +------------------------------------------------------------------------------ +-- | Attempt to generate a term of the right type using in-scope bindings, and +-- a given tactic. +runTactic + :: Judgement + -> TacticsM () -- ^ Tactic to use + -> Either TacticError (LHsExpr GhcPs) +runTactic jdg t + = fmap (fst) + . runProvableT + $ runTacticT t jdg + + +------------------------------------------------------------------------------ +-- | Which names are in scope? +getInScope :: Map OccName a -> [OccName] +getInScope = M.keys + + +------------------------------------------------------------------------------ +-- | Construct a data con with subgoals for each field. +buildDataCon + :: 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 + sgs <- traverse (newSubgoal hy . CType) args + pure + . noLoc + . foldl' (@@) + (HsVar noExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) + $ fmap unLoc sgs + + +------------------------------------------------------------------------------ +-- | 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/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs new file mode 100644 index 0000000000..d17512fc19 --- /dev/null +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -0,0 +1,181 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Tactics + ( module Ide.Plugin.Tactic.Tactics + , runTactic + ) where + +import Control.Monad.Except (throwError) +import Data.List +import qualified Data.Map as M +import Data.Traversable +import DataCon +import Development.IDE.GHC.Compat +import GHC.Exts +import GHC.SourceGen.Binds +import GHC.SourceGen.Expr +import GHC.SourceGen.Overloaded +import GHC.SourceGen.Pat +import Ide.Plugin.Tactic.Machinery +import Name +import Refinery.Tactic +import TcType +import TyCoRep +import Type hiding (Var) + + +------------------------------------------------------------------------------ +-- | Like 'var', but works over standard GHC 'OccName's. +var' :: Var a => OccName -> a +var' = var . fromString . occNameString + +------------------------------------------------------------------------------ +-- | 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 () +assumption = rule $ \(Judgement hy g) -> + case find ((== g) . snd) $ toList hy of + Just (v, _) -> pure $ noLoc $ var' v + Nothing -> throwError $ GoalMismatch "assumption" g + + +------------------------------------------------------------------------------ +-- | Introduce a lambda. +intro :: TacticsM () +intro = rule $ \(Judgement hy g) -> + case unCType g of + (FunTy a b) -> do + v <- pure $ mkGoodName (getInScope hy) a + sg <- newSubgoal (M.singleton v (CType a) <> hy) $ CType b + pure $ noLoc $ lambda [bvar' 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' vs) + $ unLoc sg + + +------------------------------------------------------------------------------ +-- | 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 + Nothing -> throwError $ UndefinedHypothesis term + Just (_, t) -> + case splitTyConApp_maybe $ unCType t of + Nothing -> throwError $ GoalMismatch "destruct" g + Just (tc, apps) -> do + fmap noLoc + $ case' (var' term) + <$> do + for (tyConDataCons tc) $ \dc -> do + let args = dataConInstArgTys dc apps + names <- mkManyGoodNames hy args + + let pat :: Pat GhcPs + pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc) + $ fmap bvar' names + + j <- newJudgement (M.fromList (zip names (fmap CType args)) <> hy) g + sg <- f dc j + 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) + + +------------------------------------------------------------------------------ +-- | 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 + Just (func, CType ty) -> do + let (args, _) = splitFunTys ty + sgs <- traverse (newSubgoal hy . CType) args + pure . noLoc + . foldl' (@@) (var' func) + $ fmap unLoc sgs + 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 + Just (tc, apps) -> + case tyConDataCons tc of + [dc] -> buildDataCon hy dc apps + _ -> throwError $ GoalMismatch "split" 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) + (split >> auto) + (apply >> 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/plugins/default/src/Ide/TreeTransform.hs b/plugins/default/src/Ide/TreeTransform.hs new file mode 100644 index 0000000000..6c98c12393 --- /dev/null +++ b/plugins/default/src/Ide/TreeTransform.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ide.TreeTransform + ( Graft, graft, transform, useAnnotatedSource + ) where + +import BasicTypes (appPrec) +import Control.Monad +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.GHC.Compat hiding (parseExpr) +import Development.IDE.Types.Location +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() + + +------------------------------------------------------------------------------ +-- | Get the latest version of the annotated parse source. +useAnnotatedSource + :: String + -> IdeState + -> NormalizedFilePath + -> IO (Maybe (Annotated ParsedSource)) +useAnnotatedSource herald state nfp = do + pm <- runAction herald state $ use GetParsedModule nfp + pure $ fmap 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 + } + +instance Semigroup (Graft a) where + Graft a <> Graft b = Graft $ \dflags -> a dflags >=> b dflags + +instance Monoid (Graft a) where + mempty = Graft $ const pure + + +------------------------------------------------------------------------------ +-- | Convert a 'Graft' into a 'WorkspaceEdit'. +transform + :: DynFlags + -> ClientCapabilities + -> Uri + -> Graft ParsedSource + -> Annotated ParsedSource + -> WorkspaceEdit +transform dflags ccs uri f a = + let src = printA a + a' = runIdentity $ transformA a $ runGraft f dflags + res = printA 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 + => SrcSpan + -> LHsExpr GhcPs + -> Graft a +graft dst val = Graft $ \dflags a -> do + (anns, val') <- annotate dflags $ parenthesize val + modifyAnnsT $ mappend anns + pure $ everywhere' + ( mkT $ + \case + (L src _ :: LHsExpr GhcPs) | src == dst -> val' + l -> l + ) 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 + let rendered = traceId $ render dflags expr + Right (anns, expr') = parseExpr dflags uniq rendered + 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 +parenthesize = parenthesizeHsExpr appPrec + diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml index 888d60fcf8..73d1c301fb 100644 --- a/stack-8.10.1.yaml +++ b/stack-8.10.1.yaml @@ -20,6 +20,7 @@ extra-deps: - HsYAML-aeson-0.2.0.0@rev:2 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 +- refinery-0.1.0.0 - retrie-0.1.1.1 - stylish-haskell-0.11.0.3 - semigroups-0.18.5 diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index 24f8f1168e..2906f4632d 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -21,6 +21,7 @@ extra-deps: - HsYAML-aeson-0.2.0.0@rev:2 - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 +- refinery-0.1.0.0 - retrie-0.1.1.1 - stylish-haskell-0.11.0.3 - semigroups-0.18.5 diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml index 33c7463533..5cf12189e0 100644 --- a/stack-8.6.4.yaml +++ b/stack-8.6.4.yaml @@ -28,6 +28,7 @@ extra-deps: - ghc-exactprint-0.6.2 - ghc-lib-parser-8.10.1.20200523 - ghc-lib-parser-ex-8.10.0.4 +- ghc-source-gen-0.4.0.0 - haddock-api-2.22.0@rev:1 - haddock-library-1.8.0 - haskell-lsp-0.22.0.0 @@ -45,6 +46,7 @@ extra-deps: - ormolu-0.1.2.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 +- refinery-0.1.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index 0a3e7dd963..92fa42fc43 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -27,6 +27,7 @@ extra-deps: - ghc-exactprint-0.6.2 - ghc-lib-parser-8.10.1.20200523 - ghc-lib-parser-ex-8.10.0.4 + ghc-source-gen-0.4.0.0 - haddock-api-2.22.0@rev:1 - haddock-library-1.8.0 - haskell-lsp-0.22.0.0 @@ -44,6 +45,7 @@ extra-deps: - ormolu-0.1.2.0 - parser-combinators-1.2.1 - primitive-0.7.1.0 +- refinery-0.1.0.0 - regex-base-0.94.0.0 - regex-pcre-builtin-0.95.1.1.8.43 - regex-tdfa-1.3.1.0 diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml index b6f531b938..7077b955e5 100644 --- a/stack-8.8.2.yaml +++ b/stack-8.8.2.yaml @@ -39,6 +39,7 @@ extra-deps: - monad-dijkstra-0.1.1.2 - opentelemetry-0.4.2 - ormolu-0.1.2.0 +- refinery-0.1.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml index ffff979c59..61529d4208 100644 --- a/stack-8.8.3.yaml +++ b/stack-8.8.3.yaml @@ -30,6 +30,7 @@ extra-deps: - ilist-0.3.1.0 - lsp-test-0.11.0.5 - monad-dijkstra-0.1.1.2 +- refinery-0.1.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 # - github: wz1000/shake diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml index 9234ceaeb9..dfc6d285e4 100644 --- a/stack-8.8.4.yaml +++ b/stack-8.8.4.yaml @@ -32,6 +32,7 @@ extra-deps: - ilist-0.3.1.0 - lsp-test-0.11.0.5 - monad-dijkstra-0.1.1.2 +- refinery-0.1.0.0 - retrie-0.1.1.1 - semigroups-0.18.5 - stylish-haskell-0.11.0.3 diff --git a/stack.yaml b/stack.yaml index 0a3e7dd963..ad00bb848b 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: - . @@ -10,24 +10,20 @@ 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 @@ -39,24 +35,20 @@ extra-deps: - lsp-test-0.11.0.5 - 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 +- refinery-0.1.0.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 flags: haskell-language-server: 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..6141ad41f8 --- /dev/null +++ b/test/functional/Tactic.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} + +module Tactic + ( tests + ) +where + +import Data.Foldable +import Data.Text (Text) +import qualified Data.Text as T +import Control.Monad.IO.Class ( MonadIO(liftIO) ) +import Language.Haskell.LSP.Test +import Language.Haskell.LSP.Types ( Position(..) + , Range(..) + , CAResult(..) + , CodeAction(..) + ) +import Test.Hls.Util +import Test.Tasty +import Test.Tasty.HUnit +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" + [ mkTest + "Produces intros code action" + "T1.hs" 2 14 + [ (id, Intros, "") + ] + , mkTest + "Produces destruct and homomorphism code actions" + "T2.hs" 2 21 + [ (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, "") + ] + ] + + +------------------------------------------------------------------------------ +-- | Make a tactic unit test. +mkTest + :: Foldable t + => 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 -- An expected command ... + , Text -- ... for this variable + ) -- ^ A collection of (un)expected code actions. + -> 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 $ \(f, tc, var) -> do + let title = tacticTitle tc var + liftIO $ + f (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..a81756abbb --- /dev/null +++ b/test/testdata/tactic/T2.hs @@ -0,0 +1,9 @@ +eitherFmap :: (a -> b) -> Either e a -> Either e b +eitherFmap fa eab = _ + +global :: Bool +global = True + +foo :: Int +foo = _ + diff --git a/test/testdata/tactic/hie.yaml b/test/testdata/tactic/hie.yaml new file mode 100644 index 0000000000..c95f6c9a09 --- /dev/null +++ b/test/testdata/tactic/hie.yaml @@ -0,0 +1 @@ +cradle: {direct: {arguments: ["T1", "T2"]}} 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 75655092ce0ed259da309ceed2582fda1a6f9442 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 00:41:16 +0530 Subject: [PATCH 02/10] Create Types module to reduce test dependencies --- haskell-language-server.cabal | 13 +++++++++++- plugins/default/src/Ide/Plugin/Tactic.hs | 26 +----------------------- test/functional/Tactic.hs | 2 +- 3 files changed, 14 insertions(+), 27 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index d728cd3b22..789c744e81 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -92,6 +92,12 @@ executable haskell-language-server Ide.Plugin.Pragmas Ide.Plugin.Retrie Ide.Plugin.StylishHaskell + Ide.LocalBindings + Ide.Plugin.Tactic + Ide.Plugin.Tactic.Types + Ide.Plugin.Tactic.Machinery + Ide.Plugin.Tactic.Tactics + Ide.TreeTransform ghc-options: -threaded -Wall -Wno-name-shadowing -Wredundant-constraints @@ -142,6 +148,9 @@ executable haskell-language-server , time , transformers , unordered-containers + , ghc-source-gen + , refinery + , ghc-exactprint if flag(agpl) build-depends: brittany @@ -230,7 +239,7 @@ test-suite func-test , tasty-golden , tasty-rerun - hs-source-dirs: test/functional + hs-source-dirs: test/functional plugins/default/src main-is: Main.hs other-modules: Command @@ -250,6 +259,8 @@ test-suite func-test Rename Symbol TypeDefinition + Tactic + Ide.Plugin.Tactic.Types ghc-options: -Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index 4b8ee366f2..a5c27f4b14 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -36,6 +36,7 @@ import Ide.LocalBindings (bindings, mostSpecificSpan, holify) import Ide.Plugin (mkLspCommand) import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types import Ide.TreeTransform (transform, graft, useAnnotatedSource) import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) @@ -60,23 +61,10 @@ 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 - | Intro - | Intros - | Destruct - | 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. @@ -94,18 +82,6 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" 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. diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 6141ad41f8..17ca8e3843 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -22,7 +22,7 @@ import Test.Hls.Util import Test.Tasty import Test.Tasty.HUnit import Data.Maybe (mapMaybe) -import Ide.Plugin.Tactic (tacticTitle, TacticCommand (..)) +import Ide.Plugin.Tactic.Types (tacticTitle, TacticCommand (..)) ------------------------------------------------------------------------------ From 3d017aa60b03281e7c464485c65233e15fb5bd35 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 14:52:20 +0530 Subject: [PATCH 03/10] Make it compile with 8.10, handle errors, move LocalBinding to ghcide --- cabal.project | 2 +- ghcide | 2 +- haskell-language-server.cabal | 10 +- plugins/default/src/Ide/LocalBindings.hs | 115 ------------------ plugins/default/src/Ide/Plugin/Tactic.hs | 72 +++++------ .../src/Ide/Plugin/Tactic/Machinery.hs | 36 +++--- .../default/src/Ide/Plugin/Tactic/Tactics.hs | 5 +- plugins/default/src/Ide/TreeTransform.hs | 20 +-- 8 files changed, 71 insertions(+), 191 deletions(-) delete mode 100644 plugins/default/src/Ide/LocalBindings.hs diff --git a/cabal.project b/cabal.project index 4d956fc5bd..5db0d1cd23 100644 --- a/cabal.project +++ b/cabal.project @@ -20,6 +20,6 @@ package ghcide write-ghc-environment-files: never -index-state: 2020-09-09T00:00:00Z +index-state: 2020-09-16T00:00:00Z allow-newer: data-tree-print:base diff --git a/ghcide b/ghcide index 008d4db3ff..bfe35e60cc 160000 --- a/ghcide +++ b/ghcide @@ -1 +1 @@ -Subproject commit 008d4db3ff3a8a3635bf3ac709d0df593f456d0a +Subproject commit bfe35e60cc5c5cf2a2bb73ca80d6b089c3ae5731 diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 789c744e81..33fc0e0103 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -70,7 +70,7 @@ library , process , unordered-containers - ghc-options: -Wall -Wredundant-constraints -Wno-name-shadowing + ghc-options: -Wall -Wredundant-constraints -Wno-name-shadowing -Wincomplete-uni-patterns if flag(pedantic) ghc-options: -Werror @@ -92,7 +92,6 @@ executable haskell-language-server Ide.Plugin.Pragmas Ide.Plugin.Retrie Ide.Plugin.StylishHaskell - Ide.LocalBindings Ide.Plugin.Tactic Ide.Plugin.Tactic.Types Ide.Plugin.Tactic.Machinery @@ -100,7 +99,7 @@ executable haskell-language-server Ide.TreeTransform ghc-options: - -threaded -Wall -Wno-name-shadowing -Wredundant-constraints + -threaded -Wall -Wno-name-shadowing -Wredundant-constraints -Wincomplete-uni-patterns -- allow user RTS overrides -rtsopts -- disable idle GC @@ -118,7 +117,6 @@ executable haskell-language-server , deepseq , floskell ^>=0.10 , fourmolu ^>=0.1 - , fingertree , ghc , ghc-boot-th , ghcide >=0.1 @@ -150,7 +148,7 @@ executable haskell-language-server , unordered-containers , ghc-source-gen , refinery - , ghc-exactprint + , ghc-exactprint >= 0.6.3.2 if flag(agpl) build-depends: brittany @@ -166,7 +164,7 @@ executable haskell-language-server-wrapper other-modules: Paths_haskell_language_server autogen-modules: Paths_haskell_language_server ghc-options: - -threaded -Wall -Wno-name-shadowing -Wredundant-constraints + -threaded -Wall -Wno-name-shadowing -Wredundant-constraints -Wincomplete-uni-patterns -- allow user RTS overrides -rtsopts -- disable idle GC diff --git a/plugins/default/src/Ide/LocalBindings.hs b/plugins/default/src/Ide/LocalBindings.hs deleted file mode 100644 index 6bd57400a6..0000000000 --- a/plugins/default/src/Ide/LocalBindings.hs +++ /dev/null @@ -1,115 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Ide.LocalBindings - ( Bindings - , getLocalScope - , mostSpecificSpan - , holify - , bindings - ) where - -import Data.Function -import Data.Generics -import Data.IntervalMap.FingerTree (IntervalMap, Interval (..)) -import qualified Data.IntervalMap.FingerTree as IM -import Data.List -import qualified Data.Map as M -import Data.Maybe -import Data.Ord -import Data.Set (Set) -import qualified Data.Set as S -import Development.IDE.GHC.Compat (GhcTc, RefMap, identType, identInfo, noExt, getScopeFromContext, Scope(..)) -import HsExpr -import Id -import OccName -import SrcLoc - ------------------------------------------------------------------------------- --- | Turn a 'RealSrcSpan' into an 'Interval'. -realSrcSpanToInterval :: RealSrcSpan -> Interval RealSrcLoc -realSrcSpanToInterval rss = - Interval - (realSrcSpanStart rss) - (realSrcSpanEnd rss) - - ------------------------------------------------------------------------------- --- | Compute which identifiers are in scpoe at every point in the AST. Use --- 'getLocalScope' to find the results. -bindings :: RefMap -> Bindings -bindings refmap = Bindings $ foldr (uncurry IM.insert) mempty $ do - (ident, refs) <- M.toList refmap - Right name <- pure ident - (ref_span, ident_details) <- refs - Just ty <- pure $ identType ident_details - info <- S.toList $ identInfo ident_details - Just scopes <- pure $ getScopeFromContext info - scope <- scopes >>= \case - ModuleScope -> pure $ - let file = srcSpanFile ref_span - in Interval - (mkRealSrcLoc file minBound minBound) - (mkRealSrcLoc file maxBound maxBound) - LocalScope scope -> pure $ realSrcSpanToInterval scope - NoScope -> [] - pure ( scope - , S.singleton $ mkVanillaGlobal name ty - ) - ------------------------------------------------------------------------------- --- | The available bindings at every point in a Haskell tree. -newtype Bindings = Bindings - { getBindings :: IntervalMap RealSrcLoc (Set Id) - } deriving newtype (Eq, Ord, Semigroup, Monoid) - - ------------------------------------------------------------------------------- --- | Given a 'Bindings' get every identifier in scope at the given --- 'RealSrcSpan', -getLocalScope :: Bindings -> RealSrcSpan -> Set Id -getLocalScope bs rss - = foldMap snd - $ IM.dominators (realSrcSpanToInterval rss) - $ getBindings bs - - ------------------------------------------------------------------------------- --- | 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 - ) - - ------------------------------------------------------------------------------- --- | 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 (comparing srcSpanSize `on` getLoc) - $ everything (<>) (mkQ mempty $ \case - l@(L span' _) | span `isSubspanOf` span' -> [l] - _ -> []) - $ 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 bs v@(L s@(RealSrcSpan span) (HsVar _ (L _ var))) = - let occ = occName var - binds = getLocalScope bs span - in -- 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 s $ HsUnboundVar noExt $ TrueExprHole occ - False -> v -holify _ v = v - diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index a5c27f4b14..f0eb49db68 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -23,16 +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 (..), GhcSession(..), GetHieAst (..), refMap) +import Development.IDE.Core.RuleTypes 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.Error (realSrcSpanToRange) 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 import Ide.Plugin.Tactic.Tactics @@ -42,7 +41,7 @@ import Ide.Types import Language.Haskell.LSP.Core (clientCapabilities) import Language.Haskell.LSP.Types import OccName -import Type +import qualified FastString descriptor :: PluginId -> PluginDescriptor @@ -137,20 +136,17 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | 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 enabledTactics - plId - uri - resulting_range - jdg - pure $ Right $ List actions - _ -> pure $ Right $ codeActions [] + (pos, span, jdg) <- MaybeT $ judgementForHole state nfp range + resulting_range <- + liftMaybe $ toCurrentRange pos $ realSrcSpanToRange span + actions <- lift $ + -- This foldMap is over the function monoid. + foldMap commandProvider enabledTactics + plId + uri + resulting_range + jdg + pure $ Right $ List actions codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -208,38 +204,33 @@ data TacticParams = TacticParams ------------------------------------------------------------------------------ -- | Find the last typechecked module, and find the most specific span, as well -- as the judgement at the given range. -judgmentForHole +judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (Maybe (PositionMapping, LHsExpr GhcTc, Judgement)) -judgmentForHole state nfp range = runMaybeT $ do - (tmr, pos) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp + -> IO (Maybe (PositionMapping, RealSrcSpan, Judgement)) +judgementForHole state nfp range = runMaybeT $ do + (asts, pos) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp range' <- liftMaybe $ fromCurrentRange pos range - let span = rangeToSrcSpan (fromNormalizedFilePath nfp) range' - mod = tmrModule tmr - (mss@(L span' (HsVar _ (L _ v)))) - <- liftMaybe $ mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) - rss <- - liftMaybe $ case span' of - RealSrcSpan rss -> Just rss - _ -> Nothing + (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> + case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of + Nothing -> Nothing + Just ast' -> do + ty <- listToMaybe $ nodeType $ nodeInfo ast' + pure (nodeSpan ast', ty) - (har, _) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp - let refs = refMap har - binds2 = bindings refs + (binds,_) <- MaybeT $ runIde state $ useWithStale GetBindings nfp - let goal = varType v - hyps = hypothesisFromBindings rss binds2 - pure (pos, holify binds2 mss, Judgement hyps $ CType goal) + let hyps = hypothesisFromBindings rss binds + pure (pos, rss, Judgement hyps $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right Null, Nothing) $ do - (pos, _, jdg) <- MaybeT $ judgmentForHole state nfp range + (pos, _, jdg) <- MaybeT $ judgementForHole state nfp range -- Ok to use the stale 'ModIface', since all we need is its 'DynFlags' -- which don't change very often. (hscenv, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp @@ -258,10 +249,9 @@ tacticCmd tac lf state (TacticParams uri range var_name) 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) - ) + pure $ case response of + Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res)) + Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing) tacticCmd _ _ _ _ = pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing , Nothing diff --git a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs index 6bb92bea25..51ef83e6cd 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Machinery.hs @@ -5,18 +5,16 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE ViewPatterns #-} 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 import Data.Map (Map) import qualified Data.Map as M -import Data.Set (Set) -import qualified Data.Set as S import Data.Traversable import DataCon import Development.IDE.GHC.Compat @@ -25,19 +23,21 @@ import DynFlags (unsafeGlobalDynFlags) import qualified FastString as FS import GHC.Generics import GHC.SourceGen.Overloaded -import Ide.LocalBindings +import Development.IDE.Spans.LocalBindings import Name import Outputable hiding ((<>)) import Refinery.Tactic import TcType import Type import TysWiredIn (listTyCon, pairTyCon, intTyCon, floatTyCon, doubleTyCon, charTyCon) +import Data.Maybe +import SrcLoc ------------------------------------------------------------------------------ -- | Orphan instance for producing holes when attempting to solve tactics. instance MonadExtract (LHsExpr GhcPs) ProvableM where - hole = pure $ noLoc $ HsVar noExt $ noLoc $ Unqual $ mkVarOcc "_" + hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_" ------------------------------------------------------------------------------ @@ -59,12 +59,17 @@ hypothesisFromBindings span bs = buildHypothesis (getLocalScope bs span) ------------------------------------------------------------------------------ -- | Convert a @Set Id@ into a hypothesis. -buildHypothesis :: Set Id -> Map OccName CType +buildHypothesis :: [(Name, Maybe Type)] -> Map OccName CType buildHypothesis = M.fromList - . fmap (occName &&& CType . varType) - . filter (isAlpha . head . occNameString . occName) - . S.toList + . mapMaybe go + where + go (n, t) + | Just ty <- t + , isAlpha . head . occNameString $ occ = Just (occ, CType ty) + | otherwise = Nothing + where + occ = occName n ------------------------------------------------------------------------------ @@ -236,7 +241,7 @@ buildDataCon hy dc apps = do pure . noLoc . foldl' (@@) - (HsVar noExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) + (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs @@ -244,10 +249,13 @@ buildDataCon hy dc apps = do -- | 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)) +rangeToSrcSpan file range = RealSrcSpan $ rangeToRealSrcSpan file range + +rangeToRealSrcSpan :: String -> Range -> RealSrcSpan +rangeToRealSrcSpan file (Range (Position startLn startCh) (Position endLn endCh)) = + mkRealSrcSpan + (mkRealSrcLoc (FS.fsLit file) (startLn + 1) (startCh + 1)) + (mkRealSrcLoc (FS.fsLit file) (endLn + 1) (endCh + 1)) ------------------------------------------------------------------------------ -- | Print something diff --git a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs index d17512fc19..a86e668568 100644 --- a/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/default/src/Ide/Plugin/Tactic/Tactics.hs @@ -24,7 +24,6 @@ import Ide.Plugin.Tactic.Machinery import Name import Refinery.Tactic import TcType -import TyCoRep import Type hiding (Var) @@ -52,8 +51,8 @@ assumption = rule $ \(Judgement hy g) -> -- | Introduce a lambda. intro :: TacticsM () intro = rule $ \(Judgement hy g) -> - case unCType g of - (FunTy a b) -> do + case splitFunTy_maybe $ unCType g of + Just (a, b) -> do v <- pure $ mkGoodName (getInScope hy) a sg <- newSubgoal (M.singleton v (CType a) <> hy) $ CType b pure $ noLoc $ lambda [bvar' v] $ unLoc sg diff --git a/plugins/default/src/Ide/TreeTransform.hs b/plugins/default/src/Ide/TreeTransform.hs index 6c98c12393..996c552c43 100644 --- a/plugins/default/src/Ide/TreeTransform.hs +++ b/plugins/default/src/Ide/TreeTransform.hs @@ -10,7 +10,7 @@ module Ide.TreeTransform import BasicTypes (appPrec) import Control.Monad -import Data.Functor.Identity +import Control.Monad.Trans.Class import qualified Data.Text as T import Debug.Trace import Development.IDE.Core.RuleTypes @@ -45,7 +45,7 @@ useAnnotatedSource herald state nfp = do -- | 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 + { runGraft :: DynFlags -> a -> TransformT (Either String) a } instance Semigroup (Graft a) where @@ -63,12 +63,12 @@ transform -> Uri -> Graft ParsedSource -> Annotated ParsedSource - -> WorkspaceEdit -transform dflags ccs uri f a = + -> Either String WorkspaceEdit +transform dflags ccs uri f a = do let src = printA a - a' = runIdentity $ transformA a $ runGraft f dflags - res = printA a' - in diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions + a' <- transformA a $ runGraft f dflags + let res = printA a' + pure $ diffText ccs (uri, T.pack src) (T.pack res) IncludeDeletions ------------------------------------------------------------------------------ @@ -102,12 +102,12 @@ fixAnns ParsedModule {..} = ------------------------------------------------------------------------------ -- | Given an 'LHSExpr', compute its exactprint annotations. -annotate :: DynFlags -> LHsExpr GhcPs -> Transform (Anns, LHsExpr GhcPs) +annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (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 + (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered + let anns' = setPrecedingLines expr' 0 1 anns pure (anns', expr') From ea463072feb03e11864953cc8a6fae06d73d64b2 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 15:10:55 +0530 Subject: [PATCH 04/10] fix 8.10 stack yaml (let's pray) --- stack-8.10.1.yaml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml index 73d1c301fb..2a27d5e908 100644 --- a/stack-8.10.1.yaml +++ b/stack-8.10.1.yaml @@ -25,6 +25,8 @@ extra-deps: - stylish-haskell-0.11.0.3 - semigroups-0.18.5 - temporary-1.2.1.1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 flags: haskell-language-server: From b458743aa2d19100e9c695e23380b1d1727dbc86 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 15:57:00 +0530 Subject: [PATCH 05/10] update stack.yamls --- haskell-language-server.cabal | 6 +++--- stack-8.10.1.yaml | 1 + stack-8.10.2.yaml | 3 +++ stack-8.6.4.yaml | 2 ++ stack-8.6.5.yaml | 3 +++ stack-8.8.2.yaml | 4 +++- stack-8.8.3.yaml | 4 +++- stack-8.8.4.yaml | 3 +++ stack.yaml | 3 +++ 9 files changed, 24 insertions(+), 5 deletions(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 33fc0e0103..42e1c87786 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -70,7 +70,7 @@ library , process , unordered-containers - ghc-options: -Wall -Wredundant-constraints -Wno-name-shadowing -Wincomplete-uni-patterns + ghc-options: -Wall -Wredundant-constraints -Wno-name-shadowing if flag(pedantic) ghc-options: -Werror @@ -99,7 +99,7 @@ executable haskell-language-server Ide.TreeTransform ghc-options: - -threaded -Wall -Wno-name-shadowing -Wredundant-constraints -Wincomplete-uni-patterns + -threaded -Wall -Wno-name-shadowing -Wredundant-constraints -- allow user RTS overrides -rtsopts -- disable idle GC @@ -164,7 +164,7 @@ executable haskell-language-server-wrapper other-modules: Paths_haskell_language_server autogen-modules: Paths_haskell_language_server ghc-options: - -threaded -Wall -Wno-name-shadowing -Wredundant-constraints -Wincomplete-uni-patterns + -threaded -Wall -Wno-name-shadowing -Wredundant-constraints -- allow user RTS overrides -rtsopts -- disable idle GC diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml index 2a27d5e908..483e9dd060 100644 --- a/stack-8.10.1.yaml +++ b/stack-8.10.1.yaml @@ -27,6 +27,7 @@ extra-deps: - temporary-1.2.1.1 - implicit-hie-cradle-0.2.0.0 - implicit-hie-0.1.1.0 +- hie-bios-0.7.1 flags: haskell-language-server: diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml index 2906f4632d..348a1afae3 100644 --- a/stack-8.10.2.yaml +++ b/stack-8.10.2.yaml @@ -26,6 +26,9 @@ extra-deps: - stylish-haskell-0.11.0.3 - semigroups-0.18.5 - temporary-1.2.1.1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 +- hie-bios-0.7.1 flags: haskell-language-server: diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml index 5cf12189e0..f501b90af4 100644 --- a/stack-8.6.4.yaml +++ b/stack-8.6.4.yaml @@ -60,6 +60,8 @@ extra-deps: - these-1.1.1.1 - type-equality-1 - topograph-1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 flags: haskell-language-server: diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index 92fa42fc43..527ce126ad 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -59,6 +59,9 @@ extra-deps: - these-1.1.1.1 - type-equality-1 - topograph-1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 +- hie-bios-0.7.1 flags: haskell-language-server: diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml index 7077b955e5..60b183aee1 100644 --- a/stack-8.8.2.yaml +++ b/stack-8.8.2.yaml @@ -28,7 +28,6 @@ extra-deps: - haskell-lsp-0.22.0.0 - haskell-lsp-types-0.22.0.0 - haskell-src-exts-1.21.1 -- hie-bios-0.7.1 - hlint-2.2.8 - hoogle-5.0.17.11 - hsimport-0.11.0 @@ -47,6 +46,9 @@ extra-deps: - stylish-haskell-0.11.0.3 - temporary-1.2.1.1 - these-1.1.1.1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 +- hie-bios-0.7.1 flags: haskell-language-server: diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml index 61529d4208..0765b96059 100644 --- a/stack-8.8.3.yaml +++ b/stack-8.8.3.yaml @@ -22,7 +22,6 @@ extra-deps: - fourmolu-0.1.0.0@rev:1 # - ghcide-0.1.0 - haskell-src-exts-1.21.1 -- hie-bios-0.7.1 - hlint-2.2.8 - HsYAML-aeson-0.2.0.0@rev:2 - hoogle-5.0.17.11 @@ -37,6 +36,9 @@ extra-deps: # commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef - stylish-haskell-0.11.0.3 - temporary-1.2.1.1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 +- hie-bios-0.7.1 flags: haskell-language-server: diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml index dfc6d285e4..1543ee1a8f 100644 --- a/stack-8.8.4.yaml +++ b/stack-8.8.4.yaml @@ -39,6 +39,9 @@ extra-deps: # - github: wz1000/shake # commit: fb3859dca2e54d1bbb2c873e68ed225fa179fbef - temporary-1.2.1.1 +- ghc-exactprint-0.6.3.2 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 flags: haskell-language-server: diff --git a/stack.yaml b/stack.yaml index ad00bb848b..105679716a 100644 --- a/stack.yaml +++ b/stack.yaml @@ -49,6 +49,9 @@ extra-deps: - stylish-haskell-0.11.0.3 - temporary-1.2.1.1 - these-1.1.1.1 +- implicit-hie-cradle-0.2.0.0 +- implicit-hie-0.1.1.0 +- hie-bios-0.7.1 flags: haskell-language-server: From 3583d546ca17fe5531c2bcdaa979f4c191868970 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 16:43:13 +0530 Subject: [PATCH 06/10] add missing file --- .../default/src/Ide/Plugin/Tactic/Types.hs | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 plugins/default/src/Ide/Plugin/Tactic/Types.hs diff --git a/plugins/default/src/Ide/Plugin/Tactic/Types.hs b/plugins/default/src/Ide/Plugin/Tactic/Types.hs new file mode 100644 index 0000000000..5d0ae4042c --- /dev/null +++ b/plugins/default/src/Ide/Plugin/Tactic/Types.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE OverloadedStrings #-} +module Ide.Plugin.Tactic.Types + ( tacticTitle + , TacticCommand (..) + ) where + +import qualified Data.Text as T + +------------------------------------------------------------------------------ +-- | 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 + | Intro + | Intros + | Destruct + | Homomorphism + deriving (Eq, Ord, Show, Enum, Bounded) + +-- | Generate a title for the command. +tacticTitle :: TacticCommand -> T.Text -> T.Text +tacticTitle Auto _ = "Auto" +tacticTitle Split _ = "Auto" +tacticTitle Intro _ = "Intro" +tacticTitle Intros _ = "Introduce lambda" +tacticTitle Destruct var = "Case split on " <> var +tacticTitle Homomorphism var = "Homomorphic case split on " <> var From 418b9bd6f64c39cb5cbddb63c1a71a9e67fbff17 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 17:20:12 +0530 Subject: [PATCH 07/10] relax exactprint bound --- haskell-language-server.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal index 42e1c87786..46a48386ce 100644 --- a/haskell-language-server.cabal +++ b/haskell-language-server.cabal @@ -148,7 +148,7 @@ executable haskell-language-server , unordered-containers , ghc-source-gen , refinery - , ghc-exactprint >= 0.6.3.2 + , ghc-exactprint if flag(agpl) build-depends: brittany From 7ada5383c4477f6f95e341984c896721f807bb27 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 19:24:42 +0530 Subject: [PATCH 08/10] aarghhh add missing '-' to stack-8.6.5.yaml --- stack-8.6.5.yaml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml index 527ce126ad..48f52f1bcc 100644 --- a/stack-8.6.5.yaml +++ b/stack-8.6.5.yaml @@ -25,9 +25,9 @@ extra-deps: # - 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 - ghc-source-gen-0.4.0.0 +- ghc-lib-parser-8.10.2.20200808 +- ghc-lib-parser-ex-8.10.0.16 +- ghc-source-gen-0.4.0.0 - haddock-api-2.22.0@rev:1 - haddock-library-1.8.0 - haskell-lsp-0.22.0.0 @@ -61,7 +61,6 @@ extra-deps: - topograph-1 - implicit-hie-cradle-0.2.0.0 - implicit-hie-0.1.1.0 -- hie-bios-0.7.1 flags: haskell-language-server: From 85713e8b9e8bae2eefb105d46a674f8ef4ce962e Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 22:07:34 +0530 Subject: [PATCH 09/10] Only produce code actions for unbound variables --- plugins/default/src/Ide/Plugin/Tactic.hs | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/plugins/default/src/Ide/Plugin/Tactic.hs b/plugins/default/src/Ide/Plugin/Tactic.hs index f0eb49db68..6629a29471 100644 --- a/plugins/default/src/Ide/Plugin/Tactic.hs +++ b/plugins/default/src/Ide/Plugin/Tactic.hs @@ -19,6 +19,7 @@ import Control.Monad.Trans.Maybe import Data.Aeson import Data.Coerce import qualified Data.Map as M +import qualified Data.Set as S import Data.Maybe import qualified Data.Text as T import Data.Traversable @@ -136,15 +137,13 @@ codeActionProvider :: CodeActionProvider codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = fromMaybeT (Right $ List []) $ do - (pos, span, jdg) <- MaybeT $ judgementForHole state nfp range - resulting_range <- - liftMaybe $ toCurrentRange pos $ realSrcSpanToRange span + (_, span, jdg) <- MaybeT $ judgementForHole state nfp range actions <- lift $ -- This foldMap is over the function monoid. foldMap commandProvider enabledTactics plId uri - resulting_range + span jdg pure $ Right $ List actions codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -208,22 +207,26 @@ judgementForHole :: IdeState -> NormalizedFilePath -> Range - -> IO (Maybe (PositionMapping, RealSrcSpan, Judgement)) + -> IO (Maybe (PositionMapping, Range, Judgement)) judgementForHole state nfp range = runMaybeT $ do - (asts, pos) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp - range' <- liftMaybe $ fromCurrentRange pos range + (asts, amapping) <- MaybeT $ runIde state $ useWithStale GetHieAst nfp + range' <- liftMaybe $ fromCurrentRange amapping range + + (binds, _) <- MaybeT $ runIde state $ useWithStale GetBindings nfp (rss, goal) <- liftMaybe $ join $ listToMaybe $ M.elems $ flip M.mapWithKey (getAsts $ hieAst asts) $ \fs ast -> case selectSmallestContaining (rangeToRealSrcSpan (FastString.unpackFS fs) range') ast of Nothing -> Nothing Just ast' -> do - ty <- listToMaybe $ nodeType $ nodeInfo ast' + let info = nodeInfo ast' + ty <- listToMaybe $ nodeType info + guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info pure (nodeSpan ast', ty) - (binds,_) <- MaybeT $ runIde state $ useWithStale GetBindings nfp + resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss let hyps = hypothesisFromBindings rss binds - pure (pos, rss, Judgement hyps $ CType goal) + pure (amapping, resulting_range, Judgement hyps $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams From ea487566b968921e7caa10fa9ebc8d16d7e96b61 Mon Sep 17 00:00:00 2001 From: Zubin Duggal Date: Wed, 16 Sep 2020 22:28:03 +0530 Subject: [PATCH 10/10] make 8.6.5 default stack.yaml --- stack.yaml | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/stack.yaml b/stack.yaml index 105679716a..48f52f1bcc 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: - . @@ -10,20 +10,25 @@ 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-lib-parser-8.10.1.20200523 -- ghc-lib-parser-ex-8.10.0.4 +- ghc-exactprint-0.6.2 +- ghc-lib-parser-8.10.2.20200808 +- ghc-lib-parser-ex-8.10.0.16 +- ghc-source-gen-0.4.0.0 +- 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 @@ -35,6 +40,8 @@ extra-deps: - lsp-test-0.11.0.5 - 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 @@ -43,15 +50,17 @@ extra-deps: - 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 +- type-equality-1 +- topograph-1 - implicit-hie-cradle-0.2.0.0 - implicit-hie-0.1.1.0 -- hie-bios-0.7.1 flags: haskell-language-server: