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