diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.5.2 *December 3rd 2025* +* Add `CLogWZ`, an extension of 'CLog', which returns the additional third argument in case the second argument is zero +* Add rewrite rules for `Min`, `Max`, `FLog`, `CLog`, and `Log` + # 0.5.1 *October 21st 2025* * Compatibility with `ghc-typelits-natnormalise` 0.9.1 release diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal --- a/ghc-typelits-extra.cabal +++ b/ghc-typelits-extra.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: ghc-typelits-extra -version: 0.5.1 +version: 0.5.2 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@: @@ -19,6 +19,8 @@ * @CLog@: type-level equivalent of /the ceiling of/ i.e. the exact integer equivalent to @ceiling (logBase x y)@ + * @CLogWZ@: extension of @CLog@, which returns the additional third argument in case the second argument is zero + * @Log@: type-level equivalent of where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@ @@ -74,7 +76,7 @@ ghc-prim >= 0.5 && <1.0, ghc-tcplugin-api >= 0.18.1.0 && <0.19, ghc-typelits-knownnat >= 0.7.2 && <0.9, - ghc-typelits-natnormalise >= 0.9 && <0.10, + ghc-typelits-natnormalise >= 0.9.3 && <0.10, transformers >= 0.4.2.0 && <0.7, template-haskell >= 2.15 && <2.25 if impl(ghc >= 9.0.0) 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 @@ -20,6 +20,8 @@ * 'CLog': type-level equivalent of /the ceiling of/ .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" + * 'CLogWZ': extension of 'CLog', which returns the additional third argument in case the second argument is zero + * 'Log': type-level equivalent of where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" @@ -70,6 +72,7 @@ -- ** Logarithm , FLog , CLog + , CLogWZ -- *** Exact logarithm , Log -- Numeric @@ -101,7 +104,8 @@ #if MIN_VERSION_ghc(8,4,0) import GHC.TypeLits (Div, Mod) #endif -import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol) +import GHC.TypeLits.KnownNat (KnownNat2 (..), KnownNat3 (..), + SNatKn (..), nameToSymbol) #if MIN_VERSION_ghc(8,2,0) intToNumber :: Int# -> Natural @@ -191,6 +195,27 @@ z1 = integerLogBase# x y z2 = integerLogBase# x (y-1) in case y of + 1 -> SNatKn 0 + _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) + | otherwise -> SNatKn (intToNumber z1) + +-- | Extended version of 'CLog', which is well-defined for the second, non-base argument being zero. The additional third argument argument is returned in this particular case. +type family CLogWZ (base :: Nat) (value :: Nat) (ifzero :: Nat) :: Nat where + CLogWZ _ 0 z = z + CLogWZ b v _ = CLog b v + +#if MIN_VERSION_ghc(9,4,0) +instance (KnownNat x, KnownNat y, KnownNat z, (2 <= x) ~ (() :: Constraint)) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where +#else +instance (KnownNat x, KnownNat y, KnownNat z, 2 <= x) => KnownNat3 $(nameToSymbol ''CLogWZ) x y z where +#endif + natSing3 = let x = natVal (Proxy @x) + y = natVal (Proxy @y) + z = natVal (Proxy @z) + z1 = integerLogBase# x y + z2 = integerLogBase# x (y-1) + in case y of + 0 -> SNatKn $ fromInteger z 1 -> SNatKn 0 _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) | otherwise -> SNatKn (intToNumber z1) 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 @@ -59,6 +59,8 @@ -- * 'CLog': type-level equivalent of /the ceiling of/ -- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" -- +-- * 'CLogWZ': extension of @CLog@, which returns the additional third argument in case the second argument is zero +-- -- * 'Log': type-level equivalent of -- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" -- @@ -90,18 +92,70 @@ extraRewrite :: ExtraDefs -> UniqFM TyCon TcPluginRewriter extraRewrite defs = listToUFM - [ (gcdTyCon defs, gcdRewrite) + [ (minTyCon defs, minRewrite) + , (maxTyCon defs, maxRewrite) + , (flogTyCon defs, flogRewrite) + , (clogTyCon defs, clogRewrite) + , (clogWZTyCon defs, clogWZRewrite) + , (logTyCon defs, logRewrite) + , (gcdTyCon defs, gcdRewrite) , (lcmTyCon defs, lcmRewrite) ] where - gcdRewrite _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ - TcPluginRewriteTo (reduce (gcdTyCon defs) args (LitTy (NumTyLit (i `gcd` j)))) [] + minRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + = pure $ rewriteTo (minTyCon defs) args $ min i j + minRewrite _ _ = pure TcPluginNoRewrite + + maxRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + = pure $ rewriteTo (maxTyCon defs) args $ max i j + maxRewrite _ _ = pure TcPluginNoRewrite + + flogRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + , i > 1 + , Just r <- flogBase i j + = pure $ rewriteTo (flogTyCon defs) args r + flogRewrite _ _ = pure TcPluginNoRewrite + + clogRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + , i > 1 + , Just r <- clogBase i j + = pure $ rewriteTo (clogTyCon defs) args r + clogRewrite _ _ = pure TcPluginNoRewrite + + clogWZRewrite _ args + | [_, LitTy (NumTyLit 0), z] <- args + = pure $ TcPluginRewriteTo (reduce (clogWZTyCon defs) args z) [] + clogWZRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j), _] <- args + , i > 1 + , Just r <- clogBase i j + = pure $ rewriteTo (clogWZTyCon defs) args r + clogWZRewrite _ _ = pure TcPluginNoRewrite + + logRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + , i > 1 + , Just r <- exactLogBase i j + = pure $ rewriteTo (logTyCon defs) args r + logRewrite _ _ = pure TcPluginNoRewrite + + gcdRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + = pure $ rewriteTo (gcdTyCon defs) args (i `gcd` j) gcdRewrite _ _ = pure TcPluginNoRewrite - lcmRewrite _ args@[LitTy (NumTyLit i), LitTy (NumTyLit j)] = pure $ - TcPluginRewriteTo (reduce (lcmTyCon defs) args (LitTy (NumTyLit (i `lcm` j)))) [] + lcmRewrite _ args + | [LitTy (NumTyLit i), LitTy (NumTyLit j)] <- args + = pure $ rewriteTo (lcmTyCon defs) args (i `lcm` j) lcmRewrite _ _ = pure TcPluginNoRewrite + rewriteTo tyCon args x = + TcPluginRewriteTo (reduce tyCon args (LitTy (NumTyLit x))) [] + reduce tc args res = Reduction co res where co = mkPluginUnivCo "ghc-typelits-extra" Nominal [] @@ -156,18 +210,34 @@ simples :: [Maybe (EvTerm, Ct)] -> [Ct] -> [SolverConstraint] -> TcPluginM 'Solve SimplifyResult simples evs news [] = return (Simplified (catMaybes evs) news) simples evs news (eq@(NatEquality ct u v norm):eqs') = do - ur <- unifyExtra ct u v - tcPluginTrace "unifyExtra result" (ppr ur) let evM = evMagic (ordTyCons defs) ct (depsFromNormalised norm) - case ur of - Win -> simples (fmap (,ct) evM:evs) news eqs' - Lose | null evs && null eqs' -> return (Impossible eq) - _ | Normalised {} <- norm - , isWantedCt ct -> do - newCt <- createWantedFromNormalised defs eq + -- transform: CLogWZ a b c ~ CLog a b + -- to: 1 <= b + -- which is equivalent by definition and try to solve that + -- along with the rest of the eqs' + wz = case (u, v) of + (CLogWZ a b _, CLog a' b') | a == a' && b == b' -> Just b + (CLog a' b', CLogWZ a b _) | a == a' && b == b' -> Just b + _ -> Nothing + case wz of + Just x -> do + let x' = reifyEOP defs x + one = reifyEOP defs (I 1) + ev <- newWanted (ctLoc ct) $ mkLEqNat (ordTyCons defs) one x' + let newCt = mkNonCanonical ev simples (fmap (,ct) evM:evs) (newCt:news) eqs' - Lose -> simples evs news eqs' - Draw -> simples evs news eqs' + Nothing -> do + ur <- unifyExtra ct u v + tcPluginTrace "unifyExtra result" (ppr ur) + case ur of + Win -> simples (fmap (,ct) evM:evs) news eqs' + Lose | null evs && null eqs' -> return (Impossible eq) + _ | Normalised {} <- norm + , isWantedCt ct -> do + newCt <- createWantedFromNormalised defs eq + simples (fmap (,ct) evM:evs) (newCt:news) eqs' + Lose -> simples evs news eqs' + Draw -> simples evs news eqs' simples evs news (eq@(NatInequality ct deps u v b norm):eqs') = do tcPluginTrace "unifyExtra leq result" (ppr (u,v,b)) let evM = evMagic (ordTyCons defs) ct (deps <> depsFromNormalised norm) diff --git a/src/GHC/TypeLits/Extra/Solver/Compat.hs b/src/GHC/TypeLits/Extra/Solver/Compat.hs --- a/src/GHC/TypeLits/Extra/Solver/Compat.hs +++ b/src/GHC/TypeLits/Extra/Solver/Compat.hs @@ -35,16 +35,17 @@ import qualified GHC.TypeLits.Extra data ExtraDefs = ExtraDefs - { maxTyCon :: TyCon - , minTyCon :: TyCon - , divTyCon :: TyCon - , modTyCon :: TyCon - , flogTyCon :: TyCon - , clogTyCon :: TyCon - , logTyCon :: TyCon - , gcdTyCon :: TyCon - , lcmTyCon :: TyCon - , ordTyCons :: LookedUpTyCons + { maxTyCon :: TyCon + , minTyCon :: TyCon + , divTyCon :: TyCon + , modTyCon :: TyCon + , flogTyCon :: TyCon + , clogTyCon :: TyCon + , clogWZTyCon :: TyCon + , logTyCon :: TyCon + , gcdTyCon :: TyCon + , lcmTyCon :: TyCon + , ordTyCons :: LookedUpTyCons } -- | Find the \"magic\" classes and instances in "GHC.TypeLits.KnownNat" @@ -56,6 +57,7 @@ <*> pure typeNatModTyCon <*> look ''GHC.TypeLits.Extra.FLog <*> look ''GHC.TypeLits.Extra.CLog + <*> look ''GHC.TypeLits.Extra.CLogWZ <*> look ''GHC.TypeLits.Extra.Log <*> look ''GHC.TypeLits.Extra.GCD <*> look ''GHC.TypeLits.Extra.LCM 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 @@ -7,6 +7,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE MagicHash #-} +{-# LANGUAGE LambdaCase #-} module GHC.TypeLits.Extra.Solver.Operations ( ExtraOp (..) @@ -21,10 +22,14 @@ , mergeMod , mergeFLog , mergeCLog + , mergeCLogWZ , mergeLog , mergeGCD , mergeLCM , mergeExp + , flogBase + , clogBase + , exactLogBase ) where @@ -71,19 +76,20 @@ type NormaliseResult = (ExtraOp, Normalised) data ExtraOp - = I Integer - | V TyVar - | C CType - | Max ExtraOp ExtraOp - | Min ExtraOp ExtraOp - | Div ExtraOp ExtraOp - | Mod ExtraOp ExtraOp - | FLog ExtraOp ExtraOp - | CLog ExtraOp ExtraOp - | Log ExtraOp ExtraOp - | GCD ExtraOp ExtraOp - | LCM ExtraOp ExtraOp - | Exp ExtraOp ExtraOp + = I Integer + | V TyVar + | C CType + | Max ExtraOp ExtraOp + | Min ExtraOp ExtraOp + | Div ExtraOp ExtraOp + | Mod ExtraOp ExtraOp + | FLog ExtraOp ExtraOp + | CLog ExtraOp ExtraOp + | CLogWZ ExtraOp ExtraOp ExtraOp + | Log ExtraOp ExtraOp + | GCD ExtraOp ExtraOp + | LCM ExtraOp ExtraOp + | Exp ExtraOp ExtraOp deriving Eq instance Outputable ExtraOp where @@ -100,31 +106,25 @@ 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 ")" + ppr (CLogWZ x y z) = text "CLogWZ " <+> text "(" <+> ppr x <+> text "," + <+> ppr y <+> text "," <+> ppr z <+> text ")" 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] +reifyEOP defs = \case + I i -> mkNumLitTy i + V v -> mkTyVarTy v + C (CType c) -> c + Max x y -> mkTyConApp (maxTyCon defs) $ reifyEOP defs <$> [x, y] + Min x y -> mkTyConApp (minTyCon defs) $ reifyEOP defs <$> [x, y] + Div x y -> mkTyConApp (divTyCon defs) $ reifyEOP defs <$> [x, y] + Mod x y -> mkTyConApp (modTyCon defs) $ reifyEOP defs <$> [x, y] + CLog x y -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y] + CLogWZ x y z -> mkTyConApp (clogTyCon defs) $ reifyEOP defs <$> [x, y, z] + FLog x y -> mkTyConApp (flogTyCon defs) $ reifyEOP defs <$> [x, y] + Log x y -> mkTyConApp (logTyCon defs) $ reifyEOP defs <$> [x, y] + GCD x y -> mkTyConApp (gcdTyCon defs) $ reifyEOP defs <$> [x, y] + LCM x y -> mkTyConApp (lcmTyCon defs) $ reifyEOP defs <$> [x, y] + Exp x y -> mkTyConApp typeNatExpTyCon $ reifyEOP defs <$> [x, y] mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult mergeMax _ (I 0) y = (y, Normalised []) @@ -179,6 +179,16 @@ mergeCLog i (Exp j k) | i == j = Just (k, Normalised []) mergeCLog (I i) (I j) = fmap (\r -> (I r, Normalised [])) (clogBase i j) mergeCLog x y = Just (CLog x y, Untouched) + +mergeCLogWZ :: ExtraOp -> ExtraOp -> ExtraOp -> Maybe NormaliseResult +mergeCLogWZ (I i) _ _ | i < 2 = Nothing +mergeCLogWZ _ (I 0) z = Just (z, Normalised []) +mergeCLogWZ i (Exp j k) _ | i == j = Just (k, Normalised []) +-- CLogWZ a b c = CLog a b for all b > 0 by definition, hence we can +-- elide one layer of constructor applications in this particular case +mergeCLogWZ x y@(I _) _ = do (res, _) <- mergeCLog x y + pure (res, Normalised []) +mergeCLogWZ x y z = Just (CLogWZ x y z, Untouched) mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult mergeLog (I i) _ | i < 2 = 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 @@ -6,6 +6,7 @@ -} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE LambdaCase #-} module GHC.TypeLits.Extra.Solver.Unify ( UnifyResult (..) @@ -55,6 +56,7 @@ go ty | Just ty1 <- coreView ty = go ty1 go (TyVarTy v) = pure (V v, Untouched) go (LitTy (NumTyLit i)) = pure (I i, Untouched) + go (TyConApp tc [x,y]) | tc == maxTyCon defs = mergeNormResWith (\x' y' -> return (mergeMax defs x' y')) @@ -97,6 +99,14 @@ (go x) (go y) + go (TyConApp tc [x,y,z]) + | tc == clogWZTyCon defs + = do (x', n1) <- normaliseNat defs x + (y', n2) <- normaliseNat defs y + (z', n3) <- normaliseNat defs z + (res, n4) <- MaybeT $ return $ mergeCLogWZ x' y' z' + pure (res, foldl mergeNormalised Untouched [n1,n2,n3,n4]) + go (TyConApp tc tys) = do let mergeExtraOp [] = [] mergeExtraOp ((Just (op, Normalised []), _):xs) = reifyEOP defs op:mergeExtraOp xs @@ -149,34 +159,37 @@ commuteResult _ _ = Draw fvOP :: ExtraOp -> UniqSet TyVar -fvOP (I _) = emptyUniqSet -fvOP (V v) = unitUniqSet v -fvOP (C _) = emptyUniqSet -fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y -fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y -fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y -fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y -fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y -fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y +fvOP (I _) = emptyUniqSet +fvOP (V v) = unitUniqSet v +fvOP (C _) = emptyUniqSet +fvOP (Max x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Min x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Div x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Mod x y) = fvOP x `unionUniqSets` fvOP y +fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y +fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y +fvOP (CLogWZ x y z) = fvOP x `unionUniqSets` fvOP y `unionUniqSets` fvOP z +fvOP (Log x y) = fvOP x `unionUniqSets` fvOP y +fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y +fvOP (LCM x y) = fvOP x `unionUniqSets` fvOP y +fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y eqFV :: ExtraOp -> ExtraOp -> Bool eqFV = (==) `on` fvOP containsConstants :: ExtraOp -> Bool -containsConstants (I _) = False -containsConstants (V _) = False -containsConstants (C _) = True -containsConstants (Max x y) = containsConstants x || containsConstants y -containsConstants (Min x y) = containsConstants x || containsConstants y -containsConstants (Div x y) = containsConstants x || containsConstants y -containsConstants (Mod x y) = containsConstants x || containsConstants y -containsConstants (FLog x y) = containsConstants x || containsConstants y -containsConstants (CLog x y) = containsConstants x || containsConstants y -containsConstants (Log x y) = containsConstants x || containsConstants y -containsConstants (GCD x y) = containsConstants x || containsConstants y -containsConstants (LCM x y) = containsConstants x || containsConstants y -containsConstants (Exp x y) = containsConstants x || containsConstants y +containsConstants = \case + I _ -> False + V _ -> False + C _ -> True + Max x y -> or $ containsConstants <$> [x, y] + Min x y -> or $ containsConstants <$> [x, y] + Div x y -> or $ containsConstants <$> [x, y] + Mod x y -> or $ containsConstants <$> [x, y] + FLog x y -> or $ containsConstants <$> [x, y] + CLog x y -> or $ containsConstants <$> [x, y] + CLogWZ x y z -> or $ containsConstants <$> [x, y, z] + Log x y -> or $ containsConstants <$> [x, y] + GCD x y -> or $ containsConstants <$> [x, y] + LCM x y -> or $ containsConstants <$> [x, y] + Exp x y -> or $ containsConstants <$> [x, y] diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -129,8 +129,12 @@ ] testFail4Errors = -#if __GLASGOW_HASKELL__ >= 900 +#if __GLASGOW_HASKELL__ >= 904 ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" + ,"Proxy (3 + x) -> Proxy (3 + x)" + ] +#elif __GLASGOW_HASKELL__ >= 900 + ["Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)" ,"Proxy (CLog 3 10 + x) -> Proxy (CLog 3 10 + x)" ] #else @@ -173,13 +177,9 @@ testFail11Errors = #if __GLASGOW_HASKELL__ >= 904 - ["Cannot satisfy: CLog 2 4 <= CLog 4 4"] -#elif __GLASGOW_HASKELL__ >= 902 - ["Couldn't match type ‘Data.Type.Ord.OrdCond" - ,"(CmpNat (CLog 2 4) (CLog 4 4)) 'True 'True 'False’" - ,"with ‘'True’"] + ["Cannot satisfy: 2 <= 1"] #else - ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"] + ["Couldn't match type ‘'False` with ‘'True’"] #endif testFail12Errors = @@ -236,7 +236,9 @@ #endif testFail20Errors = -#if __GLASGOW_HASKELL__ >= 900 +#if __GLASGOW_HASKELL__ >= 904 + ["Couldn't match type ‘2’ with ‘3’"] +#elif __GLASGOW_HASKELL__ >= 900 ["Couldn't match type: FLog 3 10" ," with: CLog 3 10"] #else diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -242,6 +242,39 @@ -> Proxy (Max (n+2) 1) test58b _ = test58a +test59 :: Proxy (CLogWZ 3 10 9) -> Proxy 3 +test59 = id + +test60 :: Proxy ((CLogWZ 3 10 3) + x) -> Proxy (x + (CLogWZ 2 7 8)) +test60 = id + +test61 :: Proxy (CLogWZ x (x^y) 8) -> Proxy y +test61 = id + +test62 :: Integer +test62 = natVal (Proxy :: Proxy (CLogWZ 6 8 3)) + +test63 :: Integer +test63 = natVal (Proxy :: Proxy (CLogWZ 3 10 9)) + +test64 :: Integer +test64 = natVal (Proxy :: Proxy ((CLogWZ 2 4 11) * (3 ^ (CLogWZ 2 4 8)))) + +test65 :: Integer +test65 = natVal (Proxy :: Proxy (Max (CLogWZ 2 4 8) (CLogWZ 4 20 5))) + +test66 :: Proxy (CLogWZ 3 0 8) -> Proxy 8 +test66 = id + +test67 :: Proxy (CLogWZ 2 0 x) -> Proxy x +test67 = id + +test68 :: Proxy (CLogWZ 5 0 0) -> Proxy 0 +test68 = id + +test69 :: 1 <= n => Proxy n -> Proxy (CLogWZ 2 n 0) -> Proxy (CLog 2 n) +test69 _ = id + main :: IO () main = defaultMain tests @@ -418,6 +451,39 @@ "Proxy" , testCase "forall n p . n + 1 <= Max (n + p + 1) p" $ show (test57 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "CLogWZ 3 10 9 ~ 3" $ + show (test59 Proxy) @?= + "Proxy" + , testCase "forall x . CLogWZ 3 10 3 + x ~ x + CLogWZ 2 7 8" $ + show (test60 Proxy) @?= + "Proxy" + , testCase "forall x>1 . CLogWZ x (x^y) 8 ~ y" $ + show (test61 Proxy) @?= + "Proxy" + , testCase "KnownNat (CLogWZ 6 8 3) ~ 2" $ + show test62 @?= + "2" + , testCase "KnownNat (CLogWZ 3 10 9) ~ 3" $ + show test63 @?= + "3" + , testCase "KnownNat ((CLogWZ 2 4 11) * (3 ^ (CLogWZ 2 4 8)))) ~ 18" $ + show test64 @?= + "18" + , testCase "KnownNat (Max (CLogWZ 2 4 8) (CLogWZ 4 20 5)) ~ 3" $ + show test65 @?= + "3" + , testCase "CLogWZ 3 0 8 ~ 8" $ + show (test66 Proxy) @?= + "Proxy" + , testCase "forall x. CLogWZ 2 0 x ~ x" $ + show (test67 Proxy) @?= + "Proxy" + , testCase "CLogWZ 5 0 0 ~ 0" $ + show (test68 Proxy) @?= + "Proxy" + , testCase "1 <= n => CLogWZ 2 n 0 ~ CLog 2 n" $ + show (test69 (Proxy :: Proxy 3) Proxy) @?= "Proxy" ] , testGroup "errors"