ghc-typelits-extra 0.1 → 0.1.1
raw patch · 6 files changed
+79/−63 lines, 6 filesdep ~basedep ~ghcdep ~ghc-tcplugins-extra
Dependency ranges changed: base, ghc, ghc-tcplugins-extra, ghc-typelits-extra, ghc-typelits-natnormalise
Files
- CHANGELOG.md +3/−0
- ghc-typelits-extra.cabal +16/−8
- src/GHC/TypeLits/Extra/Solver.hs +30/−39
- src/GHC/TypeLits/Extra/Solver/Unify.hs +15/−10
- tests/ErrorTests.hs +1/−1
- tests/Main.hs +14/−5
CHANGELOG.md view
@@ -1,4 +1,7 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +## 0.1.1 *January 20th 2015*+* Compile on GHC 8.0++ ## 0.1 *October 21st 2015* * Initial release
ghc-typelits-extra.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-extra-version: 0.1+version: 0.1.1 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@:@@ -7,7 +7,7 @@ * @GHC.TypeLits.Extra.GCD@: a type-level @gcd@ . * @GHC.TypeLits.Extra.CLog@: type-level equivalent of- "@clog x y = ceiling (logBase x y)@"+ \"@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,@@ -46,11 +46,15 @@ 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+ build-depends: base >= 4.8 && <5,+ ghc >= 7.10 && <8.2,+ ghc-tcplugins-extra >= 0.2 hs-source-dirs: src default-language: Haskell2010+ other-extensions: CPP+ DataKinds+ TupleSections+ TypeFamilies if flag(deverror) ghc-options: -Wall -Werror else@@ -60,12 +64,16 @@ 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,+ build-depends: base >= 4.8 && <5,+ ghc-typelits-extra >= 0.1.1,+ ghc-typelits-natnormalise >= 0.4, tasty >= 0.10, tasty-hunit >= 0.9 hs-source-dirs: tests default-language: Haskell2010+ other-extensions: CPP+ DataKinds+ TypeOperators+ ScopedTypeVariables if flag(deverror) ghc-options: -O0 -dcore-lint
src/GHC/TypeLits/Extra/Solver.hs view
@@ -1,7 +1,12 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE TupleSections #-} {-# OPTIONS_HADDOCK show-extensions #-} +#if __GLASGOW_HASKELL__ < 711+{-# OPTIONS_GHC -fno-warn-deprecations #-}+#endif+ {-| Copyright : (C) 2015, Christiaan Baaij License : BSD2 (see the file LICENSE)@@ -14,9 +19,10 @@ -- external import Data.Maybe (catMaybes, mapMaybe)-import GHC.TcPluginM.Extra (evByFiat, failWithProvenace, lookupModule,- lookupName, newGiven, newWantedWithProvenance,- tracePlugin)+import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName, tracePlugin)+#if __GLASGOW_HASKELL__ < 711+import GHC.TcPluginM.Extra (failWithProvenace)+#endif -- GHC API import FastString (fsLit)@@ -26,11 +32,11 @@ 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 TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,+ isWanted)+import TcType (typeKind) import Type (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,- mkTyVarTy)+ eqType) import TysWiredIn (typeNatKind) -- internal@@ -74,50 +80,35 @@ 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+ 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 type NatEquality = (Ct,ExtraOp,ExtraOp) data SimplifyResult- = Simplified ExtraSubst [(EvTerm,Ct)]+ = Simplified [(EvTerm,Ct)] | Impossible NatEquality instance Outputable SimplifyResult where- ppr (Simplified subst evs) = text "Simplified" $$ ppr subst $$ ppr evs+ ppr (Simplified evs) = text "Simplified" $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult-simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] [] [] eqs+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)+ simples :: [Maybe (EvTerm, Ct)] -> [NatEquality] -> TcPluginM SimplifyResult+ simples evs [] = return (Simplified (catMaybes evs))+ simples evs (eq@(ct,u,v):eqs') = do+ ur <- unifyExtra ct u 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')+ Win -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'+ Lose -> return (Impossible eq)+ Draw -> simples evs eqs' -- Extract the Nat equality constraints toNatEquality :: ExtraDefs -> Ct -> Maybe NatEquality@@ -128,7 +119,7 @@ _ -> Nothing where isNatKind :: Kind -> Bool- isNatKind = (== typeNatKind)+ isNatKind = (`eqType` typeNatKind) fromNatEquality :: NatEquality -> Ct fromNatEquality (ct, _, _) = ct
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} module GHC.TypeLits.Extra.Solver.Unify where -- external@@ -8,9 +9,13 @@ import TcPluginM (TcPluginM, tcPluginTrace) import TcRnMonad (Ct) import TcTypeNats (typeNatExpTyCon)-import Type (TyVar, tcView, mkNumLitTy, mkTyConApp, mkTyVarTy)+import Type (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy) import TyCon (TyCon)-import TypeRep (Type (..), TyLit (..))+#if __GLASGOW_HASKELL__ >= 711+import TyCoRep (Type (..), TyLit (..))+#else+import TypeRep (Type (..), TyLit (..))+#endif import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) -- internal@@ -22,7 +27,7 @@ } normaliseNat :: ExtraDefs -> Type -> Maybe ExtraOp-normaliseNat defs ty | Just ty1 <- tcView ty = normaliseNat defs ty1+normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1 normaliseNat _ (TyVarTy v) = pure (V v) normaliseNat _ (LitTy (NumTyLit i)) = pure (I i) normaliseNat defs (TyConApp tc [x,y])@@ -89,14 +94,14 @@ -- | 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+ = Win -- ^ Two terms are equal+ | Lose -- ^ Two terms are /not/ equal+ | Draw -- ^ We don't know if the two terms are equal instance Outputable UnifyResult where- ppr Win = text "Win"- ppr (Draw subst) = text "Draw" <+> ppr subst- ppr Lose = text "Lose"+ ppr Win = text "Win"+ ppr Lose = text "Lose"+ ppr Draw = text "Draw" unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult unifyExtra ct u v = do@@ -106,7 +111,7 @@ unifyExtra' :: Ct -> ExtraOp -> ExtraOp -> UnifyResult unifyExtra' _ u v | eqFV u v = if u == v then Win else Lose- | otherwise = Draw []+ | otherwise = Draw fvOP :: ExtraOp -> UniqSet TyVar fvOP (I _) = emptyUniqSet
tests/ErrorTests.hs view
@@ -6,9 +6,9 @@ module ErrorTests where +import Data.Proxy import GHC.TypeLits import GHC.TypeLits.Extra-import Data.Proxy testFail1 :: Proxy (GCD 6 8) -> Proxy 4 testFail1 = id
tests/Main.hs view
@@ -1,9 +1,10 @@-{-# LANGUAGE DataKinds, TypeOperators, ScopedTypeVariables #-}+{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} import Data.List (isInfixOf)+import Data.Proxy import Control.Exception import Test.Tasty import Test.Tasty.HUnit@@ -12,7 +13,6 @@ import GHC.TypeLits import GHC.TypeLits.Extra-import Data.Proxy test1 :: Proxy (GCD 6 8) -> Proxy 2 test1 = id@@ -68,6 +68,15 @@ -- 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+throws v xs = do+ 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