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