Generalized interface

src/Ide/LocalBindings.hs

@@ -5,10 +5,9 @@ module Ide.LocalBindings
   ( Bindings (..)
   , bindings
   , mostSpecificSpan
-  , isItAHole
+  , holify
   ) where
 
-import Data.Ord
 import           Bag
 import           Control.Lens
 import           Data.Data.Lens
@@ -18,16 +17,16 @@ import           Data.List
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
-import           Data.Monoid
+import           Data.Ord
 import           Data.Set (Set)
 import qualified Data.Set as S
-import           GHC (TypecheckedModule (..), GhcTc)
+import           GHC (TypecheckedModule (..), GhcTc, NoExt (..))
 import           HsBinds
 import           HsExpr
 import           Id
+import           OccName
 import           SrcLoc
 
-
 data Bindings = Bindings
   { bGlobalBinds :: Set Id
   , bLocalBinds  :: Map SrcSpan (Set Id)
@@ -160,12 +159,16 @@ mostSpecificSpan span z
       _                                        -> [])
   $ z
 
-isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar
-isItAHole tcm span = getFirst $
-  everything (<>) (
-    mkQ mempty $ \case
-      L span' (HsUnboundVar _ z :: HsExpr GhcTc)
-        | span == span' -> pure z
-      _ -> mempty
-    ) $ tm_typechecked_source tcm
+------------------------------------------------------------------------------
+-- | Convert an HsVar back into an HsUnboundVar if it isn't actually in scope.
+-- TODO(sandy): this will throw away the type >:(
+holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc
+holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) =
+  case M.lookup span local of
+    Nothing -> v
+    Just binds ->
+      case S.member var binds of
+        True  -> v
+        False -> L span $ HsUnboundVar NoExt $ TrueExprHole $ occName var
+holify _ v = v
 

src/Ide/Plugin/Tactic.hs

@@ -1,10 +1,11 @@
--- | A plugin that uses tactics to synthesize code
 {-# LANGUAGE DeriveAnyClass    #-}
 {-# LANGUAGE DeriveGeneric     #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TupleSections     #-}
 {-# LANGUAGE TypeApplications  #-}
+{-# LANGUAGE ViewPatterns      #-}
 
+-- | A plugin that uses tactics to synthesize code
 module Ide.Plugin.Tactic
   ( descriptor
   ) where
@@ -36,43 +37,103 @@ import           Ide.LocalBindings
 import qualified Language.Haskell.LSP.Types      as J
 import           Language.Haskell.LSP.Types
 
+import Data.List (intercalate)
 import OccName
 import           HsExpr
 import           GHC
 import           DynFlags
 import           Type
+import System.IO
 
 
 descriptor :: PluginId -> PluginDescriptor
 descriptor plId = (defaultPluginDescriptor plId)
     { pluginCommands
-        = fmap (\(name, tac) ->
+        = fmap (\tc ->
             PluginCommand
-              (coerce $ name <> "Command")
-              (tacticDesc name)
-              (tacticCmd tac))
-              (Map.toList registeredCommands)
+              (tcCommandId tc)
+              (tacticDesc $ tcCommandName tc)
+              (tacticCmd $ commandTactic tc))
+              [minBound .. maxBound]
     , pluginCodeActionProvider = Just codeActionProvider
     }
 
 tacticDesc :: T.Text -> T.Text
 tacticDesc name = "fill the hole using the " <> name <> " tactic"
 
-registeredCommands :: Map.Map T.Text (OccName -> TacticsM ())
-registeredCommands = Map.fromList
-    [ ("auto",     const auto)
-    , ("split",    const split)
-    , ("intro",    const intro)
-    , ("destruct", destruct)
-    , ("homo",     homo)
-    ]
-
-alwaysCommands :: [T.Text]
-alwaysCommands =
-    [ "auto"
-    , "split"
-    , "intro"
-    ]
+------------------------------------------------------------------------------
+-- | 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
+  | Destruct
+  | Homo
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
+
+------------------------------------------------------------------------------
+-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
+-- UI.
+type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
+
+
+------------------------------------------------------------------------------
+-- | Construct a 'CommandId'
+tcCommandId :: TacticCommand -> CommandId
+tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
+
+
+------------------------------------------------------------------------------
+-- | The name of the command for the LS.
+tcCommandName :: TacticCommand -> T.Text
+tcCommandName = T.pack . show
+
+------------------------------------------------------------------------------
+-- | Construct a title for a command.
+tcCommandTitle :: TacticCommand -> OccName -> T.Text
+tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ
+
+------------------------------------------------------------------------------
+-- | Mapping from tactic commands to their contextual providers. See 'provide',
+-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
+commandProvider :: TacticCommand -> TacticProvider
+commandProvider Auto  = provide Auto "Auto" ""
+commandProvider Split = provide Split "Split" ""
+commandProvider Intro =
+  filterGoalType isFunction $
+    provide Intro "Intro" ""
+commandProvider Destruct =
+  filterBindingType destructFilter $ \occ _ ->
+    provide Destruct (tcCommandTitle Destruct occ) $ T.pack $ occNameString occ
+commandProvider Homo =
+  filterBindingType homoFilter $ \occ _ ->
+    provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ
+
+------------------------------------------------------------------------------
+-- | A mapping from tactic commands to actual tactics for refinery.
+commandTactic :: TacticCommand -> OccName -> TacticsM ()
+commandTactic Auto     = const auto
+commandTactic Split    = const split
+commandTactic Intro    = const intro
+commandTactic Destruct = autoIfPossible . destruct
+commandTactic Homo     = autoIfPossible . homo
+
+------------------------------------------------------------------------------
+-- | 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
@@ -82,40 +143,18 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       (pos, mss, jdg) <- judgmentForHole state nfp range
       case mss of
-        -- FIXME For some reason we get an HsVar instead of an
-        -- HsUnboundVar. We should check if this is a hole somehow??
-        L span' (HsVar _ (L _ var)) -> do
+        L span' (HsUnboundVar _ _) -> do
           let resulting_range
                 = fromMaybe (error "that is not great")
                 $ toCurrentRange pos =<< srcSpanToRange span'
-          let params = TacticParams
-                { file = uri
-                , range = resulting_range
-                , var_name = T.pack $ occNameString $ occName var
-                }
-          let names = alwaysCommands
-          actions <- for names $ \name -> do
-            cmd <-
-              mkLspCommand
-                plId
-                (coerce $ name <> "Command")
-                name
-                (Just [toJSON params])
-            pure
-              $ CACodeAction
-              $ CodeAction
-                  name
-                  (Just CodeActionQuickFix)
-                  Nothing
-                  Nothing
-              $ Just cmd
-          split_actions <- mkSplits plId uri resulting_range jdg
-          homo_actions  <- mkHomos plId uri resulting_range jdg
-          pure $ Right $ List $ mconcat
-            [ actions
-            , split_actions
-            , homo_actions
-            ]
+          actions <-
+            -- This foldMap is over the function monoid.
+            foldMap commandProvider [minBound .. maxBound]
+              plId
+              uri
+              resulting_range
+              jdg
+          pure $ Right $ List actions
         _ -> pure $ Right $ codeActions []
 codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []
 
@@ -124,69 +163,43 @@ codeActions :: [CodeAction] -> List CAResult
 codeActions = List . fmap CACodeAction
 
 
-mkSplits :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
-mkSplits plId uri range (Judgement hys _) =
-  fmap join $ for (Map.toList hys) $ \(occ, CType ty) ->
-    case algebraicTyCon ty of
-      Nothing -> pure []
-      Just _ -> do
-        let name = T.pack $ occNameString occ
-        let params = TacticParams
-              { file = uri
-              , range = range
-              , var_name = name
-              }
-        cmd <-
-          mkLspCommand
-            plId
-            ("destructCommand")
-            name
-            (Just [toJSON params])
-        pure
-          $ pure
-          $ CACodeAction
-          $ CodeAction
-              ("destruct " <> name)
-              (Just CodeActionQuickFix)
-              Nothing
-              Nothing
-          $ Just cmd
-
-
-mkHomos :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
-mkHomos plId uri range (Judgement hys (CType g)) =
-  case algebraicTyCon g of
-    Nothing -> pure []
-    Just tycon ->
-      fmap join $ for (Map.toList hys) $ \(occ, CType ty) ->
-        case algebraicTyCon ty of
-          Just tycon2 | tycon == tycon2 -> do
-            let name = T.pack $ occNameString occ
-            let params = TacticParams
-                  { file = uri
-                  , range = range
-                  , var_name = name
-                  }
-            cmd <-
-              mkLspCommand
-                plId
-                ("homoCommand")
-                name
-                (Just [toJSON params])
-            pure
-              $ pure
-              $ CACodeAction
-              $ CodeAction
-                  ("homo " <> name)
-                  (Just CodeActionQuickFix)
-                  Nothing
-                  Nothing
-              $ Just cmd
-          _ -> pure []
+------------------------------------------------------------------------------
+-- | Terminal constructor for providing context-sensitive tactics. Tactics
+-- given by 'provide' are always available.
+provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider
+provide tc title name plId uri range _ = do
+  let params = TacticParams { file = uri , range = range , var_name = name }
+  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 (Map.toList hys) $ \(occ, CType ty) ->
+    case p g ty of
+      True  -> tp occ ty plId uri range jdg
+      False -> pure []
+
 
 data TacticParams = TacticParams
     { file :: J.Uri -- ^ Uri of the file to fill the hole in
@@ -196,6 +209,9 @@ data TacticParams = TacticParams
   deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON)
 
 
+------------------------------------------------------------------------------
+-- | Find the last typechecked module, and find the most specific span, as well
+-- as the judgement at the given range.
 judgmentForHole
     :: IdeState
     -> NormalizedFilePath
@@ -210,14 +226,16 @@ judgmentForHole state nfp range = do
       Just (mss@(L span' (HsVar _ (L _ v))))
         = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod)
       goal = varType v
-      hyps = hypothesisFromBindings span' $ bindings mod
-  pure (pos, mss, Judgement hyps $ CType goal)
+      binds = bindings mod
+      hyps = hypothesisFromBindings span' binds
+  pure (pos, holify binds mss, Judgement hyps $ CType goal)
 
 
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
 tacticCmd tac _lf state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       (pos, _, jdg) <- judgmentForHole state nfp range
+      hPutStrLn stderr $ intercalate "; " $ fmap (\(occ, CType ty) -> occNameString occ <> " :: " <> render unsafeGlobalDynFlags ty) $ Map.toList $ jHypothesis jdg
       pure $
         case runTactic
                 unsafeGlobalDynFlags