ghc-typelits-natnormalise: GHC typechecker plugin for types of kind GHC.TypeLits.Nat
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
Warnings:
- 'ghc-options: -O0' is not needed. Use the --disable-optimization configure flag.
A type checker plugin for GHC that can solve equalities and inequalities
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 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, 0.5.6, 0.5.7, 0.5.8, 0.5.9, 0.5.10, 0.6, 0.6.1, 0.6.2, 0.7, 0.7.1, 0.7.2, 0.7.3, 0.7.4, 0.7.4, 0.7.5, 0.7.6, 0.7.7, 0.7.8, 0.7.9, 0.7.10 |
|---|---|
| Change log | CHANGELOG.md |
| Dependencies | base (>=4.9 && <5), containers (>=0.5.7.1 && <0.7), ghc (>=8.0.1 && <9.2), ghc-bignum (>=1.0 && <1.1), ghc-tcplugins-extra (>=0.3.1), integer-gmp (>=1.0 && <1.1), transformers (>=0.5.2.0 && <0.6) [details] |
| License | BSD-2-Clause |
| Copyright | Copyright © 2015-2016, University of Twente, 2017-2018, QBayLogic B.V. |
| 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 repo | head: git clone https://github.com/clash-lang/ghc-typelits-natnormalise.git |
| Uploaded | by ChristiaanBaaij at 2021-02-12T18:07:29Z |
Modules
[Index] [Quick Jump]
Flags
Manual Flags
| Name | Description | Default |
|---|---|---|
| deverror | Enables `-Werror` for development mode and TravisCI | Disabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- ghc-typelits-natnormalise-0.7.4.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees
Readme for ghc-typelits-natnormalise-0.7.4
[back to package description]ghc-typelits-natnormalise
A type checker plugin for GHC that can solve equalities and inequalities
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.