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