1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
|
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>
Sebastian Graf <sgraf1337@gmail.com>
-}
-- | Types used through-out pattern match checking. This module is mostly there
-- to be imported from "GHC.HsToCore.Types". The exposed API is that of
-- "GHC.HsToCore.Pmc".
--
-- These types model the paper
-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
module GHC.HsToCore.Pmc.Types (
-- * LYG syntax
-- ** Guard language
SrcInfo(..), PmGrd(..), GrdVec(..),
-- ** Guard tree language
PmMatchGroup(..), PmMatch(..), PmGRHSs(..), PmGRHS(..), PmPatBind(..), PmEmptyCase(..),
-- * Coverage Checking types
RedSets (..), Precision (..), CheckResult (..),
-- * Pre and post coverage checking synonyms
Pre, Post,
-- * Normalised refinement types
module GHC.HsToCore.Pmc.Solver.Types
) where
#include "HsVersions.h"
import GHC.Prelude
import GHC.HsToCore.Pmc.Solver.Types
import GHC.Data.OrdList
import GHC.Types.Id
import GHC.Types.Var (EvVar)
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Core.Type
import GHC.Core
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import qualified Data.Semigroup as Semi
--
-- * Guard language
--
-- | A very simple language for pattern guards. Let bindings, bang patterns,
-- and matching variables against flat constructor patterns.
-- The LYG guard language.
data PmGrd
= -- | @PmCon x K dicts args@ corresponds to a @K dicts args <- x@ guard.
-- The @args@ are bound in this construct, the @x@ is just a use.
-- For the arguments' meaning see 'GHC.Hs.Pat.ConPatOut'.
PmCon {
pm_id :: !Id,
pm_con_con :: !PmAltCon,
pm_con_tvs :: ![TyVar],
pm_con_dicts :: ![EvVar],
pm_con_args :: ![Id]
}
-- | @PmBang x@ corresponds to a @seq x True@ guard.
-- If the extra 'SrcInfo' is present, the bang guard came from a source
-- bang pattern, in which case we might want to report it as redundant.
-- See Note [Dead bang patterns] in GHC.HsToCore.Pmc.Check.
| PmBang {
pm_id :: !Id,
_pm_loc :: !(Maybe SrcInfo)
}
-- | @PmLet x expr@ corresponds to a @let x = expr@ guard. This actually
-- /binds/ @x@.
| PmLet {
pm_id :: !Id,
_pm_let_expr :: !CoreExpr
}
-- | Should not be user-facing.
instance Outputable PmGrd where
ppr (PmCon x alt _tvs _con_dicts con_args)
= hsep [ppr alt, hsep (map ppr con_args), text "<-", ppr x]
ppr (PmBang x _loc) = char '!' <> ppr x
ppr (PmLet x expr) = hsep [text "let", ppr x, text "=", ppr expr]
--
-- * Guard tree language
--
-- | Means by which we identify a source construct for later pretty-printing in
-- a warning message. 'SDoc' for the equation to show, 'Located' for the
-- location.
newtype SrcInfo = SrcInfo (Located SDoc)
-- | A sequence of 'PmGrd's.
newtype GrdVec = GrdVec [PmGrd]
-- | A guard tree denoting 'MatchGroup'.
newtype PmMatchGroup p = PmMatchGroup (NonEmpty (PmMatch p))
-- | A guard tree denoting 'Match': A payload describing the pats and a bunch of
-- GRHS.
data PmMatch p = PmMatch { pm_pats :: !p, pm_grhss :: !(PmGRHSs p) }
-- | A guard tree denoting 'GRHSs': A bunch of 'PmLet' guards for local
-- bindings from the 'GRHSs's @where@ clauses and the actual list of 'GRHS'.
-- See Note [Long-distance information for HsLocalBinds] in
-- "GHC.HsToCore.Pmc.Desugar".
data PmGRHSs p = PmGRHSs { pgs_lcls :: !p, pgs_grhss :: !(NonEmpty (PmGRHS p))}
-- | A guard tree denoting 'GRHS': A payload describing the grds and a 'SrcInfo'
-- useful for printing out in warnings messages.
data PmGRHS p = PmGRHS { pg_grds :: !p, pg_rhs :: !SrcInfo }
-- | A guard tree denoting an -XEmptyCase.
newtype PmEmptyCase = PmEmptyCase { pe_var :: Id }
-- | A guard tree denoting a pattern binding.
newtype PmPatBind p =
-- just reuse GrdGRHS and pretend its @SrcInfo@ is info on the /pattern/,
-- rather than on the pattern bindings.
PmPatBind (PmGRHS p)
instance Outputable SrcInfo where
ppr (SrcInfo (L (RealSrcSpan rss _) _)) = ppr (srcSpanStartLine rss)
ppr (SrcInfo (L s _)) = ppr s
-- | Format LYG guards as @| True <- x, let x = 42, !z@
instance Outputable GrdVec where
ppr (GrdVec []) = empty
ppr (GrdVec (g:gs)) = fsep (char '|' <+> ppr g : map ((comma <+>) . ppr) gs)
-- | Format a LYG sequence (e.g. 'Match'es of a 'MatchGroup' or 'GRHSs') as
-- @{ <first alt>; ...; <last alt> }@
pprLygSequence :: Outputable a => NonEmpty a -> SDoc
pprLygSequence (NE.toList -> as) =
braces (space <> fsep (punctuate semi (map ppr as)) <> space)
instance Outputable p => Outputable (PmMatchGroup p) where
ppr (PmMatchGroup matches) = pprLygSequence matches
instance Outputable p => Outputable (PmMatch p) where
ppr (PmMatch { pm_pats = grds, pm_grhss = grhss }) =
ppr grds <+> ppr grhss
instance Outputable p => Outputable (PmGRHSs p) where
ppr (PmGRHSs { pgs_lcls = _lcls, pgs_grhss = grhss }) =
ppr grhss
instance Outputable p => Outputable (PmGRHS p) where
ppr (PmGRHS { pg_grds = grds, pg_rhs = rhs }) =
ppr grds <+> text "->" <+> ppr rhs
instance Outputable p => Outputable (PmPatBind p) where
ppr (PmPatBind PmGRHS { pg_grds = grds, pg_rhs = bind }) =
ppr bind <+> ppr grds <+> text "=" <+> text "..."
instance Outputable PmEmptyCase where
ppr (PmEmptyCase { pe_var = var }) =
text "<empty case on " <> ppr var <> text ">"
data Precision = Approximate | Precise
deriving (Eq, Show)
instance Outputable Precision where
ppr = text . show
instance Semi.Semigroup Precision where
Precise <> Precise = Precise
_ <> _ = Approximate
instance Monoid Precision where
mempty = Precise
mappend = (Semi.<>)
-- | Redundancy sets, used to determine redundancy of RHSs and bang patterns
-- (later digested into a 'CIRB').
data RedSets
= RedSets
{ rs_cov :: !Nablas
-- ^ The /Covered/ set; the set of values reaching a particular program
-- point.
, rs_div :: !Nablas
-- ^ The /Diverging/ set; empty if no match can lead to divergence.
-- If it wasn't empty, we have to turn redundancy warnings into
-- inaccessibility warnings for any subclauses.
, rs_bangs :: !(OrdList (Nablas, SrcInfo))
-- ^ If any of the 'Nablas' is empty, the corresponding 'SrcInfo' pin-points
-- a bang pattern in source that is redundant. See Note [Dead bang patterns].
}
instance Outputable RedSets where
ppr RedSets { rs_cov = _cov, rs_div = _div, rs_bangs = _bangs }
-- It's useful to change this definition for different verbosity levels in
-- printf-debugging
= empty
-- | Pattern-match coverage check result
data CheckResult a
= CheckResult
{ cr_ret :: !a
-- ^ A hole for redundancy info and covered sets.
, cr_uncov :: !Nablas
-- ^ The set of uncovered values falling out at the bottom.
-- (for -Wincomplete-patterns, but also important state for the algorithm)
, cr_approx :: !Precision
-- ^ A flag saying whether we ran into the 'maxPmCheckModels' limit for the
-- purpose of suggesting to crank it up in the warning message. Writer state.
} deriving Functor
instance Outputable a => Outputable (CheckResult a) where
ppr (CheckResult c unc pc)
= text "CheckResult" <+> ppr_precision pc <+> braces (fsep
[ field "ret" c <> comma
, field "uncov" unc])
where
ppr_precision Precise = empty
ppr_precision Approximate = text "(Approximate)"
field name value = text name <+> equals <+> ppr value
--
-- * Pre and post coverage checking synonyms
--
-- | Used as tree payload pre-checking. The LYG guards to check.
type Pre = GrdVec
-- | Used as tree payload post-checking. The redundancy info we elaborated.
type Post = RedSets
|