Improve documentation (Related to #8447)
[ghc.git] / compiler / typecheck / TcTypeNats.hs
1 module TcTypeNats
2 ( typeNatTyCons
3 , typeNatCoAxiomRules
4 , TcBuiltInSynFamily(..)
5 ) where
6
7 import Type
8 import Pair
9 import TcType ( TcType )
10 import TyCon ( TyCon, SynTyConRhs(..), mkSynTyCon, TyConParent(..) )
11 import Coercion ( Role(..) )
12 import TcRnTypes ( Xi )
13 import TcEvidence ( mkTcAxiomRuleCo, TcCoercion )
14 import CoAxiom ( CoAxiomRule(..) )
15 import Name ( Name, BuiltInSyntax(..) )
16 import TysWiredIn ( typeNatKind, mkWiredInTyConName
17 , promotedBoolTyCon
18 , promotedFalseDataCon, promotedTrueDataCon
19 )
20 import TysPrim ( tyVarList, mkArrowKinds )
21 import PrelNames ( gHC_TYPELITS
22 , typeNatAddTyFamNameKey
23 , typeNatMulTyFamNameKey
24 , typeNatExpTyFamNameKey
25 , typeNatLeqTyFamNameKey
26 , typeNatSubTyFamNameKey
27 )
28 import FamInst ( TcBuiltInSynFamily(..) )
29 import FastString ( FastString, fsLit )
30 import qualified Data.Map as Map
31 import Data.Maybe ( isJust )
32
33 {-------------------------------------------------------------------------------
34 Built-in type constructors for functions on type-lelve nats
35 -}
36
37 typeNatTyCons :: [TyCon]
38 typeNatTyCons =
39 [ typeNatAddTyCon
40 , typeNatMulTyCon
41 , typeNatExpTyCon
42 , typeNatLeqTyCon
43 , typeNatSubTyCon
44 ]
45
46 typeNatAddTyCon :: TyCon
47 typeNatAddTyCon = mkTypeNatFunTyCon2 name
48 TcBuiltInSynFamily
49 { sfMatchFam = matchFamAdd
50 , sfInteractTop = interactTopAdd
51 , sfInteractInert = interactInertAdd
52 }
53 where
54 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
55 typeNatAddTyFamNameKey typeNatAddTyCon
56
57 typeNatSubTyCon :: TyCon
58 typeNatSubTyCon = mkTypeNatFunTyCon2 name
59 TcBuiltInSynFamily
60 { sfMatchFam = matchFamSub
61 , sfInteractTop = interactTopSub
62 , sfInteractInert = interactInertSub
63 }
64 where
65 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "-")
66 typeNatSubTyFamNameKey typeNatSubTyCon
67
68 typeNatMulTyCon :: TyCon
69 typeNatMulTyCon = mkTypeNatFunTyCon2 name
70 TcBuiltInSynFamily
71 { sfMatchFam = matchFamMul
72 , sfInteractTop = interactTopMul
73 , sfInteractInert = interactInertMul
74 }
75 where
76 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
77 typeNatMulTyFamNameKey typeNatMulTyCon
78
79 typeNatExpTyCon :: TyCon
80 typeNatExpTyCon = mkTypeNatFunTyCon2 name
81 TcBuiltInSynFamily
82 { sfMatchFam = matchFamExp
83 , sfInteractTop = interactTopExp
84 , sfInteractInert = interactInertExp
85 }
86 where
87 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
88 typeNatExpTyFamNameKey typeNatExpTyCon
89
90 typeNatLeqTyCon :: TyCon
91 typeNatLeqTyCon =
92 mkSynTyCon name
93 (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
94 (take 2 $ tyVarList typeNatKind)
95 [Nominal,Nominal]
96 (BuiltInSynFamTyCon ops)
97 NoParentTyCon
98
99 where
100 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
101 typeNatLeqTyFamNameKey typeNatLeqTyCon
102 ops = TcBuiltInSynFamily
103 { sfMatchFam = matchFamLeq
104 , sfInteractTop = interactTopLeq
105 , sfInteractInert = interactInertLeq
106 }
107
108
109 -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
110 mkTypeNatFunTyCon2 :: Name -> TcBuiltInSynFamily -> TyCon
111 mkTypeNatFunTyCon2 op tcb =
112 mkSynTyCon op
113 (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
114 (take 2 $ tyVarList typeNatKind)
115 [Nominal,Nominal]
116 (BuiltInSynFamTyCon tcb)
117 NoParentTyCon
118
119
120
121
122 {-------------------------------------------------------------------------------
123 Built-in rules axioms
124 -------------------------------------------------------------------------------}
125
126 -- If you add additional rules, please remember to add them to
127 -- `typeNatCoAxiomRules` also.
128 axAddDef
129 , axMulDef
130 , axExpDef
131 , axLeqDef
132 , axAdd0L
133 , axAdd0R
134 , axMul0L
135 , axMul0R
136 , axMul1L
137 , axMul1R
138 , axExp1L
139 , axExp0R
140 , axExp1R
141 , axLeqRefl
142 , axLeq0L
143 , axSubDef
144 , axSub0R
145 :: CoAxiomRule
146
147 axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
148 \x y -> Just $ num (x + y)
149
150 axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
151 \x y -> Just $ num (x * y)
152
153 axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
154 \x y -> Just $ num (x ^ y)
155
156 axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
157 \x y -> Just $ bool (x <= y)
158
159 axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
160 \x y -> fmap num (minus x y)
161
162 axAdd0L = mkAxiom1 "Add0L" $ \t -> (num 0 .+. t) === t
163 axAdd0R = mkAxiom1 "Add0R" $ \t -> (t .+. num 0) === t
164 axSub0R = mkAxiom1 "Sub0R" $ \t -> (t .-. num 0) === t
165 axMul0L = mkAxiom1 "Mul0L" $ \t -> (num 0 .*. t) === num 0
166 axMul0R = mkAxiom1 "Mul0R" $ \t -> (t .*. num 0) === num 0
167 axMul1L = mkAxiom1 "Mul1L" $ \t -> (num 1 .*. t) === t
168 axMul1R = mkAxiom1 "Mul1R" $ \t -> (t .*. num 1) === t
169 axExp1L = mkAxiom1 "Exp1L" $ \t -> (num 1 .^. t) === num 1
170 axExp0R = mkAxiom1 "Exp0R" $ \t -> (t .^. num 0) === num 1
171 axExp1R = mkAxiom1 "Exp1R" $ \t -> (t .^. num 1) === t
172 axLeqRefl = mkAxiom1 "LeqRefl" $ \t -> (t <== t) === bool True
173 axLeq0L = mkAxiom1 "Leq0L" $ \t -> (num 0 <== t) === bool True
174
175 typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
176 typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
177 [ axAddDef
178 , axMulDef
179 , axExpDef
180 , axLeqDef
181 , axAdd0L
182 , axAdd0R
183 , axMul0L
184 , axMul0R
185 , axMul1L
186 , axMul1R
187 , axExp1L
188 , axExp0R
189 , axExp1R
190 , axLeqRefl
191 , axLeq0L
192 , axSubDef
193 ]
194
195
196
197 {-------------------------------------------------------------------------------
198 Various utilities for making axioms and types
199 -------------------------------------------------------------------------------}
200
201 (.+.) :: Type -> Type -> Type
202 s .+. t = mkTyConApp typeNatAddTyCon [s,t]
203
204 (.-.) :: Type -> Type -> Type
205 s .-. t = mkTyConApp typeNatSubTyCon [s,t]
206
207 (.*.) :: Type -> Type -> Type
208 s .*. t = mkTyConApp typeNatMulTyCon [s,t]
209
210 (.^.) :: Type -> Type -> Type
211 s .^. t = mkTyConApp typeNatExpTyCon [s,t]
212
213 (<==) :: Type -> Type -> Type
214 s <== t = mkTyConApp typeNatLeqTyCon [s,t]
215
216 (===) :: Type -> Type -> Pair Type
217 x === y = Pair x y
218
219 num :: Integer -> Type
220 num = mkNumLitTy
221
222 boolKind :: Kind
223 boolKind = mkTyConApp promotedBoolTyCon []
224
225 bool :: Bool -> Type
226 bool b = if b then mkTyConApp promotedTrueDataCon []
227 else mkTyConApp promotedFalseDataCon []
228
229 isBoolLitTy :: Type -> Maybe Bool
230 isBoolLitTy tc =
231 do (tc,[]) <- splitTyConApp_maybe tc
232 case () of
233 _ | tc == promotedFalseDataCon -> return False
234 | tc == promotedTrueDataCon -> return True
235 | otherwise -> Nothing
236
237 known :: (Integer -> Bool) -> TcType -> Bool
238 known p x = case isNumLitTy x of
239 Just a -> p a
240 Nothing -> False
241
242
243
244
245 -- For the definitional axioms
246 mkBinAxiom :: String -> TyCon ->
247 (Integer -> Integer -> Maybe Type) -> CoAxiomRule
248 mkBinAxiom str tc f =
249 CoAxiomRule
250 { coaxrName = fsLit str
251 , coaxrTypeArity = 2
252 , coaxrAsmpRoles = []
253 , coaxrRole = Nominal
254 , coaxrProves = \ts cs ->
255 case (ts,cs) of
256 ([s,t],[]) -> do x <- isNumLitTy s
257 y <- isNumLitTy t
258 z <- f x y
259 return (mkTyConApp tc [s,t] === z)
260 _ -> Nothing
261 }
262
263 mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
264 mkAxiom1 str f =
265 CoAxiomRule
266 { coaxrName = fsLit str
267 , coaxrTypeArity = 1
268 , coaxrAsmpRoles = []
269 , coaxrRole = Nominal
270 , coaxrProves = \ts cs ->
271 case (ts,cs) of
272 ([s],[]) -> return (f s)
273 _ -> Nothing
274 }
275
276
277 {-------------------------------------------------------------------------------
278 Evaluation
279 -------------------------------------------------------------------------------}
280
281 matchFamAdd :: [Type] -> Maybe (TcCoercion, TcType)
282 matchFamAdd [s,t]
283 | Just 0 <- mbX = Just (mkTcAxiomRuleCo axAdd0L [t] [], t)
284 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axAdd0R [s] [], s)
285 | Just x <- mbX, Just y <- mbY =
286 Just (mkTcAxiomRuleCo axAddDef [s,t] [], num (x + y))
287 where mbX = isNumLitTy s
288 mbY = isNumLitTy t
289 matchFamAdd _ = Nothing
290
291 matchFamSub :: [Type] -> Maybe (TcCoercion, TcType)
292 matchFamSub [s,t]
293 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axSub0R [s] [], s)
294 | Just x <- mbX, Just y <- mbY, Just z <- minus x y =
295 Just (mkTcAxiomRuleCo axSubDef [s,t] [], num z)
296 where mbX = isNumLitTy s
297 mbY = isNumLitTy t
298 matchFamSub _ = Nothing
299
300 matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
301 matchFamMul [s,t]
302 | Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
303 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axMul0R [s] [], num 0)
304 | Just 1 <- mbX = Just (mkTcAxiomRuleCo axMul1L [t] [], t)
305 | Just 1 <- mbY = Just (mkTcAxiomRuleCo axMul1R [s] [], s)
306 | Just x <- mbX, Just y <- mbY =
307 Just (mkTcAxiomRuleCo axMulDef [s,t] [], num (x * y))
308 where mbX = isNumLitTy s
309 mbY = isNumLitTy t
310 matchFamMul _ = Nothing
311
312 matchFamExp :: [Xi] -> Maybe (TcCoercion, Xi)
313 matchFamExp [s,t]
314 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axExp0R [s] [], num 1)
315 | Just 1 <- mbX = Just (mkTcAxiomRuleCo axExp1L [t] [], num 1)
316 | Just 1 <- mbY = Just (mkTcAxiomRuleCo axExp1R [s] [], s)
317 | Just x <- mbX, Just y <- mbY =
318 Just (mkTcAxiomRuleCo axExpDef [s,t] [], num (x ^ y))
319 where mbX = isNumLitTy s
320 mbY = isNumLitTy t
321 matchFamExp _ = Nothing
322
323 matchFamLeq :: [Xi] -> Maybe (TcCoercion, Xi)
324 matchFamLeq [s,t]
325 | Just 0 <- mbX = Just (mkTcAxiomRuleCo axLeq0L [t] [], bool True)
326 | Just x <- mbX, Just y <- mbY =
327 Just (mkTcAxiomRuleCo axLeqDef [s,t] [], bool (x <= y))
328 | eqType s t = Just (mkTcAxiomRuleCo axLeqRefl [s] [], bool True)
329 where mbX = isNumLitTy s
330 mbY = isNumLitTy t
331 matchFamLeq _ = Nothing
332
333 {-------------------------------------------------------------------------------
334 Interact with axioms
335 -------------------------------------------------------------------------------}
336
337 interactTopAdd :: [Xi] -> Xi -> [Pair Type]
338 interactTopAdd [s,t] r
339 | Just 0 <- mbZ = [ s === num 0, t === num 0 ] -- (s + t ~ 0) => (s ~ 0, t ~ 0)
340 | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y] -- (5 + t ~ 8) => (t ~ 3)
341 | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x] -- (s + 5 ~ 8) => (s ~ 3)
342 where
343 mbX = isNumLitTy s
344 mbY = isNumLitTy t
345 mbZ = isNumLitTy r
346 interactTopAdd _ _ = []
347
348 {-
349 Note [Weakened interaction rule for subtraction]
350 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
351
352 A simpler interaction here might be:
353
354 `s - t ~ r` --> `t + r ~ s`
355
356 This would enable us to reuse all the code for addition.
357 Unfortunately, this works a little too well at the moment.
358 Consider the following example:
359
360 0 - 5 ~ r --> 5 + r ~ 0 --> (5 = 0, r = 0)
361
362 This (correctly) spots that the constraint cannot be solved.
363
364 However, this may be a problem if the constraint did not
365 need to be solved in the first place! Consider the following example:
366
367 f :: Proxy (If (5 <=? 0) (0 - 5) (5 - 0)) -> Proxy 5
368 f = id
369
370 Currently, GHC is strict while evaluating functions, so this does not
371 work, because even though the `If` should evaluate to `5 - 0`, we
372 also evaluate the "then" branch which generates the constraint `0 - 5 ~ r`,
373 which fails.
374
375 So, for the time being, we only add an improvement when the RHS is a constant,
376 which happens to work OK for the moment, although clearly we need to do
377 something more general.
378 -}
379 interactTopSub :: [Xi] -> Xi -> [Pair Type]
380 interactTopSub [s,t] r
381 | Just z <- mbZ = [ s === (num z .+. t) ] -- (s - t ~ 5) => (5 + t ~ s)
382 where
383 mbZ = isNumLitTy r
384 interactTopSub _ _ = []
385
386
387
388
389
390 interactTopMul :: [Xi] -> Xi -> [Pair Type]
391 interactTopMul [s,t] r
392 | Just 1 <- mbZ = [ s === num 1, t === num 1 ] -- (s * t ~ 1) => (s ~ 1, t ~ 1)
393 | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y] -- (3 * t ~ 15) => (t ~ 5)
394 | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x] -- (s * 3 ~ 15) => (s ~ 5)
395 where
396 mbX = isNumLitTy s
397 mbY = isNumLitTy t
398 mbZ = isNumLitTy r
399 interactTopMul _ _ = []
400
401 interactTopExp :: [Xi] -> Xi -> [Pair Type]
402 interactTopExp [s,t] r
403 | Just 0 <- mbZ = [ s === num 0 ] -- (s ^ t ~ 0) => (s ~ 0)
404 | Just x <- mbX, Just z <- mbZ, Just y <- logExact z x = [t === num y] -- (2 ^ t ~ 8) => (t ~ 3)
405 | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x] -- (s ^ 2 ~ 9) => (s ~ 3)
406 where
407 mbX = isNumLitTy s
408 mbY = isNumLitTy t
409 mbZ = isNumLitTy r
410 interactTopExp _ _ = []
411
412 interactTopLeq :: [Xi] -> Xi -> [Pair Type]
413 interactTopLeq [s,t] r
414 | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ] -- (s <= 0) => (s ~ 0)
415 where
416 mbY = isNumLitTy t
417 mbZ = isBoolLitTy r
418 interactTopLeq _ _ = []
419
420
421
422 {-------------------------------------------------------------------------------
423 Interaction with inerts
424 -------------------------------------------------------------------------------}
425
426 interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
427 interactInertAdd [x1,y1] z1 [x2,y2] z2
428 | sameZ && eqType x1 x2 = [ y1 === y2 ]
429 | sameZ && eqType y1 y2 = [ x1 === x2 ]
430 where sameZ = eqType z1 z2
431 interactInertAdd _ _ _ _ = []
432
433 interactInertSub :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
434 interactInertSub [x1,y1] z1 [x2,y2] z2
435 | sameZ && eqType x1 x2 = [ y1 === y2 ]
436 | sameZ && eqType y1 y2 = [ x1 === x2 ]
437 where sameZ = eqType z1 z2
438 interactInertSub _ _ _ _ = []
439
440 interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
441 interactInertMul [x1,y1] z1 [x2,y2] z2
442 | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
443 | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ]
444 where sameZ = eqType z1 z2
445
446 interactInertMul _ _ _ _ = []
447
448 interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
449 interactInertExp [x1,y1] z1 [x2,y2] z2
450 | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ]
451 | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ]
452 where sameZ = eqType z1 z2
453
454 interactInertExp _ _ _ _ = []
455
456
457 interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
458 interactInertLeq [x1,y1] z1 [x2,y2] z2
459 | bothTrue && eqType x1 y2 && eqType y1 x2 = [ x1 === y1 ]
460 | bothTrue && eqType y1 x2 = [ (x1 <== y2) === bool True ]
461 | bothTrue && eqType y2 x1 = [ (x2 <== y1) === bool True ]
462 where bothTrue = isJust $ do True <- isBoolLitTy z1
463 True <- isBoolLitTy z2
464 return ()
465
466 interactInertLeq _ _ _ _ = []
467
468
469
470
471 {- -----------------------------------------------------------------------------
472 These inverse functions are used for simplifying propositions using
473 concrete natural numbers.
474 ----------------------------------------------------------------------------- -}
475
476 -- | Subtract two natural numbers.
477 minus :: Integer -> Integer -> Maybe Integer
478 minus x y = if x >= y then Just (x - y) else Nothing
479
480 -- | Compute the exact logarithm of a natural number.
481 -- The logarithm base is the second argument.
482 logExact :: Integer -> Integer -> Maybe Integer
483 logExact x y = do (z,True) <- genLog x y
484 return z
485
486
487 -- | Divide two natural numbers.
488 divide :: Integer -> Integer -> Maybe Integer
489 divide _ 0 = Nothing
490 divide x y = case divMod x y of
491 (a,0) -> Just a
492 _ -> Nothing
493
494 -- | Compute the exact root of a natural number.
495 -- The second argument specifies which root we are computing.
496 rootExact :: Integer -> Integer -> Maybe Integer
497 rootExact x y = do (z,True) <- genRoot x y
498 return z
499
500
501
502 {- | Compute the the n-th root of a natural number, rounded down to
503 the closest natural number. The boolean indicates if the result
504 is exact (i.e., True means no rounding was done, False means rounded down).
505 The second argument specifies which root we are computing. -}
506 genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
507 genRoot _ 0 = Nothing
508 genRoot x0 1 = Just (x0, True)
509 genRoot x0 root = Just (search 0 (x0+1))
510 where
511 search from to = let x = from + div (to - from) 2
512 a = x ^ root
513 in case compare a x0 of
514 EQ -> (x, True)
515 LT | x /= from -> search x to
516 | otherwise -> (from, False)
517 GT | x /= to -> search from x
518 | otherwise -> (from, False)
519
520 {- | Compute the logarithm of a number in the given base, rounded down to the
521 closest integer. The boolean indicates if we the result is exact
522 (i.e., True means no rounding happened, False means we rounded down).
523 The logarithm base is the second argument. -}
524 genLog :: Integer -> Integer -> Maybe (Integer, Bool)
525 genLog x 0 = if x == 1 then Just (0, True) else Nothing
526 genLog _ 1 = Nothing
527 genLog 0 _ = Nothing
528 genLog x base = Just (exactLoop 0 x)
529 where
530 exactLoop s i
531 | i == 1 = (s,True)
532 | i < base = (s,False)
533 | otherwise =
534 let s1 = s + 1
535 in s1 `seq` case divMod i base of
536 (j,r)
537 | r == 0 -> exactLoop s1 j
538 | otherwise -> (underLoop s1 j, False)
539
540 underLoop s i
541 | i < base = s
542 | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)
543
544
545
546
547
548
549