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