Hello community,
here is the log from the commit of package ghc-ghc-typelits-extra for
openSUSE:Factory checked in at 2017-05-09 18:00:56
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/ghc-ghc-typelits-extra (Old)
and /work/SRC/openSUSE:Factory/.ghc-ghc-typelits-extra.new (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "ghc-ghc-typelits-extra"
Tue May 9 18:00:56 2017 rev:2 rq:453298 version:0.2.2
Changes:
--------
---
/work/SRC/openSUSE:Factory/ghc-ghc-typelits-extra/ghc-ghc-typelits-extra.changes
2016-11-01 09:53:16.000000000 +0100
+++
/work/SRC/openSUSE:Factory/.ghc-ghc-typelits-extra.new/ghc-ghc-typelits-extra.changes
2017-05-09 18:00:58.851283691 +0200
@@ -1,0 +2,15 @@
+Wed Jan 18 09:00:30 UTC 2017 - [email protected]
+
+- Update to version 0.2.2 with cabal2obs.
+
+-------------------------------------------------------------------
+Sat Oct 1 17:18:10 UTC 2016 - [email protected]
+
+- Update to version 0.2.1 with cabal2obs.
+
+-------------------------------------------------------------------
+Thu Sep 15 07:07:21 UTC 2016 - [email protected]
+
+- Update to version 0.2 revision 1 with cabal2obs.
+
+-------------------------------------------------------------------
Old:
----
ghc-typelits-extra-0.1.3.tar.gz
New:
----
ghc-typelits-extra-0.2.2.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ ghc-ghc-typelits-extra.spec ++++++
--- /var/tmp/diff_new_pack.oEzi7H/_old 2017-05-09 18:01:01.950845689 +0200
+++ /var/tmp/diff_new_pack.oEzi7H/_new 2017-05-09 18:01:01.954845123 +0200
@@ -1,7 +1,7 @@
#
# spec file for package ghc-ghc-typelits-extra
#
-# Copyright (c) 2016 SUSE LINUX GmbH, Nuernberg, Germany.
+# Copyright (c) 2017 SUSE LINUX GmbH, Nuernberg, Germany.
#
# All modifications and additions to the file contributed by third parties
# remain the property of their copyright owners, unless otherwise agreed
@@ -19,33 +19,61 @@
%global pkg_name ghc-typelits-extra
%bcond_with tests
Name: ghc-%{pkg_name}
-Version: 0.1.3
+Version: 0.2.2
Release: 0
Summary: Additional type-level operations on GHC.TypeLits.Nat
License: BSD-2-Clause
-Group: System/Libraries
+Group: Development/Languages/Other
Url: https://hackage.haskell.org/package/%{pkg_name}
Source0:
https://hackage.haskell.org/package/%{pkg_name}-%{version}/%{pkg_name}-%{version}.tar.gz
BuildRequires: ghc-Cabal-devel
BuildRequires: ghc-ghc-devel
BuildRequires: ghc-ghc-tcplugins-extra-devel
+BuildRequires: ghc-ghc-typelits-knownnat-devel
+BuildRequires: ghc-ghc-typelits-natnormalise-devel
BuildRequires: ghc-rpm-macros
+BuildRequires: ghc-singletons-devel
BuildRequires: ghc-transformers-devel
BuildRoot: %{_tmppath}/%{name}-%{version}-build
%if %{with tests}
-BuildRequires: ghc-ghc-typelits-natnormalise-devel
BuildRequires: ghc-tasty-devel
BuildRequires: ghc-tasty-hunit-devel
+BuildRequires: ghc-template-haskell-devel
%endif
%description
Additional type-level operations on 'GHC.TypeLits.Nat':
-* 'GHC.TypeLits.Extra.GCD': a type-level 'gcd'
+* '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>
-* 'GHC.TypeLits.Extra.CLog': type-level equivalent /the ceiling of/
+* '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#>
+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,
@@ -70,19 +98,15 @@
%prep
%setup -q -n %{pkg_name}-%{version}
-
%build
%ghc_lib_build
-
%install
%ghc_lib_install
-
%check
%cabal_test
-
%post devel
%ghc_pkg_recache
++++++ ghc-typelits-extra-0.1.3.tar.gz -> ghc-typelits-extra-0.2.2.tar.gz ++++++
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/CHANGELOG.md
new/ghc-typelits-extra-0.2.2/CHANGELOG.md
--- old/ghc-typelits-extra-0.1.3/CHANGELOG.md 2016-07-19 14:10:24.000000000
+0200
+++ new/ghc-typelits-extra-0.2.2/CHANGELOG.md 2017-01-15 19:02:16.000000000
+0100
@@ -1,5 +1,28 @@
# Changelog for the
[`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra)
package
+# 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
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/LICENSE
new/ghc-typelits-extra-0.2.2/LICENSE
--- old/ghc-typelits-extra-0.1.3/LICENSE 2016-07-19 14:10:24.000000000
+0200
+++ new/ghc-typelits-extra-0.2.2/LICENSE 2017-01-15 19:02:16.000000000
+0100
@@ -1,4 +1,5 @@
-Copyright (c) 2015-2016, University of Twente
+Copyright (c) 2015-2016, University of Twente,
+ 2017, QBayLogic
All rights reserved.
Redistribution and use in source and binary forms, with or without
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/README.md
new/ghc-typelits-extra-0.2.2/README.md
--- old/ghc-typelits-extra-0.1.3/README.md 2016-07-19 15:17:00.000000000
+0200
+++ new/ghc-typelits-extra-0.2.2/README.md 2017-01-15 19:02:16.000000000
+0100
@@ -1,11 +1,21 @@
# ghc-typelits-extra
-[](http://travis-ci.org/clash-lang/ghc-typelits-extra)
+[](http://travis-ci.org/clash-lang/ghc-typelits-extra)
[](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.GCD`: a type-level `gcd`
+* `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)
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/ghc-typelits-extra.cabal
new/ghc-typelits-extra-0.2.2/ghc-typelits-extra.cabal
--- old/ghc-typelits-extra-0.1.3/ghc-typelits-extra.cabal 2016-07-19
15:15:55.000000000 +0200
+++ new/ghc-typelits-extra-0.2.2/ghc-typelits-extra.cabal 2017-01-15
19:02:16.000000000 +0100
@@ -1,12 +1,29 @@
name: ghc-typelits-extra
-version: 0.1.3
+version: 0.2.2
synopsis: Additional type-level operations on GHC.TypeLits.Nat
description:
Additional type-level operations on @GHC.TypeLits.Nat@:
.
- * @GHC.TypeLits.Extra.GCD@: a type-level @gcd@
+ * @Max@: type-level
<http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max>
.
- * @GHC.TypeLits.Extra.CLog@: type-level equivalent /the ceiling of/
<https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-
integerLogBase#>
+ * @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,
@@ -23,7 +40,7 @@
license-file: LICENSE
author: Christiaan Baaij
maintainer: [email protected]
-copyright: Copyright © 2015-2016 University of Twente
+copyright: Copyright © 2015-2016, University of Twente, 2017,
QBayLogic
category: Type System
build-type: Simple
extra-source-files: README.md
@@ -45,17 +62,28 @@
GHC.TypeLits.Extra.Solver
other-modules: GHC.TypeLits.Extra.Solver.Unify
GHC.TypeLits.Extra.Solver.Operations
- build-depends: base >= 4.8 && <5,
- ghc >= 7.10 && <8.2,
- ghc-tcplugins-extra >= 0.2,
- integer-gmp >= 1.0 && <1.1,
- transformers >= 0.4.2.0 && < 0.6
+ build-depends: base >= 4.8 && <5,
+ ghc >= 7.10 && <8.2,
+ ghc-tcplugins-extra >= 0.2,
+ ghc-typelits-knownnat >= 0.2 && <0.3,
+ ghc-typelits-natnormalise >= 0.5 && <0.6,
+ integer-gmp >= 1.0 && <1.1,
+ singletons >= 2.2 && <3,
+ transformers >= 0.4.2.0 && <0.6
hs-source-dirs: src
default-language: Haskell2010
- other-extensions: CPP
- DataKinds
+ other-extensions: DataKinds
+ FlexibleInstances
+ GADTs
+ MagicHash
+ MultiParamTypeClasses
+ ScopedTypeVariables
+ TemplateHaskell
TupleSections
+ TypeApplications
TypeFamilies
+ TypeOperators
+ UndecidableInstances
if flag(deverror)
ghc-options: -Wall -Werror
else
@@ -67,14 +95,15 @@
Other-Modules: ErrorTests
build-depends: base >= 4.8 && <5,
ghc-typelits-extra >= 0.1.1,
+ ghc-typelits-knownnat >= 0.2,
ghc-typelits-natnormalise >= 0.4.1,
tasty >= 0.10,
- tasty-hunit >= 0.9
+ tasty-hunit >= 0.9,
+ template-haskell >= 2.11.0.0
hs-source-dirs: tests
default-language: Haskell2010
- other-extensions: CPP
- DataKinds
+ other-extensions: DataKinds
+ TemplateHaskell
TypeOperators
- ScopedTypeVariables
if flag(deverror)
ghc-options: -O0 -dcore-lint
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra/Solver/Operations.hs
new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra/Solver/Operations.hs
--- old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra/Solver/Operations.hs
2016-07-19 14:10:24.000000000 +0200
+++ new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra/Solver/Operations.hs
2017-01-15 19:02:16.000000000 +0100
@@ -4,47 +4,50 @@
Maintainer : Christiaan Baaij <[email protected]>
-}
-{-# LANGUAGE CPP, GeneralizedNewtypeDeriving, MagicHash #-}
-#if __GLASGOW_HASKELL__ < 711
-{-# LANGUAGE StandaloneDeriving #-}
-#endif
+{-# LANGUAGE MagicHash #-}
module GHC.TypeLits.Extra.Solver.Operations
( ExtraOp (..)
- , EType (..)
- , mergeGCD
+ , ExtraDefs (..)
+ , reifyEOP
+ , mergeMax
+ , mergeMin
+ , mergeDiv
+ , mergeMod
+ , mergeFLog
, mergeCLog
+ , mergeLog
+ , mergeGCD
+ , mergeLCM
, mergeExp
)
where
-- external
-import GHC.Base (isTrue#,(==#),(+#))
-import GHC.Integer (smallInteger)
-import GHC.Integer.Logarithms (integerLogBase#)
+import GHC.Base (isTrue#,(==#),(+#))
+import GHC.Integer (smallInteger)
+import GHC.Integer.Logarithms (integerLogBase#)
+import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural)
-- GHC API
import Outputable (Outputable (..), (<+>), integer, text)
-import Type (Type, TyVar)
-#if __GLASGOW_HASKELL__ >= 711
-import Type (eqType)
-#endif
-
-newtype EType = EType Type
- deriving Outputable
-#if __GLASGOW_HASKELL__ < 711
-deriving instance Eq EType
-#else
-instance Eq EType where
- (EType t1) == (EType t2) = eqType t1 t2
-#endif
+import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon)
+import TyCon (TyCon)
+import Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)
data ExtraOp
= I Integer
| V TyVar
- | C EType
- | GCD ExtraOp ExtraOp
+ | 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
@@ -52,30 +55,138 @@
ppr (I i) = integer i
ppr (V v) = ppr v
ppr (C c) = ppr c
- ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"
+ 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
+ }
+
+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 -> ExtraOp
+mergeMax defs x y =
+ let x' = reifyEOP defs x
+ y' = reifyEOP defs y
+ z = normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])
+ in case isNatural z of
+ Just True -> y
+ Just False -> x
+ _ -> Max x y
+
+mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp
+mergeMin defs x y =
+ let x' = reifyEOP defs x
+ y' = reifyEOP defs y
+ z = normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])
+ in case isNatural z of
+ Just True -> x
+ Just False -> y
+ _ -> Max x y
+
+mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeDiv _ (I 0) = Nothing
+mergeDiv (I i) (I j) = Just (I (div i j))
+mergeDiv x y = Just (Div x y)
+
+mergeMod :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeMod _ (I 0) = Nothing
+mergeMod (I i) (I j) = Just (I (mod i j))
+mergeMod x y = Just (Mod x y)
+
+mergeFLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeFLog (I i) _ | i < 2 = Nothing
+mergeFLog i (Exp j k) | i == j = Just k
+mergeFLog (I i) (I j) = I <$> flogBase i j
+mergeFLog x y = Just (FLog x y)
+
+mergeCLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeCLog (I i) _ | i < 2 = Nothing
+mergeCLog i (Exp j k) | i == j = Just k
+mergeCLog (I i) (I j) = I <$> clogBase i j
+mergeCLog x y = Just (CLog x y)
+
+mergeLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
+mergeLog (I i) _ | i < 2 = Nothing
+mergeLog b (Exp b' y) | b == b' = Just y
+mergeLog (I i) (I j) = I <$> exactLogBase i j
+mergeLog x y = Just (Log x y)
+
mergeGCD :: ExtraOp -> ExtraOp -> ExtraOp
mergeGCD (I i) (I j) = I (gcd i j)
mergeGCD x y = GCD x y
-mergeCLog :: ExtraOp -> ExtraOp -> Maybe ExtraOp
-mergeCLog i (Exp j k)
- | i == j && (i /= (I 0)) = Just k
-mergeCLog (I i) (I j) = I <$> clogBase i j
-mergeCLog x y = Just (CLog x y)
+mergeLCM :: ExtraOp -> ExtraOp -> ExtraOp
+mergeLCM (I i) (I j) = I (lcm i j)
+mergeLCM x y = GCD x y
mergeExp :: ExtraOp -> ExtraOp -> ExtraOp
-mergeExp (I i) (I j) = I (i^j)
-mergeExp x y = Exp x y
+mergeExp (I i) (I j) = I (i^j)
+mergeExp b (Log b' y) | b == b' = y
+mergeExp x y = Exp x y
+
+-- | \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 | x > 1 && y > 0 =
+clogBase x y | y > 0 =
let z1 = integerLogBase# x y
z2 = integerLogBase# x (y-1)
- in if (isTrue# (z1 ==# z2))
- then Just (smallInteger (z1 +# 1#))
- else Just (smallInteger z1)
+ in case y of
+ 1 -> Just 0
+ _ | isTrue# (z1 ==# z2) -> Just (smallInteger (z1 +# 1#))
+ | otherwise -> Just (smallInteger z1)
clogBase _ _ = Nothing
+
+-- | \x y -> logBase x y, x > 1 && y > 0, logBase x y == ceiling (logBase x y)
+exactLogBase :: Integer -> Integer -> Maybe Integer
+exactLogBase x y | y > 0 =
+ let z1 = integerLogBase# x y
+ z2 = integerLogBase# x (y-1)
+ in case y of
+ 1 -> Just 0
+ _ | isTrue# (z1 ==# z2) -> Nothing
+ | otherwise -> Just (smallInteger z1)
+exactLogBase _ _ = Nothing
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra/Solver/Unify.hs
new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra/Solver/Unify.hs
--- old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra/Solver/Unify.hs
2016-07-19 14:10:24.000000000 +0200
+++ new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra/Solver/Unify.hs
2017-01-15 19:02:16.000000000 +0100
@@ -4,8 +4,6 @@
Maintainer : Christiaan Baaij <[email protected]>
-}
-{-# LANGUAGE CPP #-}
-
module GHC.TypeLits.Extra.Solver.Unify
( ExtraDefs (..)
, UnifyResult (..)
@@ -15,42 +13,51 @@
where
-- external
-import Control.Monad.Trans.Class (lift)
-import Control.Monad.Trans.Maybe (MaybeT (..))
-import Data.Function (on)
+import Control.Monad.Trans.Class (lift)
+import Control.Monad.Trans.Maybe (MaybeT (..))
+import Data.Function (on)
+import GHC.TypeLits.Normalise.Unify (CType (..))
-- GHC API
import Outputable (Outputable (..), ($$), text)
import TcPluginM (TcPluginM, matchFam, tcPluginTrace)
import TcRnMonad (Ct)
import TcTypeNats (typeNatExpTyCon)
-import Type (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy)
-import TyCon (TyCon)
-#if __GLASGOW_HASKELL__ >= 711
+import Type (TyVar, coreView)
import TyCoRep (Type (..), TyLit (..))
-#else
-import TypeRep (Type (..), TyLit (..))
-#endif
import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
-- internal
import GHC.TypeLits.Extra.Solver.Operations
-data ExtraDefs = ExtraDefs
- { gcdTyCon :: TyCon
- , clogTyCon :: TyCon
- }
-
normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1
normaliseNat _ (TyVarTy v) = pure (V v)
normaliseNat _ (LitTy (NumTyLit i)) = pure (I i)
normaliseNat defs (TyConApp tc [x,y])
- | tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x
- <*> normaliseNat defs y
+ | tc == maxTyCon defs = mergeMax defs <$> normaliseNat defs x
+ <*> normaliseNat defs y
+ | tc == minTyCon defs = mergeMin defs <$> normaliseNat defs x
+ <*> normaliseNat defs y
+ | tc == divTyCon defs = do x' <- normaliseNat defs x
+ y' <- normaliseNat defs y
+ MaybeT (return (mergeDiv x' y'))
+ | tc == modTyCon defs = do x' <- normaliseNat defs x
+ y' <- normaliseNat defs y
+ MaybeT (return (mergeMod x' y'))
+ | tc == flogTyCon defs = do x' <- normaliseNat defs x
+ y' <- normaliseNat defs y
+ MaybeT (return (mergeFLog x' y'))
| tc == clogTyCon defs = do x' <- normaliseNat defs x
y' <- normaliseNat defs y
MaybeT (return (mergeCLog x' y'))
+ | tc == logTyCon defs = do x' <- normaliseNat defs x
+ y' <- normaliseNat defs y
+ MaybeT (return (mergeLog x' y'))
+ | tc == gcdTyCon defs = mergeGCD <$> normaliseNat defs x
+ <*> normaliseNat defs y
+ | tc == lcmTyCon defs = mergeLCM <$> normaliseNat defs x
+ <*> normaliseNat defs y
| tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x
<*> normaliseNat defs y
@@ -59,9 +66,9 @@
tyM <- lift (matchFam tc tys')
case tyM of
Just (_,ty) -> normaliseNat defs ty
- _ -> return (C (EType (TyConApp tc tys)))
+ _ -> return (C (CType (TyConApp tc tys)))
-normaliseNat _ t = return (C (EType t))
+normaliseNat _ t = return (C (CType t))
-- | Result of comparing two 'SOP' terms, returning a potential substitution
-- list under which the two terms are equal.
@@ -92,28 +99,31 @@
fvOP (I _) = emptyUniqSet
fvOP (V v) = unitUniqSet v
fvOP (C _) = emptyUniqSet
-fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y
+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
-reifyEOP :: ExtraDefs -> ExtraOp -> Type
-reifyEOP _ (I i) = mkNumLitTy i
-reifyEOP _ (V v) = mkTyVarTy v
-reifyEOP _ (C (EType c)) = c
-reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x
- ,reifyEOP defs y]
-reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x
- ,reifyEOP defs y]
-reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x
- ,reifyEOP defs y]
-
containsConstants :: ExtraOp -> Bool
containsConstants (I _) = False
containsConstants (V _) = False
containsConstants (C _) = True
-containsConstants (GCD x y) = containsConstants x || containsConstants y
+containsConstants (Max x y) = containsConstants x || containsConstants y
+containsConstants (Min x y) = containsConstants x || containsConstants y
+containsConstants (Div x y) = containsConstants x || containsConstants y
+containsConstants (Mod x y) = containsConstants x || containsConstants y
+containsConstants (FLog x y) = containsConstants x || containsConstants y
containsConstants (CLog x y) = containsConstants x || containsConstants y
+containsConstants (Log x y) = containsConstants x || containsConstants y
+containsConstants (GCD x y) = containsConstants x || containsConstants y
+containsConstants (LCM x y) = containsConstants x || containsConstants y
containsConstants (Exp x y) = containsConstants x || containsConstants y
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra/Solver.hs
new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra/Solver.hs
--- old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra/Solver.hs
2016-07-19 15:17:44.000000000 +0200
+++ new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra/Solver.hs
2017-01-15 19:02:16.000000000 +0100
@@ -13,15 +13,10 @@
-}
-{-# LANGUAGE CPP #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-#if __GLASGOW_HASKELL__ < 711
-{-# OPTIONS_GHC -fno-warn-deprecations #-}
-#endif
-
module GHC.TypeLits.Extra.Solver
( plugin )
where
@@ -32,28 +27,23 @@
import Data.Maybe (catMaybes)
import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName,
tracePlugin)
-#if __GLASGOW_HASKELL__ < 711
-import GHC.TcPluginM.Extra (failWithProvenace)
-#endif
-- GHC API
-import Class (Class, classMethods, className, classTyCon)
-import FamInst (tcInstNewTyCon_maybe)
import FastString (fsLit)
-import Id (idType)
import Module (mkModuleName)
import OccName (mkTcOcc)
import Outputable (Outputable (..), (<+>), ($$), text)
import Plugins (Plugin (..), defaultPlugin)
-import PrelNames (knownNatClassName)
-import TcEvidence (EvTerm (EvLit), EvLit (EvNum), mkEvCast, mkTcSymCo,
mkTcTransCo)
+import TcEvidence (EvTerm)
import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt)
import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,
isWanted)
import TcType (typeKind)
-import Type (EqRel (NomEq), Kind, PredTree (EqPred, ClassPred), Type,
classifyPredType,
- dropForAlls, eqType, funResultTy, tyConAppTyCon_maybe)
-import TysWiredIn (typeNatKind)
+import Type (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,
+ eqType)
+import TyCoRep (Type (..))
+import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)
+import TcTypeNats (typeNatLeqTyCon)
-- internal
import GHC.TypeLits.Extra.Solver.Operations
@@ -61,9 +51,22 @@
-- | A solver implement as a type-checker plugin for:
--
--- * @GHC.TypeLits.Extra.GCD@: a type-level 'gcd'
+-- * '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)@"
--
--- * @GHC.TypeLits.Extra.CLog@: type-level equivalent of /the ceiling of/
<https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35-
integerLogBase#>
+-- * '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
--
@@ -96,64 +99,75 @@
tcPluginTrace "normalised" (ppr sr)
case sr of
Simplified evs -> return (TcPluginOk (filter (isWanted . ctEvidence .
snd) evs) [])
-#if __GLASGOW_HASKELL__ >= 711
- Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])
-#else
- Impossible eq -> failWithProvenace (fromNatEquality eq)
-#endif
+ Impossible eq -> return (TcPluginContradiction [fromNatEquality eq])
-type NatEquality = (Ct,ExtraOp,ExtraOp)
-type KnConstraint = (Ct,Class,Type,ExtraOp)
+type NatEquality = (Ct,ExtraOp,ExtraOp)
+type NatInEquality = (Ct,ExtraOp,ExtraOp,Bool)
data SimplifyResult
= Simplified [(EvTerm,Ct)]
- | Impossible NatEquality
+ | Impossible (Either NatEquality NatInEquality)
instance Outputable SimplifyResult where
ppr (Simplified evs) = text "Simplified" $$ ppr evs
ppr (Impossible eq) = text "Impossible" <+> ppr eq
-simplifyExtra :: [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult
+simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult
simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs
where
- simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality KnConstraint] ->
TcPluginM SimplifyResult
+ simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] ->
TcPluginM SimplifyResult
simples evs [] = return (Simplified (catMaybes evs))
- simples evs (Left eq@((ct,u,v)):eqs') = do
+ simples evs (eq@(Left (ct,u,v)):eqs') = do
ur <- unifyExtra ct u v
tcPluginTrace "unifyExtra result" (ppr ur)
case ur of
Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'
Lose -> return (Impossible eq)
Draw -> simples evs eqs'
- simples evs (Right (ct,cls,ty,u):eqs') = do
- tcPluginTrace "unifyExtra KnownNat result" (ppr u)
- case u of
- (I i) -> simples (((,) <$> makeLitDict cls ty (EvNum i) <*> pure
ct):evs) eqs'
+ simples evs (eq@(Right (ct,u,v,b)):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)
eqs'
+ | otherwise -> return (Impossible eq)
_ -> simples evs eqs'
+
-- Extract the Nat equality constraints
-toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality
KnConstraint)
+toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality
NatInEquality)
toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
EqPred NomEq t1 t2
- | isNatKind (typeKind t1) || isNatKind (typeKind t1)
+ | isNatKind (typeKind t1) || isNatKind (typeKind t2)
-> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2)
- ClassPred cls [ty]
- | className cls == knownNatClassName
- -> Right <$> ((ct,cls,ty,) <$> normaliseNat defs ty)
+ | TyConApp tc [x,y] <- t1
+ , tc == typeNatLeqTyCon
+ , TyConApp tc' [] <- t2
+ -> if tc' == promotedTrueDataCon
+ then Right <$> ((ct,,,True) <$> normaliseNat defs x <*>
normaliseNat defs y)
+ else if tc' == promotedFalseDataCon
+ then Right <$> ((ct,,,False) <$> normaliseNat defs x <*>
normaliseNat defs y)
+ else fail "Nothing"
_ -> fail "Nothing"
where
isNatKind :: Kind -> Bool
isNatKind = (`eqType` typeNatKind)
-fromNatEquality :: NatEquality -> Ct
-fromNatEquality (ct, _, _) = ct
+fromNatEquality :: Either NatEquality NatInEquality -> Ct
+fromNatEquality (Left (ct, _, _)) = ct
+fromNatEquality (Right (ct,_,_,_)) = ct
lookupExtraDefs :: TcPluginM ExtraDefs
lookupExtraDefs = do
md <- lookupModule myModule myPackage
- gcdTc <- look md "GCD"
- clogTc <- look md "CLog"
- return $ ExtraDefs gcdTc clogTc
+ ExtraDefs <$> look md "Max"
+ <*> look md "Min"
+ <*> look md "Div"
+ <*> look md "Mod"
+ <*> look md "FLog"
+ <*> look md "CLog"
+ <*> look md "Log"
+ <*> look md "GCD"
+ <*> look md "LCM"
where
look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)
myModule = mkModuleName "GHC.TypeLits.Extra"
@@ -164,32 +178,3 @@
evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of
EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)
_ -> Nothing
-
-makeLitDict :: Class -> Type -> EvLit -> Maybe EvTerm
--- THIS CODE IS COPIED FROM:
---
https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973
---
--- makeLitDict adds a coercion that will convert the literal into a dictionary
--- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
--- in TcEvidence. The coercion happens in 2 steps:
---
--- Integer -> SNat n -- representation of literal to singleton
--- SNat n -> KnownNat n -- singleton to dictionary
---
--- The process is mirrored for Symbols:
--- String -> SSymbol n
--- SSymbol n -> KnownSymbol n -}
-makeLitDict clas ty evLit
- | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
- -- co_dict :: KnownNat n ~ SNat n
- , [ meth ] <- classMethods clas
- , Just tcRep <- tyConAppTyCon_maybe -- SNat
- $ funResultTy -- SNat n
- $ dropForAlls -- KnownNat n => SNat n
- $ idType meth -- forall n. KnownNat n => SNat n
- , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
- -- SNat n ~ Integer
- , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
- = Just ev_tm
- | otherwise
- = Nothing
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra.hs
new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra.hs
--- old/ghc-typelits-extra-0.1.3/src/GHC/TypeLits/Extra.hs 2016-07-19
15:14:59.000000000 +0200
+++ new/ghc-typelits-extra-0.2.2/src/GHC/TypeLits/Extra.hs 2017-01-15
19:02:16.000000000 +0100
@@ -5,9 +5,26 @@
Additional type-level operations on 'GHC.TypeLits.Nat':
- * 'GCD': a type-level 'gcd'
+ * '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,
@@ -20,27 +37,192 @@
pragma to the header of your file.
-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# 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 Safe #-}
+{-# LANGUAGE Trustworthy #-}
-module GHC.TypeLits.Extra where
+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.Singletons.TH (genDefunSymbols)
+import Data.Type.Bool (If)
+import GHC.Base (isTrue#,(==#),(+#))
+import GHC.Integer (smallInteger)
+import GHC.Integer.Logarithms (integerLogBase#)
+import GHC.TypeLits
+ (KnownNat, Nat, type (+), type (-), type (<=), type (<=?), natVal)
+import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol)
+
+-- | Type-level 'max'
+type family Max (x :: Nat) (y :: Nat) :: Nat where
+ Max 0 y = y
+ Max x 0 = x
+ Max n n = n
+ Max x y = If (x <=? y) y x
+
+genDefunSymbols [''Max]
+
+instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where
+ type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0
+ natSing2 = SNatKn (max (natVal (Proxy @x)) (natVal (Proxy @y)))
+
+-- | Type-level 'min'
+type family Min (x :: Nat) (y :: Nat) :: Nat where
+ Min 0 y = 0
+ Min x 0 = 0
+ Min n n = n
+ Min x y = If (x <=? y) x y
+
+genDefunSymbols [''Min]
+
+instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Min) x y where
+ type KnownNatF2 $(nameToSymbol ''Min) = MinSym0
+ natSing2 = SNatKn (min (natVal (Proxy @x)) (natVal (Proxy @y)))
-import GHC.TypeLits (Nat)
+-- | 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
--- | Type-level greatest common denominator (GCD).
+-- | A variant of 'Div' that rounds up instead of down
+type DivRU n d = Div (n + (d - 1)) d
+
+genDefunSymbols [''Div]
+
+instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x
y where
+ type KnownNatF2 $(nameToSymbol ''Div) = DivSym0
+ natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y)))
+
+-- | Type-level 'mod'
--
-- 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 -- Additional equations are provided by the custom solver
+type family Mod (x :: Nat) (y :: Nat) :: Nat where
+ Mod x 1 = 0
+
+genDefunSymbols [''Mod]
+
+instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x
y where
+ type KnownNatF2 $(nameToSymbol ''Mod) = ModSym0
+ natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))
+
+-- | 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
+
+genDefunSymbols [''FLog]
+
+instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol
''FLog) x y where
+ type KnownNatF2 $(nameToSymbol ''FLog) = FLogSym0
+ natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal
(Proxy @y))))
-- | 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
+
+genDefunSymbols [''CLog]
+
+instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol
''CLog) x y where
+ type KnownNatF2 $(nameToSymbol ''CLog) = CLogSym0
+ 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 (smallInteger (z1 +# 1#))
+ | otherwise -> SNatKn (smallInteger 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
+
+genDefunSymbols [''Log]
+
+instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2
$(nameToSymbol ''Log) x y where
+ type KnownNatF2 $(nameToSymbol ''Log) = LogSym0
+ natSing2 = SNatKn (smallInteger (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 -- Additional equations are provided by the custom solver
+
+genDefunSymbols [''GCD]
+
+instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''GCD) x y where
+ type KnownNatF2 $(nameToSymbol ''GCD) = GCDSym0
+ natSing2 = SNatKn (gcd (natVal (Proxy @x)) (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 -- Additional equations are provided by the custom solver
+
+genDefunSymbols [''LCM]
+
+instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''LCM) x y where
+ type KnownNatF2 $(nameToSymbol ''LCM) = LCMSym0
+ natSing2 = SNatKn (lcm (natVal (Proxy @x)) (natVal (Proxy @y)))
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/tests/ErrorTests.hs
new/ghc-typelits-extra-0.2.2/tests/ErrorTests.hs
--- old/ghc-typelits-extra-0.1.3/tests/ErrorTests.hs 2016-07-19
14:10:24.000000000 +0200
+++ new/ghc-typelits-extra-0.2.2/tests/ErrorTests.hs 2017-01-15
19:02:16.000000000 +0100
@@ -1,7 +1,8 @@
-{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE DataKinds, TypeOperators, TypeApplications, TypeFamilies,
TemplateHaskell #-}
{-# 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
@@ -10,6 +11,10 @@
import GHC.TypeLits
import GHC.TypeLits.Extra
+import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8)
+import Language.Haskell.TH (litE, stringL)
+import Language.Haskell.TH.Syntax (runIO)
+
testFail1 :: Proxy (GCD 6 8) -> Proxy 4
testFail1 = id
@@ -43,6 +48,46 @@
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)
+
+
testFail1Errors =
["Expected type: Proxy (GCD 6 8) -> Proxy 4"
,"Actual type: Proxy 4 -> Proxy 4"
@@ -89,7 +134,76 @@
]
testFail10Errors =
- ["No instance for (KnownNat (CLog 1 4))"]
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘'False’ with ‘'True’"
+ else litE $ stringL "Couldn't match type 'False with 'True"
+ )]
testFail11Errors =
- ["No instance for (KnownNat (CLog 4 4 - CLog 2 4))"]
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘CLog 2 4 <=? CLog 4 4’
with ‘'True’"
+ else litE $ stringL "Couldn't match type `CLog 2 4 <=? CLog 4 4'
with 'True"
+ )]
+
+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 =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"
+ else litE $ stringL "Couldn't match type `FLog 3 0' with `CLog 3 0'"
+ )]
+
+testFail20Errors =
+ [$(do localeEncoding <- runIO (getLocaleEncoding)
+ if textEncodingName localeEncoding == textEncodingName utf8
+ then litE $ stringL "Couldn't match type ‘FLog 3 10’ with ‘CLog 3
10’"
+ else litE $ stringL "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)"]
+
+testFail23Errors =
+ ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/ghc-typelits-extra-0.1.3/tests/Main.hs
new/ghc-typelits-extra-0.2.2/tests/Main.hs
--- old/ghc-typelits-extra-0.1.3/tests/Main.hs 2016-07-19 14:10:24.000000000
+0200
+++ new/ghc-typelits-extra-0.2.2/tests/Main.hs 2017-01-15 19:02:16.000000000
+0100
@@ -1,7 +1,7 @@
-{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables,
KindSignatures,
- TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
+{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}
import Data.List (isInfixOf)
@@ -40,13 +40,93 @@
test8 :: Integer
test8 = natVal (Proxy :: Proxy ((CLog 2 4) * (3 ^ (CLog 2 4))))
-type family Max (x :: Nat) (y :: Nat) :: Nat
- where
- Max x y = If (x <=? y) y x
-
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 _ _ = ()
+
main :: IO ()
main = defaultMain tests
@@ -66,7 +146,7 @@
show (test4 Proxy) @?=
"Proxy"
, testCase "forall x>1 . CLog x (x^y) ~ y" $
- show (test4 Proxy) @?=
+ show (test5 Proxy) @?=
"Proxy"
, testCase "KnownNat (CLog 6 8) ~ 2" $
show test6 @?=
@@ -80,19 +160,115 @@
, 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)) @?=
+ "()"
]
, 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 "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
]
]
@@ -104,11 +280,7 @@
result <- try (evaluate v)
case result of
Right _ -> assertFailure "No exception!"
-#if MIN_VERSION_base(4,9,0)
Left (TypeError msg) ->
-#else
- Left (ErrorCall msg) ->
-#endif
if all (`isInfixOf` msg) xs
then return ()
else assertFailure msg
