diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,12 @@ # 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` diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal --- a/ghc-typelits-extra.cabal +++ b/ghc-typelits-extra.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-extra -version: 0.2.1 +version: 0.2.2 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@: @@ -40,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 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 @@ -62,6 +62,9 @@ -- ** Integral , Div , Mod + , DivMod + -- *** Variants + , DivRU -- ** Logarithm , FLog , CLog @@ -79,7 +82,8 @@ 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, Nat, type (+), type (-), type (<=), type (<=?), natVal) import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol) -- | Type-level 'max' @@ -115,6 +119,9 @@ type family Div (x :: Nat) (y :: Nat) :: Nat where Div x 1 = x +-- | 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 @@ -133,6 +140,9 @@ 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 -- .i.e. the exact integer equivalent to "@'floor' ('logBase' x 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 @@ -41,7 +41,9 @@ import TcType (typeKind) import Type (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType, eqType) -import TysWiredIn (typeNatKind) +import TyCoRep (Type (..)) +import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon) +import TcTypeNats (typeNatLeqTyCon) -- internal import GHC.TypeLits.Extra.Solver.Operations @@ -99,47 +101,67 @@ Simplified evs -> return (TcPluginOk (filter (isWanted . ctEvidence . snd) evs) []) Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) -type NatEquality = (Ct,ExtraOp,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 :: [NatEquality] -> TcPluginM SimplifyResult +simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs where - simples :: [Maybe (EvTerm, Ct)] -> [NatEquality] -> TcPluginM SimplifyResult + simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult simples evs [] = return (Simplified (catMaybes evs)) - simples evs (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 (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 NatEquality +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 t2) - -> (ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2 + -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2) + | 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 - ExtraDefs <$> look md "Div" + ExtraDefs <$> look md "Max" + <*> look md "Min" + <*> look md "Div" <*> look md "Mod" <*> look md "FLog" <*> look md "CLog" 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 @@ -8,6 +8,10 @@ module GHC.TypeLits.Extra.Solver.Operations ( ExtraOp (..) + , ExtraDefs (..) + , reifyEOP + , mergeMax + , mergeMin , mergeDiv , mergeMod , mergeFLog @@ -23,16 +27,20 @@ import GHC.Base (isTrue#,(==#),(+#)) import GHC.Integer (smallInteger) import GHC.Integer.Logarithms (integerLogBase#) -import GHC.TypeLits.Normalise.Unify (CType (..)) +import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural) -- GHC API import Outputable (Outputable (..), (<+>), integer, text) -import Type (TyVar) +import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon) +import TyCon (TyCon) +import Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy) data ExtraOp = I Integer | V TyVar | C CType + | Max ExtraOp ExtraOp + | Min ExtraOp ExtraOp | Div ExtraOp ExtraOp | Mod ExtraOp ExtraOp | FLog ExtraOp ExtraOp @@ -47,6 +55,8 @@ ppr (I i) = integer i ppr (V v) = ppr v ppr (C c) = ppr c + ppr (Max x y) = text "Max (" <+> ppr x <+> text "," <+> ppr y <+> text ")" + ppr (Min x y) = text "Min (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (Div x y) = text "Div (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (Mod x y) = text "Mod (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (FLog x y) = text "FLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")" @@ -55,6 +65,63 @@ 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 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 @@ -23,29 +23,22 @@ import TcPluginM (TcPluginM, matchFam, tcPluginTrace) import TcRnMonad (Ct) import TcTypeNats (typeNatExpTyCon) -import Type (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy) -import TyCon (TyCon) +import Type (TyVar, coreView) import TyCoRep (Type (..), TyLit (..)) import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) -- internal import GHC.TypeLits.Extra.Solver.Operations -data ExtraDefs = ExtraDefs - { divTyCon :: TyCon - , modTyCon :: TyCon - , flogTyCon :: TyCon - , clogTyCon :: TyCon - , logTyCon :: TyCon - , gcdTyCon :: TyCon - , lcmTyCon :: 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 == 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')) @@ -106,6 +99,8 @@ fvOP (I _) = emptyUniqSet fvOP (V v) = unitUniqSet v fvOP (C _) = emptyUniqSet +fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y @@ -118,32 +113,12 @@ eqFV :: ExtraOp -> ExtraOp -> Bool eqFV = (==) `on` fvOP -reifyEOP :: ExtraDefs -> ExtraOp -> Type -reifyEOP _ (I i) = mkNumLitTy i -reifyEOP _ (V v) = mkTyVarTy v -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 (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 (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 diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds, TypeOperators, TemplateHaskell #-} +{-# LANGUAGE DataKinds, TypeOperators, TypeApplications, TypeFamilies, TemplateHaskell #-} {-# OPTIONS_GHC -fdefer-type-errors #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -75,6 +75,19 @@ 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" @@ -182,3 +195,15 @@ 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 --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds, TypeOperators #-} +{-# LANGUAGE DataKinds, TypeOperators, TypeApplications, TypeFamilies #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} @@ -106,6 +106,27 @@ 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 @@ -202,6 +223,27 @@ , 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 @@ -224,6 +266,9 @@ , 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 ] ]