| ... |
... |
@@ -30,6 +30,7 @@ |
|
30
|
30
|
module GHC.HsToCore.Pmc (
|
|
31
|
31
|
-- Checking and printing
|
|
32
|
32
|
pmcPatBind, pmcMatches, pmcGRHSs, pmcRecSel,
|
|
|
33
|
+ initNablasMatches,
|
|
33
|
34
|
isMatchContextPmChecked, isMatchContextPmChecked_SinglePat,
|
|
34
|
35
|
|
|
35
|
36
|
-- See Note [Long-distance information]
|
| ... |
... |
@@ -45,6 +46,7 @@ import GHC.HsToCore.Pmc.Utils |
|
45
|
46
|
import GHC.HsToCore.Pmc.Desugar
|
|
46
|
47
|
import GHC.HsToCore.Pmc.Check
|
|
47
|
48
|
import GHC.HsToCore.Pmc.Solver
|
|
|
49
|
+import GHC.HsToCore.Types
|
|
48
|
50
|
import GHC.Types.Basic (Origin(..), isDoExpansionGenerated)
|
|
49
|
51
|
import GHC.Core
|
|
50
|
52
|
import GHC.Driver.DynFlags
|
| ... |
... |
@@ -77,26 +79,35 @@ import GHC.Tc.Utils.Monad |
|
77
|
79
|
-- capturing long-distance information, or the trivially habitable 'Nablas' if
|
|
78
|
80
|
-- the former is uninhabited.
|
|
79
|
81
|
-- See Note [Recovering from unsatisfiable pattern-matching constraints].
|
|
80
|
|
-getLdiNablas :: DsM Nablas
|
|
|
82
|
+getLdiNablas :: DsM LdiNablas
|
|
81
|
83
|
getLdiNablas = do
|
|
82
|
84
|
nablas <- getPmNablas
|
|
83
|
|
- isInhabited nablas >>= \case
|
|
84
|
|
- True -> pure nablas
|
|
85
|
|
- False -> pure initNablas
|
|
|
85
|
+ case nablas of
|
|
|
86
|
+ NoPmc -> pure NoPmc
|
|
|
87
|
+ Ldi nablas -> isInhabited nablas >>= \case
|
|
|
88
|
+ True -> pure (Ldi nablas)
|
|
|
89
|
+ False -> pure (Ldi initNablas)
|
|
86
|
90
|
|
|
87
|
91
|
-- | We need to call the Hs desugarer to get the Core of a let-binding or where
|
|
88
|
92
|
-- clause. We don't want to run the coverage checker when doing so! Efficiency
|
|
89
|
93
|
-- is one concern, but also a lack of properly set up long-distance information
|
|
90
|
94
|
-- might trigger warnings that we normally wouldn't emit.
|
|
91
|
|
-noCheckDs :: DsM a -> DsM a
|
|
92
|
|
-noCheckDs = updTopFlags (\dflags -> foldl' wopt_unset dflags allPmCheckWarnings)
|
|
|
95
|
+dontDoPmc :: DsM a -> DsM a
|
|
|
96
|
+dontDoPmc thing_inside = updPmNablas NoPmc thing_inside
|
|
|
97
|
+
|
|
|
98
|
+whenDoingPmc :: a -> (Nablas -> DsM a) -> DsM a
|
|
|
99
|
+whenDoingPmc no_pmc thing_inside
|
|
|
100
|
+ = do { ldi_nablas <- getPmNablas
|
|
|
101
|
+ ; case ldi_nablas of
|
|
|
102
|
+ NoPmc -> return no_pmc
|
|
|
103
|
+ Ldi nablas -> thing_inside nablas }
|
|
93
|
104
|
|
|
94
|
105
|
-- | Check a pattern binding (let, where) for exhaustiveness.
|
|
95
|
|
-pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM Nablas
|
|
|
106
|
+pmcPatBind :: DsMatchContext -> Id -> Pat GhcTc -> DsM LdiNablas
|
|
96
|
107
|
pmcPatBind ctxt@(DsMatchContext match_ctxt loc) var p
|
|
97
|
|
- = mb_discard_warnings $ do
|
|
98
|
|
- !missing <- getLdiNablas
|
|
99
|
|
- pat_bind <- noCheckDs $ desugarPatBind loc var p
|
|
|
108
|
+ = whenDoingPmc NoPmc $ \ !missing ->
|
|
|
109
|
+ mb_discard_warnings $ do
|
|
|
110
|
+ pat_bind <- dontDoPmc $ desugarPatBind loc var p
|
|
100
|
111
|
tracePm "pmcPatBind {" (vcat [ppr ctxt, ppr var, ppr p, ppr pat_bind, ppr missing])
|
|
101
|
112
|
result <- unCA (checkPatBind pat_bind) missing
|
|
102
|
113
|
let ldi = ldiGRHS $ ( \ pb -> case pb of PmPatBind grhs -> grhs) $ cr_ret result
|
| ... |
... |
@@ -124,21 +135,21 @@ pmcPatBind ctxt@(DsMatchContext match_ctxt loc) var p |
|
124
|
135
|
pmcGRHSs
|
|
125
|
136
|
:: HsMatchContextRn -- ^ Match context, for warning messages
|
|
126
|
137
|
-> GRHSs GhcTc (LHsExpr GhcTc) -- ^ The GRHSs to check
|
|
127
|
|
- -> DsM (NonEmpty Nablas) -- ^ Covered 'Nablas' for each RHS, for long
|
|
128
|
|
- -- distance info
|
|
129
|
|
-pmcGRHSs hs_ctxt guards@(GRHSs _ grhss _) = do
|
|
130
|
|
- let combined_loc = foldl1 combineSrcSpans (NE.map getLocA grhss)
|
|
131
|
|
- ctxt = DsMatchContext hs_ctxt combined_loc
|
|
132
|
|
- !missing <- getLdiNablas
|
|
133
|
|
- matches <- noCheckDs $ desugarGRHSs combined_loc empty guards
|
|
134
|
|
- tracePm "pmcGRHSs" (hang (vcat [ppr ctxt
|
|
135
|
|
- , text "Guards:"])
|
|
136
|
|
- 2
|
|
137
|
|
- (pprGRHSs hs_ctxt guards $$ ppr missing))
|
|
138
|
|
- result <- unCA (checkGRHSs matches) missing
|
|
139
|
|
- tracePm "}: " (ppr (cr_uncov result))
|
|
140
|
|
- formatReportWarnings ReportGRHSs ctxt [] result
|
|
141
|
|
- return (ldiGRHSs (cr_ret result))
|
|
|
138
|
+ -> DsM (NonEmpty LdiNablas) -- ^ Covered 'Nablas' for each RHS,
|
|
|
139
|
+ -- for long distance info
|
|
|
140
|
+pmcGRHSs hs_ctxt guards@(GRHSs _ grhss _) =
|
|
|
141
|
+ whenDoingPmc (NE.map (const NoPmc) grhss) $ \ !missing -> do
|
|
|
142
|
+ let combined_loc = foldl1 combineSrcSpans (NE.map getLocA grhss)
|
|
|
143
|
+ ctxt = DsMatchContext hs_ctxt combined_loc
|
|
|
144
|
+ matches <- dontDoPmc $ desugarGRHSs combined_loc empty guards
|
|
|
145
|
+ tracePm "pmcGRHSs" (hang (vcat [ppr ctxt
|
|
|
146
|
+ , text "Guards:"])
|
|
|
147
|
+ 2
|
|
|
148
|
+ (pprGRHSs hs_ctxt guards $$ ppr missing))
|
|
|
149
|
+ result <- unCA (checkGRHSs matches) missing
|
|
|
150
|
+ tracePm "}: " (ppr (cr_uncov result))
|
|
|
151
|
+ formatReportWarnings ReportGRHSs ctxt [] result
|
|
|
152
|
+ return (ldiGRHSs (cr_ret result))
|
|
142
|
153
|
|
|
143
|
154
|
-- | Check a list of syntactic 'Match'es (part of case, functions, etc.), each
|
|
144
|
155
|
-- with a 'Pat' and one or more 'GRHSs':
|
| ... |
... |
@@ -160,37 +171,44 @@ pmcMatches |
|
160
|
171
|
-> DsMatchContext -- ^ Match context, for warnings messages
|
|
161
|
172
|
-> [Id] -- ^ Match variables, i.e. x and y above
|
|
162
|
173
|
-> [LMatch GhcTc (LHsExpr GhcTc)] -- ^ List of matches
|
|
163
|
|
- -> DsM [(Nablas, NonEmpty Nablas)] -- ^ One covered 'Nablas' per Match and
|
|
164
|
|
- -- GRHS, for long distance info.
|
|
165
|
|
-pmcMatches origin ctxt vars matches = {-# SCC "pmcMatches" #-} do
|
|
166
|
|
- -- We have to force @missing@ before printing out the trace message,
|
|
167
|
|
- -- otherwise we get interleaved output from the solver. This function
|
|
168
|
|
- -- should be strict in @missing@ anyway!
|
|
169
|
|
- !missing <- getLdiNablas
|
|
170
|
|
- tracePm "pmcMatches {" $
|
|
171
|
|
- hang (vcat [ppr origin, ppr ctxt, ppr vars, text "Matches:"])
|
|
172
|
|
- 2
|
|
173
|
|
- ((ppr matches) $$ (text "missing:" <+> ppr missing))
|
|
174
|
|
- case NE.nonEmpty matches of
|
|
175
|
|
- Nothing -> do
|
|
176
|
|
- -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
|
|
177
|
|
- let var = only vars
|
|
178
|
|
- empty_case <- noCheckDs $ desugarEmptyCase var
|
|
179
|
|
- result <- unCA (checkEmptyCase empty_case) missing
|
|
180
|
|
- tracePm "}: " (ppr (cr_uncov result))
|
|
181
|
|
- formatReportWarnings ReportEmptyCase ctxt vars result
|
|
182
|
|
- return []
|
|
183
|
|
- Just matches -> do
|
|
184
|
|
- matches <- {-# SCC "desugarMatches" #-}
|
|
185
|
|
- noCheckDs $ desugarMatches vars matches
|
|
186
|
|
- tracePm "desugared matches" (ppr matches)
|
|
187
|
|
- result <- {-# SCC "checkMatchGroup" #-}
|
|
188
|
|
- unCA (checkMatchGroup matches) missing
|
|
189
|
|
- tracePm "}: " (ppr (cr_uncov result))
|
|
190
|
|
- unless (isDoExpansionGenerated origin) -- Do expansion generated code shouldn't emit overlapping warnings
|
|
191
|
|
- ({-# SCC "formatReportWarnings" #-}
|
|
192
|
|
- formatReportWarnings ReportMatchGroup ctxt vars result)
|
|
193
|
|
- return (NE.toList (ldiMatchGroup (cr_ret result)))
|
|
|
174
|
+ -> DsM [(LdiNablas, NonEmpty LdiNablas)] -- ^ One covered 'Nablas' per Match and
|
|
|
175
|
+ -- GRHS, for long distance info.
|
|
|
176
|
+pmcMatches origin ctxt vars matches = {-# SCC "pmcMatches" #-}
|
|
|
177
|
+ whenDoingPmc (initNablasMatches NoPmc matches) $ \ !missing -> do
|
|
|
178
|
+ -- We have to force @missing@ before printing out the trace message,
|
|
|
179
|
+ -- otherwise we get interleaved output from the solver. This function
|
|
|
180
|
+ -- should be strict in @missing@ anyway!
|
|
|
181
|
+ tracePm "pmcMatches {" $
|
|
|
182
|
+ hang (vcat [ppr origin, ppr ctxt, ppr vars, text "Matches:"])
|
|
|
183
|
+ 2
|
|
|
184
|
+ ((ppr matches) $$ (text "missing:" <+> ppr missing))
|
|
|
185
|
+ case NE.nonEmpty matches of
|
|
|
186
|
+ Nothing -> do
|
|
|
187
|
+ -- This must be an -XEmptyCase. See Note [Checking EmptyCase]
|
|
|
188
|
+ let var = only vars
|
|
|
189
|
+ empty_case <- dontDoPmc $ desugarEmptyCase var
|
|
|
190
|
+ result <- unCA (checkEmptyCase empty_case) missing
|
|
|
191
|
+ tracePm "}: " (ppr (cr_uncov result))
|
|
|
192
|
+ formatReportWarnings ReportEmptyCase ctxt vars result
|
|
|
193
|
+ return []
|
|
|
194
|
+ Just matches -> do
|
|
|
195
|
+ matches <- {-# SCC "desugarMatches" #-}
|
|
|
196
|
+ dontDoPmc $ desugarMatches vars matches
|
|
|
197
|
+ tracePm "desugared matches" (ppr matches)
|
|
|
198
|
+ result <- {-# SCC "checkMatchGroup" #-}
|
|
|
199
|
+ unCA (checkMatchGroup matches) missing
|
|
|
200
|
+ tracePm "}: " (ppr (cr_uncov result))
|
|
|
201
|
+ unless (isDoExpansionGenerated origin) -- Do expansion generated code shouldn't emit overlapping warnings
|
|
|
202
|
+ ({-# SCC "formatReportWarnings" #-}
|
|
|
203
|
+ formatReportWarnings ReportMatchGroup ctxt vars result)
|
|
|
204
|
+ return (NE.toList (ldiMatchGroup (cr_ret result)))
|
|
|
205
|
+
|
|
|
206
|
+initNablasMatches :: LdiNablas -> [LMatch GhcTc b] -> [(LdiNablas, NonEmpty LdiNablas)]
|
|
|
207
|
+initNablasMatches ldi_nablas ms
|
|
|
208
|
+ = map (\(L _ m) -> (ldi_nablas, initNablasGRHSs ldi_nablas (m_grhss m))) ms
|
|
|
209
|
+ where
|
|
|
210
|
+ initNablasGRHSs :: LdiNablas -> GRHSs GhcTc b -> NonEmpty LdiNablas
|
|
|
211
|
+ initNablasGRHSs ldi_nablas m = NE.map (const ldi_nablas) (grhssGRHSs m)
|
|
194
|
212
|
|
|
195
|
213
|
{-
|
|
196
|
214
|
Note [Detecting incomplete record selectors]
|
| ... |
... |
@@ -361,9 +379,8 @@ pmcRecSel sel_id arg |
|
361
|
379
|
| RecSelId{ sel_cons = rec_sel_info } <- idDetails sel_id
|
|
362
|
380
|
, RSI { rsi_def = cons_w_field, rsi_undef = cons_wo_field } <- rec_sel_info
|
|
363
|
381
|
, not (null cons_wo_field)
|
|
364
|
|
- = do { !missing <- getLdiNablas
|
|
365
|
|
-
|
|
366
|
|
- ; tracePm "pmcRecSel {" (ppr sel_id)
|
|
|
382
|
+ = whenDoingPmc () $ \ !missing ->
|
|
|
383
|
+ do { tracePm "pmcRecSel {" (ppr sel_id)
|
|
367
|
384
|
; CheckResult{ cr_ret = PmRecSel{ pr_arg_var = arg_id }, cr_uncov = uncov_nablas }
|
|
368
|
385
|
<- unCA (checkRecSel (PmRecSel () arg cons_w_field)) missing
|
|
369
|
386
|
; tracePm "}: " $ ppr uncov_nablas
|
| ... |
... |
@@ -415,18 +432,18 @@ discardWarningsDs. |
|
415
|
432
|
-- * Collecting long-distance information
|
|
416
|
433
|
--
|
|
417
|
434
|
|
|
418
|
|
-ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (Nablas, NonEmpty Nablas)
|
|
|
435
|
+ldiMatchGroup :: PmMatchGroup Post -> NonEmpty (LdiNablas, NonEmpty LdiNablas)
|
|
419
|
436
|
ldiMatchGroup (PmMatchGroup matches) = ldiMatch <$> matches
|
|
420
|
437
|
|
|
421
|
|
-ldiMatch :: PmMatch Post -> (Nablas, NonEmpty Nablas)
|
|
|
438
|
+ldiMatch :: PmMatch Post -> (LdiNablas, NonEmpty LdiNablas)
|
|
422
|
439
|
ldiMatch (PmMatch { pm_pats = red, pm_grhss = grhss }) =
|
|
423
|
|
- (rs_cov red, ldiGRHSs grhss)
|
|
|
440
|
+ (Ldi (rs_cov red), ldiGRHSs grhss)
|
|
424
|
441
|
|
|
425
|
|
-ldiGRHSs :: PmGRHSs Post -> NonEmpty Nablas
|
|
|
442
|
+ldiGRHSs :: PmGRHSs Post -> NonEmpty LdiNablas
|
|
426
|
443
|
ldiGRHSs (PmGRHSs { pgs_grhss = grhss }) = ldiGRHS <$> grhss
|
|
427
|
444
|
|
|
428
|
|
-ldiGRHS :: PmGRHS Post -> Nablas
|
|
429
|
|
-ldiGRHS (PmGRHS { pg_grds = red }) = rs_cov red
|
|
|
445
|
+ldiGRHS :: PmGRHS Post -> LdiNablas
|
|
|
446
|
+ldiGRHS (PmGRHS { pg_grds = red }) = Ldi (rs_cov red)
|
|
430
|
447
|
|
|
431
|
448
|
--
|
|
432
|
449
|
-- * Collecting redundancy information
|
| ... |
... |
@@ -620,9 +637,11 @@ getNFirstUncovered mode vars n (MkNablas nablas) = go n (bagToList nablas) |
|
620
|
637
|
-- with 'unsafeInterleaveM' in order not to do unnecessary work.
|
|
621
|
638
|
locallyExtendPmNablas :: DsM a -> (Nablas -> DsM Nablas) -> DsM a
|
|
622
|
639
|
locallyExtendPmNablas k ext = do
|
|
623
|
|
- nablas <- getLdiNablas
|
|
624
|
|
- nablas' <- unsafeInterleaveM $ ext nablas
|
|
625
|
|
- updPmNablas nablas' k
|
|
|
640
|
+ ldi_nablas <- getLdiNablas
|
|
|
641
|
+ case ldi_nablas of
|
|
|
642
|
+ NoPmc -> k -- No nablas to extend, easy!
|
|
|
643
|
+ Ldi nablas -> do { nablas' <- unsafeInterleaveM $ ext nablas
|
|
|
644
|
+ ; updPmNablas (Ldi nablas') k }
|
|
626
|
645
|
|
|
627
|
646
|
-- | Add in-scope type constraints if the coverage checker might run and then
|
|
628
|
647
|
-- run the given action.
|
| ... |
... |
@@ -670,18 +689,40 @@ Consider |
|
670
|
689
|
|
|
671
|
690
|
Humans can make the "long-distance connection" between the outer pattern match
|
|
672
|
691
|
and the nested case pattern match to see that the inner pattern match is
|
|
673
|
|
-exhaustive: @c@ can't be @R@ anymore because it was matched in the first clause
|
|
674
|
|
-of @f@.
|
|
675
|
|
-
|
|
676
|
|
-To achieve similar reasoning in the coverage checker, we keep track of the set
|
|
677
|
|
-of values that can reach a particular program point (often loosely referred to
|
|
678
|
|
-as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas'.
|
|
679
|
|
-We fill that set with Covered Nablas returned by the exported checking
|
|
680
|
|
-functions, which the call sites put into place with
|
|
681
|
|
-'GHC.HsToCore.Monad.updPmNablas'.
|
|
682
|
|
-Call sites also extend this set with facts from type-constraint dictionaries,
|
|
683
|
|
-case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
|
|
684
|
|
-and 'addHsScrutTmCs'.
|
|
|
692
|
+exhaustive: `c` can't be `R` anymore because it was matched in the first clause
|
|
|
693
|
+of `f`.
|
|
|
694
|
+
|
|
|
695
|
+To achieve similar reasoning in the coverage checker:
|
|
|
696
|
+
|
|
|
697
|
+* We keep track of the set of values that can reach a particular program point
|
|
|
698
|
+ (often loosely refer red to as "Covered set") in 'GHC.HsToCore.Monad.dsl_nablas
|
|
|
699
|
+ :: LdiNablas'.
|
|
|
700
|
+
|
|
|
701
|
+* We fill that set with Covered Nablas returned by the exported checking functions,
|
|
|
702
|
+ which the call sites put into place with 'GHC.HsToCore.Monad.updPmNablas'.
|
|
|
703
|
+
|
|
|
704
|
+* Call sites also extend this set with facts from type-constraint dictionaries,
|
|
|
705
|
+ case scrutinees, etc. with the exported functions 'addTyCs', 'addCoreScrutTmCs'
|
|
|
706
|
+ and 'addHsScrutTmCs'.
|
|
|
707
|
+
|
|
|
708
|
+Wrinkles:
|
|
|
709
|
+
|
|
|
710
|
+(LDI1) During patterm-match checking, we need to make an auxiliary call the Hs
|
|
|
711
|
+ desugarer to get the Core of a let-binding or where-clause. We don't want to run
|
|
|
712
|
+ the coverage checker when doing so! Efficiency is one concern, but also a lack of
|
|
|
713
|
+ properly set up long-distance information might trigger warnings that we normally
|
|
|
714
|
+ wouldn't emit.
|
|
|
715
|
+
|
|
|
716
|
+ So `dsl_nablas :: LdiNablas` where
|
|
|
717
|
+ data LdiNablas = NoPmc | Ldi Nablas
|
|
|
718
|
+
|
|
|
719
|
+ If dsl_nablas = NoPmc, that means we are in one of these auxiliary calls; so
|
|
|
720
|
+ we want to do no pattern-match checking whatsoever. We won't need to carry
|
|
|
721
|
+ any long-distance info around; we are simply degsugaring to Core.
|
|
|
722
|
+
|
|
|
723
|
+ If dsl_nablas = Ldi nablas, then we do want to do pattern-match checking,
|
|
|
724
|
+ and the long-distance context is given by `nablas`
|
|
|
725
|
+
|
|
685
|
726
|
|
|
686
|
727
|
Note [Recovering from unsatisfiable pattern-matching constraints]
|
|
687
|
728
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|