diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal --- a/ghc-typelits-presburger.cabal +++ b/ghc-typelits-presburger.cabal @@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2. +-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack -- --- hash: 213617ccefa67bad574a0687988e14cef38a75e07ac2e08140bcda55feeee3f6 +-- hash: 3e336ef49eb47a4a5b2a74bdb84e17585fa0870e8c22e48ebb8402904c01ffe7 name: ghc-typelits-presburger -version: 0.3.0.0 +version: 0.3.0.1 synopsis: Presburger Arithmetic Solver for GHC Type-level natural numbers. description: @ghc-typelits-presburger@ augments GHC type-system with Presburger Arithmetic Solver for Type-level natural numbers. @@ -29,7 +29,7 @@ copyright: 2015 (c) Hiromi ISHII license: BSD3 license-file: LICENSE -tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.2 +tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.1 build-type: Simple source-repository head @@ -56,7 +56,7 @@ base >=4.7 && <5 , containers , ghc >=7.10 && <8.11 - , ghc-tcplugins-extra >=0.2 && <0.4 + , ghc-tcplugins-extra >=0.2 && <0.5 , mtl , pretty , reflection diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs --- a/src/GHC/TypeLits/Presburger/Compat.hs +++ b/src/GHC/TypeLits/Presburger/Compat.hs @@ -5,11 +5,10 @@ import Data.Function (on) import FamInst as GHC.TypeLits.Presburger.Compat import FastString as GHC.TypeLits.Presburger.Compat (fsLit) +import Class import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName, tracePlugin) -import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..)) -import GhcPlugins as GHC.TypeLits.Presburger.Compat (classifyPredType, isEqPred, - lookupTyCon, mkTyConTy) +import GhcPlugins as GHC.TypeLits.Presburger.Compat (lookupTyCon, mkTyConTy) import GhcPlugins as GHC.TypeLits.Presburger.Compat (mkTcOcc, ppr, promotedFalseDataCon) import GhcPlugins as GHC.TypeLits.Presburger.Compat (promotedTrueDataCon, text) import GhcPlugins as GHC.TypeLits.Presburger.Compat (tyConAppTyCon_maybe, typeKind) @@ -21,8 +20,8 @@ import TcHsType as GHC.TypeLits.Presburger.Compat (tcInferApps) import TcPluginM as GHC.TypeLits.Presburger.Compat (TcPluginM, tcLookupTyCon, tcPluginTrace) -import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, TcPluginResult (..), isWanted) -import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..), ctEvPred, ctEvidence) +import TcRnMonad as GHC.TypeLits.Presburger.Compat (TcPluginResult (..)) +import TcRnTypes as GHC.TypeLits.Presburger.Compat (TcPlugin (..)) import TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts) import TcTypeNats as GHC.TypeLits.Presburger.Compat import TyCon as GHC.TypeLits.Presburger.Compat @@ -62,7 +61,35 @@ #if MIN_VERSION_ghc(8,8,1) import qualified TysWiredIn #endif +#if MIN_VERSION_ghc(8,8,1) +import TysWiredIn (eqTyConName) +#else +import PrelNames (eqTyConName) +#endif +#if MIN_VERSION_ghc(8,10,1) +import Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred(..)) +import Predicate as GHC.TypeLits.Presburger.Compat (isEqPred) + +import qualified Predicate as Old (classifyPredType) +import Predicate as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole) +import Constraint as GHC.TypeLits.Presburger.Compat + (Ct, ctEvidence, ctEvPred, isWanted) +#else +import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..)) +import GhcPlugins as GHC.TypeLits.Presburger.Compat (isEqPred) +import qualified GhcPlugins as Old (classifyPredType) +import TcRnMonad as GHC.TypeLits.Presburger.Compat (Ct, isWanted) +import Type as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole) +import TcRnTypes as GHC.TypeLits.Presburger.Compat (ctEvPred, ctEvidence) +#endif + + +#if MIN_VERSION_ghc(8,10,1) +type PredTree = Pred +#endif + + #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 data TvSubst = TvSubst InScopeSet TvSubstEnv @@ -127,7 +154,11 @@ tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:") decompFunTy :: Type -> [Type] +#if MIN_VERSION_ghc(8,10,1) +decompFunTy (FunTy _ t1 t2) = t1 : decompFunTy t2 +#else decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2 +#endif decompFunTy t = [t] newtype TypeEq = TypeEq { runTypeEq :: Type } @@ -192,3 +223,12 @@ EqPred NomEq t u -> fromMaybe emptyTvSubst $ GHC.TypeLits.Presburger.Compat.tcUnifyTy t u _ -> emptyTvSubst #endif + + +classifyPredType :: Type -> PredTree +classifyPredType ty = case Old.classifyPredType ty of + e@EqPred{} -> e + ClassPred cls [_,t1,t2] + | className cls == eqTyConName + -> EqPred NomEq t1 t2 + e -> e diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs --- a/src/GHC/TypeLits/Presburger/Types.hs +++ b/src/GHC/TypeLits/Presburger/Types.hs @@ -11,6 +11,7 @@ import Class (classTyCon) import Control.Applicative ((<|>)) import Control.Arrow (second) +import Outputable (showSDocUnsafe) import Control.Monad (forM_, guard, mzero, unless) import Control.Monad.State.Class import Control.Monad.Trans.Class @@ -32,10 +33,16 @@ import PrelNames import TcPluginM (lookupOrig, newFlexiTyVar, newWanted, tcLookupClass) -import Type (mkPrimEqPredRole, mkTyVarTy) +import Type (mkTyVarTy) import TysWiredIn (promotedEQDataCon, promotedGTDataCon, promotedLTDataCon) +#if MIN_VERSION_ghc(8,8,1) +import TysWiredIn (eqTyConName) +#else +import PrelNames (eqTyConName) +#endif + import Var #if MIN_VERSION_ghc(8,6,0) import Plugins (purePlugin) @@ -238,7 +245,7 @@ decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult decidePresburger _ genTrans _ gs [] [] = do - tcPluginTrace "Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs) + tcPluginTrace "pres: Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs) trans <- genTrans give trans $ do ngs <- mapM (\a -> runMachine $ (,) a <$> toPresburgerPred (deconsPred a)) gs @@ -258,10 +265,10 @@ give trans $ do gs' <- normaliseGivens gs let subst = mkSubstitution (gs' ++ ds) - tcPluginTrace "Current subst" (ppr subst) - tcPluginTrace "wanteds" $ ppr $ map deconsPred ws - tcPluginTrace "givens" $ ppr $ map (subsType subst . deconsPred) gs - tcPluginTrace "deriveds" $ ppr $ map deconsPred ds + tcPluginTrace "pres: Current subst" (ppr subst) + tcPluginTrace "pres: wanteds" $ ppr $ map (subsType subst . deconsPred . subsCt subst) ws + tcPluginTrace "pres: givens" $ ppr $ map (subsType subst . deconsPred) gs + tcPluginTrace "pres: deriveds" $ ppr $ map deconsPred ds (prems, wants, prems0) <- do wants <- catMaybes <$> mapM @@ -279,15 +286,15 @@ | ct <- solved , EqPred NomEq t1 t2 <- return (classifyPredType $ deconsPred ct) ] - tcPluginTrace "final premises" (text $ show prems0) - tcPluginTrace "final goals" (text $ show $ map snd wants) + tcPluginTrace "pres: final premises" (text $ show prems0) + tcPluginTrace "pres: final goals" (text $ show $ map snd wants) case testIf prems (foldr ((:&&) . snd) PTrue wants) of Proved -> do - tcPluginTrace "Proved" (text $ show $ map snd wants) - tcPluginTrace "... with coercions" (ppr coerced) + tcPluginTrace "pres: Proved" (text $ show $ map snd wants) + tcPluginTrace "pres: ... with coercions" (ppr coerced) return $ TcPluginOk coerced [] Disproved wit -> do - tcPluginTrace "Failed! " (text $ show wit) + tcPluginTrace "pres: Failed! " (text $ show wit) return $ TcPluginContradiction $ map fst wants defaultTranslation :: TcPluginM Translation @@ -326,10 +333,10 @@ p <=> q = (p :&& q) :|| (Not p :&& Not q) withEv :: Ct -> (EvTerm, Ct) -withEv ct - | EqPred _ t1 t2 <- classifyPredType (deconsPred ct) = - (evByFiat "ghc-typelits-presburger" t1 t2, ct) - | otherwise = undefined +withEv ct = + case classifyPredType (deconsPred ct) of + EqPred _ t1 t2 -> (evByFiat "ghc-typelits-presburger" t1 t2, ct) + _ -> error $ "UnknownPredEv: " <> showSDocUnsafe (ppr ct) orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)] orderingDic = @@ -349,6 +356,8 @@ , con `elem` trueData given = return PTrue | Just (con, []) <- splitTyConApp_maybe ty , con `elem` falseData given = return PFalse + | cls@(EqPred NomEq _ _) <- classifyPredType ty + = toPresburgerPredTree cls | isEqPred ty = toPresburgerPredTree $ classifyPredType ty | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r , con `elem` (tyEq given ++ tyEqBool given) @@ -378,7 +387,7 @@ , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do - lift $ lift $ tcPluginTrace "EQBOOL:" $ ppr (p, q) + lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q) (<=>) <$> toPresburgerPred p <*> toPresburgerPred q toPresburgerPredTree (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat) @@ -462,7 +471,11 @@ simpleExp :: Given Translation => Type -> Type simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2) +#if MIN_VERSION_ghc(8,10,1) +simpleExp (FunTy f t1 t2) = FunTy f (simpleExp t1) (simpleExp t2) +#else simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2) +#endif simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) simpleExp (TyConApp tc (lastTwo -> ts)) = fromMaybe (TyConApp tc (map simpleExp ts)) $ asum (map simpler