diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,9 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package -## 0.1.1 *January 20th 2015* +## 0.1.2 *July 8th 2016* +* Solve KnownNat constraints over CLog and GCD, i.e., KnownNat (CLog 2 4) + +## 0.1.1 *January 20th 2016* * Compile on GHC 8.0+ ## 0.1 *October 21st 2015* diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2015, Christiaan Baaij +Copyright (c) 2015-2016, University of Twente All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal --- a/ghc-typelits-extra.cabal +++ b/ghc-typelits-extra.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-extra -version: 0.1.1 +version: 0.1.2 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@: @@ -24,7 +24,7 @@ license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com -copyright: Copyright © 2015 University of Twente +copyright: Copyright © 2015-2016 University of Twente category: Type System build-type: Simple extra-source-files: README.md @@ -48,7 +48,8 @@ GHC.TypeLits.Extra.Solver.Operations build-depends: base >= 4.8 && <5, ghc >= 7.10 && <8.2, - ghc-tcplugins-extra >= 0.2 + ghc-tcplugins-extra >= 0.2, + transformers >= 0.4.2.0 && < 0.6 hs-source-dirs: src default-language: Haskell2010 other-extensions: CPP @@ -66,7 +67,7 @@ Other-Modules: ErrorTests build-depends: base >= 4.8 && <5, ghc-typelits-extra >= 0.1.1, - ghc-typelits-natnormalise >= 0.4, + ghc-typelits-natnormalise >= 0.4.1, tasty >= 0.10, tasty-hunit >= 0.9 hs-source-dirs: tests 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 @@ -1,12 +1,5 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeFamilies #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -{-# LANGUAGE Safe #-} - {-| -Copyright : (C) 2015, University of Twente +Copyright : (C) 2015-2016, University of Twente License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij @@ -27,6 +20,14 @@ pragma to the header of your file. -} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +{-# LANGUAGE Safe #-} + module GHC.TypeLits.Extra where import GHC.TypeLits (Nat) 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 @@ -1,3 +1,18 @@ +{-| +Copyright : (C) 2015-2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij + +To use the plugin, add the + +@ +{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\} +@ + +pragma to the header of your file + +-} + {-# LANGUAGE CPP #-} {-# LANGUAGE TupleSections #-} @@ -7,36 +22,37 @@ {-# OPTIONS_GHC -fno-warn-deprecations #-} #endif -{-| -Copyright : (C) 2015, Christiaan Baaij -License : BSD2 (see the file LICENSE) -Maintainer : Christiaan Baaij - --} module GHC.TypeLits.Extra.Solver ( plugin ) where -- external -import Data.Maybe (catMaybes, mapMaybe) -import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName, tracePlugin) +import Control.Monad ((<=<)) +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Data.Maybe (catMaybes) +import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName, + tracePlugin) #if __GLASGOW_HASKELL__ < 711 -import GHC.TcPluginM.Extra (failWithProvenace) +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 TcEvidence (EvTerm) +import PrelNames (knownNatClassName) +import TcEvidence (EvTerm (EvLit), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo) import TcPluginM (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt) import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred, isWanted) import TcType (typeKind) -import Type (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType, - eqType) +import Type (EqRel (NomEq), Kind, PredTree (EqPred, ClassPred), Type, classifyPredType, + dropForAlls, eqType, funResultTy, tyConAppTyCon_maybe) import TysWiredIn (typeNatKind) -- internal @@ -72,11 +88,11 @@ 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' + unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds' case unit_wanteds of [] -> return (TcPluginOk [] []) _ -> do - unit_givens <- mapMaybe (toNatEquality defs) <$> mapM zonkCt givens + unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens sr <- simplifyExtra (unit_givens ++ unit_wanteds) tcPluginTrace "normalised" (ppr sr) case sr of @@ -87,7 +103,8 @@ Impossible eq -> failWithProvenace (fromNatEquality eq) #endif -type NatEquality = (Ct,ExtraOp,ExtraOp) +type NatEquality = (Ct,ExtraOp,ExtraOp) +type KnConstraint = (Ct,Class,Type,ExtraOp) data SimplifyResult = Simplified [(EvTerm,Ct)] @@ -97,26 +114,34 @@ ppr (Simplified evs) = text "Simplified" $$ ppr evs ppr (Impossible eq) = text "Impossible" <+> ppr eq -simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult +simplifyExtra :: [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs where - simples :: [Maybe (EvTerm, Ct)] -> [NatEquality] -> TcPluginM SimplifyResult + simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult simples evs [] = return (Simplified (catMaybes evs)) - simples evs (eq@(ct,u,v):eqs') = do + simples evs (Left 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 -> Maybe NatEquality +toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality KnConstraint) 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 + -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2) + ClassPred cls [ty] + | className cls == knownNatClassName + -> Right <$> ((ct,cls,ty,) <$> normaliseNat defs ty) + _ -> fail "Nothing" where isNatKind :: Kind -> Bool isNatKind = (`eqType` typeNatKind) @@ -140,3 +165,32 @@ 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 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 @@ -1,12 +1,46 @@ -module GHC.TypeLits.Extra.Solver.Operations where +{-| +Copyright : (C) 2015-2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij +-} +{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-} +#if __GLASGOW_HASKELL__ < 711 +{-# LANGUAGE StandaloneDeriving #-} +#endif + +module GHC.TypeLits.Extra.Solver.Operations + ( ExtraOp (..) + , EType (..) + , mergeGCD + , mergeCLog + , mergeExp + , mergeAdd + , mergeSub + , mergeMul + ) +where + -- GHC API import Outputable (Outputable (..), (<+>), integer, text) -import Type (TyVar) +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 + data ExtraOp = I Integer | V TyVar + | C EType | GCD ExtraOp ExtraOp | CLog ExtraOp ExtraOp | Exp ExtraOp ExtraOp @@ -15,6 +49,7 @@ instance Outputable ExtraOp where 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 (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")" ppr (Exp x y) = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")" @@ -35,3 +70,17 @@ mergeExp :: ExtraOp -> ExtraOp -> ExtraOp mergeExp (I i) (I j) = I (i^j) mergeExp x y = Exp x y + +mergeAdd :: ExtraOp -> ExtraOp -> Maybe ExtraOp +mergeAdd (I i) (I j) = Just (I (i + j)) +mergeAdd _ _ = Nothing + +mergeSub :: ExtraOp -> ExtraOp -> Maybe ExtraOp +mergeSub (I i) (I j) + | let s = i - j + , s >= 0 = Just (I s) +mergeSub _ _ = Nothing + +mergeMul :: ExtraOp -> ExtraOp -> Maybe ExtraOp +mergeMul (I i) (I j) = Just (I (i * j)) +mergeMul _ _ = 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 @@ -1,20 +1,35 @@ +{-| +Copyright : (C) 2015-2016, University of Twente +License : BSD2 (see the file LICENSE) +Maintainer : Christiaan Baaij +-} + {-# LANGUAGE CPP #-} -module GHC.TypeLits.Extra.Solver.Unify where +module GHC.TypeLits.Extra.Solver.Unify + ( ExtraDefs (..) + , UnifyResult (..) + , normaliseNat + , unifyExtra + ) +where + -- external -import Data.Function (on) +import Control.Monad.Trans.Class (lift) +import Control.Monad.Trans.Maybe (MaybeT (..)) +import Data.Function (on) -- GHC API -import Outputable (Outputable (..), (<+>), ($$), text) -import TcPluginM (TcPluginM, tcPluginTrace) +import Outputable (Outputable (..), ($$), text) +import TcPluginM (TcPluginM, matchFam, tcPluginTrace) import TcRnMonad (Ct) import TcTypeNats (typeNatExpTyCon) import Type (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy) import TyCon (TyCon) #if __GLASGOW_HASKELL__ >= 711 -import TyCoRep (Type (..), TyLit (..)) +import TyCoRep (Type (..), TyLit (..)) #else -import TypeRep (Type (..), TyLit (..)) +import TypeRep (Type (..), TyLit (..)) #endif import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) @@ -26,7 +41,7 @@ , clogTyCon :: TyCon } -normaliseNat :: ExtraDefs -> Type -> Maybe ExtraOp +normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1 normaliseNat _ (TyVarTy v) = pure (V v) normaliseNat _ (LitTy (NumTyLit i)) = pure (I i) @@ -35,61 +50,18 @@ <*> normaliseNat defs y | tc == clogTyCon defs = do x' <- normaliseNat defs x y' <- normaliseNat defs y - mergeCLog x' y' + MaybeT (return (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) +normaliseNat defs (TyConApp tc tys) = do + tys' <- mapM (fmap (reifyEOP defs) . normaliseNat defs) tys + tyM <- lift (matchFam tc tys') + case tyM of + Just (_,ty) -> normaliseNat defs ty + _ -> return (C (EType (TyConApp tc tys))) -substsSubst :: ExtraSubst -> ExtraSubst -> ExtraSubst -substsSubst s = map (\si -> si {siOP = substsExtra s (siOP si)}) +normaliseNat _ t = return (C (EType t)) -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal. @@ -110,15 +82,38 @@ unifyExtra' :: Ct -> ExtraOp -> ExtraOp -> UnifyResult unifyExtra' _ u v - | eqFV u v = if u == v then Win else Lose + | eqFV u v = if u == v then Win + else if containsConstants u || containsConstants v + then Draw + else Lose | otherwise = Draw fvOP :: ExtraOp -> UniqSet TyVar fvOP (I _) = emptyUniqSet fvOP (V v) = unitUniqSet v +fvOP (C _) = emptyUniqSet 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 + +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 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] + +containsConstants :: ExtraOp -> Bool +containsConstants (I _) = False +containsConstants (V _) = False +containsConstants (C _) = True +containsConstants (GCD x y) = containsConstants x || containsConstants y +containsConstants (CLog x y) = containsConstants x || containsConstants y +containsConstants (Exp x y) = containsConstants x || containsConstants y diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -37,6 +37,12 @@ testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y testFail9 = id +testFail10 :: Integer +testFail10 = natVal (Proxy :: Proxy (CLog 1 4)) + +testFail11 :: Integer +testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4))) + testFail1Errors = ["Expected type: Proxy (GCD 6 8) -> Proxy 4" ,"Actual type: Proxy 4 -> Proxy 4" @@ -81,3 +87,9 @@ ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y" ,"Actual type: Proxy y -> Proxy y" ] + +testFail10Errors = + ["No instance for (KnownNat (CLog 1 4))"] + +testFail11Errors = + ["No instance for (KnownNat (CLog 4 4 - CLog 2 4))"] diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,10 +1,12 @@ -{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables #-} +{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables, KindSignatures, + TypeFamilies, UndecidableInstances #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-} import Data.List (isInfixOf) import Data.Proxy +import Data.Type.Bool import Control.Exception import Test.Tasty import Test.Tasty.HUnit @@ -29,6 +31,22 @@ test5 :: Proxy (CLog x (x^y)) -> Proxy y test5 = id +test6 :: Integer +test6 = natVal (Proxy :: Proxy (CLog 6 8)) + +test7 :: Integer +test7 = natVal (Proxy :: Proxy (CLog 3 10)) + +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))) + main :: IO () main = defaultMain tests @@ -50,6 +68,18 @@ , testCase "forall x>1 . CLog x (x^y) ~ y" $ show (test4 Proxy) @?= "Proxy" + , testCase "KnownNat (CLog 6 8) ~ 2" $ + show test6 @?= + "2" + , testCase "KnownNat (CLog 3 10) ~ 3" $ + show test7 @?= + "3" + , testCase "KnownNat ((CLog 2 4) * (3 ^ (CLog 2 4)))) ~ 18" $ + show test8 @?= + "18" + , testCase "KnownNat (Max (CLog 2 4) (CLog 4 20)) ~ 3" $ + show test9 @?= + "3" ] , testGroup "errors" [ testCase "GCD 6 8 ~ 4" $ testFail1 `throws` testFail1Errors @@ -61,6 +91,8 @@ , 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 ] ]