ghc-typelits-extra

Additional type-level operations on GHC.TypeLits.Nat

http://www.clash-lang.org/

Version on this page:0.4
LTS Haskell 19.18:0.4.3@rev:1
Stackage Nightly 2022-08-04:0.4.3@rev:1
Latest on Hackage:0.4.3@rev:1

See all snapshots ghc-typelits-extra appears in

BSD-2-Clause licensed by Christiaan Baaij
Maintained by christiaan.baaij@gmail.com
This version can be pinned in stack with:ghc-typelits-extra-0.4@sha256:e1ba4ebf14cb7025dd940380dfb15db444f7e8bced7e30bdad6e1707f0af7622,4813

Module documentation for 0.4

Used by 2 packages in lts-16.11(full list with versions):
clash-ghc, clash-prelude

ghc-typelits-extra

Build Status Hackage Hackage Dependencies

Extra type-level operations on GHC.TypeLits.Nat and a custom solver implemented as a GHC type-checker plugin:

  • GHC.TypeLits.Extra.Max: type-level max
  • GHC.TypeLits.Extra.Min: type-level min
  • GHC.TypeLits.Extra.Div: type-level div
  • GHC.TypeLits.Extra.Mod: type-level mod
  • GHC.TypeLits.Extra.FLog: type-level equivalent of integerLogBase# .i.e. the exact integer equivalent to “floor (logBase x y)”
  • GHC.TypeLits.Extra.CLog: type-level equivalent of the ceiling of integerLogBase# .i.e. the exact integer equivalent to “ceiling (logBase x y)”
  • ‘GHC.TypeLits.Extra.Log’: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> where the operation only reduces when “floor (logBase b x) ~ ceiling (logBase b x)”
  • GHC.TypeLits.Extra.GCD: a type-level gcd
  • GHC.TypeLits.Extra.LCM: a type-level lcm

Changes

Changelog for the ghc-typelits-extra package

0.4 March 9 2020

  • 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

0.3.3 February 6th 2020

  • Add support for GHC 8.10.1-alpha2

0.3.2 January 18th 2020

0.3.1 August 26th 2019

  • Reduce a <=? Max a b to True
  • Reduce n ~ (Max a b) => a <=? n to True
  • Prove Max (1 + n) 1 ~ (n+1)

0.3 September 14th 2018

  • Move KnownNat2 instances for GHC 8.4’s Div and Mod from ghc-typelits-extra to ghc-typelits-knownnat

0.2.6 Julty 10th 2018

  • Add support for GHC-8.6.1-alpha1

0.2.5 May 9th 2018

  • Add support for ghc-typelits-natnormalise-0.6

0.2.4 January 4th 2018

  • Add support for GHC-8.4.1-alpha1

0.2.3 May 15th 2017

  • Support GHC 8.2
  • Max, Min, GCD, and LCM now have a commutativity property #9
  • Reduce GCD 0 x to x #9
  • Reduce GCD 1 x to 1 #9
  • Reduce GCD x x to x #9
  • Reduce LCM 0 x to 0 #9
  • Reduce LCM 1 x to x #9
  • Reduce LCM x x to x #9
  • Reduce Max (0-1) 0 to 0 #10
  • Reduce Min (0-1) 0 to 0 - 1 #10
  • Fixes bugs:
    • Solver turns LCM into GCD #8
    • Solver turns Max into Min

0.2.2 January 15th 2017

  • Reduce Min n (n+1) to n
  • Reduce Max n (n+1) to n+1
  • Reduce cases like 1 <=? Div 18 6 to True
  • 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)

0.2.1 September 29th 2016

  • Reduce Max n n to n
  • Reduce Min n n to n

0.2 August 19th 2016

  • New type-level operations:
    • Max: type-level max
    • Min: type-level min
    • Div: type-level div
    • Mod: type-level mod
    • FLog: floor of logBase
    • Log: exact integer logBase (i.e. where floor (logBase b x) ~ ceiling (logBase b x) holds)
    • LCM: type-level lcm
  • Fixes bugs:
    • CLog b 1 doesn’t reduce to 0

0.1.3 July 19th 2016

  • Fixes bugs:
    • Rounding error in CLog calculation

0.1.2 July 8th 2016

  • Solve KnownNat constraints over CLog and GCD, i.e., KnownNat (CLog 2 4)

0.1.1 January 20th 2016

  • Compile on GHC 8.0+

0.1 October 21st 2015

  • Initial release
A service provided by FP Complete