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