From 26df332703cafe265c56daff841613da26718355 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 7 Sep 2020 17:35:29 -0700 Subject: [PATCH 1/8] Generalized interface --- src/Ide/Plugin/Tactic.hs | 195 ++++++++++++++++++++------------------- 1 file changed, 102 insertions(+), 93 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index b277dd1ad6..3af846a53d 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -1,10 +1,11 @@ --- | A plugin that uses tactics to synthesize code {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} +-- | A plugin that uses tactics to synthesize code module Ide.Plugin.Tactic ( descriptor ) where @@ -46,33 +47,69 @@ import Type descriptor :: PluginId -> PluginDescriptor descriptor plId = (defaultPluginDescriptor plId) { pluginCommands - = fmap (\(name, tac) -> + = fmap (\tc -> PluginCommand - (coerce $ name <> "Command") - (tacticDesc name) - (tacticCmd tac)) - (Map.toList registeredCommands) + (tcCommandId tc) + (tacticDesc $ tcCommandName tc) + (tacticCmd $ commandTactic tc)) + [minBound .. maxBound] , pluginCodeActionProvider = Just codeActionProvider } tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" -registeredCommands :: Map.Map T.Text (OccName -> TacticsM ()) -registeredCommands = Map.fromList - [ ("auto", const auto) - , ("split", const split) - , ("intro", const intro) - , ("destruct", destruct) - , ("homo", homo) - ] - -alwaysCommands :: [T.Text] -alwaysCommands = - [ "auto" - , "split" - , "intro" - ] +data TacticCommand + = Auto + | Split + | Intro + | Destruct + | Homo + deriving (Eq, Ord, Show, Enum, Bounded) + +data TacticVariety + = PerHole + | PerBinding + deriving (Eq, Ord, Show, Enum, Bounded) + +tcCommandId :: TacticCommand -> CommandId +tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" + +tcCommandName :: TacticCommand -> T.Text +tcCommandName = T.pack . show + +tcCommandTitle :: TacticCommand -> OccName -> T.Text +tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ + +commandVariety :: TacticCommand -> TacticVariety +commandVariety Auto = PerHole +commandVariety Split = PerHole +commandVariety Intro = PerHole +commandVariety Destruct = PerBinding +commandVariety Homo = PerBinding + +commandTactic :: TacticCommand -> OccName -> TacticsM () +commandTactic Auto = const auto +commandTactic Split = const split +commandTactic Intro = const intro +commandTactic Destruct = destruct +commandTactic Homo = homo + +commandHoleFilter + :: TacticCommand + -> Type -- ^ goal type + -> Bool +commandHoleFilter _ _ = True + +commandBindingFilter + :: TacticCommand + -> Type -- ^ goal type + -> Type -- ^ binding type + -> Bool +commandBindingFilter Homo (algebraicTyCon -> Just t1) + (algebraicTyCon -> Just t2) = t1 == t2 +commandBindingFilter Destruct (algebraicTyCon -> Just _) _ = True +commandBindingFilter _ _ _ = False runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state @@ -84,38 +121,12 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx case mss of -- FIXME For some reason we get an HsVar instead of an -- HsUnboundVar. We should check if this is a hole somehow?? - L span' (HsVar _ (L _ var)) -> do + L span' (HsVar _ (L _ _)) -> do let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - let params = TacticParams - { file = uri - , range = resulting_range - , var_name = T.pack $ occNameString $ occName var - } - let names = alwaysCommands - actions <- for names $ \name -> do - cmd <- - mkLspCommand - plId - (coerce $ name <> "Command") - name - (Just [toJSON params]) - pure - $ CACodeAction - $ CodeAction - name - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd - split_actions <- mkSplits plId uri resulting_range jdg - homo_actions <- mkHomos plId uri resulting_range jdg - pure $ Right $ List $ mconcat - [ actions - , split_actions - , homo_actions - ] + actions <- mkTactics plId uri resulting_range jdg + pure $ Right $ List actions _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -123,13 +134,46 @@ codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction +mkTactics :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkTactics = flip foldMap [minBound .. maxBound] $ \tc -> + case commandVariety tc of + PerHole -> mkGoalTactic tc + PerBinding -> mkBindingTactic tc + -mkSplits :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkSplits plId uri range (Judgement hys _) = +mkGoalTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkGoalTactic tc plId uri range (Judgement _ (CType g)) = + case commandHoleFilter tc g of + False -> pure [] + True -> do + let params = TacticParams + { file = uri + , range = range + -- TODO(sandy): this should be Nothing + , var_name = "" + } + cmd <- + mkLspCommand + plId + (tcCommandId tc) + (tcCommandName tc) + (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction + (tcCommandName tc) + (Just CodeActionQuickFix) + Nothing + Nothing + $ Just cmd + +mkBindingTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] +mkBindingTactic tc plId uri range (Judgement hys (CType g)) = fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> - case algebraicTyCon ty of - Nothing -> pure [] - Just _ -> do + case commandBindingFilter tc g ty of + False -> pure [] + True -> do let name = T.pack $ occNameString occ let params = TacticParams { file = uri @@ -139,55 +183,20 @@ mkSplits plId uri range (Judgement hys _) = cmd <- mkLspCommand plId - ("destructCommand") - name + (tcCommandId tc) + (tcCommandTitle tc occ) (Just [toJSON params]) pure $ pure $ CACodeAction $ CodeAction - ("destruct " <> name) + (tcCommandTitle tc occ) (Just CodeActionQuickFix) Nothing Nothing $ Just cmd -mkHomos :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkHomos plId uri range (Judgement hys (CType g)) = - case algebraicTyCon g of - Nothing -> pure [] - Just tycon -> - fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> - case algebraicTyCon ty of - Just tycon2 | tycon == tycon2 -> do - let name = T.pack $ occNameString occ - let params = TacticParams - { file = uri - , range = range - , var_name = name - } - cmd <- - mkLspCommand - plId - ("homoCommand") - name - (Just [toJSON params]) - pure - $ pure - $ CACodeAction - $ CodeAction - ("homo " <> name) - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd - _ -> pure [] - - - - - data TacticParams = TacticParams { file :: J.Uri -- ^ Uri of the file to fill the hole in , range :: J.Range -- ^ The range of the hole From 7475f3fb2ec7e58ac64ee73610c406730f66bd64 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 08:56:52 -0700 Subject: [PATCH 2/8] More composable --- src/Ide/Plugin/Tactic.hs | 125 +++++++++++++------------------------ src/Ide/TacticMachinery.hs | 7 ++- 2 files changed, 51 insertions(+), 81 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 3af846a53d..4bd8ac2054 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -81,12 +81,18 @@ tcCommandName = T.pack . show tcCommandTitle :: TacticCommand -> OccName -> T.Text tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ -commandVariety :: TacticCommand -> TacticVariety -commandVariety Auto = PerHole -commandVariety Split = PerHole -commandVariety Intro = PerHole -commandVariety Destruct = PerBinding -commandVariety Homo = PerBinding +commandProvider :: TacticCommand -> TacticProvider +commandProvider Auto = provide Auto "Auto" "" +commandProvider Split = provide Split "Split" "" +commandProvider Intro = + filterGoalType isFunction $ + provide Intro "Intro" "" +commandProvider Destruct = + filterBindingType destructFilter $ \occ _ -> + provide Destruct (tcCommandTitle Destruct occ) $ T.pack $ occNameString occ +commandProvider Homo = + filterBindingType homoFilter $ \occ _ -> + provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto @@ -95,21 +101,13 @@ commandTactic Intro = const intro commandTactic Destruct = destruct commandTactic Homo = homo -commandHoleFilter - :: TacticCommand - -> Type -- ^ goal type - -> Bool -commandHoleFilter _ _ = True - -commandBindingFilter - :: TacticCommand - -> Type -- ^ goal type - -> Type -- ^ binding type - -> Bool -commandBindingFilter Homo (algebraicTyCon -> Just t1) - (algebraicTyCon -> Just t2) = t1 == t2 -commandBindingFilter Destruct (algebraicTyCon -> Just _) _ = True -commandBindingFilter _ _ _ = False +homoFilter :: Type -> Type -> Bool +homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2 +homoFilter _ _ = False + +destructFilter :: Type -> Type -> Bool +destructFilter _ (algebraicTyCon -> Just _) = True +destructFilter _ _ = False runIde :: IdeState -> Action a -> IO a runIde state = runAction "tactic" state @@ -125,7 +123,7 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - actions <- mkTactics plId uri resulting_range jdg + actions <- (foldMap commandProvider [minBound .. maxBound]) plId uri resulting_range jdg pure $ Right $ List actions _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] @@ -134,67 +132,34 @@ codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction -mkTactics :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkTactics = flip foldMap [minBound .. maxBound] $ \tc -> - case commandVariety tc of - PerHole -> mkGoalTactic tc - PerBinding -> mkBindingTactic tc - -mkGoalTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkGoalTactic tc plId uri range (Judgement _ (CType g)) = - case commandHoleFilter tc g of - False -> pure [] - True -> do - let params = TacticParams - { file = uri - , range = range - -- TODO(sandy): this should be Nothing - , var_name = "" - } - cmd <- - mkLspCommand - plId - (tcCommandId tc) - (tcCommandName tc) - (Just [toJSON params]) - pure - $ pure - $ CACodeAction - $ CodeAction - (tcCommandName tc) - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd - -mkBindingTactic :: TacticCommand -> PluginId -> Uri -> Range -> Judgement -> IO [CAResult] -mkBindingTactic tc plId uri range (Judgement hys (CType g)) = +type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] + +provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider +provide tc title name plId uri range _ = do + let params = TacticParams { file = uri , range = range , var_name = name } + cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params]) + pure + $ pure + $ CACodeAction + $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing + $ Just cmd + +filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider +filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) = + case p g of + True -> tp plId uri range jdg + False -> pure [] + +filterBindingType + :: (Type -> Type -> Bool) + -> (OccName -> Type -> TacticProvider) + -> TacticProvider +filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = fmap join $ for (Map.toList hys) $ \(occ, CType ty) -> - case commandBindingFilter tc g ty of + case p g ty of + True -> tp occ ty plId uri range jdg False -> pure [] - True -> do - let name = T.pack $ occNameString occ - let params = TacticParams - { file = uri - , range = range - , var_name = name - } - cmd <- - mkLspCommand - plId - (tcCommandId tc) - (tcCommandTitle tc occ) - (Just [toJSON params]) - pure - $ pure - $ CACodeAction - $ CodeAction - (tcCommandTitle tc occ) - (Just CodeActionQuickFix) - Nothing - Nothing - $ Just cmd data TacticParams = TacticParams diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 028947b88b..975a1b41c2 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -142,6 +142,12 @@ mkTyName (tcSplitSigmaTy-> ((_:_), _, t)) mkTyName _ = "x" +------------------------------------------------------------------------------ +-- | Is this a function type? +isFunction :: Type -> Bool +isFunction (tcSplitFunTys -> ((_:_), _)) = True +isFunction _ = False + ------------------------------------------------------------------------------ -- | Is this an algebraic type? algebraicTyCon :: Type -> Maybe TyCon @@ -155,7 +161,6 @@ algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _)) algebraicTyCon _ = Nothing - ------------------------------------------------------------------------------ -- | Get a good name for a type constructor. mkTyConName :: TyCon -> String From 42d16be9c97682cdd36d6bc0d83f543288de79a7 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 09:01:15 -0700 Subject: [PATCH 3/8] Remove TacticVariety --- src/Ide/Plugin/Tactic.hs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 4bd8ac2054..13c6fdde79 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -67,11 +67,6 @@ data TacticCommand | Homo deriving (Eq, Ord, Show, Enum, Bounded) -data TacticVariety - = PerHole - | PerBinding - deriving (Eq, Ord, Show, Enum, Bounded) - tcCommandId :: TacticCommand -> CommandId tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" From 83ef2143075c0351a0c341fb57681102bade5930 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 09:11:27 -0700 Subject: [PATCH 4/8] Haddock --- src/Ide/Plugin/Tactic.hs | 47 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 44 insertions(+), 3 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 13c6fdde79..81ad50162c 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -59,6 +59,10 @@ descriptor plId = (defaultPluginDescriptor plId) tacticDesc :: T.Text -> T.Text tacticDesc name = "fill the hole using the " <> name <> " tactic" +------------------------------------------------------------------------------ +-- | The list of tactics exposed to the outside world. These are attached to +-- actual tactics via 'commandTactic' and are contextually provided to the +-- editor via 'commandProvider'. data TacticCommand = Auto | Split @@ -67,15 +71,32 @@ data TacticCommand | Homo deriving (Eq, Ord, Show, Enum, Bounded) + +------------------------------------------------------------------------------ +-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS +-- UI. +type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] + + +------------------------------------------------------------------------------ +-- | Construct a 'CommandId' tcCommandId :: TacticCommand -> CommandId tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command" + +------------------------------------------------------------------------------ +-- | The name of the command for the LS. tcCommandName :: TacticCommand -> T.Text tcCommandName = T.pack . show +------------------------------------------------------------------------------ +-- | Construct a title for a command. tcCommandTitle :: TacticCommand -> OccName -> T.Text tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ +------------------------------------------------------------------------------ +-- | Mapping from tactic commands to their contextual providers. See 'provide', +-- 'filterGoalType' and 'filterBindingType' for the nitty gritty. commandProvider :: TacticCommand -> TacticProvider commandProvider Auto = provide Auto "Auto" "" commandProvider Split = provide Split "Split" "" @@ -89,6 +110,8 @@ commandProvider Homo = filterBindingType homoFilter $ \occ _ -> provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ +------------------------------------------------------------------------------ +-- | A mapping from tactic commands to actual tactics for refinery. commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto commandTactic Split = const split @@ -96,10 +119,16 @@ commandTactic Intro = const intro commandTactic Destruct = destruct commandTactic Homo = homo +------------------------------------------------------------------------------ +-- | We should show homos only when the goal type is the same as the binding +-- type, and that both are usual algebraic types. homoFilter :: Type -> Type -> Bool homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2 homoFilter _ _ = False +------------------------------------------------------------------------------ +-- | We should show destruct for bindings only when those bindings have usual +-- algebraic types. destructFilter :: Type -> Type -> Bool destructFilter _ (algebraicTyCon -> Just _) = True destructFilter _ _ = False @@ -128,8 +157,9 @@ codeActions :: [CodeAction] -> List CAResult codeActions = List . fmap CACodeAction -type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult] - +------------------------------------------------------------------------------ +-- | Terminal constructor for providing context-sensitive tactics. Tactics +-- given by 'provide' are always available. provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider provide tc title name plId uri range _ = do let params = TacticParams { file = uri , range = range , var_name = name } @@ -140,14 +170,22 @@ provide tc title name plId uri range _ = do $ CodeAction title (Just CodeActionQuickFix) Nothing Nothing $ Just cmd + +------------------------------------------------------------------------------ +-- | Restrict a 'TacticProvider', making sure it appears only when the given +-- predicate holds for the goal. filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) = case p g of True -> tp plId uri range jdg False -> pure [] + +------------------------------------------------------------------------------ +-- | Multiply a 'TacticProvider' for each binding, making sure it appears only +-- when the given predicate holds over the goal and binding types. filterBindingType - :: (Type -> Type -> Bool) + :: (Type -> Type -> Bool) -- ^ Goal and then binding types. -> (OccName -> Type -> TacticProvider) -> TacticProvider filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) = @@ -165,6 +203,9 @@ data TacticParams = TacticParams deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON) +------------------------------------------------------------------------------ +-- | Find the last typechecked module, and find the most specific span, as well +-- as the judgement at the given range. judgmentForHole :: IdeState -> NormalizedFilePath From 405fec271a9218c637b15214a0bde10158c1a271 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 09:12:54 -0700 Subject: [PATCH 5/8] Describe spooky monoidal behavior --- src/Ide/Plugin/Tactic.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 81ad50162c..8e89bf3259 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -147,7 +147,13 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' - actions <- (foldMap commandProvider [minBound .. maxBound]) plId uri resulting_range jdg + actions <- + -- This foldMap is over the function monoid. + foldMap commandProvider [minBound .. maxBound] + plId + uri + resulting_range + jdg pure $ Right $ List actions _ -> pure $ Right $ codeActions [] codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions [] From 964354ef9e2703a64ace64417747e5157040fa79 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 10:01:11 -0700 Subject: [PATCH 6/8] Only look at actual holes --- src/Ide/LocalBindings.hs | 28 +++++++++++++++------------- src/Ide/Plugin/Tactic.hs | 9 ++++----- 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index 120351e410..a532f4228b 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -5,10 +5,9 @@ module Ide.LocalBindings ( Bindings (..) , bindings , mostSpecificSpan - , isItAHole + , holify ) where -import Data.Ord import Bag import Control.Lens import Data.Data.Lens @@ -18,16 +17,16 @@ import Data.List import Data.Map (Map) import qualified Data.Map as M import Data.Maybe -import Data.Monoid +import Data.Ord import Data.Set (Set) import qualified Data.Set as S -import GHC (TypecheckedModule (..), GhcTc) +import GHC (TypecheckedModule (..), GhcTc, NoExt (..)) import HsBinds import HsExpr import Id +import OccName import SrcLoc - data Bindings = Bindings { bGlobalBinds :: Set Id , bLocalBinds :: Map SrcSpan (Set Id) @@ -160,12 +159,15 @@ mostSpecificSpan span z _ -> []) $ z -isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar -isItAHole tcm span = getFirst $ - everything (<>) ( - mkQ mempty $ \case - L span' (HsUnboundVar _ z :: HsExpr GhcTc) - | span == span' -> pure z - _ -> mempty - ) $ tm_typechecked_source tcm +------------------------------------------------------------------------------ +-- | Convert an HsVar back into an HsUnboundVar if it isn't actually in scope. +holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc +holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) = + case M.lookup span local of + Nothing -> v + Just binds -> + case S.member var binds of + True -> v + False -> L span $ HsUnboundVar NoExt $ TrueExprHole $ occName var +holify _ v = v diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 8e89bf3259..c3e75a538e 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -141,9 +141,7 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do (pos, mss, jdg) <- judgmentForHole state nfp range case mss of - -- FIXME For some reason we get an HsVar instead of an - -- HsUnboundVar. We should check if this is a hole somehow?? - L span' (HsVar _ (L _ _)) -> do + L span' (HsUnboundVar _ _) -> do let resulting_range = fromMaybe (error "that is not great") $ toCurrentRange pos =<< srcSpanToRange span' @@ -226,8 +224,9 @@ judgmentForHole state nfp range = do Just (mss@(L span' (HsVar _ (L _ v)))) = mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod) goal = varType v - hyps = hypothesisFromBindings span' $ bindings mod - pure (pos, mss, Judgement hyps $ CType goal) + binds = bindings mod + hyps = hypothesisFromBindings span' binds + pure (pos, holify binds mss, Judgement hyps $ CType goal) tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams From e1617bb273bdf46bbf255cec193c1df1e931d505 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 10:14:09 -0700 Subject: [PATCH 7/8] Auto if possible --- src/Ide/Plugin/Tactic.hs | 4 ++-- src/Ide/TacticMachinery.hs | 2 ++ src/Ide/Tactics.hs | 9 +++++++++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index c3e75a538e..47547e8ac9 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -116,8 +116,8 @@ commandTactic :: TacticCommand -> OccName -> TacticsM () commandTactic Auto = const auto commandTactic Split = const split commandTactic Intro = const intro -commandTactic Destruct = destruct -commandTactic Homo = homo +commandTactic Destruct = autoIfPossible . destruct +commandTactic Homo = autoIfPossible . homo ------------------------------------------------------------------------------ -- | We should show homos only when the goal type is the same as the binding diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index 975a1b41c2..f819343418 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -74,11 +74,13 @@ data TacticError = UndefinedHypothesis OccName | GoalMismatch String CType | UnsolvedSubgoals [Judgement] + | NoProgress instance Show TacticError where show (UndefinedHypothesis name) = "undefined is not a function" show (GoalMismatch str typ) = "oh no" show (UnsolvedSubgoals jdgs) = "so sad" + show NoProgress = "No Progress" type ProvableM = ProvableT Judgement (Either TacticError) diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index e2820cb4e2..a9c09b8bc1 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -81,6 +81,10 @@ homo = destruct' $ \dc (Judgement hy (CType g)) -> buildDataCon hy dc (snd $ splitAppTys g) +solve :: TacticsM () -> TacticsM () +solve t = t >> throwError NoProgress + + apply :: TacticsM () apply = rule $ \(Judgement hy g) -> do case find ((== Just g) . fmap (CType . snd) . splitFunTy_maybe . unCType . snd) $ toList hy of @@ -116,6 +120,11 @@ auto = (intro >> auto) (apply >> auto) pure () + +autoIfPossible :: TacticsM () -> TacticsM () +autoIfPossible t = t >> (solve auto pure ()) + + one :: TacticsM () one = intro assumption split apply pure () From 44528b0ee6e3d2154f8ef62c789da3534c28f0fc Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 8 Sep 2020 12:58:37 -0700 Subject: [PATCH 8/8] debugging --- src/Ide/LocalBindings.hs | 1 + src/Ide/Plugin/Tactic.hs | 3 +++ src/Ide/TacticMachinery.hs | 2 +- src/Ide/Tactics.hs | 2 +- 4 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/Ide/LocalBindings.hs b/src/Ide/LocalBindings.hs index a532f4228b..94fee414e2 100644 --- a/src/Ide/LocalBindings.hs +++ b/src/Ide/LocalBindings.hs @@ -161,6 +161,7 @@ mostSpecificSpan span z ------------------------------------------------------------------------------ -- | Convert an HsVar back into an HsUnboundVar if it isn't actually in scope. +-- TODO(sandy): this will throw away the type >:( holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) = case M.lookup span local of diff --git a/src/Ide/Plugin/Tactic.hs b/src/Ide/Plugin/Tactic.hs index 47547e8ac9..01b083e105 100644 --- a/src/Ide/Plugin/Tactic.hs +++ b/src/Ide/Plugin/Tactic.hs @@ -37,11 +37,13 @@ import Ide.LocalBindings import qualified Language.Haskell.LSP.Types as J import Language.Haskell.LSP.Types +import Data.List (intercalate) import OccName import HsExpr import GHC import DynFlags import Type +import System.IO descriptor :: PluginId -> PluginDescriptor @@ -233,6 +235,7 @@ tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams tacticCmd tac _lf state (TacticParams uri range var_name) | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do (pos, _, jdg) <- judgmentForHole state nfp range + hPutStrLn stderr $ intercalate "; " $ fmap (\(occ, CType ty) -> occNameString occ <> " :: " <> render unsafeGlobalDynFlags ty) $ Map.toList $ jHypothesis jdg pure $ case runTactic unsafeGlobalDynFlags diff --git a/src/Ide/TacticMachinery.hs b/src/Ide/TacticMachinery.hs index f819343418..d04d86c5e3 100644 --- a/src/Ide/TacticMachinery.hs +++ b/src/Ide/TacticMachinery.hs @@ -224,6 +224,6 @@ buildDataCon hy dc apps = do (HsVar NoExt $ noLoc $ Unqual $ nameOccName $ dataConName dc) $ fmap unLoc sgs -render :: Outputable (LHsExpr pass) => DynFlags -> LHsExpr pass -> String +render :: Outputable a => DynFlags -> a -> String render dflags = showSDoc dflags . ppr diff --git a/src/Ide/Tactics.hs b/src/Ide/Tactics.hs index a9c09b8bc1..abc78351f6 100644 --- a/src/Ide/Tactics.hs +++ b/src/Ide/Tactics.hs @@ -122,7 +122,7 @@ auto = (intro >> auto) autoIfPossible :: TacticsM () -> TacticsM () -autoIfPossible t = t >> (solve auto pure ()) +autoIfPossible t = (t >> solve auto) t one :: TacticsM ()