singletons-presburger 0.7.2.0 → 0.7.3.0
raw patch · 4 files changed
+55/−114 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- Changelog.md +5/−0
- examples/simple-arith.hs +11/−37
- singletons-presburger.cabal +11/−28
- src/Data/Singletons/TypeNats/Presburger.hs +28/−49
Changelog.md view
@@ -1,5 +1,10 @@ # Changelog +## 0.7.3.0++* Supports GHC 9.8+* Drops support for GHC <9+ ## 0.7.2.0 * Supports GHC 9.6
examples/simple-arith.hs view
@@ -4,59 +4,33 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE NoStarIsType #-}-#endif-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810-{-# LANGUAGE StandaloneKindSignatures #-}-#endif {-# OPTIONS_GHC -dcore-lint #-} {-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-} 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 GHC.TypeLits.Singletons+import Prelude.Singletons import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) -#if !MIN_VERSION_singletons(2,4,0)-import Data.Promotion.Prelude.Num--type l <= m = l :<= m-type l * m = l :* m-type l + m = l :+ m-type l - m = l :- m-infix 4 <=-infixl 6 +, --infixl 7 *-#endif- type n <=! m = IsTrue (n <=? m) infix 4 <=! natLen ::- (Length xs <= Length ys) ~ 'True =>+ ((Length xs <= Length ys) ~ 'True) => proxy xs -> proxy ys -> (Length ys - Length xs) + Length xs :~: Length ys@@ -68,7 +42,7 @@ leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) <= m) -> CmpNat n m :~: 'LT leqSucc _ _ Witness = Refl -leqEquiv :: (n <= m) ~ 'True => Sing (n :: Nat) -> Sing m -> IsTrue (n <=? m)+leqEquiv :: ((n <= m) ~ 'True) => Sing (n :: Nat) -> Sing m -> IsTrue (n <=? m) leqEquiv _ _ = Witness data NatView (n :: Nat) where@@ -81,10 +55,10 @@ Proved Refl -> IsZero Disproved _emp -> withEmpty _emp $ IsSucc $ sPred sn -plusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m)+plusLeq :: ((n <= m) ~ 'True) => proxy (n :: Nat) -> proxy m -> ((m - n) + n :~: m) plusLeq _ _ = Refl -minusLeq :: (n <= m) ~ 'True => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <= m)+minusLeq :: ((n <= m) ~ 'True) => proxy (n :: Nat) -> proxy m -> IsTrue ((m - n) + n <= m) minusLeq _ _ = Witness (%:<=?) :: Sing (n :: Nat) -> Sing m -> Sing (n <=? m)@@ -108,7 +82,7 @@ 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 :: forall proxy n. (Empty (n <=! 0)) => proxy n -> IsTrue (n + 1 <=? 2 * n) predSucc _ = Witness succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT@@ -120,10 +94,10 @@ eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m eqToRefl _n _m Refl = Refl -minFlip :: (n <= m) ~ 'True => Proxy (m :: Nat) -> Proxy n -> Min m n :~: n+minFlip :: ((n <= m) ~ 'True) => Proxy (m :: Nat) -> Proxy n -> Min m n :~: n minFlip _ _ = Refl -minMax :: (n <= m) ~ 'True => Proxy (m :: Nat) -> Proxy n -> Max m n :~: m+minMax :: ((n <= m) ~ 'True) => Proxy (m :: Nat) -> Proxy n -> Max m n :~: m minMax _ _ = Refl minComm :: Proxy (m :: Nat) -> Proxy n -> Min n m :~: Min m n
singletons-presburger.cabal view
@@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.0.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack ----- hash: 2213630b253991041dc53ede5bf5b932e53a94af97c45f489ffe5958a28071d1+-- hash: 01c951fe1f6f3e8e9be648f36b92368502b685056280abef68bae093cfe61a89 name: singletons-presburger-version: 0.7.2.0+version: 0.7.3.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.@@ -25,7 +25,7 @@ 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.7 GHC==9.4.4 GHC==9.6.1+ GHC==9.0.2 GHC==9.2.7 GHC==9.4.4 GHC==9.6.3 GHC==9.8.1 extra-source-files: Changelog.md build-type: Simple@@ -47,21 +47,16 @@ hs-source-dirs: src ghc-options: -Wall -Wno-dodgy-imports+ cpp-options: -DSINGLETONS_BASE build-depends: base >=4.7 && <5 , ghc , ghc-typelits-presburger >=0.4 , mtl , reflection+ , singletons+ , singletons-base >=3.0 default-language: Haskell2010- if impl(ghc >= 9)- cpp-options: -DSINGLETONS_BASE- build-depends:- singletons- , singletons-base >=3.0- else- build-depends:- singletons executable simple-arith main-is: simple-arith.hs@@ -70,26 +65,14 @@ hs-source-dirs: examples ghc-options: -Wall -Wno-dodgy-imports -Wno-unused-imports+ cpp-options: -DSINGLETONS_BASE build-depends: base , equational-reasoning+ , singletons+ , singletons-base >=3.0 , singletons-presburger+ , singletons-th default-language: Haskell2010- 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
src/Data/Singletons/TypeNats/Presburger.hs view
@@ -10,11 +10,10 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} -module Data.Singletons.TypeNats.Presburger- ( plugin,- singletonTranslation,- )-where+module Data.Singletons.TypeNats.Presburger (+ plugin,+ singletonTranslation,+) where import Control.Monad import Control.Monad.Trans (MonadTrans (lift))@@ -74,22 +73,12 @@ } 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@@ -99,7 +88,6 @@ singletonsNum = mkModule singUnit numModName 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 "<") singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ">=")@@ -107,15 +95,6 @@ singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "+") singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "*") singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc "-")-#else- singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<=")- singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<")- singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>=")- singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>")- singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":+")- singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":*")- singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":-")-#endif singMin <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Min") singMax <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc "Max") caseNameForSingLeq <- getCaseNameForSingletonBinRel singNatLeq@@ -163,14 +142,14 @@ Machine Expr parseSingExpr toE ty | Just (con, [_, l, r, _]) <- splitTyConApp_maybe ty- , Just bin <- lookup con minLikeCaseDic = do- lift $ lift $ tcPluginTrace "hit!" $ ppr (ty, con)- bin <$> toE l <*> toE r+ , Just bin <- lookup con minLikeCaseDic = do+ lift $ lift $ tcPluginTrace "hit!" $ ppr (ty, con)+ bin <$> toE l <*> toE r | otherwise = do- lift $ lift $ tcPluginTrace "I don't know how to read:" $ ppr (ty, splitTyConApp_maybe ty)- mzero+ lift $ lift $ tcPluginTrace "I don't know how to read:" $ ppr (ty, splitTyConApp_maybe ty)+ mzero -minLikeCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Expr)]+minLikeCaseDic :: (Given SingletonCons) => [(TyCon, Expr -> Expr -> Expr)] minLikeCaseDic = [ (caseNameForMin given, Min) , (caseNameForMax given, Max)@@ -184,15 +163,15 @@ parseSingPred toExp ty | isEqPred ty = parseSingPredTree toExp $ classifyPredType ty | Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe ty- , Just bin <- lookup con compCaseDic- , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy- , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =- bin <$> toExp l <*> toExp r+ , Just bin <- lookup con compCaseDic+ , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =+ bin <$> toExp l <*> toExp r | otherwise = do- lift $ lift $ tcPluginTrace "pres: Miokuring" (ppr ty)- mzero+ lift $ lift $ tcPluginTrace "pres: Miokuring" (ppr ty)+ mzero -compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]+compCaseDic :: (Given SingletonCons) => [(TyCon, Expr -> Expr -> Prop)] compCaseDic = [ (caseNameForSingLeq given, (:<=)) , (caseNameForSingLt given, (:<))@@ -201,21 +180,21 @@ ] parseSingPredTree ::- Given SingletonCons =>+ (Given SingletonCons) => (Type -> Machine Expr) -> PredTree -> Machine Prop parseSingPredTree toExp (EqPred NomEq p b) -- (n :<=? m) ~ 'True | Just promotedTrueDataCon == tyConAppTyCon_maybe b -- Singleton's <=...- , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p- , Just bin <- lookup con compCaseDic- , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy- , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =- bin <$> toExp l <*> toExp r+ , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p+ , Just bin <- lookup con compCaseDic+ , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =+ bin <$> toExp l <*> toExp r | Just promotedFalseDataCon == tyConAppTyCon_maybe b -- Singleton's <=...- , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p- , Just bin <- lookup con compCaseDic- , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy- , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =- fmap Not . bin <$> toExp l <*> toExp r+ , Just (con, [_, _, _, _, cmpTy]) <- splitTyConApp_maybe p+ , Just bin <- lookup con compCaseDic+ , Just (cmp, lastTwo -> [l, r]) <- splitTyConApp_maybe cmpTy+ , cmp `elem` [singNatCompare given, typeNatCmpTyCon] =+ fmap Not . bin <$> toExp l <*> toExp r parseSingPredTree _ _ = mzero