diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 120351e410..94fee414e2 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -5,10 +5,9 @@ module Ide.LocalBindings ( Bindings (..) , bindings , mostSpecificSpan - , isItAHole + , holify ) where -import Data.Ord import Bag import Control.Lens import Data.Data.Lens @@ -18,16 +17,16 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import Data.Monoid +import Data.Ord import Data.Set (Set) import qualified Data.Set as S -import GHC (TypecheckedModule (..), GhcTc) +import GHC (TypecheckedModule (..), GhcTc, NoExt (..)) import HsBinds import HsExpr import Id +import OccName import SrcLoc - data Bindings = Bindings { bGlobalBinds :: Set Id , bLocalBinds :: Map SrcSpan (Set Id) @@ -160,12 +159,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 diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index b277dd1ad6..01b083e105 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,10 +1,11 @@ --- | A plugin that uses tactics to synthesize code {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} +-- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic ( descriptor ) where @@ -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 diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 028947b88b..d04d86c5e3 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -74,11 +74,13 @@ data TacticError = UndefinedHypothesis OccName | GoalMismatch String CType | UnsolvedSubgoals [Judgement] + | NoProgress instance Show TacticError where show (UndefinedHypothesis name) = "undefined is not a function" show (GoalMismatch str typ) = "oh no" show (UnsolvedSubgoals jdgs) = "so sad" + show NoProgress = "No Progress" type ProvableM = ProvableT Judgement (Either TacticError) @@ -142,6 +144,12 @@ mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) mkTyName _ = "x" +------------------------------------------------------------------------------ +-- | Is this a function type? +isFunction :: Type -> Bool +isFunction (tcSplitFunTys -> ((_:_), _)) = True +isFunction _ = False + ------------------------------------------------------------------------------ -- | Is this an algebraic type? algebraicTyCon :: Type -> Maybe TyCon @@ -155,7 +163,6 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) algebraicTyCon _ = Nothing - ------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String @@ -217,6 +224,6 @@ buildDataCon hy dc apps = do (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs -render :: Outputable (LHsExpr pass) => DynFlags -> LHsExpr pass -> String +render :: Outputable a => DynFlags -> a -> String render dflags = showSDoc dflags . ppr diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index e2820cb4e2..abc78351f6 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -81,6 +81,10 @@ homo = destruct' $ \dc (Judgement hy (CType g)) -> buildDataCon hy dc (snd $ splitAppTys g) +solve :: TacticsM () -> TacticsM () +solve t = t >> throwError NoProgress + + apply :: TacticsM () apply = rule $ \(Judgement hy g) -> do case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of @@ -116,6 +120,11 @@ auto = (intro >> auto) (apply >> auto) pure () + +autoIfPossible :: TacticsM () -> TacticsM () +autoIfPossible t = (t >> solve auto) t + + one :: TacticsM () one = intro assumption split apply pure ()