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