Skip to content

Case splitting and lambda introduction #391

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
Sep 16, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 4 additions & 0 deletions exe/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"
Expand Down
23 changes: 22 additions & 1 deletion haskell-language-server.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,11 @@ executable haskell-language-server
Ide.Plugin.Pragmas
Ide.Plugin.Retrie
Ide.Plugin.StylishHaskell
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
Expand Down Expand Up @@ -123,13 +128,27 @@ 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
, ghc-source-gen
, refinery
, ghc-exactprint

if flag(agpl)
build-depends: brittany
Expand Down Expand Up @@ -218,7 +237,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
Expand All @@ -238,6 +257,8 @@ test-suite func-test
Rename
Symbol
TypeDefinition
Tactic
Ide.Plugin.Tactic.Types

ghc-options:
-Wall -Wno-name-shadowing -threaded -rtsopts -with-rtsopts=-N
Expand Down
269 changes: 269 additions & 0 deletions plugins/default/src/Ide/Plugin/Tactic.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,269 @@
{-# 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 qualified Data.Set as S
import Data.Maybe
import qualified Data.Text as T
import Data.Traversable
import Development.IDE.Core.PositionMapping
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 (realSrcSpanToRange)
import Development.IDE.GHC.Util (hscEnv)
import Development.Shake (Action)
import GHC.Generics (Generic)
import HscTypes (hsc_dflags)
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)
import Language.Haskell.LSP.Types
import OccName
import qualified FastString


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"

------------------------------------------------------------------------------

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

------------------------------------------------------------------------------
-- | 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
(_, span, jdg) <- MaybeT $ judgementForHole state nfp range
actions <- lift $
-- This foldMap is over the function monoid.
foldMap commandProvider enabledTactics
plId
uri
span
jdg
pure $ Right $ List actions
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.
judgementForHole
:: IdeState
-> NormalizedFilePath
-> Range
-> IO (Maybe (PositionMapping, Range, Judgement))
judgementForHole state nfp range = runMaybeT $ do
(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
let info = nodeInfo ast'
ty <- listToMaybe $ nodeType info
guard $ ("HsUnboundVar","HsExpr") `S.member` nodeAnnotations info
pure (nodeSpan ast', ty)

resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss

let hyps = hypothesisFromBindings rss binds
pure (amapping, resulting_range, 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 $ 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
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 $ 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
)


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

Loading