ghc-typelits-extra (empty) → 0.1
raw patch · 11 files changed
+627/−0 lines, 11 filesdep +basedep +ghcdep +ghc-tcplugins-extrasetup-changed
Dependencies added: base, ghc, ghc-tcplugins-extra, ghc-typelits-extra, ghc-typelits-natnormalise, tasty, tasty-hunit
Files
- CHANGELOG.md +4/−0
- LICENSE +26/−0
- README.md +11/−0
- Setup.hs +2/−0
- ghc-typelits-extra.cabal +71/−0
- src/GHC/TypeLits/Extra.hs +50/−0
- src/GHC/TypeLits/Extra/Solver.hs +151/−0
- src/GHC/TypeLits/Extra/Solver/Operations.hs +37/−0
- src/GHC/TypeLits/Extra/Solver/Unify.hs +119/−0
- tests/ErrorTests.hs +83/−0
- tests/Main.hs +73/−0
+ CHANGELOG.md view
@@ -0,0 +1,4 @@+# Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package++## 0.1 *October 21st 2015*+* Initial release
+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) 2015, Christiaan Baaij+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the+ distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,11 @@+# ghc-typelits-extra++[](http://travis-ci.org/clash-lang/ghc-typelits-extra)+[](https://hackage.haskell.org/package/ghc-typelits-extra)+[](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-extra)++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.CLog`: type-level equivalent of `clog x y = ceiling (logBase x y)`
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ghc-typelits-extra.cabal view
@@ -0,0 +1,71 @@+name: ghc-typelits-extra+version: 0.1+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@+ .+ * @GHC.TypeLits.Extra.CLog@: type-level equivalent of+ "@clog x y = ceiling (logBase x y)@"+ .+ 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+ .+ @+ OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver+ @+ .+ pragma to the header of your file.+homepage: http://www.clash-lang.org/+bug-reports: http://github.com/clash-lang/ghc-typelits-extra/issues+license: BSD2+license-file: LICENSE+author: Christiaan Baaij+maintainer: christiaan.baaij@gmail.com+copyright: Copyright © 2015 University of Twente+category: Type System+build-type: Simple+extra-source-files: README.md+ CHANGELOG.md+cabal-version: >=1.10++source-repository head+ type: git+ location: https://github.com/clash-lang/ghc-typelits-extra.git++flag deverror+ description:+ Enables `-Werror` for development mode and TravisCI+ default: False+ manual: True++library+ exposed-modules: GHC.TypeLits.Extra,+ GHC.TypeLits.Extra.Solver+ other-modules: GHC.TypeLits.Extra.Solver.Unify+ GHC.TypeLits.Extra.Solver.Operations+ build-depends: base >= 4.8 && <4.9,+ ghc >= 7.10 && <7.12,+ ghc-tcplugins-extra >= 0.1+ hs-source-dirs: src+ default-language: Haskell2010+ if flag(deverror)+ ghc-options: -Wall -Werror+ else+ ghc-options: -Wall++test-suite test-ghc-typelits-extra+ type: exitcode-stdio-1.0+ main-is: Main.hs+ Other-Modules: ErrorTests+ build-depends: base >= 4.8 && <4.9,+ ghc-typelits-extra >= 0.1,+ ghc-typelits-natnormalise >= 0.3,+ tasty >= 0.10,+ tasty-hunit >= 0.9+ hs-source-dirs: tests+ default-language: Haskell2010+ if flag(deverror)+ ghc-options: -O0 -dcore-lint
+ src/GHC/TypeLits/Extra.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeFamilies #-}++{-# OPTIONS_HADDOCK show-extensions #-}++{-# LANGUAGE Safe #-}++{-|+Copyright : (C) 2015, University of Twente+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++Additional type-level operations on 'GHC.TypeLits.Nat':++ * 'GCD': a type-level 'gcd'++ * 'CLog': type-level equivalent of+ \"@clog x y = 'ceiling' ('logBase' x y)@\"++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++@+{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}+@++pragma to the header of your file.+-}+module GHC.TypeLits.Extra where++import GHC.TypeLits (Nat)++-- | 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++-- | Type-level equivalent of:+--+-- @+-- clog x y = '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
+ src/GHC/TypeLits/Extra/Solver.hs view
@@ -0,0 +1,151 @@+{-# LANGUAGE TupleSections #-}++{-# OPTIONS_HADDOCK show-extensions #-}++{-|+Copyright : (C) 2015, Christiaan Baaij+License : BSD2 (see the file LICENSE)+Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com>++-}+module GHC.TypeLits.Extra.Solver+ ( plugin )+where++-- external+import Data.Maybe (catMaybes, mapMaybe)+import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, lookupModule,+ lookupName, newGiven, newWantedWithProvenance,+ tracePlugin)++-- GHC API+import FastString (fsLit)+import Module (mkModuleName)+import OccName (mkTcOcc)+import Outputable (Outputable (..), (<+>), ($$), text)+import Plugins (Plugin (..), defaultPlugin)+import TcEvidence (EvTerm)+import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt)+import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence,+ ctEvPred, ctLoc, isGiven, isWanted, mkNonCanonical)+import TcType (mkEqPred, typeKind)+import Type (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,+ mkTyVarTy)+import TysWiredIn (typeNatKind)++-- internal+import GHC.TypeLits.Extra.Solver.Operations+import GHC.TypeLits.Extra.Solver.Unify++-- | A solver implement as a type-checker plugin for:+--+-- * @GHC.TypeLits.Extra.GCD@: a type-level 'gcd'+--+-- * @GHC.TypeLits.Extra.CLog@: type-level equivalent of+-- \"@clog x y = 'ceiling' ('logBase' x y)@\"+--+-- To use the plugin, add+--+-- @+-- {\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}+-- @+--+-- To the header of your file.+plugin :: Plugin+plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }++normalisePlugin :: TcPlugin+normalisePlugin = tracePlugin "ghc-typelits-extra"+ TcPlugin { tcPluginInit = lookupExtraDefs+ , tcPluginSolve = decideEqualSOP+ , tcPluginStop = const (return ())+ }++decideEqualSOP :: ExtraDefs -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult+decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] [])+decideEqualSOP defs givens _deriveds wanteds = do+ -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out+ let wanteds' = filter (isWanted . ctEvidence) wanteds+ let unit_wanteds = mapMaybe (toNatEquality defs) wanteds'+ case unit_wanteds of+ [] -> return (TcPluginOk [] [])+ _ -> do+ unit_givens <- mapMaybe (toNatEquality defs) <$> mapM zonkCt givens+ sr <- simplifyExtra (unit_givens ++ unit_wanteds)+ tcPluginTrace "normalised" (ppr sr)+ case sr of+ Simplified subst evs ->+ TcPluginOk (filter (isWanted . ctEvidence . snd) evs) <$>+ mapM (substItemToCt defs) (filter (isWanted . ctEvidence . siNote) subst)+ Impossible eq -> failWithProvenace $ fromNatEquality eq++substItemToCt :: ExtraDefs -> SubstItem -> TcPluginM Ct+substItemToCt defs si+ | isGiven (ctEvidence ct) = mkNonCanonical <$> newGiven loc predicate evTm+ | otherwise = mkNonCanonical <$> newWantedWithProvenance+ (ctEvidence ct) predicate+ where+ predicate = mkEqPred ty1 ty2+ ty1 = mkTyVarTy (siVar si)+ ty2 = reifyExtraOp defs (siOP si)+ ct = siNote si+ loc = ctLoc ct+ evTm = evByFiat "ghc-typelits-extra" ty1 ty2++type NatEquality = (Ct,ExtraOp,ExtraOp)++data SimplifyResult+ = Simplified ExtraSubst [(EvTerm,Ct)]+ | Impossible NatEquality++instance Outputable SimplifyResult where+ ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs+ ppr (Impossible eq) = text "Impossible" <+> ppr eq++simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult+simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] [] eqs+ where+ simples :: ExtraSubst -> [Maybe (EvTerm, Ct)] -> [NatEquality]+ -> [NatEquality] -> TcPluginM SimplifyResult+ simples subst evs _xs [] = return (Simplified subst (catMaybes evs))+ simples subst evs xs (eq@(ct,u,v):eqs') = do+ ur <- unifyExtra ct (substsExtra subst u) (substsExtra subst v)+ tcPluginTrace "unifyExtra result" (ppr ur)+ case ur of+ Win -> simples subst (((,) <$> evMagic ct <*> pure ct):evs) []+ (xs ++ eqs')+ Lose -> return (Impossible eq)+ Draw [] -> simples subst evs (eq:xs) eqs'+ Draw subst' -> simples (substsSubst subst' subst ++ subst') evs [eq]+ (xs ++ eqs')++-- Extract the Nat equality constraints+toNatEquality :: ExtraDefs -> Ct -> Maybe NatEquality+toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2+ | isNatKind (typeKind t1) || isNatKind (typeKind t1)+ -> (ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2+ _ -> Nothing+ where+ isNatKind :: Kind -> Bool+ isNatKind = (== typeNatKind)++fromNatEquality :: NatEquality -> Ct+fromNatEquality (ct, _, _) = ct++lookupExtraDefs :: TcPluginM ExtraDefs+lookupExtraDefs = do+ md <- lookupModule myModule myPackage+ gcdTc <- look md "GCD"+ clogTc <- look md "CLog"+ return $ ExtraDefs gcdTc clogTc+ where+ look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)+ myModule = mkModuleName "GHC.TypeLits.Extra"+ myPackage = fsLit "ghc-typelits-extra"++-- Utils+evMagic :: Ct -> Maybe EvTerm+evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+ EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)+ _ -> Nothing
+ src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -0,0 +1,37 @@+module GHC.TypeLits.Extra.Solver.Operations where++-- GHC API+import Outputable (Outputable (..), (<+>), integer, text)+import Type (TyVar)++data ExtraOp+ = I Integer+ | V TyVar+ | GCD ExtraOp ExtraOp+ | CLog ExtraOp ExtraOp+ | Exp ExtraOp ExtraOp+ deriving Eq++instance Outputable ExtraOp where+ ppr (I i) = integer i+ ppr (V v) = ppr v+ ppr (GCD x y) = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"+ ppr (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")"+ ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"++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 > 1 && j > 0 = Just (I (ceiling (logBase (fromInteger i :: Double)+ (fromInteger j))))+ | otherwise = Nothing+mergeCLog x y = Just (CLog x y)++mergeExp :: ExtraOp -> ExtraOp -> ExtraOp+mergeExp (I i) (I j) = I (i^j)+mergeExp x y = Exp x y
+ src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -0,0 +1,119 @@+module GHC.TypeLits.Extra.Solver.Unify where++-- external+import Data.Function (on)++-- GHC API+import Outputable (Outputable (..), (<+>), ($$), text)+import TcPluginM (TcPluginM, tcPluginTrace)+import TcRnMonad (Ct)+import TcTypeNats (typeNatExpTyCon)+import Type (TyVar, tcView, mkNumLitTy, mkTyConApp, mkTyVarTy)+import TyCon (TyCon)+import TypeRep (Type (..), TyLit (..))+import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)++-- internal+import GHC.TypeLits.Extra.Solver.Operations++data ExtraDefs = ExtraDefs+ { gcdTyCon :: TyCon+ , clogTyCon :: TyCon+ }++normaliseNat :: ExtraDefs -> Type -> Maybe ExtraOp+normaliseNat defs ty | Just ty1 <- tcView ty = normaliseNat defs ty1+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 == clogTyCon defs = do x' <- normaliseNat defs x+ y' <- normaliseNat defs y+ mergeCLog x' y'+ | tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x+ <*> normaliseNat defs y+ | otherwise = Nothing+normaliseNat _ _ = Nothing++reifyExtraOp :: ExtraDefs -> ExtraOp -> Type+reifyExtraOp _ (I i) = mkNumLitTy i+reifyExtraOp _ (V v) = mkTyVarTy v+reifyExtraOp defs (GCD x y) = mkTyConApp (gcdTyCon defs)+ [reifyExtraOp defs x+ ,reifyExtraOp defs y+ ]+reifyExtraOp defs (CLog x y) = mkTyConApp (clogTyCon defs)+ [reifyExtraOp defs x+ ,reifyExtraOp defs y+ ]+reifyExtraOp defs (Exp x y) = mkTyConApp typeNatExpTyCon+ [reifyExtraOp defs x+ ,reifyExtraOp defs y+ ]+++type ExtraSubst = [SubstItem]++data SubstItem+ = SubstItem+ { siVar :: TyVar+ , siOP :: ExtraOp+ , siNote :: Ct+ }++instance Outputable SubstItem where+ ppr si = ppr (siVar si) <+> text " := " <+> ppr (siOP si)++substsExtra :: ExtraSubst -> ExtraOp -> ExtraOp+substsExtra [] u = u+substsExtra (si:s) u = substsExtra s (substExtra (siVar si) (siOP si) u)++substExtra :: TyVar -> ExtraOp -> ExtraOp -> ExtraOp+substExtra _ _ i@(I _) = i+substExtra tv e v@(V tv')+ | tv == tv' = e+ | otherwise = v+substExtra tv e (GCD x y) = mergeGCD (substExtra tv e x) (substExtra tv e y)+substExtra tv e (CLog x y) = case mergeCLog x' y' of+ Just k -> k+ Nothing -> CLog x' y'+ where+ x' = substExtra tv e x+ y' = substExtra tv e y+substExtra tv e (Exp x y) = mergeExp (substExtra tv e x) (substExtra tv e y)++substsSubst :: ExtraSubst -> ExtraSubst -> ExtraSubst+substsSubst s = map (\si -> si {siOP = substsExtra s (siOP si)})++-- | Result of comparing two 'SOP' terms, returning a potential substitution+-- list under which the two terms are equal.+data UnifyResult+ = Win -- ^ Two terms are equal+ | Lose -- ^ Two terms are /not/ equal+ | Draw ExtraSubst -- ^ Two terms are only equal if the given substitution holds++instance Outputable UnifyResult where+ ppr Win = text "Win"+ ppr (Draw subst) = text "Draw" <+> ppr subst+ ppr Lose = text "Lose"++unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult+unifyExtra ct u v = do+ tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v)+ return (unifyExtra' ct u v)++unifyExtra' :: Ct -> ExtraOp -> ExtraOp -> UnifyResult+unifyExtra' _ u v+ | eqFV u v = if u == v then Win else Lose+ | otherwise = Draw []++fvOP :: ExtraOp -> UniqSet TyVar+fvOP (I _) = emptyUniqSet+fvOP (V v) = unitUniqSet v+fvOP (GCD x y) = fvOP x `unionUniqSets` fvOP y+fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y+fvOP (Exp x y) = fvOP x `unionUniqSets` fvOP y++eqFV :: ExtraOp -> ExtraOp -> Bool+eqFV = (==) `on` fvOP
+ tests/ErrorTests.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE DataKinds, TypeOperators #-}++{-# OPTIONS_GHC -fdefer-type-errors #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}++module ErrorTests where++import GHC.TypeLits+import GHC.TypeLits.Extra+import Data.Proxy++testFail1 :: Proxy (GCD 6 8) -> Proxy 4+testFail1 = id++testFail2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 6 9))+testFail2 = id++testFail3 :: Proxy (CLog 3 10) -> Proxy 2+testFail3 = id++testFail4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 9))+testFail4 = id++testFail5 :: Proxy (CLog 0 4) -> Proxy 100+testFail5 = id++testFail6 :: Proxy (CLog 1 4) -> Proxy 100+testFail6 = id++testFail7 :: Proxy (CLog 4 0) -> Proxy 0+testFail7 = id++testFail8 :: Proxy (CLog 1 (1^y)) -> Proxy y+testFail8 = id++testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y+testFail9 = id++testFail1Errors =+ ["Expected type: Proxy (GCD 6 8) -> Proxy 4"+ ,"Actual type: Proxy 4 -> Proxy 4"+ ]++testFail2Errors =+ ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)"+ ,"Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)"+ ]++testFail3Errors =+ ["Expected type: Proxy (CLog 3 10) -> Proxy 2"+ ,"Actual type: Proxy 2 -> Proxy 2"+ ]++testFail4Errors =+ ["Expected type: Proxy (CLog 3 10 + x) -> Proxy (x + CLog 2 9)"+ ,"Actual type: Proxy (x + CLog 2 9) -> Proxy (x + CLog 2 9)"+ ]++testFail5Errors =+ ["Expected type: Proxy (CLog 0 4) -> Proxy 100"+ ,"Actual type: Proxy 100 -> Proxy 100"+ ]++testFail6Errors =+ ["Expected type: Proxy (CLog 1 4) -> Proxy 100"+ ,"Actual type: Proxy 100 -> Proxy 100"+ ]++testFail7Errors =+ ["Expected type: Proxy (CLog 4 0) -> Proxy 0"+ ,"Actual type: Proxy 0 -> Proxy 0"+ ]++testFail8Errors =+ ["Expected type: Proxy (CLog 1 (1 ^ y)) -> Proxy y"+ ,"Actual type: Proxy y -> Proxy y"+ ]++testFail9Errors =+ ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y"+ ,"Actual type: Proxy y -> Proxy y"+ ]
+ tests/Main.hs view
@@ -0,0 +1,73 @@+{-# LANGUAGE DataKinds, TypeOperators, ScopedTypeVariables #-}++{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}++import Data.List (isInfixOf)+import Control.Exception+import Test.Tasty+import Test.Tasty.HUnit++import ErrorTests++import GHC.TypeLits+import GHC.TypeLits.Extra+import Data.Proxy++test1 :: Proxy (GCD 6 8) -> Proxy 2+test1 = id++test2 :: Proxy ((GCD 6 8) + x) -> Proxy (x + (GCD 10 8))+test2 = id++test3 :: Proxy (CLog 3 10) -> Proxy 3+test3 = id++test4 :: Proxy ((CLog 3 10) + x) -> Proxy (x + (CLog 2 7))+test4 = id++test5 :: Proxy (CLog x (x^y)) -> Proxy y+test5 = id++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "ghc-typelits-natnormalise"+ [ testGroup "Basic functionality"+ [ testCase "GCD 6 8 ~ 2" $+ show (test1 Proxy) @?=+ "Proxy"+ , testCase "forall x . GCD 6 8 + x ~ x + GCD 10 8" $+ show (test2 Proxy) @?=+ "Proxy"+ , testCase "CLog 3 10 ~ 3" $+ show (test3 Proxy) @?=+ "Proxy"+ , testCase "forall x . CLog 3 10 + x ~ x + CLog 2 7" $+ show (test4 Proxy) @?=+ "Proxy"+ , testCase "forall x>1 . CLog x (x^y) ~ y" $+ show (test4 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+ ]+ ]++-- | Assert that evaluation of the first argument (to WHNF) will throw+-- an exception whose string representation contains the given+-- substrings.+throws :: a -> [String] -> Assertion+throws v xs =+ (evaluate v >> assertFailure "No exception!")+ `catch` \ (e :: SomeException) -> if all (`isInfixOf` show e) xs then return () else throw e