ghc-typelits-presburger 0.7.1.0 → 0.7.2.0

raw patch · 7 files changed

+199/−61 lines, 7 filesdep ~ghcdep ~ghc-typelits-presburgerPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc, ghc-typelits-presburger

API changes (from Hackage documentation)

Files

• Changelog.md +44/−0
• examples/simple-arith-core.hs +10/−5
• ghc-typelits-presburger.cabal +8/−5
• src/GHC/TypeLits/Presburger/Compat.hs +82/−20
• src/GHC/TypeLits/Presburger/Flags.hs +26/−0
• src/GHC/TypeLits/Presburger/Types.hs +6/−8
• test/GHC/TypeLits/PresburgerSpec.hs +23/−23

@@ -0,0 +1,44 @@+# Changelog++## 0.7.2.0++* Supports GHC 9.6+* More robust `equational-reasoning` package detection logic.++## 0.7.1.0++* Proper Support of GHC 9.4 (Now can solve `Assert` properly)++## 0.7.0.0++* Support GHC 9.4+* The plugin can solve constraints involving type-level `Assert`, `Not`, `(&&)`, `(||)`, and/or `If` from new base.++## 0.6.2.0++* Support GHC 9.2.1+* Decoding in Min/Max expression in terms of OrdCond++## 0.6.0.0++* Stop discharging redundant constraints+* Support GHC 9.0.1+* Drop a support for GHC <8.6++## 0.4.0.0++* Fixes constraint solving (fixes #9); this may change the previous (unsound) behaviour, and hence it is breaking change.++## 0.3.0.1++* Supports GHC >= 8.10.++## 0.3.0.0++* Drops support for GHC < 8.4+* Entire overhaul.+* Adds `negated-numbers` option.+* Allows terms which includes uninterpreted terms (still much incomplete).+* Separates `singletons` support as `singletons-presburger` package.+* Provides an interface for extending solver with additional syntax constructs.+  See `GHC.TypeLits.Presburger.Types` module for more detail.

@@ -14,6 +14,7 @@ {-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -dcore-lint #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}+{-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-}@@ -27,7 +28,7 @@ import Data.Proxy import Numeric.Natural import Data.Type.Equality-import GHC.TypeLits+import GHC.TypeLits hiding (SNat) import Data.Void import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902@@ -43,7 +44,7 @@ type n <=! m = IsTrue (n <=? m)  infix 4 <=!-+{-  type family Length (as :: [k]) where   Length '[] = 0   Length (x ': xs) = 1 + Length xs@@ -90,9 +91,12 @@ eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1)) eqv _ _ = Refl -predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)-predSucc _ = Witness-+predSuccBool :: forall proxy n. (n <=? 0) ~ 'False => proxy n -> IsTrue (n + 1 <=? 2 * n)+predSuccBool _ = Witness+ -}+predSuccProp :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)+predSuccProp _ = Witness+{-  succLEqLTSucc :: pxy m -> CmpNat 0 (m + 1) :~: 'LT succLEqLTSucc _ = Refl @@ -207,3 +211,4 @@ boolToPropLeq Zero m = ZeroLeq m boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness+ -}

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: d6484409d9fcbd50b1fb2f56f79743a1587a1330768401bbaeecaa4e969e8160+-- hash: d47f404951bd3c54bbbabe3cea49f853ffe14cf61c99382f7240c493409fcdda  name:          ghc-typelits-presburger-version:       0.7.1.0+version:       0.7.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.@@ -30,7 +30,9 @@ license:       BSD3 license-file:  LICENSE tested-with:-    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.4 GHC==9.4.3+    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.7 GHC==9.4.4 GHC==9.6.1+extra-source-files:+    Changelog.md build-type:    Simple  source-repository head@@ -49,6 +51,7 @@       GHC.TypeLits.Presburger.Compat   other-modules:       Data.Integer.SAT+      GHC.TypeLits.Presburger.Flags       Paths_ghc_typelits_presburger   hs-source-dirs:       src@@ -56,7 +59,7 @@   build-depends:       base >=4.7 && <5     , containers-    , ghc <9.5+    , ghc <9.7     , ghc-tcplugins-extra >=0.2 && <0.5     , mtl     , pretty@@ -75,7 +78,7 @@   build-depends:       base     , equational-reasoning-    , ghc-typelits-presburger >=0.7.1.0+    , ghc-typelits-presburger   default-language: Haskell2010   if !(flag(examples))     buildable: False

@@ -8,8 +8,10 @@ import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (evByFiat, lookupModule, lookupName,                                           tracePlugin) import Data.Generics.Twins+import Data.Coerce (coerce)  #if MIN_VERSION_ghc(9,0,0)+import Data.Functor ((<&>)) import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (gHC_TYPENATS) #if MIN_VERSION_ghc(9,4,1) import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..))@@ -55,7 +57,7 @@ import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) #else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))-import GHC.Driver.Session (unitState)+import GHC.Driver.Session (unitState, unitDatabases) #endif import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit, Name) #if MIN_VERSION_ghc(9,2,0)@@ -70,18 +72,36 @@   ) #endif +#if MIN_VERSION_ghc(9,6,1) import GHC.Plugins as GHC.TypeLits.Presburger.Compat+  ( Subst (..),+    emptySubst,+    unionSubst,+  )+import GHC.Core.TyCo.Compare as GHC.TypeLits.Presburger.Compat+  (eqType)+#else+import GHC.Plugins as GHC.TypeLits.Presburger.Compat+  ( TCvSubst (..),+    emptyTCvSubst,+    eqType,+    unionTCvSubst,+  )+#endif++import GHC.Plugins as GHC.TypeLits.Presburger.Compat   ( PackageName (..),isStrLitTy, isNumLitTy,     nilDataCon, consDataCon,     Hsc,     Plugin (..),-    TCvSubst (..),     TvSubstEnv,     TyVar,     defaultPlugin,-    emptyTCvSubst,-    eqType,     mkTcOcc,+    UnitDatabase(..),+    GenericUnitInfo(..),+    elementOfUniqSet,+    mkUniqSet,     mkTyConTy,     mkTyVarTy,     ppr,@@ -93,14 +113,12 @@     text,     tyConAppTyCon_maybe,     typeKind,-    unionTCvSubst,   ) import GHC.Tc.Plugin (lookupOrig) import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances) #if MIN_VERSION_ghc(9,2,0) import GHC.Tc.Plugin (unsafeTcPluginTcM) import GHC.Utils.Logger (getLogger)-import Data.Functor ((<&>)) import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..)) #else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..))@@ -141,9 +159,11 @@ import GHC.Utils.Outputable as GHC.TypeLits.Presburger.Compat (showSDocUnsafe) -- GHC 9 Ends HERE #else+import UniqSet+import PackageConfig 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, Name)+import GhcPlugins (InScopeSet, Outputable, emptyUFM, InstalledUnitId(..), initPackages, Name, listPackageConfigMap) 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)@@ -242,25 +262,52 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 data TvSubst = TvSubst InScopeSet TvSubstEnv +#if MIN_VERSION_ghc(9,6,1)+type TCvSubst = Subst+unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst+unionTCvSubst = unionSubst++emptyTCvSubst :: Subst+emptyTCvSubst = emptySubst+#endif++ instance Outputable  TvSubst where   ppr = ppr . toTCv  emptyTvSubst :: TvSubst+#if MIN_VERSION_ghc(9,6,1) emptyTvSubst = case emptyTCvSubst of+  Subst set _ tvsenv _ -> TvSubst set tvsenv+#else+emptyTvSubst = case emptyTCvSubst of   TCvSubst set tvsenv _ -> TvSubst set tvsenv+#endif + toTCv :: TvSubst -> TCvSubst+#if MIN_VERSION_ghc(9,6,1)+toTCv (TvSubst set tvenv) = Subst set emptyUFM tvenv emptyUFM+#else toTCv (TvSubst set tvenv) = TCvSubst set tvenv emptyUFM+#endif + substTy :: TvSubst -> Type -> Type substTy tvs = Old.substTy (toTCv tvs)  unionTvSubst :: TvSubst -> TvSubst -> TvSubst unionTvSubst s1 s2 =   fromTCv $ unionTCvSubst (toTCv s1) (toTCv s2)+ fromTCv :: TCvSubst -> TvSubst+#if MIN_VERSION_ghc(9,6,1)+fromTCv (Subst set _ tvsenv _) = TvSubst set tvsenv+#else fromTCv (TCvSubst set tvsenv _) = TvSubst set tvsenv+#endif + promotedBoolTyCon :: TyCon promotedBoolTyCon = boolTyCon @@ -391,38 +438,53 @@ fsToUnitId = toUnitId . fsToUnit #endif -type RawUnitId = FastString-preloadedUnitsM :: TcPluginM [FastString] +#if MIN_VERSION_ghc(9,0,0)+loadedPackageNames ::+  [UnitDatabase UnitId] ->+  UnitState ->+  [RawPackageName]+loadedPackageNames unitDb us =+  let preloads = mkUniqSet $ map (\(UnitId p) -> p) $ preloadUnits us+      ents = filter ((`elementOfUniqSet` preloads) . unitIdFS . unitId) $ concatMap unitDatabaseUnits unitDb+   in map (coerce . unitPackageName) ents+#endif+++type RawPackageName = FastString+preloadedUnitsM :: TcPluginM [RawPackageName]  #if MIN_VERSION_ghc(9,4,0) preloadedUnitsM = do   logger <- unsafeTcPluginTcM getLogger   dflags <- hsc_dflags <$> getTopEnv-  packs <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> -    \(_, us, _, _ ) -> preloadUnits us-  let packNames = map (\(UnitId p) -> p) packs+  packNames <- tcPluginIO $ initUnits logger dflags Nothing mempty <&> +    \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us   tcPluginTrace "pres: packs" $ ppr packNames-  pure packNames+  pure $ coerce packNames #elif MIN_VERSION_ghc(9,2,0) preloadedUnitsM = do   logger <- unsafeTcPluginTcM getLogger   dflags <- hsc_dflags <$> getTopEnv-  packs <- tcPluginIO $ initUnits logger dflags Nothing <&> -    \(_, us, _, _ ) -> preloadUnits us-  let packNames = map (\(UnitId p) -> p) packs+  packNames <- tcPluginIO $ initUnits logger dflags Nothing <&> +    \(unitDb, us, _, _ ) -> loadedPackageNames unitDb us   tcPluginTrace "pres: packs" $ ppr packNames   pure packNames #elif 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+  packNames <- tcPluginIO $ initUnits dflags <&> \dfs' ->+    let st = unitState dfs'+        db = maybe [] id $ unitDatabases dfs'+     in loadedPackageNames db st   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+  (dfs', packs) <- tcPluginIO $ initPackages dflags+  let db = listPackageConfigMap dfs'+      loadeds = mkUniqSet $ map (\(InstalledUnitId p) -> p) packs+      packNames = map (coerce . packageName) $+        filter ((`elementOfUniqSet` loadeds) . coerce . unitId) db   tcPluginTrace "pres: packs" $ ppr packNames   pure packNames #endif

@@ -0,0 +1,26 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE CPP #-}+module GHC.TypeLits.Presburger.Flags (GHCVer(..), ghcVer) where+import GHC.Generics (Generic)++data GHCVer +  = GHC806 | GHC808 | GHC810 +  | GHC900 | GHC902 | GHC904 | GHC906+  deriving (Show, Eq, Ord, Generic)++ghcVer :: GHCVer+#if MIN_VERSION_ghc(9,6,1)+ghcVer = GHC906+#elif MIN_VERSION_ghc(9,4,1)+ghcVer = GHC904+#elif MIN_VERSION_ghc(9,2,1)+ghcVer = GHC902+#elif MIN_VERSION_ghc(9,0,1)+ghcVer = GHC900+#elif MIN_VERSION_ghc(8,10,1)+ghcVer = GHC810+#elif MIN_VERSION_ghc(8,8,1)+ghcVer = GHC808+#else+ghcVer = GHC806+#endif

@@ -58,6 +58,7 @@ import qualified Data.Set as Set import GHC.TypeLits.Presburger.Compat as Compat import qualified Data.Foldable as F+import GHC.TypeLits.Presburger.Flags  assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos)@@ -376,13 +377,7 @@ defaultTranslation :: TcPluginM Translation defaultTranslation = do   packs <- preloadedUnitsM-  let eqThere = fromMaybe False $-        listToMaybe $ do-          pname <- packs-          rest <--            maybeToList $-              L.stripPrefix "equational-reasoning-" $ unpackFS pname-          pure $ null rest || isDigit (head rest)+  let eqThere = elem eqReasoning packs   (isEmpties, isTrues) <-     if eqThere       then do@@ -401,7 +396,10 @@   eqBoolTyCon <- tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==")   eqWitCon_ <- getEqWitnessTyCon   assertTy <- lookupAssertTyCon-  vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")+  vmd <- +    if ghcVer >= GHC906+    then lookupModule (mkModuleName "GHC.Base") (fsLit "base")+    else lookupModule (mkModuleName "Data.Void") (fsLit "base")   voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")   nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq   tyLeqB <- lookupTyNatBoolLeq

@@ -20,22 +20,22 @@         eith <- try $ void (evaluate $ NoPlugin.zipMVec (True :- Nil) (() :- Nil))         case eith of           Left (TypeError msg)-            | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"-                `T.isInfixOf` T.pack msg -              || -              "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"-                `T.isInfixOf` T.pack msg ->-              pure ()+            | any (`T.isInfixOf` T.pack msg)+              [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"+              , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"+              , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’"+              ]+              -> pure ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith     , testCase "With plugin" $ do         eith <- try $ void (evaluate $ Plugin.zipMVec (True :- Nil) (() :- Nil))         case eith of           Left (TypeError msg)-            | "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"-                `T.isInfixOf` T.pack msg -              || "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"-                `T.isInfixOf` T.pack msg ->-              pure ()+            | any (`T.isInfixOf` T.pack msg)+              [ "Could not deduce: (n GHC.TypeNats.+ 1) ~ n"+              , "Could not deduce ((n GHC.TypeNats.+ 1) ~ n)"+              , "Could not deduce ‘(n GHC.TypeNats.+ 1) ~ n’"+              ] -> pure ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith     ] @@ -47,22 +47,22 @@         eith <- try $ void (evaluate $ NoPlugin.unSpin (True :- Nil))         case eith of           Left (TypeError msg)-            | "Could not deduce: n1 ~ n"-                `T.isInfixOf` T.pack msg -              || "Could not deduce (n1 ~ n)"-                `T.isInfixOf` T.pack msg -              ->-              pure ()+            | any (`T.isInfixOf` T.pack msg )+              [ "Could not deduce: n1 ~ n"+              , "Could not deduce (n1 ~ n)"+              , "Could not deduce ‘n1 ~ n’"+              ]+              -> pure ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith     , testCase "With plugin" $ do         eith <- try $ void (evaluate $ Plugin.unSpin (True :- Nil))         case eith of           Left (TypeError msg)-            | "Could not deduce: n1 ~ n"-                `T.isInfixOf` T.pack msg -              || -              "Could not deduce (n1 ~ n)"-                `T.isInfixOf` T.pack msg ->-              pure ()+            | any (`T.isInfixOf` T.pack msg )+              [ "Could not deduce: n1 ~ n"+              , "Could not deduce (n1 ~ n)"+              , "Could not deduce ‘n1 ~ n’"+              ]+              -> pure ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith     ]