The ghc-typelits-natnormalise package

[ Tags: bsd2, library, type-system ] [ Propose Tags ]

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

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 the

OPTIONS_GHC -fplugin GHC.TypeLits.Normalise

Pragma to the header of your file.


[Skip to Readme]

Properties

Versions 0.1, 0.1.1, 0.1.2, 0.2, 0.2.1, 0.3, 0.3.1, 0.4, 0.4.1, 0.4.2, 0.4.3, 0.4.4, 0.4.5, 0.4.6, 0.5, 0.5.1, 0.5.2, 0.5.3, 0.5.4, 0.5.5
Change log CHANGELOG.md
Dependencies base (>=4.8 && <5), ghc (>=7.10 && <8.2), ghc-tcplugins-extra (>=0.2) [details]
License BSD2
Copyright Copyright © 2015-2016 University of Twente
Author Christiaan Baaij
Maintainer christiaan.baaij@gmail.com
Category Type System
Home page http://www.clash-lang.org/
Bug tracker http://github.com/clash-lang/ghc-typelits-natnormalise/issues
Source repository head: git clone https://github.com/clash-lang/ghc-typelits-natnormalise.git
Uploaded Thu Feb 4 11:32:18 UTC 2016 by ChristiaanBaaij
Distributions LTSHaskell:0.5.4, NixOS:0.5.3, Stackage:0.5.5, Tumbleweed:0.5.3
Downloads 2287 total (169 in the last 30 days)
Rating 2.25 (2 ratings) [clear rating]
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]
Hackage Matrix CI

Modules

[Index]

Flags

NameDescriptionDefaultType
deverror

Enables -Werror for development mode and TravisCI

DisabledManual

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for ghc-typelits-natnormalise-0.4.1

[back to package description]

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.