diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,102 +1,105 @@ -# Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package - -# 0.4.7 *May 22nd, 2024* -* Add support for GHC 9.10.1 -* Fix Plugin silently fails when normalizing <= in GHC 9.4+ [#50](https://github.com/clash-lang/ghc-typelits-extra/issues/50) -* Fix faulty lookup for `Mod` and `Div` in GHC >= 9.2 - -# 0.4.6 *October 10th 2023* -* Support for GHC-9.8.1 - -# 0.4.5 *February 20th 2023* -* Support for GHC-9.6.0.20230210 - -# 0.4.4 *October 21st 2022* -* Add support for GHC 9.4 - -# 0.4.3 *June 18th 2021* -* Add support for GHC 9.2.0.20210422 - -# 0.4.2 *January 1st 2021* -* Add support for GHC 9.0.1-rc1 - -# 0.4.1 *November 10 2020* -* Reduce `n <=? Max (n + p) p` to `True` - -# 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* -* Fix https://github.com/clash-lang/clash-compiler/issues/1019 - -# 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](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `GCD 0 x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `GCD 1 x` to `1` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `GCD x x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `LCM 0 x` to `0` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `LCM 1 x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `LCM x x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) -* Reduce `Max (0-1) 0` to `0` [#10](https://github.com/clash-lang/ghc-typelits-extra/issues/10) -* Reduce `Min (0-1) 0` to `0 - 1` [#10](https://github.com/clash-lang/ghc-typelits-extra/issues/10) -* Fixes bugs: - * Solver turns LCM into GCD [#8](https://github.com/clash-lang/ghc-typelits-extra/issues/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 +# Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package + +# 0.4.8 *March 4th 2025* +* Add support for GHC 9.12.1 + +# 0.4.7 *May 22nd, 2024* +* Add support for GHC 9.10.1 +* Fix Plugin silently fails when normalizing <= in GHC 9.4+ [#50](https://github.com/clash-lang/ghc-typelits-extra/issues/50) +* Fix faulty lookup for `Mod` and `Div` in GHC >= 9.2 + +# 0.4.6 *October 10th 2023* +* Support for GHC-9.8.1 + +# 0.4.5 *February 20th 2023* +* Support for GHC-9.6.0.20230210 + +# 0.4.4 *October 21st 2022* +* Add support for GHC 9.4 + +# 0.4.3 *June 18th 2021* +* Add support for GHC 9.2.0.20210422 + +# 0.4.2 *January 1st 2021* +* Add support for GHC 9.0.1-rc1 + +# 0.4.1 *November 10 2020* +* Reduce `n <=? Max (n + p) p` to `True` + +# 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* +* Fix https://github.com/clash-lang/clash-compiler/issues/1019 + +# 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](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `GCD 0 x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `GCD 1 x` to `1` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `GCD x x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `LCM 0 x` to `0` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `LCM 1 x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `LCM x x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `Max (0-1) 0` to `0` [#10](https://github.com/clash-lang/ghc-typelits-extra/issues/10) +* Reduce `Min (0-1) 0` to `0 - 1` [#10](https://github.com/clash-lang/ghc-typelits-extra/issues/10) +* Fixes bugs: + * Solver turns LCM into GCD [#8](https://github.com/clash-lang/ghc-typelits-extra/issues/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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,27 +1,27 @@ -Copyright (c) 2015-2016, University of Twente, - 2017-2018, QBayLogic B.V. -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are -met: - -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the - distribution. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +Copyright (c) 2015-2016, University of Twente, + 2017-2018, QBayLogic B.V. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the + distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,21 +1,21 @@ -# ghc-typelits-extra - -[![Build Status](https://github.com/clash-lang/ghc-typelits-extra/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-extra/actions) -[![Hackage](https://img.shields.io/hackage/v/ghc-typelits-extra.svg)](https://hackage.haskell.org/package/ghc-typelits-extra) -[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-extra.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-extra) - -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](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max) -* `GHC.TypeLits.Extra.Min`: type-level [min](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min) -* `GHC.TypeLits.Extra.Div`: type-level [div](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div) -* `GHC.TypeLits.Extra.Mod`: type-level [mod](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod) -* `GHC.TypeLits.Extra.FLog`: type-level equivalent of [integerLogBase#](https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-) - .i.e. the exact integer equivalent to "`floor (logBase x y)`" -* `GHC.TypeLits.Extra.CLog`: type-level equivalent of _the ceiling of_ [integerLogBase#](https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-) - .i.e. the exact integer equivalent to "`ceiling (logBase x y)`" -* 'GHC.TypeLits.Extra.Log': type-level equivalent of - where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`" -* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd) -* `GHC.TypeLits.Extra.LCM`: a type-level [lcm](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm) +# ghc-typelits-extra + +[![Build Status](https://github.com/clash-lang/ghc-typelits-extra/actions/workflows/haskell-ci.yml/badge.svg?branch=master)](https://github.com/clash-lang/ghc-typelits-extra/actions) +[![Hackage](https://img.shields.io/hackage/v/ghc-typelits-extra.svg)](https://hackage.haskell.org/package/ghc-typelits-extra) +[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-extra.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-extra) + +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](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max) +* `GHC.TypeLits.Extra.Min`: type-level [min](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min) +* `GHC.TypeLits.Extra.Div`: type-level [div](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div) +* `GHC.TypeLits.Extra.Mod`: type-level [mod](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod) +* `GHC.TypeLits.Extra.FLog`: type-level equivalent of [integerLogBase#](https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-) + .i.e. the exact integer equivalent to "`floor (logBase x y)`" +* `GHC.TypeLits.Extra.CLog`: type-level equivalent of _the ceiling of_ [integerLogBase#](https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-) + .i.e. the exact integer equivalent to "`ceiling (logBase x y)`" +* 'GHC.TypeLits.Extra.Log': type-level equivalent of + where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`" +* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd) +* `GHC.TypeLits.Extra.LCM`: a type-level [lcm](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm) diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple -main = defaultMain +import Distribution.Simple +main = defaultMain diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal --- a/ghc-typelits-extra.cabal +++ b/ghc-typelits-extra.cabal @@ -1,125 +1,129 @@ -name: ghc-typelits-extra -version: 0.4.7 -synopsis: Additional type-level operations on GHC.TypeLits.Nat -description: - Additional type-level operations on @GHC.TypeLits.Nat@: - . - * @Max@: type-level - . - * @Min@: type-level - . - * @Div@: type-level - . - * @Mod@: type-level - . - * @FLog@: type-level equivalent of - i.e. the exact integer equivalent to @floor (logBase x y)@ - . - * @CLog@: type-level equivalent of /the ceiling of/ - i.e. the exact integer equivalent to @ceiling (logBase x y)@ - . - * @Log@: type-level equivalent of - where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@ - . - * @GCD@: a type-level - . - * @LCM@: a type-level - . - And a custom solver for the above operations defined in - @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, - add the - . - @ - OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver - @ - . - pragma to the header of your file. -homepage: http://www.clash-lang.org/ -bug-reports: http://github.com/clash-lang/ghc-typelits-extra/issues -license: BSD2 -license-file: LICENSE -author: Christiaan Baaij -maintainer: christiaan.baaij@gmail.com -copyright: Copyright © 2015-2016, University of Twente, - 2017-2018, QBayLogic B.V. -category: Type System -build-type: Simple -extra-source-files: README.md - CHANGELOG.md -cabal-version: >=1.10 -tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, - GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, - GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.2, GHC == 9.10.1 - - -source-repository head - type: git - location: https://github.com/clash-lang/ghc-typelits-extra.git - -flag deverror - description: - Enables `-Werror` for development mode and TravisCI - default: False - manual: True - -library - exposed-modules: GHC.TypeLits.Extra, - GHC.TypeLits.Extra.Solver - other-modules: GHC.TypeLits.Extra.Solver.Unify - GHC.TypeLits.Extra.Solver.Operations - build-depends: base >= 4.8 && <5, - containers >= 0.5.7.1 && <0.8, - ghc >= 7.10 && <9.12, - ghc-prim >= 0.5 && <1.0, - ghc-tcplugins-extra >= 0.3.1, - ghc-typelits-knownnat >= 0.7.2 && <0.8, - ghc-typelits-natnormalise >= 0.7.1 && <0.8, - transformers >= 0.4.2.0 && <0.7 - if impl(ghc >= 9.0.0) - build-depends: ghc-bignum >=1.0 && <1.4 - else - build-depends: integer-gmp >=1.0 && <1.1 - hs-source-dirs: src - if impl(ghc >= 8.0) && impl(ghc < 9.4) - hs-source-dirs: src-pre-ghc-9.4 - if impl(ghc >= 9.4) && impl(ghc < 9.12) - hs-source-dirs: src-ghc-9.4 - build-depends: template-haskell >= 2.17 && <2.23 - default-language: Haskell2010 - other-extensions: DataKinds - FlexibleInstances - GADTs - MagicHash - MultiParamTypeClasses - ScopedTypeVariables - TemplateHaskell - TupleSections - TypeApplications - TypeFamilies - TypeOperators - UndecidableInstances - if flag(deverror) - ghc-options: -Wall -Werror - else - ghc-options: -Wall - -test-suite test-ghc-typelits-extra - type: exitcode-stdio-1.0 - main-is: Main.hs - Other-Modules: ErrorTests - build-depends: base >= 4.8 && <5, - ghc-typelits-extra, - ghc-typelits-knownnat >= 0.7.2, - ghc-typelits-natnormalise >= 0.7.1, - tasty >= 0.10, - tasty-hunit >= 0.9 - hs-source-dirs: tests - if impl(ghc >= 8.0) && impl(ghc < 9.4) - hs-source-dirs: tests-pre-ghc-9.4 - if impl(ghc >= 9.4) && impl(ghc < 9.12) - hs-source-dirs: tests-ghc-9.4 - default-language: Haskell2010 - other-extensions: DataKinds - TypeOperators - if flag(deverror) - ghc-options: -dcore-lint +name: ghc-typelits-extra +version: 0.4.8 +synopsis: Additional type-level operations on GHC.TypeLits.Nat +description: + Additional type-level operations on @GHC.TypeLits.Nat@: + . + * @Max@: type-level + . + * @Min@: type-level + . + * @Div@: type-level + . + * @Mod@: type-level + . + * @FLog@: type-level equivalent of + i.e. the exact integer equivalent to @floor (logBase x y)@ + . + * @CLog@: type-level equivalent of /the ceiling of/ + i.e. the exact integer equivalent to @ceiling (logBase x y)@ + . + * @Log@: type-level equivalent of + where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@ + . + * @GCD@: a type-level + . + * @LCM@: a type-level + . + And a custom solver for the above operations defined in + @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, + add the + . + @ + OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver + @ + . + pragma to the header of your file. +homepage: http://www.clash-lang.org/ +bug-reports: http://github.com/clash-lang/ghc-typelits-extra/issues +license: BSD2 +license-file: LICENSE +author: Christiaan Baaij +maintainer: christiaan.baaij@gmail.com +copyright: Copyright © 2015-2016, University of Twente, + 2017-2018, QBayLogic B.V. +category: Type System +build-type: Simple +extra-source-files: README.md + CHANGELOG.md +cabal-version: >=1.10 +tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, + GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8, + GHC == 9.4.8, GHC == 9.6.6, GHC == 9.8.4, GHC == 9.10.1, + GHC == 9.12.1 + + +source-repository head + type: git + location: https://github.com/clash-lang/ghc-typelits-extra.git + +flag deverror + description: + Enables `-Werror` for development mode and TravisCI + default: False + manual: True + +library + exposed-modules: GHC.TypeLits.Extra, + GHC.TypeLits.Extra.Solver + other-modules: GHC.TypeLits.Extra.Solver.Unify + GHC.TypeLits.Extra.Solver.Operations + build-depends: base >= 4.8 && <5, + containers >= 0.5.7.1 && <0.8, + ghc >= 7.10 && <9.13, + ghc-prim >= 0.5 && <1.0, + ghc-tcplugins-extra >= 0.3.1, + ghc-typelits-knownnat >= 0.7.2 && <0.8, + ghc-typelits-natnormalise >= 0.7.1 && <0.8, + transformers >= 0.4.2.0 && <0.7 + if impl(ghc >= 9.0.0) + build-depends: ghc-bignum >=1.0 && <1.4 + else + build-depends: integer-gmp >=1.0 && <1.1 + hs-source-dirs: src + if impl(ghc >= 8.0) && impl(ghc < 9.4) + hs-source-dirs: src-pre-ghc-9.4 + if impl(ghc >= 9.4) && impl(ghc < 9.11) + hs-source-dirs: src-ghc-9.4 + build-depends: template-haskell >= 2.17 && <2.23 + if impl(ghc >= 9.11) && impl(ghc < 9.13) + hs-source-dirs: src-ghc-9.12 + build-depends: template-haskell >= 2.17 && <2.24 + default-language: Haskell2010 + other-extensions: DataKinds + FlexibleInstances + GADTs + MagicHash + MultiParamTypeClasses + ScopedTypeVariables + TemplateHaskell + TupleSections + TypeApplications + TypeFamilies + TypeOperators + UndecidableInstances + if flag(deverror) + ghc-options: -Wall -Werror + else + ghc-options: -Wall + +test-suite test-ghc-typelits-extra + type: exitcode-stdio-1.0 + main-is: Main.hs + Other-Modules: ErrorTests + build-depends: base >= 4.8 && <5, + ghc-typelits-extra, + ghc-typelits-knownnat >= 0.7.2, + ghc-typelits-natnormalise >= 0.7.1, + tasty >= 0.10, + tasty-hunit >= 0.9 + hs-source-dirs: tests + if impl(ghc >= 8.0) && impl(ghc < 9.4) + hs-source-dirs: tests-pre-ghc-9.4 + if impl(ghc >= 9.4) && impl(ghc < 9.13) + hs-source-dirs: tests-ghc-9.4 + default-language: Haskell2010 + other-extensions: DataKinds + TypeOperators + if flag(deverror) + ghc-options: -dcore-lint diff --git a/src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs b/src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs new file mode 100644 --- /dev/null +++ b/src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs @@ -0,0 +1,349 @@ +{-| +Copyright : (C) 2015-2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +To use the plugin, add the + +@ +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +@ + +pragma to the header of your file + +-} + +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.Extra.Solver + ( plugin ) +where + +-- external +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Data.Maybe (catMaybes) +import GHC.TcPluginM.Extra (evByFiatWithDependencies, tracePlugin, newWanted) +import qualified Data.Type.Ord +import qualified GHC.TypeError + +-- GHC API +import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique) +import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon) +import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon) +import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon) +import GHC.Core.Coercion (Coercion, mkUnivCo) +import GHC.Core.DataCon (dataConWrapId) +import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType) +import GHC.Core.Reduction (Reduction(..)) +import GHC.Core.TyCon (TyCon) +import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv)) +import GHC.Core.Type (Kind, mkTyConApp, splitTyConApp_maybe, typeKind) +import GHC.Core.TyCo.Compare (eqType) +import GHC.Data.IOEnv (getEnv) +import GHC.Driver.Env (hsc_NC) +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) +import GHC.Plugins (thNameToGhcNameIO) +import GHC.Tc.Plugin + (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM) +import GHC.Tc.Types + (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..), + Env (env_top)) +import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt) +import GHC.Tc.Types.Constraint + (Ct (..), DictCt(..), EqCt(..), IrredCt(..), ctEvCoercion, qci_ev) +import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId) +import GHC.Types.Unique.FM (UniqFM, listToUFM) +import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) +import GHC (Name) + +-- template-haskell +import qualified Language.Haskell.TH as TH + +-- internal +import GHC.TypeLits.Extra.Solver.Operations +import GHC.TypeLits.Extra.Solver.Unify +import GHC.TypeLits.Extra + +-- | A solver implement as a type-checker plugin for: +-- +-- * 'Div': type-level 'div' +-- +-- * 'Mod': type-level 'mod' +-- +-- * 'FLog': type-level equivalent of +-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" +-- +-- * 'CLog': type-level equivalent of /the ceiling of/ +-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" +-- +-- * 'Log': type-level equivalent of +-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" +-- +-- * 'GCD': a type-level 'gcd' +-- +-- * 'LCM': a type-level 'lcm' +-- +-- To use the plugin, add +-- +-- @ +-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +-- @ +-- +-- To the header of your file. +plugin :: Plugin +plugin + = defaultPlugin + { tcPlugin = const $ Just normalisePlugin + , pluginRecompile = purePlugin + } + +normalisePlugin :: TcPlugin +normalisePlugin = tracePlugin "ghc-typelits-extra" + TcPlugin { tcPluginInit = lookupExtraDefs + , tcPluginSolve = decideEqualSOP + , tcPluginRewrite = extraRewrite + , tcPluginStop = const (return ()) + } + +extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter +extraRewrite defs = listToUFM + [ (gcdTyCon defs, gcdRewrite) + , (lcmTyCon defs, lcmRewrite) + ] + where + gcdRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ + TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) [] + gcdRewrite _ _ _ = pure TcPluginNoRewrite + + lcmRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ + TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) [] + lcmRewrite _ _ _ = pure TcPluginNoRewrite + + reduce tc args res = Reduction co res + where + co = mkUnivCo (PluginProv "ghc-typelits-extra") [] Nominal + (mkTyConApp tc args) res + + +decideEqualSOP :: ExtraDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult +decideEqualSOP _ _ _givens [] = return (TcPluginOk [] []) +decideEqualSOP defs _ givens wanteds = do + unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds + case unit_wanteds of + [] -> return (TcPluginOk [] []) + _ -> do + unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) givens + sr <- simplifyExtra defs (unit_givens ++ unit_wanteds) + tcPluginTrace "normalised" (ppr sr) + case sr of + Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new) + Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq]) + +data SolverConstraint + = NatEquality Ct ExtraOp ExtraOp Normalised + | NatInequality Ct [Coercion] ExtraOp ExtraOp Bool Normalised + +instance Outputable SolverConstraint where + ppr (NatEquality ct op1 op2 norm) = + text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm + ppr (NatInequality _ _ op1 op2 b norm) = + text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm + +data SimplifyResult + = Simplified [(EvTerm,Ct)] [Ct] + | Impossible SolverConstraint + +instance Outputable SimplifyResult where + ppr (Simplified evs new) = + text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new + ppr (Impossible sct) = + text "Impossible" <+> ppr sct + +simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult +simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs + where + simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult + simples evs news [] = return (Simplified (catMaybes evs) news) + simples evs news (eq@(NatEquality ct u v norm):eqs') = do + ur <- unifyExtra ct u v + tcPluginTrace "unifyExtra result" (ppr ur) + case ur of + Win -> simples (((,) <$> evMagic ct [] <*> pure ct):evs) news eqs' + Lose | null evs && null eqs' -> return (Impossible eq) + _ | norm == Normalised && isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (((,) <$> evMagic ct [] <*> pure ct):evs) (newCt:news) eqs' + Lose -> simples evs news eqs' + Draw -> simples evs news eqs' + simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do + tcPluginTrace "unifyExtra leq result" (ppr (u,v,b)) + case (u,v) of + (I i,I j) + | (i <= j) == b -> simples (((,) <$> evMagic ct deps <*> pure ct):evs) news eqs' + | otherwise -> return (Impossible eq) + (p, Max x y) + | b && (p == x || p == y) + -> simples (((,) <$> evMagic ct deps <*> pure ct):evs) news eqs' + + -- transform: q ~ Max x y => (p <=? q ~ True) + -- to: (p <=? Max x y) ~ True + -- and try to solve that along with the rest of the eqs' + (p, q@(V _)) + | b -> case findMax q eqs of + Just (i,m) -> + simples evs news + (NatInequality ct (i:deps) p m b norm:eqs') + Nothing -> simples evs news eqs' + _ | norm == Normalised && isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (((,) <$> evMagic ct deps <*> pure ct):evs) (newCt:news) eqs' + _ -> simples evs news eqs' + + -- look for given constraint with the form: c ~ Max x y + findMax :: ExtraOp -> [SolverConstraint] -> Maybe (Coercion, ExtraOp) + findMax c = go + where + go [] = Nothing + go ((NatEquality ct a b@(Max _ _) _) :_) + | c == a && not (isWantedCt ct) + = Just (ctEvCoercion (ctEvidence ct), b) + go ((NatEquality ct a@(Max _ _) b _) :_) + | c == b && not (isWantedCt ct) + = Just (ctEvCoercion (ctEvidence ct), a) + go (_:rest) = go rest + + +-- Extract the Nat equality constraints +toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint +toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 + | isNatKind (typeKind t1) || isNatKind (typeKind t2) + -> do + (t1', n1) <- normaliseNat defs t1 + (t2', n2) <- normaliseNat defs t2 + pure (NatEquality ct t1' t2' (mergeNormalised n1 n2)) + | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1 + , tc == ordTyCon defs + , TyConApp cmpNatTc [x,y] <- cmpNat + , cmpNatTc == typeNatCmpTyCon + , tt1 == promotedTrueDataCon + , tt2 == promotedTrueDataCon + , ff1 == promotedFalseDataCon + , TyConApp tc' [] <- t2 + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + let res | tc' == promotedTrueDataCon + = pure (NatInequality ct [] x' y' True + (mergeNormalised n1 n2)) + | tc' == promotedFalseDataCon + = pure (NatInequality ct [] x' y' False + (mergeNormalised n1 n2)) + | otherwise = fail "Nothing" + res + | TyConApp tc [TyConApp ordCondTc zs, _] <- t1 + , tc == assertTC defs + , TyConApp tc' [] <- t2 + , tc' == cTupleTyCon 0 + , ordCondTc == ordTyCon defs + , [_,cmp,lt,eq,gt] <- zs + , TyConApp tcCmpNat [x,y] <- cmp + , tcCmpNat == typeNatCmpTyCon + , TyConApp ltTc [] <- lt + , ltTc == promotedTrueDataCon + , TyConApp eqTc [] <- eq + , eqTc == promotedTrueDataCon + , TyConApp gtTc [] <- gt + , gtTc == promotedFalseDataCon + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + pure (NatInequality ct [] x' y' True (mergeNormalised n1 n2)) + IrredPred (TyConApp tc [TyConApp ordCondTc zs, _]) + | tc == assertTC defs + , ordCondTc == ordTyCon defs + , [_,cmp,lt,eq,gt] <- zs + , TyConApp tcCmpNat [x,y] <- cmp + , tcCmpNat == typeNatCmpTyCon + , TyConApp ltTc [] <- lt + , ltTc == promotedTrueDataCon + , TyConApp eqTc [] <- eq + , eqTc == promotedTrueDataCon + , TyConApp gtTc [] <- gt + , gtTc == promotedFalseDataCon + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + pure (NatInequality ct [] x' y' True (mergeNormalised n1 n2)) + _ -> fail "Nothing" + where + isNatKind :: Kind -> Bool + isNatKind = (`eqType` naturalTy) + +createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct +createWantedFromNormalised defs sct = do + let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2) + extractCtSides (NatInequality ct _ x y b _) = + let tc = if b then promotedTrueDataCon else promotedFalseDataCon + t1 = TyConApp (ordTyCon defs) + [ boolTy + , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y] + , TyConApp promotedTrueDataCon [] + , TyConApp promotedTrueDataCon [] + , TyConApp promotedFalseDataCon [] + ] + t2 = TyConApp tc [] + in (ct, t1, t2) + let (ct, t1, t2) = extractCtSides sct + newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of + Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2]) + Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b]) + _ -> error "Impossible: neither (<=?) nor Assert" + ev <- newWanted (ctLoc ct) newPredTy + let ctN = case ct of + CQuantCan qc -> CQuantCan (qc { qci_ev = ev}) + CDictCan di -> CDictCan (di { di_ev = ev}) + CIrredCan ir -> CIrredCan (ir { ir_ev = ev}) + CEqCan eq -> CEqCan (eq { eq_ev = ev}) + CNonCanonical _ -> CNonCanonical ev + return ctN + +fromSolverConstraint :: SolverConstraint -> Ct +fromSolverConstraint (NatEquality ct _ _ _) = ct +fromSolverConstraint (NatInequality ct _ _ _ _ _) = ct + +lookupExtraDefs :: TcPluginM ExtraDefs +lookupExtraDefs = do + ExtraDefs <$> look ''GHC.TypeLits.Extra.Max + <*> look ''GHC.TypeLits.Extra.Min + <*> pure typeNatDivTyCon + <*> pure typeNatModTyCon + <*> look ''GHC.TypeLits.Extra.FLog + <*> look ''GHC.TypeLits.Extra.CLog + <*> look ''GHC.TypeLits.Extra.Log + <*> look ''GHC.TypeLits.Extra.GCD + <*> look ''GHC.TypeLits.Extra.LCM + <*> look ''Data.Type.Ord.OrdCond + <*> look ''GHC.TypeError.Assert + where + look nm = tcLookupTyCon =<< lookupTHName nm + +lookupTHName :: TH.Name -> TcPluginM Name +lookupTHName th = do + nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv) + res <- tcPluginIO $ thNameToGhcNameIO nc th + maybe (fail $ "Failed to lookup " ++ show th) return res + +-- Utils +evMagic :: Ct -> [Coercion] -> Maybe EvTerm +evMagic ct deps = case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 -> Just (evByFiatWithDependencies "ghc-typelits-extra" deps t1 t2) + IrredPred p -> + let t1 = mkTyConApp (cTupleTyCon 0) [] + co = mkUnivCo (PluginProv "ghc-typelits-extra") deps Representational t1 p + dcApp = evId (dataConWrapId (cTupleDataCon 0)) + in Just (evCast dcApp co) + _ -> Nothing diff --git a/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs b/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs --- a/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +++ b/src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs @@ -1,348 +1,348 @@ -{-| -Copyright : (C) 2015-2016, University of Twente -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -To use the plugin, add the - -@ -{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} -@ - -pragma to the header of your file - --} - -{-# LANGUAGE CPP #-} -{-# LANGUAGE TupleSections #-} -{-# LANGUAGE TemplateHaskellQuotes #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -module GHC.TypeLits.Extra.Solver - ( plugin ) -where - --- external -import Control.Monad.Trans.Maybe (MaybeT (..)) -import Data.Maybe (catMaybes) -import GHC.TcPluginM.Extra (evByFiat, tracePlugin, newWanted) -import qualified Data.Type.Ord -import qualified GHC.TypeError - --- GHC API -import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique) -import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon) -import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon) -import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon) -import GHC.Core.Coercion (mkUnivCo) -import GHC.Core.DataCon (dataConWrapId) -import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType) -import GHC.Core.Reduction (Reduction(..)) -import GHC.Core.TyCon (TyCon) -import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv)) -import GHC.Core.Type (Kind, mkTyConApp, splitTyConApp_maybe, typeKind) -#if MIN_VERSION_ghc(9,6,0) -import GHC.Core.TyCo.Compare (eqType) -#else -import GHC.Core.Type (eqType) -#endif -import GHC.Data.IOEnv (getEnv) -import GHC.Driver.Env (hsc_NC) -import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) -import GHC.Plugins (thNameToGhcNameIO) -import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM) -import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..), Env (env_top)) -import GHC.Tc.Types.Constraint - (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt) -#if MIN_VERSION_ghc(9,8,0) -import GHC.Tc.Types.Constraint (Ct (..), DictCt(..), EqCt(..), IrredCt(..), qci_ev) -#else -import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev, cc_ev) -#endif -import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId) -import GHC.Types.Unique.FM (UniqFM, listToUFM) -import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) -import GHC (Name) - --- template-haskell -import qualified Language.Haskell.TH as TH - --- internal -import GHC.TypeLits.Extra.Solver.Operations -import GHC.TypeLits.Extra.Solver.Unify -import GHC.TypeLits.Extra - --- | A solver implement as a type-checker plugin for: --- --- * 'Div': type-level 'div' --- --- * 'Mod': type-level 'mod' --- --- * 'FLog': type-level equivalent of --- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" --- --- * 'CLog': type-level equivalent of /the ceiling of/ --- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" --- --- * 'Log': type-level equivalent of --- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" --- --- * 'GCD': a type-level 'gcd' --- --- * 'LCM': a type-level 'lcm' --- --- To use the plugin, add --- --- @ --- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} --- @ --- --- To the header of your file. -plugin :: Plugin -plugin - = defaultPlugin - { tcPlugin = const $ Just normalisePlugin - , pluginRecompile = purePlugin - } - -normalisePlugin :: TcPlugin -normalisePlugin = tracePlugin "ghc-typelits-extra" - TcPlugin { tcPluginInit = lookupExtraDefs - , tcPluginSolve = decideEqualSOP - , tcPluginRewrite = extraRewrite - , tcPluginStop = const (return ()) - } - -extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter -extraRewrite defs = listToUFM - [ (gcdTyCon defs, gcdRewrite) - , (lcmTyCon defs, lcmRewrite) - ] - where - gcdRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ - TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) [] - gcdRewrite _ _ _ = pure TcPluginNoRewrite - - lcmRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ - TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) [] - lcmRewrite _ _ _ = pure TcPluginNoRewrite - - reduce tc args res = Reduction co res - where - co = mkUnivCo (PluginProv "ghc-typelits-extra") Nominal - (mkTyConApp tc args) res - - -decideEqualSOP :: ExtraDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult -decideEqualSOP _ _ _givens [] = return (TcPluginOk [] []) -decideEqualSOP defs _ givens wanteds = do - unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds - case unit_wanteds of - [] -> return (TcPluginOk [] []) - _ -> do - unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) givens - sr <- simplifyExtra defs (unit_givens ++ unit_wanteds) - tcPluginTrace "normalised" (ppr sr) - case sr of - Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new) - Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq]) - -data SolverConstraint - = NatEquality Ct ExtraOp ExtraOp Normalised - | NatInequality Ct ExtraOp ExtraOp Bool Normalised - -instance Outputable SolverConstraint where - ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm - ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm - -data SimplifyResult - = Simplified [(EvTerm,Ct)] [Ct] - | Impossible SolverConstraint - -instance Outputable SimplifyResult where - ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new - ppr (Impossible sct) = text "Impossible" <+> ppr sct - -simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult -simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs - where - simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult - simples evs news [] = return (Simplified (catMaybes evs) news) - simples evs news (eq@(NatEquality ct u v norm):eqs') = do - ur <- unifyExtra ct u v - tcPluginTrace "unifyExtra result" (ppr ur) - case ur of - Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' - Lose | null evs && null eqs' -> return (Impossible eq) - _ | norm == Normalised && isWantedCt ct -> do - newCt <- createWantedFromNormalised defs eq - simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' - Lose -> simples evs news eqs' - Draw -> simples evs news eqs' - simples evs news (eq@(NatInequality ct u v b norm):eqs') = do - tcPluginTrace "unifyExtra leq result" (ppr (u,v,b)) - case (u,v) of - (I i,I j) - | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' - | otherwise -> return (Impossible eq) - (p, Max x y) - | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' - - -- transform: q ~ Max x y => (p <=? q ~ True) - -- to: (p <=? Max x y) ~ True - -- and try to solve that along with the rest of the eqs' - (p, q@(V _)) - | b -> case findMax q eqs of - Just m -> simples evs news (NatInequality ct p m b norm:eqs') - Nothing -> simples evs news eqs' - _ | norm == Normalised && isWantedCt ct -> do - newCt <- createWantedFromNormalised defs eq - simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' - _ -> simples evs news eqs' - - -- look for given constraint with the form: c ~ Max x y - findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp - findMax c = go - where - go [] = Nothing - go ((NatEquality ct a b@(Max _ _) _) :_) - | c == a && not (isWantedCt ct) - = Just b - go ((NatEquality ct a@(Max _ _) b _) :_) - | c == b && not (isWantedCt ct) - = Just a - go (_:rest) = go rest - - --- Extract the Nat equality constraints -toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint -toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - | isNatKind (typeKind t1) || isNatKind (typeKind t2) - -> do - (t1', n1) <- normaliseNat defs t1 - (t2', n2) <- normaliseNat defs t2 - pure (NatEquality ct t1' t2' (mergeNormalised n1 n2)) - | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1 - , tc == ordTyCon defs - , TyConApp cmpNatTc [x,y] <- cmpNat - , cmpNatTc == typeNatCmpTyCon - , tt1 == promotedTrueDataCon - , tt2 == promotedTrueDataCon - , ff1 == promotedFalseDataCon - , TyConApp tc' [] <- t2 - -> do - (x', n1) <- normaliseNat defs x - (y', n2) <- normaliseNat defs y - let res | tc' == promotedTrueDataCon = pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) - | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2)) - | otherwise = fail "Nothing" - res - | TyConApp tc [TyConApp ordCondTc zs, _] <- t1 - , tc == assertTC defs - , TyConApp tc' [] <- t2 - , tc' == cTupleTyCon 0 - , ordCondTc == ordTyCon defs - , [_,cmp,lt,eq,gt] <- zs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - -> do - (x', n1) <- normaliseNat defs x - (y', n2) <- normaliseNat defs y - pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) - IrredPred (TyConApp tc [TyConApp ordCondTc zs, _]) - | tc == assertTC defs - , ordCondTc == ordTyCon defs - , [_,cmp,lt,eq,gt] <- zs - , TyConApp tcCmpNat [x,y] <- cmp - , tcCmpNat == typeNatCmpTyCon - , TyConApp ltTc [] <- lt - , ltTc == promotedTrueDataCon - , TyConApp eqTc [] <- eq - , eqTc == promotedTrueDataCon - , TyConApp gtTc [] <- gt - , gtTc == promotedFalseDataCon - -> do - (x', n1) <- normaliseNat defs x - (y', n2) <- normaliseNat defs y - pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) - _ -> fail "Nothing" - where - isNatKind :: Kind -> Bool - isNatKind = (`eqType` naturalTy) - -createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct -createWantedFromNormalised defs sct = do - let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2) - extractCtSides (NatInequality ct x y b _) = - let tc = if b then promotedTrueDataCon else promotedFalseDataCon - t1 = TyConApp (ordTyCon defs) - [ boolTy - , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y] - , TyConApp promotedTrueDataCon [] - , TyConApp promotedTrueDataCon [] - , TyConApp promotedFalseDataCon [] - ] - t2 = TyConApp tc [] - in (ct, t1, t2) - let (ct, t1, t2) = extractCtSides sct - newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of - Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2]) - Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b]) - _ -> error "Impossible: neither (<=?) nor Assert" - ev <- newWanted (ctLoc ct) newPredTy - let ctN = case ct of - CQuantCan qc -> CQuantCan (qc { qci_ev = ev}) -#if MIN_VERSION_ghc(9,8,0) - CDictCan di -> CDictCan (di { di_ev = ev}) - CIrredCan ir -> CIrredCan (ir { ir_ev = ev}) - CEqCan eq -> CEqCan (eq { eq_ev = ev}) - CNonCanonical _ -> CNonCanonical ev -#else - ctX -> ctX { cc_ev = ev } -#endif - return ctN - -fromSolverConstraint :: SolverConstraint -> Ct -fromSolverConstraint (NatEquality ct _ _ _) = ct -fromSolverConstraint (NatInequality ct _ _ _ _) = ct - -lookupExtraDefs :: TcPluginM ExtraDefs -lookupExtraDefs = do - ExtraDefs <$> look ''GHC.TypeLits.Extra.Max - <*> look ''GHC.TypeLits.Extra.Min - <*> pure typeNatDivTyCon - <*> pure typeNatModTyCon - <*> look ''GHC.TypeLits.Extra.FLog - <*> look ''GHC.TypeLits.Extra.CLog - <*> look ''GHC.TypeLits.Extra.Log - <*> look ''GHC.TypeLits.Extra.GCD - <*> look ''GHC.TypeLits.Extra.LCM - <*> look ''Data.Type.Ord.OrdCond - <*> look ''GHC.TypeError.Assert - where - look nm = tcLookupTyCon =<< lookupTHName nm - -lookupTHName :: TH.Name -> TcPluginM Name -lookupTHName th = do - nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv) - res <- tcPluginIO $ thNameToGhcNameIO nc th - maybe (fail $ "Failed to lookup " ++ show th) return res - --- Utils -evMagic :: Ct -> Maybe EvTerm -evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2) - IrredPred p -> - let t1 = mkTyConApp (cTupleTyCon 0) [] - co = mkUnivCo (PluginProv "ghc-typelits-extra") Representational t1 p - dcApp = evId (dataConWrapId (cTupleDataCon 0)) - in Just (evCast dcApp co) - _ -> Nothing +{-| +Copyright : (C) 2015-2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +To use the plugin, add the + +@ +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +@ + +pragma to the header of your file + +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TemplateHaskellQuotes #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.Extra.Solver + ( plugin ) +where + +-- external +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Data.Maybe (catMaybes) +import GHC.TcPluginM.Extra (evByFiat, tracePlugin, newWanted) +import qualified Data.Type.Ord +import qualified GHC.TypeError + +-- GHC API +import GHC.Builtin.Names (eqPrimTyConKey, hasKey, getUnique) +import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon) +import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon) +import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon, typeNatCmpTyCon) +import GHC.Core.Coercion (mkUnivCo) +import GHC.Core.DataCon (dataConWrapId) +import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred, IrredPred), classifyPredType) +import GHC.Core.Reduction (Reduction(..)) +import GHC.Core.TyCon (TyCon) +import GHC.Core.TyCo.Rep (Type (..), TyLit (..), UnivCoProvenance (PluginProv)) +import GHC.Core.Type (Kind, mkTyConApp, splitTyConApp_maybe, typeKind) +#if MIN_VERSION_ghc(9,6,0) +import GHC.Core.TyCo.Compare (eqType) +#else +import GHC.Core.Type (eqType) +#endif +import GHC.Data.IOEnv (getEnv) +import GHC.Driver.Env (hsc_NC) +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) +import GHC.Plugins (thNameToGhcNameIO) +import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace, tcPluginIO, unsafeTcPluginTcM) +import GHC.Tc.Types (TcPlugin(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..), Env (env_top)) +import GHC.Tc.Types.Constraint + (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt) +#if MIN_VERSION_ghc(9,8,0) +import GHC.Tc.Types.Constraint (Ct (..), DictCt(..), EqCt(..), IrredCt(..), qci_ev) +#else +import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev, cc_ev) +#endif +import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId) +import GHC.Types.Unique.FM (UniqFM, listToUFM) +import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) +import GHC (Name) + +-- template-haskell +import qualified Language.Haskell.TH as TH + +-- internal +import GHC.TypeLits.Extra.Solver.Operations +import GHC.TypeLits.Extra.Solver.Unify +import GHC.TypeLits.Extra + +-- | A solver implement as a type-checker plugin for: +-- +-- * 'Div': type-level 'div' +-- +-- * 'Mod': type-level 'mod' +-- +-- * 'FLog': type-level equivalent of +-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" +-- +-- * 'CLog': type-level equivalent of /the ceiling of/ +-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" +-- +-- * 'Log': type-level equivalent of +-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" +-- +-- * 'GCD': a type-level 'gcd' +-- +-- * 'LCM': a type-level 'lcm' +-- +-- To use the plugin, add +-- +-- @ +-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +-- @ +-- +-- To the header of your file. +plugin :: Plugin +plugin + = defaultPlugin + { tcPlugin = const $ Just normalisePlugin + , pluginRecompile = purePlugin + } + +normalisePlugin :: TcPlugin +normalisePlugin = tracePlugin "ghc-typelits-extra" + TcPlugin { tcPluginInit = lookupExtraDefs + , tcPluginSolve = decideEqualSOP + , tcPluginRewrite = extraRewrite + , tcPluginStop = const (return ()) + } + +extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter +extraRewrite defs = listToUFM + [ (gcdTyCon defs, gcdRewrite) + , (lcmTyCon defs, lcmRewrite) + ] + where + gcdRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ + TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) [] + gcdRewrite _ _ _ = pure TcPluginNoRewrite + + lcmRewrite _ _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ + TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) [] + lcmRewrite _ _ _ = pure TcPluginNoRewrite + + reduce tc args res = Reduction co res + where + co = mkUnivCo (PluginProv "ghc-typelits-extra") Nominal + (mkTyConApp tc args) res + + +decideEqualSOP :: ExtraDefs -> EvBindsVar -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult +decideEqualSOP _ _ _givens [] = return (TcPluginOk [] []) +decideEqualSOP defs _ givens wanteds = do + unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds + case unit_wanteds of + [] -> return (TcPluginOk [] []) + _ -> do + unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) givens + sr <- simplifyExtra defs (unit_givens ++ unit_wanteds) + tcPluginTrace "normalised" (ppr sr) + case sr of + Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new) + Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq]) + +data SolverConstraint + = NatEquality Ct ExtraOp ExtraOp Normalised + | NatInequality Ct ExtraOp ExtraOp Bool Normalised + +instance Outputable SolverConstraint where + ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm + ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm + +data SimplifyResult + = Simplified [(EvTerm,Ct)] [Ct] + | Impossible SolverConstraint + +instance Outputable SimplifyResult where + ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new + ppr (Impossible sct) = text "Impossible" <+> ppr sct + +simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult +simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs + where + simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult + simples evs news [] = return (Simplified (catMaybes evs) news) + simples evs news (eq@(NatEquality ct u v norm):eqs') = do + ur <- unifyExtra ct u v + tcPluginTrace "unifyExtra result" (ppr ur) + case ur of + Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' + Lose | null evs && null eqs' -> return (Impossible eq) + _ | norm == Normalised && isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' + Lose -> simples evs news eqs' + Draw -> simples evs news eqs' + simples evs news (eq@(NatInequality ct u v b norm):eqs') = do + tcPluginTrace "unifyExtra leq result" (ppr (u,v,b)) + case (u,v) of + (I i,I j) + | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' + | otherwise -> return (Impossible eq) + (p, Max x y) + | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' + + -- transform: q ~ Max x y => (p <=? q ~ True) + -- to: (p <=? Max x y) ~ True + -- and try to solve that along with the rest of the eqs' + (p, q@(V _)) + | b -> case findMax q eqs of + Just m -> simples evs news (NatInequality ct p m b norm:eqs') + Nothing -> simples evs news eqs' + _ | norm == Normalised && isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' + _ -> simples evs news eqs' + + -- look for given constraint with the form: c ~ Max x y + findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp + findMax c = go + where + go [] = Nothing + go ((NatEquality ct a b@(Max _ _) _) :_) + | c == a && not (isWantedCt ct) + = Just b + go ((NatEquality ct a@(Max _ _) b _) :_) + | c == b && not (isWantedCt ct) + = Just a + go (_:rest) = go rest + + +-- Extract the Nat equality constraints +toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint +toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 + | isNatKind (typeKind t1) || isNatKind (typeKind t2) + -> do + (t1', n1) <- normaliseNat defs t1 + (t2', n2) <- normaliseNat defs t2 + pure (NatEquality ct t1' t2' (mergeNormalised n1 n2)) + | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1 + , tc == ordTyCon defs + , TyConApp cmpNatTc [x,y] <- cmpNat + , cmpNatTc == typeNatCmpTyCon + , tt1 == promotedTrueDataCon + , tt2 == promotedTrueDataCon + , ff1 == promotedFalseDataCon + , TyConApp tc' [] <- t2 + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + let res | tc' == promotedTrueDataCon = pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) + | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2)) + | otherwise = fail "Nothing" + res + | TyConApp tc [TyConApp ordCondTc zs, _] <- t1 + , tc == assertTC defs + , TyConApp tc' [] <- t2 + , tc' == cTupleTyCon 0 + , ordCondTc == ordTyCon defs + , [_,cmp,lt,eq,gt] <- zs + , TyConApp tcCmpNat [x,y] <- cmp + , tcCmpNat == typeNatCmpTyCon + , TyConApp ltTc [] <- lt + , ltTc == promotedTrueDataCon + , TyConApp eqTc [] <- eq + , eqTc == promotedTrueDataCon + , TyConApp gtTc [] <- gt + , gtTc == promotedFalseDataCon + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) + IrredPred (TyConApp tc [TyConApp ordCondTc zs, _]) + | tc == assertTC defs + , ordCondTc == ordTyCon defs + , [_,cmp,lt,eq,gt] <- zs + , TyConApp tcCmpNat [x,y] <- cmp + , tcCmpNat == typeNatCmpTyCon + , TyConApp ltTc [] <- lt + , ltTc == promotedTrueDataCon + , TyConApp eqTc [] <- eq + , eqTc == promotedTrueDataCon + , TyConApp gtTc [] <- gt + , gtTc == promotedFalseDataCon + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) + _ -> fail "Nothing" + where + isNatKind :: Kind -> Bool + isNatKind = (`eqType` naturalTy) + +createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct +createWantedFromNormalised defs sct = do + let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2) + extractCtSides (NatInequality ct x y b _) = + let tc = if b then promotedTrueDataCon else promotedFalseDataCon + t1 = TyConApp (ordTyCon defs) + [ boolTy + , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y] + , TyConApp promotedTrueDataCon [] + , TyConApp promotedTrueDataCon [] + , TyConApp promotedFalseDataCon [] + ] + t2 = TyConApp tc [] + in (ct, t1, t2) + let (ct, t1, t2) = extractCtSides sct + newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of + Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2]) + Just (tc, [_, b]) | tc `hasKey` getUnique (assertTC defs) -> pure (mkTyConApp tc [t1,b]) + _ -> error "Impossible: neither (<=?) nor Assert" + ev <- newWanted (ctLoc ct) newPredTy + let ctN = case ct of + CQuantCan qc -> CQuantCan (qc { qci_ev = ev}) +#if MIN_VERSION_ghc(9,8,0) + CDictCan di -> CDictCan (di { di_ev = ev}) + CIrredCan ir -> CIrredCan (ir { ir_ev = ev}) + CEqCan eq -> CEqCan (eq { eq_ev = ev}) + CNonCanonical _ -> CNonCanonical ev +#else + ctX -> ctX { cc_ev = ev } +#endif + return ctN + +fromSolverConstraint :: SolverConstraint -> Ct +fromSolverConstraint (NatEquality ct _ _ _) = ct +fromSolverConstraint (NatInequality ct _ _ _ _) = ct + +lookupExtraDefs :: TcPluginM ExtraDefs +lookupExtraDefs = do + ExtraDefs <$> look ''GHC.TypeLits.Extra.Max + <*> look ''GHC.TypeLits.Extra.Min + <*> pure typeNatDivTyCon + <*> pure typeNatModTyCon + <*> look ''GHC.TypeLits.Extra.FLog + <*> look ''GHC.TypeLits.Extra.CLog + <*> look ''GHC.TypeLits.Extra.Log + <*> look ''GHC.TypeLits.Extra.GCD + <*> look ''GHC.TypeLits.Extra.LCM + <*> look ''Data.Type.Ord.OrdCond + <*> look ''GHC.TypeError.Assert + where + look nm = tcLookupTyCon =<< lookupTHName nm + +lookupTHName :: TH.Name -> TcPluginM Name +lookupTHName th = do + nc <- unsafeTcPluginTcM (hsc_NC . env_top <$> getEnv) + res <- tcPluginIO $ thNameToGhcNameIO nc th + maybe (fail $ "Failed to lookup " ++ show th) return res + +-- Utils +evMagic :: Ct -> Maybe EvTerm +evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2) + IrredPred p -> + let t1 = mkTyConApp (cTupleTyCon 0) [] + co = mkUnivCo (PluginProv "ghc-typelits-extra") Representational t1 p + dcApp = evId (dataConWrapId (cTupleDataCon 0)) + in Just (evCast dcApp co) + _ -> Nothing diff --git a/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs b/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs --- a/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +++ b/src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs @@ -1,347 +1,347 @@ -{-| -Copyright : (C) 2015-2016, University of Twente -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -To use the plugin, add the - -@ -{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} -@ - -pragma to the header of your file - --} - -{-# LANGUAGE CPP #-} -{-# LANGUAGE TupleSections #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -module GHC.TypeLits.Extra.Solver - ( plugin ) -where - --- external -import Control.Monad.Trans.Maybe (MaybeT (..)) -import Data.Maybe (catMaybes) -import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName - ,tracePlugin, newWanted) -#if MIN_VERSION_ghc(8,4,0) -import GHC.TcPluginM.Extra (flattenGivens) -#else -import Control.Monad ((<=<)) -#endif - --- GHC API -#if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Names (eqPrimTyConKey, hasKey) -import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Builtin.Types (boolTy, naturalTy) -#else -import GHC.Builtin.Types (typeNatKind) -#endif -import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Builtin.Types.Literals (typeNatCmpTyCon) -#else -import GHC.Builtin.Types.Literals (typeNatLeqTyCon) -#endif -import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType) -import GHC.Core.TyCo.Rep (Type (..)) -import GHC.Core.Type (Kind, eqType, mkTyConApp, splitTyConApp_maybe, typeKind) -import GHC.Data.FastString (fsLit) -import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) -import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace) -import GHC.Tc.Types (TcPlugin(..), TcPluginResult (..)) -import GHC.Tc.Types.Constraint - (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) -#if MIN_VERSION_ghc(9,2,0) -import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev) -#endif -import GHC.Tc.Types.Evidence (EvTerm) -import GHC.Types.Name.Occurrence (mkTcOcc) -import GHC.Unit.Module (mkModuleName) -import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) -#else -import FastString (fsLit) -import Module (mkModuleName) -import OccName (mkTcOcc) -import Outputable (Outputable (..), (<+>), ($$), text) -import Plugins (Plugin (..), defaultPlugin) -#if MIN_VERSION_ghc(8,6,0) -import Plugins (purePlugin) -#endif -import PrelNames (eqPrimTyConKey, hasKey) -import TcEvidence (EvTerm) -import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace) -import TcRnTypes (TcPlugin(..), TcPluginResult (..)) -import Type (Kind, eqType, mkTyConApp, splitTyConApp_maybe) -import TyCoRep (Type (..)) -import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon) -import TcTypeNats (typeNatLeqTyCon) -#if MIN_VERSION_ghc(8,4,0) -import TcTypeNats (typeNatDivTyCon, typeNatModTyCon) -#else -import TcPluginM (zonkCt) -#endif - -#if MIN_VERSION_ghc(8,10,0) -import Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) -import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType) -import Type (typeKind) -#else -import TcRnTypes (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) -import TcType (typeKind) -import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType) -#endif -#endif - --- internal -import GHC.TypeLits.Extra.Solver.Operations -import GHC.TypeLits.Extra.Solver.Unify - -#if MIN_VERSION_ghc(9,2,0) -typeNatKind :: Type -typeNatKind = naturalTy -#endif - --- | A solver implement as a type-checker plugin for: --- --- * 'Div': type-level 'div' --- --- * 'Mod': type-level 'mod' --- --- * 'FLog': type-level equivalent of --- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" --- --- * 'CLog': type-level equivalent of /the ceiling of/ --- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" --- --- * 'Log': type-level equivalent of --- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" --- --- * 'GCD': a type-level 'gcd' --- --- * 'LCM': a type-level 'lcm' --- --- To use the plugin, add --- --- @ --- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} --- @ --- --- To the header of your file. -plugin :: Plugin -plugin - = defaultPlugin - { tcPlugin = const $ Just normalisePlugin -#if MIN_VERSION_ghc(8,6,0) - , pluginRecompile = purePlugin -#endif - } - -normalisePlugin :: TcPlugin -normalisePlugin = tracePlugin "ghc-typelits-extra" - TcPlugin { tcPluginInit = lookupExtraDefs - , tcPluginSolve = decideEqualSOP - , tcPluginStop = const (return ()) - } - -decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult -decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] []) -decideEqualSOP defs givens _deriveds wanteds = do - -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out - let wanteds' = filter isWantedCt wanteds - unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds' - case unit_wanteds of - [] -> return (TcPluginOk [] []) - _ -> do -#if MIN_VERSION_ghc(8,4,0) - unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) (givens ++ flattenGivens givens) -#else - unit_givens <- catMaybes <$> mapM ((runMaybeT . toSolverConstraint defs) <=< zonkCt) givens -#endif - sr <- simplifyExtra defs (unit_givens ++ unit_wanteds) - tcPluginTrace "normalised" (ppr sr) - case sr of - Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new) - Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq]) - -data SolverConstraint - = NatEquality Ct ExtraOp ExtraOp Normalised - | NatInequality Ct ExtraOp ExtraOp Bool Normalised - -instance Outputable SolverConstraint where - ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm - ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm - -data SimplifyResult - = Simplified [(EvTerm,Ct)] [Ct] - | Impossible SolverConstraint - -instance Outputable SimplifyResult where - ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new - ppr (Impossible sct) = text "Impossible" <+> ppr sct - -simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult -simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs - where - simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult - simples evs news [] = return (Simplified (catMaybes evs) news) - simples evs news (eq@(NatEquality ct u v norm):eqs') = do - ur <- unifyExtra ct u v - tcPluginTrace "unifyExtra result" (ppr ur) - case ur of - Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' - Lose | null evs && null eqs' -> return (Impossible eq) - _ | norm == Normalised && isWantedCt ct -> do - newCt <- createWantedFromNormalised defs eq - simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' - Lose -> simples evs news eqs' - Draw -> simples evs news eqs' - simples evs news (eq@(NatInequality ct u v b norm):eqs') = do - tcPluginTrace "unifyExtra leq result" (ppr (u,v,b)) - case (u,v) of - (I i,I j) - | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' - | otherwise -> return (Impossible eq) - (p, Max x y) - | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' - - -- transform: q ~ Max x y => (p <=? q ~ True) - -- to: (p <=? Max x y) ~ True - -- and try to solve that along with the rest of the eqs' - (p, q@(V _)) - | b -> case findMax q eqs of - Just m -> simples evs news (NatInequality ct p m b norm:eqs') - Nothing -> simples evs news eqs' - _ | norm == Normalised && isWantedCt ct -> do - newCt <- createWantedFromNormalised defs eq - simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' - _ -> simples evs news eqs' - - -- look for given constraint with the form: c ~ Max x y - findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp - findMax c = go - where - go [] = Nothing - go ((NatEquality ct a b@(Max _ _) _) :_) - | c == a && not (isWantedCt ct) - = Just b - go ((NatEquality ct a@(Max _ _) b _) :_) - | c == b && not (isWantedCt ct) - = Just a - go (_:rest) = go rest - - --- Extract the Nat equality constraints -toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint -toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 - | isNatKind (typeKind t1) || isNatKind (typeKind t2) - -> do - (t1', n1) <- normaliseNat defs t1 - (t2', n2) <- normaliseNat defs t2 - pure (NatEquality ct t1' t2' (mergeNormalised n1 n2)) -#if MIN_VERSION_ghc(9,2,0) - | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1 - , tc == ordTyCon defs - , TyConApp cmpNatTc [x,y] <- cmpNat - , cmpNatTc == typeNatCmpTyCon - , tt1 == promotedTrueDataCon - , tt2 == promotedTrueDataCon - , ff1 == promotedFalseDataCon -#else - | TyConApp tc [x,y] <- t1 - , tc == typeNatLeqTyCon -#endif - , TyConApp tc' [] <- t2 - -> do - (x', n1) <- normaliseNat defs x - (y', n2) <- normaliseNat defs y - let res | tc' == promotedTrueDataCon = pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) - | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2)) - | otherwise = fail "Nothing" - res - _ -> fail "Nothing" - where - isNatKind :: Kind -> Bool - isNatKind = (`eqType` typeNatKind) - -createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct -createWantedFromNormalised defs sct = do - let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2) - extractCtSides (NatInequality ct x y b _) = - let tc = if b then promotedTrueDataCon else promotedFalseDataCon -#if MIN_VERSION_ghc(9,2,0) - t1 = TyConApp (ordTyCon defs) - [ boolTy - , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y] - , TyConApp promotedTrueDataCon [] - , TyConApp promotedTrueDataCon [] - , TyConApp promotedFalseDataCon [] - ] -#else - t1 = TyConApp typeNatLeqTyCon [reifyEOP defs x, reifyEOP defs y] -#endif - t2 = TyConApp tc [] - in (ct, t1, t2) - let (ct, t1, t2) = extractCtSides sct - newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of - Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2]) - _ -> fail "Nothing" - ev <- newWanted (ctLoc ct) newPredTy - let ctN = case ct of -#if MIN_VERSION_ghc(9,2,0) - CQuantCan qc -> CQuantCan (qc { qci_ev = ev}) -#endif - ctX -> ctX { cc_ev = ev } - return ctN - -fromSolverConstraint :: SolverConstraint -> Ct -fromSolverConstraint (NatEquality ct _ _ _) = ct -fromSolverConstraint (NatInequality ct _ _ _ _) = ct - -lookupExtraDefs :: TcPluginM ExtraDefs -lookupExtraDefs = do - md <- lookupModule myModule myPackage -#if MIN_VERSION_ghc(9,2,0) - md2 <- lookupModule ordModule basePackage -#endif - ExtraDefs <$> look md "Max" - <*> look md "Min" -#if MIN_VERSION_ghc(8,4,0) - <*> pure typeNatDivTyCon - <*> pure typeNatModTyCon -#else - <*> look md "Div" - <*> look md "Mod" -#endif - <*> look md "FLog" - <*> look md "CLog" - <*> look md "Log" - <*> look md "GCD" - <*> look md "LCM" -#if MIN_VERSION_ghc(9,2,0) - <*> look md2 "OrdCond" - <*> look md2 "OrdCond" -#else - <*> pure typeNatLeqTyCon - <*> pure typeNatLeqTyCon -#endif - where - look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s) - myModule = mkModuleName "GHC.TypeLits.Extra" - myPackage = fsLit "ghc-typelits-extra" -#if MIN_VERSION_ghc(9,2,0) - ordModule = mkModuleName "Data.Type.Ord" - basePackage = fsLit "base" -#endif - --- Utils -evMagic :: Ct -> Maybe EvTerm -evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of - EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2) - _ -> Nothing +{-| +Copyright : (C) 2015-2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +To use the plugin, add the + +@ +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +@ + +pragma to the header of your file + +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE TupleSections #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +module GHC.TypeLits.Extra.Solver + ( plugin ) +where + +-- external +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Data.Maybe (catMaybes) +import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName + ,tracePlugin, newWanted) +#if MIN_VERSION_ghc(8,4,0) +import GHC.TcPluginM.Extra (flattenGivens) +#else +import Control.Monad ((<=<)) +#endif + +-- GHC API +#if MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Names (eqPrimTyConKey, hasKey) +import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Builtin.Types (boolTy, naturalTy) +#else +import GHC.Builtin.Types (typeNatKind) +#endif +import GHC.Builtin.Types.Literals (typeNatDivTyCon, typeNatModTyCon) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Builtin.Types.Literals (typeNatCmpTyCon) +#else +import GHC.Builtin.Types.Literals (typeNatLeqTyCon) +#endif +import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType) +import GHC.Core.TyCo.Rep (Type (..)) +import GHC.Core.Type (Kind, eqType, mkTyConApp, splitTyConApp_maybe, typeKind) +import GHC.Data.FastString (fsLit) +import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) +import GHC.Tc.Plugin (TcPluginM, tcLookupTyCon, tcPluginTrace) +import GHC.Tc.Types (TcPlugin(..), TcPluginResult (..)) +import GHC.Tc.Types.Constraint + (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev) +#endif +import GHC.Tc.Types.Evidence (EvTerm) +import GHC.Types.Name.Occurrence (mkTcOcc) +import GHC.Unit.Module (mkModuleName) +import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) +#else +import FastString (fsLit) +import Module (mkModuleName) +import OccName (mkTcOcc) +import Outputable (Outputable (..), (<+>), ($$), text) +import Plugins (Plugin (..), defaultPlugin) +#if MIN_VERSION_ghc(8,6,0) +import Plugins (purePlugin) +#endif +import PrelNames (eqPrimTyConKey, hasKey) +import TcEvidence (EvTerm) +import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace) +import TcRnTypes (TcPlugin(..), TcPluginResult (..)) +import Type (Kind, eqType, mkTyConApp, splitTyConApp_maybe) +import TyCoRep (Type (..)) +import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon) +import TcTypeNats (typeNatLeqTyCon) +#if MIN_VERSION_ghc(8,4,0) +import TcTypeNats (typeNatDivTyCon, typeNatModTyCon) +#else +import TcPluginM (zonkCt) +#endif + +#if MIN_VERSION_ghc(8,10,0) +import Constraint (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) +import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType) +import Type (typeKind) +#else +import TcRnTypes (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) +import TcType (typeKind) +import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType) +#endif +#endif + +-- internal +import GHC.TypeLits.Extra.Solver.Operations +import GHC.TypeLits.Extra.Solver.Unify + +#if MIN_VERSION_ghc(9,2,0) +typeNatKind :: Type +typeNatKind = naturalTy +#endif + +-- | A solver implement as a type-checker plugin for: +-- +-- * 'Div': type-level 'div' +-- +-- * 'Mod': type-level 'mod' +-- +-- * 'FLog': type-level equivalent of +-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" +-- +-- * 'CLog': type-level equivalent of /the ceiling of/ +-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" +-- +-- * 'Log': type-level equivalent of +-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" +-- +-- * 'GCD': a type-level 'gcd' +-- +-- * 'LCM': a type-level 'lcm' +-- +-- To use the plugin, add +-- +-- @ +-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +-- @ +-- +-- To the header of your file. +plugin :: Plugin +plugin + = defaultPlugin + { tcPlugin = const $ Just normalisePlugin +#if MIN_VERSION_ghc(8,6,0) + , pluginRecompile = purePlugin +#endif + } + +normalisePlugin :: TcPlugin +normalisePlugin = tracePlugin "ghc-typelits-extra" + TcPlugin { tcPluginInit = lookupExtraDefs + , tcPluginSolve = decideEqualSOP + , tcPluginStop = const (return ()) + } + +decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult +decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] []) +decideEqualSOP defs givens _deriveds wanteds = do + -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out + let wanteds' = filter isWantedCt wanteds + unit_wanteds <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) wanteds' + case unit_wanteds of + [] -> return (TcPluginOk [] []) + _ -> do +#if MIN_VERSION_ghc(8,4,0) + unit_givens <- catMaybes <$> mapM (runMaybeT . toSolverConstraint defs) (givens ++ flattenGivens givens) +#else + unit_givens <- catMaybes <$> mapM ((runMaybeT . toSolverConstraint defs) <=< zonkCt) givens +#endif + sr <- simplifyExtra defs (unit_givens ++ unit_wanteds) + tcPluginTrace "normalised" (ppr sr) + case sr of + Simplified evs new -> return (TcPluginOk (filter (isWantedCt . snd) evs) new) + Impossible eq -> return (TcPluginContradiction [fromSolverConstraint eq]) + +data SolverConstraint + = NatEquality Ct ExtraOp ExtraOp Normalised + | NatInequality Ct ExtraOp ExtraOp Bool Normalised + +instance Outputable SolverConstraint where + ppr (NatEquality ct op1 op2 norm) = text "NatEquality" $$ ppr ct $$ ppr op1 $$ ppr op2 $$ ppr norm + ppr (NatInequality _ op1 op2 b norm) = text "NatInequality" $$ ppr op1 $$ ppr op2 $$ ppr b $$ ppr norm + +data SimplifyResult + = Simplified [(EvTerm,Ct)] [Ct] + | Impossible SolverConstraint + +instance Outputable SimplifyResult where + ppr (Simplified evs new) = text "Simplified" $$ text "Solved:" $$ ppr evs $$ text "New:" $$ ppr new + ppr (Impossible sct) = text "Impossible" <+> ppr sct + +simplifyExtra :: ExtraDefs -> [SolverConstraint] -> TcPluginM SimplifyResult +simplifyExtra defs eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] eqs + where + simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM SimplifyResult + simples evs news [] = return (Simplified (catMaybes evs) news) + simples evs news (eq@(NatEquality ct u v norm):eqs') = do + ur <- unifyExtra ct u v + tcPluginTrace "unifyExtra result" (ppr ur) + case ur of + Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' + Lose | null evs && null eqs' -> return (Impossible eq) + _ | norm == Normalised && isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' + Lose -> simples evs news eqs' + Draw -> simples evs news eqs' + simples evs news (eq@(NatInequality ct u v b norm):eqs') = do + tcPluginTrace "unifyExtra leq result" (ppr (u,v,b)) + case (u,v) of + (I i,I j) + | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' + | otherwise -> return (Impossible eq) + (p, Max x y) + | b && (p == x || p == y) -> simples (((,) <$> evMagic ct <*> pure ct):evs) news eqs' + + -- transform: q ~ Max x y => (p <=? q ~ True) + -- to: (p <=? Max x y) ~ True + -- and try to solve that along with the rest of the eqs' + (p, q@(V _)) + | b -> case findMax q eqs of + Just m -> simples evs news (NatInequality ct p m b norm:eqs') + Nothing -> simples evs news eqs' + _ | norm == Normalised && isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (((,) <$> evMagic ct <*> pure ct):evs) (newCt:news) eqs' + _ -> simples evs news eqs' + + -- look for given constraint with the form: c ~ Max x y + findMax :: ExtraOp -> [SolverConstraint] -> Maybe ExtraOp + findMax c = go + where + go [] = Nothing + go ((NatEquality ct a b@(Max _ _) _) :_) + | c == a && not (isWantedCt ct) + = Just b + go ((NatEquality ct a@(Max _ _) b _) :_) + | c == b && not (isWantedCt ct) + = Just a + go (_:rest) = go rest + + +-- Extract the Nat equality constraints +toSolverConstraint :: ExtraDefs -> Ct -> MaybeT TcPluginM SolverConstraint +toSolverConstraint defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 + | isNatKind (typeKind t1) || isNatKind (typeKind t2) + -> do + (t1', n1) <- normaliseNat defs t1 + (t2', n2) <- normaliseNat defs t2 + pure (NatEquality ct t1' t2' (mergeNormalised n1 n2)) +#if MIN_VERSION_ghc(9,2,0) + | TyConApp tc [_,cmpNat,TyConApp tt1 [],TyConApp tt2 [],TyConApp ff1 []] <- t1 + , tc == ordTyCon defs + , TyConApp cmpNatTc [x,y] <- cmpNat + , cmpNatTc == typeNatCmpTyCon + , tt1 == promotedTrueDataCon + , tt2 == promotedTrueDataCon + , ff1 == promotedFalseDataCon +#else + | TyConApp tc [x,y] <- t1 + , tc == typeNatLeqTyCon +#endif + , TyConApp tc' [] <- t2 + -> do + (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + let res | tc' == promotedTrueDataCon = pure (NatInequality ct x' y' True (mergeNormalised n1 n2)) + | tc' == promotedFalseDataCon = pure (NatInequality ct x' y' False (mergeNormalised n1 n2)) + | otherwise = fail "Nothing" + res + _ -> fail "Nothing" + where + isNatKind :: Kind -> Bool + isNatKind = (`eqType` typeNatKind) + +createWantedFromNormalised :: ExtraDefs -> SolverConstraint -> TcPluginM Ct +createWantedFromNormalised defs sct = do + let extractCtSides (NatEquality ct t1 t2 _) = (ct, reifyEOP defs t1, reifyEOP defs t2) + extractCtSides (NatInequality ct x y b _) = + let tc = if b then promotedTrueDataCon else promotedFalseDataCon +#if MIN_VERSION_ghc(9,2,0) + t1 = TyConApp (ordTyCon defs) + [ boolTy + , TyConApp typeNatCmpTyCon [reifyEOP defs x, reifyEOP defs y] + , TyConApp promotedTrueDataCon [] + , TyConApp promotedTrueDataCon [] + , TyConApp promotedFalseDataCon [] + ] +#else + t1 = TyConApp typeNatLeqTyCon [reifyEOP defs x, reifyEOP defs y] +#endif + t2 = TyConApp tc [] + in (ct, t1, t2) + let (ct, t1, t2) = extractCtSides sct + newPredTy <- case splitTyConApp_maybe $ ctEvPred $ ctEvidence ct of + Just (tc, [a, b, _, _]) | tc `hasKey` eqPrimTyConKey -> pure (mkTyConApp tc [a, b, t1, t2]) + _ -> fail "Nothing" + ev <- newWanted (ctLoc ct) newPredTy + let ctN = case ct of +#if MIN_VERSION_ghc(9,2,0) + CQuantCan qc -> CQuantCan (qc { qci_ev = ev}) +#endif + ctX -> ctX { cc_ev = ev } + return ctN + +fromSolverConstraint :: SolverConstraint -> Ct +fromSolverConstraint (NatEquality ct _ _ _) = ct +fromSolverConstraint (NatInequality ct _ _ _ _) = ct + +lookupExtraDefs :: TcPluginM ExtraDefs +lookupExtraDefs = do + md <- lookupModule myModule myPackage +#if MIN_VERSION_ghc(9,2,0) + md2 <- lookupModule ordModule basePackage +#endif + ExtraDefs <$> look md "Max" + <*> look md "Min" +#if MIN_VERSION_ghc(8,4,0) + <*> pure typeNatDivTyCon + <*> pure typeNatModTyCon +#else + <*> look md "Div" + <*> look md "Mod" +#endif + <*> look md "FLog" + <*> look md "CLog" + <*> look md "Log" + <*> look md "GCD" + <*> look md "LCM" +#if MIN_VERSION_ghc(9,2,0) + <*> look md2 "OrdCond" + <*> look md2 "OrdCond" +#else + <*> pure typeNatLeqTyCon + <*> pure typeNatLeqTyCon +#endif + where + look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s) + myModule = mkModuleName "GHC.TypeLits.Extra" + myPackage = fsLit "ghc-typelits-extra" +#if MIN_VERSION_ghc(9,2,0) + ordModule = mkModuleName "Data.Type.Ord" + basePackage = fsLit "base" +#endif + +-- Utils +evMagic :: Ct -> Maybe EvTerm +evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of + EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2) + _ -> Nothing diff --git a/src/GHC/TypeLits/Extra.hs b/src/GHC/TypeLits/Extra.hs --- a/src/GHC/TypeLits/Extra.hs +++ b/src/GHC/TypeLits/Extra.hs @@ -1,253 +1,253 @@ -{-| -Copyright : (C) 2015-2016, University of Twente, - 2017-2018, QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - -Additional type-level operations on 'GHC.TypeLits.Nat': - - * 'Max': type-level 'max' - - * 'Min': type-level 'min' - - * 'Div': type-level 'div' - - * 'Mod': type-level 'mod' - - * 'FLog': type-level equivalent of - .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" - - * 'CLog': type-level equivalent of /the ceiling of/ - .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" - - * 'Log': type-level equivalent of - where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" - - * 'GCD': a type-level 'gcd' - - * 'LCM': a type-level 'lcm' - -A custom solver for the above operations defined is defined in -"GHC.TypeLits.Extra.Solver" as a GHC type-checker plugin. To use the plugin, -add the - -@ -{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} -@ - -pragma to the header of your file. --} - -{-# LANGUAGE CPP #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE MagicHash #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -{-# OPTIONS_HADDOCK show-extensions #-} -{-# OPTIONS_GHC -Wno-orphans #-} - -{-# LANGUAGE Trustworthy #-} - -module GHC.TypeLits.Extra - ( -- * Type-level operations on `Nat` - -- ** Ord - Max - , Min - -- ** Integral - , Div - , Mod - , DivMod - -- *** Variants - , DivRU - -- ** Logarithm - , FLog - , CLog - -- *** Exact logarithm - , Log - -- Numeric - , GCD - , LCM - ) -where - -import Data.Proxy (Proxy (..)) -import Data.Type.Bool (If) -import GHC.Base (Int#,isTrue#,(==#),(+#)) -#if MIN_VERSION_ghc(9,4,0) -import GHC.Base (Constraint) -#endif -import GHC.Integer.Logarithms (integerLogBase#) -#if MIN_VERSION_ghc(8,2,0) -import GHC.Magic (noinline) -#endif -#if MIN_VERSION_ghc(8,2,0) -import qualified GHC.TypeNats as N -import GHC.Natural -import GHC.Prim (int2Word#) -import GHC.TypeLits -#else -import GHC.Integer (smallInteger) -import GHC.TypeLits as N -#endif - (KnownNat, Nat, type (+), type (-), type (<=), type (<=?), natVal) -#if MIN_VERSION_ghc(8,4,0) -import GHC.TypeLits (Div, Mod) -#endif -import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol) - -#if MIN_VERSION_ghc(8,2,0) -intToNumber :: Int# -> Natural -intToNumber x = NatS# (int2Word# x) -#else -intToNumber :: Int# -> Integer -intToNumber x = smallInteger x -#endif -{-# INLINE intToNumber #-} - --- | Type-level 'max' -type family Max (x :: Nat) (y :: Nat) :: Nat where - Max n n = n - Max x y = If (x <=? y) y x - -instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where - natSing2 = SNatKn (max (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) - --- | Type-level 'min' -type family Min (x :: Nat) (y :: Nat) :: Nat where - Min n n = n - Min x y = If (x <=? y) x y - -instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Min) x y where - natSing2 = SNatKn (min (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) - -#if !MIN_VERSION_ghc(8,4,0) --- | Type-level 'div' --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family Div (dividend :: Nat) (divisor :: Nat) :: Nat where - Div x 1 = x - -instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where - natSing2 = SNatKn (quot (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -#endif - --- | A variant of 'Div' that rounds up instead of down -type DivRU n d = Div (n + (d - 1)) d - -#if !MIN_VERSION_ghc(8,4,0) --- | Type-level 'mod' --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family Mod (x :: Nat) (y :: Nat) :: Nat where - Mod x 1 = 0 - -instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where - natSing2 = SNatKn (rem (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -#endif - --- | Type-level `divMod` -type DivMod n d = '(Div n d, Mod n d) - --- | Type-level equivalent of --- .i.e. the exact integer equivalent to "@'floor' ('logBase' base value)@" --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family FLog (base :: Nat) (value :: Nat) :: Nat where - FLog 2 1 = 0 -- Additional equations are provided by the custom solver - -instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''FLog) x y where -#if MIN_VERSION_ghc (8,2,0) - natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) -#else - natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) -#endif - --- | Type-level equivalent of /the ceiling of/ --- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' base value)@" --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family CLog (base :: Nat) (value :: Nat) :: Nat where - CLog 2 1 = 0 -- Additional equations are provided by the custom solver - -#if MIN_VERSION_ghc(9,4,0) -instance (KnownNat x, KnownNat y, (2 <= x) ~ (() :: Constraint), 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where -#else -instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where -#endif - natSing2 = let x = natVal (Proxy @x) - y = natVal (Proxy @y) - z1 = integerLogBase# x y - z2 = integerLogBase# x (y-1) - in case y of - 1 -> SNatKn 0 - _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) - | otherwise -> SNatKn (intToNumber z1) - --- | Type-level equivalent of --- where the operation only reduces when: --- --- @ --- 'FLog' base value ~ 'CLog' base value --- @ --- --- Additionally, the following property holds for 'Log': --- --- > (base ^ (Log base value)) ~ value --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family Log (base :: Nat) (value :: Nat) :: Nat where - Log 2 1 = 0 -- Additional equations are provided by the custom solver - -instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where - natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) - --- | Type-level greatest common denominator (GCD). --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family GCD (x :: Nat) (y :: Nat) :: Nat where - GCD 0 x = x - GCD x 0 = x - GCD 1 x = 1 - GCD x 1 = 1 - GCD x x = x - -- Additional equations are provided by the custom solver - -instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''GCD) x y where - natSing2 = SNatKn ( -#if MIN_VERSION_ghc(8,2,0) - noinline -#endif - gcd (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) - --- | Type-level least common multiple (LCM). --- --- Note that additional equations are provided by the type-checker plugin solver --- "GHC.TypeLits.Extra.Solver". -type family LCM (x :: Nat) (y :: Nat) :: Nat where - LCM 0 x = 0 - LCM x 0 = 0 - LCM 1 x = x - LCM x 1 = x - LCM x x = x - -- Additional equations are provided by the custom solver - -instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''LCM) x y where - natSing2 = SNatKn ( -#if MIN_VERSION_ghc(8,2,0) - noinline -#endif - lcm (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) +{-| +Copyright : (C) 2015-2016, University of Twente, + 2017-2018, QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +Additional type-level operations on 'GHC.TypeLits.Nat': + + * 'Max': type-level 'max' + + * 'Min': type-level 'min' + + * 'Div': type-level 'div' + + * 'Mod': type-level 'mod' + + * 'FLog': type-level equivalent of + .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" + + * 'CLog': type-level equivalent of /the ceiling of/ + .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" + + * 'Log': type-level equivalent of + where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" + + * 'GCD': a type-level 'gcd' + + * 'LCM': a type-level 'lcm' + +A custom solver for the above operations defined is defined in +"GHC.TypeLits.Extra.Solver" as a GHC type-checker plugin. To use the plugin, +add the + +@ +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +@ + +pragma to the header of your file. +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_HADDOCK show-extensions #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +{-# LANGUAGE Trustworthy #-} + +module GHC.TypeLits.Extra + ( -- * Type-level operations on `Nat` + -- ** Ord + Max + , Min + -- ** Integral + , Div + , Mod + , DivMod + -- *** Variants + , DivRU + -- ** Logarithm + , FLog + , CLog + -- *** Exact logarithm + , Log + -- Numeric + , GCD + , LCM + ) +where + +import Data.Proxy (Proxy (..)) +import Data.Type.Bool (If) +import GHC.Base (Int#,isTrue#,(==#),(+#)) +#if MIN_VERSION_ghc(9,4,0) +import GHC.Base (Constraint) +#endif +import GHC.Integer.Logarithms (integerLogBase#) +#if MIN_VERSION_ghc(8,2,0) +import GHC.Magic (noinline) +#endif +#if MIN_VERSION_ghc(8,2,0) +import qualified GHC.TypeNats as N +import GHC.Natural +import GHC.Prim (int2Word#) +import GHC.TypeLits +#else +import GHC.Integer (smallInteger) +import GHC.TypeLits as N +#endif + (KnownNat, Nat, type (+), type (-), type (<=), type (<=?), natVal) +#if MIN_VERSION_ghc(8,4,0) +import GHC.TypeLits (Div, Mod) +#endif +import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol) + +#if MIN_VERSION_ghc(8,2,0) +intToNumber :: Int# -> Natural +intToNumber x = NatS# (int2Word# x) +#else +intToNumber :: Int# -> Integer +intToNumber x = smallInteger x +#endif +{-# INLINE intToNumber #-} + +-- | Type-level 'max' +type family Max (x :: Nat) (y :: Nat) :: Nat where + Max n n = n + Max x y = If (x <=? y) y x + +instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where + natSing2 = SNatKn (max (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) + +-- | Type-level 'min' +type family Min (x :: Nat) (y :: Nat) :: Nat where + Min n n = n + Min x y = If (x <=? y) x y + +instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Min) x y where + natSing2 = SNatKn (min (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) + +#if !MIN_VERSION_ghc(8,4,0) +-- | Type-level 'div' +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family Div (dividend :: Nat) (divisor :: Nat) :: Nat where + Div x 1 = x + +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where + natSing2 = SNatKn (quot (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) +#endif + +-- | A variant of 'Div' that rounds up instead of down +type DivRU n d = Div (n + (d - 1)) d + +#if !MIN_VERSION_ghc(8,4,0) +-- | Type-level 'mod' +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family Mod (x :: Nat) (y :: Nat) :: Nat where + Mod x 1 = 0 + +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where + natSing2 = SNatKn (rem (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) +#endif + +-- | Type-level `divMod` +type DivMod n d = '(Div n d, Mod n d) + +-- | Type-level equivalent of +-- .i.e. the exact integer equivalent to "@'floor' ('logBase' base value)@" +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family FLog (base :: Nat) (value :: Nat) :: Nat where + FLog 2 1 = 0 -- Additional equations are provided by the custom solver + +instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''FLog) x y where +#if MIN_VERSION_ghc (8,2,0) + natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) +#else + natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) +#endif + +-- | Type-level equivalent of /the ceiling of/ +-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' base value)@" +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family CLog (base :: Nat) (value :: Nat) :: Nat where + CLog 2 1 = 0 -- Additional equations are provided by the custom solver + +#if MIN_VERSION_ghc(9,4,0) +instance (KnownNat x, KnownNat y, (2 <= x) ~ (() :: Constraint), 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where +#else +instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where +#endif + natSing2 = let x = natVal (Proxy @x) + y = natVal (Proxy @y) + z1 = integerLogBase# x y + z2 = integerLogBase# x (y-1) + in case y of + 1 -> SNatKn 0 + _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) + | otherwise -> SNatKn (intToNumber z1) + +-- | Type-level equivalent of +-- where the operation only reduces when: +-- +-- @ +-- 'FLog' base value ~ 'CLog' base value +-- @ +-- +-- Additionally, the following property holds for 'Log': +-- +-- > (base ^ (Log base value)) ~ value +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family Log (base :: Nat) (value :: Nat) :: Nat where + Log 2 1 = 0 -- Additional equations are provided by the custom solver + +instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where + natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) + +-- | Type-level greatest common denominator (GCD). +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family GCD (x :: Nat) (y :: Nat) :: Nat where + GCD 0 x = x + GCD x 0 = x + GCD 1 x = 1 + GCD x 1 = 1 + GCD x x = x + -- Additional equations are provided by the custom solver + +instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''GCD) x y where + natSing2 = SNatKn ( +#if MIN_VERSION_ghc(8,2,0) + noinline +#endif + gcd (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) + +-- | Type-level least common multiple (LCM). +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family LCM (x :: Nat) (y :: Nat) :: Nat where + LCM 0 x = 0 + LCM x 0 = 0 + LCM 1 x = x + LCM x 1 = x + LCM x x = x + -- Additional equations are provided by the custom solver + +instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''LCM) x y where + natSing2 = SNatKn ( +#if MIN_VERSION_ghc(8,2,0) + noinline +#endif + lcm (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) diff --git a/src/GHC/TypeLits/Extra/Solver/Operations.hs b/src/GHC/TypeLits/Extra/Solver/Operations.hs --- a/src/GHC/TypeLits/Extra/Solver/Operations.hs +++ b/src/GHC/TypeLits/Extra/Solver/Operations.hs @@ -1,242 +1,242 @@ -{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij --} - -{-# LANGUAGE CPP #-} -{-# LANGUAGE MagicHash #-} - -module GHC.TypeLits.Extra.Solver.Operations - ( ExtraOp (..) - , ExtraDefs (..) - , Normalised (..) - , NormaliseResult - , mergeNormalised - , reifyEOP - , mergeMax - , mergeMin - , mergeDiv - , mergeMod - , mergeFLog - , mergeCLog - , mergeLog - , mergeGCD - , mergeLCM - , mergeExp - ) -where - --- external -import Control.Monad.Trans.Writer.Strict -#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0) -import Data.Set as Set -#endif - -import GHC.Base (isTrue#,(==#),(+#)) -import GHC.Integer (smallInteger) -import GHC.Integer.Logarithms (integerLogBase#) -import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural) - --- GHC API -#if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Types.Literals (typeNatExpTyCon, typeNatSubTyCon) -import GHC.Core.TyCon (TyCon) -import GHC.Core.Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy) -import GHC.Utils.Outputable (Outputable (..), (<+>), integer, text) -#else -import Outputable (Outputable (..), (<+>), integer, text) -import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon) -import TyCon (TyCon) -import Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy) -#endif - --- | Indicates whether normalisation has occured -data Normalised = Normalised | Untouched - deriving Eq - -instance Outputable Normalised where - ppr Normalised = text "Normalised" - ppr Untouched = text "Untouched" - -mergeNormalised :: Normalised -> Normalised -> Normalised -mergeNormalised Normalised _ = Normalised -mergeNormalised _ Normalised = Normalised -mergeNormalised _ _ = Untouched - --- | A normalise result contains the ExtraOp and a flag that indicates whether any expression --- | was normalised within the ExtraOp. -type NormaliseResult = (ExtraOp, Normalised) - -data ExtraOp - = I Integer - | V TyVar - | C CType - | Max ExtraOp ExtraOp - | Min ExtraOp ExtraOp - | Div ExtraOp ExtraOp - | Mod ExtraOp ExtraOp - | FLog ExtraOp ExtraOp - | CLog ExtraOp ExtraOp - | Log ExtraOp ExtraOp - | GCD ExtraOp ExtraOp - | LCM ExtraOp ExtraOp - | Exp ExtraOp ExtraOp - deriving Eq - -instance Outputable ExtraOp where - ppr (I i) = integer i - ppr (V v) = ppr v - ppr (C c) = ppr c - ppr (Max x y) = text "Max (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (Min x y) = text "Min (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (Div x y) = text "Div (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (Mod x y) = text "Mod (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (FLog x y) = text "FLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (Log x y) = text "Log (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (LCM x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")" - -data ExtraDefs = ExtraDefs - { maxTyCon :: TyCon - , minTyCon :: TyCon - , divTyCon :: TyCon - , modTyCon :: TyCon - , flogTyCon :: TyCon - , clogTyCon :: TyCon - , logTyCon :: TyCon - , gcdTyCon :: TyCon - , lcmTyCon :: TyCon - , ordTyCon :: TyCon - , assertTC :: TyCon - } - -reifyEOP :: ExtraDefs -> ExtraOp -> Type -reifyEOP _ (I i) = mkNumLitTy i -reifyEOP _ (V v) = mkTyVarTy v -reifyEOP _ (C (CType c)) = c -reifyEOP defs (Max x y) = mkTyConApp (maxTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (Min x y) = mkTyConApp (minTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (Div x y) = mkTyConApp (divTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (Mod x y) = mkTyConApp (modTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (Log x y) = mkTyConApp (logTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (LCM x y) = mkTyConApp (lcmTyCon defs) [reifyEOP defs x - ,reifyEOP defs y] -reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x - ,reifyEOP defs y] - -mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult -mergeMax _ (I 0) y = (y, Normalised) -mergeMax _ x (I 0) = (x, Normalised) -mergeMax defs x y = - let x' = reifyEOP defs x - y' = reifyEOP defs y - z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) -#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0) - in case runWriterT (isNatural z) of - Just (True , cs) | Set.null cs -> (y, Normalised) - Just (False, cs) | Set.null cs -> (x, Normalised) -#else - in case isNatural z of - Just True -> (y, Normalised) - Just False -> (x, Normalised) -#endif - _ -> (Max x y, Untouched) - -mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult -mergeMin defs x y = - let x' = reifyEOP defs x - y' = reifyEOP defs y - z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) -#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0) - in case runWriterT (isNatural z) of - Just (True, cs) | Set.null cs -> (x, Normalised) - Just (False,cs) | Set.null cs -> (y, Normalised) -#else - in case isNatural z of - Just True -> (x, Normalised) - Just False -> (y, Normalised) -#endif - _ -> (Min x y, Untouched) - -mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult -mergeDiv _ (I 0) = Nothing -mergeDiv (I i) (I j) = Just (I (div i j), Normalised) -mergeDiv x y = Just (Div x y, Untouched) - -mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult -mergeMod _ (I 0) = Nothing -mergeMod (I i) (I j) = Just (I (mod i j), Normalised) -mergeMod x y = Just (Mod x y, Untouched) - -mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult -mergeFLog (I i) _ | i < 2 = Nothing -mergeFLog i (Exp j k) | i == j = Just (k, Normalised) -mergeFLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (flogBase i j) -mergeFLog x y = Just (FLog x y, Untouched) - -mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult -mergeCLog (I i) _ | i < 2 = Nothing -mergeCLog i (Exp j k) | i == j = Just (k, Normalised) -mergeCLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (clogBase i j) -mergeCLog x y = Just (CLog x y, Untouched) - -mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult -mergeLog (I i) _ | i < 2 = Nothing -mergeLog b (Exp b' y) | b == b' = Just (y, Normalised) -mergeLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (exactLogBase i j) -mergeLog x y = Just (Log x y, Untouched) - -mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult -mergeGCD (I i) (I j) = (I (gcd i j), Normalised) -mergeGCD x y = (GCD x y, Untouched) - -mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult -mergeLCM (I i) (I j) = (I (lcm i j), Normalised) -mergeLCM x y = (LCM x y, Untouched) - -mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult -mergeExp (I i) (I j) = (I (i^j), Normalised) -mergeExp b (Log b' y) | b == b' = (y, Normalised) -mergeExp x y = (Exp x y, Untouched) - --- | \x y -> logBase x y, x > 1 && y > 0 -flogBase :: Integer -> Integer -> Maybe Integer -flogBase x y | y > 0 = Just (smallInteger (integerLogBase# x y)) -flogBase _ _ = Nothing - --- | \x y -> ceiling (logBase x y), x > 1 && y > 0 -clogBase :: Integer -> Integer -> Maybe Integer -clogBase x y | y > 0 = - let z1 = integerLogBase# x y - z2 = integerLogBase# x (y-1) - in case y of - 1 -> Just 0 - _ | isTrue# (z1 ==# z2) -> Just (smallInteger (z1 +# 1#)) - | otherwise -> Just (smallInteger z1) -clogBase _ _ = Nothing - --- | \x y -> logBase x y, x > 1 && y > 0, logBase x y == ceiling (logBase x y) -exactLogBase :: Integer -> Integer -> Maybe Integer -exactLogBase x y | y > 0 = - let z1 = integerLogBase# x y - z2 = integerLogBase# x (y-1) - in case y of - 1 -> Just 0 - _ | isTrue# (z1 ==# z2) -> Nothing - | otherwise -> Just (smallInteger z1) -exactLogBase _ _ = Nothing +{-| +Copyright : (C) 2015-2016, University of Twente, + 2017 , QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij +-} + +{-# LANGUAGE CPP #-} +{-# LANGUAGE MagicHash #-} + +module GHC.TypeLits.Extra.Solver.Operations + ( ExtraOp (..) + , ExtraDefs (..) + , Normalised (..) + , NormaliseResult + , mergeNormalised + , reifyEOP + , mergeMax + , mergeMin + , mergeDiv + , mergeMod + , mergeFLog + , mergeCLog + , mergeLog + , mergeGCD + , mergeLCM + , mergeExp + ) +where + +-- external +import Control.Monad.Trans.Writer.Strict +#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0) +import Data.Set as Set +#endif + +import GHC.Base (isTrue#,(==#),(+#)) +import GHC.Integer (smallInteger) +import GHC.Integer.Logarithms (integerLogBase#) +import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural) + +-- GHC API +#if MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Types.Literals (typeNatExpTyCon, typeNatSubTyCon) +import GHC.Core.TyCon (TyCon) +import GHC.Core.Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy) +import GHC.Utils.Outputable (Outputable (..), (<+>), integer, text) +#else +import Outputable (Outputable (..), (<+>), integer, text) +import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon) +import TyCon (TyCon) +import Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy) +#endif + +-- | Indicates whether normalisation has occured +data Normalised = Normalised | Untouched + deriving Eq + +instance Outputable Normalised where + ppr Normalised = text "Normalised" + ppr Untouched = text "Untouched" + +mergeNormalised :: Normalised -> Normalised -> Normalised +mergeNormalised Normalised _ = Normalised +mergeNormalised _ Normalised = Normalised +mergeNormalised _ _ = Untouched + +-- | A normalise result contains the ExtraOp and a flag that indicates whether any expression +-- | was normalised within the ExtraOp. +type NormaliseResult = (ExtraOp, Normalised) + +data ExtraOp + = I Integer + | V TyVar + | C CType + | Max ExtraOp ExtraOp + | Min ExtraOp ExtraOp + | Div ExtraOp ExtraOp + | Mod ExtraOp ExtraOp + | FLog ExtraOp ExtraOp + | CLog ExtraOp ExtraOp + | Log ExtraOp ExtraOp + | GCD ExtraOp ExtraOp + | LCM ExtraOp ExtraOp + | Exp ExtraOp ExtraOp + deriving Eq + +instance Outputable ExtraOp where + ppr (I i) = integer i + ppr (V v) = ppr v + ppr (C c) = ppr c + ppr (Max x y) = text "Max (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (Min x y) = text "Min (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (Div x y) = text "Div (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (Mod x y) = text "Mod (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (FLog x y) = text "FLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (Log x y) = text "Log (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (LCM x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + +data ExtraDefs = ExtraDefs + { maxTyCon :: TyCon + , minTyCon :: TyCon + , divTyCon :: TyCon + , modTyCon :: TyCon + , flogTyCon :: TyCon + , clogTyCon :: TyCon + , logTyCon :: TyCon + , gcdTyCon :: TyCon + , lcmTyCon :: TyCon + , ordTyCon :: TyCon + , assertTC :: TyCon + } + +reifyEOP :: ExtraDefs -> ExtraOp -> Type +reifyEOP _ (I i) = mkNumLitTy i +reifyEOP _ (V v) = mkTyVarTy v +reifyEOP _ (C (CType c)) = c +reifyEOP defs (Max x y) = mkTyConApp (maxTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (Min x y) = mkTyConApp (minTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (Div x y) = mkTyConApp (divTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (Mod x y) = mkTyConApp (modTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (Log x y) = mkTyConApp (logTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (LCM x y) = mkTyConApp (lcmTyCon defs) [reifyEOP defs x + ,reifyEOP defs y] +reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x + ,reifyEOP defs y] + +mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult +mergeMax _ (I 0) y = (y, Normalised) +mergeMax _ x (I 0) = (x, Normalised) +mergeMax defs x y = + let x' = reifyEOP defs x + y' = reifyEOP defs y + z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) +#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0) + in case runWriterT (isNatural z) of + Just (True , cs) | Set.null cs -> (y, Normalised) + Just (False, cs) | Set.null cs -> (x, Normalised) +#else + in case isNatural z of + Just True -> (y, Normalised) + Just False -> (x, Normalised) +#endif + _ -> (Max x y, Untouched) + +mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult +mergeMin defs x y = + let x' = reifyEOP defs x + y' = reifyEOP defs y + z = fst (runWriter (normaliseNat (mkTyConApp typeNatSubTyCon [y',x']))) +#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0) + in case runWriterT (isNatural z) of + Just (True, cs) | Set.null cs -> (x, Normalised) + Just (False,cs) | Set.null cs -> (y, Normalised) +#else + in case isNatural z of + Just True -> (x, Normalised) + Just False -> (y, Normalised) +#endif + _ -> (Min x y, Untouched) + +mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult +mergeDiv _ (I 0) = Nothing +mergeDiv (I i) (I j) = Just (I (div i j), Normalised) +mergeDiv x y = Just (Div x y, Untouched) + +mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult +mergeMod _ (I 0) = Nothing +mergeMod (I i) (I j) = Just (I (mod i j), Normalised) +mergeMod x y = Just (Mod x y, Untouched) + +mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult +mergeFLog (I i) _ | i < 2 = Nothing +mergeFLog i (Exp j k) | i == j = Just (k, Normalised) +mergeFLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (flogBase i j) +mergeFLog x y = Just (FLog x y, Untouched) + +mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult +mergeCLog (I i) _ | i < 2 = Nothing +mergeCLog i (Exp j k) | i == j = Just (k, Normalised) +mergeCLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (clogBase i j) +mergeCLog x y = Just (CLog x y, Untouched) + +mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult +mergeLog (I i) _ | i < 2 = Nothing +mergeLog b (Exp b' y) | b == b' = Just (y, Normalised) +mergeLog (I i) (I j) = fmap (\r -> (I r, Normalised)) (exactLogBase i j) +mergeLog x y = Just (Log x y, Untouched) + +mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult +mergeGCD (I i) (I j) = (I (gcd i j), Normalised) +mergeGCD x y = (GCD x y, Untouched) + +mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult +mergeLCM (I i) (I j) = (I (lcm i j), Normalised) +mergeLCM x y = (LCM x y, Untouched) + +mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult +mergeExp (I i) (I j) = (I (i^j), Normalised) +mergeExp b (Log b' y) | b == b' = (y, Normalised) +mergeExp x y = (Exp x y, Untouched) + +-- | \x y -> logBase x y, x > 1 && y > 0 +flogBase :: Integer -> Integer -> Maybe Integer +flogBase x y | y > 0 = Just (smallInteger (integerLogBase# x y)) +flogBase _ _ = Nothing + +-- | \x y -> ceiling (logBase x y), x > 1 && y > 0 +clogBase :: Integer -> Integer -> Maybe Integer +clogBase x y | y > 0 = + let z1 = integerLogBase# x y + z2 = integerLogBase# x (y-1) + in case y of + 1 -> Just 0 + _ | isTrue# (z1 ==# z2) -> Just (smallInteger (z1 +# 1#)) + | otherwise -> Just (smallInteger z1) +clogBase _ _ = Nothing + +-- | \x y -> logBase x y, x > 1 && y > 0, logBase x y == ceiling (logBase x y) +exactLogBase :: Integer -> Integer -> Maybe Integer +exactLogBase x y | y > 0 = + let z1 = integerLogBase# x y + z2 = integerLogBase# x (y-1) + in case y of + 1 -> Just 0 + _ | isTrue# (z1 ==# z2) -> Nothing + | otherwise -> Just (smallInteger z1) +exactLogBase _ _ = Nothing diff --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs --- a/src/GHC/TypeLits/Extra/Solver/Unify.hs +++ b/src/GHC/TypeLits/Extra/Solver/Unify.hs @@ -1,182 +1,182 @@ -{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij --} - -{-# LANGUAGE CPP #-} - -module GHC.TypeLits.Extra.Solver.Unify - ( ExtraDefs (..) - , UnifyResult (..) - , NormaliseResult - , normaliseNat - , unifyExtra - ) -where - --- external -import Control.Monad.Trans.Class (lift) -import Control.Monad.Trans.Maybe (MaybeT (..)) -import Data.Maybe (catMaybes) -import Data.Function (on) -import GHC.TypeLits.Normalise.Unify (CType (..)) - --- GHC API -#if MIN_VERSION_ghc(9,0,0) -import GHC.Builtin.Types.Literals (typeNatExpTyCon) -import GHC.Core.TyCo.Rep (Type (..), TyLit (..)) -import GHC.Core.Type (TyVar, coreView) -import GHC.Tc.Plugin (TcPluginM, tcPluginTrace) -import GHC.Tc.Types.Constraint (Ct) -import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) -import GHC.Utils.Outputable (Outputable (..), ($$), text) -#else -import Outputable (Outputable (..), ($$), text) -import TcPluginM (TcPluginM, tcPluginTrace) -import TcTypeNats (typeNatExpTyCon) -import Type (TyVar, coreView) -import TyCoRep (Type (..), TyLit (..)) -import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) -#if MIN_VERSION_ghc(8,10,0) -import Constraint (Ct) -#else -import TcRnMonad (Ct) -#endif -#endif - --- internal -import GHC.TypeLits.Extra.Solver.Operations - -mergeNormResWith - :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult) - -> MaybeT TcPluginM NormaliseResult - -> MaybeT TcPluginM NormaliseResult - -> MaybeT TcPluginM NormaliseResult -mergeNormResWith f x y = do - (x', n1) <- x - (y', n2) <- y - (res, n3) <- f x' y' - pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3) - - -normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult -normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1 -normaliseNat _ (TyVarTy v) = pure (V v, Untouched) -normaliseNat _ (LitTy (NumTyLit i)) = pure (I i, Untouched) -normaliseNat defs (TyConApp tc [x,y]) - | tc == maxTyCon defs = mergeNormResWith (\x' y' -> return (mergeMax defs x' y')) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == minTyCon defs = mergeNormResWith (\x' y' -> return (mergeMin defs x' y')) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == divTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y'))) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == modTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y'))) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == flogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y'))) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == clogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y'))) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == logTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y'))) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == gcdTyCon defs = mergeNormResWith (\x' y' -> return (mergeGCD x' y')) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == lcmTyCon defs = mergeNormResWith (\x' y' -> return (mergeLCM x' y')) - (normaliseNat defs x) - (normaliseNat defs y) - | tc == typeNatExpTyCon = mergeNormResWith (\x' y' -> return (mergeExp x' y')) - (normaliseNat defs x) - (normaliseNat defs y) - -normaliseNat defs (TyConApp tc tys) = do - let mergeExtraOp [] = [] - mergeExtraOp ((Just (op, Normalised), _):xs) = reifyEOP defs op:mergeExtraOp xs - mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs - - normResults <- lift (sequence (runMaybeT . normaliseNat defs <$> tys)) - let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults) - let tys' = mergeExtraOp (zip normResults tys) - pure (C (CType (TyConApp tc tys')), anyNormalised) - -normaliseNat _ t = return (C (CType t), Untouched) - --- | Result of comparing two 'SOP' terms, returning a potential substitution --- list under which the two terms are equal. -data UnifyResult - = Win -- ^ Two terms are equal - | Lose -- ^ Two terms are /not/ equal - | Draw -- ^ We don't know if the two terms are equal - -instance Outputable UnifyResult where - ppr Win = text "Win" - ppr Lose = text "Lose" - ppr Draw = text "Draw" - -unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult -unifyExtra ct u v = do - tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v) - return (unifyExtra' u v) - -unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult -unifyExtra' u v - | eqFV u v - = go u v - | otherwise - = Draw - where - go a b | a == b = Win - -- The following operations commute - go (Max a b) (Max x y) = commuteResult (go a y) (go b x) - go (Min a b) (Min x y) = commuteResult (go a y) (go b x) - go (GCD a b) (GCD x y) = commuteResult (go a y) (go b x) - go (LCM a b) (LCM x y) = commuteResult (go a y) (go b x) - -- If there are operations contained in the type which this solver does - -- not understand, then the result is a Draw - go a b = if containsConstants a || containsConstants b then Draw else Lose - - commuteResult Win Win = Win - commuteResult Lose _ = Lose - commuteResult _ Lose = Lose - commuteResult _ _ = Draw - -fvOP :: ExtraOp -> UniqSet TyVar -fvOP (I _) = emptyUniqSet -fvOP (V v) = unitUniqSet v -fvOP (C _) = emptyUniqSet -fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y -fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y -fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y -fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y -fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y - -eqFV :: ExtraOp -> ExtraOp -> Bool -eqFV = (==) `on` fvOP - -containsConstants :: ExtraOp -> Bool -containsConstants (I _) = False -containsConstants (V _) = False -containsConstants (C _) = True -containsConstants (Max x y) = containsConstants x || containsConstants y -containsConstants (Min x y) = containsConstants x || containsConstants y -containsConstants (Div x y) = containsConstants x || containsConstants y -containsConstants (Mod x y) = containsConstants x || containsConstants y -containsConstants (FLog x y) = containsConstants x || containsConstants y -containsConstants (CLog x y) = containsConstants x || containsConstants y -containsConstants (Log x y) = containsConstants x || containsConstants y -containsConstants (GCD x y) = containsConstants x || containsConstants y -containsConstants (LCM x y) = containsConstants x || containsConstants y -containsConstants (Exp x y) = containsConstants x || containsConstants y +{-| +Copyright : (C) 2015-2016, University of Twente, + 2017 , QBayLogic B.V. +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij +-} + +{-# LANGUAGE CPP #-} + +module GHC.TypeLits.Extra.Solver.Unify + ( ExtraDefs (..) + , UnifyResult (..) + , NormaliseResult + , normaliseNat + , unifyExtra + ) +where + +-- external +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Data.Maybe (catMaybes) +import Data.Function (on) +import GHC.TypeLits.Normalise.Unify (CType (..)) + +-- GHC API +#if MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Types.Literals (typeNatExpTyCon) +import GHC.Core.TyCo.Rep (Type (..), TyLit (..)) +import GHC.Core.Type (TyVar, coreView) +import GHC.Tc.Plugin (TcPluginM, tcPluginTrace) +import GHC.Tc.Types.Constraint (Ct) +import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) +import GHC.Utils.Outputable (Outputable (..), ($$), text) +#else +import Outputable (Outputable (..), ($$), text) +import TcPluginM (TcPluginM, tcPluginTrace) +import TcTypeNats (typeNatExpTyCon) +import Type (TyVar, coreView) +import TyCoRep (Type (..), TyLit (..)) +import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) +#if MIN_VERSION_ghc(8,10,0) +import Constraint (Ct) +#else +import TcRnMonad (Ct) +#endif +#endif + +-- internal +import GHC.TypeLits.Extra.Solver.Operations + +mergeNormResWith + :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult) + -> MaybeT TcPluginM NormaliseResult + -> MaybeT TcPluginM NormaliseResult + -> MaybeT TcPluginM NormaliseResult +mergeNormResWith f x y = do + (x', n1) <- x + (y', n2) <- y + (res, n3) <- f x' y' + pure (res, n1 `mergeNormalised` n2 `mergeNormalised` n3) + + +normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult +normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1 +normaliseNat _ (TyVarTy v) = pure (V v, Untouched) +normaliseNat _ (LitTy (NumTyLit i)) = pure (I i, Untouched) +normaliseNat defs (TyConApp tc [x,y]) + | tc == maxTyCon defs = mergeNormResWith (\x' y' -> return (mergeMax defs x' y')) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == minTyCon defs = mergeNormResWith (\x' y' -> return (mergeMin defs x' y')) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == divTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeDiv x' y'))) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == modTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeMod x' y'))) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == flogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeFLog x' y'))) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == clogTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeCLog x' y'))) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == logTyCon defs = mergeNormResWith (\x' y' -> MaybeT (return (mergeLog x' y'))) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == gcdTyCon defs = mergeNormResWith (\x' y' -> return (mergeGCD x' y')) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == lcmTyCon defs = mergeNormResWith (\x' y' -> return (mergeLCM x' y')) + (normaliseNat defs x) + (normaliseNat defs y) + | tc == typeNatExpTyCon = mergeNormResWith (\x' y' -> return (mergeExp x' y')) + (normaliseNat defs x) + (normaliseNat defs y) + +normaliseNat defs (TyConApp tc tys) = do + let mergeExtraOp [] = [] + mergeExtraOp ((Just (op, Normalised), _):xs) = reifyEOP defs op:mergeExtraOp xs + mergeExtraOp ((_, ty):xs) = ty:mergeExtraOp xs + + normResults <- lift (sequence (runMaybeT . normaliseNat defs <$> tys)) + let anyNormalised = foldr mergeNormalised Untouched (snd <$> catMaybes normResults) + let tys' = mergeExtraOp (zip normResults tys) + pure (C (CType (TyConApp tc tys')), anyNormalised) + +normaliseNat _ t = return (C (CType t), Untouched) + +-- | Result of comparing two 'SOP' terms, returning a potential substitution +-- list under which the two terms are equal. +data UnifyResult + = Win -- ^ Two terms are equal + | Lose -- ^ Two terms are /not/ equal + | Draw -- ^ We don't know if the two terms are equal + +instance Outputable UnifyResult where + ppr Win = text "Win" + ppr Lose = text "Lose" + ppr Draw = text "Draw" + +unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult +unifyExtra ct u v = do + tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v) + return (unifyExtra' u v) + +unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult +unifyExtra' u v + | eqFV u v + = go u v + | otherwise + = Draw + where + go a b | a == b = Win + -- The following operations commute + go (Max a b) (Max x y) = commuteResult (go a y) (go b x) + go (Min a b) (Min x y) = commuteResult (go a y) (go b x) + go (GCD a b) (GCD x y) = commuteResult (go a y) (go b x) + go (LCM a b) (LCM x y) = commuteResult (go a y) (go b x) + -- If there are operations contained in the type which this solver does + -- not understand, then the result is a Draw + go a b = if containsConstants a || containsConstants b then Draw else Lose + + commuteResult Win Win = Win + commuteResult Lose _ = Lose + commuteResult _ Lose = Lose + commuteResult _ _ = Draw + +fvOP :: ExtraOp -> UniqSet TyVar +fvOP (I _) = emptyUniqSet +fvOP (V v) = unitUniqSet v +fvOP (C _) = emptyUniqSet +fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y +fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y +fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y +fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y +fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y + +eqFV :: ExtraOp -> ExtraOp -> Bool +eqFV = (==) `on` fvOP + +containsConstants :: ExtraOp -> Bool +containsConstants (I _) = False +containsConstants (V _) = False +containsConstants (C _) = True +containsConstants (Max x y) = containsConstants x || containsConstants y +containsConstants (Min x y) = containsConstants x || containsConstants y +containsConstants (Div x y) = containsConstants x || containsConstants y +containsConstants (Mod x y) = containsConstants x || containsConstants y +containsConstants (FLog x y) = containsConstants x || containsConstants y +containsConstants (CLog x y) = containsConstants x || containsConstants y +containsConstants (Log x y) = containsConstants x || containsConstants y +containsConstants (GCD x y) = containsConstants x || containsConstants y +containsConstants (LCM x y) = containsConstants x || containsConstants y +containsConstants (Exp x y) = containsConstants x || containsConstants y diff --git a/tests-ghc-9.4/ErrorTests.hs b/tests-ghc-9.4/ErrorTests.hs --- a/tests-ghc-9.4/ErrorTests.hs +++ b/tests-ghc-9.4/ErrorTests.hs @@ -1,245 +1,253 @@ -{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} -#if __GLASGOW_HASKELL__ >= 805 -{-# LANGUAGE NoStarIsType #-} -#endif -{-# OPTIONS_GHC -fdefer-type-errors #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} - -module ErrorTests where - -import Data.Proxy -import GHC.TypeLits -import GHC.TypeLits.Extra - -testFail1 :: Proxy (GCD 6 8) -> Proxy 4 -testFail1 = id - -testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9)) -testFail2 = id - -testFail3 :: Proxy (CLog 3 10) -> Proxy 2 -testFail3 = id - -testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9)) -testFail4 = id - -testFail5 :: Proxy (CLog 0 4) -> Proxy 100 -testFail5 = id - -testFail6 :: Proxy (CLog 1 4) -> Proxy 100 -testFail6 = id - -testFail7 :: Proxy (CLog 4 0) -> Proxy 0 -testFail7 = id - -testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y -testFail8 = id - -testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y -testFail9 = id - -testFail10 :: Integer -testFail10 = natVal (Proxy :: Proxy (CLog 1 4)) - -testFail11 :: Integer -testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4))) - -testFail12 :: Proxy (Div 4 0) -> Proxy 4 -testFail12 = id - -testFail13 :: Proxy (Mod 4 0) -> Proxy 4 -testFail13 = id - -testFail14 :: Proxy (FLog 0 4) -> Proxy 100 -testFail14 = id - -testFail15 :: Proxy (FLog 1 4) -> Proxy 100 -testFail15 = id - -testFail16 :: Proxy (FLog 4 0) -> Proxy 0 -testFail16 = id - -testFail17 :: Proxy (LCM 6 8) -> Proxy 48 -testFail17 = id - -testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9)) -testFail18 = id - -testFail19 :: Integer -testFail19 = natVal (Proxy :: Proxy (Log 3 0)) - -testFail20 :: Integer -testFail20 = natVal (Proxy :: Proxy (Log 3 10)) - -testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a -testFail21 _ _ = id - -testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b) -testFail22 _ _ = id - -testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> () -testFail23' _ _ = () - -testFail23 :: () -testFail23 = testFail23' (Proxy @18) (Proxy @3) - -testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True -testFail24 _ _ _ = id - -testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True -testFail25 _ _ = id - --- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true. -testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n -testFail26' _ _ _ = id - -testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6) - -testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True -testFail27 _ = id - -testFail1Errors = - ["Expected: Proxy (GCD 6 8) -> Proxy 4" - ," Actual: Proxy 4 -> Proxy 4" - ] - -testFail2Errors = - ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)" - ," Actual: Proxy (2 + x) -> Proxy (2 + x)" - ] - -testFail3Errors = - ["Expected: Proxy (CLog 3 10) -> Proxy 2" - ," Actual: Proxy 2 -> Proxy 2" - ] - -testFail4Errors = - ["Expected: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" - ," Actual: Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)" - ] - -testFail5Errors = - ["Expected: Proxy (CLog 0 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail6Errors = - ["Expected: Proxy (CLog 1 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail7Errors = - ["Expected: Proxy (CLog 4 0) -> Proxy 0" - ," Actual: Proxy 0 -> Proxy 0" - ] - -testFail8Errors = - ["Expected: Proxy (CLog 1 (1 ^ y)) -> Proxy y" - ," Actual: Proxy y -> Proxy y" - ] - -testFail9Errors = - ["Expected: Proxy (CLog 0 (0 ^ y)) -> Proxy y" - ," Actual: Proxy y -> Proxy y" - ] - -testFail12Errors = - ["Expected: Proxy (Div 4 0) -> Proxy 4" - ," Actual: Proxy 4 -> Proxy 4" - ] - -testFail13Errors = - ["Expected: Proxy (Mod 4 0) -> Proxy 4" - ," Actual: Proxy 4 -> Proxy 4" - ] - -testFail14Errors = - ["Expected: Proxy (FLog 0 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail15Errors = - ["Expected: Proxy (FLog 1 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail16Errors = - ["Expected: Proxy (FLog 4 0) -> Proxy 0" - ," Actual: Proxy 0 -> Proxy 0" - ] - -testFail17Errors = - ["Expected: Proxy (LCM 6 8) -> Proxy 48" - ," Actual: Proxy 48 -> Proxy 48" - ] - -testFail18Errors = - ["Expected: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)" - ," Actual: Proxy (24 + x) -> Proxy (24 + x)" - ] - -testFail19Errors = - ["Couldn't match type: FLog 3 0" - ," with: CLog 3 0"] - -testFail20Errors = - ["Couldn't match type: FLog 3 10" - ," with: CLog 3 10"] - -testFail21Errors = - ["Expected: Proxy (Min a (a * b)) -> Proxy a" - ," Actual: Proxy a -> Proxy a" - ] - -testFail22Errors = - ["Expected: Proxy (Max a (a * b)) -> Proxy (a * b)" - ," Actual: Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"] - -testFail27Errors = - ["Expected: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True" - ," Actual: Proxy 'True -> Proxy 'True" - ] - -testFail10Errors = - ["Cannot satisfy: 2 <= 1"] - -testFail11Errors = - ["Cannot satisfy: CLog 2 4 <= CLog 4 4"] - -testFail23Errors = - ["Couldn't match type ‘'True’ with ‘'False’"] - -testFail24Errors = -#if __GLASGOW_HASKELL__ >= 910 - ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond" - ,"(CmpNat z (Max x y)) 'True 'True 'False’" - ,"with ‘'True’"] -#else - ["Couldn't match type ‘Data.Type.Ord.OrdCond" - ,"(CmpNat z (Max x y)) 'True 'True 'False’" - ,"with ‘'True’"] -#endif - -testFail25Errors = -#if __GLASGOW_HASKELL__ >= 910 - ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond" - ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" - ,"with ‘'True’"] -#else - ["Couldn't match type ‘Data.Type.Ord.OrdCond" - ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" - ,"with ‘'True’"] -#endif - -testFail26Errors = -#if __GLASGOW_HASKELL__ >= 906 - ["Could not deduce ‘Max x y ~ n’" - ,"from the context: (x <=? n) ~ True" - ] -#else - ["Could not deduce (Max x y ~ n)" - ,"from the context: (x <=? n) ~ 'True" - ] -#endif +{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE NoStarIsType #-} +#endif +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} + +module ErrorTests where + +import Data.Proxy +import GHC.TypeLits +import GHC.TypeLits.Extra + +testFail1 :: Proxy (GCD 6 8) -> Proxy 4 +testFail1 = id + +testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9)) +testFail2 = id + +testFail3 :: Proxy (CLog 3 10) -> Proxy 2 +testFail3 = id + +testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9)) +testFail4 = id + +testFail5 :: Proxy (CLog 0 4) -> Proxy 100 +testFail5 = id + +testFail6 :: Proxy (CLog 1 4) -> Proxy 100 +testFail6 = id + +testFail7 :: Proxy (CLog 4 0) -> Proxy 0 +testFail7 = id + +testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y +testFail8 = id + +testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y +testFail9 = id + +testFail10 :: Integer +testFail10 = natVal (Proxy :: Proxy (CLog 1 4)) + +testFail11 :: Integer +testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4))) + +testFail12 :: Proxy (Div 4 0) -> Proxy 4 +testFail12 = id + +testFail13 :: Proxy (Mod 4 0) -> Proxy 4 +testFail13 = id + +testFail14 :: Proxy (FLog 0 4) -> Proxy 100 +testFail14 = id + +testFail15 :: Proxy (FLog 1 4) -> Proxy 100 +testFail15 = id + +testFail16 :: Proxy (FLog 4 0) -> Proxy 0 +testFail16 = id + +testFail17 :: Proxy (LCM 6 8) -> Proxy 48 +testFail17 = id + +testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9)) +testFail18 = id + +testFail19 :: Integer +testFail19 = natVal (Proxy :: Proxy (Log 3 0)) + +testFail20 :: Integer +testFail20 = natVal (Proxy :: Proxy (Log 3 10)) + +testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a +testFail21 _ _ = id + +testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b) +testFail22 _ _ = id + +testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> () +testFail23' _ _ = () + +testFail23 :: () +testFail23 = testFail23' (Proxy @18) (Proxy @3) + +testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True +testFail24 _ _ _ = id + +testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True +testFail25 _ _ = id + +-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true. +testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n +testFail26' _ _ _ = id + +testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6) + +testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True +testFail27 _ = id + +testFail1Errors = + ["Expected: Proxy (GCD 6 8) -> Proxy 4" + ," Actual: Proxy 4 -> Proxy 4" + ] + +testFail2Errors = + ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)" + ," Actual: Proxy (2 + x) -> Proxy (2 + x)" + ] + +testFail3Errors = + ["Expected: Proxy (CLog 3 10) -> Proxy 2" + ," Actual: Proxy 2 -> Proxy 2" + ] + +testFail4Errors = + ["Expected: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" + ," Actual: Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)" + ] + +testFail5Errors = + ["Expected: Proxy (CLog 0 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail6Errors = + ["Expected: Proxy (CLog 1 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail7Errors = + ["Expected: Proxy (CLog 4 0) -> Proxy 0" + ," Actual: Proxy 0 -> Proxy 0" + ] + +testFail8Errors = + ["Expected: Proxy (CLog 1 (1 ^ y)) -> Proxy y" + ," Actual: Proxy y -> Proxy y" + ] + +testFail9Errors = + ["Expected: Proxy (CLog 0 (0 ^ y)) -> Proxy y" + ," Actual: Proxy y -> Proxy y" + ] + +testFail12Errors = + ["Expected: Proxy (Div 4 0) -> Proxy 4" + ," Actual: Proxy 4 -> Proxy 4" + ] + +testFail13Errors = + ["Expected: Proxy (Mod 4 0) -> Proxy 4" + ," Actual: Proxy 4 -> Proxy 4" + ] + +testFail14Errors = + ["Expected: Proxy (FLog 0 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail15Errors = + ["Expected: Proxy (FLog 1 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail16Errors = + ["Expected: Proxy (FLog 4 0) -> Proxy 0" + ," Actual: Proxy 0 -> Proxy 0" + ] + +testFail17Errors = + ["Expected: Proxy (LCM 6 8) -> Proxy 48" + ," Actual: Proxy 48 -> Proxy 48" + ] + +testFail18Errors = + ["Expected: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)" + ," Actual: Proxy (24 + x) -> Proxy (24 + x)" + ] + +testFail19Errors = + ["Couldn't match type: FLog 3 0" + ," with: CLog 3 0"] + +testFail20Errors = + ["Couldn't match type: FLog 3 10" + ," with: CLog 3 10"] + +testFail21Errors = + ["Expected: Proxy (Min a (a * b)) -> Proxy a" + ," Actual: Proxy a -> Proxy a" + ] + +testFail22Errors = + ["Expected: Proxy (Max a (a * b)) -> Proxy (a * b)" + ," Actual: Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"] + +testFail27Errors = + ["Expected: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True" + ," Actual: Proxy 'True -> Proxy 'True" + ] + +testFail10Errors = + ["Cannot satisfy: 2 <= 1"] + +testFail11Errors = + ["Cannot satisfy: CLog 2 4 <= CLog 4 4"] + +testFail23Errors = + ["Couldn't match type ‘'True’ with ‘'False’"] + +testFail24Errors = +#if __GLASGOW_HASKELL__ >= 912 + ["Couldn't match type ‘ghc-internal-9.1201.0:GHC.Internal.Data.Type.Ord.OrdCond" + ,"(CmpNat z (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#elif __GLASGOW_HASKELL__ >= 910 + ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond" + ,"(CmpNat z (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#else + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat z (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#endif + +testFail25Errors = +#if __GLASGOW_HASKELL__ >= 912 + ["Couldn't match type ‘ghc-internal-9.1201.0:GHC.Internal.Data.Type.Ord.OrdCond" + ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#elif __GLASGOW_HASKELL__ >= 910 + ["Couldn't match type ‘ghc-internal-9.1001.0:GHC.Internal.Data.Type.Ord.OrdCond" + ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#else + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#endif + +testFail26Errors = +#if __GLASGOW_HASKELL__ >= 906 + ["Could not deduce ‘Max x y ~ n’" + ,"from the context: (x <=? n) ~ True" + ] +#else + ["Could not deduce (Max x y ~ n)" + ,"from the context: (x <=? n) ~ 'True" + ] +#endif diff --git a/tests-pre-ghc-9.4/ErrorTests.hs b/tests-pre-ghc-9.4/ErrorTests.hs --- a/tests-pre-ghc-9.4/ErrorTests.hs +++ b/tests-pre-ghc-9.4/ErrorTests.hs @@ -1,347 +1,347 @@ -{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} -#if __GLASGOW_HASKELL__ >= 805 -{-# LANGUAGE NoStarIsType #-} -#endif -{-# OPTIONS_GHC -fdefer-type-errors #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} - -module ErrorTests where - -import Data.Proxy -import GHC.TypeLits -import GHC.TypeLits.Extra - -testFail1 :: Proxy (GCD 6 8) -> Proxy 4 -testFail1 = id - -testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9)) -testFail2 = id - -testFail3 :: Proxy (CLog 3 10) -> Proxy 2 -testFail3 = id - -testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9)) -testFail4 = id - -testFail5 :: Proxy (CLog 0 4) -> Proxy 100 -testFail5 = id - -testFail6 :: Proxy (CLog 1 4) -> Proxy 100 -testFail6 = id - -testFail7 :: Proxy (CLog 4 0) -> Proxy 0 -testFail7 = id - -testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y -testFail8 = id - -testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y -testFail9 = id - -testFail10 :: Integer -testFail10 = natVal (Proxy :: Proxy (CLog 1 4)) - -testFail11 :: Integer -testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4))) - -testFail12 :: Proxy (Div 4 0) -> Proxy 4 -testFail12 = id - -testFail13 :: Proxy (Mod 4 0) -> Proxy 4 -testFail13 = id - -testFail14 :: Proxy (FLog 0 4) -> Proxy 100 -testFail14 = id - -testFail15 :: Proxy (FLog 1 4) -> Proxy 100 -testFail15 = id - -testFail16 :: Proxy (FLog 4 0) -> Proxy 0 -testFail16 = id - -testFail17 :: Proxy (LCM 6 8) -> Proxy 48 -testFail17 = id - -testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9)) -testFail18 = id - -testFail19 :: Integer -testFail19 = natVal (Proxy :: Proxy (Log 3 0)) - -testFail20 :: Integer -testFail20 = natVal (Proxy :: Proxy (Log 3 10)) - -testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a -testFail21 _ _ = id - -testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b) -testFail22 _ _ = id - -testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> () -testFail23' _ _ = () - -testFail23 :: () -testFail23 = testFail23' (Proxy @18) (Proxy @3) - -testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True -testFail24 _ _ _ = id - -testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True -testFail25 _ _ = id - --- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true. -testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n -testFail26' _ _ _ = id - -testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6) - -testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True -testFail27 _ = id - -#if __GLASGOW_HASKELL__ >= 900 -testFail1Errors = - ["Expected: Proxy (GCD 6 8) -> Proxy 4" - ," Actual: Proxy 4 -> Proxy 4" - ] - -testFail2Errors = - ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)" - ," Actual: Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)" - ] - -testFail3Errors = - ["Expected: Proxy (CLog 3 10) -> Proxy 2" - ," Actual: Proxy 2 -> Proxy 2" - ] - -testFail4Errors = - ["Expected: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" - ," Actual: Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)" - ] - -testFail5Errors = - ["Expected: Proxy (CLog 0 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail6Errors = - ["Expected: Proxy (CLog 1 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail7Errors = - ["Expected: Proxy (CLog 4 0) -> Proxy 0" - ," Actual: Proxy 0 -> Proxy 0" - ] - -testFail8Errors = - ["Expected: Proxy (CLog 1 (1 ^ y)) -> Proxy y" - ," Actual: Proxy y -> Proxy y" - ] - -testFail9Errors = - ["Expected: Proxy (CLog 0 (0 ^ y)) -> Proxy y" - ," Actual: Proxy y -> Proxy y" - ] - -testFail12Errors = - ["Expected: Proxy (Div 4 0) -> Proxy 4" - ," Actual: Proxy 4 -> Proxy 4" - ] - -testFail13Errors = - ["Expected: Proxy (Mod 4 0) -> Proxy 4" - ," Actual: Proxy 4 -> Proxy 4" - ] - -testFail14Errors = - ["Expected: Proxy (FLog 0 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail15Errors = - ["Expected: Proxy (FLog 1 4) -> Proxy 100" - ," Actual: Proxy 100 -> Proxy 100" - ] - -testFail16Errors = - ["Expected: Proxy (FLog 4 0) -> Proxy 0" - ," Actual: Proxy 0 -> Proxy 0" - ] - -testFail17Errors = - ["Expected: Proxy (LCM 6 8) -> Proxy 48" - ," Actual: Proxy 48 -> Proxy 48" - ] - -testFail18Errors = - ["Expected: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)" - ," Actual: Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)" - ] - -testFail19Errors = - ["Couldn't match type: FLog 3 0" - ," with: CLog 3 0"] - -testFail20Errors = - ["Couldn't match type: FLog 3 10" - ," with: CLog 3 10"] - -testFail21Errors = - ["Expected: Proxy (Min a (a * b)) -> Proxy a" - ," Actual: Proxy a -> Proxy a" - ] - -testFail22Errors = - ["Expected: Proxy (Max a (a * b)) -> Proxy (a * b)" - ," Actual: Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"] - -testFail27Errors = - ["Expected: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True" - ," Actual: Proxy 'True -> Proxy 'True" - ] -#else -testFail1Errors = - ["Expected type: Proxy (GCD 6 8) -> Proxy 4" - ,"Actual type: Proxy 4 -> Proxy 4" - ] - -testFail2Errors = - ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)" - ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)" - ] - -testFail3Errors = - ["Expected type: Proxy (CLog 3 10) -> Proxy 2" - ,"Actual type: Proxy 2 -> Proxy 2" - ] - -testFail4Errors = - ["Expected type: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" - ,"Actual type: Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)" - ] - -testFail5Errors = - ["Expected type: Proxy (CLog 0 4) -> Proxy 100" - ,"Actual type: Proxy 100 -> Proxy 100" - ] - -testFail6Errors = - ["Expected type: Proxy (CLog 1 4) -> Proxy 100" - ,"Actual type: Proxy 100 -> Proxy 100" - ] - -testFail7Errors = - ["Expected type: Proxy (CLog 4 0) -> Proxy 0" - ,"Actual type: Proxy 0 -> Proxy 0" - ] - -testFail8Errors = - ["Expected type: Proxy (CLog 1 (1 ^ y)) -> Proxy y" - ,"Actual type: Proxy y -> Proxy y" - ] - -testFail9Errors = - ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y" - ,"Actual type: Proxy y -> Proxy y" - ] - -testFail12Errors = - ["Expected type: Proxy (Div 4 0) -> Proxy 4" - ,"Actual type: Proxy 4 -> Proxy 4" - ] - -testFail13Errors = - ["Expected type: Proxy (Mod 4 0) -> Proxy 4" - ,"Actual type: Proxy 4 -> Proxy 4" - ] - -testFail14Errors = - ["Expected type: Proxy (FLog 0 4) -> Proxy 100" - ,"Actual type: Proxy 100 -> Proxy 100" - ] - -testFail15Errors = - ["Expected type: Proxy (FLog 1 4) -> Proxy 100" - ,"Actual type: Proxy 100 -> Proxy 100" - ] - -testFail16Errors = - ["Expected type: Proxy (FLog 4 0) -> Proxy 0" - ,"Actual type: Proxy 0 -> Proxy 0" - ] - -testFail17Errors = - ["Expected type: Proxy (LCM 6 8) -> Proxy 48" - ,"Actual type: Proxy 48 -> Proxy 48" - ] - -testFail18Errors = - ["Expected type: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)" - ,"Actual type: Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)" - ] - -testFail19Errors = - ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"] - -testFail20Errors = - ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"] - -testFail21Errors = - ["Expected type: Proxy (Min a (a * b)) -> Proxy a" - ,"Actual type: Proxy a -> Proxy a" - ] - -testFail22Errors = - ["Expected type: Proxy (Max a (a * b)) -> Proxy (a * b)" - ,"Actual type: Proxy (a * b) -> Proxy (a * b)"] - -testFail27Errors = - ["Expected type: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True" - ,"Actual type: Proxy 'True -> Proxy 'True" - ] -#endif - -testFail10Errors = - ["Couldn't match type ‘'False’ with ‘'True’"] - -testFail11Errors = -#if __GLASGOW_HASKELL__ >= 902 - ["Couldn't match type ‘Data.Type.Ord.OrdCond" - ,"(CmpNat (CLog 2 4) (CLog 4 4)) 'True 'True 'False’" - ,"with ‘'True’"] -#else - ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"] -#endif - -testFail23Errors = -#if __GLASGOW_HASKELL__ >= 804 - ["Couldn't match type ‘'True’ with ‘'False’"] -#else - ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"] -#endif - -testFail24Errors = -#if __GLASGOW_HASKELL__ >= 902 - ["Couldn't match type ‘Data.Type.Ord.OrdCond" - ,"(CmpNat z (Max x y)) 'True 'True 'False’" - ,"with ‘'True’"] -#else - ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"] -#endif - -testFail25Errors = -#if __GLASGOW_HASKELL__ >= 902 - ["Couldn't match type ‘Data.Type.Ord.OrdCond" - ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" - ,"with ‘'True’"] -#else - ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"] -#endif - -testFail26Errors = - ["Could not deduce: Max x y ~ n" - ,"from the context: (x <=? n) ~ 'True" - ] +{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE NoStarIsType #-} +#endif +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} + +module ErrorTests where + +import Data.Proxy +import GHC.TypeLits +import GHC.TypeLits.Extra + +testFail1 :: Proxy (GCD 6 8) -> Proxy 4 +testFail1 = id + +testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9)) +testFail2 = id + +testFail3 :: Proxy (CLog 3 10) -> Proxy 2 +testFail3 = id + +testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9)) +testFail4 = id + +testFail5 :: Proxy (CLog 0 4) -> Proxy 100 +testFail5 = id + +testFail6 :: Proxy (CLog 1 4) -> Proxy 100 +testFail6 = id + +testFail7 :: Proxy (CLog 4 0) -> Proxy 0 +testFail7 = id + +testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y +testFail8 = id + +testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y +testFail9 = id + +testFail10 :: Integer +testFail10 = natVal (Proxy :: Proxy (CLog 1 4)) + +testFail11 :: Integer +testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4))) + +testFail12 :: Proxy (Div 4 0) -> Proxy 4 +testFail12 = id + +testFail13 :: Proxy (Mod 4 0) -> Proxy 4 +testFail13 = id + +testFail14 :: Proxy (FLog 0 4) -> Proxy 100 +testFail14 = id + +testFail15 :: Proxy (FLog 1 4) -> Proxy 100 +testFail15 = id + +testFail16 :: Proxy (FLog 4 0) -> Proxy 0 +testFail16 = id + +testFail17 :: Proxy (LCM 6 8) -> Proxy 48 +testFail17 = id + +testFail18 :: Proxy ((LCM 6 8) + x) -> Proxy (x + (LCM 6 9)) +testFail18 = id + +testFail19 :: Integer +testFail19 = natVal (Proxy :: Proxy (Log 3 0)) + +testFail20 :: Integer +testFail20 = natVal (Proxy :: Proxy (Log 3 10)) + +testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a +testFail21 _ _ = id + +testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b) +testFail22 _ _ = id + +testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> () +testFail23' _ _ = () + +testFail23 :: () +testFail23 = testFail23' (Proxy @18) (Proxy @3) + +testFail24 :: Proxy x -> Proxy y -> Proxy z -> Proxy (z <=? Max x y) -> Proxy True +testFail24 _ _ _ = id + +testFail25 :: Proxy x -> Proxy y -> Proxy (x+1 <=? Max x y) -> Proxy True +testFail25 _ _ = id + +-- While n ~ (Max x y) implies x <= n (see test46), the reverse is not true. +testFail26' :: ((x <=? n) ~ True) => Proxy x -> Proxy y -> Proxy n -> Proxy ((Max x y)) -> Proxy n +testFail26' _ _ _ = id + +testFail26 = testFail26' (Proxy @4) (Proxy @6) (Proxy @6) + +testFail27 :: Proxy n -> Proxy (n + 2 <=? Max (n + 1) 1) -> Proxy True +testFail27 _ = id + +#if __GLASGOW_HASKELL__ >= 900 +testFail1Errors = + ["Expected: Proxy (GCD 6 8) -> Proxy 4" + ," Actual: Proxy 4 -> Proxy 4" + ] + +testFail2Errors = + ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)" + ," Actual: Proxy (GCD 6 8 + x) -> Proxy (GCD 6 8 + x)" + ] + +testFail3Errors = + ["Expected: Proxy (CLog 3 10) -> Proxy 2" + ," Actual: Proxy 2 -> Proxy 2" + ] + +testFail4Errors = + ["Expected: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" + ," Actual: Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)" + ] + +testFail5Errors = + ["Expected: Proxy (CLog 0 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail6Errors = + ["Expected: Proxy (CLog 1 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail7Errors = + ["Expected: Proxy (CLog 4 0) -> Proxy 0" + ," Actual: Proxy 0 -> Proxy 0" + ] + +testFail8Errors = + ["Expected: Proxy (CLog 1 (1 ^ y)) -> Proxy y" + ," Actual: Proxy y -> Proxy y" + ] + +testFail9Errors = + ["Expected: Proxy (CLog 0 (0 ^ y)) -> Proxy y" + ," Actual: Proxy y -> Proxy y" + ] + +testFail12Errors = + ["Expected: Proxy (Div 4 0) -> Proxy 4" + ," Actual: Proxy 4 -> Proxy 4" + ] + +testFail13Errors = + ["Expected: Proxy (Mod 4 0) -> Proxy 4" + ," Actual: Proxy 4 -> Proxy 4" + ] + +testFail14Errors = + ["Expected: Proxy (FLog 0 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail15Errors = + ["Expected: Proxy (FLog 1 4) -> Proxy 100" + ," Actual: Proxy 100 -> Proxy 100" + ] + +testFail16Errors = + ["Expected: Proxy (FLog 4 0) -> Proxy 0" + ," Actual: Proxy 0 -> Proxy 0" + ] + +testFail17Errors = + ["Expected: Proxy (LCM 6 8) -> Proxy 48" + ," Actual: Proxy 48 -> Proxy 48" + ] + +testFail18Errors = + ["Expected: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)" + ," Actual: Proxy (LCM 6 8 + x) -> Proxy (LCM 6 8 + x)" + ] + +testFail19Errors = + ["Couldn't match type: FLog 3 0" + ," with: CLog 3 0"] + +testFail20Errors = + ["Couldn't match type: FLog 3 10" + ," with: CLog 3 10"] + +testFail21Errors = + ["Expected: Proxy (Min a (a * b)) -> Proxy a" + ," Actual: Proxy a -> Proxy a" + ] + +testFail22Errors = + ["Expected: Proxy (Max a (a * b)) -> Proxy (a * b)" + ," Actual: Proxy (Max a (a * b)) -> Proxy (Max a (a * b))"] + +testFail27Errors = + ["Expected: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True" + ," Actual: Proxy 'True -> Proxy 'True" + ] +#else +testFail1Errors = + ["Expected type: Proxy (GCD 6 8) -> Proxy 4" + ,"Actual type: Proxy 4 -> Proxy 4" + ] + +testFail2Errors = + ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)" + ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)" + ] + +testFail3Errors = + ["Expected type: Proxy (CLog 3 10) -> Proxy 2" + ,"Actual type: Proxy 2 -> Proxy 2" + ] + +testFail4Errors = + ["Expected type: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" + ,"Actual type: Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)" + ] + +testFail5Errors = + ["Expected type: Proxy (CLog 0 4) -> Proxy 100" + ,"Actual type: Proxy 100 -> Proxy 100" + ] + +testFail6Errors = + ["Expected type: Proxy (CLog 1 4) -> Proxy 100" + ,"Actual type: Proxy 100 -> Proxy 100" + ] + +testFail7Errors = + ["Expected type: Proxy (CLog 4 0) -> Proxy 0" + ,"Actual type: Proxy 0 -> Proxy 0" + ] + +testFail8Errors = + ["Expected type: Proxy (CLog 1 (1 ^ y)) -> Proxy y" + ,"Actual type: Proxy y -> Proxy y" + ] + +testFail9Errors = + ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y" + ,"Actual type: Proxy y -> Proxy y" + ] + +testFail12Errors = + ["Expected type: Proxy (Div 4 0) -> Proxy 4" + ,"Actual type: Proxy 4 -> Proxy 4" + ] + +testFail13Errors = + ["Expected type: Proxy (Mod 4 0) -> Proxy 4" + ,"Actual type: Proxy 4 -> Proxy 4" + ] + +testFail14Errors = + ["Expected type: Proxy (FLog 0 4) -> Proxy 100" + ,"Actual type: Proxy 100 -> Proxy 100" + ] + +testFail15Errors = + ["Expected type: Proxy (FLog 1 4) -> Proxy 100" + ,"Actual type: Proxy 100 -> Proxy 100" + ] + +testFail16Errors = + ["Expected type: Proxy (FLog 4 0) -> Proxy 0" + ,"Actual type: Proxy 0 -> Proxy 0" + ] + +testFail17Errors = + ["Expected type: Proxy (LCM 6 8) -> Proxy 48" + ,"Actual type: Proxy 48 -> Proxy 48" + ] + +testFail18Errors = + ["Expected type: Proxy (LCM 6 8 + x) -> Proxy (x + LCM 6 9)" + ,"Actual type: Proxy (x + LCM 6 9) -> Proxy (x + LCM 6 9)" + ] + +testFail19Errors = + ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"] + +testFail20Errors = + ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"] + +testFail21Errors = + ["Expected type: Proxy (Min a (a * b)) -> Proxy a" + ,"Actual type: Proxy a -> Proxy a" + ] + +testFail22Errors = + ["Expected type: Proxy (Max a (a * b)) -> Proxy (a * b)" + ,"Actual type: Proxy (a * b) -> Proxy (a * b)"] + +testFail27Errors = + ["Expected type: Proxy ((n + 2) <=? Max (n + 1) 1) -> Proxy 'True" + ,"Actual type: Proxy 'True -> Proxy 'True" + ] +#endif + +testFail10Errors = + ["Couldn't match type ‘'False’ with ‘'True’"] + +testFail11Errors = +#if __GLASGOW_HASKELL__ >= 902 + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat (CLog 2 4) (CLog 4 4)) 'True 'True 'False’" + ,"with ‘'True’"] +#else + ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"] +#endif + +testFail23Errors = +#if __GLASGOW_HASKELL__ >= 804 + ["Couldn't match type ‘'True’ with ‘'False’"] +#else + ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"] +#endif + +testFail24Errors = +#if __GLASGOW_HASKELL__ >= 902 + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat z (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#else + ["Couldn't match type ‘z <=? Max x y’ with ‘'True’"] +#endif + +testFail25Errors = +#if __GLASGOW_HASKELL__ >= 902 + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] +#else + ["Couldn't match type ‘(x + 1) <=? Max x y’ with ‘'True’"] +#endif + +testFail26Errors = + ["Could not deduce: Max x y ~ n" + ,"from the context: (x <=? n) ~ 'True" + ] diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,463 +1,463 @@ -{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} -#if __GLASGOW_HASKELL__ >= 805 -{-# LANGUAGE NoStarIsType #-} -#endif -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} - -import Data.List (isInfixOf) -import Data.Proxy -import Data.Type.Bool -import Control.Exception -import Test.Tasty -import Test.Tasty.HUnit - -import ErrorTests - -import GHC.TypeLits -import GHC.TypeLits.Extra - -test1 :: Proxy (GCD 6 8) -> Proxy 2 -test1 = id - -test2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 10 8)) -test2 = id - -test3 :: Proxy (CLog 3 10) -> Proxy 3 -test3 = id - -test4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 7)) -test4 = id - -test5 :: Proxy (CLog x (x^y)) -> Proxy y -test5 = id - -test6 :: Integer -test6 = natVal (Proxy :: Proxy (CLog 6 8)) - -test7 :: Integer -test7 = natVal (Proxy :: Proxy (CLog 3 10)) - -test8 :: Integer -test8 = natVal (Proxy :: Proxy ((CLog 2 4) * (3 ^ (CLog 2 4)))) - -test9 :: Integer -test9 = natVal (Proxy :: Proxy (Max (CLog 2 4) (CLog 4 20))) - -test10 :: Proxy (Div 9 3) -> Proxy 3 -test10 = id - -test11 :: Proxy (Div 9 4) -> Proxy 2 -test11 = id - -test12 :: Proxy (Mod 9 3) -> Proxy 0 -test12 = id - -test13 :: Proxy (Mod 9 4) -> Proxy 1 -test13 = id - -test14 :: Integer -test14 = natVal (Proxy :: Proxy (Div 9 3)) - -test15 :: Integer -test15 = natVal (Proxy :: Proxy (Mod 9 4)) - -test16 :: Proxy (LCM 18 7) -> Proxy 126 -test16 = id - -test17 :: Integer -test17 = natVal (Proxy :: Proxy (LCM 18 7)) - -test18 :: Proxy ((LCM 6 4) + x) -> Proxy (x + (LCM 3 4)) -test18 = id - -test19 :: Integer -test19 = natVal (Proxy :: Proxy (FLog 3 1)) - -test20 :: Proxy (FLog 3 1) -> Proxy 0 -test20 = id - -test21 :: Integer -test21 = natVal (Proxy :: Proxy (CLog 3 1)) - -test22 :: Proxy (CLog 3 1) -> Proxy 0 -test22 = id - -test23 :: Integer -test23 = natVal (Proxy :: Proxy (Log 3 1)) - -test24 :: Integer -test24 = natVal (Proxy :: Proxy (Log 3 9)) - -test25 :: Proxy (Log 3 9) -> Proxy 2 -test25 = id - -test26 :: Proxy (b ^ (Log b y)) -> Proxy y -test26 = id - -test27 :: Proxy (Max n n) -> Proxy n -test27 = id - -test28 :: Proxy (Min n n) -> Proxy n -test28 = id - -test29 :: Proxy (Max n n + 1) -> Proxy (1 + n) -test29 = id - -test30 :: Proxy n -> Proxy (1 + Max n n) -> Proxy (Min n n + 1) -test30 _ = id - -test31 :: Proxy (Min n (n + 1)) -> Proxy n -test31 = id - -test32 :: Proxy (Min (n + 1) n) -> Proxy n -test32 = id - -test33 :: Proxy (Max n (n + 1)) -> Proxy (n+1) -test33 = id - -test34 :: Proxy (Max (n + 1) n) -> Proxy (n+1) -test34 = id - -test35 :: Proxy n -> Proxy (1 + Max n (1 + n)) -> Proxy (n + 2) -test35 _ = id - -test36 :: Proxy n -> Proxy (1 + Min n (1 + n)) -> Proxy (n + 1) -test36 _ = id - -test37 :: (1 <= Div l r) => Proxy l -> Proxy r -> () -test37 _ _ = () - -test38 :: Proxy (Min (0-1) 0) -> Proxy (0-1) -test38 = id - -test39 :: Proxy (Max (0-1) 0) -> Proxy (0-1) -test39 = id - -test40 :: Proxy x -> Proxy y -> Proxy (Max x y) -> Proxy (Max y x) -test40 _ _ = id - -test41 :: Proxy x -> Proxy y -> Proxy (Min x y) -> Proxy (Min y x) -test41 _ _ = id - -test42 :: Proxy x -> Proxy y -> Proxy (GCD x y) -> Proxy (GCD y x) -test42 _ _ = id - -test43 :: Proxy x -> Proxy y -> Proxy (LCM x y) -> Proxy (LCM y x) -test43 _ _ = id - -test44 :: Proxy x -> Proxy y -> Proxy (x <=? (Max x y)) -> Proxy True -test44 _ _ = id - -test45 :: Proxy x -> Proxy y -> Proxy (y <=? (Max x y)) -> Proxy True -test45 _ _ = id - -test46 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (x <=? n) -> Proxy True -test46 _ _ = id - -test47 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (y <=? n) -> Proxy True -test47 _ _ = id - -test48 - :: Proxy n - -> Proxy (Max (1+n) 1) - -> Proxy (n+1) -test48 _ = id - -test49 - :: Proxy n - -> Proxy (Max (n+1) 1) - -> Proxy (1+n) -test49 _ = id - -test50 - :: Proxy n - -> Proxy (Max (n+2) 1) - -> Proxy (Max (2+n) 2) -test50 _ = id - -test51 - :: Proxy n - -> Proxy (Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1) - -> Proxy (2+((2^n)*2)) -test51 _ = id - -type family BitPack a :: Nat - -test52 - :: Proxy a - -> Proxy (1 + BitPack a) - -> Proxy (Max 0 (BitPack a) + CLog 2 2) -test52 _ = id - -test53 - :: Proxy n - -> Proxy (1 <=? Max (n + 1) 1) - -> Proxy True -test53 _ = id - -test54 - :: Proxy n - -> Proxy (n <=? Max (n + 1) 1) - -> Proxy True -test54 _ = id - -test55 - :: Proxy n - -> Proxy (n + 1 <=? Max (n + 1) 1) - -> Proxy True -test55 _ = id - -test56 - :: Proxy n - -> Proxy p - -> Proxy (n <=? Max (n + p) p) - -> Proxy True -test56 _ _ = id - -test57 - :: Proxy n - -> Proxy p - -> Proxy (n + 1 <=? Max (n + p + 1) p) - -> Proxy True -test57 _ _ = id - -test58a - :: 1 <= n - => Proxy n - -> Proxy n -test58a = id - -test58b - :: Proxy (Max (n+2) 1) - -> Proxy (Max (n+2) 1) -test58b = test58a - -main :: IO () -main = defaultMain tests - -tests :: TestTree -tests = testGroup "ghc-typelits-natnormalise" - [ testGroup "Basic functionality" - [ testCase "GCD 6 8 ~ 2" $ - show (test1 Proxy) @?= - "Proxy" - , testCase "forall x . GCD 6 8 + x ~ x + GCD 10 8" $ - show (test2 Proxy) @?= - "Proxy" - , testCase "CLog 3 10 ~ 3" $ - show (test3 Proxy) @?= - "Proxy" - , testCase "forall x . CLog 3 10 + x ~ x + CLog 2 7" $ - show (test4 Proxy) @?= - "Proxy" - , testCase "forall x>1 . CLog x (x^y) ~ y" $ - show (test5 Proxy) @?= - "Proxy" - , testCase "KnownNat (CLog 6 8) ~ 2" $ - show test6 @?= - "2" - , testCase "KnownNat (CLog 3 10) ~ 3" $ - show test7 @?= - "3" - , testCase "KnownNat ((CLog 2 4) * (3 ^ (CLog 2 4)))) ~ 18" $ - show test8 @?= - "18" - , testCase "KnownNat (Max (CLog 2 4) (CLog 4 20)) ~ 3" $ - show test9 @?= - "3" - , testCase "Div 9 3 ~ 3" $ - show (test10 Proxy) @?= - "Proxy" - , testCase "Div 9 4 ~ 2" $ - show (test11 Proxy) @?= - "Proxy" - , testCase "Mod 9 3 ~ 0" $ - show (test12 Proxy) @?= - "Proxy" - , testCase "Mod 9 4 ~ 1" $ - show (test13 Proxy) @?= - "Proxy" - , testCase "KnownNat (Div 9 3) ~ 3" $ - show test14 @?= - "3" - , testCase "KnownNat (Mod 9 4) ~ 1" $ - show test15 @?= - "1" - , testCase "LCM 18 7 ~ 126" $ - show (test16 Proxy) @?= - "Proxy" - , testCase "KnownNat (LCM 18 7) ~ 126" $ - show test17 @?= - "126" - , testCase "forall x . LCM 3 4 + x ~ x + LCM 6 4" $ - show (test18 Proxy) @?= - "Proxy" - , testCase "KnownNat (FLog 3 1) ~ 0" $ - show test19 @?= - "0" - , testCase "FLog 3 1 ~ 0" $ - show (test20 Proxy) @?= - "Proxy" - , testCase "KnownNat (CLog 3 1) ~ 0" $ - show test21 @?= - "0" - , testCase "CLog 3 1 ~ 0" $ - show (test22 Proxy) @?= - "Proxy" - , testCase "KnownNat (Log 3 1) ~ 0" $ - show test23 @?= - "0" - , testCase "KnownNat (Log 3 9) ~ 2" $ - show test24 @?= - "2" - , testCase "Log 3 9 ~ 2" $ - show (test25 Proxy) @?= - "Proxy" - , testCase "forall x>1 . x ^ (Log x y) ~ y" $ - show (test26 Proxy) @?= - "Proxy" - , testCase "forall x . Max x x ~ x" $ - show (test27 Proxy) @?= - "Proxy" - , testCase "forall x . Min x x ~ x" $ - show (test28 Proxy) @?= - "Proxy" - , testCase "forall x . (Max x x + 1) ~ (1 + x)" $ - show (test29 Proxy) @?= - "Proxy" - , testCase "forall x . (Min x x + 1) ~ (1 + Max x x)" $ - show (test30 Proxy Proxy) @?= - "Proxy" - , testCase "forall x . Min x (x+1) ~ x" $ - show (test31 Proxy) @?= - "Proxy" - , testCase "forall x . Min (x+1) x ~ x" $ - show (test32 Proxy) @?= - "Proxy" - , testCase "forall x . Max x (x+1) ~ (x+1)" $ - show (test33 Proxy) @?= - "Proxy" - , testCase "forall x . Max (x+1) x ~ (x+1)" $ - show (test34 Proxy) @?= - "Proxy" - , testCase "forall x . (1 + Max n (1+n)) ~ (2 + x)" $ - show (test35 Proxy Proxy) @?= - "Proxy" - , testCase "forall x . (1 + Min n (1+n)) ~ (1 + x)" $ - show (test36 Proxy Proxy) @?= - "Proxy" - , testCase "1 <= Div 18 3" $ - show (test37 (Proxy @18) (Proxy @3)) @?= - "()" - , testCase "Min (0-1) 0 ~ (0-1)" $ - show (test38 Proxy) @?= - "Proxy" - , testCase "Max (0-1) 0 ~ (0-1)" $ - show (test39 Proxy) @?= - "Proxy" - , testCase "forall x y . Max x y ~ Max y x" $ - show (test40 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y . Min x y ~ Min y x" $ - show (test41 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y . GCD x y ~ GCD y x" $ - show (test42 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y . LCM x y ~ LCM y x" $ - show (test43 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y . x <=? Max x y ~ True" $ - show (test44 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y . y <=? Max x y ~ True" $ - show (test45 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y n . n ~ Max x y => x <=? n ~ True" $ - show (test46 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall x y n . n ~ Max x y => y <=? n ~ True" $ - show (test47 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall n . Max (n+1) 1 ~ 1+n" $ - show (test48 Proxy Proxy) @?= - "Proxy" - , testCase "forall n . Max (1+n) 1 ~ n+1" $ - show (test49 Proxy Proxy) @?= - "Proxy" - , testCase "forall n . Max (n+2) 1 ~ Max (2+n) 2" $ - show (test50 Proxy Proxy) @?= - "Proxy" - , testCase "forall n . Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1 ~ 2 + ((2 ^ n) * 2)" $ - show (test51 Proxy Proxy) @?= - "Proxy" - , testCase "forall a . (1 + BitPack a) ~ (Max 0 (BitPack a) + CLog 2 2" $ - show (test52 Proxy Proxy) @?= - "Proxy" - , testCase "forall n . 1 <= Max (n + 1) 1" $ - show (test53 Proxy Proxy) @?= - "Proxy" - , testCase "forall n . n <= Max (n + 1) 1" $ - show (test54 Proxy Proxy) @?= - "Proxy" - , testCase "forall n . n + 1 <= Max (n + 1) 1" $ - show (test55 Proxy Proxy) @?= - "Proxy" - , testCase "forall n p . n <= Max (n + p) p" $ - show (test56 Proxy Proxy Proxy) @?= - "Proxy" - , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $ - show (test57 Proxy Proxy Proxy) @?= - "Proxy" - ] - , testGroup "errors" - [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors - , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors - , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors - , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors - , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors - , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors - , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors - , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors - , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors - , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors - , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors - , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors - , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors - , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors - , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors - , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors - , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors - , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors - , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors - , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors - , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors - , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors - , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors - , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors - , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors - , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors - , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors - ] - ] - --- | Assert that evaluation of the first argument (to WHNF) will throw --- an exception whose string representation contains the given --- substrings. -throws :: a -> [String] -> Assertion -throws v xs = do - result <- try (evaluate v) - case result of - Right _ -> assertFailure "No exception!" - Left (TypeError msg) -> - if all (`isInfixOf` (removeProblemChars msg)) $ map removeProblemChars xs - then return () - else assertFailure msg - --- The kind and amount of quotes in GHC error messages changes depending on --- whether or not our locale supports unicode. --- Remove the problematic characters to enable comparison of errors. -removeProblemChars = filter (`notElem` problemChars) - where problemChars = "‘’`'" +{-# LANGUAGE CPP, DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} +#if __GLASGOW_HASKELL__ >= 805 +{-# LANGUAGE NoStarIsType #-} +#endif +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} + +import Data.List (isInfixOf) +import Data.Proxy +import Data.Type.Bool +import Control.Exception +import Test.Tasty +import Test.Tasty.HUnit + +import ErrorTests + +import GHC.TypeLits +import GHC.TypeLits.Extra + +test1 :: Proxy (GCD 6 8) -> Proxy 2 +test1 = id + +test2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 10 8)) +test2 = id + +test3 :: Proxy (CLog 3 10) -> Proxy 3 +test3 = id + +test4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 7)) +test4 = id + +test5 :: Proxy (CLog x (x^y)) -> Proxy y +test5 = id + +test6 :: Integer +test6 = natVal (Proxy :: Proxy (CLog 6 8)) + +test7 :: Integer +test7 = natVal (Proxy :: Proxy (CLog 3 10)) + +test8 :: Integer +test8 = natVal (Proxy :: Proxy ((CLog 2 4) * (3 ^ (CLog 2 4)))) + +test9 :: Integer +test9 = natVal (Proxy :: Proxy (Max (CLog 2 4) (CLog 4 20))) + +test10 :: Proxy (Div 9 3) -> Proxy 3 +test10 = id + +test11 :: Proxy (Div 9 4) -> Proxy 2 +test11 = id + +test12 :: Proxy (Mod 9 3) -> Proxy 0 +test12 = id + +test13 :: Proxy (Mod 9 4) -> Proxy 1 +test13 = id + +test14 :: Integer +test14 = natVal (Proxy :: Proxy (Div 9 3)) + +test15 :: Integer +test15 = natVal (Proxy :: Proxy (Mod 9 4)) + +test16 :: Proxy (LCM 18 7) -> Proxy 126 +test16 = id + +test17 :: Integer +test17 = natVal (Proxy :: Proxy (LCM 18 7)) + +test18 :: Proxy ((LCM 6 4) + x) -> Proxy (x + (LCM 3 4)) +test18 = id + +test19 :: Integer +test19 = natVal (Proxy :: Proxy (FLog 3 1)) + +test20 :: Proxy (FLog 3 1) -> Proxy 0 +test20 = id + +test21 :: Integer +test21 = natVal (Proxy :: Proxy (CLog 3 1)) + +test22 :: Proxy (CLog 3 1) -> Proxy 0 +test22 = id + +test23 :: Integer +test23 = natVal (Proxy :: Proxy (Log 3 1)) + +test24 :: Integer +test24 = natVal (Proxy :: Proxy (Log 3 9)) + +test25 :: Proxy (Log 3 9) -> Proxy 2 +test25 = id + +test26 :: Proxy (b ^ (Log b y)) -> Proxy y +test26 = id + +test27 :: Proxy (Max n n) -> Proxy n +test27 = id + +test28 :: Proxy (Min n n) -> Proxy n +test28 = id + +test29 :: Proxy (Max n n + 1) -> Proxy (1 + n) +test29 = id + +test30 :: Proxy n -> Proxy (1 + Max n n) -> Proxy (Min n n + 1) +test30 _ = id + +test31 :: Proxy (Min n (n + 1)) -> Proxy n +test31 = id + +test32 :: Proxy (Min (n + 1) n) -> Proxy n +test32 = id + +test33 :: Proxy (Max n (n + 1)) -> Proxy (n+1) +test33 = id + +test34 :: Proxy (Max (n + 1) n) -> Proxy (n+1) +test34 = id + +test35 :: Proxy n -> Proxy (1 + Max n (1 + n)) -> Proxy (n + 2) +test35 _ = id + +test36 :: Proxy n -> Proxy (1 + Min n (1 + n)) -> Proxy (n + 1) +test36 _ = id + +test37 :: (1 <= Div l r) => Proxy l -> Proxy r -> () +test37 _ _ = () + +test38 :: Proxy (Min (0-1) 0) -> Proxy (0-1) +test38 = id + +test39 :: Proxy (Max (0-1) 0) -> Proxy (0-1) +test39 = id + +test40 :: Proxy x -> Proxy y -> Proxy (Max x y) -> Proxy (Max y x) +test40 _ _ = id + +test41 :: Proxy x -> Proxy y -> Proxy (Min x y) -> Proxy (Min y x) +test41 _ _ = id + +test42 :: Proxy x -> Proxy y -> Proxy (GCD x y) -> Proxy (GCD y x) +test42 _ _ = id + +test43 :: Proxy x -> Proxy y -> Proxy (LCM x y) -> Proxy (LCM y x) +test43 _ _ = id + +test44 :: Proxy x -> Proxy y -> Proxy (x <=? (Max x y)) -> Proxy True +test44 _ _ = id + +test45 :: Proxy x -> Proxy y -> Proxy (y <=? (Max x y)) -> Proxy True +test45 _ _ = id + +test46 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (x <=? n) -> Proxy True +test46 _ _ = id + +test47 :: n ~ (Max x y) => Proxy x -> Proxy y -> Proxy (y <=? n) -> Proxy True +test47 _ _ = id + +test48 + :: Proxy n + -> Proxy (Max (1+n) 1) + -> Proxy (n+1) +test48 _ = id + +test49 + :: Proxy n + -> Proxy (Max (n+1) 1) + -> Proxy (1+n) +test49 _ = id + +test50 + :: Proxy n + -> Proxy (Max (n+2) 1) + -> Proxy (Max (2+n) 2) +test50 _ = id + +test51 + :: Proxy n + -> Proxy (Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1) + -> Proxy (2+((2^n)*2)) +test51 _ = id + +type family BitPack a :: Nat + +test52 + :: Proxy a + -> Proxy (1 + BitPack a) + -> Proxy (Max 0 (BitPack a) + CLog 2 2) +test52 _ = id + +test53 + :: Proxy n + -> Proxy (1 <=? Max (n + 1) 1) + -> Proxy True +test53 _ = id + +test54 + :: Proxy n + -> Proxy (n <=? Max (n + 1) 1) + -> Proxy True +test54 _ = id + +test55 + :: Proxy n + -> Proxy (n + 1 <=? Max (n + 1) 1) + -> Proxy True +test55 _ = id + +test56 + :: Proxy n + -> Proxy p + -> Proxy (n <=? Max (n + p) p) + -> Proxy True +test56 _ _ = id + +test57 + :: Proxy n + -> Proxy p + -> Proxy (n + 1 <=? Max (n + p + 1) p) + -> Proxy True +test57 _ _ = id + +test58a + :: 1 <= n + => Proxy n + -> Proxy n +test58a = id + +test58b + :: Proxy (Max (n+2) 1) + -> Proxy (Max (n+2) 1) +test58b = test58a + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = testGroup "ghc-typelits-natnormalise" + [ testGroup "Basic functionality" + [ testCase "GCD 6 8 ~ 2" $ + show (test1 Proxy) @?= + "Proxy" + , testCase "forall x . GCD 6 8 + x ~ x + GCD 10 8" $ + show (test2 Proxy) @?= + "Proxy" + , testCase "CLog 3 10 ~ 3" $ + show (test3 Proxy) @?= + "Proxy" + , testCase "forall x . CLog 3 10 + x ~ x + CLog 2 7" $ + show (test4 Proxy) @?= + "Proxy" + , testCase "forall x>1 . CLog x (x^y) ~ y" $ + show (test5 Proxy) @?= + "Proxy" + , testCase "KnownNat (CLog 6 8) ~ 2" $ + show test6 @?= + "2" + , testCase "KnownNat (CLog 3 10) ~ 3" $ + show test7 @?= + "3" + , testCase "KnownNat ((CLog 2 4) * (3 ^ (CLog 2 4)))) ~ 18" $ + show test8 @?= + "18" + , testCase "KnownNat (Max (CLog 2 4) (CLog 4 20)) ~ 3" $ + show test9 @?= + "3" + , testCase "Div 9 3 ~ 3" $ + show (test10 Proxy) @?= + "Proxy" + , testCase "Div 9 4 ~ 2" $ + show (test11 Proxy) @?= + "Proxy" + , testCase "Mod 9 3 ~ 0" $ + show (test12 Proxy) @?= + "Proxy" + , testCase "Mod 9 4 ~ 1" $ + show (test13 Proxy) @?= + "Proxy" + , testCase "KnownNat (Div 9 3) ~ 3" $ + show test14 @?= + "3" + , testCase "KnownNat (Mod 9 4) ~ 1" $ + show test15 @?= + "1" + , testCase "LCM 18 7 ~ 126" $ + show (test16 Proxy) @?= + "Proxy" + , testCase "KnownNat (LCM 18 7) ~ 126" $ + show test17 @?= + "126" + , testCase "forall x . LCM 3 4 + x ~ x + LCM 6 4" $ + show (test18 Proxy) @?= + "Proxy" + , testCase "KnownNat (FLog 3 1) ~ 0" $ + show test19 @?= + "0" + , testCase "FLog 3 1 ~ 0" $ + show (test20 Proxy) @?= + "Proxy" + , testCase "KnownNat (CLog 3 1) ~ 0" $ + show test21 @?= + "0" + , testCase "CLog 3 1 ~ 0" $ + show (test22 Proxy) @?= + "Proxy" + , testCase "KnownNat (Log 3 1) ~ 0" $ + show test23 @?= + "0" + , testCase "KnownNat (Log 3 9) ~ 2" $ + show test24 @?= + "2" + , testCase "Log 3 9 ~ 2" $ + show (test25 Proxy) @?= + "Proxy" + , testCase "forall x>1 . x ^ (Log x y) ~ y" $ + show (test26 Proxy) @?= + "Proxy" + , testCase "forall x . Max x x ~ x" $ + show (test27 Proxy) @?= + "Proxy" + , testCase "forall x . Min x x ~ x" $ + show (test28 Proxy) @?= + "Proxy" + , testCase "forall x . (Max x x + 1) ~ (1 + x)" $ + show (test29 Proxy) @?= + "Proxy" + , testCase "forall x . (Min x x + 1) ~ (1 + Max x x)" $ + show (test30 Proxy Proxy) @?= + "Proxy" + , testCase "forall x . Min x (x+1) ~ x" $ + show (test31 Proxy) @?= + "Proxy" + , testCase "forall x . Min (x+1) x ~ x" $ + show (test32 Proxy) @?= + "Proxy" + , testCase "forall x . Max x (x+1) ~ (x+1)" $ + show (test33 Proxy) @?= + "Proxy" + , testCase "forall x . Max (x+1) x ~ (x+1)" $ + show (test34 Proxy) @?= + "Proxy" + , testCase "forall x . (1 + Max n (1+n)) ~ (2 + x)" $ + show (test35 Proxy Proxy) @?= + "Proxy" + , testCase "forall x . (1 + Min n (1+n)) ~ (1 + x)" $ + show (test36 Proxy Proxy) @?= + "Proxy" + , testCase "1 <= Div 18 3" $ + show (test37 (Proxy @18) (Proxy @3)) @?= + "()" + , testCase "Min (0-1) 0 ~ (0-1)" $ + show (test38 Proxy) @?= + "Proxy" + , testCase "Max (0-1) 0 ~ (0-1)" $ + show (test39 Proxy) @?= + "Proxy" + , testCase "forall x y . Max x y ~ Max y x" $ + show (test40 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . Min x y ~ Min y x" $ + show (test41 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . GCD x y ~ GCD y x" $ + show (test42 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . LCM x y ~ LCM y x" $ + show (test43 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . x <=? Max x y ~ True" $ + show (test44 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . y <=? Max x y ~ True" $ + show (test45 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y n . n ~ Max x y => x <=? n ~ True" $ + show (test46 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y n . n ~ Max x y => y <=? n ~ True" $ + show (test47 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall n . Max (n+1) 1 ~ 1+n" $ + show (test48 Proxy Proxy) @?= + "Proxy" + , testCase "forall n . Max (1+n) 1 ~ n+1" $ + show (test49 Proxy Proxy) @?= + "Proxy" + , testCase "forall n . Max (n+2) 1 ~ Max (2+n) 2" $ + show (test50 Proxy Proxy) @?= + "Proxy" + , testCase "forall n . Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1 ~ 2 + ((2 ^ n) * 2)" $ + show (test51 Proxy Proxy) @?= + "Proxy" + , testCase "forall a . (1 + BitPack a) ~ (Max 0 (BitPack a) + CLog 2 2" $ + show (test52 Proxy Proxy) @?= + "Proxy" + , testCase "forall n . 1 <= Max (n + 1) 1" $ + show (test53 Proxy Proxy) @?= + "Proxy" + , testCase "forall n . n <= Max (n + 1) 1" $ + show (test54 Proxy Proxy) @?= + "Proxy" + , testCase "forall n . n + 1 <= Max (n + 1) 1" $ + show (test55 Proxy Proxy) @?= + "Proxy" + , testCase "forall n p . n <= Max (n + p) p" $ + show (test56 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $ + show (test57 Proxy Proxy Proxy) @?= + "Proxy" + ] + , testGroup "errors" + [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors + , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail2 `throws` testFail2Errors + , testCase "CLog 3 10 /~ 2" $ testFail3 `throws` testFail3Errors + , testCase "CLog 3 10 + x /~ x + CLog 2 9" $ testFail4 `throws` testFail4Errors + , testCase "CLog 0 4 /~ 100" $ testFail5 `throws` testFail5Errors + , testCase "CLog 1 4 /~ 100" $ testFail5 `throws` testFail5Errors + , testCase "CLog 4 0 /~ 0" $ testFail7 `throws` testFail7Errors + , testCase "CLog 1 (1^y) /~ y" $ testFail8 `throws` testFail8Errors + , testCase "CLog 0 (0^y) /~ y" $ testFail9 `throws` testFail9Errors + , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors + , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors + , testCase "Div 4 0 /~ 4" $ testFail12 `throws` testFail12Errors + , testCase "Mod 4 0 /~ 4" $ testFail13 `throws` testFail13Errors + , testCase "FLog 0 4 /~ 100" $ testFail14 `throws` testFail14Errors + , testCase "FLog 1 4 /~ 100" $ testFail15 `throws` testFail15Errors + , testCase "FLog 4 0 /~ 0" $ testFail16 `throws` testFail16Errors + , testCase "GCD 6 8 /~ 4" $ testFail17 `throws` testFail17Errors + , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors + , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors + , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors + , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors + , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors + , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors + , testCase "(z <=? Max x y) /~ True" $ testFail24 `throws` testFail24Errors + , testCase "(x+1 <=? Max x y) /~ True" $ testFail25 `throws` testFail25Errors + , testCase "(x <= n) /=> (Max x y) ~ n" $ testFail26 `throws` testFail26Errors + , testCase "n + 2 <=? Max (n + 1) 1 /~ True" $ testFail27 `throws` testFail27Errors + ] + ] + +-- | Assert that evaluation of the first argument (to WHNF) will throw +-- an exception whose string representation contains the given +-- substrings. +throws :: a -> [String] -> Assertion +throws v xs = do + result <- try (evaluate v) + case result of + Right _ -> assertFailure "No exception!" + Left (TypeError msg) -> + if all (`isInfixOf` (removeProblemChars msg)) $ map removeProblemChars xs + then return () + else assertFailure msg + +-- The kind and amount of quotes in GHC error messages changes depending on +-- whether or not our locale supports unicode. +-- Remove the problematic characters to enable comparison of errors. +removeProblemChars = filter (`notElem` problemChars) + where problemChars = "‘’`'"