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