commit ghc-ghc-typelits-extra for openSUSE:Factory

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 - psimons@suse.com + +- Update to version 0.2.2 with cabal2obs. + +------------------------------------------------------------------- +Sat Oct 1 17:18:10 UTC 2016 - psimons@suse.com + +- Update to version 0.2.1 with cabal2obs. + +------------------------------------------------------------------- +Thu Sep 15 07:07:21 UTC 2016 - psimons@suse.com + +- 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.... +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.... -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.... +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....) + .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....) + .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.... 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.... 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.... 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.... 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.... 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: christiaan.baaij@gmail.com -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 -} -{-# 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 -} -{-# 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.... 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.... 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.... integerLogBase#> +-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.... 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/com... --- --- 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.... 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.... 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.... 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.... 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.... 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.... 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