diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs --- a/examples/simple-arith-core.hs +++ b/examples/simple-arith-core.hs @@ -62,7 +62,7 @@ hoge _ Witness = absurdTrueFalse Refl #endif -bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> () +bar :: (2 * (n + 1)) ~ (2 * n + 2) => proxy n -> () bar _ = () barResult :: () @@ -88,3 +88,15 @@ main :: IO () main = putStrLn "finished" + +rangeEql :: + ((n == 0) ~ 'False) => + pxy n -> + (1 <=? n) :~: 'True +rangeEql _ = Refl + +rangeEqlLeq :: + ((n == 3) ~ 'False, n <= 3) => + pxy n -> + (n <=? 2) :~: 'True +rangeEqlLeq _ = Refl diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal --- a/ghc-typelits-presburger.cabal +++ b/ghc-typelits-presburger.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 65b575c871af31347563414029325499d7d362c533a6eef7ffc5ebe477ee9fa1 +-- hash: f4ea69ea55a2f6e349e91e0e359ba111afa36236c8c094e799d1e95ac82ce411 name: ghc-typelits-presburger -version: 0.5.0.0 +version: 0.5.2.0 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.3 GHC==8.10.3 +tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.3 GHC==9.0.1 build-type: Simple source-repository head @@ -55,7 +55,7 @@ build-depends: base >=4.7 && <5 , containers - , ghc >=7.10 && <8.11 + , ghc <9.1 , ghc-tcplugins-extra >=0.2 && <0.5 , mtl , pretty diff --git a/src/GHC/TypeLits/Presburger.hs b/src/GHC/TypeLits/Presburger.hs --- a/src/GHC/TypeLits/Presburger.hs +++ b/src/GHC/TypeLits/Presburger.hs @@ -1,10 +1,12 @@ --- | Provides a plain Presburger solver plugin for @'GHC.TypeNats.Nat'@. --- --- For an interface for extension, see --- "GHC.TypeLits.Presburger.Types". +{- | Provides a plain Presburger solver plugin for @'GHC.TypeNats.Nat'@. + + For an interface for extension, see + "GHC.TypeLits.Presburger.Types". +-} module GHC.TypeLits.Presburger (plugin) where + +import GHC.TypeLits.Presburger.Compat import GHC.TypeLits.Presburger.Types -import GhcPlugins plugin :: Plugin plugin = pluginWith defaultTranslation 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 @@ -3,68 +3,157 @@ {-# OPTIONS_GHC -Wno-orphans #-} module GHC.TypeLits.Presburger.Compat (module GHC.TypeLits.Presburger.Compat) where 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 (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) -import GhcPlugins as GHC.TypeLits.Presburger.Compat (typeNatKind) -import Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName) -import OccName as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc) -import Plugins as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin) -import TcEvidence as GHC.TypeLits.Presburger.Compat (EvTerm) -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 (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 +import Data.Generics.Twins + +#if MIN_VERSION_ghc(9,0,0) +import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS, dATA_TYPE_EQUALITY) +import qualified GHC.Builtin.Names as Old +import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat + ( boolTyCon, + eqTyConName, + promotedEQDataCon, + promotedGTDataCon, + promotedLTDataCon, + ) +import qualified GHC.Builtin.Types as TysWiredIn +import GHC.Builtin.Types.Literals as GHC.TypeLits.Presburger.Compat +import GHC.Core.Class as GHC.TypeLits.Presburger.Compat (className, classTyCon) +import GHC.Core.FamInstEnv as GHC.TypeLits.Presburger.Compat +import GHC.Core.Predicate as GHC.TypeLits.Presburger.Compat (EqRel (..), Pred (..), isEqPred, mkPrimEqPredRole) +import qualified GHC.Core.Predicate as Old (classifyPredType) +import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..)) +import GHC.Core.TyCon as GHC.TypeLits.Presburger.Compat +import qualified GHC.Core.Type as Old +import GHC.Core.Unify as Old (tcUnifyTy) +import GHC.Unit.Types (Module, UnitId, toUnitId) +import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule) +import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS) +import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) +import GHC.Driver.Session (unitState) +import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit) +import GHC.Plugins as GHC.TypeLits.Presburger.Compat + ( PackageName (..), + Plugin (..), + TCvSubst (..), + TvSubstEnv, + TyVar, + defaultPlugin, + emptyTCvSubst, + eqType, + lookupTyCon, + mkTcOcc, + mkTyConTy, + mkTyVarTy, + ppr, + promotedFalseDataCon, + promotedTrueDataCon, + purePlugin, + splitTyConApp, + splitTyConApp_maybe, + text, + tyConAppTyCon_maybe, + typeKind, + typeNatKind, + unionTCvSubst, + ) +import GHC.Tc.Plugin (lookupOrig) +import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat + ( TcPluginM, + getTopEnv, + lookupOrig, + newFlexiTyVar, + newWanted, + matchFam, + tcLookupClass, + tcLookupTyCon, + tcPluginIO, + tcPluginTrace, + ) +import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) +import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat + ( Ct, + ctEvPred, + ctEvidence, + isWanted, + ) +import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (EvTerm) +import GHC.Tc.Utils.TcType (TcTyVar, TcType) +import GHC.Tc.Utils.TcType as GHC.TypeLits.Presburger.Compat (tcTyFamInsts) +import qualified GHC.TcPluginM.Extra as Extra +import GHC.Types.Name.Occurrence as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc) +import GHC.Types.Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique) +import GHC.Unit.Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName) +import GHC.Unit.State as GHC.TypeLits.Presburger.Compat (lookupPackageName) +import GHC.Unit.State (initUnits, UnitState (preloadUnits)) +import GHC.Unit.Types (UnitId(..), fsToUnit, toUnitId) +import GHC.Utils.Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe) +-- GHC 9 Ends HERE +#else +import Class as GHC.TypeLits.Presburger.Compat (classTyCon, className) +import FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS) +import GhcPlugins (InScopeSet, Outputable, emptyUFM, InstalledUnitId(..), initPackages) +import GhcPlugins as GHC.TypeLits.Presburger.Compat (PackageName (..), fsToUnitId, lookupPackageName, lookupTyCon, mkTcOcc, mkTyConTy, ppr, promotedFalseDataCon, promotedTrueDataCon, text, tyConAppTyCon_maybe, typeKind, typeNatKind) +import HscTypes as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) +import Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName, mkModule) +import Module (Module, UnitId) +import OccName as GHC.TypeLits.Presburger.Compat (emptyOccSet, mkInstTyTcOcc) +import Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe) +import Plugins as GHC.TypeLits.Presburger.Compat (Plugin (..), defaultPlugin) +import PrelNames as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS, dATA_TYPE_EQUALITY) +import qualified PrelNames as Old +import TcEvidence as GHC.TypeLits.Presburger.Compat (EvTerm) +import TcHsType as GHC.TypeLits.Presburger.Compat (tcInferApps) +import TcPluginM as GHC.TypeLits.Presburger.Compat + ( TcPluginM, + getTopEnv, + lookupOrig, + matchFam, + newFlexiTyVar, + newWanted, + tcLookupClass, + tcLookupTyCon, + tcPluginIO, + tcPluginTrace, + ) +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 TyCoRep () +import TyCoRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..)) +import TyCon as GHC.TypeLits.Presburger.Compat +import Type as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv, emptyTCvSubst, eqType, mkTyVarTy, splitTyConApp, splitTyConApp_maybe, unionTCvSubst) +import qualified Type as Old +import TysWiredIn as GHC.TypeLits.Presburger.Compat + ( boolTyCon, + promotedEQDataCon, + promotedGTDataCon, + promotedLTDataCon, + ) +import Unify as Old (tcUnifyTy) +import Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique) +import Var as GHC.TypeLits.Presburger.Compat (TyVar) +-- Conditional imports for GHC <9 #if MIN_VERSION_ghc(8,4,1) import TcType (TcTyVar, TcType) +import qualified GHC.TcPluginM.Extra as Extra +import qualified GHC #else -import TcRnTypes (cc_ev, ctev_pred) import Data.Maybe import TcPluginM (zonkCt) -#endif -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 -import GhcPlugins (InScopeSet, Outputable, emptyUFM) -import qualified PrelNames as Old -import TyCoRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..)) -import Type as GHC.TypeLits.Presburger.Compat (TCvSubst (..), TvSubstEnv, - emptyTCvSubst) -import Type as GHC.TypeLits.Presburger.Compat (eqType, unionTCvSubst) -import qualified Type as Old -import TysWiredIn as GHC.TypeLits.Presburger.Compat (boolTyCon) -import Unify as Old (tcUnifyTy) -#else -import Type as GHC.TypeLits.Presburger.Compat (TvSubst, emptyTvSubst) -import Type as GHC.TypeLits.Presburger.Compat (substTy, unionTvSubst) -import TypeRep as GHC.TypeLits.Presburger.Compat (TyLit (NumTyLit), Type (..)) -import TysWiredIn as Old (eqTyCon) -import TysWiredIn as GHC.TypeLits.Presburger.Compat (promotedBoolTyCon) -import Unify as GHC.TypeLits.Presburger.Compat (tcUnifyTy) +import TcRnTypes (cc_ev, ctev_pred) #endif -import Data.Generics.Twins -import TcPluginM (lookupOrig) -import TyCoRep () -import Type as GHC.TypeLits.Presburger.Compat (splitTyConApp_maybe) -import Unique as GHC.TypeLits.Presburger.Compat (getKey, getUnique) -#if MIN_VERSION_ghc(8,4,1) -import qualified GHC.TcPluginM.Extra as Extra +#if MIN_VERSION_ghc(8,6,0) +import Plugins as GHC.TypeLits.Presburger.Compat (purePlugin) #endif #if MIN_VERSION_ghc(8,8,1) +import Name +import TysWiredIn as GHC.TypeLits.Presburger.Compat (eqTyConName) import qualified TysWiredIn -#endif -#if MIN_VERSION_ghc(8,8,1) -import TysWiredIn (eqTyConName) #else -import PrelNames (eqTyConName) +import PrelNames as GHC.TypeLits.Presburger.Compat (eqTyConName) #endif #if MIN_VERSION_ghc(8,10,1) @@ -83,7 +172,7 @@ import Type as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole) import TcRnTypes as GHC.TypeLits.Presburger.Compat (ctEvPred, ctEvidence) #endif - +#endif #if MIN_VERSION_ghc(8,10,1) type PredTree = Pred @@ -154,11 +243,15 @@ tcLookupTyCon =<< lookupOrig md (mkTcOcc ":~:") decompFunTy :: Type -> [Type] +#if MIN_VERSION_ghc(9,0,0) +decompFunTy (FunTy _ _ t1 t2) = t1 : decompFunTy t2 +#else #if MIN_VERSION_ghc(8,10,1) decompFunTy (FunTy _ t1 t2) = t1 : decompFunTy t2 #else decompFunTy (FunTy t1 t2) = t1 : decompFunTy t2 #endif +#endif decompFunTy t = [t] newtype TypeEq = TypeEq { runTypeEq :: Type } @@ -232,3 +325,37 @@ | className cls == eqTyConName -> EqPred NomEq t1 t2 e -> e + +#if MIN_VERSION_ghc(9,0,0) +fsToUnitId :: FastString -> UnitId +fsToUnitId = toUnitId . fsToUnit +#endif + +type RawUnitId = FastString +preloadedUnitsM :: TcPluginM [FastString] +#if MIN_VERSION_ghc(9,0,0) +preloadedUnitsM = do + dflags <- hsc_dflags <$> getTopEnv + packs <- tcPluginIO $ preloadUnits . unitState <$> initUnits dflags + let packNames = map (\(UnitId p) -> p) packs + tcPluginTrace "pres: packs" $ ppr packNames + pure packNames +#else +preloadedUnitsM = do + dflags <- hsc_dflags <$> getTopEnv + (_, packs) <- tcPluginIO $ initPackages dflags + let packNames = map (\(InstalledUnitId p) -> p) packs + tcPluginTrace "pres: packs" $ ppr packNames + pure packNames +#endif + + +#if MIN_VERSION_ghc(9,0,0) +type ModuleUnit = Unit +moduleUnit' :: Module -> ModuleUnit +moduleUnit' = moduleUnit +#else +type ModuleUnit = UnitId +moduleUnit' :: Module -> ModuleUnit +moduleUnit' = GHC.moduleUnitId +#endif 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 @@ -23,7 +23,6 @@ ) where -import Class (classTyCon) import Control.Applicative ((<|>)) import Control.Arrow (second) import Control.Monad (forM, forM_, guard, mzero, unless) @@ -32,17 +31,6 @@ import Control.Monad.Trans.Maybe (MaybeT (..)) import Control.Monad.Trans.RWS.Strict (runRWS, tell) import Control.Monad.Trans.State (StateT, runStateT) -#if MIN_VERSION_ghc(8,8,1) -import TysWiredIn (eqTyConName) -#else -import PrelNames (eqTyConName) -#endif - -#if MIN_VERSION_ghc(8,6,0) -import Plugins (purePlugin) -import GhcPlugins (InstalledUnitId, PackageName(..), lookupPackageName, fsToUnitId, lookupPackage) -#endif - import Data.Char (isDigit) import Data.Foldable (asum) import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName) @@ -59,28 +47,7 @@ ) import Data.Reflection (Given, give, given) import qualified Data.Set as Set -import FastString import GHC.TypeLits.Presburger.Compat -import HscTypes (HscEnv (hsc_dflags)) -import Module (InstalledUnitId (InstalledUnitId)) -import Outputable (showSDocUnsafe) -import Packages (initPackages) -import PrelNames -import TcPluginM - ( getTopEnv, - lookupOrig, - newFlexiTyVar, - newWanted, - tcLookupClass, - tcPluginIO, - ) -import Type (mkTyVarTy) -import TysWiredIn - ( promotedEQDataCon, - promotedGTDataCon, - promotedLTDataCon, - ) -import Var assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos) @@ -361,12 +328,10 @@ defaultTranslation :: TcPluginM Translation defaultTranslation = do - dflags <- hsc_dflags <$> getTopEnv - (_, packs) <- tcPluginIO $ initPackages dflags - tcPluginTrace "pres: packs" $ ppr (map (\(InstalledUnitId p) -> p) packs) + packs <- preloadedUnitsM let eqThere = fromMaybe False $ listToMaybe $ do - InstalledUnitId pname <- packs + pname <- packs rest <- maybeToList $ L.stripPrefix "equational-reasoning-" $ unpackFS pname @@ -386,6 +351,7 @@ pure ([], []) eqTyCon_ <- getEqTyCon + eqBoolTyCon <- tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==") eqWitCon_ <- getEqWitnessTyCon vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base") voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void") @@ -395,6 +361,7 @@ { isEmpty = isEmpties , tyEq = [eqTyCon_] , tyEqWitness = [eqWitCon_] + , tyEqBool = [eqBoolTyCon] , isTrue = isTrues , voids = [voidTyCon] , natMinus = [typeNatSubTyCon] @@ -455,6 +422,14 @@ | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l => , con `elem` isTrue given = toPresburgerPred l + | Just (con, ts) <- splitTyConApp_maybe ty + , let n = length ts + , n >= 2 + , [t1, t2] <- drop (n - 2) ts + , typeKind t1 `eqType` typeNatKind + , typeKind t2 `eqType` typeNatKind = + let p = lookup con binPropDic + in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2 | otherwise = parsePred given toPresburgerExp ty splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type]) @@ -473,6 +448,12 @@ , Just (con, [t1, t2]) <- splitTyConAppLastBin p , con `elem` natLeqBool given = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'True + | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b = + toPresburgerPred p +toPresburgerPredTree (EqPred NomEq b p) -- 'True ~ (n :<=? m) + | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b = + toPresburgerPred p toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) | typeKind p `eqType` mkTyConTy promotedBoolTyCon = do lift $ lift $ tcPluginTrace "pres: EQBOOL:" $ ppr (p, q) @@ -522,6 +503,7 @@ ++ [(n, (:>=)) | n <- natGeq given ++ natGeqBool given] ++ [(n, (:==)) | n <- tyEq given ++ tyEqBool given] ++ [(n, (:/=)) | n <- tyNeqBool given] + ++ [(n, (:==)) | n <- tyEqBool given] toPresburgerExp :: Given Translation => Type -> Machine Expr toPresburgerExp ty = case ty of @@ -546,8 +528,8 @@ [tl, tr] | tc `elem` natTimes given -> case (simpleExp tl, simpleExp tr) of (LitTy (NumTyLit n), LitTy (NumTyLit m)) -> return $ K $ n * m - (LitTy (NumTyLit n), x) -> (:*) <$> pure n <*> toPresburgerExp x - (x, LitTy (NumTyLit n)) -> (:*) <$> pure n <*> toPresburgerExp x + (LitTy (NumTyLit n), x) -> (:*) n <$> toPresburgerExp x + (x, LitTy (NumTyLit n)) -> (:*) n <$> toPresburgerExp x _ -> mzero _ -> asum $ @@ -571,10 +553,14 @@ simpleExp :: Given Translation => Type -> Type simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2) +#if MIN_VERSION_ghc(9,0,0) +simpleExp (FunTy f m t1 t2) = FunTy f m (simpleExp t1) (simpleExp t2) +#else #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 #endif simpleExp (ForAllTy t1 t2) = ForAllTy t1 (simpleExp t2) simpleExp (TyConApp tc (lastTwo -> ts)) =