cef94767a9d296856a870c58127eb6e5a03dde7a
[ghc.git] / compiler / basicTypes / PatSyn.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1998
4
5 \section[PatSyn]{@PatSyn@: Pattern synonyms}
6 -}
7
8 {-# LANGUAGE CPP, DeriveDataTypeable #-}
9
10 module PatSyn (
11 -- * Main data types
12 PatSyn, mkPatSyn,
13
14 -- ** Type deconstruction
15 patSynName, patSynArity, patSynIsInfix,
16 patSynArgs, patSynType,
17 patSynMatcher, patSynBuilder,
18 patSynExTyVars, patSynSig,
19 patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
20 patSynFieldType,
21
22 tidyPatSynIds
23 ) where
24
25 #include "HsVersions.h"
26
27 import Type
28 import TcType( mkSpecSigmaTy )
29 import Name
30 import Outputable
31 import Unique
32 import Util
33 import BasicTypes
34 import Var
35 import FieldLabel
36
37 import qualified Data.Data as Data
38 import qualified Data.Typeable
39 import Data.Function
40 import Data.List
41
42 {-
43 ************************************************************************
44 * *
45 \subsection{Pattern synonyms}
46 * *
47 ************************************************************************
48 -}
49
50 -- | A pattern synonym
51 -- See Note [Pattern synonym representation]
52 -- See Note [Pattern synonym signatures]
53 data PatSyn
54 = MkPatSyn {
55 psName :: Name,
56 psUnique :: Unique, -- Cached from Name
57
58 psArgs :: [Type],
59 psArity :: Arity, -- == length psArgs
60 psInfix :: Bool, -- True <=> declared infix
61 psFieldLabels :: [FieldLabel], -- List of fields for a
62 -- record pattern synonym
63 -- INVARIANT: either empty if no
64 -- record pat syn or same length as
65 -- psArgs
66
67 psUnivTyVars :: [TyVar], -- Universially-quantified type variables
68 psReqTheta :: ThetaType, -- Required dictionaries
69 -- these constraints are very much like
70 -- stupid thetas (which is a useful
71 -- guideline when implementing)
72 -- but are actually needed.
73 psExTyVars :: [TyVar], -- Existentially-quantified type vars
74 psProvTheta :: ThetaType, -- Provided dictionaries
75 psOrigResTy :: Type, -- Mentions only psUnivTyVars
76
77 -- See Note [Matchers and builders for pattern synonyms]
78 psMatcher :: (Id, Bool),
79 -- Matcher function.
80 -- If Bool is True then prov_theta and arg_tys are empty
81 -- and type is
82 -- forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
83 -- req_theta
84 -- => res_ty
85 -- -> (forall ex_tvs. Void# -> r)
86 -- -> (Void# -> r)
87 -- -> r
88 --
89 -- Otherwise type is
90 -- forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
91 -- req_theta
92 -- => res_ty
93 -- -> (forall ex_tvs. prov_theta => arg_tys -> r)
94 -- -> (Void# -> r)
95 -- -> r
96
97 psBuilder :: Maybe (Id, Bool)
98 -- Nothing => uni-directional pattern synonym
99 -- Just (builder, is_unlifted) => bi-directional
100 -- Builder function, of type
101 -- forall univ_tvs, ex_tvs. (req_theta, prov_theta)
102 -- => arg_tys -> res_ty
103 -- See Note [Builder for pattern synonyms with unboxed type]
104 }
105 deriving Data.Typeable.Typeable
106
107 {- Note [Pattern synonym signatures]
108 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
109 In a pattern synonym signature we write
110 pattern P :: req => prov => t1 -> ... tn -> res_ty
111
112 Note that the "required" context comes first, then the "provided"
113 context. Moreover, the "required" context must not mention
114 existentially-bound type variables; that is, ones not mentioned in
115 res_ty. See lots of discussion in Trac #10928.
116
117 If there is no "provided" context, you can omit it; but you
118 can't omit the "required" part (unless you omit both).
119
120 Example 1:
121 pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b)
122 pattern P1 x = Just (3,x)
123
124 We require (Num a, Eq a) to match the 3; there is no provided
125 context.
126
127 Example 2:
128 data T2 where
129 MkT2 :: (Num a, Eq a) => a -> a -> T2
130
131 pattern P2 :: () => (Num a, Eq a) => a -> T2
132 pattern P2 x = MkT2 3 x
133
134 When we match against P2 we get a Num dictionary provided.
135 We can use that to check the match against 3.
136
137 Example 3:
138 pattern P3 :: Eq a => a -> b -> T3 b
139
140 This signature is illegal because the (Eq a) is a required
141 constraint, but it mentions the existentially-bound variable 'a'.
142 You can see it's existential because it doesn't appear in the
143 result type (T3 b).
144
145 Note [Pattern synonym representation]
146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
147 Consider the following pattern synonym declaration
148
149 pattern P x = MkT [x] (Just 42)
150
151 where
152 data T a where
153 MkT :: (Show a, Ord b) => [b] -> a -> T a
154
155 so pattern P has type
156
157 b -> T (Maybe t)
158
159 with the following typeclass constraints:
160
161 requires: (Eq t, Num t)
162 provides: (Show (Maybe t), Ord b)
163
164 In this case, the fields of MkPatSyn will be set as follows:
165
166 psArgs = [b]
167 psArity = 1
168 psInfix = False
169
170 psUnivTyVars = [t]
171 psExTyVars = [b]
172 psProvTheta = (Show (Maybe t), Ord b)
173 psReqTheta = (Eq t, Num t)
174 psOrigResTy = T (Maybe t)
175
176 Note [Matchers and builders for pattern synonyms]
177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
178 For each pattern synonym P, we generate
179
180 * a "matcher" function, used to desugar uses of P in patterns,
181 which implements pattern matching
182
183 * A "builder" function (for bidirectional pattern synonyms only),
184 used to desugar uses of P in expressions, which constructs P-values.
185
186 For the above example, the matcher function has type:
187
188 $mP :: forall (r :: ?) t. (Eq t, Num t)
189 => T (Maybe t)
190 -> (forall b. (Show (Maybe t), Ord b) => b -> r)
191 -> (Void# -> r)
192 -> r
193
194 with the following implementation:
195
196 $mP @r @t $dEq $dNum scrut cont fail
197 = case scrut of
198 MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x
199 _ -> fail Void#
200
201 Notice that the return type 'r' has an open kind, so that it can
202 be instantiated by an unboxed type; for example where we see
203 f (P x) = 3#
204
205 The extra Void# argument for the failure continuation is needed so that
206 it is lazy even when the result type is unboxed.
207
208 For the same reason, if the pattern has no arguments, an extra Void#
209 argument is added to the success continuation as well.
210
211 For *bidirectional* pattern synonyms, we also generate a "builder"
212 function which implements the pattern synonym in an expression
213 context. For our running example, it will be:
214
215 $bP :: forall t b. (Eq t, Num t, Show (Maybe t), Ord b)
216 => b -> T (Maybe t)
217 $bP x = MkT [x] (Just 42)
218
219 NB: the existential/universal and required/provided split does not
220 apply to the builder since you are only putting stuff in, not getting
221 stuff out.
222
223 Injectivity of bidirectional pattern synonyms is checked in
224 tcPatToExpr which walks the pattern and returns its corresponding
225 expression when available.
226
227 Note [Builder for pattern synonyms with unboxed type]
228 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
229 For bidirectional pattern synonyms that have no arguments and have an
230 unboxed type, we add an extra Void# argument to the builder, else it
231 would be a top-level declaration with an unboxed type.
232
233 pattern P = 0#
234
235 $bP :: Void# -> Int#
236 $bP _ = 0#
237
238 This means that when typechecking an occurrence of P in an expression,
239 we must remember that the builder has this void argument. This is
240 done by TcPatSyn.patSynBuilderOcc.
241
242
243 ************************************************************************
244 * *
245 \subsection{Instances}
246 * *
247 ************************************************************************
248 -}
249
250 instance Eq PatSyn where
251 (==) = (==) `on` getUnique
252 (/=) = (/=) `on` getUnique
253
254 instance Ord PatSyn where
255 (<=) = (<=) `on` getUnique
256 (<) = (<) `on` getUnique
257 (>=) = (>=) `on` getUnique
258 (>) = (>) `on` getUnique
259 compare = compare `on` getUnique
260
261 instance Uniquable PatSyn where
262 getUnique = psUnique
263
264 instance NamedThing PatSyn where
265 getName = patSynName
266
267 instance Outputable PatSyn where
268 ppr = ppr . getName
269
270 instance OutputableBndr PatSyn where
271 pprInfixOcc = pprInfixName . getName
272 pprPrefixOcc = pprPrefixName . getName
273
274 instance Data.Data PatSyn where
275 -- don't traverse?
276 toConstr _ = abstractConstr "PatSyn"
277 gunfold _ _ = error "gunfold"
278 dataTypeOf _ = mkNoRepType "PatSyn"
279
280 {-
281 ************************************************************************
282 * *
283 \subsection{Construction}
284 * *
285 ************************************************************************
286 -}
287
288 -- | Build a new pattern synonym
289 mkPatSyn :: Name
290 -> Bool -- ^ Is the pattern synonym declared infix?
291 -> ([TyVar], ThetaType) -- ^ Universially-quantified type variables
292 -- and required dicts
293 -> ([TyVar], ThetaType) -- ^ Existentially-quantified type variables
294 -- and provided dicts
295 -> [Type] -- ^ Original arguments
296 -> Type -- ^ Original result type
297 -> (Id, Bool) -- ^ Name of matcher
298 -> Maybe (Id, Bool) -- ^ Name of builder
299 -> [FieldLabel] -- ^ Names of fields for
300 -- a record pattern synonym
301 -> PatSyn
302 mkPatSyn name declared_infix
303 (univ_tvs, req_theta)
304 (ex_tvs, prov_theta)
305 orig_args
306 orig_res_ty
307 matcher builder field_labels
308 = MkPatSyn {psName = name, psUnique = getUnique name,
309 psUnivTyVars = univ_tvs, psExTyVars = ex_tvs,
310 psProvTheta = prov_theta, psReqTheta = req_theta,
311 psInfix = declared_infix,
312 psArgs = orig_args,
313 psArity = length orig_args,
314 psOrigResTy = orig_res_ty,
315 psMatcher = matcher,
316 psBuilder = builder,
317 psFieldLabels = field_labels
318 }
319
320 -- | The 'Name' of the 'PatSyn', giving it a unique, rooted identification
321 patSynName :: PatSyn -> Name
322 patSynName = psName
323
324 patSynType :: PatSyn -> Type
325 -- The full pattern type, used only in error messages
326 -- See Note [Pattern synonym signatures]
327 patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
328 , psExTyVars = ex_tvs, psProvTheta = prov_theta
329 , psArgs = orig_args, psOrigResTy = orig_res_ty })
330 = mkSpecSigmaTy univ_tvs req_theta $ -- use mkSpecSigmaTy because it
331 mkSpecSigmaTy ex_tvs prov_theta $ -- prints better
332 mkFunTys orig_args orig_res_ty
333
334 -- | Should the 'PatSyn' be presented infix?
335 patSynIsInfix :: PatSyn -> Bool
336 patSynIsInfix = psInfix
337
338 -- | Arity of the pattern synonym
339 patSynArity :: PatSyn -> Arity
340 patSynArity = psArity
341
342 patSynArgs :: PatSyn -> [Type]
343 patSynArgs = psArgs
344
345 patSynFieldLabels :: PatSyn -> [FieldLabel]
346 patSynFieldLabels = psFieldLabels
347
348 -- | Extract the type for any given labelled field of the 'DataCon'
349 patSynFieldType :: PatSyn -> FieldLabelString -> Type
350 patSynFieldType ps label
351 = case find ((== label) . flLabel . fst) (psFieldLabels ps `zip` psArgs ps) of
352 Just (_, ty) -> ty
353 Nothing -> pprPanic "dataConFieldType" (ppr ps <+> ppr label)
354
355 patSynExTyVars :: PatSyn -> [TyVar]
356 patSynExTyVars = psExTyVars
357
358 patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
359 patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
360 , psProvTheta = prov, psReqTheta = req
361 , psArgs = arg_tys, psOrigResTy = res_ty })
362 = (univ_tvs, req, ex_tvs, prov, arg_tys, res_ty)
363
364 patSynMatcher :: PatSyn -> (Id,Bool)
365 patSynMatcher = psMatcher
366
367 patSynBuilder :: PatSyn -> Maybe (Id, Bool)
368 patSynBuilder = psBuilder
369
370 tidyPatSynIds :: (Id -> Id) -> PatSyn -> PatSyn
371 tidyPatSynIds tidy_fn ps@(MkPatSyn { psMatcher = matcher, psBuilder = builder })
372 = ps { psMatcher = tidy_pr matcher, psBuilder = fmap tidy_pr builder }
373 where
374 tidy_pr (id, dummy) = (tidy_fn id, dummy)
375
376 patSynInstArgTys :: PatSyn -> [Type] -> [Type]
377 -- Return the types of the argument patterns
378 -- e.g. data D a = forall b. MkD a b (b->a)
379 -- pattern P f x y = MkD (x,True) y f
380 -- D :: forall a. forall b. a -> b -> (b->a) -> D a
381 -- P :: forall c. forall b. (b->(c,Bool)) -> c -> b -> P c
382 -- patSynInstArgTys P [Int,bb] = [bb->(Int,Bool), Int, bb]
383 -- NB: the inst_tys should be both universal and existential
384 patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
385 , psExTyVars = ex_tvs, psArgs = arg_tys })
386 inst_tys
387 = ASSERT2( length tyvars == length inst_tys
388 , text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys )
389 map (substTyWith tyvars inst_tys) arg_tys
390 where
391 tyvars = univ_tvs ++ ex_tvs
392
393 patSynInstResTy :: PatSyn -> [Type] -> Type
394 -- Return the type of whole pattern
395 -- E.g. pattern P x y = Just (x,x,y)
396 -- P :: a -> b -> Just (a,a,b)
397 -- (patSynInstResTy P [Int,Bool] = Maybe (Int,Int,Bool)
398 -- NB: unlikepatSynInstArgTys, the inst_tys should be just the *universal* tyvars
399 patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
400 , psOrigResTy = res_ty })
401 inst_tys
402 = ASSERT2( length univ_tvs == length inst_tys
403 , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys )
404 substTyWith univ_tvs inst_tys res_ty