ghc-typelits-presburger 0.5.0.0 → 0.5.2.0

raw patch · 5 files changed

+227/−100 lines, 5 filesdep ~ghcPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• examples/simple-arith-core.hs +13/−1
• ghc-typelits-presburger.cabal +4/−4
• src/GHC/TypeLits/Presburger.hs +7/−5
• src/GHC/TypeLits/Presburger/Compat.hs +178/−51
• src/GHC/TypeLits/Presburger/Types.hs +25/−39

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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)) =