Skip to content

Commit 690e50f

Browse files
isovectorisovector
authored
Merge pull request #1 from isovector/general-interface
Generalized interface
2 parents 73854c7 + 44528b0 commit 690e50f

File tree

4 files changed

+165
-128
lines changed

4 files changed

+165
-128
lines changed

‎src/Ide/LocalBindings.hs

+16-13
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,9 @@ module Ide.LocalBindings
55
( Bindings (..)
66
, bindings
77
, mostSpecificSpan
8-
, isItAHole
8+
, holify
99
) where
1010

11-
import Data.Ord
1211
import Bag
1312
import Control.Lens
1413
import Data.Data.Lens
@@ -18,16 +17,16 @@ import Data.List
1817
import Data.Map (Map)
1918
import qualified Data.Map as M
2019
import Data.Maybe
21-
import Data.Monoid
20+
import Data.Ord
2221
import Data.Set (Set)
2322
import qualified Data.Set as S
24-
import GHC (TypecheckedModule (..), GhcTc)
23+
import GHC (TypecheckedModule (..), GhcTc, NoExt (..))
2524
import HsBinds
2625
import HsExpr
2726
import Id
27+
import OccName
2828
import SrcLoc
2929

30-
3130
data Bindings = Bindings
3231
{ bGlobalBinds :: Set Id
3332
, bLocalBinds :: Map SrcSpan (Set Id)
@@ -160,12 +159,16 @@ mostSpecificSpan span z
160159
_ -> [])
161160
$ z
162161

163-
isItAHole :: TypecheckedModule -> SrcSpan -> Maybe UnboundVar
164-
isItAHole tcm span = getFirst $
165-
everything (<>) (
166-
mkQ mempty $ \case
167-
L span' (HsUnboundVar _ z :: HsExpr GhcTc)
168-
| span == span' -> pure z
169-
_ -> mempty
170-
) $ tm_typechecked_source tcm
162+
------------------------------------------------------------------------------
163+
-- | Convert an HsVar back into an HsUnboundVar if it isn't actually in scope.
164+
-- TODO(sandy): this will throw away the type >:(
165+
holify :: Bindings -> LHsExpr GhcTc -> LHsExpr GhcTc
166+
holify (Bindings _ local) v@(L span (HsVar _ (L _ var))) =
167+
case M.lookup span local of
168+
Nothing -> v
169+
Just binds ->
170+
case S.member var binds of
171+
True -> v
172+
False -> L span $ HsUnboundVar NoExt $ TrueExprHole $ occName var
173+
holify _ v = v
171174

‎src/Ide/Plugin/Tactic.hs

+131-113
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
1-
-- | A plugin that uses tactics to synthesize code
21
{-# LANGUAGE DeriveAnyClass #-}
32
{-# LANGUAGE DeriveGeneric #-}
43
{-# LANGUAGE OverloadedStrings #-}
54
{-# LANGUAGE TupleSections #-}
65
{-# LANGUAGE TypeApplications #-}
6+
{-# LANGUAGE ViewPatterns #-}
77

8+
-- | A plugin that uses tactics to synthesize code
89
module Ide.Plugin.Tactic
910
( descriptor
1011
) where
@@ -36,43 +37,103 @@ import Ide.LocalBindings
3637
import qualified Language.Haskell.LSP.Types as J
3738
import Language.Haskell.LSP.Types
3839

40+
import Data.List (intercalate)
3941
import OccName
4042
import HsExpr
4143
import GHC
4244
import DynFlags
4345
import Type
46+
import System.IO
4447

4548

4649
descriptor :: PluginId -> PluginDescriptor
4750
descriptor plId = (defaultPluginDescriptor plId)
4851
{ pluginCommands
49-
= fmap (\(name, tac) ->
52+
= fmap (\tc ->
5053
PluginCommand
51-
(coerce $ name <> "Command")
52-
(tacticDesc name)
53-
(tacticCmd tac))
54-
(Map.toList registeredCommands)
54+
(tcCommandId tc)
55+
(tacticDesc $ tcCommandName tc)
56+
(tacticCmd $ commandTactic tc))
57+
[minBound .. maxBound]
5558
, pluginCodeActionProvider = Just codeActionProvider
5659
}
5760

5861
tacticDesc :: T.Text -> T.Text
5962
tacticDesc name = "fill the hole using the " <> name <> " tactic"
6063

61-
registeredCommands :: Map.Map T.Text (OccName -> TacticsM ())
62-
registeredCommands = Map.fromList
63-
[ ("auto", const auto)
64-
, ("split", const split)
65-
, ("intro", const intro)
66-
, ("destruct", destruct)
67-
, ("homo", homo)
68-
]
69-
70-
alwaysCommands :: [T.Text]
71-
alwaysCommands =
72-
[ "auto"
73-
, "split"
74-
, "intro"
75-
]
64+
------------------------------------------------------------------------------
65+
-- | The list of tactics exposed to the outside world. These are attached to
66+
-- actual tactics via 'commandTactic' and are contextually provided to the
67+
-- editor via 'commandProvider'.
68+
data TacticCommand
69+
= Auto
70+
| Split
71+
| Intro
72+
| Destruct
73+
| Homo
74+
deriving (Eq, Ord, Show, Enum, Bounded)
75+
76+
77+
------------------------------------------------------------------------------
78+
-- | A 'TacticProvider' is a way of giving context-sensitive actions to the LS
79+
-- UI.
80+
type TacticProvider = PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
81+
82+
83+
------------------------------------------------------------------------------
84+
-- | Construct a 'CommandId'
85+
tcCommandId :: TacticCommand -> CommandId
86+
tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
87+
88+
89+
------------------------------------------------------------------------------
90+
-- | The name of the command for the LS.
91+
tcCommandName :: TacticCommand -> T.Text
92+
tcCommandName = T.pack . show
93+
94+
------------------------------------------------------------------------------
95+
-- | Construct a title for a command.
96+
tcCommandTitle :: TacticCommand -> OccName -> T.Text
97+
tcCommandTitle tc occ = T.pack $ show tc <> " " <> occNameString occ
98+
99+
------------------------------------------------------------------------------
100+
-- | Mapping from tactic commands to their contextual providers. See 'provide',
101+
-- 'filterGoalType' and 'filterBindingType' for the nitty gritty.
102+
commandProvider :: TacticCommand -> TacticProvider
103+
commandProvider Auto = provide Auto "Auto" ""
104+
commandProvider Split = provide Split "Split" ""
105+
commandProvider Intro =
106+
filterGoalType isFunction $
107+
provide Intro "Intro" ""
108+
commandProvider Destruct =
109+
filterBindingType destructFilter $ \occ _ ->
110+
provide Destruct (tcCommandTitle Destruct occ) $ T.pack $ occNameString occ
111+
commandProvider Homo =
112+
filterBindingType homoFilter $ \occ _ ->
113+
provide Homo (tcCommandTitle Homo occ) $ T.pack $ occNameString occ
114+
115+
------------------------------------------------------------------------------
116+
-- | A mapping from tactic commands to actual tactics for refinery.
117+
commandTactic :: TacticCommand -> OccName -> TacticsM ()
118+
commandTactic Auto = const auto
119+
commandTactic Split = const split
120+
commandTactic Intro = const intro
121+
commandTactic Destruct = autoIfPossible . destruct
122+
commandTactic Homo = autoIfPossible . homo
123+
124+
------------------------------------------------------------------------------
125+
-- | We should show homos only when the goal type is the same as the binding
126+
-- type, and that both are usual algebraic types.
127+
homoFilter :: Type -> Type -> Bool
128+
homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
129+
homoFilter _ _ = False
130+
131+
------------------------------------------------------------------------------
132+
-- | We should show destruct for bindings only when those bindings have usual
133+
-- algebraic types.
134+
destructFilter :: Type -> Type -> Bool
135+
destructFilter _ (algebraicTyCon -> Just _) = True
136+
destructFilter _ _ = False
76137

77138
runIde :: IdeState -> Action a -> IO a
78139
runIde state = runAction "tactic" state
@@ -82,40 +143,18 @@ codeActionProvider _conf state plId (TextDocumentIdentifier uri) range _ctx
82143
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
83144
(pos, mss, jdg) <- judgmentForHole state nfp range
84145
case mss of
85-
-- FIXME For some reason we get an HsVar instead of an
86-
-- HsUnboundVar. We should check if this is a hole somehow??
87-
L span' (HsVar _ (L _ var)) -> do
146+
L span' (HsUnboundVar _ _) -> do
88147
let resulting_range
89148
= fromMaybe (error "that is not great")
90149
$ toCurrentRange pos =<< srcSpanToRange span'
91-
let params = TacticParams
92-
{ file = uri
93-
, range = resulting_range
94-
, var_name = T.pack $ occNameString $ occName var
95-
}
96-
let names = alwaysCommands
97-
actions <- for names $ \name -> do
98-
cmd <-
99-
mkLspCommand
100-
plId
101-
(coerce $ name <> "Command")
102-
name
103-
(Just [toJSON params])
104-
pure
105-
$ CACodeAction
106-
$ CodeAction
107-
name
108-
(Just CodeActionQuickFix)
109-
Nothing
110-
Nothing
111-
$ Just cmd
112-
split_actions <- mkSplits plId uri resulting_range jdg
113-
homo_actions <- mkHomos plId uri resulting_range jdg
114-
pure $ Right $ List $ mconcat
115-
[ actions
116-
, split_actions
117-
, homo_actions
118-
]
150+
actions <-
151+
-- This foldMap is over the function monoid.
152+
foldMap commandProvider [minBound .. maxBound]
153+
plId
154+
uri
155+
resulting_range
156+
jdg
157+
pure $ Right $ List actions
119158
_ -> pure $ Right $ codeActions []
120159
codeActionProvider _ _ _ _ _ _ = pure $ Right $ codeActions []
121160

@@ -124,69 +163,43 @@ codeActions :: [CodeAction] -> List CAResult
124163
codeActions = List . fmap CACodeAction
125164

126165

127-
mkSplits :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
128-
mkSplits plId uri range (Judgement hys _) =
129-
fmap join $ for (Map.toList hys) $ \(occ, CType ty) ->
130-
case algebraicTyCon ty of
131-
Nothing -> pure []
132-
Just _ -> do
133-
let name = T.pack $ occNameString occ
134-
let params = TacticParams
135-
{ file = uri
136-
, range = range
137-
, var_name = name
138-
}
139-
cmd <-
140-
mkLspCommand
141-
plId
142-
("destructCommand")
143-
name
144-
(Just [toJSON params])
145-
pure
146-
$ pure
147-
$ CACodeAction
148-
$ CodeAction
149-
("destruct " <> name)
150-
(Just CodeActionQuickFix)
151-
Nothing
152-
Nothing
153-
$ Just cmd
154-
155-
156-
mkHomos :: PluginId -> Uri -> Range -> Judgement -> IO [CAResult]
157-
mkHomos plId uri range (Judgement hys (CType g)) =
158-
case algebraicTyCon g of
159-
Nothing -> pure []
160-
Just tycon ->
161-
fmap join $ for (Map.toList hys) $ \(occ, CType ty) ->
162-
case algebraicTyCon ty of
163-
Just tycon2 | tycon == tycon2 -> do
164-
let name = T.pack $ occNameString occ
165-
let params = TacticParams
166-
{ file = uri
167-
, range = range
168-
, var_name = name
169-
}
170-
cmd <-
171-
mkLspCommand
172-
plId
173-
("homoCommand")
174-
name
175-
(Just [toJSON params])
176-
pure
177-
$ pure
178-
$ CACodeAction
179-
$ CodeAction
180-
("homo " <> name)
181-
(Just CodeActionQuickFix)
182-
Nothing
183-
Nothing
184-
$ Just cmd
185-
_ -> pure []
166+
------------------------------------------------------------------------------
167+
-- | Terminal constructor for providing context-sensitive tactics. Tactics
168+
-- given by 'provide' are always available.
169+
provide :: TacticCommand -> T.Text -> T.Text -> TacticProvider
170+
provide tc title name plId uri range _ = do
171+
let params = TacticParams { file = uri , range = range , var_name = name }
172+
cmd <- mkLspCommand plId (tcCommandId tc) title (Just [toJSON params])
173+
pure
174+
$ pure
175+
$ CACodeAction
176+
$ CodeAction title (Just CodeActionQuickFix) Nothing Nothing
177+
$ Just cmd
186178

187179

180+
------------------------------------------------------------------------------
181+
-- | Restrict a 'TacticProvider', making sure it appears only when the given
182+
-- predicate holds for the goal.
183+
filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
184+
filterGoalType p tp plId uri range jdg@(Judgement _ (CType g)) =
185+
case p g of
186+
True -> tp plId uri range jdg
187+
False -> pure []
188188

189189

190+
------------------------------------------------------------------------------
191+
-- | Multiply a 'TacticProvider' for each binding, making sure it appears only
192+
-- when the given predicate holds over the goal and binding types.
193+
filterBindingType
194+
:: (Type -> Type -> Bool) -- ^ Goal and then binding types.
195+
-> (OccName -> Type -> TacticProvider)
196+
-> TacticProvider
197+
filterBindingType p tp plId uri range jdg@(Judgement hys (CType g)) =
198+
fmap join $ for (Map.toList hys) $ \(occ, CType ty) ->
199+
case p g ty of
200+
True -> tp occ ty plId uri range jdg
201+
False -> pure []
202+
190203

191204
data TacticParams = TacticParams
192205
{ file :: J.Uri -- ^ Uri of the file to fill the hole in
@@ -196,6 +209,9 @@ data TacticParams = TacticParams
196209
deriving (Show, Eq, Generics.Generic, ToJSON, FromJSON)
197210

198211

212+
------------------------------------------------------------------------------
213+
-- | Find the last typechecked module, and find the most specific span, as well
214+
-- as the judgement at the given range.
199215
judgmentForHole
200216
:: IdeState
201217
-> NormalizedFilePath
@@ -210,14 +226,16 @@ judgmentForHole state nfp range = do
210226
Just (mss@(L span' (HsVar _ (L _ v))))
211227
= mostSpecificSpan @_ @GhcTc span (tm_typechecked_source mod)
212228
goal = varType v
213-
hyps = hypothesisFromBindings span' $ bindings mod
214-
pure (pos, mss, Judgement hyps $ CType goal)
229+
binds = bindings mod
230+
hyps = hypothesisFromBindings span' binds
231+
pure (pos, holify binds mss, Judgement hyps $ CType goal)
215232

216233

217234
tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction TacticParams
218235
tacticCmd tac _lf state (TacticParams uri range var_name)
219236
| Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
220237
(pos, _, jdg) <- judgmentForHole state nfp range
238+
hPutStrLn stderr $ intercalate "; " $ fmap (\(occ, CType ty) -> occNameString occ <> " :: " <> render unsafeGlobalDynFlags ty) $ Map.toList $ jHypothesis jdg
221239
pure $
222240
case runTactic
223241
unsafeGlobalDynFlags

0 commit comments

Comments
 (0)