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