diff --git a/Changelog.md b/Changelog.md --- a/Changelog.md +++ b/Changelog.md @@ -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 diff --git a/examples/simple-arith.hs b/examples/simple-arith.hs --- a/examples/simple-arith.hs +++ b/examples/simple-arith.hs @@ -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 diff --git a/singletons-presburger.cabal b/singletons-presburger.cabal --- a/singletons-presburger.cabal +++ b/singletons-presburger.cabal @@ -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 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 diff --git a/src/Data/Singletons/TypeNats/Presburger.hs b/src/Data/Singletons/TypeNats/Presburger.hs --- a/src/Data/Singletons/TypeNats/Presburger.hs +++ b/src/Data/Singletons/TypeNats/Presburger.hs @@ -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