singletons-presburger 0.5.0.0 → 0.6.0.0
raw patch · 3 files changed
+58/−12 lines, 3 filesdep +singletons-basedep +singletons-thdep −ghcPVP ok
version bump matches the API change (PVP)
Dependencies added: singletons-base, singletons-th
Dependencies removed: ghc
API changes (from Hackage documentation)
Files
- examples/simple-arith.hs +9/−0
- singletons-presburger.cabal +27/−6
- src/Data/Singletons/TypeNats/Presburger.hs +22/−6
examples/simple-arith.hs view
@@ -9,6 +9,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-} #endif@@ -20,12 +21,20 @@ module Main where +#if defined(SINGLETONS_BASE)+import Prelude.Singletons+import Data.Singletons.Base.Enum+import Data.Singletons.TH+import GHC.TypeLits.Singletons+#else import Data.Singletons.Decide import Data.Singletons.Prelude import Data.Singletons.Prelude.Enum import Data.Singletons.Prelude.List import Data.Singletons.TH import Data.Singletons.TypeLits+#endif+ import Data.Type.Equality import GHC.TypeLits (CmpNat, Nat, type (<=?)) import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty)
singletons-presburger.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 70dbe672ac6a08a171c823e902bc91918e2e99e85f85577e9d450133c8d5f202+-- hash: 067f024523630b434307a5ddecb854a92115694a3e9c16f2391e96bf77395e8a name: singletons-presburger-version: 0.5.0.0+version: 0.6.0.0 synopsis: Presburger Arithmetic Solver for GHC Type-level natural numbers with Singletons package. description: The @singletons-presburger@ plugin augments GHC type-system with Presburger Arithmetic Solver for Type-level natural numbers, with integration with <https://hackage.haskell.org/package/singletons singletons> package.@@ -24,7 +24,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.1+tested-with: GHC==8.6.5 GHC==8.8.4 GHC==8.10.4 GHC==9.0.1 build-type: Simple source-repository head@@ -46,11 +46,17 @@ ghc-options: -Wall -Wno-dodgy-imports build-depends: base >=4.7 && <5- , ghc >=7.10 && <8.11 , ghc-typelits-presburger >=0.4 , mtl , reflection- , singletons+ if impl(ghc >= 9)+ cpp-options: -DSINGLETONS_BASE+ build-depends:+ singletons+ , singletons-base >=3.0+ else+ build-depends:+ singletons default-language: Haskell2010 executable simple-arith@@ -63,8 +69,23 @@ build-depends: base , equational-reasoning- , singletons , singletons-presburger+ if impl(ghc >= 9)+ cpp-options: -DSINGLETONS_BASE+ build-depends:+ singletons+ , singletons-base >=3.0+ else+ build-depends:+ singletons+ if impl(ghc >= 9)+ cpp-options: -DSINGLETONS_BASE+ build-depends:+ singletons-base >=3.0+ , singletons-th+ else+ build-depends:+ singletons if !(flag(examples)) buildable: False default-language: Haskell2010
src/Data/Singletons/TypeNats/Presburger.hs view
@@ -19,11 +19,8 @@ import Control.Monad import Control.Monad.Trans (MonadTrans (lift)) import Data.Reflection (Given, give, given)-import GHC (mkModule, moduleUnitId) import GHC.TypeLits.Presburger.Compat import GHC.TypeLits.Presburger.Types-import TcPluginM (lookupOrig, matchFam)-import Type (splitTyConApp) plugin :: Plugin plugin =@@ -76,11 +73,30 @@ , falseData = [singFalseSym0] } +singPackage :: FastString+#if defined(MIN_VERISION_singletons_base)+singPackage = "singletons-base"+#else+singPackage = "singletons"+#endif++ordModName, numModName, prelInstName :: ModuleName+#if defined(SINGLETONS_BASE)+ordModName = mkModuleName "Data.Ord.Singletons"+numModName = mkModuleName "GHC.Num.Singletons"+prelInstName = mkModuleName "Data.Singletons.Base.Instances"+#else+ordModName = mkModuleName "Data.Singletons.Prelude.Ord"+numModName = mkModuleName "Data.Singletons.Prelude.Num"+prelInstName = mkModuleName "Data.Singletons.Prelude.Instances"+#endif+ genSingletonCons :: TcPluginM SingletonCons genSingletonCons = do- singletonOrd <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons")- singletonsNum <- lookupModule (mkModuleName "Data.Singletons.Prelude.Num") (fsLit "singletons")- let prel = mkModule (moduleUnitId singletonsNum) (mkModuleName "Data.Singletons.Prelude.Instances")+ singletonOrd <- lookupModule ordModName singPackage+ let singUnit = moduleUnit' singletonOrd+ prel = mkModule singUnit prelInstName+ singletonsNum = mkModule singUnit numModName singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0") singFalseSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "FalseSym0") #if MIN_VERSION_singletons(2,4,1)