singletons-presburger 0.3.0.0 → 0.3.0.1
raw patch · 3 files changed
+15/−6 lines, 3 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- examples/simple-arith.hs +3/−0
- singletons-presburger.cabal +4/−4
- src/Data/Singletons/TypeNats/Presburger.hs +8/−2
examples/simple-arith.hs view
@@ -6,6 +6,9 @@ #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-} #endif+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810+{-# LANGUAGE StandaloneKindSignatures #-}+#endif module Main where import Data.Singletons.Decide
singletons-presburger.cabal view
@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.31.2.+-- This file has been generated from package.yaml by hpack version 0.33.0. -- -- see: https://github.com/sol/hpack ----- hash: 1398143e2ff5a7650c68eda0c0513d0db5b5ed760488ce49e28425fa4f97830c+-- hash: b271b824f909f5d2533590977ec2a9e9d107034176402483ca143b699d7d46cd name: singletons-presburger-version: 0.3.0.0+version: 0.3.0.1 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.2+tested-with: GHC==8.4.3 GHC==8.6.3 GHC==8.8.3 GHC==8.10.1 build-type: Simple source-repository head
src/Data/Singletons/TypeNats/Presburger.hs view
@@ -9,6 +9,7 @@ import Control.Monad import Data.Reflection (Given, give, given)+import GHC (mkModule, moduleUnitId) import TcPluginM (lookupOrig, matchFam) import Type (splitTyConApp) @@ -26,6 +27,8 @@ , singNatMinus :: TyCon , singNatTimes :: TyCon , singNatCompare :: TyCon+ , singTrueSym0 :: TyCon+ , singFalseSym0 :: TyCon , caseNameForSingLeq :: TyCon , caseNameForSingGeq :: TyCon , caseNameForSingLt :: TyCon@@ -50,14 +53,17 @@ , natMinus = [singNatMinus] , natTimes = [singNatTimes] , parsePred = parseSingPred+ , trueData = [singTrueSym0]+ , falseData = [singFalseSym0] } genSingletonCons :: TcPluginM SingletonCons genSingletonCons = do singletonOrd <- lookupModule (mkModuleName "Data.Singletons.Prelude.Ord") (fsLit "singletons") singletonsNum <- lookupModule (mkModuleName "Data.Singletons.Prelude.Num") (fsLit "singletons")- -- prel <- lookupModule (mkModuleName "Data.Singletons.Prelude") (fsLit "singletons")- -- singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")+ let prel = mkModule (moduleUnitId singletonsNum) (mkModuleName "Data.Singletons.Prelude.Instances")+ singTrueSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "TrueSym0")+ singFalseSym0 <- tcLookupTyCon =<< lookupOrig prel (mkTcOcc "FalseSym0") #if MIN_VERSION_singletons(2,4,1) singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<=") singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "<")