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