Skip to content

Commit a339902

Browse files
isovectorAilrunmergify[bot]
authored
Generate a more robust top-level binding Provenance (#1473)
* Add new variables to the extract when doing intros * Implement the correct top-level hypothesis * Implement top-level list and tuple hypotheses * Add tests to prove top level matches work now * Remove getPatName * Remove debug trace * PatCompat issues * More PatCompat woes * PatCompat is the bane of my existence * Maybe the test was wrong all along Co-authored-by: Junyoung/Clare Jang <[email protected]> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
1 parent 364960a commit a339902

File tree

8 files changed

+193
-60
lines changed

8 files changed

+193
-60
lines changed

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -250,15 +250,18 @@ lambdaCaseable _ = Nothing
250250

251251
-- It's hard to generalize over these since weird type families are involved.
252252
fromPatCompatTc :: PatCompat GhcTc -> Pat GhcTc
253+
toPatCompatTc :: Pat GhcTc -> PatCompat GhcTc
253254
fromPatCompatPs :: PatCompat GhcPs -> Pat GhcPs
254255
#if __GLASGOW_HASKELL__ == 808
255256
type PatCompat pass = Pat pass
256257
fromPatCompatTc = id
257258
fromPatCompatPs = id
259+
toPatCompatTc = id
258260
#else
259261
type PatCompat pass = LPat pass
260262
fromPatCompatTc = unLoc
261263
fromPatCompatPs = unLoc
264+
toPatCompatTc = noLoc
262265
#endif
263266

264267
------------------------------------------------------------------------------
@@ -271,22 +274,6 @@ pattern TopLevelRHS name ps body <-
271274
(GRHSs _
272275
[L _ (GRHS _ [] body)] _)
273276

274-
getPatName :: PatCompat GhcTc -> Maybe OccName
275-
getPatName (fromPatCompatTc -> p0) =
276-
case p0 of
277-
VarPat _ x -> Just $ occName $ unLoc x
278-
LazyPat _ p -> getPatName p
279-
AsPat _ x _ -> Just $ occName $ unLoc x
280-
ParPat _ p -> getPatName p
281-
BangPat _ p -> getPatName p
282-
ViewPat _ _ p -> getPatName p
283-
#if __GLASGOW_HASKELL__ >= 808
284-
SigPat _ p _ -> getPatName p
285-
#endif
286-
#if __GLASGOW_HASKELL__ == 808
287-
XPat p -> getPatName $ unLoc p
288-
#endif
289-
_ -> Nothing
290277

291278
dataConExTys :: DataCon -> [TyCoVar]
292279
#if __GLASGOW_HASKELL__ >= 808

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -210,6 +210,15 @@ jAncestryMap jdg =
210210
flip M.map (jPatHypothesis jdg) pv_ancestry
211211

212212

213+
provAncestryOf :: Provenance -> Set OccName
214+
provAncestryOf (TopLevelArgPrv o i i3) = S.singleton o
215+
provAncestryOf (PatternMatchPrv (PatVal mo so ud i)) = maybe mempty S.singleton mo <> so
216+
provAncestryOf (ClassMethodPrv uc) = mempty
217+
provAncestryOf UserPrv = mempty
218+
provAncestryOf RecursivePrv = mempty
219+
provAncestryOf (DisallowedPrv d p2) = provAncestryOf p2
220+
221+
213222
------------------------------------------------------------------------------
214223
-- TODO(sandy): THIS THING IS A BIG BIG HACK
215224
--

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

Lines changed: 168 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -1,58 +1,58 @@
1+
{-# LANGUAGE CPP #-}
12
{-# LANGUAGE FlexibleContexts #-}
23
{-# LANGUAGE GADTs #-}
34
{-# LANGUAGE LambdaCase #-}
45
{-# LANGUAGE OverloadedStrings #-}
56
{-# LANGUAGE ScopedTypeVariables #-}
7+
{-# LANGUAGE ViewPatterns #-}
8+
{-# OPTIONS_GHC -Wall #-}
69

710
module Ide.Plugin.Tactic.LanguageServer where
811

12+
import ConLike
913
import Control.Arrow
1014
import Control.Monad
15+
import Control.Monad.State (State, get, put, evalState)
1116
import Control.Monad.Trans.Maybe
12-
import Data.Aeson (Value (Object), fromJSON)
13-
import Data.Aeson.Types (Result (Error, Success))
17+
import Data.Aeson (Value (Object), fromJSON)
18+
import Data.Aeson.Types (Result (Error, Success))
1419
import Data.Coerce
15-
import Data.Functor ((<&>))
16-
import Data.Generics.Aliases (mkQ)
17-
import Data.Generics.Schemes (everything)
18-
import Data.Map (Map)
19-
import qualified Data.Map as M
20+
import Data.Functor ((<&>))
21+
import Data.Generics.Aliases (mkQ)
22+
import Data.Generics.Schemes (everything)
23+
import qualified Data.Map as M
2024
import Data.Maybe
2125
import Data.Monoid
22-
import qualified Data.Set as S
23-
import qualified Data.Text as T
26+
import qualified Data.Set as S
27+
import qualified Data.Text as T
2428
import Data.Traversable
25-
import Development.IDE (ShakeExtras,
26-
getPluginConfig)
29+
import Development.IDE (ShakeExtras, getPluginConfig)
2730
import Development.IDE.Core.PositionMapping
2831
import Development.IDE.Core.RuleTypes
29-
import Development.IDE.Core.Service (runAction)
30-
import Development.IDE.Core.Shake (IdeState (..),
31-
useWithStale)
32+
import Development.IDE.Core.Service (runAction)
33+
import Development.IDE.Core.Shake (IdeState (..), useWithStale)
3234
import Development.IDE.GHC.Compat
33-
import Development.IDE.GHC.Error (realSrcSpanToRange)
34-
import Development.IDE.Spans.LocalBindings (Bindings,
35-
getDefiningBindings)
36-
import Development.Shake (Action, RuleResult)
37-
import Development.Shake.Classes
35+
import Development.IDE.GHC.Error (realSrcSpanToRange)
36+
import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindings)
37+
import Development.Shake (Action, RuleResult)
38+
import Development.Shake.Classes (Typeable, Binary, Hashable, NFData)
3839
import qualified FastString
39-
import Ide.Plugin.Config (PluginConfig (plcConfig))
40-
import qualified Ide.Plugin.Config as Plugin
40+
import GhcPlugins (mkAppTys, tupleDataCon, consDataCon)
41+
import Ide.Plugin.Config (PluginConfig (plcConfig))
42+
import qualified Ide.Plugin.Config as Plugin
4143
import Ide.Plugin.Tactic.Context
4244
import Ide.Plugin.Tactic.FeatureSet
4345
import Ide.Plugin.Tactic.GHC
4446
import Ide.Plugin.Tactic.Judgements
4547
import Ide.Plugin.Tactic.Range
46-
import Ide.Plugin.Tactic.TestTypes (Config, TacticCommand,
47-
cfg_feature_set,
48-
emptyConfig)
48+
import Ide.Plugin.Tactic.TestTypes (TacticCommand, cfg_feature_set, emptyConfig, Config)
4949
import Ide.Plugin.Tactic.Types
50-
import Language.LSP.Server (MonadLsp)
50+
import Language.LSP.Server (MonadLsp)
5151
import Language.LSP.Types
5252
import OccName
53-
import Prelude hiding (span)
54-
import SrcLoc (containsSpan)
55-
import TcRnTypes (tcg_binds)
53+
import Prelude hiding (span)
54+
import SrcLoc (containsSpan)
55+
import TcRnTypes (tcg_binds)
5656

5757

5858
tacticDesc :: T.Text -> T.Text
@@ -179,37 +179,162 @@ liftMaybe :: Monad m => Maybe a -> MaybeT m a
179179
liftMaybe a = MaybeT $ pure a
180180

181181

182+
------------------------------------------------------------------------------
183+
-- | Combine two (possibly-overlapping) hypotheses; using the provenance from
184+
-- the first hypothesis if the bindings overlap.
182185
spliceProvenance
183-
:: Map OccName Provenance
184-
-> Hypothesis a
186+
:: Hypothesis a -- ^ Bindings to keep
187+
-> Hypothesis a -- ^ Bindings to keep if they don't overlap with the first set
185188
-> Hypothesis a
186-
spliceProvenance provs x =
187-
Hypothesis $ flip fmap (unHypothesis x) $ \hi ->
188-
overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi
189+
spliceProvenance top x =
190+
let bound = S.fromList $ fmap hi_name $ unHypothesis top
191+
in mappend top $ Hypothesis . filter (flip S.notMember bound . hi_name) $ unHypothesis x
189192

190193

191194
------------------------------------------------------------------------------
192195
-- | Compute top-level position vals of a function
193-
getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Map OccName Provenance
196+
getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Hypothesis CType
194197
getRhsPosVals rss tcs
195-
= M.fromList
196-
$ join
197-
$ maybeToList
198-
$ getFirst
199-
$ everything (<>) (mkQ mempty $ \case
198+
= everything (<>) (mkQ mempty $ \case
200199
TopLevelRHS name ps
201200
(L (RealSrcSpan span) -- body with no guards and a single defn
202201
(HsVar _ (L _ hole)))
203202
| containsSpan rss span -- which contains our span
204203
, isHole $ occName hole -- and the span is a hole
205-
-> First $ do
206-
patnames <- traverse getPatName ps
207-
pure $ zip patnames $ [0..] <&> \n ->
208-
TopLevelArgPrv name n (length patnames)
204+
-> flip evalState 0 $ buildTopLevelHypothesis name ps
209205
_ -> mempty
210206
) tcs
211207

212208

209+
------------------------------------------------------------------------------
210+
-- | Construct a hypothesis given the patterns from the left side of a HsMatch.
211+
-- These correspond to things that the user put in scope before running
212+
-- tactics.
213+
buildTopLevelHypothesis
214+
:: OccName -- ^ Function name
215+
-> [PatCompat GhcTc]
216+
-> State Int (Hypothesis CType)
217+
buildTopLevelHypothesis name ps = do
218+
fmap mconcat $
219+
for (zip [0..] ps) $ \(ix, p) ->
220+
buildPatHy (TopLevelArgPrv name ix $ length ps) p
221+
222+
223+
------------------------------------------------------------------------------
224+
-- | Construct a hypothesis for a single pattern, including building
225+
-- sub-hypotheses for constructor pattern matches.
226+
buildPatHy :: Provenance -> PatCompat GhcTc -> State Int (Hypothesis CType)
227+
buildPatHy prov (fromPatCompatTc -> p0) =
228+
case p0 of
229+
VarPat _ x -> pure $ mkIdHypothesis (unLoc x) prov
230+
LazyPat _ p -> buildPatHy prov p
231+
AsPat _ x p -> do
232+
hy' <- buildPatHy prov p
233+
pure $ mkIdHypothesis (unLoc x) prov <> hy'
234+
ParPat _ p -> buildPatHy prov p
235+
BangPat _ p -> buildPatHy prov p
236+
ViewPat _ _ p -> buildPatHy prov p
237+
-- Desugar lists into cons
238+
ListPat _ [] -> pure mempty
239+
ListPat x@(ListPatTc ty _) (p : ps) ->
240+
mkDerivedConHypothesis prov consDataCon [ty]
241+
[ (0, p)
242+
, (1, toPatCompatTc $ ListPat x ps)
243+
]
244+
-- Desugar tuples into an explicit constructor
245+
TuplePat tys pats boxity ->
246+
mkDerivedConHypothesis
247+
prov
248+
(tupleDataCon boxity $ length pats)
249+
tys
250+
$ zip [0.. ] pats
251+
ConPatOut (L _ (RealDataCon dc)) args _ _ _ f _ ->
252+
case f of
253+
PrefixCon l_pgt ->
254+
mkDerivedConHypothesis prov dc args $ zip [0..] l_pgt
255+
InfixCon pgt pgt5 ->
256+
mkDerivedConHypothesis prov dc args $ zip [0..] [pgt, pgt5]
257+
RecCon r ->
258+
mkDerivedRecordHypothesis prov dc args r
259+
#if __GLASGOW_HASKELL__ >= 808
260+
SigPat _ p _ -> buildPatHy prov p
261+
#endif
262+
#if __GLASGOW_HASKELL__ == 808
263+
XPat p -> buildPatHy prov $ unLoc p
264+
#endif
265+
_ -> pure mempty
266+
267+
268+
------------------------------------------------------------------------------
269+
-- | Like 'mkDerivedConHypothesis', but for record patterns.
270+
mkDerivedRecordHypothesis
271+
:: Provenance
272+
-> DataCon -- ^ Destructing constructor
273+
-> [Type] -- ^ Applied type variables
274+
-> HsRecFields GhcTc (PatCompat GhcTc)
275+
-> State Int (Hypothesis CType)
276+
mkDerivedRecordHypothesis prov dc args (HsRecFields (fmap unLoc -> fs) _)
277+
| Just rec_fields <- getRecordFields dc
278+
= do
279+
let field_lookup = M.fromList $ zip (fmap (occNameFS . fst) rec_fields) [0..]
280+
mkDerivedConHypothesis prov dc args $ fs <&> \(HsRecField (L _ rec_occ) p _) ->
281+
( field_lookup M.! (occNameFS $ occName $ unLoc $ rdrNameFieldOcc rec_occ)
282+
, p
283+
)
284+
mkDerivedRecordHypothesis _ _ _ _ =
285+
error "impossible! using record pattern on something that isn't a record"
286+
287+
288+
------------------------------------------------------------------------------
289+
-- | Construct a fake variable name. Used to track the provenance of top-level
290+
-- pattern matches which otherwise wouldn't have anything to attach their
291+
-- 'TopLevelArgPrv' to.
292+
mkFakeVar :: State Int OccName
293+
mkFakeVar = do
294+
i <- get
295+
put $ i + 1
296+
pure $ mkVarOcc $ "_" <> show i
297+
298+
299+
------------------------------------------------------------------------------
300+
-- | Construct a fake varible to attach the current 'Provenance' to, and then
301+
-- build a sub-hypothesis for the pattern match.
302+
mkDerivedConHypothesis
303+
:: Provenance
304+
-> DataCon -- ^ Destructing constructor
305+
-> [Type] -- ^ Applied type variables
306+
-> [(Int, PatCompat GhcTc)] -- ^ Patterns, and their order in the data con
307+
-> State Int (Hypothesis CType)
308+
mkDerivedConHypothesis prov dc args ps = do
309+
var <- mkFakeVar
310+
hy' <- fmap mconcat $
311+
for ps $ \(ix, p) -> do
312+
let prov' = PatternMatchPrv
313+
$ PatVal (Just var)
314+
(S.singleton var <> provAncestryOf prov)
315+
(Uniquely dc)
316+
ix
317+
buildPatHy prov' p
318+
pure
319+
$ mappend hy'
320+
$ Hypothesis
321+
$ pure
322+
$ HyInfo var (DisallowedPrv AlreadyDestructed prov)
323+
$ CType
324+
-- TODO(sandy): This is the completely wrong type, but we don't have a good
325+
-- way to get the real one. It's probably OK though, since we're generating
326+
-- this term with a disallowed provenance, and it doesn't actually exist
327+
-- anyway.
328+
$ mkAppTys (dataConUserType dc) args
329+
330+
331+
------------------------------------------------------------------------------
332+
-- | Build a 'Hypothesis' given an 'Id'.
333+
mkIdHypothesis :: Id -> Provenance -> Hypothesis CType
334+
mkIdHypothesis (splitId -> (name, ty)) prov =
335+
Hypothesis $ pure $ HyInfo name prov ty
336+
337+
213338
------------------------------------------------------------------------------
214339
-- | Is this hole immediately to the right of an equals sign?
215340
isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import TcType
1515
import TyCon
1616
import Type
1717
import TysWiredIn (listTyCon, pairTyCon, unitTyCon)
18+
import Ide.Plugin.Tactic.Types
1819

1920

2021
------------------------------------------------------------------------------
@@ -95,3 +96,4 @@ mkManyGoodNames in_scope args =
9596
-- | Which names are in scope?
9697
getInScope :: Map OccName a -> [OccName]
9798
getInScope = M.keys
99+

‎plugins/hls-tactics-plugin/test/GoldenSpec.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,7 @@ spec = do
9999
describe "golden" $ do
100100
destructAllTest "DestructAllAnd.hs" 2 11
101101
destructAllTest "DestructAllMany.hs" 4 23
102+
destructAllTest "DestructAllNonVarTopMatch.hs" 2 18
102103

103104

104105
-- test via:

‎plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
and :: (a, b) -> Bool -> Bool -> Bool
2+
and (a, b) x y = _
3+

‎plugins/hls-tactics-plugin/test/golden/DestructAllNonVarTopMatch.hs.expected

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
and :: (a, b) -> Bool -> Bool -> Bool
2+
and (a, b) False False = _
3+
and (a, b) True False = _
4+
and (a, b) False True = _
5+
and (a, b) True True = _
6+

‎plugins/hls-tactics-plugin/test/golden/SplitPattern.hs.expected

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,6 @@ case_split Three = _
77
case_split (Four b One) = _
88
case_split (Four b (Two i)) = _
99
case_split (Four b Three) = _
10-
case_split (Four b (Four b2 a3)) = _
10+
case_split (Four b (Four b3 a4)) = _
1111
case_split (Four b Five) = _
1212
case_split Five = _

0 commit comments

Comments
 (0)