ghc-typelits-natnormalise

GHC typechecker plugin for types of kind GHC.TypeLits.Nat http://www.clash-lang.org/

Version on this page:0.3
LTS Haskell 8.23:0.5.3
Stackage Nightly 2017-07-25:0.5.3
Latest on Hackage:0.5.3
BSD2 licensed by Christiaan Baaij
Maintained by christiaan.baaij@gmail.com

Module documentation for 0.3

ghc-typelits-natnormalise

Build Status Hackage Hackage Dependencies

A type checker plugin for GHC that can solve equalities of types of kind Nat, where these types are either:

  • Type-level naturals
  • Type variables
  • Applications of the arithmetic expressions (+,-,*,^).

It solves these equalities by normalising them to sort-of SOP (Sum-of-Products) form, and then perform a simple syntactic equality.

For example, this solver can prove the equality between:

(x + 2)^(y + 2)

and

4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2

Because the latter is actually the SOP normal form of the former.

To use the plugin, add

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

To the header of your file.

Changes

Changelog for the ghc-typelits-natnormalise package

0.5.3 May 15th 2017

  • Add support for GHC 8.2

0.5.2 January 15th 2017

  • Fixes bugs: * Reification from SOP to Type sometimes loses product terms

0.5.1 September 29th 2016

  • Fixes bugs: * Cannot solve an equality for the second time in a definition group

0.5 August 17th 2016

  • Solve simple inequalities, i.e.: a <= a + 1 2a <= 3a * 1 <= a^b

0.4.6 July 21th 2016

  • Reduce "x^(-y) * x^y" to 1
  • Fixes bugs: * Subtraction in exponent induces infinite loop

0.4.5 July 20th 2016

  • Fixes bugs: * Reifying negative exponent causes GHC panic

0.4.4 July 19th 2016

  • Fixes bugs: * Rounding error in logBase calculation

0.4.3 July 18th 2016

  • Fixes bugs: * False positive: "f :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)"

0.4.2 July 8th 2016

  • Find more unifications: (2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)] a^d * a^e ~ a^c ==> [c := d + e] * x+5 ~ y ==> [x := y - 5], but only when x+5 ~ y is a given constraint

0.4.1 February 4th 2016

  • Find more unifications: * F x y k z ~ F x y (k-1+1) z ==> [k := k], where F can be any type function

0.4 January 19th 2016

  • Stop using 'provenance' hack to create conditional evidence (GHC 8.0+ only)
  • Find more unifications: * F x + 2 - 1 - 1 ~ F x ==> [F x := F x], where F can be any type function with result Nat.

0.3.2

  • Find more unifications: (z ^ a) ~ (z ^ b) ==> [a := b] (i ^ a) ~ j ==> [a := round (logBase i j)], when i and j are integers, and ceiling (logBase i j) == floor (logBase i j).

0.3.1 October 19th 2015

  • Find more unifications: (i * a) ~ j ==> [a := div j i], when i and j are integers, and mod j i == 0. (i * a) + j ~ k ==> [a := div (k-j) i], when i, j, and k are integers, and k-j >= 0 and mod (k-j) i == 0.

0.3 June 3rd 2015

  • Find more unifications: * <TyApp xs> + x ~ 2 + x ==> [<TyApp xs> ~ 2]
  • Fixes bugs: Unifying a*b ~ b now returns [a ~ 1]; before it erroneously returned [a ~ ], which is interpred as [a ~ 0]... Unifying a+b ~ b now returns [a ~ 0]; before it returned the undesirable, though equal, [a ~ ]

0.2.1 May 6th 2015

  • Update Eq instance of SOP: Empty SOP is equal to 0

0.2 April 22nd 2015

  • Finds more unifications: (2 + a) ~ 5 ==> [a := 3] (3 * a) ~ 0 ==> [a := 0]

0.1.2 April 21st 2015

  • Don't simplify expressions with negative exponents

0.1.1 April 17th 2015

  • Add workaround for https://ghc.haskell.org/trac/ghc/ticket/10301

0.1 March 30th 2015

  • Initial release
comments powered byDisqus