Skip to content

Commit 18d758f

Browse files
christiaanbchristiaanb
committed
Add exact integer logaritm Log 
1 parent 47fae74 commit 18d758f

File tree

8 files changed

+117
-4
lines changed

8 files changed

+117
-4
lines changed

‎README.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,10 @@ as a GHC type-checker plugin:
1212
* `GHC.TypeLits.Extra.Div`: type-level [div](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div)
1313
* `GHC.TypeLits.Extra.Mod`: type-level [mod](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod)
1414
* `GHC.TypeLits.Extra.FLog`: type-level equivalent of [integerLogBase#](https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-)
15+
.i.e. the exact integer equivalent to "`floor (logBase x y)`"
1516
* `GHC.TypeLits.Extra.CLog`: type-level equivalent of _the ceiling of_ [integerLogBase#](https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-)
17+
.i.e. the exact integer equivalent to "`ceiling (logBase x y)`"
18+
* 'GHC.TypeLits.Extra.Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
19+
where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`"
1620
* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd)
1721
* `GHC.TypeLits.Extra.LCM`: a type-level [lcm](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm)

‎ghc-typelits-extra.cabal‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,13 @@ description:
1313
* @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>
1414
.
1515
* @FLog@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
16+
.i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
1617
.
1718
* @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
19+
.i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"
20+
.
21+
* @Log@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
22+
where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"
1823
.
1924
* @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>
2025
.

‎src/GHC/TypeLits/Extra.hs‎

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,13 @@ Additional type-level operations on 'GHC.TypeLits.Nat':
1414
* 'Mod': type-level 'mod'
1515
1616
* 'FLog': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
17+
.i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
1718
1819
* 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
20+
.i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"
21+
22+
* 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
23+
where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"
1924
2025
* 'GCD': a type-level 'gcd'
2126
@@ -51,7 +56,7 @@ pragma to the header of your file.
5156

5257
module GHC.TypeLits.Extra
5358
( -- * Type-level operations on `Nat`
54-
-- ** Order
59+
-- ** Ord
5560
Max
5661
, Min
5762
-- ** Integral
@@ -60,6 +65,8 @@ module GHC.TypeLits.Extra
6065
-- ** Logarithm
6166
, FLog
6267
, CLog
68+
-- *** Exact logarithm
69+
, Log
6370
-- Numeric
6471
, GCD
6572
, LCM
@@ -124,6 +131,7 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y
124131
natSing2 = SNatKn (mod (natVal (Proxy @x)) (natVal (Proxy @y)))
125132

126133
-- | Type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
134+
-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
127135
--
128136
-- Note that additional equations are provided by the type-checker plugin solver
129137
-- "GHC.TypeLits.Extra.Solver".
@@ -137,6 +145,7 @@ instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''
137145
natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y))))
138146

139147
-- | Type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
148+
-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"
140149
--
141150
-- Note that additional equations are provided by the type-checker plugin solver
142151
-- "GHC.TypeLits.Extra.Solver".
@@ -156,6 +165,28 @@ instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''
156165
_ | isTrue# (z1 ==# z2) -> SNatKn (smallInteger (z1 +# 1#))
157166
| otherwise -> SNatKn (smallInteger z1)
158167

168+
-- | Type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
169+
-- where the operation only reduces when:
170+
--
171+
-- @
172+
-- 'FLog' b x ~ 'CLog' b x
173+
-- @
174+
--
175+
-- Additionally, the following property holds for 'Log':
176+
--
177+
-- > (b ^ (Log b x)) ~ x
178+
--
179+
-- Note that additional equations are provided by the type-checker plugin solver
180+
-- "GHC.TypeLits.Extra.Solver".
181+
type family Log (x :: Nat) (y :: Nat) :: Nat where
182+
Log 2 1 = 0 -- Additional equations are provided by the custom solver
183+
184+
genDefunSymbols [''Log]
185+
186+
instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where
187+
type KnownNatF2 $(nameToSymbol ''Log) = LogSym0
188+
natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y))))
189+
159190
-- | Type-level greatest common denominator (GCD).
160191
--
161192
-- Note that additional equations are provided by the type-checker plugin solver

‎src/GHC/TypeLits/Extra/Solver.hs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,13 @@ import GHC.TypeLits.Extra.Solver.Unify
5858
-- * 'Mod': type-level 'mod'
5959
--
6060
-- * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
61+
-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
6162
--
6263
-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
64+
-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"
65+
--
66+
-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>
67+
-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"
6368
--
6469
-- * 'GCD': a type-level 'gcd'
6570
--
@@ -142,6 +147,7 @@ lookupExtraDefs = do
142147
<*> look md "Mod"
143148
<*> look md "FLog"
144149
<*> look md "CLog"
150+
<*> look md "Log"
145151
<*> look md "GCD"
146152
<*> look md "LCM"
147153
where

‎src/GHC/TypeLits/Extra/Solver/Operations.hs‎

Lines changed: 24 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ module GHC.TypeLits.Extra.Solver.Operations
1212
, mergeMod
1313
, mergeFLog
1414
, mergeCLog
15+
, mergeLog
1516
, mergeGCD
1617
, mergeLCM
1718
, mergeExp
@@ -36,8 +37,9 @@ data ExtraOp
3637
| Mod ExtraOp ExtraOp
3738
| FLog ExtraOp ExtraOp
3839
| CLog ExtraOp ExtraOp
40+
| Log ExtraOp ExtraOp
3941
| GCD ExtraOp ExtraOp
40-
| LCM ExtraOp ExtraOp
42+
| LCM ExtraOp ExtraOp
4143
| Exp ExtraOp ExtraOp
4244
deriving Eq
4345

@@ -49,6 +51,7 @@ instance Outputable ExtraOp where
4951
ppr (Mod x y) = text "Mod (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
5052
ppr (FLog x y) = text "FLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
5153
ppr (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
54+
ppr (Log x y) = text "Log (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
5255
ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
5356
ppr (LCM x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
5457
ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
@@ -75,6 +78,12 @@ mergeCLog i (Exp j k) | i == j = Just k
7578
mergeCLog (I i) (I j) = I <$> clogBase i j
7679
mergeCLog x y = Just (CLog x y)
7780

81+
mergeLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
82+
mergeLog (I i) _ | i < 2 = Nothing
83+
mergeLog b (Exp b' y) | b == b' = Just y
84+
mergeLog (I i) (I j) = I <$> exactLogBase i j
85+
mergeLog x y = Just (Log x y)
86+
7887
mergeGCD :: ExtraOp -> ExtraOp -> ExtraOp
7988
mergeGCD (I i) (I j) = I (gcd i j)
8089
mergeGCD x y = GCD x y
@@ -84,8 +93,9 @@ mergeLCM (I i) (I j) = I (lcm i j)
8493
mergeLCM x y = GCD x y
8594

8695
mergeExp :: ExtraOp -> ExtraOp -> ExtraOp
87-
mergeExp (I i) (I j) = I (i^j)
88-
mergeExp x y = Exp x y
96+
mergeExp (I i) (I j) = I (i^j)
97+
mergeExp b (Log b' y) | b == b' = y
98+
mergeExp x y = Exp x y
8999

90100
-- | \x y -> logBase x y, x > 1 && y > 0
91101
flogBase :: Integer -> Integer -> Maybe Integer
@@ -102,3 +112,14 @@ clogBase x y | y > 0 =
102112
_ | isTrue# (z1 ==# z2) -> Just (smallInteger (z1 +# 1#))
103113
| otherwise -> Just (smallInteger z1)
104114
clogBase _ _ = Nothing
115+
116+
-- | \x y -> logBase x y, x > 1 && y > 0, logBase x y == ceiling (logBase x y)
117+
exactLogBase :: Integer -> Integer -> Maybe Integer
118+
exactLogBase x y | y > 0 =
119+
let z1 = integerLogBase# x y
120+
z2 = integerLogBase# x (y-1)
121+
in case y of
122+
1 -> Just 0
123+
_ | isTrue# (z1 ==# z2) -> Nothing
124+
| otherwise -> Just (smallInteger z1)
125+
exactLogBase _ _ = Nothing

‎src/GHC/TypeLits/Extra/Solver/Unify.hs‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ data ExtraDefs = ExtraDefs
3636
, modTyCon :: TyCon
3737
, flogTyCon :: TyCon
3838
, clogTyCon :: TyCon
39+
, logTyCon :: TyCon
3940
, gcdTyCon :: TyCon
4041
, lcmTyCon :: TyCon
4142
}
@@ -57,6 +58,9 @@ normaliseNat defs (TyConApp tc [x,y])
5758
| tc == clogTyCon defs = do x' <- normaliseNat defs x
5859
y' <- normaliseNat defs y
5960
MaybeT (return (mergeCLog x' y'))
61+
| tc == logTyCon defs = do x' <- normaliseNat defs x
62+
y' <- normaliseNat defs y
63+
MaybeT (return (mergeLog x' y'))
6064
| tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x
6165
<*> normaliseNat defs y
6266
| tc == lcmTyCon defs = mergeLCM <$> normaliseNat defs x
@@ -106,6 +110,7 @@ fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y
106110
fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y
107111
fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y
108112
fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y
113+
fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y
109114
fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y
110115
fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y
111116
fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y
@@ -125,6 +130,8 @@ reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x
125130
,reifyEOP defs y]
126131
reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x
127132
,reifyEOP defs y]
133+
reifyEOP defs (Log x y) = mkTyConApp (logTyCon defs) [reifyEOP defs x
134+
,reifyEOP defs y]
128135
reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x
129136
,reifyEOP defs y]
130137
reifyEOP defs (LCM x y) = mkTyConApp (lcmTyCon defs) [reifyEOP defs x
@@ -140,6 +147,7 @@ containsConstants (Div x y) = containsConstants x || containsConstants y
140147
containsConstants (Mod x y) = containsConstants x || containsConstants y
141148
containsConstants (FLog x y) = containsConstants x || containsConstants y
142149
containsConstants (CLog x y) = containsConstants x || containsConstants y
150+
containsConstants (Log x y) = containsConstants x || containsConstants y
143151
containsConstants (GCD x y) = containsConstants x || containsConstants y
144152
containsConstants (LCM x y) = containsConstants x || containsConstants y
145153
containsConstants (Exp x y) = containsConstants x || containsConstants y

‎tests/ErrorTests.hs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -65,6 +65,12 @@ testFail17 = id
6565
testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9))
6666
testFail18 = id
6767

68+
testFail19 :: Integer
69+
testFail19 = natVal (Proxy :: Proxy (Log 3 0))
70+
71+
testFail20 :: Integer
72+
testFail20 = natVal (Proxy :: Proxy (Log 3 10))
73+
6874
testFail1Errors =
6975
["Expected type: Proxy (GCD 6 8) -> Proxy 4"
7076
,"Actual type: Proxy 4 -> Proxy 4"
@@ -150,3 +156,9 @@ testFail18Errors =
150156
["Expected type: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)"
151157
,"Actual type: Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)"
152158
]
159+
160+
testFail19Errors =
161+
["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"]
162+
163+
testFail20Errors =
164+
["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"]

‎tests/Main.hs‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,18 @@ test21 = natVal (Proxy :: Proxy (CLog 3 1))
8282
test22 :: Proxy (CLog 3 1) -> Proxy 0
8383
test22 = id
8484

85+
test23 :: Integer
86+
test23 = natVal (Proxy :: Proxy (Log 3 1))
87+
88+
test24 :: Integer
89+
test24 = natVal (Proxy :: Proxy (Log 3 9))
90+
91+
test25 :: Proxy (Log 3 9) -> Proxy 2
92+
test25 = id
93+
94+
test26 :: Proxy (b ^ (Log b y)) -> Proxy y
95+
test26 = id
96+
8597
main :: IO ()
8698
main = defaultMain tests
8799

@@ -154,6 +166,18 @@ tests = testGroup "ghc-typelits-natnormalise"
154166
, testCase "CLog 3 1 ~ 0" $
155167
show (test22 Proxy) @?=
156168
"Proxy"
169+
, testCase "KnownNat (Log 3 1) ~ 0" $
170+
show test23 @?=
171+
"0"
172+
, testCase "KnownNat (Log 3 9) ~ 2" $
173+
show test24 @?=
174+
"2"
175+
, testCase "Log 3 9 ~ 2" $
176+
show (test25 Proxy) @?=
177+
"Proxy"
178+
, testCase "forall x>1 . x ^ (Log x y) ~ y" $
179+
show (test26 Proxy) @?=
180+
"Proxy"
157181
]
158182
, testGroup "errors"
159183
[ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors
@@ -174,6 +198,8 @@ tests = testGroup "ghc-typelits-natnormalise"
174198
, testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors
175199
, testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors
176200
, testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors
201+
, testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors
202+
, testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors
177203
]
178204
]
179205

0 commit comments

Comments
 (0)