diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,17 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 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 --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -7,5 +7,15 @@ 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 + where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`" +* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd) +* `GHC.TypeLits.Extra.LCM`: a type-level [lcm](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm) diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal --- a/ghc-typelits-extra.cabal +++ b/ghc-typelits-extra.cabal @@ -1,13 +1,30 @@ name: ghc-typelits-extra -version: 0.1.3 +version: 0.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 . - * @GHC.TypeLits.Extra.CLog@: type-level equivalent /the ceiling of/ + * @Min@: type-level . + * @Div@: type-level + . + * @Mod@: type-level + . + * @FLog@: type-level equivalent of + .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" + . + * @CLog@: type-level equivalent of /the ceiling of/ + .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" + . + * @Log@: type-level equivalent of + where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" + . + * @GCD@: a type-level + . + * @LCM@: a type-level + . And a custom solver for the above operations defined in @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, add the @@ -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,13 @@ 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 hs-source-dirs: tests default-language: Haskell2010 - other-extensions: CPP - DataKinds + other-extensions: DataKinds TypeOperators - ScopedTypeVariables if flag(deverror) ghc-options: -O0 -dcore-lint diff --git a/src/GHC/TypeLits/Extra.hs b/src/GHC/TypeLits/Extra.hs --- a/src/GHC/TypeLits/Extra.hs +++ b/src/GHC/TypeLits/Extra.hs @@ -5,10 +5,27 @@ 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 + .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" + * 'CLog': type-level equivalent of /the ceiling of/ + .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" + * 'Log': type-level equivalent of + where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" + + * 'GCD': a type-level 'gcd' + + * 'LCM': a type-level 'lcm' + A custom solver for the above operations defined is defined in "GHC.TypeLits.Extra.Solver" as a GHC type-checker plugin. To use the plugin, add the @@ -20,27 +37,178 @@ 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 + -- ** Logarithm + , FLog + , CLog + -- *** Exact logarithm + , Log + -- Numeric + , GCD + , LCM + ) +where -import GHC.TypeLits (Nat) +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 (<=?), natVal) +import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol) --- | Type-level greatest common denominator (GCD). +-- | Type-level 'max' +type family Max (x :: Nat) (y :: Nat) :: Nat where + Max 0 y = y + 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 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))) + +-- | Type-level 'div' -- -- 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 Div (x :: Nat) (y :: Nat) :: Nat where + Div x 1 = x +genDefunSymbols [''Div] + +instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where + type KnownNatF2 $(nameToSymbol ''Div) = DivSym0 + natSing2 = SNatKn (div (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 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 (mod (natVal (Proxy @x)) (natVal (Proxy @y))) + +-- | Type-level equivalent of +-- .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/ +-- .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 +-- 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 --git a/src/GHC/TypeLits/Extra/Solver.hs b/src/GHC/TypeLits/Extra/Solver.hs --- a/src/GHC/TypeLits/Extra/Solver.hs +++ b/src/GHC/TypeLits/Extra/Solver.hs @@ -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,27 +27,20 @@ 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 Type (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType, + eqType) import TysWiredIn (typeNatKind) -- internal @@ -61,10 +49,27 @@ -- | A solver implement as a type-checker plugin for: -- --- * @GHC.TypeLits.Extra.GCD@: a type-level 'gcd' +-- * 'Max': type-level 'max' -- --- * @GHC.TypeLits.Extra.CLog@: type-level equivalent of /the ceiling of/ +-- * 'Min': type-level 'min' -- +-- * 'Div': type-level 'div' +-- +-- * 'Mod': type-level 'mod' +-- +-- * 'FLog': type-level equivalent of +-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" +-- +-- * 'CLog': type-level equivalent of /the ceiling of/ +-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" +-- +-- * 'Log': type-level equivalent of +-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" +-- +-- * 'GCD': a type-level 'gcd' +-- +-- * 'LCM': a type-level 'lcm' +-- -- To use the plugin, add -- -- @ @@ -96,14 +101,9 @@ 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) data SimplifyResult = Simplified [(EvTerm,Ct)] @@ -113,33 +113,25 @@ ppr (Simplified evs) = text "Simplified" $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq -simplifyExtra :: [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult +simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs where - simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult + simples :: [Maybe (EvTerm, Ct)] -> [NatEquality] -> TcPluginM SimplifyResult simples evs [] = return (Simplified (catMaybes evs)) - simples evs (Left eq@((ct,u,v)):eqs') = do + simples evs (eq@((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 eqs' -- Extract the Nat equality constraints -toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality KnConstraint) +toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM NatEquality toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 - | isNatKind (typeKind t1) || isNatKind (typeKind t1) - -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2) - ClassPred cls [ty] - | className cls == knownNatClassName - -> Right <$> ((ct,cls,ty,) <$> normaliseNat defs ty) + | isNatKind (typeKind t1) || isNatKind (typeKind t2) + -> (ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2 _ -> fail "Nothing" where isNatKind :: Kind -> Bool @@ -151,9 +143,13 @@ lookupExtraDefs :: TcPluginM ExtraDefs lookupExtraDefs = do md <- lookupModule myModule myPackage - gcdTc <- look md "GCD" - clogTc <- look md "CLog" - return $ ExtraDefs gcdTc clogTc + ExtraDefs <$> 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 +160,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 --git a/src/GHC/TypeLits/Extra/Solver/Operations.hs b/src/GHC/TypeLits/Extra/Solver/Operations.hs --- a/src/GHC/TypeLits/Extra/Solver/Operations.hs +++ b/src/GHC/TypeLits/Extra/Solver/Operations.hs @@ -4,47 +4,42 @@ 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 + , 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 (..)) -- 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 Type (TyVar) data ExtraOp = I Integer | V TyVar - | C EType - | GCD ExtraOp ExtraOp + | C CType + | 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 +47,79 @@ 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 (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 ")" +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 --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs --- a/src/GHC/TypeLits/Extra/Solver/Unify.hs +++ b/src/GHC/TypeLits/Extra/Solver/Unify.hs @@ -4,8 +4,6 @@ Maintainer : Christiaan Baaij -} -{-# LANGUAGE CPP #-} - module GHC.TypeLits.Extra.Solver.Unify ( ExtraDefs (..) , UnifyResult (..) @@ -15,9 +13,10 @@ 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) @@ -26,19 +25,20 @@ import TcTypeNats (typeNatExpTyCon) import Type (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy) import TyCon (TyCon) -#if __GLASGOW_HASKELL__ >= 711 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 + { divTyCon :: TyCon + , modTyCon :: TyCon + , flogTyCon :: TyCon , clogTyCon :: TyCon + , logTyCon :: TyCon + , gcdTyCon :: TyCon + , lcmTyCon :: TyCon } normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp @@ -46,11 +46,25 @@ 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 == 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 +73,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,8 +106,13 @@ fvOP (I _) = emptyUniqSet fvOP (V v) = unitUniqSet v fvOP (C _) = emptyUniqSet -fvOP (GCD 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 @@ -102,18 +121,33 @@ 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 _ (C (CType c)) = c +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 (Exp x y) = mkTyConApp typeNatExpTyCon [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] containsConstants :: ExtraOp -> Bool containsConstants (I _) = False containsConstants (V _) = False containsConstants (C _) = True -containsConstants (GCD x y) = containsConstants x || containsConstants y +containsConstants (Div x y) = containsConstants x || containsConstants y +containsConstants (Mod x y) = containsConstants x || containsConstants y +containsConstants (FLog x y) = containsConstants x || containsConstants y containsConstants (CLog x y) = containsConstants x || containsConstants y +containsConstants (Log x y) = containsConstants x || containsConstants y +containsConstants (GCD x y) = containsConstants x || containsConstants y +containsConstants (LCM x y) = containsConstants x || containsConstants y containsConstants (Exp x y) = containsConstants x || containsConstants y diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -2,6 +2,7 @@ {-# 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 @@ -43,6 +44,33 @@ 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)) + testFail1Errors = ["Expected type: Proxy (GCD 6 8) -> Proxy 4" ,"Actual type: Proxy 4 -> Proxy 4" @@ -89,7 +117,48 @@ ] testFail10Errors = - ["No instance for (KnownNat (CLog 1 4))"] + ["Couldn't match type ‘'False’ with ‘'True’"] testFail11Errors = - ["No instance for (KnownNat (CLog 4 4 - CLog 2 4))"] + ["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 = + ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"] + +testFail20Errors = + ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"] diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,7 +1,7 @@ -{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables, KindSignatures, - TypeFamilies, UndecidableInstances #-} +{-# LANGUAGE DataKinds, TypeOperators #-} {-# 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,60 @@ 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 + main :: IO () main = defaultMain tests @@ -66,7 +113,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 +127,79 @@ , 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" ] , 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 ] ] @@ -104,11 +211,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