ghc-typelits-extra 0.4.7 → 0.4.8
raw patch · 14 files changed
+3068/−2704 lines, 14 filesdep ~ghcdep ~template-haskellsetup-changedPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc, template-haskell
API changes (from Hackage documentation)
Files
- CHANGELOG.md +105/−102
- LICENSE +27/−27
- README.md +21/−21
- Setup.hs +2/−2
- ghc-typelits-extra.cabal +129/−125
- src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs +349/−0
- src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +348/−348
- src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +347/−347
- src/GHC/TypeLits/Extra.hs +253/−253
- src/GHC/TypeLits/Extra/Solver/Operations.hs +242/−242
- src/GHC/TypeLits/Extra/Solver/Unify.hs +182/−182
- tests-ghc-9.4/ErrorTests.hs +253/−245
- tests-pre-ghc-9.4/ErrorTests.hs +347/−347
- tests/Main.hs +463/−463
CHANGELOG.md view
@@ -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
LICENSE view
@@ -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.
README.md view
@@ -1,21 +1,21 @@-# ghc-typelits-extra - -[](https://github.com/clash-lang/ghc-typelits-extra/actions) -[](https://hackage.haskell.org/package/ghc-typelits-extra) -[](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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`" -* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](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++[](https://github.com/clash-lang/ghc-typelits-extra/actions)+[](https://hackage.haskell.org/package/ghc-typelits-extra)+[](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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`"+* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](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)
Setup.hs view
@@ -1,2 +1,2 @@-import Distribution.Simple -main = defaultMain +import Distribution.Simple+main = defaultMain
ghc-typelits-extra.cabal view
@@ -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 <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max> - . - * @Min@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min min> - . - * @Div@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div div> - . - * @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod> - . - * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - i.e. the exact integer equivalent to @floor (logBase x y)@ - . - * @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - i.e. the exact integer equivalent to @ceiling (logBase x y)@ - . - * @Log@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@ - . - * @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd> - . - * @LCM@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm lcm> - . - 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 <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max>+ .+ * @Min@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min min>+ .+ * @Div@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div div>+ .+ * @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>+ .+ * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ i.e. the exact integer equivalent to @floor (logBase x y)@+ .+ * @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ i.e. the exact integer equivalent to @ceiling (logBase x y)@+ .+ * @Log@: type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@+ .+ * @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>+ .+ * @LCM@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm lcm>+ .+ 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
+ src-ghc-9.12/GHC/TypeLits/Extra/Solver.hs view
@@ -0,0 +1,349 @@+{-|+Copyright : (C) 2015-2016, University of Twente+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+--+-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- 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
src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs view
@@ -1,348 +1,348 @@-{-| -Copyright : (C) 2015-2016, University of Twente -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> - -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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" --- --- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" --- --- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- 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 <christiaan.baaij@gmail.com>++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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+--+-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- 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
src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs view
@@ -1,347 +1,347 @@-{-| -Copyright : (C) 2015-2016, University of Twente -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> - -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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" --- --- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" --- --- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- 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 <christiaan.baaij@gmail.com>++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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+--+-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- 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
src/GHC/TypeLits/Extra.hs view
@@ -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 <christiaan.baaij@gmail.com> - -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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" - - * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" - - * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> - 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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- .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/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- .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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --- 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 <christiaan.baaij@gmail.com>++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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"++ * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"++ * 'Log': type-level equivalent of <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ 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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .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/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- 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)))
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -1,242 +1,242 @@-{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> --} - -{-# 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 <christiaan.baaij@gmail.com>+-}++{-# 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
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -1,182 +1,182 @@-{-| -Copyright : (C) 2015-2016, University of Twente, - 2017 , QBayLogic B.V. -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> --} - -{-# 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 <christiaan.baaij@gmail.com>+-}++{-# 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
tests-ghc-9.4/ErrorTests.hs view
@@ -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
tests-pre-ghc-9.4/ErrorTests.hs view
@@ -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"+ ]
tests/Main.hs view
@@ -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 = "‘’`'"