ghc-typelits-extra 0.1.3 → 0.2
raw patch · 9 files changed
+606/−172 lines, 9 filesdep +ghc-typelits-knownnatdep +singletonsdep ~ghc-typelits-natnormalise
Dependencies added: ghc-typelits-knownnat, singletons
Dependency ranges changed: ghc-typelits-natnormalise
Files
- CHANGELOG.md +12/−0
- README.md +11/−1
- ghc-typelits-extra.cabal +40/−13
- src/GHC/TypeLits/Extra.hs +177/−9
- src/GHC/TypeLits/Extra/Solver.hs +37/−70
- src/GHC/TypeLits/Extra/Solver/Operations.hs +80/−36
- src/GHC/TypeLits/Extra/Solver/Unify.hs +55/−21
- tests/ErrorTests.hs +71/−2
- tests/Main.hs +123/−20
CHANGELOG.md view
@@ -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
README.md view
@@ -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 <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ where the operation only reduces when "`floor (logBase b x) ~ ceiling (logBase b x)`"+* `GHC.TypeLits.Extra.GCD`: a type-level [gcd](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd)+* `GHC.TypeLits.Extra.LCM`: a type-level [lcm](http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm)
ghc-typelits-extra.cabal view
@@ -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 <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:max max> .- * @GHC.TypeLits.Extra.CLog@: type-level equivalent /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ * @Min@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:min min> .+ * @Div@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:div div>+ .+ * @Mod@: type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>+ .+ * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+ .+ * @CLog@: type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+ .+ * @Log@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"+ .+ * @GCD@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>+ .+ * @LCM@: a type-level <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:lcm lcm>+ . And a custom solver for the above operations defined in @GHC.TypeLits.Extra.Solver@ as a GHC type-checker plugin. To use the plugin, 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
src/GHC/TypeLits/Extra.hs view
@@ -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 <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+ * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" + * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+ where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"++ * 'GCD': a type-level 'gcd'++ * 'LCM': a type-level 'lcm'+ A custom solver for the above operations defined is defined in "GHC.TypeLits.Extra.Solver" as a GHC type-checker plugin. To use the plugin, 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 <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+--+-- Note that additional equations are provided by the type-checker plugin solver+-- "GHC.TypeLits.Extra.Solver".+type family FLog (x :: Nat) (y :: Nat) :: Nat where+ FLog 2 1 = 0 -- Additional equations are provided by the custom solver++genDefunSymbols [''FLog]++instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''FLog) x y where+ type KnownNatF2 $(nameToSymbol ''FLog) = FLogSym0+ natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y))))+ -- | Type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver". type family CLog (x :: Nat) (y :: Nat) :: Nat where CLog 2 1 = 0 -- Additional equations are provided by the custom solver++genDefunSymbols [''CLog]++instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''CLog) x y where+ type KnownNatF2 $(nameToSymbol ''CLog) = CLogSym0+ natSing2 = let x = natVal (Proxy @x)+ y = natVal (Proxy @y)+ z1 = integerLogBase# x y+ z2 = integerLogBase# x (y-1)+ in case y of+ 1 -> SNatKn 0+ _ | isTrue# (z1 ==# z2) -> SNatKn (smallInteger (z1 +# 1#))+ | otherwise -> SNatKn (smallInteger z1)++-- | Type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- where the operation only reduces when:+--+-- @+-- 'FLog' b x ~ 'CLog' b x+-- @+--+-- Additionally, the following property holds for 'Log':+--+-- > (b ^ (Log b x)) ~ x+--+-- Note that additional equations are provided by the type-checker plugin solver+-- "GHC.TypeLits.Extra.Solver".+type family Log (x :: Nat) (y :: Nat) :: Nat where+ Log 2 1 = 0 -- Additional equations are provided by the custom solver++genDefunSymbols [''Log]++instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where+ type KnownNatF2 $(nameToSymbol ''Log) = LogSym0+ natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y))))++-- | Type-level greatest common denominator (GCD).+--+-- Note that additional equations are provided by the type-checker plugin solver+-- "GHC.TypeLits.Extra.Solver".+type family GCD (x :: Nat) (y :: Nat) :: Nat where+ GCD 0 x = x -- Additional equations are provided by the custom solver++genDefunSymbols [''GCD]++instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''GCD) x y where+ type KnownNatF2 $(nameToSymbol ''GCD) = GCDSym0+ natSing2 = SNatKn (gcd (natVal (Proxy @x)) (natVal (Proxy @y)))++-- | Type-level least common multiple (LCM).+--+-- Note that additional equations are provided by the type-checker plugin solver+-- "GHC.TypeLits.Extra.Solver".+type family LCM (x :: Nat) (y :: Nat) :: Nat where+ LCM 0 x = 0 -- Additional equations are provided by the custom solver++genDefunSymbols [''LCM]++instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''LCM) x y where+ type KnownNatF2 $(nameToSymbol ''LCM) = LCMSym0+ natSing2 = SNatKn (lcm (natVal (Proxy @x)) (natVal (Proxy @y)))
src/GHC/TypeLits/Extra/Solver.hs view
@@ -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/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- * 'Min': type-level 'min' --+-- * 'Div': type-level 'div'+--+-- * 'Mod': type-level 'mod'+--+-- * 'FLog': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"+--+-- * 'CLog': type-level equivalent of /the ceiling of/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@"+--+-- * 'Log': type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>+-- where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@"+--+-- * 'GCD': a type-level 'gcd'+--+-- * 'LCM': a type-level 'lcm'+-- -- To use the plugin, add -- -- @@@ -96,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
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -4,47 +4,42 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# 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
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -4,8 +4,6 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} -{-# 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
tests/ErrorTests.hs view
@@ -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’"]
tests/Main.hs view
@@ -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