Skip to content

Commit 7916fc2

Browse files
jneirajneira
authored
Merge branch 'master' into build-windows-ghcup
2 parents 1df73aa + a1e7193 commit 7916fc2

File tree

16 files changed

+220
-76
lines changed

16 files changed

+220
-76
lines changed

‎.github/workflows/nix.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ jobs:
4444
- if: ${{ needs.pre_job.outputs.should_skip_develop != 'true' }}
4545
uses: cachix/install-nix-action@v13
4646
with:
47-
install_url: https://nixos-nix-install-tests.cachix.org/serve/lb41az54kzk6j12p81br4bczary7m145/install
47+
install_url: https://nixos-nix-install-tests.cachix.org/serve/i6laym9jw3wg9mw6ncyrk6gjx4l34vvx/install
4848
install_options: '--tarball-url-prefix https://nixos-nix-install-tests.cachix.org/serve'
4949
extra_nix_config: |
5050
experimental-features = nix-command flakes
@@ -81,7 +81,7 @@ jobs:
8181
submodules: true
8282
- uses: cachix/install-nix-action@v13
8383
with:
84-
install_url: https://nixos-nix-install-tests.cachix.org/serve/lb41az54kzk6j12p81br4bczary7m145/install
84+
install_url: https://nixos-nix-install-tests.cachix.org/serve/i6laym9jw3wg9mw6ncyrk6gjx4l34vvx/install
8585
install_options: '--tarball-url-prefix https://nixos-nix-install-tests.cachix.org/serve'
8686
extra_nix_config: |
8787
experimental-features = nix-command flakes

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

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -150,16 +150,19 @@ emptyCaseScrutinees state nfp = do
150150
hscenv <- stale GhcSessionDeps
151151

152152
let scrutinees = traverse (emptyCaseQ . tcg_binds) tcg
153-
for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do
153+
fmap catMaybes $ for scrutinees $ \aged@(unTrack -> (ss, scrutinee)) -> do
154154
ty <- MaybeT
155155
. fmap (scrutinzedType <=< sequence)
156156
. traverse (typeCheck (hscEnv $ untrackedStaleValue hscenv) tcg')
157157
$ scrutinee
158-
case ss of
159-
RealSrcSpan r -> do
160-
rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
161-
pure (rss', ty)
162-
UnhelpfulSpan _ -> empty
158+
case null $ tacticsGetDataCons ty of
159+
True -> pure empty
160+
False ->
161+
case ss of
162+
RealSrcSpan r -> do
163+
rss' <- liftMaybe $ mapAgeTo tcg_map $ unsafeCopyAge aged r
164+
pure $ Just (rss', ty)
165+
UnhelpfulSpan _ -> empty
163166

164167
data EmptyCaseSort a
165168
= EmptyCase a

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ import Development.IDE.Core.RuleTypes
2222
import Development.IDE.Core.Shake (IdeState (..))
2323
import Development.IDE.Core.UseStale
2424
import Development.IDE.GHC.Compat
25-
import GhcPlugins (containsSpan, realSrcLocSpan)
25+
import GhcPlugins (containsSpan, realSrcLocSpan, realSrcSpanStart)
2626
import Ide.Types
2727
import Language.LSP.Types
2828
import Prelude hiding (span)
@@ -50,8 +50,9 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
5050
case (find (flip containsSpan (unTrack loc) . unTrack . fst) holes) of
5151
Just (trss, program) -> do
5252
let tr_range = fmap realSrcSpanToRange trss
53+
rsl = realSrcSpanStart $ unTrack trss
5354
HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
54-
z <- liftIO $ attempt_it ctx jdg $ T.unpack program
55+
z <- liftIO $ attempt_it rsl ctx jdg $ T.unpack program
5556
pure $ Hover
5657
{ _contents = HoverContents
5758
$ MarkupContent MkMarkdown

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

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Data.Bool (bool)
1717
import Data.Coerce
1818
import Data.Maybe
1919
import Data.Monoid
20+
import qualified Data.Set as S
2021
import qualified Data.Text as T
2122
import Data.Traversable
2223
import DataCon (dataConName)
@@ -32,7 +33,7 @@ import Prelude hiding (span)
3233
import Wingman.Auto
3334
import Wingman.GHC
3435
import Wingman.Judgements
35-
import Wingman.Machinery (useNameFromHypothesis)
36+
import Wingman.Machinery (useNameFromHypothesis, uncoveredDataCons)
3637
import Wingman.Metaprogramming.Parser (parseMetaprogram)
3738
import Wingman.Tactics
3839
import Wingman.Types
@@ -126,7 +127,7 @@ commandProvider DestructLambdaCase =
126127
commandProvider HomomorphismLambdaCase =
127128
requireHoleSort (== Hole) $
128129
requireExtension LambdaCase $
129-
filterGoalType ((== Just True) . lambdaCaseable) $
130+
filterGoalType (liftLambdaCase False homoFilter) $
130131
provide HomomorphismLambdaCase ""
131132
commandProvider DestructAll =
132133
requireHoleSort (== Hole) $
@@ -313,8 +314,20 @@ tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
313314
-- | We should show homos only when the goal type is the same as the binding
314315
-- type, and that both are usual algebraic types.
315316
homoFilter :: Type -> Type -> Bool
316-
homoFilter (algebraicTyCon -> Just t1) (algebraicTyCon -> Just t2) = t1 == t2
317-
homoFilter _ _ = False
317+
homoFilter codomain domain =
318+
case uncoveredDataCons domain codomain of
319+
Just s -> S.null s
320+
_ -> False
321+
322+
323+
------------------------------------------------------------------------------
324+
-- | Lift a function of (codomain, domain) over a lambda case.
325+
liftLambdaCase :: r -> (Type -> Type -> r) -> Type -> r
326+
liftLambdaCase nil f t =
327+
case tacticsSplitFunTy t of
328+
(_, _, arg : _, res) -> f res arg
329+
_ -> nil
330+
318331

319332

320333
------------------------------------------------------------------------------

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

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ import Refinery.Tactic.Internal
3232
import TcType
3333
import Type (tyCoVarsOfTypeWellScoped)
3434
import Wingman.Context (getInstance)
35-
import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst)
35+
import Wingman.GHC (tryUnifyUnivarsButNotSkolems, updateSubst, tacticsGetDataCons)
3636
import Wingman.Judgements
3737
import Wingman.Simplify (simplify)
3838
import Wingman.Types
@@ -412,3 +412,15 @@ getCurrentDefinitions = do
412412
for ctx_funcs $ \res@(occ, _) ->
413413
pure . maybe res (occ,) =<< lookupNameInContext occ
414414

415+
416+
------------------------------------------------------------------------------
417+
-- | Given two types, see if we can construct a homomorphism by mapping every
418+
-- data constructor in the domain to the same in the codomain. This function
419+
-- returns 'Just' when all the lookups succeeded, and a non-empty value if the
420+
-- homomorphism *is not* possible.
421+
uncoveredDataCons :: Type -> Type -> Maybe (S.Set (Uniquely DataCon))
422+
uncoveredDataCons domain codomain = do
423+
(g_dcs, _) <- tacticsGetDataCons codomain
424+
(hi_dcs, _) <- tacticsGetDataCons domain
425+
pure $ S.fromList (coerce hi_dcs) S.\\ S.fromList (coerce g_dcs)
426+

‎plugins/hls-tactics-plugin/src/Wingman/Metaprogramming/Parser.hs‎

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ import Wingman.Metaprogramming.Parser.Documentation
2121
import Wingman.Metaprogramming.ProofState (proofState, layout)
2222
import Wingman.Tactics
2323
import Wingman.Types
24+
import Development.IDE.GHC.Compat (RealSrcLoc, srcLocLine, srcLocCol, srcLocFile)
25+
import FastString (unpackFS)
2426

2527

2628
nullary :: T.Text -> TacticsM () -> Parser (TacticsM ())
@@ -421,17 +423,30 @@ wrapError :: String -> String
421423
wrapError err = "```\n" <> err <> "\n```\n"
422424

423425

426+
fixErrorOffset :: RealSrcLoc -> P.ParseErrorBundle a b -> P.ParseErrorBundle a b
427+
fixErrorOffset rsl (P.ParseErrorBundle ne (P.PosState a n (P.SourcePos _ line col) pos s))
428+
= P.ParseErrorBundle ne
429+
$ P.PosState a n
430+
(P.SourcePos
431+
(unpackFS $ srcLocFile rsl)
432+
((<>) line $ P.mkPos $ srcLocLine rsl - 1)
433+
((<>) col $ P.mkPos $ srcLocCol rsl - 1 + length @[] "[wingman|")
434+
)
435+
pos
436+
s
437+
424438
------------------------------------------------------------------------------
425439
-- | Attempt to run a metaprogram tactic, returning the proof state, or the
426440
-- errors.
427441
attempt_it
428-
:: Context
442+
:: RealSrcLoc
443+
-> Context
429444
-> Judgement
430445
-> String
431446
-> IO (Either String String)
432-
attempt_it ctx jdg program =
447+
attempt_it rsl ctx jdg program =
433448
case P.runParser tacticProgram "<splice>" (T.pack program) of
434-
Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty peb
449+
Left peb -> pure $ Left $ wrapError $ P.errorBundlePretty $ fixErrorOffset rsl peb
435450
Right tt -> do
436451
res <- runTactic
437452
ctx

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

Lines changed: 26 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -127,21 +127,23 @@ intros' names = rule $ \jdg -> do
127127
let g = jGoal jdg
128128
case tacticsSplitFunTy $ unCType g of
129129
(_, _, [], _) -> throwError $ GoalMismatch "intros" g
130-
(_, _, as, b) -> do
130+
(_, _, args, res) -> do
131131
ctx <- ask
132-
let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
133-
num_args = length vs
132+
let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names
133+
num_occs = length occs
134134
top_hole = isTopHole ctx jdg
135-
hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
135+
bindings = zip occs $ coerce args
136+
bound_occs = fmap fst bindings
137+
hy' = lambdaHypothesis top_hole bindings
136138
jdg' = introduce ctx hy'
137-
$ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg
139+
$ withNewGoal (CType $ mkFunTys' (drop num_occs args) res) jdg
138140
ext <- newSubgoal jdg'
139141
pure $
140142
ext
141-
& #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}")
143+
& #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show bound_occs) <> "}")
142144
. pure
143145
& #syn_scoped <>~ hy'
144-
& #syn_val %~ noLoc . lambda (fmap bvar' vs) . unLoc
146+
& #syn_val %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc
145147

146148

147149
------------------------------------------------------------------------------
@@ -198,8 +200,23 @@ destructPun hi = requireConcreteHole $ tracing "destructPun(user)" $
198200
------------------------------------------------------------------------------
199201
-- | Case split, using the same data constructor in the matches.
200202
homo :: HyInfo CType -> TacticsM ()
201-
homo = requireConcreteHole . tracing "homo" . rule . destruct' False (\dc jdg ->
202-
buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
203+
homo hi = requireConcreteHole . tracing "homo" $ do
204+
jdg <- goal
205+
let g = jGoal jdg
206+
207+
-- Ensure that every data constructor in the domain type is covered in the
208+
-- codomain; otherwise 'homo' will produce an ill-typed program.
209+
case (uncoveredDataCons (coerce $ hi_type hi) (coerce g)) of
210+
Just uncovered_dcs ->
211+
unless (S.null uncovered_dcs) $
212+
throwError $ TacticPanic "Can't cover every datacon in domain"
213+
_ -> throwError $ TacticPanic "Unable to fetch datacons"
214+
215+
rule
216+
$ destruct'
217+
False
218+
(\dc jdg -> buildDataCon False jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
219+
$ hi
203220

204221

205222
------------------------------------------------------------------------------

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

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,3 +35,81 @@ spec = do
3535
destructTest "a" 7 17 "LayoutSplitPattern"
3636
destructTest "a" 8 26 "LayoutSplitPatSyn"
3737

38+
describe "providers" $ do
39+
mkTest
40+
"Produces destruct and homomorphism code actions"
41+
"T2" 2 21
42+
[ (id, Destruct, "eab")
43+
, (id, Homomorphism, "eab")
44+
, (not, DestructPun, "eab")
45+
]
46+
47+
mkTest
48+
"Won't suggest homomorphism on the wrong type"
49+
"T2" 8 8
50+
[ (not, Homomorphism, "global")
51+
]
52+
53+
mkTest
54+
"Produces (homomorphic) lambdacase code actions"
55+
"T3" 4 24
56+
[ (id, HomomorphismLambdaCase, "")
57+
, (id, DestructLambdaCase, "")
58+
]
59+
60+
mkTest
61+
"Produces lambdacase code actions"
62+
"T3" 7 13
63+
[ (id, DestructLambdaCase, "")
64+
]
65+
66+
mkTest
67+
"Doesn't suggest lambdacase without -XLambdaCase"
68+
"T2" 11 25
69+
[ (not, DestructLambdaCase, "")
70+
]
71+
72+
mkTest
73+
"Doesn't suggest destruct if already destructed"
74+
"ProvideAlreadyDestructed" 6 18
75+
[ (not, Destruct, "x")
76+
]
77+
78+
mkTest
79+
"...but does suggest destruct if destructed in a different branch"
80+
"ProvideAlreadyDestructed" 9 7
81+
[ (id, Destruct, "x")
82+
]
83+
84+
mkTest
85+
"Doesn't suggest destruct on class methods"
86+
"ProvideLocalHyOnly" 2 12
87+
[ (not, Destruct, "mempty")
88+
]
89+
90+
mkTest
91+
"Suggests homomorphism if the domain is bigger than the codomain"
92+
"ProviderHomomorphism" 12 13
93+
[ (id, Homomorphism, "g")
94+
]
95+
96+
mkTest
97+
"Doesn't suggest homomorphism if the domain is smaller than the codomain"
98+
"ProviderHomomorphism" 15 14
99+
[ (not, Homomorphism, "g")
100+
, (id, Destruct, "g")
101+
]
102+
103+
mkTest
104+
"Suggests lambda homomorphism if the domain is bigger than the codomain"
105+
"ProviderHomomorphism" 18 14
106+
[ (id, HomomorphismLambdaCase, "")
107+
]
108+
109+
mkTest
110+
"Doesn't suggest lambda homomorphism if the domain is smaller than the codomain"
111+
"ProviderHomomorphism" 21 15
112+
[ (not, HomomorphismLambdaCase, "")
113+
, (id, DestructLambdaCase, "")
114+
]
115+

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,5 @@ spec = do
3838
metaTest 4 28 "MetaUseSymbol"
3939
metaTest 7 53 "MetaDeepOf"
4040
metaTest 2 34 "MetaWithArg"
41+
metaTest 2 12 "IntrosTooMany"
4142

‎plugins/hls-tactics-plugin/test/CodeLens/EmptyCaseSpec.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import Utils
99
spec :: Spec
1010
spec = do
1111
let test = mkCodeLensTest
12+
noTest = mkNoCodeLensTest
1213

1314
describe "golden" $ do
1415
test "EmptyCaseADT"
@@ -19,3 +20,6 @@ spec = do
1920
test "EmptyCaseGADT"
2021
test "EmptyCaseLamCase"
2122

23+
describe "no code lenses" $ do
24+
noTest "EmptyCaseSpuriousGADT"
25+

0 commit comments

Comments
 (0)