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