Changelog for the ghc-typelits-extra
package
- Add support for GHC 9.10.1
- Fix Plugin silently fails when normalizing <= in GHC 9.4+ #50
- Fix faulty lookup for
Mod
andDiv
in GHC >= 9.2
- Support for GHC-9.8.1
- Support for GHC-9.6.0.20230210
- Add support for GHC 9.4
- Add support for GHC 9.2.0.20210422
- Add support for GHC 9.0.1-rc1
- Reduce
n <=? Max (n + p) p
toTrue
Max
short-circuits on zero, but is stuckness preserving. i.e.Max (0-1) 0
reduces to(0-1)
- Reduce inside arithmetic equations. e.g.
1 + a ~ Max 0 a + CLog 2 2
- Add support for GHC 8.10.1-alpha2
- Reduce
a <=? Max a b
toTrue
- Reduce
n ~ (Max a b) => a <=? n
toTrue
- Prove
Max (1 + n) 1 ~ (n+1)
- Move
KnownNat2
instances for GHC 8.4'sDiv
andMod
fromghc-typelits-extra
toghc-typelits-knownnat
- Add support for GHC-8.6.1-alpha1
- Add support for ghc-typelits-natnormalise-0.6
- Add support for GHC-8.4.1-alpha1
- Support GHC 8.2
Max
,Min
,GCD
, andLCM
now have a commutativity property #9- Reduce
GCD 0 x
tox
#9 - Reduce
GCD 1 x
to1
#9 - Reduce
GCD x x
tox
#9 - Reduce
LCM 0 x
to0
#9 - Reduce
LCM 1 x
tox
#9 - Reduce
LCM x x
tox
#9 - Reduce
Max (0-1) 0
to0
#10 - Reduce
Min (0-1) 0
to0 - 1
#10 - Fixes bugs:
- Solver turns LCM into GCD #8
- Solver turns Max into Min
- Reduce
Min n (n+1)
ton
- Reduce
Max n (n+1)
ton+1
- Reduce cases like
1 <=? Div 18 6
toTrue
- Add a type-level division that rounds up:
type DivRU n d = Div (n + (d - 1)) d
- Add a type-level
divMod
:DivMod :: Nat -> Nat -> '(Nat, Nat)
- Reduce
Max n n
ton
- Reduce
Min n n
ton
- New type-level operations:
Max
: type-levelmax
Min
: type-levelmin
Div
: type-leveldiv
Mod
: type-levelmod
FLog
: floor of logBaseLog
: exact integer logBase (i.e. wherefloor (logBase b x) ~ ceiling (logBase b x)
holds)LCM
: type-levellcm
- Fixes bugs:
CLog b 1
doesn't reduce to0
- Fixes bugs:
- Rounding error in
CLog
calculation
- Rounding error in
- Solve KnownNat constraints over CLog and GCD, i.e., KnownNat (CLog 2 4)
- Compile on GHC 8.0+
- Initial release