Skip to content

Commit e1fe536

Browse files
berbermanberberman
authored
Merge branch 'master' into new-import-no-exactprint
2 parents 1f84e79 + 05f25c9 commit e1fe536

24 files changed

+297
-30
lines changed

‎plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,11 @@ module Wingman.CodeGen
1111

1212
import Control.Lens ((%~), (<>~), (&))
1313
import Control.Monad.Except
14+
import Control.Monad.State
1415
import Data.Generics.Labels ()
1516
import Data.List
17+
import Data.Maybe (mapMaybe)
18+
import Data.Monoid (Endo(..))
1619
import qualified Data.Set as S
1720
import Data.Traversable
1821
import DataCon
@@ -26,6 +29,7 @@ import Type hiding (Var)
2629
import Wingman.CodeGen.Utils
2730
import Wingman.GHC
2831
import Wingman.Judgements
32+
import Wingman.Judgements.Theta
2933
import Wingman.Machinery
3034
import Wingman.Naming
3135
import Wingman.Types
@@ -50,12 +54,20 @@ destructMatches f scrut t jdg = do
5054
case dcs of
5155
[] -> throwError $ GoalMismatch "destruct" g
5256
_ -> fmap unzipTrace $ for dcs $ \dc -> do
53-
let args = dataConInstOrigArgTys' dc apps
57+
let ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
58+
-- We explicitly do not need to add the method hypothesis to
59+
-- #syn_scoped
60+
method_hy = foldMap evidenceToHypothesis ev
61+
args = dataConInstOrigArgTys' dc apps
62+
modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
63+
subst <- gets ts_unifier
5464
names <- mkManyGoodNames (hyNamesInScope hy) args
5565
let hy' = patternHypothesis scrut dc jdg
5666
$ zip names
5767
$ coerce args
58-
j = introduce hy'
68+
j = fmap (CType . substTyAddInScope subst . unCType)
69+
$ introduce hy'
70+
$ introduce method_hy
5971
$ withNewGoal g jdg
6072
ext <- f dc j
6173
pure $ ext

‎plugins/hls-tactics-plugin/src/Wingman/Judgements.hs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -369,6 +369,13 @@ isTopLevel TopLevelArgPrv{} = True
369369
isTopLevel _ = False
370370

371371

372+
------------------------------------------------------------------------------
373+
-- | Was this term defined by the user?
374+
isUserProv :: Provenance -> Bool
375+
isUserProv UserPrv{} = True
376+
isUserProv _ = False
377+
378+
372379
------------------------------------------------------------------------------
373380
-- | Is this a local function argument, pattern match or user val?
374381
isLocalHypothesis :: Provenance -> Bool

‎plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs

Lines changed: 123 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,100 @@
1+
{-# LANGUAGE CPP #-}
12
{-# LANGUAGE ViewPatterns #-}
23

34
module Wingman.Judgements.Theta
4-
( getMethodHypothesisAtHole
5+
( Evidence
6+
, getEvidenceAtHole
7+
, mkEvidence
8+
, evidenceToSubst
9+
, evidenceToHypothesis
510
) where
611

7-
import Data.Maybe (fromMaybe)
12+
import Data.Maybe (fromMaybe, mapMaybe)
813
import Data.Set (Set)
914
import qualified Data.Set as S
1015
import Development.IDE.GHC.Compat
11-
import Generics.SYB
12-
import GhcPlugins (EvVar, mkVarOcc)
16+
import Generics.SYB hiding (tyConName)
17+
import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe)
18+
#if __GLASGOW_HASKELL__ > 806
19+
import GhcPlugins (eqTyCon)
20+
#else
21+
import GhcPlugins (nameRdrName, tyConName)
22+
import PrelNames (eqTyCon_RDR)
23+
#endif
24+
import TcEvidence
25+
import TcType (tcTyConAppTyCon_maybe)
26+
import TysPrim (eqPrimTyCon)
1327
import Wingman.Machinery
1428
import Wingman.Types
1529

1630

1731
------------------------------------------------------------------------------
18-
-- | Create a 'Hypothesis' containing 'ClassMethodPrv' provenance. For every
19-
-- dictionary that is in scope at the given 'SrcSpan', find every method and
20-
-- superclass method available.
21-
getMethodHypothesisAtHole :: SrcSpan -> LHsBinds GhcTc -> Hypothesis CType
22-
getMethodHypothesisAtHole dst
23-
= Hypothesis
24-
. excludeForbiddenMethods
25-
. fromMaybe []
26-
. foldMap methodHypothesis
27-
. (everything (<>) $ mkQ mempty $ evbinds dst)
32+
-- | Something we've learned about the type environment.
33+
data Evidence
34+
-- | The two types are equal, via a @a ~ b@ relationship
35+
= EqualityOfTypes Type Type
36+
-- | We have an instance in scope
37+
| HasInstance PredType
38+
deriving (Show)
39+
40+
41+
------------------------------------------------------------------------------
42+
-- | Given a 'PredType', pull an 'Evidence' out of it.
43+
mkEvidence :: PredType -> Maybe Evidence
44+
mkEvidence (getEqualityTheta -> Just (a, b))
45+
= Just $ EqualityOfTypes a b
46+
mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (isClassTyCon -> True))
47+
= Just $ HasInstance inst
48+
mkEvidence _ = Nothing
49+
50+
51+
------------------------------------------------------------------------------
52+
-- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
53+
getEvidenceAtHole :: SrcSpan -> LHsBinds GhcTc -> [Evidence]
54+
getEvidenceAtHole dst
55+
= mapMaybe mkEvidence
56+
. (everything (<>) $
57+
mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)
58+
59+
60+
------------------------------------------------------------------------------
61+
-- | Update our knowledge of which types are equal.
62+
evidenceToSubst :: Evidence -> TacticState -> TacticState
63+
evidenceToSubst (EqualityOfTypes a b) ts =
64+
let tyvars = S.fromList $ mapMaybe getTyVar_maybe [a, b]
65+
-- If we can unify our skolems, at least one is no longer a skolem.
66+
-- Removing them from this set ensures we can get a subtitution between
67+
-- the two. But it's okay to leave them in 'ts_skolems' in general, since
68+
-- they won't exist after running this substitution.
69+
skolems = ts_skolems ts S.\\ tyvars
70+
in
71+
case tryUnifyUnivarsButNotSkolems skolems (CType a) (CType b) of
72+
Just subst -> updateSubst subst ts
73+
Nothing -> ts
74+
evidenceToSubst HasInstance{} ts = ts
75+
76+
77+
------------------------------------------------------------------------------
78+
-- | Get all of the methods that are in scope from this piece of 'Evidence'.
79+
evidenceToHypothesis :: Evidence -> Hypothesis CType
80+
evidenceToHypothesis EqualityOfTypes{} = mempty
81+
evidenceToHypothesis (HasInstance t) =
82+
Hypothesis . excludeForbiddenMethods . fromMaybe [] $ methodHypothesis t
83+
84+
85+
------------------------------------------------------------------------------
86+
-- | Given @a ~ b@ or @a ~# b@, returns @Just (a, b)@, otherwise @Nothing@.
87+
getEqualityTheta :: PredType -> Maybe (Type, Type)
88+
getEqualityTheta (splitTyConApp_maybe -> Just (tc, [_k, a, b]))
89+
#if __GLASGOW_HASKELL__ > 806
90+
| tc == eqTyCon
91+
#else
92+
| nameRdrName (tyConName tc) == eqTyCon_RDR
93+
#endif
94+
= Just (a, b)
95+
getEqualityTheta (splitTyConApp_maybe -> Just (tc, [_k1, _k2, a, b]))
96+
| tc == eqPrimTyCon = Just (a, b)
97+
getEqualityTheta _ = Nothing
2898

2999

30100
------------------------------------------------------------------------------
@@ -38,13 +108,48 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name
38108
forbiddenMethods = S.map mkVarOcc $ S.fromList
39109
[ -- monadfail
40110
"fail"
111+
-- show
112+
, "showsPrec"
113+
, "showList"
41114
]
42115

43116

44117
------------------------------------------------------------------------------
45-
-- | Extract the types of the evidence bindings in scope.
46-
evbinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
47-
evbinds dst (L src (AbsBinds _ _ h _ _ _ _))
118+
-- | Extract evidence from 'AbsBinds' in scope.
119+
absBinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
120+
absBinds dst (L src (AbsBinds _ _ h _ _ _ _))
48121
| dst `isSubspanOf` src = fmap idType h
49-
evbinds _ _ = []
122+
absBinds _ _ = []
123+
124+
125+
------------------------------------------------------------------------------
126+
-- | Extract evidence from 'HsWrapper's in scope
127+
wrapperBinds :: SrcSpan -> LHsExpr GhcTc -> [PredType]
128+
wrapperBinds dst (L src (HsWrap _ h _))
129+
| dst `isSubspanOf` src = wrapper h
130+
wrapperBinds _ _ = []
131+
132+
133+
------------------------------------------------------------------------------
134+
-- | Extract evidence from the 'ConPatOut's bound in this 'Match'.
135+
matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
136+
matchBinds dst (L src (Match _ _ pats _))
137+
| dst `isSubspanOf` src = everything (<>) (mkQ mempty patBinds) pats
138+
matchBinds _ _ = []
139+
140+
141+
------------------------------------------------------------------------------
142+
-- | Extract evidence from a 'ConPatOut'.
143+
patBinds :: Pat GhcTc -> [PredType]
144+
patBinds (ConPatOut { pat_dicts = dicts })
145+
= fmap idType dicts
146+
patBinds _ = []
147+
148+
149+
------------------------------------------------------------------------------
150+
-- | Extract the types of the evidence bindings in scope.
151+
wrapper :: HsWrapper -> [PredType]
152+
wrapper (WpCompose h h2) = wrapper h <> wrapper h2
153+
wrapper (WpEvLam v) = [idType v]
154+
wrapper _ = []
50155

‎plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ import Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
3131
import Development.Shake (Action, RuleResult)
3232
import Development.Shake.Classes (Typeable, Binary, Hashable, NFData)
3333
import qualified FastString
34-
import GhcPlugins (mkAppTys, tupleDataCon, consDataCon)
34+
import GhcPlugins (mkAppTys, tupleDataCon, consDataCon, substTyAddInScope)
3535
import Ide.Plugin.Config (PluginConfig (plcConfig))
3636
import qualified Ide.Plugin.Config as Plugin
3737
import Language.LSP.Server (MonadLsp, sendNotification)
@@ -44,7 +44,7 @@ import Wingman.Context
4444
import Wingman.FeatureSet
4545
import Wingman.GHC
4646
import Wingman.Judgements
47-
import Wingman.Judgements.Theta (getMethodHypothesisAtHole)
47+
import Wingman.Judgements.Theta
4848
import Wingman.Range
4949
import Wingman.Types
5050

@@ -143,8 +143,10 @@ mkJudgementAndContext features g binds rss tcmod = do
143143
top_provs = getRhsPosVals rss tcs
144144
local_hy = spliceProvenance top_provs
145145
$ hypothesisFromBindings rss binds
146-
cls_hy = getMethodHypothesisAtHole (RealSrcSpan rss) tcs
147-
in ( mkFirstJudgement
146+
evidence = getEvidenceAtHole (RealSrcSpan rss) tcs
147+
cls_hy = foldMap evidenceToHypothesis evidence
148+
subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
149+
in ( fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
148150
(local_hy <> cls_hy)
149151
(isRhsHole rss tcs)
150152
g

‎plugins/hls-tactics-plugin/src/Wingman/Machinery.hs

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Data.Generics (everything, gcount, mkQ)
1717
import Data.Generics.Product (field')
1818
import Data.List (sortBy)
1919
import qualified Data.Map as M
20+
import Data.Maybe (mapMaybe)
2021
import Data.Monoid (getSum)
2122
import Data.Ord (Down (..), comparing)
2223
import Data.Set (Set)
@@ -79,7 +80,7 @@ runTactic ctx jdg t =
7980
(_, fmap assoc23 -> solns) -> do
8081
let sorted =
8182
flip sortBy solns $ comparing $ \(ext, (_, holes)) ->
82-
Down $ scoreSolution ext holes
83+
Down $ scoreSolution ext jdg holes
8384
case sorted of
8485
((syn, _) : _) ->
8586
Right $
@@ -142,6 +143,7 @@ mappingExtract f (TacticT m)
142143
-- to produce the right test results.
143144
scoreSolution
144145
:: Synthesized (LHsExpr GhcPs)
146+
-> Judgement
145147
-> [Judgement]
146148
-> ( Penalize Int -- number of holes
147149
, Reward Bool -- all bindings used
@@ -151,18 +153,23 @@ scoreSolution
151153
, Penalize Int -- number of recursive calls
152154
, Penalize Int -- size of extract
153155
)
154-
scoreSolution ext holes
156+
scoreSolution ext goal holes
155157
= ( Penalize $ length holes
156158
, Reward $ S.null $ intro_vals S.\\ used_vals
157159
, Penalize $ S.size unused_top_vals
158160
, Penalize $ S.size intro_vals
159-
, Reward $ S.size used_vals
161+
, Reward $ S.size used_vals + length used_user_vals
160162
, Penalize $ getSum $ syn_recursion_count ext
161163
, Penalize $ solutionSize $ syn_val ext
162164
)
163165
where
166+
initial_scope = hyByName $ jEntireHypothesis goal
164167
intro_vals = M.keysSet $ hyByName $ syn_scoped ext
165168
used_vals = S.intersection intro_vals $ syn_used_vals ext
169+
used_user_vals = filter (isUserProv . hi_provenance)
170+
$ mapMaybe (flip M.lookup initial_scope)
171+
$ S.toList
172+
$ syn_used_vals ext
166173
top_vals = S.fromList
167174
. fmap hi_name
168175
. filter (isTopLevel . hi_provenance)
@@ -198,6 +205,10 @@ tryUnifyUnivarsButNotSkolems skolems goal inst =
198205
_ -> Nothing
199206

200207

208+
updateSubst :: TCvSubst -> TacticState -> TacticState
209+
updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) }
210+
211+
201212

202213
------------------------------------------------------------------------------
203214
-- | Attempt to unify two types.
@@ -208,7 +219,7 @@ unify goal inst = do
208219
skolems <- gets ts_skolems
209220
case tryUnifyUnivarsButNotSkolems skolems goal inst of
210221
Just subst ->
211-
modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) })
222+
modify $ updateSubst subst
212223
Nothing -> throwError (UnificationError inst goal)
213224

214225

‎plugins/hls-tactics-plugin/src/Wingman/Plugin.hs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ import Wingman.CaseSplit
3131
import Wingman.GHC
3232
import Wingman.LanguageServer
3333
import Wingman.LanguageServer.TacticProviders
34+
import Wingman.Machinery (scoreSolution)
3435
import Wingman.Range
3536
import Wingman.Tactics
3637
import Wingman.Types
@@ -136,7 +137,9 @@ mkWorkspaceEdits
136137
-> RunTacticResults
137138
-> Either UserFacingMessage WorkspaceEdit
138139
mkWorkspaceEdits span dflags ccs uri pm rtr = do
139-
for_ (rtr_other_solns rtr) $ traceMX "other solution"
140+
for_ (rtr_other_solns rtr) $ \soln -> do
141+
traceMX "other solution" soln
142+
traceMX "with score" $ scoreSolution soln (rtr_jdg rtr) []
140143
traceMX "solution" $ rtr_extract rtr
141144
let g = graftHole (RealSrcSpan span) rtr
142145
response = transform dflags ccs uri g pm

‎plugins/hls-tactics-plugin/src/Wingman/Types.hs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,9 @@ instance Show (Pat GhcPs) where
144144
instance Show (LHsSigType GhcPs) where
145145
show = unsafeRender
146146

147+
instance Show TyCon where
148+
show = unsafeRender
149+
147150

148151
------------------------------------------------------------------------------
149152
-- | The state that should be shared between subgoals. Extracts move towards

‎plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,14 +47,24 @@ spec = do
4747
autoTest 2 9 "Fgmap.hs"
4848
autoTest 4 19 "FmapJoinInLet.hs"
4949
autoTest 9 12 "AutoEndo.hs"
50-
autoTest 12 10 "AutoThetaFix.hs"
5150

5251
failing "flaky in CI" $
5352
autoTest 2 11 "GoldenApplicativeThen.hs"
5453

5554
failing "not enough auto gas" $
5655
autoTest 5 18 "GoldenFish.hs"
5756

57+
describe "theta" $ do
58+
autoTest 12 10 "AutoThetaFix.hs"
59+
autoTest 7 20 "AutoThetaRankN.hs"
60+
autoTest 6 10 "AutoThetaGADT.hs"
61+
autoTest 6 8 "AutoThetaGADTDestruct.hs"
62+
autoTest 4 8 "AutoThetaEqCtx.hs"
63+
autoTest 6 10 "AutoThetaEqGADT.hs"
64+
autoTest 6 8 "AutoThetaEqGADTDestruct.hs"
65+
autoTest 6 10 "AutoThetaRefl.hs"
66+
autoTest 6 8 "AutoThetaReflDestruct.hs"
67+
5868

5969
describe "messages" $ do
6070
mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA.hs" TacticErrors

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{-# LANGUAGE GADTs #-}
2+
3+
fun2 :: (a ~ b) => a -> b
4+
fun2 = _ -- id
5+

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{-# LANGUAGE GADTs #-}
2+
3+
fun2 :: (a ~ b) => a -> b
4+
fun2 = id -- id
5+

0 commit comments

Comments
 (0)