ghc-typelits-extra 0.4.3 → 0.4.4
raw patch · 15 files changed
+2641/−2066 lines, 15 filesdep ~ghcdep ~ghc-bignumsetup-changedPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: ghc, ghc-bignum
API changes (from Hackage documentation)
- GHC.TypeLits.Extra: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, 2 GHC.TypeNats.<= x, 1 GHC.TypeNats.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.CLog" x y
- GHC.TypeLits.Extra: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, 2 GHC.TypeNats.<= x, 1 GHC.TypeNats.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.FLog" x y
- GHC.TypeLits.Extra.Solver: instance Outputable.Outputable GHC.TypeLits.Extra.Solver.SimplifyResult
- GHC.TypeLits.Extra.Solver: instance Outputable.Outputable GHC.TypeLits.Extra.Solver.SolverConstraint
+ GHC.TypeLits.Extra: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, 2 Data.Type.Ord.<= x, 1 Data.Type.Ord.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.CLog" x y
+ GHC.TypeLits.Extra: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, 2 Data.Type.Ord.<= x, 1 Data.Type.Ord.<= y) => GHC.TypeLits.KnownNat.KnownNat2 "GHC.TypeLits.Extra.FLog" x y
+ GHC.TypeLits.Extra.Solver: instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Extra.Solver.SimplifyResult
+ GHC.TypeLits.Extra.Solver: instance GHC.Utils.Outputable.Outputable GHC.TypeLits.Extra.Solver.SolverConstraint
Files
- CHANGELOG.md +91/−88
- LICENSE +27/−27
- README.md +21/−21
- Setup.hs +2/−2
- ghc-typelits-extra.cabal +124/−115
- src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +326/−0
- src-pre-ghc-9.4/GHC/TypeLits/Extra/Solver.hs +347/−0
- src/GHC/TypeLits/Extra.hs +253/−246
- src/GHC/TypeLits/Extra/Solver.hs +0/−345
- src/GHC/TypeLits/Extra/Solver/Operations.hs +242/−241
- src/GHC/TypeLits/Extra/Solver/Unify.hs +182/−182
- tests-ghc-9.4/ErrorTests.hs +227/−0
- tests-pre-ghc-9.4/ErrorTests.hs +347/−0
- tests/ErrorTests.hs +0/−347
- tests/Main.hs +452/−452
CHANGELOG.md view
@@ -1,88 +1,91 @@-# Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package--# 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.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/integer-gmp/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/integer-gmp/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/integer-gmp/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/integer-gmp/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/integer-gmp/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/integer-gmp/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,115 +1,124 @@-name: ghc-typelits-extra-version: 0.4.3-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/integer-gmp/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/integer-gmp/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/integer-gmp/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.4, GHC == 9.0.1, GHC == 9.2.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.7,- ghc >= 7.10 && <9.4,- 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.6- if impl(ghc >= 9.0.0)- build-depends: ghc-bignum >=1.0 && <1.1- else- build-depends: integer-gmp >=1.0 && <1.1- hs-source-dirs: src- 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- default-language: Haskell2010- other-extensions: DataKinds- TypeOperators- if flag(deverror)- ghc-options: -O0 -dcore-lint+name: ghc-typelits-extra +version: 0.4.4 +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/integer-gmp/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/integer-gmp/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/integer-gmp/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.4, + GHC == 9.4.2 + + +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.7, + ghc >= 7.10 && <9.6, + 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.6 + 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.6) + hs-source-dirs: src-ghc-9.4 + 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.6) + hs-source-dirs: tests-ghc-9.4 + default-language: Haskell2010 + other-extensions: DataKinds + TypeOperators + if flag(deverror) + ghc-options: -dcore-lint
+ src-ghc-9.4/GHC/TypeLits/Extra/Solver.hs view
@@ -0,0 +1,326 @@+{-| +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 #-} + +{-# 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) + +-- GHC API +import GHC.Builtin.Names (eqPrimTyConKey, hasKey) +import GHC.Builtin.Types (promotedTrueDataCon, promotedFalseDataCon) +import GHC.Builtin.Types (boolTy, naturalTy, cTupleDataCon, cTupleTyCon) +import GHC.Builtin.Types.Literals (typeNatTyCons) +import GHC.Builtin.Types.Literals (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, 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(..), TcPluginSolveResult (..), TcPluginRewriter, TcPluginRewriteResult (..)) +import GHC.Tc.Types.Constraint + (Ct, ctEvidence, ctEvPred, ctLoc, isWantedCt, cc_ev) +import GHC.Tc.Types.Constraint (Ct (CQuantCan), qci_ev) +import GHC.Tc.Types.Evidence (EvTerm, EvBindsVar, Role(..), evCast, evId) +import GHC.Types.Name.Occurrence (mkTcOcc) +import GHC.Types.Unique.FM (UniqFM, listToUFM) +import GHC.Unit.Module (mkModuleName) +import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) + +-- internal +import GHC.TypeLits.Extra.Solver.Operations +import GHC.TypeLits.Extra.Solver.Unify + +-- | 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/integer-gmp/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/integer-gmp/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/integer-gmp/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]) + _ -> fail "Nothing" + ev <- newWanted (ctLoc ct) newPredTy + let ctN = case ct of + CQuantCan qc -> CQuantCan (qc { qci_ev = ev}) + 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 + md1 <- lookupModule ordModule basePackage + md2 <- lookupModule typeErrModule basePackage + ExtraDefs <$> look md "Max" + <*> look md "Min" + <*> pure (typeNatTyCons !! 5) + <*> pure (typeNatTyCons !! 6) + <*> look md "FLog" + <*> look md "CLog" + <*> look md "Log" + <*> look md "GCD" + <*> look md "LCM" + <*> look md1 "OrdCond" + <*> look md2 "Assert" + where + look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s) + myModule = mkModuleName "GHC.TypeLits.Extra" + myPackage = fsLit "ghc-typelits-extra" + ordModule = mkModuleName "Data.Type.Ord" + basePackage = fsLit "base" + typeErrModule = mkModuleName "GHC.TypeError" + +-- 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
@@ -0,0 +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 (typeNatTyCons) +#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 (typeNatTyCons) +#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/integer-gmp/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/integer-gmp/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/integer-gmp/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 (typeNatTyCons !! 5) + <*> pure (typeNatTyCons !! 6) +#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,246 +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/integer-gmp/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/integer-gmp/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/integer-gmp/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#,(==#),(+#))-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 (x :: Nat) (y :: 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/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"------ Note that additional equations are provided by the type-checker plugin solver--- "GHC.TypeLits.Extra.Solver".-type family FLog (x :: Nat) (y :: 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/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"------ Note that additional equations are provided by the type-checker plugin solver--- "GHC.TypeLits.Extra.Solver".-type family CLog (x :: Nat) (y :: Nat) :: Nat where- CLog 2 1 = 0 -- Additional equations are provided by the custom solver--instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where- 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/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>--- where the operation only reduces when:------ @--- 'FLog' b x ~ 'CLog' b x--- @------ Additionally, the following property holds for 'Log':------ > (b ^ (Log b x)) ~ x------ Note that additional equations are provided by the type-checker plugin solver--- "GHC.TypeLits.Extra.Solver".-type family Log (x :: Nat) (y :: 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/integer-gmp/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/integer-gmp/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/integer-gmp/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 (x :: Nat) (y :: 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/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> +-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family FLog (x :: Nat) (y :: 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/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> +-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family CLog (x :: Nat) (y :: 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/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> +-- where the operation only reduces when: +-- +-- @ +-- 'FLog' b x ~ 'CLog' b x +-- @ +-- +-- Additionally, the following property holds for 'Log': +-- +-- > (b ^ (Log b x)) ~ x +-- +-- Note that additional equations are provided by the type-checker plugin solver +-- "GHC.TypeLits.Extra.Solver". +type family Log (x :: Nat) (y :: 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.hs
@@ -1,345 +0,0 @@-{-|-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 (typeNatTyCons)-#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 (typeNatTyCons)-#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, 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/integer-gmp/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/integer-gmp/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/integer-gmp/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 (typeNatTyCons !! 5)- <*> pure (typeNatTyCons !! 6)-#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"-#else- <*> 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/Solver/Operations.hs view
@@ -1,241 +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- }--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
@@ -0,0 +1,227 @@+{-# 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 = + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat z (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] + +testFail25Errors = + ["Couldn't match type ‘Data.Type.Ord.OrdCond" + ,"(CmpNat (x + 1) (Max x y)) 'True 'True 'False’" + ,"with ‘'True’"] + +testFail26Errors = + ["Could not deduce (Max x y ~ n)" + ,"from the context: (x <=? n) ~ 'True" + ]
+ tests-pre-ghc-9.4/ErrorTests.hs view
@@ -0,0 +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" + ]
− tests/ErrorTests.hs
@@ -1,347 +0,0 @@-{-# 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,452 +1,452 @@-{-# 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--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 + +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 = "‘’`'"