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
|
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
-- | Provides factilities for pretty-printing 'Nabla's in a way appropriate for
-- user facing pattern match warnings.
module GHC.HsToCore.Pmc.Ppr (
pprUncovered
) where
#include "HsVersions.h"
import GHC.Prelude
import GHC.Types.Basic
import GHC.Types.Id
import GHC.Types.Var.Env
import GHC.Types.Unique.DFM
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Builtin.Types
import GHC.Utils.Outputable
import GHC.Utils.Panic
import Control.Monad.Trans.RWS.CPS
import GHC.Utils.Misc
import GHC.Data.Maybe
import Data.List.NonEmpty (NonEmpty, nonEmpty, toList)
import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Solver
-- | Pretty-print the guts of an uncovered value vector abstraction, i.e., its
-- components and refutable shapes associated to any mentioned variables.
--
-- Example for @([Just p, q], [p :-> [3,4], q :-> [0,5]])@:
--
-- @
-- (Just p) q
-- where p is not one of {3, 4}
-- q is not one of {0, 5}
-- @
--
-- When the set of refutable shapes contains more than 3 elements, the
-- additional elements are indicated by "...".
pprUncovered :: Nabla -> [Id] -> SDoc
pprUncovered nabla vas
| isNullUDFM refuts = fsep vec -- there are no refutations
| otherwise = hang (fsep vec) 4 $
text "where" <+> vcat (map (pprRefutableShapes . snd) (udfmToList refuts))
where
init_prec
-- No outer parentheses when it's a unary pattern by assuming lowest
-- precedence
| [_] <- vas = topPrec
| otherwise = appPrec
ppr_action = mapM (pprPmVar init_prec) vas
(vec, renamings) = runPmPpr nabla ppr_action
refuts = prettifyRefuts nabla renamings
-- | Output refutable shapes of a variable in the form of @var is not one of {2,
-- Nothing, 3}@. Will never print more than 3 refutable shapes, the tail is
-- indicated by an ellipsis.
pprRefutableShapes :: (SDoc,[PmAltCon]) -> SDoc
pprRefutableShapes (var, alts)
= var <+> text "is not one of" <+> format_alts alts
where
format_alts = braces . fsep . punctuate comma . shorten . map ppr_alt
shorten (a:b:c:_:_) = a:b:c:[text "..."]
shorten xs = xs
ppr_alt (PmAltConLike cl) = ppr cl
ppr_alt (PmAltLit lit) = ppr lit
{- 1. Literals
~~~~~~~~~~~~~~
Starting with a function definition like:
f :: Int -> Bool
f 5 = True
f 6 = True
The uncovered set looks like:
{ var |> var /= 5, var /= 6 }
Yet, we would like to print this nicely as follows:
x , where x not one of {5,6}
Since these variables will be shown to the programmer, we give them better names
(t1, t2, ..) in 'prettifyRefuts', hence the SDoc in 'PrettyPmRefutEnv'.
2. Residual Constraints
~~~~~~~~~~~~~~~~~~~~~~~
Unhandled constraints that refer to HsExpr are typically ignored by the solver
(it does not even substitute in HsExpr so they are even printed as wildcards).
Additionally, the oracle returns a substitution if it succeeds so we apply this
substitution to the vectors before printing them out (see function `pprOne' in
"GHC.HsToCore.Pmc") to be more precise.
-}
-- | Extract and assigns pretty names to constraint variables with refutable
-- shapes.
prettifyRefuts :: Nabla -> DIdEnv (Id, SDoc) -> DIdEnv (SDoc, [PmAltCon])
prettifyRefuts nabla = listToUDFM_Directly . map attach_refuts . udfmToList
where
attach_refuts (u, (x, sdoc)) = (u, (sdoc, lookupRefuts nabla x))
type PmPprM a = RWS Nabla () (DIdEnv (Id, SDoc), [SDoc]) a
-- Try nice names p,q,r,s,t before using the (ugly) t_i
nameList :: [SDoc]
nameList = map text ["p","q","r","s","t"] ++
[ text ('t':show u) | u <- [(0 :: Int)..] ]
runPmPpr :: Nabla -> PmPprM a -> (a, DIdEnv (Id, SDoc))
runPmPpr nabla m = case runRWS m nabla (emptyDVarEnv, nameList) of
(a, (renamings, _), _) -> (a, renamings)
-- | Allocates a new, clean name for the given 'Id' if it doesn't already have
-- one.
getCleanName :: Id -> PmPprM SDoc
getCleanName x = do
(renamings, name_supply) <- get
let (clean_name:name_supply') = name_supply
case lookupDVarEnv renamings x of
Just (_, nm) -> pure nm
Nothing -> do
put (extendDVarEnv renamings x (x, clean_name), name_supply')
pure clean_name
checkRefuts :: Id -> PmPprM (Maybe SDoc) -- the clean name if it has negative info attached
checkRefuts x = do
nabla <- ask
case lookupRefuts nabla x of
[] -> pure Nothing -- Will just be a wildcard later on
_ -> Just <$> getCleanName x
-- | Pretty print a variable, but remember to prettify the names of the variables
-- that refer to neg-literals. The ones that cannot be shown are printed as
-- underscores.
pprPmVar :: PprPrec -> Id -> PmPprM SDoc
pprPmVar prec x = do
nabla <- ask
case lookupSolution nabla x of
Just (PACA alt _tvs args) -> pprPmAltCon prec alt args
Nothing -> fromMaybe underscore <$> checkRefuts x
pprPmAltCon :: PprPrec -> PmAltCon -> [Id] -> PmPprM SDoc
pprPmAltCon _prec (PmAltLit l) _ = pure (ppr l)
pprPmAltCon prec (PmAltConLike cl) args = do
nabla <- ask
pprConLike nabla prec cl args
pprConLike :: Nabla -> PprPrec -> ConLike -> [Id] -> PmPprM SDoc
pprConLike nabla _prec cl args
| Just pm_expr_list <- pmExprAsList nabla (PmAltConLike cl) args
= case pm_expr_list of
NilTerminated list ->
brackets . fsep . punctuate comma <$> mapM (pprPmVar appPrec) list
WcVarTerminated pref x ->
parens . fcat . punctuate colon <$> mapM (pprPmVar appPrec) (toList pref ++ [x])
pprConLike _nabla _prec (RealDataCon con) args
| isUnboxedTupleDataCon con
, let hash_parens doc = text "(#" <+> doc <+> text "#)"
= hash_parens . fsep . punctuate comma <$> mapM (pprPmVar appPrec) args
| isTupleDataCon con
= parens . fsep . punctuate comma <$> mapM (pprPmVar appPrec) args
pprConLike _nabla prec cl args
| conLikeIsInfix cl = case args of
[x, y] -> do x' <- pprPmVar funPrec x
y' <- pprPmVar funPrec y
return (cparen (prec > opPrec) (x' <+> ppr cl <+> y'))
-- can it be infix but have more than two arguments?
list -> pprPanic "pprConLike:" (ppr list)
| null args = return (ppr cl)
| otherwise = do args' <- mapM (pprPmVar appPrec) args
return (cparen (prec > funPrec) (fsep (ppr cl : args')))
-- | The result of 'pmExprAsList'.
data PmExprList
= NilTerminated [Id]
| WcVarTerminated (NonEmpty Id) Id
-- | Extract a list of 'Id's out of a sequence of cons cells, optionally
-- terminated by a wildcard variable instead of @[]@. Some examples:
--
-- * @pmExprAsList (1:2:[]) == Just ('NilTerminated' [1,2])@, a regular,
-- @[]@-terminated list. Should be pretty-printed as @[1,2]@.
-- * @pmExprAsList (1:2:x) == Just ('WcVarTerminated' [1,2] x)@, a list prefix
-- ending in a wildcard variable x (of list type). Should be pretty-printed as
-- (1:2:_).
-- * @pmExprAsList [] == Just ('NilTerminated' [])@
pmExprAsList :: Nabla -> PmAltCon -> [Id] -> Maybe PmExprList
pmExprAsList nabla = go_con []
where
go_var rev_pref x
| Just (PACA alt _tvs args) <- lookupSolution nabla x
= go_con rev_pref alt args
go_var rev_pref x
| Just pref <- nonEmpty (reverse rev_pref)
= Just (WcVarTerminated pref x)
go_var _ _
= Nothing
go_con rev_pref (PmAltConLike (RealDataCon c)) es
| c == nilDataCon
= ASSERT( null es ) Just (NilTerminated (reverse rev_pref))
| c == consDataCon
= ASSERT( length es == 2 ) go_var (es !! 0 : rev_pref) (es !! 1)
go_con _ _ _
= Nothing
|
