packages feed

ghc-typelits-extra 0.5.1 → 0.5.2

raw patch · 9 files changed

+292/−98 lines, 9 filesdep ~ghc-typelits-natnormalisePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc-typelits-natnormalise

API changes (from Hackage documentation)

+ GHC.TypeLits.Extra: instance (GHC.TypeNats.KnownNat x, GHC.TypeNats.KnownNat y, GHC.TypeNats.KnownNat z, (2 Data.Type.Ord.<= x) GHC.Types.~ (() :: Constraint)) => GHC.TypeLits.KnownNat.KnownNat3 "GHC.TypeLits.Extra.CLogWZ" x y z

Files

CHANGELOG.md view
@@ -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
ghc-typelits-extra.cabal view
@@ -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/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>     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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>      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)
src/GHC/TypeLits/Extra.hs view
@@ -20,6 +20,8 @@   * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>     .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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>      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)
src/GHC/TypeLits/Extra/Solver.hs view
@@ -59,6 +59,8 @@ --     * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --       .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 <https://hackage.haskell.org/package/base-4.17.0.0/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> --        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)
src/GHC/TypeLits/Extra/Solver/Compat.hs view
@@ -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
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -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
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -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]
tests/ErrorTests.hs view
@@ -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
tests/Main.hs view
@@ -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"