ghc-typelits-presburger 0.7.4.1 → 0.7.4.2

raw patch · 5 files changed

+126/−108 lines, 5 filesdep ~ghc-tcplugins-extraPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc-tcplugins-extra

API changes (from Hackage documentation)

Files

• Changelog.md +0/−4
• examples/simple-arith-core.hs +16/−20
• ghc-typelits-presburger.cabal +89/−80
• src/GHC/TypeLits/Presburger/Compat.hs +20/−3
• src/GHC/TypeLits/Presburger/Types.hs +1/−1

@@ -1,9 +1,5 @@ # Changelog -## 0.7.4.1--* Supports GHC 9.8.4- ## 0.7.4.0  * Supports GHC 9.10

@@ -1,34 +1,31 @@ {-# LANGUAGE CPP #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE NoStarIsType #-}-{-# LANGUAGE NoStarIsType #-}-{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -dcore-lint #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} {-# OPTIONS_GHC -ddump-tc-trace -ddump-to-file #-}-+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}  module Main where -import Unsafe.Coerce import Data.Proxy-import Numeric.Natural import Data.Type.Equality-import GHC.TypeLits hiding (SNat) import Data.Void+import GHC.TypeLits hiding (SNat)+import Numeric.Natural import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)+import Unsafe.Coerce #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 import qualified Data.Type.Ord as DTO #endif@@ -42,7 +39,7 @@ type n <=! m = IsTrue (n <=? m)  infix 4 <=!-{- + type family Length (as :: [k]) where   Length '[] = 0   Length (x ': xs) = 1 + Length xs@@ -69,13 +66,13 @@ minusLeq :: (n <= m) => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <=? m) minusLeq _ _ = Witness -absurdTrueFalse :: ( 'True :~: 'False) -> a+absurdTrueFalse :: ('True :~: 'False) -> a absurdTrueFalse = \case {}  hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a hoge _ Witness = absurdTrueFalse Refl -bar :: (2 * (n + 1)) ~ (2 * n + 2) => proxy n -> ()+bar :: ((2 * (n + 1)) ~ (2 * n + 2)) => proxy n -> () bar _ = ()  barResult :: ()@@ -87,12 +84,12 @@ eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1)) eqv _ _ = Refl -predSuccBool :: forall proxy n. (n <=? 0) ~ 'False => proxy n -> IsTrue (n + 1 <=? 2 * n)+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 :: 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 @@ -192,10 +189,10 @@     then unsafeCoerce IsZero     else unsafeCoerce (SNat (n - 1)) -pattern Zero :: forall n. () => n ~ 0 => SNat n+pattern Zero :: forall n. () => (n ~ 0) => SNat n pattern Zero <- (viewNat -> IsZero) -pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n+pattern Succ :: forall n. () => forall n1. (n ~ Succ n1) => SNat n1 -> SNat n pattern Succ n <- (viewNat -> IsSucc n)  {-# COMPLETE Zero, Succ #-}@@ -207,4 +204,3 @@ boolToPropLeq Zero m = ZeroLeq m boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness- -}

@@ -1,39 +1,38 @@-cabal-version: 1.12---- This file has been generated from package.yaml by hpack version 0.36.0.------ see: https://github.com/sol/hpack------ hash: f62c6305d38380eb4cc8063c8e4c4b0056c9bcb01d01075789915680436a7263+cabal-version: 3.4+name: ghc-typelits-presburger+version: 0.7.4.2+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 -name:          ghc-typelits-presburger-version:       0.7.4.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.-               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+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-2025 (c) Hiromi ISHII+license: BSD-3-Clause+license-file: LICENSE+build-type: Simple tested-with:-    GHC==9.2.8 GHC==9.4.8 GHC==9.6.5 GHC==9.8.4 GHC==9.10.1+  ghc ==9.6.7+  ghc ==9.8.4+  ghc ==9.10.2+  ghc ==9.12.2+ extra-source-files:-    Changelog.md-build-type:    Simple+  Changelog.md  source-repository head   type: git@@ -44,66 +43,76 @@   manual: False   default: False +common defaults+  autogen-modules: Paths_ghc_typelits_presburger+  other-modules: Paths_ghc_typelits_presburger+  default-language: Haskell2010+  ghc-options:+    -Wall+    -Wcompat+    -Widentities+    -Wincomplete-record-updates+    -Wincomplete-uni-patterns+    -Wmissing-export-lists+    -Wmissing-home-modules+    -Wpartial-fields+    -Wredundant-constraints+    -Wunused-packages+ library+  import: defaults+  hs-source-dirs: src   exposed-modules:-      GHC.TypeLits.Presburger.Types-      GHC.TypeLits.Presburger-      GHC.TypeLits.Presburger.Compat+    GHC.TypeLits.Presburger+    GHC.TypeLits.Presburger.Compat+    GHC.TypeLits.Presburger.Types+   other-modules:-      Data.Integer.SAT-      GHC.TypeLits.Presburger.Flags-      Paths_ghc_typelits_presburger-  hs-source-dirs:-      src-  ghc-options: -Wall -Wno-dodgy-imports+    Data.Integer.SAT+    GHC.TypeLits.Presburger.Flags+   build-depends:-      base >=4.7 && <5-    , containers-    , ghc <9.13-    , ghc-tcplugins-extra >=0.2 && <0.5-    , mtl-    , pretty-    , reflection-    , syb-    , transformers-  default-language: Haskell2010+    base >=4.7 && <5,+    containers,+    ghc <9.13,+    ghc-tcplugins-extra >=0.2 && <0.6,+    mtl,+    pretty,+    reflection,+    syb,+    transformers,  executable simple-arith-core+  import: defaults   main-is: simple-arith-core.hs-  other-modules:-      Paths_ghc_typelits_presburger-  hs-source-dirs:-      examples-  ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports+  hs-source-dirs: examples   build-depends:-      base-    , equational-reasoning-    , ghc-typelits-presburger-  default-language: Haskell2010+    base,+    equational-reasoning,+    ghc-typelits-presburger,+   if !(flag(examples))     buildable: False  test-suite test-typeltis-presburger+  import: defaults   type: exitcode-stdio-1.0   main-is: test.hs+  hs-source-dirs: test+  -- cabal-gild: discover test --exclude=test/test.hs   other-modules:-      ErrorsNoPlugin-      ErrorsWithPlugin-      GHC.TypeLits.PresburgerSpec-      Shared-      Paths_ghc_typelits_presburger-  hs-source-dirs:-      test-  ghc-options: -Wall -Wno-dodgy-imports-  build-tool-depends:-      tasty-discover:tasty-discover+    ErrorsNoPlugin+    ErrorsWithPlugin+    GHC.TypeLits.PresburgerSpec+    Shared++  build-tool-depends: tasty-discover:tasty-discover   build-depends:-      base-    , equational-reasoning-    , ghc-typelits-presburger-    , tasty-    , tasty-discover-    , tasty-expected-failure-    , tasty-hunit-    , text-  default-language: Haskell2010+    base,+    equational-reasoning,+    ghc-typelits-presburger,+    tasty,+    tasty-discover,+    tasty-expected-failure,+    tasty-hunit,+    text,

@@ -1,3 +1,5 @@+{- HLINT ignore "Use camelCase" -}+{- HLINT ignore "Move filter" -} {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-}@@ -25,7 +27,7 @@ import GHC.Builtin.Names (gHC_TYPENATS, gHC_TYPEERROR) #endif #endif-import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat (CtLoc (..), initialSubGoalDepth)+import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat import GHC.Tc.Types.Origin as GHC.TypeLits.Presburger.Compat (CtOrigin (..)) import GHC.TcPluginM.Extra as GHC.TypeLits.Presburger.Compat (   evByFiat,@@ -37,13 +39,17 @@ import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginSolveResult (..)) import GHC.Builtin.Types as GHC.TypeLits.Presburger.Compat (cTupleTyCon, cTupleDataCon) import GHC.Tc.Types.Evidence as GHC.TypeLits.Presburger.Compat (evCast)-import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo)+import GHC.Plugins as GHC.TypeLits.Presburger.Compat (mkUnivCo, Role(..))+import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (Coercion) import GHC.Core.TyCo.Rep as GHC.TypeLits.Presburger.Compat (UnivCoProvenance(..)) import GHC.Core.DataCon as GHC.TypeLits.Presburger.Compat (dataConWrapId) #else import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) #endif-#if MIN_VERSION_ghc(9,4,1)+#if MIN_VERSION_ghc(9,12,1)+-- mkBaseModule is not available in GHC 9.12.1++import GHC.Core.Reduction (reductionReducedType)+#elif MIN_VERSION_ghc(9,4,1) import GHC.Builtin.Names as GHC.TypeLits.Presburger.Compat (mkBaseModule) import GHC.Core.Reduction (reductionReducedType) #else@@ -74,7 +80,9 @@ import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule) #if MIN_VERSION_ghc(9,2,0) import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags))+#if !MIN_VERSION_ghc(9,12,1) import GHC.Builtin.Names (mkBaseModule)+#endif #else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) import GHC.Driver.Session (unitState, unitDatabases)@@ -182,6 +190,15 @@  #if !MIN_VERSION_ghc(9,4,1) type TcPluginSolveResult = TcPluginResult+#endif++-- mkUnivCo API compatibility+#if MIN_VERSION_ghc(9,12,1)+mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion  +mkUnivCo' prov role ty1 ty2 = mkUnivCo prov [] role ty1 ty2+#else+mkUnivCo' :: UnivCoProvenance -> Role -> Type -> Type -> Coercion  +mkUnivCo' = mkUnivCo #endif  #if MIN_VERSION_ghc(9,10,1)

@@ -362,7 +362,7 @@   | Just (con, lastN 2 -> [_, _]) <- splitTyConApp_maybe prd   , con `elem` assertTy given =      Just $ GHC.Var (dataConWrapId $ cTupleDataCon 0) `evCast`-      mkUnivCo+      mkUnivCo'       (PluginProv $ "ghc-typelits-presburger: extractProof")       Representational       (mkTyConTy (cTupleTyCon 0))