ghc-typelits-presburger 0.6.2.0 → 0.7.0.0

raw patch · 5 files changed

+185/−42 lines, 5 filesdep ~ghcPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• examples/simple-arith-core.hs +24/−0
• ghc-typelits-presburger.cabal +29/−29
• src/GHC/TypeLits/Presburger/Compat.hs +64/−3
• src/GHC/TypeLits/Presburger/Types.hs +56/−9
• test/GHC/TypeLits/PresburgerSpec.hs +12/−1

@@ -27,7 +27,11 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 import qualified Data.Type.Ord as DTO #endif+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904+import Data.Type.Bool+#endif + main :: IO () main = putStrLn "finished" @@ -131,4 +135,24 @@  maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m maxLeq _ _ = Refl+#endif++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 904+leqGeqToEq :: NProxy n -> NProxy m -> IsTrue (n <=? m && m <=? n) -> n :~: m+leqGeqToEq _ _ Witness = Refl++leqTotal :: NProxy n -> NProxy m -> IsTrue (n <=? m || m <=? n)+leqTotal _ _ = Witness++zeroMinimal :: NProxy n -> (n DTO.<? 0) :~: 'False+zeroMinimal _ = Refl++zeroMinimal' :: NProxy n -> IsTrue (Not (n DTO.<? 0))+zeroMinimal' _ = Witness++caseZero :: NProxy n -> IsTrue (If (n DTO.<=? 0) (n == 0) (n DTO.>? 0))+caseZero _ = Witness++succGtZero :: NProxy n -> IsTrue (0 DTO.<? If (n == 0) (n + 1) n)+succGtZero _ = Witness #endif

@@ -1,37 +1,37 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.34.4.+-- This file has been generated from package.yaml by hpack version 0.35.0. -- -- see: https://github.com/sol/hpack ----- hash: 321c5fb49fa1a616b17e9d7403d059fae66cceb781b4b2a12f547a6be9636e5d+-- hash: 5bdb1784549b51d4ed7b1ae34a734767d318511c03ce6a179548a7d14f66498a -name:           ghc-typelits-presburger-version:        0.6.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.-                This plugin only work with GHC builtin operations.-                To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead.-                .-                Since 0.3.0.0, integration with <https://hackage.haskell.org/package/singletons singletons> package moves to <https://hackage.haskell.org/package/singletons-presburger singletons-presburger>.-                .-                You can use by adding this package to @build-depends@ and add the following pragma-                to the head of .hs files:-                .-                .-                > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger-category:       Math, Type System-homepage:       https://github.com/konn/ghc-typelits-presburger#readme-bug-reports:    https://github.com/konn/ghc-typelits-presburger/issues-author:         Hiromi ISHII-maintainer:     konn.jinro _at_ gmail.com-copyright:      2015 (c) Hiromi ISHII-license:        BSD3-license-file:   LICENSE+name:          ghc-typelits-presburger+version:       0.7.0.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.+               This plugin only work with GHC builtin operations.+               To work with those of @singletons@ package, use @ghc-typelits-meta@ and/or @ghc-typelits-presburger@ instead.+               .+               Since 0.3.0.0, integration with <https://hackage.haskell.org/package/singletons singletons> package moves to <https://hackage.haskell.org/package/singletons-presburger singletons-presburger>.+               .+               You can use by adding this package to @build-depends@ and add the following pragma+               to the head of .hs files:+               .+               .+               > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger+category:      Math, Type System+homepage:      https://github.com/konn/ghc-typelits-presburger#readme+bug-reports:   https://github.com/konn/ghc-typelits-presburger/issues+author:        Hiromi ISHII+maintainer:    konn.jinro _at_ gmail.com+copyright:     2015 (c) Hiromi ISHII+license:       BSD3+license-file:  LICENSE tested-with:-    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.1 GHC==9.2.1-build-type:     Simple+    GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.2 GHC==9.2.4 GHC==9.4.3+build-type:    Simple  source-repository head   type: git@@ -56,7 +56,7 @@   build-depends:       base >=4.7 && <5     , containers-    , ghc <9.3+    , ghc <9.5     , ghc-tcplugins-extra >=0.2 && <0.5     , mtl     , pretty@@ -76,9 +76,9 @@       base     , equational-reasoning     , ghc-typelits-presburger+  default-language: Haskell2010   if !(flag(examples))     buildable: False-  default-language: Haskell2010  test-suite test-typeltis-presburger   type: exitcode-stdio-1.0

@@ -10,8 +10,19 @@ 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 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 (..))+#else+import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..))+#endif+#if MIN_VERSION_ghc(9,4,1)+import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (mkBaseModule, gHC_TYPEERROR)+import GHC.Core.Reduction (reductionReducedType)+#else+import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (dATA_TYPE_EQUALITY) import qualified GHC.Builtin.Names as Old+#endif import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsModule(..), NoExtField(..)) import GHC.Hs.ImpExp as GHC.TypeLits.Presburger.Compat (ImportDecl(..), ImportDeclQualifiedStyle(..)) import GHC.Hs.Extension as GHC.TypeLits.Presburger.Compat (GhcPs)@@ -104,7 +115,7 @@     tcPluginIO,     tcPluginTrace,   )-import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..))+import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..)) import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat   ( Ct,     CtEvidence,@@ -209,6 +220,15 @@ #endif #endif +#if !MIN_VERSION_ghc(9,4,1)+type TcPluginSolveResult = TcPluginResult+#endif++#if MIN_VERSION_ghc(9,4,1)+dATA_TYPE_EQUALITY :: Module+dATA_TYPE_EQUALITY = mkBaseModule "Data.Type.Equality"+#endif+ #if MIN_VERSION_ghc(8,10,1) type PredTree = Pred #endif@@ -368,10 +388,19 @@  type RawUnitId = FastString preloadedUnitsM :: TcPluginM [FastString] -#if MIN_VERSION_ghc(9,2,0)+#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+  tcPluginTrace "pres: packs" $ ppr packNames+  pure 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@@ -464,6 +493,15 @@   pure typeNatLeqTyCon #endif +lookupAssertTyCon :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_base(4,17,0)+lookupAssertTyCon = +  fmap Just . tcLookupTyCon =<< lookupOrig gHC_TYPEERROR (mkTcOcc "Assert")+#else+lookupAssertTyCon = pure Nothing+#endif++ lookupTyNatPredLt :: TcPluginM (Maybe TyCon) -- Note:  base library shipepd with 9.2.1 has a wrong implementation; -- hence we MUST NOT desugar it with <= 9.2.1@@ -536,4 +574,27 @@   tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc "Compare") #else lookupTyGenericCompare = pure Nothing+#endif+++lookupBool47 :: String -> TcPluginM (Maybe TyCon)+#if MIN_VERSION_base(4,17,0)+lookupBool47 nam = Just <$> do+  tcLookupTyCon =<< lookupOrig (mkBaseModule "Data.Type.Bool") (mkTcOcc nam)+#else+lookupBool47 = const $ pure Nothing+#endif++lookupTyNot, lookupTyIf, lookupTyAnd, lookupTyOr :: TcPluginM (Maybe TyCon)+lookupTyNot = lookupBool47 "Not"+lookupTyIf = lookupBool47 "If"+lookupTyAnd = lookupBool47 "&&"+lookupTyOr = lookupBool47 "||"+++matchFam' :: TyCon -> [Type] -> TcPluginM (Maybe  Type)+#if MIN_VERSION_ghc(9,4,1)+matchFam' con args = fmap reductionReducedType <$> matchFam con args+#else+matchFam' con args = fmap snd <$> matchFam con args  #endif

@@ -15,6 +15,7 @@ {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE DerivingVia #-}+{-# LANGUAGE NamedFieldPuns #-} -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types   ( pluginWith,@@ -114,8 +115,16 @@     "typelits-presburger"     TcPlugin       { tcPluginInit = return ()-      , tcPluginSolve = decidePresburger mode trans       , tcPluginStop = const $ return ()+#if MIN_VERSION_ghc(9,4,1)+      , tcPluginSolve = const $ \_ gs ws -> decidePresburger mode trans () gs [] ws+#else+      , tcPluginSolve = decidePresburger mode trans+#endif++#if MIN_VERSION_ghc(9,4,1)+      , tcPluginRewrite = mempty+#endif       }  testIf :: PropSet -> Prop -> Proof@@ -167,6 +176,7 @@ data Translation = Translation   { isEmpty :: [TyCon]   , ordCond :: [TyCon]+  , assertTy :: [TyCon]   , isTrue :: [TyCon]   , trueData :: [TyCon]   , falseData :: [TyCon]@@ -174,6 +184,10 @@   , tyEq :: [TyCon]   , tyEqBool :: [TyCon]   , tyEqWitness :: [TyCon]+  , tyNot :: [TyCon]+  , tyAnd :: [TyCon]+  , tyOr :: [TyCon]+  , tyIf :: [TyCon]   , tyNeqBool :: [TyCon]   , natPlus :: [TyCon]   , natMinus :: [TyCon]@@ -202,8 +216,13 @@     Translation       { isEmpty = isEmpty l <> isEmpty r       , isTrue = isTrue l <> isTrue r+      , assertTy = assertTy l <> assertTy r       , voids = voids l <> voids r       , tyEq = tyEq l <> tyEq r+      , tyNot = tyNot l <> tyNot r+      , tyAnd = tyAnd l <> tyAnd r+      , tyOr = tyOr l <> tyOr r+      , tyIf = tyIf l <> tyIf r       , tyEqBool = tyEqBool l <> tyEqBool r       , tyEqWitness = tyEqWitness l <> tyEqWitness r       , tyNeqBool = tyNeqBool l <> tyNeqBool r@@ -237,10 +256,15 @@     Translation       { isEmpty = mempty       , isTrue = mempty+      , assertTy = mempty       , tyEq = mempty       , tyEqBool = mempty       , tyEqWitness = mempty       , tyNeqBool = mempty+      , tyNot = mempty+      , tyAnd = mempty+      , tyOr = mempty+      , tyIf = mempty       , voids = mempty       , natPlus = mempty       , natMinus = mempty@@ -267,7 +291,7 @@       , ordCond = mempty       } -decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult+decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult decidePresburger _ genTrans _ gs [] [] = do   tcPluginTrace "pres: Started givens with: " (ppr $ map (ctEvPred . ctEvidence) gs)   trans <- genTrans@@ -287,7 +311,6 @@     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@@ -355,6 +378,7 @@   eqTyCon_ <- getEqTyCon   eqBoolTyCon <- tcLookupTyCon =<< lookupOrig dATA_TYPE_EQUALITY (mkTcOcc "==")   eqWitCon_ <- getEqWitnessTyCon+  assertTy <- lookupAssertTyCon   vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base")   voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void")   nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq@@ -367,10 +391,19 @@   mTyGtB <- lookupTyNatBoolGt   mOrdCond <- mOrdCondTyCon   mtyGenericCompare <- lookupTyGenericCompare+  tyNot <- maybeToList <$> lookupTyNot+  tyAnd <- maybeToList <$> lookupTyAnd+  tyOr <- maybeToList <$> lookupTyOr+  tyIf <- maybeToList <$> lookupTyIf   let trans =         mempty           { isEmpty = isEmpties+          , assertTy = maybeToList assertTy           , tyEq = [eqTyCon_]+          , tyNot+          , tyAnd+          , tyOr+          , tyIf           , ordCond = F.toList mOrdCond           , tyEqWitness = [eqWitCon_]           , tyEqBool = [eqBoolTyCon]@@ -401,12 +434,6 @@ (<=>) :: Prop -> Prop -> Prop p <=> q = (p :&& q) :|| (Not p :&& Not q) -withEv :: Ct -> (EvTerm, Ct)-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 =   [(lt, (:<)) | lt <- orderingLT given]@@ -420,6 +447,8 @@ toPresburgerPred (TyConApp con (lastN 2 -> [t1, t2]))   | con `elem` (natLeq given ++ natLeqBool given) =     (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2+toPresburgerPred (TyConApp con [t1, _])+  | con `elem` assertTy given = toPresburgerPred t1 toPresburgerPred ty   | Just (con, []) <- splitTyConApp_maybe ty     , con `elem` trueData given =@@ -442,6 +471,21 @@   | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l =>     , con `elem` isTrue given =     toPresburgerPred l+  | Just (con, [l]) <- splitTyConApp_maybe ty -- Not p (from Data.Type.Bool)+    , con `elem` tyNot given =+    Not <$> toPresburgerPred l+  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p && q (from Data.Type.Bool)+    , con `elem` tyAnd given =+    (:&&) <$> toPresburgerPred l <*> toPresburgerPred r+  | Just (con, [l, r]) <- splitTyConApp_maybe ty -- p || q (from Data.Type.Bool)+    , con `elem` tyOr given =+    (:||) <$> toPresburgerPred l <*> toPresburgerPred r+  | Just (con, lastN 3 -> [p, t, f]) <- splitTyConApp_maybe ty -- If p t f (from Data.Type.Bool)+    , con `elem` tyIf given = do+    p' <- toPresburgerPred p+    (:||) +      <$> ((p' :&&) <$> toPresburgerPred t) +      <*> ((Not p':&&) <$> toPresburgerPred f)   | Just (con, [t1, t2]) <- splitTyConAppLastBin ty     , typeKind t1 `eqType` typeNatKind     , typeKind t2 `eqType` typeNatKind @@ -601,6 +645,9 @@ toPresburgerExp :: Given Translation => Type -> Machine Expr toPresburgerExp ty = case ty of   TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t+  TyConApp tc (lastN 3 -> [p, t, f])+    | tc `elem` tyIf given ->+      If <$> toPresburgerPred p <*> toPresburgerExp t <*> toPresburgerExp f    TyConApp tc (lastN 4 -> [cmpNM, l, e, g])     | tc `elem` ordCond given     , TyConApp cmp (lastN 2 -> [n, m]) <- cmpNM

@@ -21,6 +21,9 @@         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 ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith@@ -29,6 +32,8 @@         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 ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith@@ -43,7 +48,10 @@         case eith of           Left (TypeError msg)             | "Could not deduce: n1 ~ n"-                `T.isInfixOf` T.pack msg ->+                `T.isInfixOf` T.pack msg +              || "Could not deduce (n1 ~ n)"+                `T.isInfixOf` T.pack msg +              ->               pure ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith     , testCase "With plugin" $ do@@ -51,6 +59,9 @@         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 ()           _ -> assertFailure $ "TypeError with mismatch expected, but got: " <> show eith