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