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