Skip to content

Commit ba92f5f

Browse files
isovectorisovector
authored
Use ConLikes instead of DataCons (#1568)
* Use ConLikes instead of DataCons * Cleanup some imports
1 parent d9a5109 commit ba92f5f

15 files changed

+138
-70
lines changed

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

Lines changed: 36 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ module Wingman.CodeGen
99
) where
1010

1111

12+
import ConLike
1213
import Control.Lens ((%~), (<>~), (&))
1314
import Control.Monad.Except
1415
import Control.Monad.State
@@ -25,6 +26,7 @@ import GHC.SourceGen.Binds
2526
import GHC.SourceGen.Expr
2627
import GHC.SourceGen.Overloaded
2728
import GHC.SourceGen.Pat
29+
import PatSyn
2830
import Type hiding (Var)
2931
import Wingman.CodeGen.Utils
3032
import Wingman.GHC
@@ -36,7 +38,7 @@ import Wingman.Types
3638

3739

3840
destructMatches
39-
:: (DataCon -> Judgement -> Rule)
41+
:: (ConLike -> Judgement -> Rule)
4042
-- ^ How to construct each match
4143
-> Maybe OccName
4244
-- ^ Scrutinee
@@ -54,47 +56,49 @@ destructMatches f scrut t jdg = do
5456
case dcs of
5557
[] -> throwError $ GoalMismatch "destruct" g
5658
_ -> fmap unzipTrace $ for dcs $ \dc -> do
57-
let ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
59+
let con = RealDataCon dc
60+
ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
5861
-- We explicitly do not need to add the method hypothesis to
5962
-- #syn_scoped
6063
method_hy = foldMap evidenceToHypothesis ev
61-
args = dataConInstOrigArgTys' dc apps
64+
args = conLikeInstOrigArgTys' con apps
6265
modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
6366
subst <- gets ts_unifier
6467
names <- mkManyGoodNames (hyNamesInScope hy) args
65-
let hy' = patternHypothesis scrut dc jdg
68+
let hy' = patternHypothesis scrut con jdg
6669
$ zip names
6770
$ coerce args
6871
j = fmap (CType . substTyAddInScope subst . unCType)
6972
$ introduce hy'
7073
$ introduce method_hy
7174
$ withNewGoal g jdg
72-
ext <- f dc j
75+
ext <- f con j
7376
pure $ ext
7477
& #syn_trace %~ rose ("match " <> show dc <> " {" <> intercalate ", " (fmap show names) <> "}")
7578
. pure
7679
& #syn_scoped <>~ hy'
77-
& #syn_val %~ match [mkDestructPat dc names] . unLoc
80+
& #syn_val %~ match [mkDestructPat con names] . unLoc
7881

7982

8083
------------------------------------------------------------------------------
8184
-- | Produces a pattern for a data con and the names of its fields.
82-
mkDestructPat :: DataCon -> [OccName] -> Pat GhcPs
83-
mkDestructPat dcon names
84-
| isTupleDataCon dcon =
85+
mkDestructPat :: ConLike -> [OccName] -> Pat GhcPs
86+
mkDestructPat con names
87+
| RealDataCon dcon <- con
88+
, isTupleDataCon dcon =
8589
tuple pat_args
8690
| otherwise =
87-
infixifyPatIfNecessary dcon $
91+
infixifyPatIfNecessary con $
8892
conP
89-
(coerceName $ dataConName dcon)
93+
(coerceName $ conLikeName con)
9094
pat_args
9195
where
9296
pat_args = fmap bvar' names
9397

9498

95-
infixifyPatIfNecessary :: DataCon -> Pat GhcPs -> Pat GhcPs
99+
infixifyPatIfNecessary :: ConLike -> Pat GhcPs -> Pat GhcPs
96100
infixifyPatIfNecessary dcon x
97-
| dataConIsInfix dcon =
101+
| conLikeIsInfix dcon =
98102
case x of
99103
ConPatIn op (PrefixCon [lhs, rhs]) ->
100104
ConPatIn op $ InfixCon lhs rhs
@@ -113,8 +117,8 @@ unzipTrace = sequenceA
113117
--
114118
-- NOTE: The behaviour depends on GHC's 'dataConInstOrigArgTys'.
115119
-- We need some tweaks if the compiler changes the implementation.
116-
dataConInstOrigArgTys'
117-
:: DataCon
120+
conLikeInstOrigArgTys'
121+
:: ConLike
118122
-- ^ 'DataCon'structor
119123
-> [Type]
120124
-- ^ /Universally/ quantified type arguments to a result type.
@@ -123,21 +127,30 @@ dataConInstOrigArgTys'
123127
-- For example, for @MkMyGADT :: b -> MyGADT a c@, we
124128
-- must pass @[a, c]@ as this argument but not @b@, as @b@ is an existential.
125129
-> [Type]
126-
-- ^ Types of arguments to the DataCon with returned type is instantiated with the second argument.
127-
dataConInstOrigArgTys' con uniTys =
128-
let exvars = dataConExTys con
129-
in dataConInstOrigArgTys con $
130+
-- ^ Types of arguments to the ConLike with returned type is instantiated with the second argument.
131+
conLikeInstOrigArgTys' con uniTys =
132+
let exvars = conLikeExTys con
133+
in conLikeInstOrigArgTys con $
130134
uniTys ++ fmap mkTyVarTy exvars
131135
-- Rationale: At least in GHC <= 8.10, 'dataConInstOrigArgTys'
132136
-- unifies the second argument with DataCon's universals followed by existentials.
133137
-- If the definition of 'dataConInstOrigArgTys' changes,
134138
-- this place must be changed accordingly.
135139

140+
141+
conLikeExTys :: ConLike -> [TyCoVar]
142+
conLikeExTys (RealDataCon d) = dataConExTys d
143+
conLikeExTys (PatSynCon p) = patSynExTys p
144+
145+
patSynExTys :: PatSyn -> [TyCoVar]
146+
patSynExTys ps = patSynExTyVars ps
147+
148+
136149
------------------------------------------------------------------------------
137150
-- | Combinator for performing case splitting, and running sub-rules on the
138151
-- resulting matches.
139152

140-
destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
153+
destruct' :: (ConLike -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
141154
destruct' f hi jdg = do
142155
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
143156
let term = hi_name hi
@@ -156,7 +169,7 @@ destruct' f hi jdg = do
156169
------------------------------------------------------------------------------
157170
-- | Combinator for performign case splitting, and running sub-rules on the
158171
-- resulting matches.
159-
destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
172+
destructLambdaCase' :: (ConLike -> Judgement -> Rule) -> Judgement -> Rule
160173
destructLambdaCase' f jdg = do
161174
when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
162175
let g = jGoal jdg
@@ -171,11 +184,11 @@ destructLambdaCase' f jdg = do
171184
-- | Construct a data con with subgoals for each field.
172185
buildDataCon
173186
:: Judgement
174-
-> DataCon -- ^ The data con to build
187+
-> ConLike -- ^ The data con to build
175188
-> [Type] -- ^ Type arguments for the data con
176189
-> RuleM (Synthesized (LHsExpr GhcPs))
177190
buildDataCon jdg dc tyapps = do
178-
let args = dataConInstOrigArgTys' dc tyapps
191+
let args = conLikeInstOrigArgTys' dc tyapps
179192
ext
180193
<- fmap unzipTrace
181194
$ traverse ( \(arg, n) ->

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

Lines changed: 18 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
module Wingman.CodeGen.Utils where
22

3+
import ConLike (ConLike(RealDataCon), conLikeName)
34
import Data.List
45
import DataCon
56
import Development.IDE.GHC.Compat
@@ -13,25 +14,32 @@ import Wingman.GHC (getRecordFields)
1314

1415
------------------------------------------------------------------------------
1516
-- | Make a data constructor with the given arguments.
16-
mkCon :: DataCon -> [Type] -> [LHsExpr GhcPs] -> LHsExpr GhcPs
17-
mkCon dcon apps (fmap unLoc -> args)
18-
| dcon == nilDataCon
17+
mkCon :: ConLike -> [Type] -> [LHsExpr GhcPs] -> LHsExpr GhcPs
18+
mkCon con apps (fmap unLoc -> args)
19+
| RealDataCon dcon <- con
20+
, dcon == nilDataCon
1921
, [ty] <- apps
2022
, ty `eqType` charTy = noLoc $ string ""
21-
| isTupleDataCon dcon =
23+
24+
| RealDataCon dcon <- con
25+
, isTupleDataCon dcon =
2226
noLoc $ tuple args
23-
| dataConIsInfix dcon
27+
28+
| RealDataCon dcon <- con
29+
, dataConIsInfix dcon
2430
, (lhs : rhs : args') <- args =
25-
noLoc $ foldl' (@@) (op lhs (coerceName dcon_name) rhs) args'
26-
| Just fields <- getRecordFields dcon
31+
noLoc $ foldl' (@@) (op lhs (coerceName con_name) rhs) args'
32+
33+
| Just fields <- getRecordFields con
2734
, length fields >= 2 = -- record notation is unnatural on single field ctors
28-
noLoc $ recordConE (coerceName dcon_name) $ do
35+
noLoc $ recordConE (coerceName con_name) $ do
2936
(arg, (field, _)) <- zip args fields
3037
pure (coerceName field, arg)
38+
3139
| otherwise =
32-
noLoc $ foldl' (@@) (bvar' $ occName dcon_name) args
40+
noLoc $ foldl' (@@) (bvar' $ occName con_name) args
3341
where
34-
dcon_name = dataConName dcon
42+
con_name = conLikeName con
3543

3644

3745
coerceName :: HasOccName a => a -> RdrNameStr

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33

44
module Wingman.GHC where
55

6+
import ConLike
67
import Control.Monad.State
78
import Data.Function (on)
89
import Data.Functor ((<&>))
@@ -106,12 +107,12 @@ freshTyvars t = do
106107
------------------------------------------------------------------------------
107108
-- | Given a datacon, extract its record fields' names and types. Returns
108109
-- nothing if the datacon is not a record.
109-
getRecordFields :: DataCon -> Maybe [(OccName, CType)]
110+
getRecordFields :: ConLike -> Maybe [(OccName, CType)]
110111
getRecordFields dc =
111-
case dataConFieldLabels dc of
112+
case conLikeFieldLabels dc of
112113
[] -> Nothing
113114
lbls -> for lbls $ \lbl -> do
114-
(_, ty) <- dataConFieldType_maybe dc $ flLabel lbl
115+
let ty = conLikeFieldType dc $ flLabel lbl
115116
pure (mkVarOccFS $ flLabel lbl, CType ty)
116117

117118

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

Lines changed: 10 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
11
module Wingman.Judgements where
22

3+
import ConLike (ConLike)
34
import Control.Arrow
4-
import Control.Lens hiding (Context)
5+
import Control.Lens hiding (Context)
56
import Data.Bool
67
import Data.Char
78
import Data.Coerce
8-
import Data.Generics.Product (field)
9-
import Data.Map (Map)
10-
import qualified Data.Map as M
9+
import Data.Generics.Product (field)
10+
import Data.Map (Map)
11+
import qualified Data.Map as M
1112
import Data.Maybe
12-
import Data.Set (Set)
13-
import qualified Data.Set as S
14-
import DataCon (DataCon)
13+
import Data.Set (Set)
14+
import qualified Data.Set as S
1515
import Development.IDE.Spans.LocalBindings
1616
import OccName
1717
import SrcLoc
@@ -163,7 +163,7 @@ findPositionVal jdg defn pos = listToMaybe $ do
163163
------------------------------------------------------------------------------
164164
-- | Helper function for determining the ancestry list for
165165
-- 'filterSameTypeFromOtherPositions'.
166-
findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]
166+
findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName]
167167
findDconPositionVals jdg dcon pos = do
168168
(name, hi) <- M.toList $ hyByName $ jHypothesis jdg
169169
case hi_provenance hi of
@@ -178,7 +178,7 @@ findDconPositionVals jdg dcon pos = do
178178
-- given position for the datacon. Used to ensure recursive functions like
179179
-- 'fmap' preserve the relative ordering of their arguments by eliminating any
180180
-- other term which might match.
181-
filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement
181+
filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement
182182
filterSameTypeFromOtherPositions dcon pos jdg =
183183
let hy = hyByName
184184
. jHypothesis
@@ -230,7 +230,7 @@ extremelyStupid__definingFunction =
230230

231231
patternHypothesis
232232
:: Maybe OccName
233-
-> DataCon
233+
-> ConLike
234234
-> Judgement' a
235235
-> [(OccName, a)]
236236
-> Hypothesis a
@@ -369,13 +369,6 @@ 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-
379372
------------------------------------------------------------------------------
380373
-- | Is this a local function argument, pattern match or user val?
381374
isLocalHypothesis :: Provenance -> Bool

‎plugins/hls-tactics-plugin/src/Wingman/KnownStrategies/QuickCheck.hs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
module Wingman.KnownStrategies.QuickCheck where
22

3+
import ConLike (ConLike(RealDataCon))
34
import Control.Monad.Except (MonadError (throwError))
45
import Data.Bool (bool)
56
import Data.Generics (everything, mkQ)
@@ -76,7 +77,7 @@ data Generator = Generator
7677
mkGenerator :: TyCon -> [Type] -> DataCon -> Generator
7778
mkGenerator tc apps dc = do
7879
let dc_expr = var' $ occName $ dataConName dc
79-
args = dataConInstOrigArgTys' dc apps
80+
args = conLikeInstOrigArgTys' (RealDataCon dc) apps
8081
num_recursive_calls = sum $ fmap (bool 0 1 . doesTypeContain tc) args
8182
mkArbitrary = mkArbitraryCall tc num_recursive_calls
8283
Generator num_recursive_calls $ case args of

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

Lines changed: 10 additions & 10 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, substTyAddInScope)
34+
import GhcPlugins (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)
@@ -236,25 +236,25 @@ buildPatHy prov (fromPatCompatTc -> p0) =
236236
-- Desugar lists into cons
237237
ListPat _ [] -> pure mempty
238238
ListPat x@(ListPatTc ty _) (p : ps) ->
239-
mkDerivedConHypothesis prov consDataCon [ty]
239+
mkDerivedConHypothesis prov (RealDataCon consDataCon) [ty]
240240
[ (0, p)
241241
, (1, toPatCompatTc $ ListPat x ps)
242242
]
243243
-- Desugar tuples into an explicit constructor
244244
TuplePat tys pats boxity ->
245245
mkDerivedConHypothesis
246246
prov
247-
(tupleDataCon boxity $ length pats)
247+
(RealDataCon $ tupleDataCon boxity $ length pats)
248248
tys
249249
$ zip [0.. ] pats
250-
ConPatOut (L _ (RealDataCon dc)) args _ _ _ f _ ->
250+
ConPatOut (L _ con) args _ _ _ f _ ->
251251
case f of
252252
PrefixCon l_pgt ->
253-
mkDerivedConHypothesis prov dc args $ zip [0..] l_pgt
253+
mkDerivedConHypothesis prov con args $ zip [0..] l_pgt
254254
InfixCon pgt pgt5 ->
255-
mkDerivedConHypothesis prov dc args $ zip [0..] [pgt, pgt5]
255+
mkDerivedConHypothesis prov con args $ zip [0..] [pgt, pgt5]
256256
RecCon r ->
257-
mkDerivedRecordHypothesis prov dc args r
257+
mkDerivedRecordHypothesis prov con args r
258258
#if __GLASGOW_HASKELL__ >= 808
259259
SigPat _ p _ -> buildPatHy prov p
260260
#endif
@@ -268,7 +268,7 @@ buildPatHy prov (fromPatCompatTc -> p0) =
268268
-- | Like 'mkDerivedConHypothesis', but for record patterns.
269269
mkDerivedRecordHypothesis
270270
:: Provenance
271-
-> DataCon -- ^ Destructing constructor
271+
-> ConLike -- ^ Destructing constructor
272272
-> [Type] -- ^ Applied type variables
273273
-> HsRecFields GhcTc (PatCompat GhcTc)
274274
-> State Int (Hypothesis CType)
@@ -300,7 +300,7 @@ mkFakeVar = do
300300
-- build a sub-hypothesis for the pattern match.
301301
mkDerivedConHypothesis
302302
:: Provenance
303-
-> DataCon -- ^ Destructing constructor
303+
-> ConLike -- ^ Destructing constructor
304304
-> [Type] -- ^ Applied type variables
305305
-> [(Int, PatCompat GhcTc)] -- ^ Patterns, and their order in the data con
306306
-> State Int (Hypothesis CType)
@@ -324,7 +324,7 @@ mkDerivedConHypothesis prov dc args ps = do
324324
-- way to get the real one. It's probably OK though, since we're generating
325325
-- this term with a disallowed provenance, and it doesn't actually exist
326326
-- anyway.
327-
$ mkAppTys (dataConUserType dc) args
327+
$ conLikeResTy dc args
328328

329329

330330
------------------------------------------------------------------------------

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ scoreSolution ext goal holes
166166
initial_scope = hyByName $ jEntireHypothesis goal
167167
intro_vals = M.keysSet $ hyByName $ syn_scoped ext
168168
used_vals = S.intersection intro_vals $ syn_used_vals ext
169-
used_user_vals = filter (isUserProv . hi_provenance)
169+
used_user_vals = filter (isLocalHypothesis . hi_provenance)
170170
$ mapMaybe (flip M.lookup initial_scope)
171171
$ S.toList
172172
$ syn_used_vals ext

0 commit comments

Comments
 (0)