Comment typo only
[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 )
27 import FamInst ( TcBuiltInSynFamily(..) )
28 import FastString ( FastString, fsLit )
29 import qualified Data.Map as Map
30 import Data.Maybe ( isJust )
31
32 {-------------------------------------------------------------------------------
33 Built-in type constructors for functions on type-lelve nats
34 -}
35
36 typeNatTyCons :: [TyCon]
37 typeNatTyCons =
38 [ typeNatAddTyCon
39 , typeNatMulTyCon
40 , typeNatExpTyCon
41 , typeNatLeqTyCon
42 ]
43
44 typeNatAddTyCon :: TyCon
45 typeNatAddTyCon = mkTypeNatFunTyCon2 name
46 TcBuiltInSynFamily
47 { sfMatchFam = matchFamAdd
48 , sfInteractTop = interactTopAdd
49 , sfInteractInert = interactInertAdd
50 }
51 where
52 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "+")
53 typeNatAddTyFamNameKey typeNatAddTyCon
54
55 typeNatMulTyCon :: TyCon
56 typeNatMulTyCon = mkTypeNatFunTyCon2 name
57 TcBuiltInSynFamily
58 { sfMatchFam = matchFamMul
59 , sfInteractTop = interactTopMul
60 , sfInteractInert = interactInertMul
61 }
62 where
63 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "*")
64 typeNatMulTyFamNameKey typeNatMulTyCon
65
66 typeNatExpTyCon :: TyCon
67 typeNatExpTyCon = mkTypeNatFunTyCon2 name
68 TcBuiltInSynFamily
69 { sfMatchFam = matchFamExp
70 , sfInteractTop = interactTopExp
71 , sfInteractInert = interactInertExp
72 }
73 where
74 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "^")
75 typeNatExpTyFamNameKey typeNatExpTyCon
76
77 typeNatLeqTyCon :: TyCon
78 typeNatLeqTyCon =
79 mkSynTyCon name
80 (mkArrowKinds [ typeNatKind, typeNatKind ] boolKind)
81 (take 2 $ tyVarList typeNatKind)
82 [Nominal,Nominal]
83 (BuiltInSynFamTyCon ops)
84 NoParentTyCon
85
86 where
87 name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "<=?")
88 typeNatLeqTyFamNameKey typeNatLeqTyCon
89 ops = TcBuiltInSynFamily
90 { sfMatchFam = matchFamLeq
91 , sfInteractTop = interactTopLeq
92 , sfInteractInert = interactInertLeq
93 }
94
95
96 -- Make a binary built-in constructor of kind: Nat -> Nat -> Nat
97 mkTypeNatFunTyCon2 :: Name -> TcBuiltInSynFamily -> TyCon
98 mkTypeNatFunTyCon2 op tcb =
99 mkSynTyCon op
100 (mkArrowKinds [ typeNatKind, typeNatKind ] typeNatKind)
101 (take 2 $ tyVarList typeNatKind)
102 [Nominal,Nominal]
103 (BuiltInSynFamTyCon tcb)
104 NoParentTyCon
105
106
107
108
109 {-------------------------------------------------------------------------------
110 Built-in rules axioms
111 -------------------------------------------------------------------------------}
112
113 -- If you add additional rules, please remember to add them to
114 -- `typeNatCoAxiomRules` also.
115 axAddDef
116 , axMulDef
117 , axExpDef
118 , axLeqDef
119 , axAdd0L
120 , axAdd0R
121 , axMul0L
122 , axMul0R
123 , axMul1L
124 , axMul1R
125 , axExp1L
126 , axExp0R
127 , axExp1R
128 , axLeqRefl
129 , axLeq0L
130 :: CoAxiomRule
131
132 axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
133 \x y -> num (x + y)
134
135 axMulDef = mkBinAxiom "MulDef" typeNatMulTyCon $
136 \x y -> num (x * y)
137
138 axExpDef = mkBinAxiom "ExpDef" typeNatExpTyCon $
139 \x y -> num (x ^ y)
140
141 axLeqDef = mkBinAxiom "LeqDef" typeNatLeqTyCon $
142 \x y -> bool (x <= y)
143
144 axAdd0L = mkAxiom1 "Add0L" $ \t -> (num 0 .+. t) === t
145 axAdd0R = mkAxiom1 "Add0R" $ \t -> (t .+. num 0) === t
146 axMul0L = mkAxiom1 "Mul0L" $ \t -> (num 0 .*. t) === num 0
147 axMul0R = mkAxiom1 "Mul0R" $ \t -> (t .*. num 0) === num 0
148 axMul1L = mkAxiom1 "Mul1L" $ \t -> (num 1 .*. t) === t
149 axMul1R = mkAxiom1 "Mul1R" $ \t -> (t .*. num 1) === t
150 axExp1L = mkAxiom1 "Exp1L" $ \t -> (num 1 .^. t) === num 1
151 axExp0R = mkAxiom1 "Exp0R" $ \t -> (t .^. num 0) === num 1
152 axExp1R = mkAxiom1 "Exp1R" $ \t -> (t .^. num 1) === t
153 axLeqRefl = mkAxiom1 "LeqRefl" $ \t -> (t <== t) === bool True
154 axLeq0L = mkAxiom1 "Leq0L" $ \t -> (num 0 <== t) === bool True
155
156 typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
157 typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
158 [ axAddDef
159 , axMulDef
160 , axExpDef
161 , axLeqDef
162 , axAdd0L
163 , axAdd0R
164 , axMul0L
165 , axMul0R
166 , axMul1L
167 , axMul1R
168 , axExp1L
169 , axExp0R
170 , axExp1R
171 , axLeqRefl
172 , axLeq0L
173 ]
174
175
176
177 {-------------------------------------------------------------------------------
178 Various utilities for making axioms and types
179 -------------------------------------------------------------------------------}
180
181 (.+.) :: Type -> Type -> Type
182 s .+. t = mkTyConApp typeNatAddTyCon [s,t]
183
184 (.*.) :: Type -> Type -> Type
185 s .*. t = mkTyConApp typeNatMulTyCon [s,t]
186
187 (.^.) :: Type -> Type -> Type
188 s .^. t = mkTyConApp typeNatExpTyCon [s,t]
189
190 (<==) :: Type -> Type -> Type
191 s <== t = mkTyConApp typeNatLeqTyCon [s,t]
192
193 (===) :: Type -> Type -> Pair Type
194 x === y = Pair x y
195
196 num :: Integer -> Type
197 num = mkNumLitTy
198
199 boolKind :: Kind
200 boolKind = mkTyConApp promotedBoolTyCon []
201
202 bool :: Bool -> Type
203 bool b = if b then mkTyConApp promotedTrueDataCon []
204 else mkTyConApp promotedFalseDataCon []
205
206 isBoolLitTy :: Type -> Maybe Bool
207 isBoolLitTy tc =
208 do (tc,[]) <- splitTyConApp_maybe tc
209 case () of
210 _ | tc == promotedFalseDataCon -> return False
211 | tc == promotedTrueDataCon -> return True
212 | otherwise -> Nothing
213
214 known :: (Integer -> Bool) -> TcType -> Bool
215 known p x = case isNumLitTy x of
216 Just a -> p a
217 Nothing -> False
218
219
220
221
222 -- For the definitional axioms
223 mkBinAxiom :: String -> TyCon ->
224 (Integer -> Integer -> Type) -> CoAxiomRule
225 mkBinAxiom str tc f =
226 CoAxiomRule
227 { coaxrName = fsLit str
228 , coaxrTypeArity = 2
229 , coaxrAsmpRoles = []
230 , coaxrRole = Nominal
231 , coaxrProves = \ts cs ->
232 case (ts,cs) of
233 ([s,t],[]) -> do x <- isNumLitTy s
234 y <- isNumLitTy t
235 return (mkTyConApp tc [s,t] === f x y)
236 _ -> Nothing
237 }
238
239 mkAxiom1 :: String -> (Type -> Pair Type) -> CoAxiomRule
240 mkAxiom1 str f =
241 CoAxiomRule
242 { coaxrName = fsLit str
243 , coaxrTypeArity = 1
244 , coaxrAsmpRoles = []
245 , coaxrRole = Nominal
246 , coaxrProves = \ts cs ->
247 case (ts,cs) of
248 ([s],[]) -> return (f s)
249 _ -> Nothing
250 }
251
252
253 {-------------------------------------------------------------------------------
254 Evaluation
255 -------------------------------------------------------------------------------}
256
257 matchFamAdd :: [Type] -> Maybe (TcCoercion, TcType)
258 matchFamAdd [s,t]
259 | Just 0 <- mbX = Just (mkTcAxiomRuleCo axAdd0L [t] [], t)
260 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axAdd0R [s] [], s)
261 | Just x <- mbX, Just y <- mbY =
262 Just (mkTcAxiomRuleCo axAddDef [s,t] [], num (x + y))
263 where mbX = isNumLitTy s
264 mbY = isNumLitTy t
265 matchFamAdd _ = Nothing
266
267 matchFamMul :: [Xi] -> Maybe (TcCoercion, Xi)
268 matchFamMul [s,t]
269 | Just 0 <- mbX = Just (mkTcAxiomRuleCo axMul0L [t] [], num 0)
270 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axMul0R [s] [], num 0)
271 | Just 1 <- mbX = Just (mkTcAxiomRuleCo axMul1L [t] [], t)
272 | Just 1 <- mbY = Just (mkTcAxiomRuleCo axMul1R [s] [], s)
273 | Just x <- mbX, Just y <- mbY =
274 Just (mkTcAxiomRuleCo axMulDef [s,t] [], num (x * y))
275 where mbX = isNumLitTy s
276 mbY = isNumLitTy t
277 matchFamMul _ = Nothing
278
279 matchFamExp :: [Xi] -> Maybe (TcCoercion, Xi)
280 matchFamExp [s,t]
281 | Just 0 <- mbY = Just (mkTcAxiomRuleCo axExp0R [s] [], num 1)
282 | Just 1 <- mbX = Just (mkTcAxiomRuleCo axExp1L [t] [], num 1)
283 | Just 1 <- mbY = Just (mkTcAxiomRuleCo axExp1R [s] [], s)
284 | Just x <- mbX, Just y <- mbY =
285 Just (mkTcAxiomRuleCo axExpDef [s,t] [], num (x ^ y))
286 where mbX = isNumLitTy s
287 mbY = isNumLitTy t
288 matchFamExp _ = Nothing
289
290 matchFamLeq :: [Xi] -> Maybe (TcCoercion, Xi)
291 matchFamLeq [s,t]
292 | Just 0 <- mbX = Just (mkTcAxiomRuleCo axLeq0L [t] [], bool True)
293 | Just x <- mbX, Just y <- mbY =
294 Just (mkTcAxiomRuleCo axLeqDef [s,t] [], bool (x <= y))
295 | eqType s t = Just (mkTcAxiomRuleCo axLeqRefl [s] [], bool True)
296 where mbX = isNumLitTy s
297 mbY = isNumLitTy t
298 matchFamLeq _ = Nothing
299
300 {-------------------------------------------------------------------------------
301 Interact with axioms
302 -------------------------------------------------------------------------------}
303
304 interactTopAdd :: [Xi] -> Xi -> [Pair Type]
305 interactTopAdd [s,t] r
306 | Just 0 <- mbZ = [ s === num 0, t === num 0 ]
307 | Just x <- mbX, Just z <- mbZ, Just y <- minus z x = [t === num y]
308 | Just y <- mbY, Just z <- mbZ, Just x <- minus z y = [s === num x]
309 where
310 mbX = isNumLitTy s
311 mbY = isNumLitTy t
312 mbZ = isNumLitTy r
313 interactTopAdd _ _ = []
314
315 interactTopMul :: [Xi] -> Xi -> [Pair Type]
316 interactTopMul [s,t] r
317 | Just 1 <- mbZ = [ s === num 1, t === num 1 ]
318 | Just x <- mbX, Just z <- mbZ, Just y <- divide z x = [t === num y]
319 | Just y <- mbY, Just z <- mbZ, Just x <- divide z y = [s === num x]
320 where
321 mbX = isNumLitTy s
322 mbY = isNumLitTy t
323 mbZ = isNumLitTy r
324 interactTopMul _ _ = []
325
326 interactTopExp :: [Xi] -> Xi -> [Pair Type]
327 interactTopExp [s,t] r
328 | Just 0 <- mbZ = [ s === num 0 ]
329 | Just x <- mbX, Just z <- mbZ, Just y <- logExact z x = [t === num y]
330 | Just y <- mbY, Just z <- mbZ, Just x <- rootExact z y = [s === num x]
331 where
332 mbX = isNumLitTy s
333 mbY = isNumLitTy t
334 mbZ = isNumLitTy r
335 interactTopExp _ _ = []
336
337 interactTopLeq :: [Xi] -> Xi -> [Pair Type]
338 interactTopLeq [s,t] r
339 | Just 0 <- mbY, Just True <- mbZ = [ s === num 0 ]
340 where
341 mbY = isNumLitTy t
342 mbZ = isBoolLitTy r
343 interactTopLeq _ _ = []
344
345
346
347 {-------------------------------------------------------------------------------
348 Interaction with inerts
349 -------------------------------------------------------------------------------}
350
351 interactInertAdd :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
352 interactInertAdd [x1,y1] z1 [x2,y2] z2
353 | sameZ && eqType x1 x2 = [ y1 === y2 ]
354 | sameZ && eqType y1 y2 = [ x1 === x2 ]
355 where sameZ = eqType z1 z2
356 interactInertAdd _ _ _ _ = []
357
358 interactInertMul :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
359 interactInertMul [x1,y1] z1 [x2,y2] z2
360 | sameZ && known (/= 0) x1 && eqType x1 x2 = [ y1 === y2 ]
361 | sameZ && known (/= 0) y1 && eqType y1 y2 = [ x1 === x2 ]
362 where sameZ = eqType z1 z2
363
364 interactInertMul _ _ _ _ = []
365
366 interactInertExp :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
367 interactInertExp [x1,y1] z1 [x2,y2] z2
368 | sameZ && known (> 1) x1 && eqType x1 x2 = [ y1 === y2 ]
369 | sameZ && known (> 0) y1 && eqType y1 y2 = [ x1 === x2 ]
370 where sameZ = eqType z1 z2
371
372 interactInertExp _ _ _ _ = []
373
374
375 interactInertLeq :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
376 interactInertLeq [x1,y1] z1 [x2,y2] z2
377 | bothTrue && eqType x1 y2 && eqType y1 x2 = [ x1 === y1 ]
378 | bothTrue && eqType y1 x2 = [ (x1 <== y2) === bool True ]
379 | bothTrue && eqType y2 x1 = [ (x2 <== y1) === bool True ]
380 where bothTrue = isJust $ do True <- isBoolLitTy z1
381 True <- isBoolLitTy z2
382 return ()
383
384 interactInertLeq _ _ _ _ = []
385
386
387
388
389 {- -----------------------------------------------------------------------------
390 These inverse functions are used for simplifying propositions using
391 concrete natural numbers.
392 ----------------------------------------------------------------------------- -}
393
394 -- | Subtract two natural numbers.
395 minus :: Integer -> Integer -> Maybe Integer
396 minus x y = if x >= y then Just (x - y) else Nothing
397
398 -- | Compute the exact logarithm of a natural number.
399 -- The logarithm base is the second argument.
400 logExact :: Integer -> Integer -> Maybe Integer
401 logExact x y = do (z,True) <- genLog x y
402 return z
403
404
405 -- | Divide two natural numbers.
406 divide :: Integer -> Integer -> Maybe Integer
407 divide _ 0 = Nothing
408 divide x y = case divMod x y of
409 (a,0) -> Just a
410 _ -> Nothing
411
412 -- | Compute the exact root of a natural number.
413 -- The second argument specifies which root we are computing.
414 rootExact :: Integer -> Integer -> Maybe Integer
415 rootExact x y = do (z,True) <- genRoot x y
416 return z
417
418
419
420 {- | Compute the the n-th root of a natural number, rounded down to
421 the closest natural number. The boolean indicates if the result
422 is exact (i.e., True means no rounding was done, False means rounded down).
423 The second argument specifies which root we are computing. -}
424 genRoot :: Integer -> Integer -> Maybe (Integer, Bool)
425 genRoot _ 0 = Nothing
426 genRoot x0 1 = Just (x0, True)
427 genRoot x0 root = Just (search 0 (x0+1))
428 where
429 search from to = let x = from + div (to - from) 2
430 a = x ^ root
431 in case compare a x0 of
432 EQ -> (x, True)
433 LT | x /= from -> search x to
434 | otherwise -> (from, False)
435 GT | x /= to -> search from x
436 | otherwise -> (from, False)
437
438 {- | Compute the logarithm of a number in the given base, rounded down to the
439 closest integer. The boolean indicates if we the result is exact
440 (i.e., True means no rounding happened, False means we rounded down).
441 The logarithm base is the second argument. -}
442 genLog :: Integer -> Integer -> Maybe (Integer, Bool)
443 genLog x 0 = if x == 1 then Just (0, True) else Nothing
444 genLog _ 1 = Nothing
445 genLog 0 _ = Nothing
446 genLog x base = Just (exactLoop 0 x)
447 where
448 exactLoop s i
449 | i == 1 = (s,True)
450 | i < base = (s,False)
451 | otherwise =
452 let s1 = s + 1
453 in s1 `seq` case divMod i base of
454 (j,r)
455 | r == 0 -> exactLoop s1 j
456 | otherwise -> (underLoop s1 j, False)
457
458 underLoop s i
459 | i < base = s
460 | otherwise = let s1 = s + 1 in s1 `seq` underLoop s1 (div i base)
461
462
463
464
465
466
467